[Merged by Bors] - feat(algebra/pointwise): make instances global

src/algebraic_geometry/prime_spectrum.lean

@@ -176,7 +176,7 @@ lemma zero_locus_bot :
 (gc R).l_bot
 
 @[simp] lemma zero_locus_singleton_zero :
-  zero_locus ({0} : set R) = set.univ :=
+  zero_locus (0 : set R) = set.univ :=
 zero_locus_bot
 
 @[simp] lemma zero_locus_empty :

src/analysis/convex/basic.lean

@@ -48,8 +48,6 @@ open_locale classical big_operators
 
 local notation `I` := (Icc 0 1 : set ℝ)
 
-local attribute [instance] set.pointwise_add set.smul_set
-
 section sets
 
 /-! ### Segment -/
@@ -145,11 +143,11 @@ lemma convex_iff_pointwise_add_subset:
   convex s ↔ ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s :=
 iff.intro
   begin
-    rintros hA a b ha hb hab w ⟨au, ⟨u, hu, rfl⟩, bv, ⟨v, hv, rfl⟩, rfl⟩,
+    rintros hA a b ha hb hab w ⟨au, bv, ⟨u, hu, rfl⟩, ⟨v, hv, rfl⟩, rfl⟩,
     exact hA hu hv ha hb hab
   end
   (λ h x y hx hy a b ha hb hab,
-    (h ha hb hab) (set.add_mem_pointwise_add ⟨_, hx, rfl⟩ ⟨_, hy, rfl⟩))
+    (h ha hb hab) (set.add_mem_add ⟨_, hx, rfl⟩ ⟨_, hy, rfl⟩))
 
 /-- Alternative definition of set convexity, using division -/
 lemma convex_iff_div:
@@ -235,15 +233,15 @@ hs.is_linear_preimage is_linear_map.is_linear_map_neg
 
 lemma convex.smul (c : ℝ) (hs : convex s) : convex (c • s) :=
 begin
-  rw smul_set_eq_image,
+  rw ← image_smul,
   exact hs.is_linear_image (is_linear_map.is_linear_map_smul c)
 end
 
 lemma convex.smul_preimage (c : ℝ) (hs : convex s) : convex ((λ z, c • z) ⁻¹' s) :=
 hs.is_linear_preimage (is_linear_map.is_linear_map_smul c)
 
 lemma convex.add {t : set E}  (hs : convex s) (ht : convex t) : convex (s + t) :=
-by { rw pointwise_add_eq_image, exact (hs.prod ht).is_linear_image is_linear_map.is_linear_map_add }
+by { rw ← add_image_prod, exact (hs.prod ht).is_linear_image is_linear_map.is_linear_map_add }
 
 lemma convex.sub {t : set E}  (hs : convex s) (ht : convex t) :
   convex ((λx : E × E, x.1 - x.2) '' (s.prod t)) :=
@@ -253,13 +251,13 @@ lemma convex.translate (hs : convex s) (z : E) : convex ((λx, z + x) '' s) :=
 begin
   convert (convex_singleton z).add hs,
   ext x,
-  simp [set.mem_image, mem_pointwise_add, eq_comm]
+  simp [set.mem_image, mem_add, eq_comm]
 end
 
 lemma convex.affinity (hs : convex s) (z : E) (c : ℝ) : convex ((λx, z + c • x) '' s) :=
 begin
   convert (hs.smul c).translate z using 1,
-  erw [smul_set_eq_image, ←image_comp]
+  erw [← image_smul, ←image_comp]
 end
 
 lemma convex_real_iff {s : set ℝ} :

src/analysis/convex/cone.lean

@@ -193,15 +193,13 @@ end convex_cone
 
 namespace convex
 
-local attribute [instance] smul_set
-
 /-- The set of vectors proportional to those in a convex set forms a convex cone. -/
 def to_cone (s : set E) (hs : convex s) : convex_cone E :=
 begin
   apply convex_cone.mk (⋃ c > 0, (c : ℝ) • s);
     simp only [mem_Union, mem_smul_set],
   { rintros c c_pos _ ⟨c', c'_pos, x, hx, rfl⟩,
-    exact ⟨c * c', mul_pos c_pos c'_pos, x, hx, smul_smul _ _ _⟩ },
+    exact ⟨c * c', mul_pos c_pos c'_pos, x, hx, (smul_smul _ _ _).symm⟩ },
   { rintros _ ⟨cx, cx_pos, x, hx, rfl⟩ _ ⟨cy, cy_pos, y, hy, rfl⟩,
     have : 0 < cx + cy, from add_pos cx_pos cy_pos,
     refine ⟨_, this, _, convex_iff_div.1 hs hx hy (le_of_lt cx_pos) (le_of_lt cy_pos) this, _⟩,
@@ -212,7 +210,7 @@ variables {s : set E} (hs : convex s) {x : E}
 
 @[nolint ge_or_gt]
 lemma mem_to_cone : x ∈ hs.to_cone s ↔ ∃ (c > 0) (y ∈ s), (c : ℝ) • y = x :=
-by simp only [to_cone, convex_cone.mem_mk, mem_Union, mem_smul_set, eq_comm]
+by simp only [to_cone, convex_cone.mem_mk, mem_Union, mem_smul_set, eq_comm, exists_prop]
 
 @[nolint ge_or_gt]
 lemma mem_to_cone' : x ∈ hs.to_cone s ↔ ∃ c > 0, (c : ℝ) • x ∈ s :=

src/analysis/convex/topology.lean

@@ -71,26 +71,20 @@ section topological_vector_space
 variables [add_comm_group E] [vector_space ℝ E] [topological_space E]
   [topological_add_group E] [topological_vector_space ℝ E]
 
-local attribute [instance] set.pointwise_add set.smul_set
-
 /-- In a topological vector space, the interior of a convex set is convex. -/
 lemma convex.interior {s : set E} (hs : convex s) : convex (interior s) :=
 convex_iff_pointwise_add_subset.mpr $ λ a b ha hb hab,
   have h : is_open (a • interior s + b • interior s), from
   or.elim (classical.em (a = 0))
   (λ heq,
     have hne : b ≠ 0, by { rw [heq, zero_add] at hab, rw hab, exact one_ne_zero },
-    (smul_set_eq_image b (interior s)).symm ▸
-    (is_open_pointwise_add_left ((is_open_map_smul_of_ne_zero hne _) is_open_interior)))
+    by { rw ← image_smul, apply is_open_add_left,
+         exact is_open_map_smul_of_ne_zero hne _ is_open_interior } )
   (λ hne,
-    (smul_set_eq_image a (interior s)).symm ▸
-    (is_open_pointwise_add_right ((is_open_map_smul_of_ne_zero hne _) is_open_interior))),
+    by { rw ← image_smul, apply is_open_add_right,
+         exact is_open_map_smul_of_ne_zero hne _ is_open_interior }),
   (subset_interior_iff_subset_of_open h).mpr $ subset.trans
-    begin
-      apply pointwise_add_subset_add;
-      rw [smul_set_eq_image, smul_set_eq_image];
-      exact image_subset _ interior_subset
-    end
+    (by { simp only [← image_smul], apply add_subset_add; exact image_subset _ interior_subset })
     (convex_iff_pointwise_add_subset.mp hs ha hb hab)
 
 /-- In a topological vector space, the closure of a convex set is convex. -/

src/data/set/basic.lean

@@ -240,6 +240,8 @@ in theorem assumptions instead of `∃ x, x ∈ s` or `s ≠ ∅` as it gives ac
 to the dot notation. -/
 protected def nonempty (s : set α) : Prop := ∃ x, x ∈ s
 
+lemma nonempty_def : s.nonempty ↔ ∃ x, x ∈ s := iff.rfl
+
 lemma nonempty_of_mem {x} (h : x ∈ s) : s.nonempty := ⟨x, h⟩
 
 theorem nonempty.not_subset_empty : s.nonempty  → ¬(s ⊆ ∅)
@@ -763,7 +765,7 @@ lemma mem_compl_singleton_iff {a x : α} : x ∈ ({a} : set α)ᶜ ↔ x ≠ a :
 not_iff_not_of_iff mem_singleton_iff
 
 lemma compl_singleton_eq (a : α) : ({a} : set α)ᶜ = {x | x ≠ a} :=
-ext $ λ x,  mem_compl_singleton_iff
+ext $ λ x, mem_compl_singleton_iff
 
 theorem union_eq_compl_compl_inter_compl (s t : set α) : s ∪ t = (sᶜ ∩ tᶜ)ᶜ :=
 by simp [compl_inter, compl_compl]
@@ -1065,8 +1067,6 @@ section image
 
 infix ` '' `:80 := image
 
--- TODO(Jeremy): use bounded exists in image
-
 theorem mem_image_iff_bex {f : α → β} {s : set α} {y : β} :
   y ∈ f '' s ↔ ∃ x (_ : x ∈ s), f x = y := bex_def.symm
 
@@ -1075,6 +1075,8 @@ theorem mem_image_eq (f : α → β) (s : set α) (y: β) : y ∈ f '' s = ∃ x
 @[simp] theorem mem_image (f : α → β) (s : set α) (y : β) :
   y ∈ f '' s ↔ ∃ x, x ∈ s ∧ f x = y := iff.rfl
 
+lemma image_eta (f : α → β) : f '' s = (λ x, f x) '' s := rfl
+
 theorem mem_image_of_mem (f : α → β) {x : α} {a : set α} (h : x ∈ a) : f x ∈ f '' a :=
 ⟨_, h, rfl⟩
 
@@ -1118,13 +1120,6 @@ theorem image_comp (f : β → γ) (g : α → β) (a : set α) : (f ∘ g) '' a
 subset.antisymm
   (ball_image_of_ball $ assume a ha, mem_image_of_mem _ $ mem_image_of_mem _ ha)
   (ball_image_of_ball $ ball_image_of_ball $ assume a ha, mem_image_of_mem _ ha)
-/- Proof is removed as it uses generated names
-TODO(Jeremy): make automatic,
-begin
-  safe [ext_iff, iff_def, mem_image, (∘)],
-  have h' := h_2 (g a_2),
-  finish
-end -/
 
 /-- A variant of `image_comp`, useful for rewriting -/
 lemma image_image (g : β → γ) (f : α → β) (s : set α) : g '' (f '' s) = (λ x, g (f x)) '' s :=
@@ -1878,25 +1873,9 @@ ext $ λ ⟨x, hx⟩ , by simp [inclusion]
 
 end inclusion
 
-end set
-
-namespace subsingleton
-
-variables {α : Type*} [subsingleton α]
-
-lemma eq_univ_of_nonempty {s : set α} : s.nonempty → s = univ :=
-λ ⟨x, hx⟩, eq_univ_of_forall $ λ y, subsingleton.elim x y ▸ hx
-
-@[elab_as_eliminator]
-lemma set_cases {p : set α → Prop} (h0 : p ∅) (h1 : p univ) (s) : p s :=
-s.eq_empty_or_nonempty.elim (λ h, h.symm ▸ h0) $ λ h, (eq_univ_of_nonempty h).symm ▸ h1
-
-end subsingleton
-
-namespace set
-
+/-! ### Injectivity and surjectivity lemmas for image and preimage -/
+section image_preimage
 variables {α : Type u} {β : Type v} {f : α → β}
-
 @[simp]
 lemma preimage_injective : injective (preimage f) ↔ surjective f :=
 begin
@@ -1928,5 +1907,167 @@ begin
   rw [← singleton_eq_singleton_iff], apply h,
   rw [image_singleton, image_singleton, hx]
 end
+end image_preimage
+
+/-! ### Lemmas about images of binary and ternary functions -/
+
+section n_ary_image
+
+variables {α β γ δ ε : Type*} {f f' : α → β → γ} {g g' : α → β → γ → δ}
+variables {s s' : set α} {t t' : set β} {u u' : set γ} {a a' : α} {b b' : β} {c c' : γ} {d d' : δ}
+
+
+/-- The image of a binary function `f : α → β → γ` as a function `set α → set β → set γ`.
+  Mathematically this should be thought of as the image of the corresponding function `α × β → γ`.
+-/
+def image2 (f : α → β → γ) (s : set α) (t : set β) : set γ :=
+{c | ∃ a b, a ∈ s ∧ b ∈ t ∧ f a b = c }
+
+lemma mem_image2_eq : c ∈ image2 f s t = ∃ a b, a ∈ s ∧ b ∈ t ∧ f a b = c := rfl
+
+@[simp] lemma mem_image2 : c ∈ image2 f s t ↔ ∃ a b, a ∈ s ∧ b ∈ t ∧ f a b = c := iff.rfl
+
+lemma mem_image2_of_mem (h1 : a ∈ s) (h2 : b ∈ t) : f a b ∈ image2 f s t :=
+⟨a, b, h1, h2, rfl⟩
+
+lemma mem_image2_iff (hf : injective2 f) : f a b ∈ image2 f s t ↔ a ∈ s ∧ b ∈ t :=
+⟨ by { rintro ⟨a', b', ha', hb', h⟩, rcases hf h with ⟨rfl, rfl⟩, exact ⟨ha', hb'⟩ },
+  λ ⟨ha, hb⟩, mem_image2_of_mem ha hb⟩
+
+/-- image2 is monotone with respect to `⊆`. -/
+lemma image2_subset (hs : s ⊆ s') (ht : t ⊆ t') : image2 f s t ⊆ image2 f s' t' :=
+by { rintro _ ⟨a, b, ha, hb, rfl⟩, exact mem_image2_of_mem (hs ha) (ht hb) }
+
+lemma image2_union_left : image2 f (s ∪ s') t = image2 f s t ∪ image2 f s' t :=
+begin
+  ext c, split,
+  { rintros ⟨a, b, h1a|h2a, hb, rfl⟩;[left, right]; exact ⟨_, _, ‹_›, ‹_›, rfl⟩ },
+  { rintro (⟨_, _, _, _, rfl⟩|⟨_, _, _, _, rfl⟩); refine ⟨_, _, _, ‹_›, rfl⟩; simp [mem_union, *] }
+end
+
+lemma image2_union_right : image2 f s (t ∪ t') = image2 f s t ∪ image2 f s t' :=
+begin
+  ext c, split,
+  { rintros ⟨a, b, ha, h1b|h2b, rfl⟩;[left, right]; exact ⟨_, _, ‹_›, ‹_›, rfl⟩ },
+  { rintro (⟨_, _, _, _, rfl⟩|⟨_, _, _, _, rfl⟩); refine ⟨_, _, ‹_›, _, rfl⟩; simp [mem_union, *] }
+end
+
+@[simp] lemma image2_empty_left : image2 f ∅ t = ∅ := ext $ by simp
+@[simp] lemma image2_empty_right : image2 f s ∅ = ∅ := ext $ by simp
+
+lemma image2_inter_subset_left : image2 f (s ∩ s') t ⊆ image2 f s t ∩ image2 f s' t :=
+by { rintro _ ⟨a, b, ⟨h1a, h2a⟩, hb, rfl⟩, split; exact ⟨_, _, ‹_›, ‹_›, rfl⟩ }
+
+lemma image2_inter_subset_right : image2 f s (t ∩ t') ⊆ image2 f s t ∩ image2 f s t' :=
+by { rintro _ ⟨a, b, ha, ⟨h1b, h2b⟩, rfl⟩, split; exact ⟨_, _, ‹_›, ‹_›, rfl⟩ }
+
+@[simp] lemma image2_singleton : image2 f {a} {b} = {f a b} :=
+ext $ λ x, by simp [eq_comm]
+
+lemma image2_singleton_left : image2 f {a} t = f a '' t :=
+ext $ λ x, by simp
+
+lemma image2_singleton_right : image2 f s {b} = (λ a, f a b) '' s :=
+ext $ λ x, by simp
+
+@[congr] lemma image2_congr (h : ∀ (a ∈ s) (b ∈ t), f a b = f' a b) :
+  image2 f s t = image2 f' s t :=
+by { ext, split; rintro ⟨a, b, ha, hb, rfl⟩; refine ⟨a, b, ha, hb, by rw h a ha b hb⟩ }
+
+/-- A common special case of `image2_congr` -/
+lemma image2_congr' (h : ∀ a b, f a b = f' a b) : image2 f s t = image2 f' s t :=
+image2_congr (λ a _ b _, h a b)
+
+/-- The image of a ternary function `f : α → β → γ → δ` as a function
+  `set α → set β → set γ → set δ`. Mathematically this should be thought of as the image of the
+  corresponding function `α × β × γ → δ`.
+-/
+def image3 (g : α → β → γ → δ) (s : set α) (t : set β) (u : set γ) : set δ :=
+{d | ∃ a b c, a ∈ s ∧ b ∈ t ∧ c ∈ u ∧ g a b c = d }
+
+@[simp] lemma mem_image3 : d ∈ image3 g s t u ↔ ∃ a b c, a ∈ s ∧ b ∈ t ∧ c ∈ u ∧ g a b c = d :=
+iff.rfl
+
+@[congr] lemma image3_congr (h : ∀ (a ∈ s) (b ∈ t) (c ∈ u), g a b c = g' a b c) :
+  image3 g s t u = image3 g' s t u :=
+by { ext x,
+     split; rintro ⟨a, b, c, ha, hb, hc, rfl⟩; refine ⟨a, b, c, ha, hb, hc, by rw h a ha b hb c hc⟩ }
+
+/-- A common special case of `image3_congr` -/
+lemma image3_congr' (h : ∀ a b c, g a b c = g' a b c) : image3 g s t u = image3 g' s t u :=
+image3_congr (λ a _ b _ c _, h a b c)
+
+lemma image2_image2_left (f : δ → γ → ε) (g : α → β → δ) :
+  image2 f (image2 g s t) u = image3 (λ a b c, f (g a b) c) s t u :=
+begin
+  ext, split,
+  { rintro ⟨_, c, ⟨a, b, ha, hb, rfl⟩, hc, rfl⟩, refine ⟨a, b, c, ha, hb, hc, rfl⟩ },
+  { rintro ⟨a, b, c, ha, hb, hc, rfl⟩, refine ⟨_, c, ⟨a, b, ha, hb, rfl⟩, hc, rfl⟩ }
+end
+
+lemma image2_image2_right (f : α → δ → ε) (g : β → γ → δ) :
+  image2 f s (image2 g t u) = image3 (λ a b c, f a (g b c)) s t u :=
+begin
+  ext, split,
+  { rintro ⟨a, _, ha, ⟨b, c, hb, hc, rfl⟩, rfl⟩, refine ⟨a, b, c, ha, hb, hc, rfl⟩ },
+  { rintro ⟨a, b, c, ha, hb, hc, rfl⟩, refine ⟨a, _, ha, ⟨b, c, hb, hc, rfl⟩, rfl⟩ }
+end
+
+lemma image_image2 (f : α → β → γ) (g : γ → δ) :
+  g '' image2 f s t = image2 (λ a b, g (f a b)) s t :=
+begin
+  ext, split,
+  { rintro ⟨_, ⟨a, b, ha, hb, rfl⟩, rfl⟩, refine ⟨a, b, ha, hb, rfl⟩ },
+  { rintro ⟨a, b, ha, hb, rfl⟩, refine ⟨_, ⟨a, b, ha, hb, rfl⟩, rfl⟩ }
+end
+
+lemma image2_image_left (f : γ → β → δ) (g : α → γ) :
+  image2 f (g '' s) t = image2 (λ a b, f (g a) b) s t :=
+begin
+  ext, split,
+  { rintro ⟨_, b, ⟨a, ha, rfl⟩, hb, rfl⟩, refine ⟨a, b, ha, hb, rfl⟩ },
+  { rintro ⟨a, b, ha, hb, rfl⟩, refine ⟨_, b, ⟨a, ha, rfl⟩, hb, rfl⟩ }
+end
+
+lemma image2_image_right (f : α → γ → δ) (g : β → γ) :
+  image2 f s (g '' t) = image2 (λ a b, f a (g b)) s t :=
+begin
+  ext, split,
+  { rintro ⟨a, _, ha, ⟨b, hb, rfl⟩, rfl⟩, refine ⟨a, b, ha, hb, rfl⟩ },
+  { rintro ⟨a, b, ha, hb, rfl⟩, refine ⟨a, _, ha, ⟨b, hb, rfl⟩, rfl⟩ }
+end
+
+lemma image2_swap (f : α → β → γ) (s : set α) (t : set β) :
+  image2 f s t = image2 (λ a b, f b a) t s :=
+by { ext, split; rintro ⟨a, b, ha, hb, rfl⟩; refine ⟨b, a, hb, ha, rfl⟩ }
+
+@[simp] lemma image2_left (h : t.nonempty) : image2 (λ x y, x) s t = s :=
+by simp [nonempty_def.mp h, ext_iff]
+
+@[simp] lemma image2_right (h : s.nonempty) : image2 (λ x y, y) s t = t :=
+by simp [nonempty_def.mp h, ext_iff]
+
+@[simp] lemma image_prod (f : α → β → γ) : (λ x : α × β, f x.1 x.2) '' s.prod t = image2 f s t :=
+set.ext $ λ a,
+⟨ by { rintros ⟨_, _, rfl⟩, exact ⟨_, _, (mem_prod.mp ‹_›).1, (mem_prod.mp ‹_›).2, rfl⟩ },
+  by { rintros ⟨_, _, _, _, rfl⟩, exact ⟨(_, _), mem_prod.mpr ⟨‹_›, ‹_›⟩, rfl⟩ }⟩
+
+lemma nonempty.image2 (hs : s.nonempty) (ht : t.nonempty) : (image2 f s t).nonempty :=
+by { cases hs with a ha, cases ht with b hb, exact ⟨f a b, ⟨a, b, ha, hb, rfl⟩⟩ }
+
+end n_ary_image
 
 end set
+
+namespace subsingleton
+
+variables {α : Type*} [subsingleton α]
+
+lemma eq_univ_of_nonempty {s : set α} : s.nonempty → s = univ :=
+λ ⟨x, hx⟩, eq_univ_of_forall $ λ y, subsingleton.elim x y ▸ hx
+
+@[elab_as_eliminator]
+lemma set_cases {p : set α → Prop} (h0 : p ∅) (h1 : p univ) (s) : p s :=
+s.eq_empty_or_nonempty.elim (λ h, h.symm ▸ h0) $ λ h, (eq_univ_of_nonempty h).symm ▸ h1
+
+end subsingleton

src/data/set/finite.lean

@@ -301,6 +301,15 @@ fintype.of_finset (s.to_finset.product t.to_finset) $ by simp
 lemma finite.prod {s : set α} {t : set β} : finite s → finite t → finite (set.prod s t)
 | ⟨hs⟩ ⟨ht⟩ := by exactI ⟨set.fintype_prod s t⟩
 
+/-- `image2 f s t` is finitype if `s` and `t` are. -/
+instance fintype_image2 [decidable_eq γ] (f : α → β → γ) (s : set α) (t : set β)
+  [hs : fintype s] [ht : fintype t] : fintype (image2 f s t : set γ) :=
+by { rw ← image_prod, apply set.fintype_image }
+
+lemma finite.image2 (f : α → β → γ) {s : set α} {t : set β} (hs : finite s) (ht : finite t) :
+  finite (image2 f s t) :=
+by { rw ← image_prod, exact (hs.prod ht).image _ }
+
 /-- If `s : set α` is a set with `fintype` instance and `f : α → set β` is a function such that
 each `f a`, `a ∈ s`, has a `fintype` structure, then `s >>= f` has a `fintype` structure. -/
 def fintype_bind {α β} [decidable_eq β] (s : set α) [fintype s]