refactor(*): rename subtype_congr to subtype_equiv (#6004)

This definition is closely related to `perm.subtype_perm`, so renaming will bring them closer in use. Also releavnt is #5875 which defines a separate `perm.subtype_congr`.

src/category_theory/adjunction/lifting.lean

@@ -137,7 +137,7 @@ calc (construct_left_adjoint_obj _ _ adj₁ adj₂ X ⟶ Y)
   ... ≃ {g : U.obj X ⟶ U.obj (R.obj Y) //
           U.map (F.map g ≫ adj₁.counit.app _) = U.map (adj₁.counit.app _) ≫ g} :
             begin
-              apply (adj₂.hom_equiv _ _).subtype_congr _,
+              apply (adj₂.hom_equiv _ _).subtype_equiv _,
               intro f,
               rw [← (adj₂.hom_equiv _ _).injective.eq_iff, eq_comm, adj₂.hom_equiv_naturality_left,
                   other_map, assoc, adj₂.hom_equiv_naturality_left, ← adj₂.counit_naturality,
@@ -149,7 +149,7 @@ calc (construct_left_adjoint_obj _ _ adj₁ adj₂ X ⟶ Y)
             end
   ... ≃ {z : F.obj (U.obj X) ⟶ R.obj Y // _} :
             begin
-              apply (adj₁.hom_equiv _ _).symm.subtype_congr,
+              apply (adj₁.hom_equiv _ _).symm.subtype_equiv,
               intro g,
               rw [← (adj₁.hom_equiv _ _).symm.injective.eq_iff, adj₁.hom_equiv_counit,
                   adj₁.hom_equiv_counit, adj₁.hom_equiv_counit, F.map_comp, assoc, U.map_comp,
@@ -166,8 +166,8 @@ begin
   rw [construct_left_adjoint_equiv_apply, construct_left_adjoint_equiv_apply, function.comp_app,
       function.comp_app, equiv.trans_apply, equiv.trans_apply, equiv.trans_apply, equiv.trans_apply,
       equiv.symm_apply_eq, subtype.ext_iff, cofork.is_colimit.hom_iso_natural,
-      equiv.apply_symm_apply, equiv.subtype_congr_apply, equiv.subtype_congr_apply,
-      equiv.subtype_congr_apply, equiv.subtype_congr_apply, subtype.coe_mk, subtype.coe_mk,
+      equiv.apply_symm_apply, equiv.subtype_equiv_apply, equiv.subtype_equiv_apply,
+      equiv.subtype_equiv_apply, equiv.subtype_equiv_apply, subtype.coe_mk, subtype.coe_mk,
       subtype.coe_mk, subtype.coe_mk, ← adj₁.hom_equiv_naturality_right_symm,
       cofork.is_colimit.hom_iso_natural, adj₂.hom_equiv_naturality_right, functor.comp_map],
 end

src/category_theory/monad/monadicity.lean

@@ -98,7 +98,7 @@ calc (comparison_left_adjoint_obj A ⟶ B) ≃ {f : F .obj A.A ⟶ B // _} :
         cofork.is_colimit.hom_iso (colimit.is_colimit _) B
      ... ≃ {g : A.A ⟶ G.obj B // G.map (F .map g) ≫ G.map (adj .counit.app B) = A.a ≫ g} :
       begin
-        refine (adj .hom_equiv _ _).subtype_congr _,
+        refine (adj .hom_equiv _ _).subtype_equiv _,
         intro f,
         rw [← (adj .hom_equiv _ _).injective.eq_iff, adjunction.hom_equiv_naturality_left,
             adj .hom_equiv_unit, adj .hom_equiv_unit, G.map_comp],

src/data/equiv/basic.lean

@@ -1109,34 +1109,34 @@ open subtype
 
 /-- If `α` is equivalent to `β` and the predicates `p : α → Prop` and `q : β → Prop` are equivalent
 at corresponding points, then `{a // p a}` is equivalent to `{b // q b}`. -/
-def subtype_congr {p : α → Prop} {q : β → Prop}
+def subtype_equiv {p : α → Prop} {q : β → Prop}
   (e : α ≃ β) (h : ∀ a, p a ↔ q (e a)) : {a : α // p a} ≃ {b : β // q b} :=
 ⟨λ x, ⟨e x, (h _).1 x.2⟩,
  λ y, ⟨e.symm y, (h _).2 (by { simp, exact y.2 })⟩,
  λ ⟨x, h⟩, subtype.ext_val $ by simp,
  λ ⟨y, h⟩, subtype.ext_val $ by simp⟩
 
-@[simp] lemma subtype_congr_apply {p : α → Prop} {q : β → Prop} (e : α ≃ β)
+@[simp] lemma subtype_equiv_apply {p : α → Prop} {q : β → Prop} (e : α ≃ β)
   (h : ∀ (a : α), p a ↔ q (e a)) (x : {x // p x}) :
-  e.subtype_congr h x = ⟨e x, (h _).1 x.2⟩ :=
+  e.subtype_equiv h x = ⟨e x, (h _).1 x.2⟩ :=
 rfl
 
-@[simp] lemma subtype_congr_symm_apply {p : α → Prop} {q : β → Prop} (e : α ≃ β)
+@[simp] lemma subtype_equiv_symm_apply {p : α → Prop} {q : β → Prop} (e : α ≃ β)
   (h : ∀ (a : α), p a ↔ q (e a)) (y : {y // q y}) :
-  (e.subtype_congr h).symm y = ⟨e.symm y, (h _).2 $ (e.apply_symm_apply y).symm ▸ y.2⟩ :=
+  (e.subtype_equiv h).symm y = ⟨e.symm y, (h _).2 $ (e.apply_symm_apply y).symm ▸ y.2⟩ :=
 rfl
 
 /-- If two predicates `p` and `q` are pointwise equivalent, then `{x // p x}` is equivalent to
 `{x // q x}`. -/
 @[simps]
-def subtype_congr_right {p q : α → Prop} (e : ∀x, p x ↔ q x) : {x // p x} ≃ {x // q x} :=
-subtype_congr (equiv.refl _) e
+def subtype_equiv_right {p q : α → Prop} (e : ∀x, p x ↔ q x) : {x // p x} ≃ {x // q x} :=
+subtype_equiv (equiv.refl _) e
 
 /-- If `α ≃ β`, then for any predicate `p : β → Prop` the subtype `{a // p (e a)}` is equivalent
 to the subtype `{b // p b}`. -/
 def subtype_equiv_of_subtype {p : β → Prop} (e : α ≃ β) :
   {a : α // p (e a)} ≃ {b : β // p b} :=
-subtype_congr e $ by simp
+subtype_equiv e $ by simp
 
 /-- If `α ≃ β`, then for any predicate `p : α → Prop` the subtype `{a // p a}` is equivalent
 to the subtype `{b // p (e.symm b)}`. This version is used by `equiv_rw`. -/
@@ -1145,13 +1145,13 @@ def subtype_equiv_of_subtype' {p : α → Prop} (e : α ≃ β) :
 e.symm.subtype_equiv_of_subtype.symm
 
 /-- If two predicates are equal, then the corresponding subtypes are equivalent. -/
-def subtype_congr_prop {α : Type*} {p q : α → Prop} (h : p = q) : subtype p ≃ subtype q :=
-subtype_congr (equiv.refl α) (assume a, h ▸ iff.rfl)
+def subtype_equiv_prop {α : Type*} {p q : α → Prop} (h : p = q) : subtype p ≃ subtype q :=
+subtype_equiv (equiv.refl α) (assume a, h ▸ iff.rfl)
 
 /-- The subtypes corresponding to equal sets are equivalent. -/
 @[simps apply]
 def set_congr {α : Type*} {s t : set α} (h : s = t) : s ≃ t :=
-subtype_congr_prop h
+subtype_equiv_prop h
 
 /-- A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates. This
 version allows the “inner” predicate to depend on `h : p a`. -/
@@ -1165,14 +1165,14 @@ def subtype_subtype_equiv_subtype_exists {α : Type u} (p : α → Prop) (q : su
 def subtype_subtype_equiv_subtype_inter {α : Type u} (p q : α → Prop) :
   {x : subtype p // q x.1} ≃ subtype (λ x, p x ∧ q x) :=
 (subtype_subtype_equiv_subtype_exists p _).trans $
-subtype_congr_right $ λ x, exists_prop
+subtype_equiv_right $ λ x, exists_prop
 
 /-- If the outer subtype has more restrictive predicate than the inner one,
 then we can drop the latter. -/
 def subtype_subtype_equiv_subtype {α : Type u} {p q : α → Prop} (h : ∀ {x}, q x → p x) :
   {x : subtype p // q x.1} ≃ subtype q :=
 (subtype_subtype_equiv_subtype_inter p _).trans $
-subtype_congr_right $
+subtype_equiv_right $
 assume x,
 ⟨and.right, λ h₁, ⟨h h₁, h₁⟩⟩
 
@@ -1216,7 +1216,7 @@ calc (Σ y : subtype q, {x : α // f x = y}) ≃
     apply sigma_congr_right,
     assume y,
     symmetry,
-    refine (subtype_subtype_equiv_subtype_exists _ _).trans (subtype_congr_right _),
+    refine (subtype_subtype_equiv_subtype_exists _ _).trans (subtype_equiv_right _),
     assume x,
     exact ⟨λ ⟨hp, h'⟩, congr_arg subtype.val h', λ h', ⟨(h x).2 (h'.symm ▸ y.2), subtype.eq h'⟩⟩
   end
@@ -1262,7 +1262,7 @@ def subtype_equiv_codomain (f : {x' // x' ≠ x} → Y) : {g : X → Y // g ∘
 show unique {x' // ¬ x' ≠ x}, from @equiv.unique _ _
   (show unique {x' // x' = x}, from
     { default := ⟨x, rfl⟩, uniq := λ ⟨x', h⟩, subtype.val_injective h })
-  (subtype_congr_right $ λ a, not_not)
+  (subtype_equiv_right $ λ a, not_not)
 
 @[simp] lemma coe_subtype_equiv_codomain (f : {x' // x' ≠ x} → Y) :
   (subtype_equiv_codomain f : {g : X → Y // g ∘ coe = f} → Y) = λ g, (g : X → Y) x := rfl
@@ -1470,7 +1470,7 @@ between `sᶜ` and `tᶜ`. -/
 protected def compl {α : Type u} {β : Type v} {s : set α} {t : set β} [decidable_pred s]
   [decidable_pred t] (e₀ : s ≃ t) :
   {e : α ≃ β // ∀ x : s, e x = e₀ x} ≃ ((sᶜ : set α) ≃ (tᶜ : set β)) :=
-{ to_fun := λ e, subtype_congr e
+{ to_fun := λ e, subtype_equiv e
     (λ a, not_congr $ iff.symm $ maps_to.mem_iff
       (maps_to_iff_exists_map_subtype.2 ⟨e₀, e.2⟩)
       (surj_on.maps_to_compl (surj_on_iff_exists_map_subtype.2
@@ -1490,10 +1490,10 @@ protected def compl {α : Type u} {β : Type v} {s : set α} {t : set β} [decid
           sum.map_inl, sum_congr_apply, trans_apply,
           subtype.coe_mk, set.sum_compl_apply_inl] },
       { simp only [set.sum_compl_symm_apply_of_not_mem hx, sum.map_inr,
-          subtype_congr_apply, set.sum_compl_apply_inr, trans_apply,
+          subtype_equiv_apply, set.sum_compl_apply_inr, trans_apply,
           sum_congr_apply, subtype.coe_mk] },
     end,
-  right_inv := λ e, equiv.ext $ λ x, by simp only [sum.map_inr, subtype_congr_apply,
+  right_inv := λ e, equiv.ext $ λ x, by simp only [sum.map_inr, subtype_equiv_apply,
     set.sum_compl_apply_inr, function.comp_app, sum_congr_apply, equiv.coe_trans,
     subtype.coe_eta, subtype.coe_mk, set.sum_compl_symm_apply_compl] }
 

src/data/fintype/card.lean

@@ -260,7 +260,7 @@ lemma fin.prod_univ_eq_prod_range [comm_monoid α] (f : ℕ → α) (n : ℕ) :
   ∏ i : fin n, f i = ∏ i in range n, f i :=
 calc (∏ i : fin n, f i) = ∏ i : {x // x ∈ range n}, f i :
   ((equiv.fin_equiv_subtype n).trans
-    (equiv.subtype_congr_right (λ _, mem_range.symm))).prod_comp (f ∘ coe)
+    (equiv.subtype_equiv_right (λ _, mem_range.symm))).prod_comp (f ∘ coe)
 ... = ∏ i in range n, f i : by rw [← attach_eq_univ, prod_attach]
 
 @[to_additive]
@@ -309,9 +309,9 @@ lemma fintype.prod_dite [fintype α] {p : α → Prop} [decidable_pred p]
 begin
   simp only [prod_dite, attach_eq_univ],
   congr' 1,
-  { convert (equiv.subtype_congr_right _).prod_comp (λ x : {x // p x}, f x x.2),
+  { convert (equiv.subtype_equiv_right _).prod_comp (λ x : {x // p x}, f x x.2),
     simp },
-  { convert (equiv.subtype_congr_right _).prod_comp (λ x : {x // ¬p x}, g x x.2),
+  { convert (equiv.subtype_equiv_right _).prod_comp (λ x : {x // ¬p x}, g x x.2),
     simp }
 end
 

src/field_theory/finite/polynomial.lean

@@ -162,7 +162,7 @@ calc vector_space.dim K (R σ K) =
     by rw [finsupp.dim_eq, dim_of_field, mul_one]
   ... = cardinal.mk {s : σ → ℕ | ∀ (n : σ), s n < fintype.card K } :
   begin
-    refine quotient.sound ⟨equiv.subtype_congr finsupp.equiv_fun_on_fintype $ assume f, _⟩,
+    refine quotient.sound ⟨equiv.subtype_equiv finsupp.equiv_fun_on_fintype $ assume f, _⟩,
     refine forall_congr (assume n, nat.le_sub_right_iff_add_le _),
     exact fintype.card_pos_iff.2 ⟨0⟩
   end

src/ring_theory/polynomial/symmetric.lean

@@ -156,7 +156,7 @@ lemma rename_esymm (n : ℕ) (e : σ ≃ τ) : rename e (esymm σ R n) = esymm 
 begin
   rw [esymm_eq_sum_subtype, esymm_eq_sum_subtype, (rename ⇑e).map_sum],
   let e' : {s : finset σ // s.card = n} ≃ {s : finset τ // s.card = n} :=
-  equiv.subtype_congr (equiv.finset_congr e)
+  equiv.subtype_equiv (equiv.finset_congr e)
     (by { intro, rw [equiv.finset_congr_apply, card_map] }),
   rw ← equiv.sum_comp e'.symm,
   apply fintype.sum_congr,