diff --git a/Mathlib/Algebra/Associated/Basic.lean b/Mathlib/Algebra/Associated/Basic.lean index 239300f0919c8..4484964fb4604 100644 --- a/Mathlib/Algebra/Associated/Basic.lean +++ b/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 diff --git a/Mathlib/Algebra/Category/Grp/Colimits.lean b/Mathlib/Algebra/Category/Grp/Colimits.lean index ecd508b712dca..ffd0441416766 100644 --- a/Mathlib/Algebra/Category/Grp/Colimits.lean +++ b/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 diff --git a/Mathlib/Algebra/Category/MonCat/Colimits.lean b/Mathlib/Algebra/Category/MonCat/Colimits.lean index 3d780afe79c0e..ac67635fefbbe 100644 --- a/Mathlib/Algebra/Category/MonCat/Colimits.lean +++ b/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 _ diff --git a/Mathlib/Algebra/Category/Ring/Colimits.lean b/Mathlib/Algebra/Category/Ring/Colimits.lean index 5bc7dec58375e..140d787c20ebf 100644 --- a/Mathlib/Algebra/Category/Ring/Colimits.lean +++ b/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 diff --git a/Mathlib/Algebra/GCDMonoid/Basic.lean b/Mathlib/Algebra/GCDMonoid/Basic.lean index 25cac18588d62..917885981d942 100644 --- a/Mathlib/Algebra/GCDMonoid/Basic.lean +++ b/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 diff --git a/Mathlib/Algebra/Order/CauSeq/Completion.lean b/Mathlib/Algebra/Order/CauSeq/Completion.lean index 2747b340ab589..283cb6611892c 100644 --- a/Mathlib/Algebra/Order/CauSeq/Completion.lean +++ b/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) := diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean index e03a5579765de..e4838de2f5dd0 100644 --- a/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean +++ b/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 diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean index f6c86fa91458b..764adaaef132b 100644 --- a/Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean +++ b/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 diff --git a/Mathlib/CategoryTheory/Monoidal/Free/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Free/Basic.lean index 7a40373795a9a..04bf2a16a1b33 100644 --- a/Mathlib/CategoryTheory/Monoidal/Free/Basic.lean +++ b/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 diff --git a/Mathlib/CategoryTheory/Skeletal.lean b/Mathlib/CategoryTheory/Skeletal.lean index fbc7382e8622f..7485a3c426aab 100644 --- a/Mathlib/CategoryTheory/Skeletal.lean +++ b/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 := diff --git a/Mathlib/Data/Quot.lean b/Mathlib/Data/Quot.lean index 5862bbd3abe83..24e901a732024 100644 --- a/Mathlib/Data/Quot.lean +++ b/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 : α → β → γ) diff --git a/Mathlib/Data/Real/Basic.lean b/Mathlib/Data/Real/Basic.lean index 76818dec116b1..a47daa561e74e 100644 --- a/Mathlib/Data/Real/Basic.lean +++ b/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⟩ diff --git a/Mathlib/Data/Setoid/Basic.lean b/Mathlib/Data/Setoid/Basic.lean index 0261ec59630b7..bbaa5b239fbfe 100644 --- a/Mathlib/Data/Setoid/Basic.lean +++ b/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 diff --git a/Mathlib/GroupTheory/Congruence/Defs.lean b/Mathlib/GroupTheory/Congruence/Defs.lean index 398f2e017e0e9..0026330ad4b73 100644 --- a/Mathlib/GroupTheory/Congruence/Defs.lean +++ b/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. -/ diff --git a/Mathlib/GroupTheory/Coset/Basic.lean b/Mathlib/GroupTheory/Coset/Basic.lean index 92b002632be39..4f8c575b67fcf 100644 --- a/Mathlib/GroupTheory/Coset/Basic.lean +++ b/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)] diff --git a/Mathlib/GroupTheory/Coset/Defs.lean b/Mathlib/GroupTheory/Coset/Defs.lean index a3def598e96b6..c57164adfbaee 100644 --- a/Mathlib/GroupTheory/Coset/Defs.lean +++ b/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 := diff --git a/Mathlib/LinearAlgebra/Projectivization/Constructions.lean b/Mathlib/LinearAlgebra/Projectivization/Constructions.lean index 943576dab69c3..fd7470292b540 100644 --- a/Mathlib/LinearAlgebra/Projectivization/Constructions.lean +++ b/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 diff --git a/Mathlib/NumberTheory/RamificationInertia/Basic.lean b/Mathlib/NumberTheory/RamificationInertia/Basic.lean index 8e69ed5882758..92cb53f8ad16f 100644 --- a/Mathlib/NumberTheory/RamificationInertia/Basic.lean +++ b/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)⟩, ?_⟩ diff --git a/Mathlib/Order/Filter/Germ/Basic.lean b/Mathlib/Order/Filter/Germ/Basic.lean index e1f28cf467151..c9ad7754c4946 100644 --- a/Mathlib/Order/Filter/Germ/Basic.lean +++ b/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] diff --git a/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean b/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean index 0288b4930ef46..82a5c54c0a72c 100644 --- a/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean +++ b/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] diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean index a7c959ce55ea7..e0105b3587892 100644 --- a/Mathlib/SetTheory/Cardinal/Basic.lean +++ b/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 β. -/ diff --git a/Mathlib/SetTheory/Game/Basic.lean b/Mathlib/SetTheory/Game/Basic.lean index e9935c18f0968..155edf8c3a215 100644 --- a/Mathlib/SetTheory/Game/Basic.lean +++ b/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⟧ diff --git a/Mathlib/SetTheory/ZFC/Basic.lean b/Mathlib/SetTheory/ZFC/Basic.lean index 326f5bbfde9f3..a2b3354096bf0 100644 --- a/Mathlib/SetTheory/ZFC/Basic.lean +++ b/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 => diff --git a/Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean b/Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean index 7e3b1c21bf93b..1f2427e29b56f 100644 --- a/Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean +++ b/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 diff --git a/Mathlib/Topology/Homotopy/Path.lean b/Mathlib/Topology/Homotopy/Path.lean index a436f74ce48a4..a5ad060e6071e 100644 --- a/Mathlib/Topology/Homotopy/Path.lean +++ b/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 diff --git a/Mathlib/Topology/Homotopy/Product.lean b/Mathlib/Topology/Homotopy/Product.lean index af60f88081b50..cc848a691b504 100644 --- a/Mathlib/Topology/Homotopy/Product.lean +++ b/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₂')