Revert "fix downstream changes from Quot"

This reverts commit 73e219f.

Mathlib/Algebra/Associated/Basic.lean

@@ -475,7 +475,7 @@ section CommMonoid
 variable [CommMonoid M]
 
 instance instMul : Mul (Associates M) :=
-  ⟨Quotient.map₂ (· * ·) fun _ _ _ _ h₁ h₂ ↦ mul_mul h₁ h₂⟩
+  ⟨Quotient.map₂ (· * ·) fun _ _ h₁ _ _ h₂ ↦ h₁.mul_mul h₂⟩
 
 theorem mk_mul_mk {x y : M} : Associates.mk x * Associates.mk y = Associates.mk (x * y) :=
   rfl

Mathlib/Algebra/Category/Grp/Colimits.lean

@@ -107,7 +107,7 @@ instance : Neg (ColimitType.{w} F) where
   neg := Quotient.map neg Relation.neg_1
 
 instance : Add (ColimitType.{w} F) where
-  add := Quotient.map₂ add <| fun _x x' y _y' rx ry =>
+  add := Quotient.map₂ add <| fun _x x' rx y _y' ry =>
     Setoid.trans (Relation.add_1 _ _ y rx) (Relation.add_2 x' _ _ ry)
 
 instance : AddCommGroup (ColimitType.{w} F) where

Mathlib/Algebra/Category/MonCat/Colimits.lean

@@ -122,7 +122,7 @@ instance : Inhabited (ColimitType F) := by
 
 instance monoidColimitType : Monoid (ColimitType F) where
   one := Quotient.mk _ one
-  mul := Quotient.map₂ mul fun _ x' y _ rx ry =>
+  mul := Quotient.map₂ mul fun _ x' rx y _ ry =>
     Setoid.trans (Relation.mul_1 _ _ y rx) (Relation.mul_2 x' _ _ ry)
   one_mul := Quotient.ind fun _ => Quotient.sound <| Relation.one_mul _
   mul_one := Quotient.ind fun _ => Quotient.sound <| Relation.mul_one _

Mathlib/Algebra/Category/Ring/Colimits.lean

@@ -109,7 +109,7 @@ def ColimitType : Type v :=
 instance ColimitType.instZero : Zero (ColimitType F) where zero := Quotient.mk _ zero
 
 instance ColimitType.instAdd : Add (ColimitType F) where
-  add := Quotient.map₂ add <| fun _x x' y _y' rx ry =>
+  add := Quotient.map₂ add <| fun _x x' rx y _y' ry =>
     Setoid.trans (Relation.add_1 _ _ y rx) (Relation.add_2 x' _ _ ry)
 
 instance ColimitType.instNeg : Neg (ColimitType F) where
@@ -411,7 +411,7 @@ def ColimitType : Type v :=
 instance ColimitType.instZero : Zero (ColimitType F) where zero := Quotient.mk _ zero
 
 instance ColimitType.instAdd : Add (ColimitType F) where
-  add := Quotient.map₂ add <| fun _x x' y _y' rx ry =>
+  add := Quotient.map₂ add <| fun _x x' rx y _y' ry =>
     Setoid.trans (Relation.add_1 _ _ y rx) (Relation.add_2 x' _ _ ry)
 
 instance ColimitType.instNeg : Neg (ColimitType F) where

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -1315,8 +1315,8 @@ namespace Associates
 variable [CancelCommMonoidWithZero α] [GCDMonoid α]
 
 instance instGCDMonoid : GCDMonoid (Associates α) where
-  gcd := Quotient.map₂' gcd fun _ _ _ _ (ha : Associated _ _) (hb : Associated _ _) => ha.gcd hb
-  lcm := Quotient.map₂' lcm fun _ _ _ _ (ha : Associated _ _) (hb : Associated _ _) => ha.lcm hb
+  gcd := Quotient.map₂' gcd fun _ _ (ha : Associated _ _) _ _ (hb : Associated _ _) => ha.gcd hb
+  lcm := Quotient.map₂' lcm fun _ _ (ha : Associated _ _) _ _ (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/Order/CauSeq/Completion.lean

@@ -66,7 +66,7 @@ theorem mk_eq_zero {f : CauSeq _ abv} : mk f = 0 ↔ LimZero f := by
   rwa [sub_zero] at this
 
 instance : Add (Cauchy abv) :=
-  ⟨(Quotient.map₂ (· + ·)) fun _ _ _ _ hf hg => add_equiv_add hf hg⟩
+  ⟨(Quotient.map₂ (· + ·)) fun _ _ hf _ _ hg => add_equiv_add hf hg⟩
 
 @[simp]
 theorem mk_add (f g : CauSeq β abv) : mk f + mk g = mk (f + g) :=
@@ -80,14 +80,14 @@ theorem mk_neg (f : CauSeq β abv) : -mk f = mk (-f) :=
   rfl
 
 instance : Mul (Cauchy abv) :=
-  ⟨(Quotient.map₂ (· * ·)) fun _ _ _ _ hf hg => mul_equiv_mul hf hg⟩
+  ⟨(Quotient.map₂ (· * ·)) fun _ _ hf _ _ hg => mul_equiv_mul hf hg⟩
 
 @[simp]
 theorem mk_mul (f g : CauSeq β abv) : mk f * mk g = mk (f * g) :=
   rfl
 
 instance : Sub (Cauchy abv) :=
-  ⟨(Quotient.map₂ Sub.sub) fun _ _ _ _ hf hg => sub_equiv_sub hf hg⟩
+  ⟨(Quotient.map₂ Sub.sub) fun _ _ hf _ _ hg => sub_equiv_sub hf hg⟩
 
 @[simp]
 theorem mk_sub (f g : CauSeq β abv) : mk f - mk g = mk (f - g) :=

Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean

@@ -1283,7 +1283,7 @@ variable (W') in
 /-- The addition of two point classes. If `P` is a point representative,
 then `W.addMap ⟦P⟧ ⟦Q⟧` is definitionally equivalent to `W.add P Q`. -/
 noncomputable def addMap (P Q : PointClass R) : PointClass R :=
-  Quotient.map₂ W'.add (fun _ _ _ _ hP hQ => add_equiv hP hQ) P Q
+  Quotient.map₂ W'.add (fun _ _ hP _ _ hQ => add_equiv hP hQ) P Q
 
 lemma addMap_eq (P Q : Fin 3 → R) : W'.addMap ⟦P⟧ ⟦Q⟧ = ⟦W'.add P Q⟧ :=
   rfl

Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean

@@ -1394,7 +1394,7 @@ variable (W') in
 /-- The addition of two point classes. If `P` is a point representative,
 then `W.addMap ⟦P⟧ ⟦Q⟧` is definitionally equivalent to `W.add P Q`. -/
 noncomputable def addMap (P Q : PointClass R) : PointClass R :=
-  Quotient.map₂ W'.add (fun _ _ _ _ hP hQ => add_equiv hP hQ) P Q
+  Quotient.map₂ W'.add (fun _ _ hP _ _ hQ => add_equiv hP hQ) P Q
 
 lemma addMap_eq (P Q : Fin 3 → R) : W'.addMap ⟦P⟧ ⟦Q⟧ = ⟦W'.add P Q⟧ :=
   rfl

Mathlib/CategoryTheory/Monoidal/Free/Basic.lean

@@ -139,7 +139,7 @@ open FreeMonoidalCategory.HomEquiv
 instance categoryFreeMonoidalCategory : Category.{u} (F C) where
   Hom X Y := Quotient (FreeMonoidalCategory.setoidHom X Y)
   id X := ⟦Hom.id X⟧
-  comp := Quotient.map₂ Hom.comp (fun _ _ _ _ hf hg ↦ HomEquiv.comp hf hg)
+  comp := Quotient.map₂ Hom.comp (fun _ _ hf _ _ hg ↦ HomEquiv.comp hf hg)
   id_comp := by
     rintro X Y ⟨f⟩
     exact Quotient.sound (id_comp f)
@@ -152,7 +152,7 @@ instance categoryFreeMonoidalCategory : Category.{u} (F C) where
 
 instance : MonoidalCategory (F C) where
   tensorObj X Y := FreeMonoidalCategory.tensor X Y
-  tensorHom := Quotient.map₂ Hom.tensor (fun _ _ _ _ hf hg ↦ HomEquiv.tensor hf hg)
+  tensorHom := Quotient.map₂ Hom.tensor (fun _ _ hf _ _ hg ↦ HomEquiv.tensor hf hg)
   whiskerLeft X _ _ f := Quot.map (fun f ↦ Hom.whiskerLeft X f) (fun f f' ↦ .whiskerLeft X f f') f
   whiskerRight f Y := Quot.map (fun f ↦ Hom.whiskerRight f Y) (fun f f' ↦ .whiskerRight f f' Y) f
   tensorHom_def := by

Mathlib/CategoryTheory/Skeletal.lean

@@ -224,7 +224,7 @@ def map₂ObjMap (F : C ⥤ D ⥤ E) : ThinSkeleton C → ThinSkeleton D → Thi
   fun x y =>
     @Quotient.map₂ C D (isIsomorphicSetoid C) (isIsomorphicSetoid D) E (isIsomorphicSetoid E)
       (fun X Y => (F.obj X).obj Y)
-          (fun X₁ _ _ Y₂ ⟨hX⟩ ⟨hY⟩ => ⟨(F.obj X₁).mapIso hY ≪≫ (F.mapIso hX).app Y₂⟩) x y
+          (fun X₁ _ ⟨hX⟩ _ Y₂ ⟨hY⟩ => ⟨(F.obj X₁).mapIso hY ≪≫ (F.mapIso hX).app Y₂⟩) x y
 
 /-- For each `x : ThinSkeleton C`, we promote `map₂ObjMap F x` to a functor -/
 def map₂Functor (F : C ⥤ D ⥤ E) : ThinSkeleton C → ThinSkeleton D ⥤ ThinSkeleton E :=

Mathlib/Data/Quot.lean

@@ -242,7 +242,7 @@ to a function `f : Quotient sa → Quotient sb → Quotient sc`.
 Useful to define binary operations on quotients. -/
 protected def map₂ (f : α → β → γ) (h : ∀ ⦃a₁ a₂⦄, a₁ ≈ a₂ → ∀ ⦃b₁ b₂⦄, b₁ ≈ b₂ → f a₁ b₁ ≈ f a₂ b₂) :
     Quotient sa → Quotient sb → Quotient sc :=
-  Quotient.lift₂ (fun x y ↦ ⟦f x y⟧) fun _ _ _ _ h₁ h₂ ↦ Quot.sound <| h h₁ h₂
+  Quotient.lift₂ (fun x y ↦ ⟦f x y⟧) fun _ _ _ _ h₁ h₂ ↦ Quot.sound <| h _ _ _ _ h₁ h₂
 
 @[simp]
 theorem map₂_mk (f : α → β → γ)

Mathlib/Data/Real/Basic.lean

@@ -392,7 +392,7 @@ instance nontrivial : Nontrivial ℝ :=
   inferInstance
 
 private irreducible_def sup : ℝ → ℝ → ℝ
-  | ⟨x⟩, ⟨y⟩ => ⟨Quotient.map₂ (· ⊔ ·) (fun _ _ _ _ hx hy => sup_equiv_sup hx hy) x y⟩
+  | ⟨x⟩, ⟨y⟩ => ⟨Quotient.map₂ (· ⊔ ·) (fun _ _ hx _ _ hy => sup_equiv_sup hx hy) x y⟩
 
 instance : Max ℝ :=
   ⟨sup⟩
@@ -407,7 +407,7 @@ theorem mk_sup (a b) : (mk (a ⊔ b) : ℝ) = mk a ⊔ mk b :=
   ofCauchy_sup _ _
 
 private irreducible_def inf : ℝ → ℝ → ℝ
-  | ⟨x⟩, ⟨y⟩ => ⟨Quotient.map₂ (· ⊓ ·) (fun _ _ _ _ hx hy => inf_equiv_inf hx hy) x y⟩
+  | ⟨x⟩, ⟨y⟩ => ⟨Quotient.map₂ (· ⊓ ·) (fun _ _ hx _ _ hy => inf_equiv_inf hx hy) x y⟩
 
 instance : Min ℝ :=
   ⟨inf⟩

Mathlib/Data/Setoid/Basic.lean

@@ -133,7 +133,7 @@ equivalence relations. -/
 @[simps]
 def prodQuotientEquiv (r : Setoid α) (s : Setoid β) :
     Quotient r × Quotient s ≃ Quotient (r.prod s) where
-  toFun := fun (x, y) ↦ Quotient.map₂' Prod.mk (fun _ _ _ _ hx hy ↦ ⟨hx, hy⟩) x y
+  toFun := fun (x, y) ↦ Quotient.map₂' Prod.mk (fun _ _ hx _ _ hy ↦ ⟨hx, hy⟩) x y
   invFun := fun q ↦ Quotient.liftOn' q (fun xy ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2))
     fun x y hxy ↦ Prod.ext (by simpa using hxy.1) (by simpa using hxy.2)
   left_inv := fun q ↦ by

Mathlib/GroupTheory/Congruence/Defs.lean

@@ -281,7 +281,7 @@ protected theorem eq {a b : M} : (a : c.Quotient) = (b : c.Quotient) ↔ c a b :
 @[to_additive "The addition induced on the quotient by an additive congruence relation on a type
 with an addition."]
 instance hasMul : Mul c.Quotient :=
-  ⟨Quotient.map₂' (· * ·) fun _ _ _ _ h1 h2 => c.mul h1 h2⟩
+  ⟨Quotient.map₂' (· * ·) fun _ _ h1 _ _ h2 => c.mul h1 h2⟩
 
 /-- The kernel of the quotient map induced by a congruence relation `c` equals `c`. -/
 @[to_additive (attr := simp) "The kernel of the quotient map induced by an additive congruence
@@ -739,7 +739,7 @@ instance hasInv : Inv c.Quotient :=
 @[to_additive "The subtraction induced on the quotient by an additive congruence relation on a type
 with a subtraction."]
 instance hasDiv : Div c.Quotient :=
-  ⟨(Quotient.map₂' (· / ·)) fun _ _ _ _ h₁ h₂ => c.div h₁ h₂⟩
+  ⟨(Quotient.map₂' (· / ·)) fun _ _ h₁ _ _ h₂ => c.div h₁ h₂⟩
 
 /-- The integer scaling induced on the quotient by a congruence relation on a type with a
     subtraction. -/

Mathlib/GroupTheory/Coset/Basic.lean

@@ -377,14 +377,14 @@ def quotientEquivProdOfLE' (h_le : s ≤ t) (f : α ⧸ t → α)
     ⟨a.map' id fun _ _ h => leftRel_apply.mpr (h_le (leftRel_apply.mp h)),
       a.map' (fun g : α => ⟨(f (Quotient.mk'' g))⁻¹ * g, leftRel_apply.mp (Quotient.exact' (hf g))⟩)
         fun b c h => by
-        simp only [HasEquiv.Equiv]; rw [leftRel_apply]
+        rw [leftRel_apply]
         change ((f b)⁻¹ * b)⁻¹ * ((f c)⁻¹ * c) ∈ s
         have key : f b = f c :=
           congr_arg f (Quotient.sound' (leftRel_apply.mpr (h_le (leftRel_apply.mp h))))
         rwa [key, mul_inv_rev, inv_inv, mul_assoc, mul_inv_cancel_left, ← leftRel_apply]⟩
   invFun a := by
     refine a.2.map' (fun (b : { x // x ∈ t}) => f a.1 * b) fun b c h => by
-      simp only [HasEquiv.Equiv] at *; rw [leftRel_apply] at *
+      rw [leftRel_apply] at h ⊢
       change (f a.1 * b)⁻¹ * (f a.1 * c) ∈ s
       rwa [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
   left_inv := by
@@ -412,7 +412,7 @@ def quotientSubgroupOfEmbeddingOfLE (H : Subgroup α) (h : s ≤ t) :
     s ⧸ H.subgroupOf s ↪ t ⧸ H.subgroupOf t where
   toFun :=
     Quotient.map' (inclusion h) fun a b => by
-      simp_rw [HasEquiv.Equiv, leftRel_eq]
+      simp_rw [leftRel_eq]
       exact id
   inj' :=
     Quotient.ind₂' <| by
@@ -431,7 +431,7 @@ theorem quotientSubgroupOfEmbeddingOfLE_apply_mk (H : Subgroup α) (h : s ≤ t)
 def quotientSubgroupOfMapOfLE (H : Subgroup α) (h : s ≤ t) :
     H ⧸ s.subgroupOf H → H ⧸ t.subgroupOf H :=
   Quotient.map' id fun a b => by
-    simp_rw [HasEquiv.Equiv, leftRel_eq]
+    simp_rw [leftRel_eq]
     apply h
 
 -- Porting note: I had to add the type ascription to the right-hand side or else Lean times out.
@@ -445,7 +445,7 @@ theorem quotientSubgroupOfMapOfLE_apply_mk (H : Subgroup α) (h : s ≤ t) (g :
 @[to_additive "If `s ≤ t`, then there is a map `α ⧸ s → α ⧸ t`."]
 def quotientMapOfLE (h : s ≤ t) : α ⧸ s → α ⧸ t :=
   Quotient.map' id fun a b => by
-    simp_rw [HasEquiv.Equiv, leftRel_eq]
+    simp_rw [leftRel_eq]
     apply h
 
 @[to_additive (attr := simp)]

Mathlib/GroupTheory/Coset/Defs.lean

@@ -127,12 +127,12 @@ instance rightRelDecidable [DecidablePred (· ∈ s)] : DecidableRel (rightRel s
 def quotientRightRelEquivQuotientLeftRel : Quotient (QuotientGroup.rightRel s) ≃ α ⧸ s where
   toFun :=
     Quotient.map' (fun g => g⁻¹) fun a b => by
-      simp only [HasEquiv.Equiv]; rw [leftRel_apply, rightRel_apply]
+      rw [leftRel_apply, rightRel_apply]
       exact fun h => (congr_arg (· ∈ s) (by simp [mul_assoc])).mp (s.inv_mem h)
       -- Porting note: replace with `by group`
   invFun :=
     Quotient.map' (fun g => g⁻¹) fun a b => by
-      simp only [HasEquiv.Equiv]; rw [leftRel_apply, rightRel_apply]
+      rw [leftRel_apply, rightRel_apply]
       exact fun h => (congr_arg (· ∈ s) (by simp [mul_assoc])).mp (s.inv_mem h)
       -- Porting note: replace with `by group`
   left_inv g :=

Mathlib/LinearAlgebra/Projectivization/Constructions.lean

@@ -68,7 +68,7 @@ variable [DecidableEq F]
 /-- Cross product on the projective plane. -/
 def cross : ℙ F (Fin 3 → F) → ℙ F (Fin 3 → F) → ℙ F (Fin 3 → F) :=
   Quotient.map₂' (fun v w ↦ if h : crossProduct v.1 w.1 = 0 then v else ⟨crossProduct v.1 w.1, h⟩)
-    (fun _ _ _ _ ⟨a, ha⟩ ⟨b, hb⟩ ↦ by
+    (fun _ _ ⟨a, ha⟩ _ _ ⟨b, hb⟩ ↦ by
       simp_rw [← ha, ← hb, LinearMap.map_smul_of_tower, LinearMap.smul_apply, smul_smul,
         mul_comm b a, smul_eq_zero_iff_eq]
       split_ifs

Mathlib/NumberTheory/RamificationInertia/Basic.lean

@@ -500,7 +500,6 @@ noncomputable def quotientToQuotientRangePowQuotSuccAux {i : ℕ} {a : S} (a_mem
       (P ^ i).map (Ideal.Quotient.mk (P ^ e)) ⧸ LinearMap.range (powQuotSuccInclusion f p P i) :=
   Quotient.map' (fun x : S => ⟨_, Ideal.mem_map_of_mem _ (Ideal.mul_mem_right x _ a_mem)⟩)
     fun x y h => by
-    simp only [HasEquiv.Equiv] at *
     rw [Submodule.quotientRel_def] at h ⊢
     simp only [_root_.map_mul, LinearMap.mem_range]
     refine ⟨⟨_, Ideal.mem_map_of_mem _ (Ideal.mul_mem_mul a_mem h)⟩, ?_⟩

Mathlib/Order/Filter/Germ/Basic.lean

@@ -197,7 +197,7 @@ theorem map_map (op₁ : γ → δ) (op₂ : β → γ) (f : Germ l β) :
 
 /-- Lift a binary function `β → γ → δ` to a function `Germ l β → Germ l γ → Germ l δ`. -/
 def map₂ (op : β → γ → δ) : Germ l β → Germ l γ → Germ l δ :=
-  Quotient.map₂' (fun f g x => op (f x) (g x)) fun f f' g g' Hf Hg =>
+  Quotient.map₂' (fun f g x => op (f x) (g x)) fun f f' Hf g g' Hg =>
     Hg.mp <| Hf.mono fun x Hf Hg => by simp only [Hf, Hg]
 
 @[simp]

Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean

@@ -364,7 +364,7 @@ instance hasPow : Pow (HomogeneousLocalization 𝒜 x) ℕ where
 instance : Add (HomogeneousLocalization 𝒜 x) where
   add :=
     Quotient.map₂' (· + ·)
-      fun c1 c2  c3 c4 (h : Localization.mk _ _ = Localization.mk _ _)
+      fun c1 c2 (h : Localization.mk _ _ = Localization.mk _ _) c3 c4
         (h' : Localization.mk _ _ = Localization.mk _ _) => by
       change Localization.mk _ _ = Localization.mk _ _
       simp only [num_add, den_add, ← Localization.add_mk]
@@ -377,7 +377,7 @@ instance : Sub (HomogeneousLocalization 𝒜 x) where sub z1 z2 := z1 + -z2
 instance : Mul (HomogeneousLocalization 𝒜 x) where
   mul :=
     Quotient.map₂' (· * ·)
-      fun c1 c2 c3 c4 (h : Localization.mk _ _ = Localization.mk _ _)
+      fun c1 c2 (h : Localization.mk _ _ = Localization.mk _ _) c3 c4
         (h' : Localization.mk _ _ = Localization.mk _ _) => by
       change Localization.mk _ _ = Localization.mk _ _
       simp only [num_mul, den_mul]

Mathlib/SetTheory/Cardinal/Basic.lean

@@ -174,7 +174,7 @@ theorem map_mk (f : Type u → Type v) (hf : ∀ α β, α ≃ β → f α ≃ f
 /-- Lift a binary operation `Type* → Type* → Type*` to a binary operation on `Cardinal`s. -/
 def map₂ (f : Type u → Type v → Type w) (hf : ∀ α β γ δ, α ≃ β → γ ≃ δ → f α γ ≃ f β δ) :
     Cardinal.{u} → Cardinal.{v} → Cardinal.{w} :=
-  Quotient.map₂ f fun α β γ δ ⟨e₁⟩ ⟨e₂⟩ => ⟨hf α β γ δ e₁ e₂⟩
+  Quotient.map₂ f fun α β ⟨e₁⟩ γ δ ⟨e₂⟩ => ⟨hf α β γ δ e₁ e₂⟩
 
 /-- We define the order on cardinal numbers by `#α ≤ #β` if and only if
   there exists an embedding (injective function) from α to β. -/

Mathlib/SetTheory/Game/Basic.lean

@@ -53,7 +53,7 @@ instance : Neg Game where
 
 instance : Zero Game where zero := ⟦0⟧
 instance : Add Game where
-  add := Quotient.map₂ HAdd.hAdd <| fun _ _ _ _ hx hy => PGame.add_congr hx hy
+  add := Quotient.map₂ HAdd.hAdd <| fun _ _ hx _ _ hy => PGame.add_congr hx hy
 
 instance instAddCommGroupWithOneGame : AddCommGroupWithOne Game where
   zero := ⟦0⟧

Mathlib/SetTheory/ZFC/Basic.lean

@@ -837,7 +837,7 @@ theorem eq_empty_or_nonempty (u : ZFSet) : u = ∅ ∨ u.Nonempty := by
 /-- `Insert x y` is the set `{x} ∪ y` -/
 protected def Insert : ZFSet → ZFSet → ZFSet :=
   Quotient.map₂ PSet.insert
-    fun _ _ ⟨_, _⟩ ⟨_, _⟩ uv ⟨αβ, βα⟩ =>
+    fun _ _ uv ⟨_, _⟩ ⟨_, _⟩ ⟨αβ, βα⟩ =>
       ⟨fun o =>
         match o with
         | some a =>

Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean

@@ -85,7 +85,7 @@ variable {M : Type*} [TopologicalSpace M]
 
 @[to_additive]
 instance instMul [Mul M] [ContinuousMul M] : Mul (SeparationQuotient M) where
-  mul := Quotient.map₂' (· * ·) fun _ _ _ _ h₁ h₂ ↦ Inseparable.mul h₁ h₂
+  mul := Quotient.map₂' (· * ·) fun _ _ h₁ _ _ h₂ ↦ Inseparable.mul h₁ h₂
 
 @[to_additive (attr := simp)]
 theorem mk_mul [Mul M] [ContinuousMul M] (a b : M) : mk (a * b) = mk a * mk b := rfl
@@ -168,7 +168,7 @@ instance instInvOneClass [InvOneClass G] [ContinuousInv G] :
 
 @[to_additive]
 instance instDiv [Div G] [ContinuousDiv G] : Div (SeparationQuotient G) where
-  div := Quotient.map₂' (· / ·) fun _ _ _ _ h₁ h₂ ↦ (Inseparable.prod h₁ h₂).map continuous_div'
+  div := Quotient.map₂' (· / ·) fun _ _ h₁ _ _ h₂ ↦ (Inseparable.prod h₁ h₂).map continuous_div'
 
 @[to_additive (attr := simp)]
 theorem mk_div [Div G] [ContinuousDiv G] (x y : G) : mk (x / y) = mk x / mk y := rfl

Mathlib/Topology/Homotopy/Path.lean

@@ -275,7 +275,7 @@ instance : Inhabited (Homotopic.Quotient () ()) :=
 /-- The composition of path homotopy classes. This is `Path.trans` descended to the quotient. -/
 def Quotient.comp (P₀ : Path.Homotopic.Quotient x₀ x₁) (P₁ : Path.Homotopic.Quotient x₁ x₂) :
     Path.Homotopic.Quotient x₀ x₂ :=
-  Quotient.map₂ Path.trans (fun (_ : Path x₀ x₁) _ (_ : Path x₁ x₂) _ hp hq => hcomp hp hq) P₀ P₁
+  Quotient.map₂ Path.trans (fun (_ : Path x₀ x₁) _ hp (_ : Path x₁ x₂) _ hq => hcomp hp hq) P₀ P₁
 
 theorem comp_lift (P₀ : Path x₀ x₁) (P₁ : Path x₁ x₂) : ⟦P₀.trans P₁⟧ = Quotient.comp ⟦P₀⟧ ⟦P₁⟧ :=
   rfl

Mathlib/Topology/Homotopy/Product.lean

@@ -173,7 +173,7 @@ def prodHomotopy (h₁ : Path.Homotopy p₁ p₁') (h₂ : Path.Homotopy p₂ p
 /-- The product of path classes q₁ and q₂. This is `Path.prod` descended to the quotient. -/
 def prod (q₁ : Path.Homotopic.Quotient a₁ a₂) (q₂ : Path.Homotopic.Quotient b₁ b₂) :
     Path.Homotopic.Quotient (a₁, b₁) (a₂, b₂) :=
-  Quotient.map₂ Path.prod (fun _ _ _ _ h₁ h₂ => Nonempty.map2 prodHomotopy h₁ h₂) q₁ q₂
+  Quotient.map₂ Path.prod (fun _ _ h₁ _ _ h₂ => Nonempty.map2 prodHomotopy h₁ h₂) q₁ q₂
 
 variable (p₁ p₁' p₂ p₂')