feat(data/set/[basic|prod]): make ×ˢ bind more strongly, and define…

… `mem.out` (#13422)

* This means that  `×ˢ` does not behave the same as `∪` or `∩` around `⁻¹'` or `''`, but I think that is fine.
* From the sphere eversion project

src/data/set/basic.lean

@@ -185,9 +185,16 @@ by tauto
 
 /-! ### Lemmas about `mem` and `set_of` -/
 
-@[simp] theorem mem_set_of_eq {a : α} {p : α → Prop} : a ∈ {a | p a} = p a := rfl
+@[simp] theorem mem_set_of_eq {a : α} {p : α → Prop} : a ∈ {x | p x} = p a := rfl
 
-theorem nmem_set_of_eq {a : α} {P : α → Prop} : a ∉ {a : α | P a} = ¬ P a := rfl
+lemma mem_set_of {a : α} {p : α → Prop} : a ∈ {x | p x} ↔ p a := iff.rfl
+
+/-- If `h : a ∈ {x | p x}` then `h.out : p x`. These are definitionally equal, but this can
+nevertheless be useful for various reasons, e.g. to apply further projection notation or in an
+argument to `simp`. -/
+lemma has_mem.mem.out {p : α → Prop} {a : α} (h : a ∈ {x | p x}) : p a := h
+
+theorem nmem_set_of_eq {a : α} {p : α → Prop} : a ∉ {x | p x} = ¬ p a := rfl
 
 @[simp] theorem set_of_mem_eq {s : set α} : {x | x ∈ s} = s := rfl
 

src/data/set/pointwise.lean

@@ -122,7 +122,7 @@ lemma mul_mem_mul (ha : a ∈ s) (hb : b ∈ t) : a * b ∈ s * t := mem_image2_
 lemma mul_subset_mul (h₁ : s₁ ⊆ t₁) (h₂ : s₂ ⊆ t₂) : s₁ * s₂ ⊆ t₁ * t₂ := image2_subset h₁ h₂
 
 @[to_additive add_image_prod]
-lemma image_mul_prod : (λ x : α × α, x.fst * x.snd) '' (s ×ˢ t) = s * t := image_prod _
+lemma image_mul_prod : (λ x : α × α, x.fst * x.snd) '' s ×ˢ t = s * t := image_prod _
 
 @[simp, to_additive] lemma empty_mul : ∅ * s = ∅ := image2_empty_left
 @[simp, to_additive] lemma mul_empty : s * ∅ = ∅ := image2_empty_right
@@ -551,7 +551,7 @@ lemma div_mem_div (ha : a ∈ s) (hb : b ∈ t) : a / b ∈ s / t := mem_image2_
 lemma div_subset_div (h₁ : s₁ ⊆ t₁) (h₂ : s₂ ⊆ t₂) : s₁ / s₂ ⊆ t₁ / t₂ := image2_subset h₁ h₂
 
 @[to_additive add_image_prod]
-lemma image_div_prod : (λ x : α × α, x.fst / x.snd) '' (s ×ˢ t) = s / t := image_prod _
+lemma image_div_prod : (λ x : α × α, x.fst / x.snd) '' s ×ˢ t = s / t := image_prod _
 
 @[simp, to_additive] lemma empty_div : ∅ / s = ∅ := image2_empty_left
 @[simp, to_additive] lemma div_empty : s / ∅ = ∅ := image2_empty_right
@@ -683,7 +683,7 @@ variables {ι : Sort*} {κ : ι → Sort*} [has_scalar α β] {s s₁ s₂ : set
 lemma image2_smul : image2 has_scalar.smul s t = s • t := rfl
 
 @[to_additive add_image_prod]
-lemma image_smul_prod : (λ x : α × β, x.fst • x.snd) '' (s ×ˢ t) = s • t := image_prod _
+lemma image_smul_prod : (λ x : α × β, x.fst • x.snd) '' s ×ˢ t = s • t := image_prod _
 
 @[to_additive]
 lemma mem_smul : b ∈ s • t ↔ ∃ x y, x ∈ s ∧ y ∈ t ∧ x • y = b := iff.rfl
@@ -912,7 +912,7 @@ instance has_vsub : has_vsub (set α) (set β) := ⟨image2 (-ᵥ)⟩
 
 @[simp] lemma image2_vsub : (image2 has_vsub.vsub s t : set α) = s -ᵥ t := rfl
 
-lemma image_vsub_prod : (λ x : β × β, x.fst -ᵥ x.snd) '' (s ×ˢ t) = s -ᵥ t := image_prod _
+lemma image_vsub_prod : (λ x : β × β, x.fst -ᵥ x.snd) '' s ×ˢ t = s -ᵥ t := image_prod _
 
 lemma mem_vsub : a ∈ s -ᵥ t ↔ ∃ x y, x ∈ s ∧ y ∈ t ∧ x -ᵥ y = a := iff.rfl
 

src/data/set/prod.lean

@@ -25,7 +25,8 @@ open function
 class has_set_prod (α β : Type*) (γ : out_param Type*) :=
 (prod : α → β → γ)
 
-infixr ` ×ˢ `:72 := has_set_prod.prod
+/- This notation binds more strongly than (pre)images, unions and intersections. -/
+infixr ` ×ˢ `:82 := has_set_prod.prod
 
 namespace set
 
@@ -52,7 +53,7 @@ lemma mk_mem_prod (ha : a ∈ s) (hb : b ∈ t) : (a, b) ∈ s ×ˢ t := ⟨ha,
 lemma prod_mono (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : s₁ ×ˢ t₁ ⊆ s₂ ×ˢ t₂ :=
 λ x ⟨h₁, h₂⟩, ⟨hs h₁, ht h₂⟩
 
-lemma prod_subset_iff {P : set (α × β)} : (s ×ˢ t ⊆ P) ↔ ∀ (x ∈ s) (y ∈ t), (x, y) ∈ P :=
+lemma prod_subset_iff {P : set (α × β)} : s ×ˢ t ⊆ P ↔ ∀ (x ∈ s) (y ∈ t), (x, y) ∈ P :=
 ⟨λ h _ hx _ hy, h (mk_mem_prod hx hy), λ h ⟨_, _⟩ hp, h _ hp.1 _ hp.2⟩
 
 lemma forall_prod_set {p : α × β → Prop} : (∀ x ∈ s ×ˢ t, p x) ↔ ∀ (x ∈ s) (y ∈ t), p (x, y) :=
@@ -95,57 +96,57 @@ lemma prod_insert : s ×ˢ (insert b t) = ((λa, (a, b)) '' s) ∪ s ×ˢ t :=
 by { ext ⟨x, y⟩, simp [image, iff_def, or_imp_distrib, imp.swap] {contextual := tt} }
 
 lemma prod_preimage_eq {f : γ → α} {g : δ → β} :
-  (f ⁻¹' s) ×ˢ (g ⁻¹' t) = (λ p : γ × δ, (f p.1, g p.2)) ⁻¹' (s ×ˢ t) := rfl
+  (f ⁻¹' s) ×ˢ (g ⁻¹' t) = (λ p : γ × δ, (f p.1, g p.2)) ⁻¹' s ×ˢ t := rfl
 
 lemma prod_preimage_left {f : γ → α} :
-  (f ⁻¹' s) ×ˢ t = (λ p : γ × β, (f p.1, p.2)) ⁻¹' (s ×ˢ t) := rfl
+  (f ⁻¹' s) ×ˢ t = (λ p : γ × β, (f p.1, p.2)) ⁻¹' s ×ˢ t := rfl
 
 lemma prod_preimage_right {g : δ → β} :
-  s ×ˢ (g ⁻¹' t) = (λ p : α × δ, (p.1, g p.2)) ⁻¹' (s ×ˢ t) := rfl
+  s ×ˢ (g ⁻¹' t) = (λ p : α × δ, (p.1, g p.2)) ⁻¹' s ×ˢ t := rfl
 
 lemma preimage_prod_map_prod (f : α → β) (g : γ → δ) (s : set β) (t : set δ) :
-  prod.map f g ⁻¹' (s ×ˢ t) = (f ⁻¹' s) ×ˢ (g ⁻¹' t) :=
+  prod.map f g ⁻¹' s ×ˢ t = (f ⁻¹' s) ×ˢ (g ⁻¹' t) :=
 rfl
 
 lemma mk_preimage_prod (f : γ → α) (g : γ → β) :
-  (λ x, (f x, g x)) ⁻¹' (s ×ˢ t) = f ⁻¹' s ∩ g ⁻¹' t := rfl
+  (λ x, (f x, g x)) ⁻¹' s ×ˢ t = f ⁻¹' s ∩ g ⁻¹' t := rfl
 
-@[simp] lemma mk_preimage_prod_left (hb : b ∈ t) : (λ a, (a, b)) ⁻¹' (s ×ˢ t) = s :=
+@[simp] lemma mk_preimage_prod_left (hb : b ∈ t) : (λ a, (a, b)) ⁻¹' s ×ˢ t = s :=
 by { ext a, simp [hb] }
 
-@[simp] lemma mk_preimage_prod_right (ha : a ∈ s) : prod.mk a ⁻¹' (s ×ˢ t) = t :=
+@[simp] lemma mk_preimage_prod_right (ha : a ∈ s) : prod.mk a ⁻¹' s ×ˢ t = t :=
 by { ext b, simp [ha] }
 
-@[simp] lemma mk_preimage_prod_left_eq_empty (hb : b ∉ t) : (λ a, (a, b)) ⁻¹' (s ×ˢ t) = ∅ :=
+@[simp] lemma mk_preimage_prod_left_eq_empty (hb : b ∉ t) : (λ a, (a, b)) ⁻¹' s ×ˢ t = ∅ :=
 by { ext a, simp [hb] }
 
-@[simp] lemma mk_preimage_prod_right_eq_empty (ha : a ∉ s) : prod.mk a ⁻¹' (s ×ˢ t) = ∅ :=
+@[simp] lemma mk_preimage_prod_right_eq_empty (ha : a ∉ s) : prod.mk a ⁻¹' s ×ˢ t = ∅ :=
 by { ext b, simp [ha] }
 
 lemma mk_preimage_prod_left_eq_if [decidable_pred (∈ t)] :
-  (λ a, (a, b)) ⁻¹' (s ×ˢ t) = if b ∈ t then s else ∅ :=
+  (λ a, (a, b)) ⁻¹' s ×ˢ t = if b ∈ t then s else ∅ :=
 by split_ifs; simp [h]
 
 lemma mk_preimage_prod_right_eq_if [decidable_pred (∈ s)] :
-  prod.mk a ⁻¹' (s ×ˢ t) = if a ∈ s then t else ∅ :=
+  prod.mk a ⁻¹' s ×ˢ t = if a ∈ s then t else ∅ :=
 by split_ifs; simp [h]
 
 lemma mk_preimage_prod_left_fn_eq_if [decidable_pred (∈ t)] (f : γ → α) :
-  (λ a, (f a, b)) ⁻¹' (s ×ˢ t) = if b ∈ t then f ⁻¹' s else ∅ :=
+  (λ a, (f a, b)) ⁻¹' s ×ˢ t = if b ∈ t then f ⁻¹' s else ∅ :=
 by rw [← mk_preimage_prod_left_eq_if, prod_preimage_left, preimage_preimage]
 
 lemma mk_preimage_prod_right_fn_eq_if [decidable_pred (∈ s)] (g : δ → β) :
-  (λ b, (a, g b)) ⁻¹' (s ×ˢ t) = if a ∈ s then g ⁻¹' t else ∅ :=
+  (λ b, (a, g b)) ⁻¹' s ×ˢ t = if a ∈ s then g ⁻¹' t else ∅ :=
 by rw [← mk_preimage_prod_right_eq_if, prod_preimage_right, preimage_preimage]
 
-lemma preimage_swap_prod {s : set α} {t : set β} : prod.swap ⁻¹' (t ×ˢ s) = s ×ˢ t :=
+lemma preimage_swap_prod {s : set α} {t : set β} : prod.swap ⁻¹' t ×ˢ s = s ×ˢ t :=
 by { ext ⟨x, y⟩, simp [and_comm] }
 
-lemma image_swap_prod : prod.swap '' (t ×ˢ s) = s ×ˢ t :=
+lemma image_swap_prod : prod.swap '' t ×ˢ s = s ×ˢ t :=
 by rw [image_swap_eq_preimage_swap, preimage_swap_prod]
 
 lemma prod_image_image_eq {m₁ : α → γ} {m₂ : β → δ} :
-  (m₁ '' s) ×ˢ (m₂ '' t) = image (λ p : α × β, (m₁ p.1, m₂ p.2)) (s ×ˢ t) :=
+  (m₁ '' s) ×ˢ (m₂ '' t) = (λ p : α × β, (m₁ p.1, m₂ p.2)) '' s ×ˢ t :=
 ext $ by simp [-exists_and_distrib_right, exists_and_distrib_right.symm, and.left_comm,
   and.assoc, and.comm]
 
@@ -179,7 +180,7 @@ lemma nonempty.snd : (s ×ˢ t : set _).nonempty → t.nonempty := λ ⟨x, hx
 lemma prod_nonempty_iff : (s ×ˢ t : set _).nonempty ↔ s.nonempty ∧ t.nonempty :=
 ⟨λ h, ⟨h.fst, h.snd⟩, λ h, h.1.prod h.2⟩
 
-lemma prod_eq_empty_iff : s ×ˢ t = ∅ ↔ (s = ∅ ∨ t = ∅) :=
+lemma prod_eq_empty_iff : s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅ :=
 by simp only [not_nonempty_iff_eq_empty.symm, prod_nonempty_iff, not_and_distrib]
 
 lemma prod_sub_preimage_iff {W : set γ} {f : α × β → γ} :
@@ -192,22 +193,22 @@ by { rintro _ ⟨a, ha, rfl⟩, exact ⟨ha, hb⟩ }
 lemma image_prod_mk_subset_prod_right (ha : a ∈ s) : prod.mk a '' t ⊆ s ×ˢ t :=
 by { rintro _ ⟨b, hb, rfl⟩, exact ⟨ha, hb⟩ }
 
-lemma fst_image_prod_subset (s : set α) (t : set β) : prod.fst '' (s ×ˢ t) ⊆ s :=
+lemma fst_image_prod_subset (s : set α) (t : set β) : prod.fst '' s ×ˢ t ⊆ s :=
 λ _ h, let ⟨_, ⟨h₂, _⟩, h₁⟩ := (set.mem_image _ _ _).1 h in h₁ ▸ h₂
 
 lemma prod_subset_preimage_fst (s : set α) (t : set β) : s ×ˢ t ⊆ prod.fst ⁻¹' s :=
 image_subset_iff.1 (fst_image_prod_subset s t)
 
-lemma fst_image_prod (s : set β) {t : set α} (ht : t.nonempty) : prod.fst '' (s ×ˢ t) = s :=
+lemma fst_image_prod (s : set β) {t : set α} (ht : t.nonempty) : prod.fst '' s ×ˢ t = s :=
 (fst_image_prod_subset _ _).antisymm $ λ y hy, let ⟨x, hx⟩ := ht in ⟨(y, x), ⟨hy, hx⟩, rfl⟩
 
-lemma snd_image_prod_subset (s : set α) (t : set β) : prod.snd '' (s ×ˢ t) ⊆ t :=
+lemma snd_image_prod_subset (s : set α) (t : set β) : prod.snd '' s ×ˢ t ⊆ t :=
 λ _ h, let ⟨_, ⟨_, h₂⟩, h₁⟩ := (set.mem_image _ _ _).1 h in h₁ ▸ h₂
 
 lemma prod_subset_preimage_snd (s : set α) (t : set β) : s ×ˢ t ⊆ prod.snd ⁻¹' t :=
 image_subset_iff.1 (snd_image_prod_subset s t)
 
-lemma snd_image_prod {s : set α} (hs : s.nonempty) (t : set β) : prod.snd '' (s ×ˢ t) = t :=
+lemma snd_image_prod {s : set α} (hs : s.nonempty) (t : set β) : prod.snd '' s ×ˢ t = t :=
 (snd_image_prod_subset _ _).antisymm $ λ y y_in, let ⟨x, x_in⟩ := hs in ⟨(x, y), ⟨x_in, y_in⟩, rfl⟩
 
 lemma prod_diff_prod : s ×ˢ t \ s₁ ×ˢ t₁ = s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t :=
@@ -241,7 +242,7 @@ begin
     refl },
 end
 
-@[simp] lemma image_prod (f : α → β → γ) : (λ x : α × β, f x.1 x.2) '' (s ×ˢ t) = image2 f s t :=
+@[simp] lemma image_prod (f : α → β → γ) : (λ x : α × β, f x.1 x.2) '' s ×ˢ t = image2 f s t :=
 set.ext $ λ a,
 ⟨ by { rintro ⟨_, _, rfl⟩, exact ⟨_, _, (mem_prod.mp ‹_›).1, (mem_prod.mp ‹_›).2, rfl⟩ },
   by { rintro ⟨_, _, _, _, rfl⟩, exact ⟨(_, _), mem_prod.mpr ⟨‹_›, ‹_›⟩, rfl⟩ }⟩

src/logic/equiv/fin.lean

@@ -51,7 +51,7 @@ non-dependent version and `prod_equiv_pi_fin_two` for a version with inputs `α
   right_inv := λ ⟨x, y⟩, rfl }
 
 lemma fin.preimage_apply_01_prod {α : fin 2 → Type u} (s : set (α 0)) (t : set (α 1)) :
-  (λ f : Π i, α i, (f 0, f 1)) ⁻¹' (s ×ˢ t) =
+  (λ f : Π i, α i, (f 0, f 1)) ⁻¹' s ×ˢ t =
     set.pi set.univ (fin.cons s $ fin.cons t fin.elim0) :=
 begin
   ext f,
@@ -60,7 +60,7 @@ begin
 end
 
 lemma fin.preimage_apply_01_prod' {α : Type u} (s t : set α) :
-  (λ f : fin 2 → α, (f 0, f 1)) ⁻¹' (s ×ˢ t) = set.pi set.univ ![s, t] :=
+  (λ f : fin 2 → α, (f 0, f 1)) ⁻¹' s ×ˢ t = set.pi set.univ ![s, t] :=
 fin.preimage_apply_01_prod s t
 
 /-- A product space `α × β` is equivalent to the space `Π i : fin 2, γ i`, where

src/logic/equiv/set.lean

@@ -101,32 +101,31 @@ lemma eq_preimage_iff_image_eq {α β} (e : α ≃ β) (s t) : s = e ⁻¹' t 
 set.eq_preimage_iff_image_eq e.bijective
 
 @[simp] lemma prod_comm_preimage {α β} {s : set α} {t : set β} :
-  equiv.prod_comm α β ⁻¹' (t ×ˢ s) = (s ×ˢ t) :=
+  equiv.prod_comm α β ⁻¹' t ×ˢ s = s ×ˢ t :=
 set.preimage_swap_prod
 
-lemma prod_comm_image {α β} {s : set α} {t : set β} :
-  equiv.prod_comm α β '' (s ×ˢ t) = (t ×ˢ s) :=
+lemma prod_comm_image {α β} {s : set α} {t : set β} : equiv.prod_comm α β '' s ×ˢ t = t ×ˢ s :=
 set.image_swap_prod
 
 @[simp]
 lemma prod_assoc_preimage {α β γ} {s : set α} {t : set β} {u : set γ} :
-  equiv.prod_assoc α β γ ⁻¹' (s ×ˢ (t ×ˢ u)) = (s ×ˢ t) ×ˢ u :=
+  equiv.prod_assoc α β γ ⁻¹' s ×ˢ (t ×ˢ u) = (s ×ˢ t) ×ˢ u :=
 by { ext, simp [and_assoc] }
 
 @[simp]
 lemma prod_assoc_symm_preimage {α β γ} {s : set α} {t : set β} {u : set γ} :
-  (equiv.prod_assoc α β γ).symm ⁻¹' ((s ×ˢ t) ×ˢ u) = s ×ˢ (t ×ˢ u) :=
+  (equiv.prod_assoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u = s ×ˢ (t ×ˢ u) :=
 by { ext, simp [and_assoc] }
 
 -- `@[simp]` doesn't like these lemmas, as it uses `set.image_congr'` to turn `equiv.prod_assoc`
 -- into a lambda expression and then unfold it.
 
 lemma prod_assoc_image {α β γ} {s : set α} {t : set β} {u : set γ} :
-  equiv.prod_assoc α β γ '' ((s ×ˢ t) ×ˢ u) = s ×ˢ (t ×ˢ u) :=
+  equiv.prod_assoc α β γ '' (s ×ˢ t) ×ˢ u = s ×ˢ (t ×ˢ u) :=
 by simpa only [equiv.image_eq_preimage] using prod_assoc_symm_preimage
 
 lemma prod_assoc_symm_image {α β γ} {s : set α} {t : set β} {u : set γ} :
-  (equiv.prod_assoc α β γ).symm '' (s ×ˢ (t ×ˢ u)) = (s ×ˢ t) ×ˢ u :=
+  (equiv.prod_assoc α β γ).symm '' s ×ˢ (t ×ˢ u) = (s ×ˢ t) ×ˢ u :=
 by simpa only [equiv.image_eq_preimage] using prod_assoc_preimage
 
 /-- A set `s` in `α × β` is equivalent to the sigma-type `Σ x, {y | (x, y) ∈ s}`. -/

src/measure_theory/constructions/prod.lean

@@ -583,7 +583,7 @@ begin
   refine ⟨this, (prod_eq $ λ s t hs ht, _).symm⟩,
   rw [map_apply this (hs.prod ht)],
   refine (prod_apply (this $ hs.prod ht)).trans _,
-  have : ∀ᵐ x ∂μa, μc ((λ y, (f x, g x y)) ⁻¹' (s ×ˢ t)) = indicator (f ⁻¹' s) (λ y, μd t) x,
+  have : ∀ᵐ x ∂μa, μc ((λ y, (f x, g x y)) ⁻¹' s ×ˢ t) = indicator (f ⁻¹' s) (λ y, μd t) x,
   { refine hg.mono (λ x hx, _), unfreezingI { subst hx },
     simp only [mk_preimage_prod_right_fn_eq_if, indicator_apply, mem_preimage],
     split_ifs,

src/measure_theory/integral/lebesgue.lean

@@ -313,7 +313,7 @@ def pair (f : α →ₛ β) (g : α →ₛ γ) : α →ₛ (β × γ) := (f.map
 @[simp] lemma pair_apply (f : α →ₛ β) (g : α →ₛ γ) (a) : pair f g a = (f a, g a) := rfl
 
 lemma pair_preimage (f : α →ₛ β) (g : α →ₛ γ) (s : set β) (t : set γ) :
-  (pair f g) ⁻¹' (s ×ˢ t) = (f ⁻¹' s) ∩ (g ⁻¹' t) := rfl
+  pair f g ⁻¹' s ×ˢ t = (f ⁻¹' s) ∩ (g ⁻¹' t) := rfl
 
 /- A special form of `pair_preimage` -/
 lemma pair_preimage_singleton (f : α →ₛ β) (g : α →ₛ γ) (b : β) (c : γ) :

src/measure_theory/measurable_space.lean

@@ -561,8 +561,8 @@ lemma measurable_set_prod_of_nonempty {s : set α} {t : set β} (h : (s ×ˢ t :
 begin
   rcases h with ⟨⟨x, y⟩, hx, hy⟩,
   refine ⟨λ hst, _, λ h, h.1.prod h.2⟩,
-  have : measurable_set ((λ x, (x, y)) ⁻¹' (s ×ˢ t)) := measurable_id.prod_mk measurable_const hst,
-  have : measurable_set (prod.mk x ⁻¹' (s ×ˢ t)) := measurable_const.prod_mk measurable_id hst,
+  have : measurable_set ((λ x, (x, y)) ⁻¹' s ×ˢ t) := measurable_id.prod_mk measurable_const hst,
+  have : measurable_set (prod.mk x ⁻¹' s ×ˢ t) := measurable_const.prod_mk measurable_id hst,
   simp * at *
 end
 

src/order/filter/basic.lean

@@ -2620,7 +2620,7 @@ le_antisymm
   (λ s hs,
     let ⟨s₁, hs₁, s₂, hs₂, h⟩ := mem_prod_iff.mp hs in
     filter.sets_of_superset _ (prod_mem_prod (image_mem_map hs₁) (image_mem_map hs₂)) $
-      calc m₁ '' s₁ ×ˢ m₂ '' s₂ = (λ p : α₁×α₂, (m₁ p.1, m₂ p.2)) '' (s₁ ×ˢ s₂) :
+      calc (m₁ '' s₁) ×ˢ (m₂ '' s₂) = (λ p : α₁×α₂, (m₁ p.1, m₂ p.2)) '' s₁ ×ˢ s₂ :
           set.prod_image_image_eq
         ... ⊆ _ : by rwa [image_subset_iff])
   ((tendsto.comp le_rfl tendsto_fst).prod_mk (tendsto.comp le_rfl tendsto_snd))

src/topology/uniform_space/uniform_embedding.lean

@@ -512,9 +512,9 @@ show preimage (λp:(α×α), (ψ p.1, ψ p.2)) d ∈ 𝓤 α,
     from calc _ ⊆ preimage (λp:(β×β), (e p.1, e p.2)) (interior t) : preimage_mono hm
     ... ⊆ preimage (λp:(β×β), (e p.1, e p.2)) t : preimage_mono interior_subset
     ... ⊆ preimage (λp:(β×β), (f p.1, f p.2)) s : ts,
-  have f '' (e ⁻¹' m₁) ×ˢ f '' (e ⁻¹' m₂) ⊆ s,
+  have (f '' (e ⁻¹' m₁)) ×ˢ (f '' (e ⁻¹' m₂)) ⊆ s,
     from calc (f '' (e ⁻¹' m₁)) ×ˢ (f '' (e ⁻¹' m₂)) =
-      (λp:(β×β), (f p.1, f p.2)) '' (e ⁻¹' m₁ ×ˢ e ⁻¹' m₂) : prod_image_image_eq
+      (λp:(β×β), (f p.1, f p.2)) '' ((e ⁻¹' m₁) ×ˢ (e ⁻¹' m₂)) : prod_image_image_eq
     ... ⊆ (λp:(β×β), (f p.1, f p.2)) '' ((λp:(β×β), (f p.1, f p.2)) ⁻¹' s) : monotone_image this
     ... ⊆ s : image_preimage_subset _ _,
   have (a, b) ∈ s, from @this (a, b) ⟨ha₁, hb₁⟩,