chore: rename Injective.sum_elim and friends (#22129)

Per the naming convention, they should be written `sumElim`, etc.

Author: grunweg

Mathlib/Data/Countable/Basic.lean

@@ -59,7 +59,7 @@ variable {α : Type u} {β : Type v} {π : α → Type w}
 instance [Countable α] [Countable β] : Countable (α ⊕ β) := by
   rcases exists_injective_nat α with ⟨f, hf⟩
   rcases exists_injective_nat β with ⟨g, hg⟩
-  exact (Equiv.natSumNatEquivNat.injective.comp <| hf.sum_map hg).countable
+  exact (Equiv.natSumNatEquivNat.injective.comp <| hf.sumMap hg).countable
 
 instance Sum.uncountable_inl [Uncountable α] : Uncountable (α ⊕ β) :=
   inl_injective.uncountable

Mathlib/Data/Sum/Basic.lean

@@ -165,19 +165,23 @@ open Sum
 
 namespace Function
 
-theorem Injective.sum_elim {f : α → γ} {g : β → γ} (hf : Injective f) (hg : Injective g)
+theorem Injective.sumElim {f : α → γ} {g : β → γ} (hf : Injective f) (hg : Injective g)
     (hfg : ∀ a b, f a ≠ g b) : Injective (Sum.elim f g)
   | inl _, inl _, h => congr_arg inl <| hf h
   | inl _, inr _, h => (hfg _ _ h).elim
   | inr _, inl _, h => (hfg _ _ h.symm).elim
   | inr _, inr _, h => congr_arg inr <| hg h
 
-theorem Injective.sum_map {f : α → β} {g : α' → β'} (hf : Injective f) (hg : Injective g) :
+@[deprecated (since := "2025-02-20")] alias Injective.sum_elim := Injective.sumElim
+
+theorem Injective.sumMap {f : α → β} {g : α' → β'} (hf : Injective f) (hg : Injective g) :
     Injective (Sum.map f g)
   | inl _, inl _, h => congr_arg inl <| hf <| inl.inj h
   | inr _, inr _, h => congr_arg inr <| hg <| inr.inj h
 
-theorem Surjective.sum_map {f : α → β} {g : α' → β'} (hf : Surjective f) (hg : Surjective g) :
+@[deprecated (since := "2025-02-20")] alias Injective.sum_map := Injective.sumMap
+
+theorem Surjective.sumMap {f : α → β} {g : α' → β'} (hf : Surjective f) (hg : Surjective g) :
     Surjective (Sum.map f g)
   | inl y =>
     let ⟨x, hx⟩ := hf y
@@ -186,9 +190,13 @@ theorem Surjective.sum_map {f : α → β} {g : α' → β'} (hf : Surjective f)
     let ⟨x, hx⟩ := hg y
     ⟨inr x, congr_arg inr hx⟩
 
-theorem Bijective.sum_map {f : α → β} {g : α' → β'} (hf : Bijective f) (hg : Bijective g) :
+@[deprecated (since := "2025-02-20")] alias Surjective.sum_map := Surjective.sumMap
+
+theorem Bijective.sumMap {f : α → β} {g : α' → β'} (hf : Bijective f) (hg : Bijective g) :
     Bijective (Sum.map f g) :=
-  ⟨hf.injective.sum_map hg.injective, hf.surjective.sum_map hg.surjective⟩
+  ⟨hf.injective.sumMap hg.injective, hf.surjective.sumMap hg.surjective⟩
+
+@[deprecated (since := "2025-02-20")] alias Bijective.sum_map := Bijective.sumMap
 
 end Function
 
@@ -202,7 +210,7 @@ theorem map_injective {f : α → γ} {g : β → δ} :
   ⟨fun h =>
     ⟨fun a₁ a₂ ha => inl_injective <| @h (inl a₁) (inl a₂) (congr_arg inl ha :), fun b₁ b₂ hb =>
       inr_injective <| @h (inr b₁) (inr b₂) (congr_arg inr hb :)⟩,
-    fun h => h.1.sum_map h.2⟩
+    fun h => h.1.sumMap h.2⟩
 
 @[simp]
 theorem map_surjective {f : α → γ} {g : β → δ} :
@@ -216,7 +224,7 @@ theorem map_surjective {f : α → γ} {g : β → δ} :
         obtain ⟨a | b, h⟩ := h (inr d)
         · cases h
         · exact ⟨b, inr_injective h⟩)⟩,
-    fun h => h.1.sum_map h.2⟩
+    fun h => h.1.sumMap h.2⟩
 
 @[simp]
 theorem map_bijective {f : α → γ} {g : β → δ} :

Mathlib/Logic/Embedding/Basic.lean

@@ -258,7 +258,7 @@ open Sum
 
 /-- If `e₁` and `e₂` are embeddings, then so is `Sum.map e₁ e₂`. -/
 def sumMap {α β γ δ : Type*} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : α ⊕ γ ↪ β ⊕ δ :=
-  ⟨Sum.map e₁ e₂, e₁.injective.sum_map e₂.injective⟩
+  ⟨Sum.map e₁ e₂, e₁.injective.sumMap e₂.injective⟩
 
 @[simp]
 theorem coe_sumMap {α β γ δ} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : sumMap e₁ e₂ = Sum.map e₁ e₂ :=

Mathlib/Order/RelIso/Basic.lean

@@ -469,7 +469,7 @@ def sumLiftRelInr (r : α → α → Prop) (s : β → β → Prop) : s ↪r Sum
 @[simps]
 def sumLiftRelMap (f : r ↪r s) (g : t ↪r u) : Sum.LiftRel r t ↪r Sum.LiftRel s u where
   toFun := Sum.map f g
-  inj' := f.injective.sum_map g.injective
+  inj' := f.injective.sumMap g.injective
   map_rel_iff' := by rintro (a | b) (c | d) <;> simp [f.map_rel_iff, g.map_rel_iff]
 
 /-- `Sum.inl` as a relation embedding into `Sum.Lex r s`. -/
@@ -490,7 +490,7 @@ def sumLexInr (r : α → α → Prop) (s : β → β → Prop) : s ↪r Sum.Lex
 @[simps]
 def sumLexMap (f : r ↪r s) (g : t ↪r u) : Sum.Lex r t ↪r Sum.Lex s u where
   toFun := Sum.map f g
-  inj' := f.injective.sum_map g.injective
+  inj' := f.injective.sumMap g.injective
   map_rel_iff' := by rintro (a | b) (c | d) <;> simp [f.map_rel_iff, g.map_rel_iff]
 
 /-- `fun b ↦ Prod.mk a b` as a relation embedding. -/

Mathlib/RingTheory/AlgebraicIndependent/Transcendental.lean

@@ -119,7 +119,7 @@ theorem adjoin_of_disjoint {s t : Set ι} (h : Disjoint s t) :
   rw [Set.image_eq_range, AlgebraicIndependent, ← AlgHom.coe_restrictScalars' R, ← e.injective_comp]
   show Injective ((AlgHom.restrictScalars R <| aeval _).comp e.toAlgHom)
   rw [this, AlgHom.coe_comp]
-  exact .comp hx (rename_injective _ <| Subtype.val_injective.sum_elim
+  exact .comp hx (rename_injective _ <| Subtype.val_injective.sumElim
     Subtype.val_injective fun i j eq ↦ h.ne_of_mem j.2 i.2 eq.symm)
 
 theorem adjoin_iff_disjoint [Nontrivial A] {s t : Set ι} :

Mathlib/RingTheory/Smooth/StandardSmooth.lean

@@ -250,7 +250,7 @@ this is the canonical pre-submersive presentation of `T` as an `R`-algebra. -/
 noncomputable def comp : PreSubmersivePresentation R T where
   __ := Q.toPresentation.comp P.toPresentation
   map := Sum.elim (fun rq ↦ Sum.inl <| Q.map rq) (fun rp ↦ Sum.inr <| P.map rp)
-  map_inj := Function.Injective.sum_elim ((Sum.inl_injective).comp (Q.map_inj))
+  map_inj := Function.Injective.sumElim ((Sum.inl_injective).comp (Q.map_inj))
     ((Sum.inr_injective).comp (P.map_inj)) <| by simp
   relations_finite := inferInstanceAs <| Finite (Q.rels ⊕ P.rels)
 

Mathlib/Topology/Category/Profinite/Nobeling.lean

@@ -1407,7 +1407,7 @@ def sum_to : (GoodProducts (π C (ord I · < o))) ⊕ (MaxProducts C ho) → Pro
   Sum.elim Subtype.val Subtype.val
 
 theorem injective_sum_to : Function.Injective (sum_to C ho) := by
-  refine Function.Injective.sum_elim Subtype.val_injective Subtype.val_injective
+  refine Function.Injective.sumElim Subtype.val_injective Subtype.val_injective
     (fun ⟨a,ha⟩ ⟨b,hb⟩  ↦ (fun (hab : a = b) ↦ ?_))
   rw [← hab] at hb
   have ha' := Products.prop_of_isGood  C _ ha (term I ho) hb.2

Mathlib/Topology/Homeomorph.lean

@@ -1073,7 +1073,7 @@ lemma IsHomeomorph.comp {g : Y → Z} (hg : IsHomeomorph g) (hf : IsHomeomorph f
     IsHomeomorph (g ∘ f) := ⟨hg.1.comp hf.1, hg.2.comp hf.2, hg.3.comp hf.3⟩
 
 lemma IsHomeomorph.sumMap {g : Z → W} (hf : IsHomeomorph f) (hg : IsHomeomorph g) :
-    IsHomeomorph (Sum.map f g) := ⟨hf.1.sum_map hg.1, hf.2.sumMap hg.2, hf.3.sum_map hg.3⟩
+    IsHomeomorph (Sum.map f g) := ⟨hf.1.sum_map hg.1, hf.2.sumMap hg.2, hf.3.sumMap hg.3⟩
 
 lemma IsHomeomorph.prodMap {g : Z → W} (hf : IsHomeomorph f) (hg : IsHomeomorph g) :
     IsHomeomorph (Prod.map f g) := ⟨hf.1.prodMap hg.1, hf.2.prodMap hg.2, hf.3.prodMap hg.3⟩