chore: cleanup another erw by generalizing Equiv.range_eq_univ to EquivLike (#21710)

Author: kim-em

Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean

@@ -206,9 +206,7 @@ theorem ofBijective.symm_eq {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective
     (ofBijective hφ).symm.toEquiv = (Equiv.ofBijective _ hφ).symm :=
   rfl
 
-@[simp]
-theorem range_eq (e : P₁ ≃ᵃ[k] P₂) : range e = univ :=
-  e.surjective.range_eq
+theorem range_eq (e : P₁ ≃ᵃ[k] P₂) : range e = univ := by simp
 
 @[simp]
 theorem apply_symm_apply (e : P₁ ≃ᵃ[k] P₂) (p : P₂) : e (e.symm p) = p :=

Mathlib/Logic/Equiv/Set.lean

@@ -29,11 +29,20 @@ universe u v w z
 
 variable {α : Sort u} {β : Sort v} {γ : Sort w}
 
-namespace Equiv
+namespace EquivLike
 
 @[simp]
-theorem range_eq_univ {α : Type*} {β : Type*} (e : α ≃ β) : range e = univ :=
-  eq_univ_of_forall e.surjective
+theorem range_eq_univ {α : Type*} {β : Type*} {E : Type*} [EquivLike E α β] (e : E) :
+    range e = univ :=
+  eq_univ_of_forall (EquivLike.toEquiv e).surjective
+
+end EquivLike
+
+namespace Equiv
+
+theorem range_eq_univ {α : Type*} {β : Type*} (e : α ≃ β) :
+    range e = univ :=
+  EquivLike.range_eq_univ e
 
 protected theorem image_eq_preimage {α β} (e : α ≃ β) (s : Set α) : e '' s = e.symm ⁻¹' s :=
   Set.ext fun _ => mem_image_iff_of_inverse e.left_inv e.right_inv

Mathlib/Order/RelIso/Set.lean

@@ -48,9 +48,7 @@ end RelHomClass
 
 namespace RelIso
 
-@[simp]
-theorem range_eq (e : r ≃r s) : Set.range e = Set.univ :=
-  e.surjective.range_eq
+theorem range_eq (e : r ≃r s) : Set.range e = Set.univ := by simp
 
 end RelIso
 

Mathlib/RingTheory/Adjoin/Basic.lean

@@ -543,7 +543,7 @@ theorem Algebra.restrictScalars_adjoin_of_algEquiv
     (Algebra.adjoin L S).restrictScalars F = (Algebra.adjoin L' S).restrictScalars F := by
   apply_fun Subalgebra.toSubsemiring using fun K K' h ↦ by rwa [SetLike.ext'_iff] at h ⊢
   change Subsemiring.closure _ = Subsemiring.closure _
-  erw [hi, Set.range_comp, i.toEquiv.range_eq_univ, Set.image_univ]
+  rw [hi, Set.range_comp, EquivLike.range_eq_univ, Set.image_univ]
 
 end
 

Mathlib/Topology/Homeomorph.lean

@@ -181,9 +181,7 @@ theorem symm_comp_self (h : X ≃ₜ Y) : h.symm ∘ h = id :=
 theorem self_comp_symm (h : X ≃ₜ Y) : h ∘ h.symm = id :=
   funext h.apply_symm_apply
 
-@[simp]
-theorem range_coe (h : X ≃ₜ Y) : range h = univ :=
-  h.surjective.range_eq
+theorem range_coe (h : X ≃ₜ Y) : range h = univ := by simp
 
 theorem image_symm (h : X ≃ₜ Y) : image h.symm = preimage h :=
   funext h.symm.toEquiv.image_eq_preimage

Mathlib/Topology/MetricSpace/Isometry.lean

@@ -403,9 +403,7 @@ theorem symm_comp_self (h : α ≃ᵢ β) : (h.symm : β → α) ∘ h = id := f
 
 theorem self_comp_symm (h : α ≃ᵢ β) : (h : α → β) ∘ h.symm = id := funext h.right_inv
 
-@[simp]
-theorem range_eq_univ (h : α ≃ᵢ β) : range h = univ :=
-  h.toEquiv.range_eq_univ
+theorem range_eq_univ (h : α ≃ᵢ β) : range h = univ := by simp
 
 theorem image_symm (h : α ≃ᵢ β) : image h.symm = preimage h :=
   image_eq_preimage_of_inverse h.symm.toEquiv.left_inv h.symm.toEquiv.right_inv

Mathlib/Topology/UniformSpace/Equiv.lean

@@ -176,9 +176,7 @@ theorem symm_comp_self (h : α ≃ᵤ β) : (h.symm : β → α) ∘ h = id :=
 theorem self_comp_symm (h : α ≃ᵤ β) : (h : α → β) ∘ h.symm = id :=
   funext h.apply_symm_apply
 
-@[simp]
-theorem range_coe (h : α ≃ᵤ β) : range h = univ :=
-  h.surjective.range_eq
+theorem range_coe (h : α ≃ᵤ β) : range h = univ := by simp
 
 theorem image_symm (h : α ≃ᵤ β) : image h.symm = preimage h :=
   funext h.symm.toEquiv.image_eq_preimage