From f213ec28e753347ef35b8d1cb21766ba740d7e24 Mon Sep 17 00:00:00 2001
From: Moritz Doll <moritz.doll@googlemail.com>
Date: Mon, 27 Feb 2023 13:48:26 +0000
Subject: [PATCH] fix: bad coercions in Data.Set.Image (#2487)

The previous spelling of the coercion caused problems down the line. They are now changed to the coercion arrow, which is the preferred spelling.
---
 Mathlib/Data/Set/Image.lean | 48 ++++++++++++++++---------------------
 1 file changed, 20 insertions(+), 28 deletions(-)

diff --git a/Mathlib/Data/Set/Image.lean b/Mathlib/Data/Set/Image.lean
index b69502d5c0dc1..1805a3a17c4aa 100644
--- a/Mathlib/Data/Set/Image.lean
+++ b/Mathlib/Data/Set/Image.lean
@@ -179,7 +179,7 @@ theorem nonempty_of_nonempty_preimage {s : Set β} {f : α → β} (hf : (f ⁻
 #align set.nonempty_of_nonempty_preimage Set.nonempty_of_nonempty_preimage
 
 theorem preimage_subtype_coe_eq_compl {α : Type _} {s u v : Set α} (hsuv : s ⊆ u ∪ v)
-    (H : s ∩ (u ∩ v) = ∅) : (fun x : s => (x : α)) ⁻¹' u = ((fun x : s => (x : α)) ⁻¹' v)ᶜ := by
+    (H : s ∩ (u ∩ v) = ∅) : ((↑) : s → α) ⁻¹' u = ((↑) ⁻¹' v)ᶜ := by
   ext ⟨x, x_in_s⟩
   constructor
   · intro x_in_u x_in_v
@@ -980,7 +980,7 @@ theorem range_const : ∀ [Nonempty ι] {c : α}, (range fun _ : ι => c) = {c}
 #align set.range_const Set.range_const
 
 theorem range_subtype_map {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ x, p x → q (f x)) :
-    range (Subtype.map f h) = (fun x : Subtype q => (x : β)) ⁻¹' (f '' { x | p x }) := by
+    range (Subtype.map f h) = (↑) ⁻¹' (f '' { x | p x }) := by
   ext ⟨x, hx⟩
   rw [mem_preimage, mem_range, mem_image, Subtype.exists, Subtype.coe_mk]
   apply Iff.intro
@@ -1033,7 +1033,7 @@ theorem rangeFactorization_coe (f : ι → β) (a : ι) : (rangeFactorization f
 
 @[simp]
 theorem coe_comp_rangeFactorization (f : ι → β) :
-  (fun x : ↥(range f) => (x : β)) ∘ rangeFactorization f = f := rfl
+  (↑) ∘ rangeFactorization f = f := rfl
 #align set.coe_comp_range_factorization Set.coe_comp_rangeFactorization
 
 theorem surjective_onto_range : Surjective (rangeFactorization f) := fun ⟨_, ⟨i, rfl⟩⟩ => ⟨i, rfl⟩
@@ -1349,29 +1349,23 @@ end EquivLike
 
 namespace Subtype
 
--- Porting note:
--- Note that we can either write `fun x : s => (x : α)` or `Subtype.val : s → α`,
--- and that these are syntactically the same.
--- In mathlib3 we referred to this just as `coe`.
--- We may want to change the spelling of some statements later.
-
 variable {α : Type _}
 
 theorem coe_image {p : α → Prop} {s : Set (Subtype p)} :
-    (fun x : Subtype p => (x : α)) '' s = { x | ∃ h : p x, (⟨x, h⟩ : Subtype p) ∈ s } :=
+    (↑) '' s = { x | ∃ h : p x, (⟨x, h⟩ : Subtype p) ∈ s } :=
   Set.ext fun a =>
     ⟨fun ⟨⟨_, ha'⟩, in_s, h_eq⟩ => h_eq ▸ ⟨ha', in_s⟩, fun ⟨ha, in_s⟩ => ⟨⟨a, ha⟩, in_s, rfl⟩⟩
 #align subtype.coe_image Subtype.coe_image
 
 @[simp]
 theorem coe_image_of_subset {s t : Set α} (h : t ⊆ s) :
-  (fun x : s => (x : α)) '' { x : ↥s | ↑x ∈ t } = t := by
+  (↑) '' { x : ↥s | ↑x ∈ t } = t := by
   ext x
   rw [Set.mem_image]
   exact ⟨fun ⟨_, hx', hx⟩ => hx ▸ hx', fun hx => ⟨⟨x, h hx⟩, hx, rfl⟩⟩
 #align subtype.coe_image_of_subset Subtype.coe_image_of_subset
 
-theorem range_coe {s : Set α} : range (fun x : s => (x : α)) = s := by
+theorem range_coe {s : Set α} : range ((↑) : s → α) = s := by
   rw [← Set.image_univ]
   simp [-Set.image_univ, coe_image]
 #align subtype.range_coe Subtype.range_coe
@@ -1384,17 +1378,15 @@ theorem range_val {s : Set α} : range (Subtype.val : s → α) = s :=
 #align subtype.range_val Subtype.range_val
 
 /-- We make this the simp lemma instead of `range_coe`. The reason is that if we write
-  for `s : Set α` the function `coe : s → α`, then the inferred implicit arguments of `coe` are
-  `coe α (λ x, x ∈ s)`.
-
-  TODO: Port this docstring to mathlib4 as `coe` is something else now.-/
+  for `s : Set α` the function `(↑) : s → α`, then the inferred implicit arguments of `(↑)` are
+  `↑α (λ x, x ∈ s)`. -/
 @[simp]
-theorem range_coe_subtype {p : α → Prop} : range (fun x : Subtype p => (x : α)) = { x | p x } :=
+theorem range_coe_subtype {p : α → Prop} : range ((↑) : Subtype p → α) = { x | p x } :=
   range_coe
 #align subtype.range_coe_subtype Subtype.range_coe_subtype
 
 @[simp]
-theorem coe_preimage_self (s : Set α) : (fun x : s => (x : α)) ⁻¹' s = univ := by
+theorem coe_preimage_self (s : Set α) : ((↑) : s → α) ⁻¹' s = univ := by
   rw [← preimage_range, range_coe]
 #align subtype.coe_preimage_self Subtype.coe_preimage_self
 
@@ -1402,18 +1394,18 @@ theorem range_val_subtype {p : α → Prop} : range (Subtype.val : Subtype p →
   range_coe
 #align subtype.range_val_subtype Subtype.range_val_subtype
 
-theorem coe_image_subset (s : Set α) (t : Set s) : (fun x : s => (x : α)) '' t ⊆ s :=
+theorem coe_image_subset (s : Set α) (t : Set s) : ((↑) : s → α) '' t ⊆ s :=
   fun x ⟨y, _, yvaleq⟩ => by
   rw [← yvaleq]; exact y.property
 #align subtype.coe_image_subset Subtype.coe_image_subset
 
-theorem coe_image_univ (s : Set α) : (fun x : s => (x : α)) '' Set.univ = s :=
+theorem coe_image_univ (s : Set α) : ((↑) : s → α) '' Set.univ = s :=
   image_univ.trans range_coe
 #align subtype.coe_image_univ Subtype.coe_image_univ
 
 @[simp]
 theorem image_preimage_coe (s t : Set α) :
-  (fun x : s => (x : α)) '' ((fun x : s => (x : α)) ⁻¹' t) = t ∩ s :=
+  ((↑) : s → α) '' (((↑) : s → α) ⁻¹' t) = t ∩ s :=
   image_preimage_eq_inter_range.trans <| congr_arg _ range_coe
 #align subtype.image_preimage_coe Subtype.image_preimage_coe
 
@@ -1422,14 +1414,14 @@ theorem image_preimage_val (s t : Set α) : (Subtype.val : s → α) '' (Subtype
 #align subtype.image_preimage_val Subtype.image_preimage_val
 
 theorem preimage_coe_eq_preimage_coe_iff {s t u : Set α} :
-    (fun x : s => (x : α)) ⁻¹' t = (fun x : s => (x : α)) ⁻¹' u ↔ t ∩ s = u ∩ s := by
+    ((↑) : s → α) ⁻¹' t = ((↑) : s → α) ⁻¹' u ↔ t ∩ s = u ∩ s := by
   rw [← image_preimage_coe, ← image_preimage_coe, coe_injective.image_injective.eq_iff]
 #align subtype.preimage_coe_eq_preimage_coe_iff Subtype.preimage_coe_eq_preimage_coe_iff
 
 -- Porting note:
 -- @[simp] `simp` can prove this
 theorem preimage_coe_inter_self (s t : Set α) :
-  (fun x : s => (x : α)) ⁻¹' (t ∩ s) = (fun x : s => (x : α)) ⁻¹' t := by
+  ((↑) : s → α) ⁻¹' (t ∩ s) = ((↑) : s → α) ⁻¹' t := by
   rw [preimage_coe_eq_preimage_coe_iff, inter_assoc, inter_self]
 #align subtype.preimage_coe_inter_self Subtype.preimage_coe_inter_self
 
@@ -1439,26 +1431,26 @@ theorem preimage_val_eq_preimage_val_iff (s t u : Set α) :
 #align subtype.preimage_val_eq_preimage_val_iff Subtype.preimage_val_eq_preimage_val_iff
 
 theorem exists_set_subtype {t : Set α} (p : Set α → Prop) :
-    (∃ s : Set t, p ((fun x : t => (x : α)) '' s)) ↔ ∃ s : Set α, s ⊆ t ∧ p s := by
+    (∃ s : Set t, p (((↑) : t → α) '' s)) ↔ ∃ s : Set α, s ⊆ t ∧ p s := by
   rw [← exists_subset_range_and_iff, range_coe]
 #align subtype.exists_set_subtype Subtype.exists_set_subtype
 
 theorem forall_set_subtype {t : Set α} (p : Set α → Prop) :
-    (∀ s : Set t, p ((fun x : t => (x : α)) '' s)) ↔ ∀ s : Set α, s ⊆ t → p s := by
+    (∀ s : Set t, p (((↑) : t → α) '' s)) ↔ ∀ s : Set α, s ⊆ t → p s := by
   rw [← forall_subset_range_iff, range_coe]
 
 theorem preimage_coe_nonempty {s t : Set α} :
-  ((fun x : s => (x : α)) ⁻¹' t).Nonempty ↔ (s ∩ t).Nonempty :=
+  (((↑) : s → α) ⁻¹' t).Nonempty ↔ (s ∩ t).Nonempty :=
   by rw [inter_comm, ← image_preimage_coe, nonempty_image_iff]
 #align subtype.preimage_coe_nonempty Subtype.preimage_coe_nonempty
 
-theorem preimage_coe_eq_empty {s t : Set α} : (fun x : s => (x : α)) ⁻¹' t = ∅ ↔ s ∩ t = ∅ := by
+theorem preimage_coe_eq_empty {s t : Set α} : ((↑) : s → α) ⁻¹' t = ∅ ↔ s ∩ t = ∅ := by
   simp [← not_nonempty_iff_eq_empty, preimage_coe_nonempty]
 #align subtype.preimage_coe_eq_empty Subtype.preimage_coe_eq_empty
 
 -- Porting note:
 -- @[simp] `simp` can prove this
-theorem preimage_coe_compl (s : Set α) : (fun x : s => (x : α)) ⁻¹' sᶜ = ∅ :=
+theorem preimage_coe_compl (s : Set α) : ((↑) : s → α) ⁻¹' sᶜ = ∅ :=
   preimage_coe_eq_empty.2 (inter_compl_self s)
 #align subtype.preimage_coe_compl Subtype.preimage_coe_compl