refactor(data/equiv/basic): remove equiv.set.range (#6960)

We already had `equiv.of_injective`, which duplicated the API. `of_injective` is the preferred naming, so we change all occurrences accordingly.
This also renames `equiv.set.range_of_left_inverse` to `equiv.of_left_inverse`, to match names like `linear_equiv.of_left_inverse`.

Note that the `congr` and `powerset` definitions which appear in the diff have just been reordered, and are otherwise unchanged.

src/data/equiv/basic.lean

@@ -1667,6 +1667,25 @@ begin
   simp [equiv.set.image, equiv.set.image_of_inj_on, hf.eq_iff, this],
 end
 
+/-- If `α` is equivalent to `β`, then `set α` is equivalent to `set β`. -/
+@[simps]
+protected def congr {α β : Type*} (e : α ≃ β) : set α ≃ set β :=
+⟨λ s, e '' s, λ t, e.symm '' t, symm_image_image e, symm_image_image e.symm⟩
+
+/-- The set `{x ∈ s | t x}` is equivalent to the set of `x : s` such that `t x`. -/
+protected def sep {α : Type u} (s : set α) (t : α → Prop) :
+  ({ x ∈ s | t x } : set α) ≃ { x : s | t x } :=
+(equiv.subtype_subtype_equiv_subtype_inter s t).symm
+
+/-- The set `𝒫 S := {x | x ⊆ S}` is equivalent to the type `set S`. -/
+protected def powerset {α} (S : set α) : 𝒫 S ≃ set S :=
+{ to_fun := λ x : 𝒫 S, coe ⁻¹' (x : set α),
+  inv_fun := λ x : set S, ⟨coe '' x, by rintro _ ⟨a : S, _, rfl⟩; exact a.2⟩,
+  left_inv := λ x, by ext y; exact ⟨λ ⟨⟨_, _⟩, h, rfl⟩, h, λ h, ⟨⟨_, x.2 h⟩, h, rfl⟩⟩,
+  right_inv := λ x, by ext; simp }
+
+end set
+
 /-- If `f : α → β` has a left-inverse when `α` is nonempty, then `α` is computably equivalent to the
 range of `f`.
 
@@ -1675,7 +1694,7 @@ empty too. This hypothesis is absent on analogous definitions on stronger `equiv
 `linear_equiv.of_left_inverse` and `ring_equiv.of_left_inverse` as their typeclass assumptions
 are already sufficient to ensure non-emptiness. -/
 @[simps]
-def range_of_left_inverse {α β : Sort*}
+def of_left_inverse {α β : Sort*}
   (f : α → β) (f_inv : nonempty α → β → α) (hf : Π h : nonempty α, left_inverse (f_inv h) f) :
   α ≃ set.range f :=
 { to_fun := λ a, ⟨f a, a, rfl⟩,
@@ -1687,46 +1706,31 @@ def range_of_left_inverse {α β : Sort*}
 /-- If `f : α → β` has a left-inverse, then `α` is computably equivalent to the range of `f`.
 
 Note that if `α` is empty, no such `f_inv` exists and so this definition can't be used, unlike
-the stronger but less convenient `equiv.set.range_of_left_inverse`. -/
-abbreviation range_of_left_inverse' {α β : Sort*}
+the stronger but less convenient `of_left_inverse`. -/
+abbreviation of_left_inverse' {α β : Sort*}
   (f : α → β) (f_inv : β → α) (hf : left_inverse f_inv f) :
   α ≃ set.range f :=
-range_of_left_inverse f (λ _, f_inv) (λ _, hf)
+of_left_inverse f (λ _, f_inv) (λ _, hf)
 
-/-- If `f : α → β` is an injective function, then `α` is equivalent to the range of `f`. -/
+/-- If `f : α → β` is an injective function, then domain `α` is equivalent to the range of `f`. -/
 @[simps apply]
-protected noncomputable def range {α β} (f : α → β) (H : injective f) :
-  α ≃ range f :=
-equiv.set.range_of_left_inverse f
-  (λ h, by exactI function.inv_fun f) (λ h, by exactI function.left_inverse_inv_fun H)
-
-theorem apply_range_symm {α β} (f : α → β) (H : injective f) (b : range f) :
-  f ((set.range f H).symm b) = b :=
-subtype.ext_iff.1 $ (set.range f H).apply_symm_apply b
-
-/-- If `α` is equivalent to `β`, then `set α` is equivalent to `set β`. -/
-@[simps]
-protected def congr {α β : Type*} (e : α ≃ β) : set α ≃ set β :=
-⟨λ s, e '' s, λ t, e.symm '' t, symm_image_image e, symm_image_image e.symm⟩
+noncomputable def of_injective {α β} (f : α → β) (hf : injective f) : α ≃ _root_.set.range f :=
+equiv.of_left_inverse f
+  (λ h, by exactI function.inv_fun f) (λ h, by exactI function.left_inverse_inv_fun hf)
 
-/-- The set `{x ∈ s | t x}` is equivalent to the set of `x : s` such that `t x`. -/
-protected def sep {α : Type u} (s : set α) (t : α → Prop) :
-  ({ x ∈ s | t x } : set α) ≃ { x : s | t x } :=
-(equiv.subtype_subtype_equiv_subtype_inter s t).symm
+theorem apply_of_injective_symm {α β} (f : α → β) (hf : injective f) (b : _root_.set.range f) :
+  f ((of_injective f hf).symm b) = b :=
+subtype.ext_iff.1 $ (of_injective f hf).apply_symm_apply b
 
-/-- The set `𝒫 S := {x | x ⊆ S}` is equivalent to the type `set S`. -/
-protected def powerset {α} (S : set α) : 𝒫 S ≃ set S :=
-{ to_fun := λ x : 𝒫 S, coe ⁻¹' (x : set α),
-  inv_fun := λ x : set S, ⟨coe '' x, by rintro _ ⟨a : S, _, rfl⟩; exact a.2⟩,
-  left_inv := λ x, by ext y; exact ⟨λ ⟨⟨_, _⟩, h, rfl⟩, h, λ h, ⟨⟨_, x.2 h⟩, h, rfl⟩⟩,
-  right_inv := λ x, by ext; simp }
-
-end set
+lemma of_left_inverse_eq_of_injective {α β : Type*} [nonempty α]
+  (f : α → β) (f_inv : nonempty α → β → α) (hf : Π h : nonempty α, left_inverse (f_inv h) f) :
+  of_left_inverse f f_inv hf = of_injective f (hf ‹_›).injective :=
+by { ext, simp }
 
 /-- If `f` is a bijective function, then its domain is equivalent to its codomain. -/
 @[simps apply]
 noncomputable def of_bijective {α β} (f : α → β) (hf : bijective f) : α ≃ β :=
-(equiv.set.range f hf.1).trans $ (set_congr hf.2.range_eq).trans $ equiv.set.univ β
+(of_injective f hf.1).trans $ (set_congr hf.2.range_eq).trans $ equiv.set.univ β
 
 lemma of_bijective_apply_symm_apply {α β} (f : α → β) (hf : bijective f) (x : β) :
   f ((of_bijective f hf).symm x) = x :=
@@ -1736,12 +1740,6 @@ lemma of_bijective_apply_symm_apply {α β} (f : α → β) (hf : bijective f) (
   (of_bijective f hf).symm (f x) = x :=
 (of_bijective f hf).symm_apply_apply x
 
-/-- If `f` is an injective function, then its domain is equivalent to its range. -/
-@[simps apply]
-noncomputable def of_injective {α β} (f : α → β) (hf : injective f) : α ≃ _root_.set.range f :=
-of_bijective (λ x, ⟨f x, set.mem_range_self x⟩)
-  ⟨λ x y hxy, hf $ by injections, λ ⟨_, x, rfl⟩, ⟨x, rfl⟩⟩
-
 /-- Subtype of the quotient is equivalent to the quotient of the subtype. Let `α` be a setoid with
 equivalence relation `~`. Let `p₂` be a predicate on the quotient type `α/~`, and `p₁` be the lift
 of this predicate to `α`: `p₁ a ↔ p₂ ⟦a⟧`. Let `~₂` be the restriction of `~` to `{x // p₁ x}`.

src/data/equiv/denumerable.lean

@@ -247,7 +247,7 @@ def of_encodable_of_infinite (α : Type*) [encodable α] [infinite α] : denumer
 begin
   letI := @decidable_range_encode α _;
   letI : infinite (set.range (@encode α _)) :=
-    infinite.of_injective _ (equiv.set.range _ encode_injective).injective,
+    infinite.of_injective _ (equiv.of_injective _ encode_injective).injective,
   letI := nat.subtype.denumerable (set.range (@encode α _)),
   exact denumerable.of_equiv (set.range (@encode α _))
     (equiv_range_encode α)

src/data/fintype/basic.lean

@@ -270,7 +270,7 @@ variables {f : α → β} (hf : function.injective f)
 /--
 The inverse of an `hf : injective` function `f : α → β`, of the type `↥(set.range f) → α`.
 This is the computable version of `function.inv_fun` that requires `fintype α` and `decidable_eq β`,
-or the function version of applying `(equiv.set.range f hf).symm`.
+or the function version of applying `(equiv.of_injective f hf).symm`.
 This function should not usually be used for actual computation because for most cases,
 an explicit inverse can be stated that has better computational properties.
 This function computes by checking all terms `a : α` to find the `f a = b`, so it is O(N) where
@@ -308,7 +308,7 @@ variables (f : α ↪ β) (b : set.range f)
 /--
 The inverse of an embedding `f : α ↪ β`, of the type `↥(set.range f) → α`.
 This is the computable version of `function.inv_fun` that requires `fintype α` and `decidable_eq β`,
-or the function version of applying `(equiv.set.range f f.injective).symm`.
+or the function version of applying `(equiv.of_injective f f.injective).symm`.
 This function should not usually be used for actual computation because for most cases,
 an explicit inverse can be stated that has better computational properties.
 This function computes by checking all terms `a : α` to find the `f a = b`, so it is O(N) where

src/data/set/finite.lean

@@ -576,7 +576,7 @@ lemma subset_iff_to_finset_subset (s t : set α) [fintype s] [fintype t] :
 
 lemma card_range_of_injective [fintype α] {f : α → β} (hf : injective f)
   [fintype (range f)] : fintype.card (range f) = fintype.card α :=
-eq.symm $ fintype.card_congr $ equiv.set.range f hf
+eq.symm $ fintype.card_congr $ equiv.of_injective f hf
 
 lemma finite.exists_maximal_wrt [partial_order β] (f : α → β) (s : set α) (h : set.finite s) :
   s.nonempty → ∃a∈s, ∀a'∈s, f a ≤ f a' → f a = f a' :=

src/group_theory/perm/sign.lean

@@ -122,21 +122,21 @@ begin
     rw ← hb, exact ⟨b, rfl⟩ },
   let σ₁' := subtype_perm_of_fintype σ h1,
   let σ₂' := subtype_perm_of_fintype σ h3,
-  let σ₁ := perm_congr (equiv.set.range (@sum.inl m n) sum.inl_injective).symm σ₁',
-  let σ₂ := perm_congr (equiv.set.range (@sum.inr m n) sum.inr_injective).symm σ₂',
+  let σ₁ := perm_congr (equiv.of_injective (@sum.inl m n) sum.inl_injective).symm σ₁',
+  let σ₂ := perm_congr (equiv.of_injective (@sum.inr m n) sum.inr_injective).symm σ₂',
   rw [monoid_hom.mem_range, prod.exists],
   use [σ₁, σ₂],
   rw [perm.sum_congr_hom_apply],
   ext,
   cases x with a b,
   { rw [equiv.sum_congr_apply, sum.map_inl, perm_congr_apply, equiv.symm_symm,
-      set.apply_range_symm (@sum.inl m n)],
+        apply_of_injective_symm (@sum.inl m n)],
     erw subtype_perm_apply,
-    rw [set.range_apply, subtype.coe_mk, subtype.coe_mk] },
+    rw [of_injective_apply, subtype.coe_mk, subtype.coe_mk] },
   { rw [equiv.sum_congr_apply, sum.map_inr, perm_congr_apply, equiv.symm_symm,
-      set.apply_range_symm (@sum.inr m n)],
+        apply_of_injective_symm (@sum.inr m n)],
     erw subtype_perm_apply,
-    rw [set.range_apply, subtype.coe_mk, subtype.coe_mk] }
+    rw [of_injective_apply, subtype.coe_mk, subtype.coe_mk] }
 end
 
 /-- Two permutations `f` and `g` are `disjoint` if their supports are disjoint, i.e.,

src/group_theory/perm/subgroup.lean

@@ -33,7 +33,7 @@ instance sum_congr_hom.decidable_mem_range {α β : Type*}
 lemma sum_congr_hom.card_range {α β : Type*}
   [fintype (sum_congr_hom α β).range] [fintype (perm α × perm β)] :
   fintype.card (sum_congr_hom α β).range = fintype.card (perm α × perm β) :=
-fintype.card_eq.mpr ⟨(set.range (sum_congr_hom α β) sum_congr_hom_injective).symm⟩
+fintype.card_eq.mpr ⟨(of_injective (sum_congr_hom α β) sum_congr_hom_injective).symm⟩
 
 instance sigma_congr_right_hom.decidable_mem_range {α : Type*} {β : α → Type*}
   [decidable_eq α] [∀ a, decidable_eq (β a)] [fintype α] [∀ a, fintype (β a)] :
@@ -44,7 +44,7 @@ instance sigma_congr_right_hom.decidable_mem_range {α : Type*} {β : α → Typ
 lemma sigma_congr_right_hom.card_range {α : Type*} {β : α → Type*}
   [fintype (sigma_congr_right_hom β).range] [fintype (Π a, perm (β a))] :
   fintype.card (sigma_congr_right_hom β).range = fintype.card (Π a, perm (β a)) :=
-fintype.card_eq.mpr ⟨(set.range (sigma_congr_right_hom β) sigma_congr_right_hom_injective).symm⟩
+fintype.card_eq.mpr ⟨(of_injective (sigma_congr_right_hom β) sigma_congr_right_hom_injective).symm⟩
 
 instance subtype_congr_hom.decidable_mem_range {α : Type*} (p : α → Prop) [decidable_pred p]
   [fintype (perm {a // p a} × perm {a // ¬ p a})] [decidable_eq (perm α)] :
@@ -55,7 +55,7 @@ instance subtype_congr_hom.decidable_mem_range {α : Type*} (p : α → Prop) [d
 lemma subtype_congr_hom.card_range {α : Type*} (p : α → Prop) [decidable_pred p]
   [fintype (subtype_congr_hom p).range] [fintype (perm {a // p a} × perm {a // ¬ p a})] :
   fintype.card (subtype_congr_hom p).range = fintype.card (perm {a // p a} × perm {a // ¬ p a}) :=
-fintype.card_eq.mpr ⟨(set.range (subtype_congr_hom p) (subtype_congr_hom_injective p)).symm⟩
+fintype.card_eq.mpr ⟨(of_injective (subtype_congr_hom p) (subtype_congr_hom_injective p)).symm⟩
 
 end perm
 end equiv

src/linear_algebra/basis.lean

@@ -463,8 +463,8 @@ lemma exists_sum_is_basis (hs : linear_independent K v) :
 begin
   -- This is a hack: we jump through hoops to reuse `exists_subset_is_basis`.
   let s := set.range v,
-  let e : ι ≃ s := equiv.set.range v hs.injective,
-  have : (λ x, x : s → V) = v ∘ e.symm := by { funext, dsimp, rw [equiv.set.apply_range_symm v], },
+  let e : ι ≃ s := equiv.of_injective v hs.injective,
+  have : (λ x, x : s → V) = v ∘ e.symm := by { ext, dsimp, rw [equiv.apply_of_injective_symm v] },
   have : linear_independent K (λ x, x : s → V),
   { rw this,
     exact linear_independent.comp hs _ (e.symm.injective), },

src/linear_algebra/linear_independent.lean

@@ -224,7 +224,7 @@ h ▸ linear_independent_equiv e
 
 theorem linear_independent_subtype_range {ι} {f : ι → M} (hf : injective f) :
   linear_independent R (coe : range f → M) ↔ linear_independent R f :=
-iff.symm $ linear_independent_equiv' (equiv.set.range f hf) rfl
+iff.symm $ linear_independent_equiv' (equiv.of_injective f hf) rfl
 
 alias linear_independent_subtype_range ↔ linear_independent.of_subtype_range _
 

src/logic/small.lean

@@ -86,7 +86,7 @@ end
 theorem small_of_injective {α : Type*} {β : Type*} [small.{w} β]
   (f : α → β) (hf : function.injective f) : small.{w} α :=
 begin
-  rw small_congr (equiv.set.range f hf),
+  rw small_congr (equiv.of_injective f hf),
   apply_instance,
 end
 

src/order/rel_iso.lean

@@ -619,7 +619,7 @@ protected noncomputable def strict_mono_incr_on.order_iso {α β} [linear_order
 its range. -/
 protected noncomputable def strict_mono.order_iso {α β} [linear_order α] [preorder β] (f : α → β)
   (h_mono : strict_mono f) : α ≃o set.range f :=
-{ to_equiv := equiv.set.range f h_mono.injective,
+{ to_equiv := equiv.of_injective f h_mono.injective,
   map_rel_iff' := λ a b, h_mono.le_iff_le }
 
 /-- A strictly monotone surjective function from a linear order is an order isomorphism. -/

src/set_theory/cardinal.lean

@@ -116,7 +116,7 @@ theorem mk_le_of_surjective {α β : Type u} {f : α → β} (hf : surjective f)
 theorem le_mk_iff_exists_set {c : cardinal} {α : Type u} :
   c ≤ mk α ↔ ∃ p : set α, mk p = c :=
 ⟨quotient.induction_on c $ λ β ⟨⟨f, hf⟩⟩,
-  ⟨set.range f, eq.symm $ quot.sound ⟨equiv.set.range f hf⟩⟩,
+  ⟨set.range f, eq.symm $ quot.sound ⟨equiv.of_injective f hf⟩⟩,
 λ ⟨p, e⟩, e ▸ ⟨⟨subtype.val, λ a b, subtype.eq⟩⟩⟩
 
 theorem out_embedding {c c' : cardinal} : c ≤ c' ↔ nonempty (c.out ↪ c'.out) :=
@@ -289,7 +289,7 @@ cardinal.add_le_add (le_refl _)
 protected theorem le_iff_exists_add {a b : cardinal} : a ≤ b ↔ ∃ c, b = a + c :=
 ⟨quotient.induction_on₂ a b $ λ α β ⟨⟨f, hf⟩⟩,
   have (α ⊕ ((range f)ᶜ : set β)) ≃ β, from
-    (equiv.sum_congr (equiv.set.range f hf) (equiv.refl _)).trans $
+    (equiv.sum_congr (equiv.of_injective f hf) (equiv.refl _)).trans $
     (equiv.set.sum_compl (range f)),
   ⟨⟦↥(range f)ᶜ⟧, quotient.sound ⟨this.symm⟩⟩,
  λ ⟨c, e⟩, add_zero a ▸ e.symm ▸ cardinal.add_le_add_left _ (cardinal.zero_le _)⟩
@@ -1029,19 +1029,19 @@ theorem mk_range_le {α β : Type u} {f : α → β} : mk (range f) ≤ mk α :=
 mk_le_of_surjective surjective_onto_range
 
 lemma mk_range_eq (f : α → β) (h : injective f) : mk (range f) = mk α :=
-quotient.sound ⟨(equiv.set.range f h).symm⟩
+quotient.sound ⟨(equiv.of_injective f h).symm⟩
 
 lemma mk_range_eq_of_injective {α : Type u} {β : Type v} {f : α → β} (hf : injective f) :
   lift.{v u} (mk (range f)) = lift.{u v} (mk α) :=
 begin
-  have := (@lift_mk_eq.{v u max u v} (range f) α).2 ⟨(equiv.set.range f hf).symm⟩,
+  have := (@lift_mk_eq.{v u max u v} (range f) α).2 ⟨(equiv.of_injective f hf).symm⟩,
   simp only [lift_umax.{u v}, lift_umax.{v u}] at this,
   exact this
 end
 
 lemma mk_range_eq_lift {α : Type u} {β : Type v} {f : α → β} (hf : injective f) :
   lift.{v (max u w)} (# (range f)) = lift.{u (max v w)} (# α) :=
-lift_mk_eq.mpr ⟨(equiv.set.range f hf).symm⟩
+lift_mk_eq.mpr ⟨(equiv.of_injective f hf).symm⟩
 
 theorem mk_image_eq {α β : Type u} {f : α → β} {s : set α} (hf : injective f) :
   mk (f '' s) = mk s :=

src/set_theory/cardinal_ordinal.lean

@@ -569,7 +569,7 @@ theorem extend_function {α β : Type*} {s : set α} (f : s ↪ β)
 begin
   intros, have := h, cases this with g,
   let h : α ≃ β := (set.sum_compl (s : set α)).symm.trans
-    ((sum_congr (equiv.set.range f f.2) g).trans
+    ((sum_congr (equiv.of_injective f f.2) g).trans
     (set.sum_compl (range f))),
   refine ⟨h, _⟩, rintro ⟨x, hx⟩, simp [set.sum_compl_symm_apply_of_mem, hx]
 end

src/topology/algebra/infinite_sum.lean

@@ -153,7 +153,7 @@ e.injective.has_sum_iff $ by simp
 
 lemma function.injective.has_sum_range_iff {g : γ → β} (hg : injective g) :
   has_sum (λ x : set.range g, f x) a ↔ has_sum (f ∘ g) a :=
-(equiv.set.range g hg).has_sum_iff.symm
+(equiv.of_injective g hg).has_sum_iff.symm
 
 lemma equiv.summable_iff (e : γ ≃ β) :
   summable (f ∘ e) ↔ summable f :=

src/topology/metric_space/isometry.lean

@@ -365,7 +365,7 @@ range of the isometry. -/
 def isometry.isometric_on_range [emetric_space α] [emetric_space β] {f : α → β} (h : isometry f) :
   α ≃ᵢ range f :=
 { isometry_to_fun := λx y, by simpa [subtype.edist_eq] using h x y,
-  .. equiv.set.range f h.injective }
+  .. equiv.of_injective f h.injective }
 
 @[simp] lemma isometry.isometric_on_range_apply [emetric_space α] [emetric_space β]
   {f : α → β} (h : isometry f) (x : α) : h.isometric_on_range x = ⟨f x, mem_range_self _⟩ :=