Clean up quotient APIs

Counterexamples/CliffordAlgebraNotInjective.lean

@@ -127,7 +127,7 @@ theorem X_sq (i : Fin 3) : K.gen i * K.gen i = (0 : K) := by
 
 /-- If an element multiplied by `αβγ` is zero then it squares to zero. -/
 theorem sq_zero_of_αβγ_mul {x : K} : α * β * γ * x = 0 → x * x = 0 := by
-  induction x using Quotient.inductionOn'
+  induction x using Quotient.inductionOn
   change Ideal.Quotient.mk _ _ = 0 → Ideal.Quotient.mk _ _ = 0
   rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.Quotient.eq_zero_iff_mem]
   exact mul_self_mem_kIdeal_of_X0_X1_X2_mul_mem
@@ -207,8 +207,8 @@ theorem Q'_zero_under_ideal (v : Fin 3 → K) (hv : v ∈ LinearMap.ker lFunc) :
 def Q : QuadraticForm K L :=
   QuadraticMap.ofPolar
     (fun x =>
-      Quotient.liftOn' x Q' fun a b h => by
-        rw [Submodule.quotientRel_r_def] at h
+      Quotient.liftOn x Q' fun a b h => by
+        rw [Setoid.equiv_iff_apply, Submodule.quotientRel_r_def] at h
         suffices Q' (a - b) = 0 by rwa [Q'_sub, sub_eq_zero] at this
         apply Q'_zero_under_ideal (a - b) h)
     (fun a x => by
@@ -231,7 +231,7 @@ local notation "z'" => gen 2
 theorem gen_mul_gen (i) : gen i * gen i = 1 := by
   dsimp only [gen]
   simp_rw [CliffordAlgebra.ι_sq_scalar, Q_apply, ← Submodule.Quotient.mk''_eq_mk,
-    Quotient.liftOn'_mk'', Q'_apply_single, mul_one, map_one]
+    Quotient.liftOn_mk, Q'_apply_single, mul_one, map_one]
 
 /-- By virtue of the quotient, terms of this form are zero -/
 theorem quot_obv : α • x' - β • y' - γ • z' = 0 := by

Mathlib/Algebra/Associated/Basic.lean

@@ -964,7 +964,7 @@ instance [Nontrivial α] : Nontrivial (Associates α) :=
   ⟨⟨1, 0, mk_ne_zero.2 one_ne_zero⟩⟩
 
 theorem exists_non_zero_rep {a : Associates α} : a ≠ 0 → ∃ a0 : α, a0 ≠ 0 ∧ Associates.mk a0 = a :=
-  Quotient.inductionOn a fun b nz => ⟨b, mt (congr_arg Quotient.mk'') nz, rfl⟩
+  Quotient.inductionOn a fun b nz => ⟨b, mt (congr_arg (Quotient.mk _)) nz, rfl⟩
 
 end MonoidWithZero
 

Mathlib/Algebra/BigOperators/Group/Finset.lean

@@ -1598,14 +1598,14 @@ theorem dvd_prod_of_mem (f : α → β) {a : α} {s : Finset α} (ha : a ∈ s)
 /-- A product can be partitioned into a product of products, each equivalent under a setoid. -/
 @[to_additive "A sum can be partitioned into a sum of sums, each equivalent under a setoid."]
 theorem prod_partition (R : Setoid α) [DecidableRel R.r] :
-    ∏ x ∈ s, f x = ∏ xbar ∈ s.image Quotient.mk'', ∏ y ∈ s.filter (⟦·⟧ = xbar), f y := by
+    ∏ x ∈ s, f x = ∏ xbar ∈ s.image (Quotient.mk _), ∏ y ∈ s.filter (⟦·⟧ = xbar), f y := by
   refine (Finset.prod_image' f fun x _hx => ?_).symm
   rfl
 
 /-- If we can partition a product into subsets that cancel out, then the whole product cancels. -/
 @[to_additive "If we can partition a sum into subsets that cancel out, then the whole sum cancels."]
 theorem prod_cancels_of_partition_cancels (R : Setoid α) [DecidableRel R.r]
-    (h : ∀ x ∈ s, ∏ a ∈ s.filter fun y => y ≈ x, f a = 1) : ∏ x ∈ s, f x = 1 := by
+    (h : ∀ x ∈ s, ∏ a ∈ s.filter fun y => R y x, f a = 1) : ∏ x ∈ s, f x = 1 := by
   rw [prod_partition R, ← Finset.prod_eq_one]
   intro xbar xbar_in_s
   obtain ⟨x, x_in_s, rfl⟩ := mem_image.mp xbar_in_s

Mathlib/Algebra/CharZero/Quotient.lean

@@ -51,11 +51,11 @@ namespace QuotientAddGroup
 
 theorem zmultiples_zsmul_eq_zsmul_iff {ψ θ : R ⧸ AddSubgroup.zmultiples p} {z : ℤ} (hz : z ≠ 0) :
     z • ψ = z • θ ↔ ∃ k : Fin z.natAbs, ψ = θ + ((k : ℕ) • (p / z) : R) := by
-  induction ψ using Quotient.inductionOn'
-  induction θ using Quotient.inductionOn'
+  induction ψ using Quotient.inductionOn
+  induction θ using Quotient.inductionOn
   -- Porting note: Introduced Zp notation to shorten lines
   let Zp := AddSubgroup.zmultiples p
-  have : (Quotient.mk'' : R → R ⧸ Zp) = ((↑) : R → R ⧸ Zp) := rfl
+  have : (Quotient.mk _ : R → R ⧸ Zp) = ((↑) : R → R ⧸ Zp) := rfl
   simp only [this]
   simp_rw [← QuotientAddGroup.mk_zsmul, ← QuotientAddGroup.mk_add,
     QuotientAddGroup.eq_iff_sub_mem, ← smul_sub, ← sub_sub]

Mathlib/Algebra/DirectLimit.lean

@@ -123,7 +123,7 @@ some component of the directed system. -/
 theorem exists_of [Nonempty ι] [IsDirected ι (· ≤ ·)] (z : DirectLimit G f) :
     ∃ i x, of R ι G f i x = z :=
   Nonempty.elim (by infer_instance) fun ind : ι =>
-    Quotient.inductionOn' z fun z =>
+    Quotient.inductionOn z fun z =>
       DirectSum.induction_on z ⟨ind, 0, LinearMap.map_zero _⟩ (fun i x => ⟨i, x, rfl⟩)
         fun p q ⟨i, x, ihx⟩ ⟨j, y, ihy⟩ =>
         let ⟨k, hik, hjk⟩ := exists_ge_ge i j
@@ -574,7 +574,7 @@ some component of the directed system. -/
 theorem exists_of [Nonempty ι] [IsDirected ι (· ≤ ·)] (z : DirectLimit G f) :
     ∃ i x, of G f i x = z :=
   Nonempty.elim (by infer_instance) fun ind : ι =>
-    Quotient.inductionOn' z fun x =>
+    Quotient.inductionOn z fun x =>
       FreeAbelianGroup.induction_on x ⟨ind, 0, (of _ _ ind).map_zero⟩
         (fun s =>
           Multiset.induction_on s ⟨ind, 1, (of _ _ ind).map_one⟩ fun a s ih =>
@@ -585,7 +585,7 @@ theorem exists_of [Nonempty ι] [IsDirected ι (· ≤ ·)] (z : DirectLimit G f
               rw [(of G f k).map_mul, of_f, of_f, hs]
               /- porting note: In Lean3, from here, this was `by refl`. I have added
               the lemma `FreeCommRing.of_cons` to fix this proof. -/
-              apply congr_arg Quotient.mk''
+              apply congr_arg (Quotient.mk _)
               symm
               apply FreeCommRing.of_cons⟩)
         (fun s ⟨i, x, ih⟩ => ⟨i, -x, by

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -1326,8 +1326,8 @@ namespace Associates
 variable [CancelCommMonoidWithZero α] [GCDMonoid α]
 
 instance instGCDMonoid : GCDMonoid (Associates α) where
-  gcd := Quotient.map₂' gcd fun a₁ a₂ (ha : Associated _ _) b₁ b₂ (hb : Associated _ _) => ha.gcd hb
-  lcm := Quotient.map₂' lcm fun a₁ a₂ (ha : Associated _ _) b₁ b₂ (hb : Associated _ _) => ha.lcm hb
+  gcd := Quotient.map₂ gcd fun a₁ a₂ (ha : Associated _ _) b₁ b₂ (hb : Associated _ _) => ha.gcd hb
+  lcm := Quotient.map₂ lcm fun a₁ a₂ (ha : Associated _ _) b₁ b₂ (hb : Associated _ _) => ha.lcm hb
   gcd_dvd_left := by rintro ⟨a⟩ ⟨b⟩; exact mk_le_mk_of_dvd (gcd_dvd_left _ _)
   gcd_dvd_right := by rintro ⟨a⟩ ⟨b⟩; exact mk_le_mk_of_dvd (gcd_dvd_right _ _)
   dvd_gcd := by

Mathlib/Algebra/Lie/Free.lean

@@ -126,11 +126,11 @@ instance : Sub (FreeLieAlgebra R X) where
   sub := Quot.map₂ Sub.sub (fun _ _ _ => Rel.subLeft _) fun _ _ _ => Rel.subRight _
 
 instance : AddGroup (FreeLieAlgebra R X) :=
-  Function.Surjective.addGroup (Quot.mk _) (surjective_quot_mk _) rfl (fun _ _ => rfl)
+  Function.Surjective.addGroup (Quot.mk _) Quot.surjective_mk rfl (fun _ _ => rfl)
     (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) fun _ _ => rfl
 
 instance : AddCommSemigroup (FreeLieAlgebra R X) :=
-  Function.Surjective.addCommSemigroup (Quot.mk _) (surjective_quot_mk _) fun _ _ => rfl
+  Function.Surjective.addCommSemigroup (Quot.mk _) Quot.surjective_mk fun _ _ => rfl
 
 instance : AddCommGroup (FreeLieAlgebra R X) :=
   { (inferInstance : AddGroup (FreeLieAlgebra R X)),
@@ -139,7 +139,7 @@ instance : AddCommGroup (FreeLieAlgebra R X) :=
 instance {S : Type*} [Semiring S] [Module S R] [IsScalarTower S R R] :
     Module S (FreeLieAlgebra R X) :=
   Function.Surjective.module S ⟨⟨Quot.mk (Rel R X), rfl⟩, fun _ _ => rfl⟩
-    (surjective_quot_mk _) (fun _ _ => rfl)
+    Quot.surjective_mk (fun _ _ => rfl)
 
 /-- Note that here we turn the `Mul` coming from the `NonUnitalNonAssocSemiring` structure
 on `lib R X` into a `Bracket` on `FreeLieAlgebra`. -/

Mathlib/Algebra/Lie/Quotient.lean

@@ -73,7 +73,7 @@ abbrev mk : M → M ⧸ N :=
 theorem mk_eq_zero' {m : M} : mk (N := N) m = 0 ↔ m ∈ N :=
   Submodule.Quotient.mk_eq_zero N.toSubmodule
 
-theorem is_quotient_mk (m : M) : Quotient.mk'' m = (mk m : M ⧸ N) :=
+theorem is_quotient_mk (m : M) : ⟦m⟧ = (mk m : M ⧸ N) :=
   rfl
 
 variable [LieAlgebra R L] [LieModule R L M] (I J : LieIdeal R L)
@@ -108,10 +108,10 @@ instance lieQuotientLieModule : LieModule R L (M ⧸ N) :=
 instance lieQuotientHasBracket : Bracket (L ⧸ I) (L ⧸ I) :=
   ⟨by
     intro x y
-    apply Quotient.liftOn₂' x y fun x' y' => mk ⁅x', y'⁆
+    apply Quotient.liftOn₂ x y fun x' y' => mk ⁅x', y'⁆
     intro x₁ x₂ y₁ y₂ h₁ h₂
     apply (Submodule.Quotient.eq I.toSubmodule).2
-    rw [Submodule.quotientRel_r_def] at h₁ h₂
+    rw [Setoid.equiv_iff_apply, Submodule.quotientRel_r_def] at h₁ h₂
     have h : ⁅x₁, x₂⁆ - ⁅y₁, y₂⁆ = ⁅x₁, x₂ - y₂⁆ + ⁅x₁ - y₁, y₂⁆ := by
       simp [-lie_skew, sub_eq_add_neg, add_assoc]
     rw [h]
@@ -125,27 +125,27 @@ theorem mk_bracket (x y : L) : mk ⁅x, y⁆ = ⁅(mk x : L ⧸ I), (mk y : L 
 
 instance lieQuotientLieRing : LieRing (L ⧸ I) where
   add_lie := by
-    intro x' y' z'; refine Quotient.inductionOn₃' x' y' z' ?_; intro x y z
+    intro x' y' z'; refine Quotient.inductionOn₃ x' y' z' ?_; intro x y z
     repeat'
       first
       | rw [is_quotient_mk]
       | rw [← mk_bracket]
       | rw [← Submodule.Quotient.mk_add (R := R) (M := L)]
     apply congr_arg; apply add_lie
   lie_add := by
-    intro x' y' z'; refine Quotient.inductionOn₃' x' y' z' ?_; intro x y z
+    intro x' y' z'; refine Quotient.inductionOn₃ x' y' z' ?_; intro x y z
     repeat'
       first
       | rw [is_quotient_mk]
       | rw [← mk_bracket]
       | rw [← Submodule.Quotient.mk_add (R := R) (M := L)]
     apply congr_arg; apply lie_add
   lie_self := by
-    intro x'; refine Quotient.inductionOn' x' ?_; intro x
+    intro x'; refine Quotient.inductionOn x' ?_; intro x
     rw [is_quotient_mk, ← mk_bracket]
     apply congr_arg; apply lie_self
   leibniz_lie := by
-    intro x' y' z'; refine Quotient.inductionOn₃' x' y' z' ?_; intro x y z
+    intro x' y' z'; refine Quotient.inductionOn₃ x' y' z' ?_; intro x y z
     repeat'
       first
       | rw [is_quotient_mk]
@@ -155,7 +155,7 @@ instance lieQuotientLieRing : LieRing (L ⧸ I) where
 
 instance lieQuotientLieAlgebra : LieAlgebra R (L ⧸ I) where
   lie_smul := by
-    intro t x' y'; refine Quotient.inductionOn₂' x' y' ?_; intro x y
+    intro t x' y'; refine Quotient.inductionOn₂ x' y' ?_; intro x y
     repeat'
       first
       | rw [is_quotient_mk]
@@ -171,7 +171,7 @@ def mk' : M →ₗ⁅R,L⁆ M ⧸ N :=
     map_lie' := fun {_ _} => rfl }
 
 @[simp]
-theorem surjective_mk' : Function.Surjective (mk' N) := surjective_quot_mk _
+theorem surjective_mk' : Function.Surjective (mk' N) := Quot.surjective_mk
 
 @[simp]
 theorem range_mk' : LieModuleHom.range (mk' N) = ⊤ := by simp [LieModuleHom.range_eq_top]
@@ -196,7 +196,7 @@ theorem map_mk'_eq_bot_le : map (mk' N) N' = ⊥ ↔ N' ≤ N := by
 See note [partially-applied ext lemmas]. -/
 @[ext]
 theorem lieModuleHom_ext ⦃f g : M ⧸ N →ₗ⁅R,L⁆ M⦄ (h : f.comp (mk' N) = g.comp (mk' N)) : f = g :=
-  LieModuleHom.ext fun x => Quotient.inductionOn' x <| LieModuleHom.congr_fun h
+  LieModuleHom.ext fun x => Quotient.inductionOn x <| LieModuleHom.congr_fun h
 
 lemma toEnd_comp_mk' (x : L) :
     LieModule.toEnd R L (M ⧸ N) x ∘ₗ mk' N = mk' N ∘ₗ LieModule.toEnd R L M x :=

Mathlib/Algebra/Module/Torsion.lean

@@ -499,7 +499,7 @@ instance IsTorsionBySet.isScalarTower (hM : IsTorsionBySet R M I)
     @IsScalarTower S (R ⧸ I) M _ (IsTorsionBySet.module hM).toSMul _ :=
   -- Porting note: still needed to be fed the Module R / I M instance
   @IsScalarTower.mk S (R ⧸ I) M _ (IsTorsionBySet.module hM).toSMul _
-    (fun b d x => Quotient.inductionOn' d fun c => (smul_assoc b c x : _))
+    (fun b d x => Quotient.inductionOn d fun c => (smul_assoc b c x : _))
 
 /-- An `(R ⧸ Ideal.span {r})`-module is an `R`-module for which `IsTorsionBy R M r`. -/
 abbrev IsTorsionBy.module (hM : IsTorsionBy R M r) : Module (R ⧸ Ideal.span {r}) M :=
@@ -746,7 +746,7 @@ variable [CommRing R] [AddCommGroup M] [Module R M]
 @[simp]
 theorem torsion_eq_bot : torsion R (M ⧸ torsion R M) = ⊥ :=
   eq_bot_iff.mpr fun z =>
-    Quotient.inductionOn' z fun x ⟨a, hax⟩ => by
+    Quotient.inductionOn z fun x ⟨a, hax⟩ => by
       rw [Quotient.mk''_eq_mk, ← Quotient.mk_smul, Quotient.mk_eq_zero] at hax
       rw [mem_bot, Quotient.mk''_eq_mk, Quotient.mk_eq_zero]
       cases' hax with b h

Mathlib/Algebra/Module/Zlattice/Basic.lean

@@ -247,7 +247,7 @@ def quotientEquiv [Fintype ι] :
     apply Quotient.sound'
     rwa [QuotientAddGroup.leftRel_apply, mem_toAddSubgroup, ← fract_eq_fract]
   · obtain ⟨a, rfl⟩ := fractRestrict_surjective b x
-    exact ⟨Quotient.mk'' a, rfl⟩
+    exact ⟨⟦a⟧, rfl⟩
 
 @[simp]
 theorem quotientEquiv_apply_mk [Fintype ι] (x : E) :

Mathlib/Algebra/Order/CauSeq/Completion.lean

@@ -32,7 +32,7 @@ variable {abv}
 
 /-- The map from Cauchy sequences into the Cauchy completion. -/
 def mk : CauSeq _ abv → Cauchy abv :=
-  Quotient.mk''
+  Quotient.mk _
 
 @[simp]
 theorem mk_eq_mk (f : CauSeq _ abv) : @Eq (Cauchy abv) ⟦f⟧ (mk f) :=
@@ -140,7 +140,7 @@ private theorem one_def : 1 = mk (abv := abv) 1 :=
   rfl
 
 instance Cauchy.ring : Ring (Cauchy abv) :=
-  Function.Surjective.ring mk (surjective_quotient_mk' _) zero_def.symm one_def.symm
+  Function.Surjective.ring mk Quotient.surjective_mk' zero_def.symm one_def.symm
     (fun _ _ => (mk_add _ _).symm) (fun _ _ => (mk_mul _ _).symm) (fun _ => (mk_neg _).symm)
     (fun _ _ => (mk_sub _ _).symm) (fun _ _ => (mk_smul _ _).symm) (fun _ _ => (mk_smul _ _).symm)
     (fun _ _ => (mk_pow _ _).symm) (fun _ => rfl) fun _ => rfl
@@ -165,7 +165,7 @@ variable {α : Type*} [LinearOrderedField α]
 variable {β : Type*} [CommRing β] {abv : β → α} [IsAbsoluteValue abv]
 
 instance Cauchy.commRing : CommRing (Cauchy abv) :=
-  Function.Surjective.commRing mk (surjective_quotient_mk' _) zero_def.symm one_def.symm
+  Function.Surjective.commRing mk Quotient.surjective_mk' zero_def.symm one_def.symm
     (fun _ _ => (mk_add _ _).symm) (fun _ _ => (mk_mul _ _).symm) (fun _ => (mk_neg _).symm)
     (fun _ _ => (mk_sub _ _).symm) (fun _ _ => (mk_smul _ _).symm) (fun _ _ => (mk_smul _ _).symm)
     (fun _ _ => (mk_pow _ _).symm) (fun _ => rfl) fun _ => rfl

Mathlib/Algebra/Periodic.lean

@@ -275,8 +275,8 @@ theorem Periodic.map_vadd_multiples [AddCommMonoid α] (hf : Periodic f c)
 
 /-- Lift a periodic function to a function from the quotient group. -/
 def Periodic.lift [AddGroup α] (h : Periodic f c) (x : α ⧸ AddSubgroup.zmultiples c) : β :=
-  Quotient.liftOn' x f fun a b h' => by
-    rw [QuotientAddGroup.leftRel_apply] at h'
+  Quotient.liftOn x f fun a b h' => by
+    rw [Setoid.equiv_iff_apply, QuotientAddGroup.leftRel_apply] at h'
     obtain ⟨k, hk⟩ := h'
     exact (h.zsmul k _).symm.trans (congr_arg f (add_eq_of_eq_neg_add hk))
 

Mathlib/Algebra/RingQuot.lean

@@ -35,8 +35,8 @@ namespace RingCon
 instance (c : RingCon A) : Algebra S c.Quotient where
   smul := (· • ·)
   toRingHom := c.mk'.comp (algebraMap S A)
-  commutes' _ := Quotient.ind' fun _ ↦ congr_arg Quotient.mk'' <| Algebra.commutes _ _
-  smul_def' _ := Quotient.ind' fun _ ↦ congr_arg Quotient.mk'' <| Algebra.smul_def _ _
+  commutes' _ := Quotient.ind fun _ ↦ congr_arg (Quotient.mk _) <| Algebra.commutes _ _
+  smul_def' _ := Quotient.ind fun _ ↦ congr_arg (Quotient.mk _) <| Algebra.smul_def _ _
 
 @[simp, norm_cast]
 theorem coe_algebraMap (c : RingCon A) (s : S) :

Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean

@@ -1168,7 +1168,8 @@ lemma add_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : W'.add P Q = W'.dblXYZ P
 lemma add_smul_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) {u v : R} (hu : IsUnit u) (hv : IsUnit v) :
     W'.add (u • P) (v • Q) = u ^ 4 • W'.add P Q := by
   have smul : P ≈ Q ↔ u • P ≈ v • Q := by
-    erw [← Quotient.eq, ← Quotient.eq, smul_eq P hu, smul_eq Q hv]
+    rw [Setoid.equiv_iff_apply, Setoid.equiv_iff_apply, ← Quotient.eq, ← Quotient.eq]
+    erw [smul_eq P hu, smul_eq Q hv]
     rfl
   rw [add_of_equiv <| smul.mp h, dblXYZ_smul, add_of_equiv h]
 
@@ -1184,7 +1185,8 @@ lemma add_of_not_equiv {P Q : Fin 3 → R} (h : ¬P ≈ Q) : W'.add P Q = W'.add
 lemma add_smul_of_not_equiv {P Q : Fin 3 → R} (h : ¬P ≈ Q) {u v : R} (hu : IsUnit u)
     (hv : IsUnit v) : W'.add (u • P) (v • Q) = (u * v) ^ 2 • W'.add P Q := by
   have smul : P ≈ Q ↔ u • P ≈ v • Q := by
-    erw [← Quotient.eq, ← Quotient.eq, smul_eq P hu, smul_eq Q hv]
+    rw [Setoid.equiv_iff_apply, Setoid.equiv_iff_apply, ← Quotient.eq, ← Quotient.eq]
+    erw [smul_eq P hu, smul_eq Q hv]
     rfl
   rw [add_of_not_equiv <| h.comp smul.mpr, addXYZ_smul, add_of_not_equiv h]
 

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

@@ -217,7 +217,7 @@ def toSpec (f : A) : (Proj.T| pbo f) ⟶ Spec.T A⁰_ f where
   continuous_toFun := by
     rw [PrimeSpectrum.isTopologicalBasis_basic_opens.continuous_iff]
     rintro _ ⟨x, rfl⟩
-    obtain ⟨x, rfl⟩ := Quotient.surjective_Quotient_mk'' x
+    obtain ⟨x, rfl⟩ := Quotient.surjective_mk x
     rw [ToSpec.preimage_basicOpen]
     exact (pbo x.num).2.preimage continuous_subtype_val
 

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean

@@ -299,7 +299,7 @@ open HomogeneousLocalization in
 stalk at `x` obtained by `sectionInBasicOpen`. This is the inverse of `stalkToFiberRingHom`.
 -/
 def homogeneousLocalizationToStalk (x : ProjectiveSpectrum.top 𝒜) (y : at x) :
-    (Proj.structureSheaf 𝒜).presheaf.stalk x := Quotient.liftOn' y (fun f =>
+    (Proj.structureSheaf 𝒜).presheaf.stalk x := Quotient.liftOn y (fun f =>
   (Proj.structureSheaf 𝒜).presheaf.germ ⟨x, mem_basicOpen_den _ x f⟩ (sectionInBasicOpen _ x f))
   fun f g (e : f.embedding = g.embedding) ↦ by
     simp only [HomogeneousLocalization.NumDenSameDeg.embedding, Localization.mk_eq_mk',
@@ -325,7 +325,7 @@ lemma homogeneousLocalizationToStalk_stalkToFiberRingHom (x z) :
   obtain ⟨U, hxU, s, rfl⟩ := (Proj.structureSheaf 𝒜).presheaf.germ_exist x z
   obtain ⟨V, hxV, i, n, a, b, h, e⟩ := s.2 ⟨x, hxU⟩
   simp only at e
-  rw [stalkToFiberRingHom_germ', homogeneousLocalizationToStalk, e ⟨x, hxV⟩, Quotient.liftOn'_mk'']
+  rw [stalkToFiberRingHom_germ', homogeneousLocalizationToStalk, e ⟨x, hxV⟩, Quotient.liftOn_mk]
   refine Presheaf.germ_ext _ V hxV (by exact homOfLE <| fun _ h' ↦ h ⟨_, h'⟩) i ?_
   apply Subtype.ext
   ext ⟨t, ht⟩
@@ -335,8 +335,8 @@ lemma homogeneousLocalizationToStalk_stalkToFiberRingHom (x z) :
 
 lemma stalkToFiberRingHom_homogeneousLocalizationToStalk (x z) :
     stalkToFiberRingHom 𝒜 x (homogeneousLocalizationToStalk 𝒜 x z) = z := by
-  obtain ⟨z, rfl⟩ := Quotient.surjective_Quotient_mk'' z
-  rw [homogeneousLocalizationToStalk, Quotient.liftOn'_mk'',
+  obtain ⟨z, rfl⟩ := Quotient.surjective_mk z
+  rw [homogeneousLocalizationToStalk, Quotient.liftOn_mk,
     stalkToFiberRingHom_germ', sectionInBasicOpen]
 
 /-- Using `homogeneousLocalizationToStalk`, we construct a ring isomorphism between stalk at `x`

Mathlib/Analysis/Normed/Group/Quotient.lean

@@ -265,7 +265,7 @@ theorem normedMk.apply (S : AddSubgroup M) (m : M) : normedMk S m = QuotientAddG
 
 /-- `S.normedMk` is surjective. -/
 theorem surjective_normedMk (S : AddSubgroup M) : Function.Surjective (normedMk S) :=
-  surjective_quot_mk _
+  Quot.surjective_mk
 
 /-- The kernel of `S.normedMk` is `S`. -/
 theorem ker_normedMk (S : AddSubgroup M) : S.normedMk.ker = S :=

Mathlib/Analysis/Normed/Group/SemiNormedGrp/Kernels.lean

@@ -212,7 +212,7 @@ def explicitCokernelπ {X Y : SemiNormedGrp.{u}} (f : X ⟶ Y) : Y ⟶ explicitC
 
 theorem explicitCokernelπ_surjective {X Y : SemiNormedGrp.{u}} {f : X ⟶ Y} :
     Function.Surjective (explicitCokernelπ f) :=
-  surjective_quot_mk _
+  Quot.surjective_mk
 
 @[simp, reassoc]
 theorem comp_explicitCokernelπ {X Y : SemiNormedGrp.{u}} (f : X ⟶ Y) :

Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean

@@ -66,7 +66,7 @@ theorem coe_coeHom : (coeHom : ℝ → Angle) = ((↑) : ℝ → Angle) :=
 `induction θ using Real.Angle.induction_on`. -/
 @[elab_as_elim]
 protected theorem induction_on {p : Angle → Prop} (θ : Angle) (h : ∀ x : ℝ, p x) : p θ :=
-  Quotient.inductionOn' θ h
+  Quotient.inductionOn θ h
 
 @[simp]
 theorem coe_zero : ↑(0 : ℝ) = (0 : Angle) :=