From c8922d33629788528cbfa02f9c56afb909d1c72d Mon Sep 17 00:00:00 2001 From: FR Date: Sat, 19 Oct 2024 15:25:40 +0000 Subject: [PATCH] chore: make `Quotient.mk''` an abbrev of `Quotient.mk _` (#16264) The plan is to deprecate `Quotient.mk''` in future PRs. --- Mathlib/Algebra/BigOperators/Group/Finset.lean | 4 ++-- Mathlib/Algebra/CharZero/Quotient.lean | 6 +++--- Mathlib/Data/List/Cycle.lean | 6 +++--- Mathlib/Data/Multiset/Basic.lean | 3 +++ Mathlib/Data/Quot.lean | 6 ++---- Mathlib/Data/Set/Image.lean | 2 +- Mathlib/GroupTheory/Coset/Basic.lean | 4 ++-- Mathlib/GroupTheory/GroupAction/Quotient.lean | 6 +++--- Mathlib/GroupTheory/PGroup.lean | 2 +- 9 files changed, 20 insertions(+), 19 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Group/Finset.lean b/Mathlib/Algebra/BigOperators/Group/Finset.lean index ed79af0319d28..1dbe92862bdb6 100644 --- a/Mathlib/Algebra/BigOperators/Group/Finset.lean +++ b/Mathlib/Algebra/BigOperators/Group/Finset.lean @@ -1611,13 +1611,13 @@ 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] +theorem prod_cancels_of_partition_cancels (R : Setoid α) [DecidableRel R] (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 diff --git a/Mathlib/Algebra/CharZero/Quotient.lean b/Mathlib/Algebra/CharZero/Quotient.lean index 8a44865763c7e..79b566ed37ce1 100644 --- a/Mathlib/Algebra/CharZero/Quotient.lean +++ b/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] diff --git a/Mathlib/Data/List/Cycle.lean b/Mathlib/Data/List/Cycle.lean index 9c8cbaa143209..18607fde71b44 100644 --- a/Mathlib/Data/List/Cycle.lean +++ b/Mathlib/Data/List/Cycle.lean @@ -824,11 +824,11 @@ theorem chain_ne_nil (r : α → α → Prop) {l : List α} : theorem chain_map {β : Type*} {r : α → α → Prop} (f : β → α) {s : Cycle β} : Chain r (s.map f) ↔ Chain (fun a b => r (f a) (f b)) s := - Quotient.inductionOn' s fun l => by + Quotient.inductionOn s fun l => by cases' l with a l · rfl - dsimp only [Chain, ← mk''_eq_coe, Quotient.liftOn'_mk'', Cycle.map, Quotient.map', Quot.map, - Quotient.mk'', Quotient.liftOn', Quotient.liftOn, Quot.liftOn_mk, List.map] + dsimp only [Chain, Quotient.liftOn_mk, Cycle.map, Quotient.map', Quot.map, + Quotient.liftOn', Quotient.liftOn, Quot.liftOn_mk, List.map] rw [← concat_eq_append, ← List.map_concat, List.chain_map f] simp diff --git a/Mathlib/Data/Multiset/Basic.lean b/Mathlib/Data/Multiset/Basic.lean index e04ef7fa7a1dc..97366784110f6 100644 --- a/Mathlib/Data/Multiset/Basic.lean +++ b/Mathlib/Data/Multiset/Basic.lean @@ -67,6 +67,9 @@ theorem coe_eq_coe {l₁ l₂ : List α} : (l₁ : Multiset α) = l₂ ↔ l₁ instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ ≈ l₂) := inferInstanceAs (Decidable (l₁ ~ l₂)) +instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (isSetoid α l₁ l₂) := + inferInstanceAs (Decidable (l₁ ~ l₂)) + -- Porting note: `Quotient.recOnSubsingleton₂ s₁ s₂` was in parens which broke elaboration instance decidableEq [DecidableEq α] : DecidableEq (Multiset α) | s₁, s₂ => Quotient.recOnSubsingleton₂ s₁ s₂ fun _ _ => decidable_of_iff' _ Quotient.eq_iff_equiv diff --git a/Mathlib/Data/Quot.lean b/Mathlib/Data/Quot.lean index 2bec860ba95b9..8dfbafe4dbf99 100644 --- a/Mathlib/Data/Quot.lean +++ b/Mathlib/Data/Quot.lean @@ -546,8 +546,8 @@ several different quotient relations on a type, for example quotient groups, rin -- Porting note: Quotient.mk' is the equivalent of Lean 3's `Quotient.mk` /-- A version of `Quotient.mk` taking `{s : Setoid α}` as an implicit argument instead of an instance argument. -/ -protected def mk'' (a : α) : Quotient s₁ := - Quot.mk s₁.1 a +protected abbrev mk'' (a : α) : Quotient s₁ := + ⟦a⟧ /-- `Quotient.mk''` is a surjective function. -/ theorem surjective_Quotient_mk'' : Function.Surjective (Quotient.mk'' : α → Quotient s₁) := @@ -693,7 +693,6 @@ protected theorem eq' {s₁ : Setoid α} {a b : α} : @Quotient.mk' α s₁ a = @Quotient.mk' α s₁ b ↔ s₁ a b := Quotient.eq -@[simp] protected theorem eq'' {a b : α} : @Quotient.mk'' α s₁ a = Quotient.mk'' b ↔ s₁ a b := Quotient.eq @@ -725,7 +724,6 @@ protected theorem liftOn₂'_mk {t : Setoid β} (f : α → β → γ) (h) (a : Quotient.liftOn₂' (Quotient.mk s a) (Quotient.mk t b) f h = f a b := Quotient.liftOn₂'_mk'' _ _ _ _ -@[simp] theorem map'_mk {t : Setoid β} (f : α → β) (h) (x : α) : (Quotient.mk s x).map' f h = (Quotient.mk t (f x)) := rfl diff --git a/Mathlib/Data/Set/Image.lean b/Mathlib/Data/Set/Image.lean index 00387c99f2202..1da452c8964d3 100644 --- a/Mathlib/Data/Set/Image.lean +++ b/Mathlib/Data/Set/Image.lean @@ -836,7 +836,7 @@ theorem range_quotient_lift [s : Setoid ι] (hf) : theorem range_quotient_mk' {s : Setoid α} : range (Quotient.mk' : α → Quotient s) = univ := range_quot_mk _ -@[simp] lemma Quotient.range_mk'' {sa : Setoid α} : range (Quotient.mk'' (s₁ := sa)) = univ := +lemma Quotient.range_mk'' {sa : Setoid α} : range (Quotient.mk'' (s₁ := sa)) = univ := range_quotient_mk @[simp] diff --git a/Mathlib/GroupTheory/Coset/Basic.lean b/Mathlib/GroupTheory/Coset/Basic.lean index e7aa809a354ae..c5df256757ef5 100644 --- a/Mathlib/GroupTheory/Coset/Basic.lean +++ b/Mathlib/GroupTheory/Coset/Basic.lean @@ -491,7 +491,7 @@ open MulAction in lemma orbit_mk_eq_smul (x : α) : MulAction.orbitRel.Quotient.orbit (x : α ⧸ s) = x • s := by ext rw [orbitRel.Quotient.mem_orbit] - simpa [mem_smul_set_iff_inv_smul_mem, ← leftRel_apply] using Setoid.comm' _ + simpa [mem_smul_set_iff_inv_smul_mem, ← leftRel_apply, Quotient.eq''] using Setoid.comm' _ @[to_additive] lemma orbit_eq_out'_smul (x : α ⧸ s) : MulAction.orbitRel.Quotient.orbit x = x.out' • s := by @@ -530,7 +530,7 @@ noncomputable def groupEquivQuotientProdSubgroup : α ≃ (α ⧸ s) × s := show (_root_.Subtype fun x : α => Quotient.mk'' x = L) ≃ _root_.Subtype fun x : α => Quotient.mk'' x = Quotient.mk'' _ - simp [-Quotient.eq''] + simp rfl _ ≃ Σ _L : α ⧸ s, s := Equiv.sigmaCongrRight fun _ => leftCosetEquivSubgroup _ _ ≃ (α ⧸ s) × s := Equiv.sigmaEquivProd _ _ diff --git a/Mathlib/GroupTheory/GroupAction/Quotient.lean b/Mathlib/GroupTheory/GroupAction/Quotient.lean index f58416df124ac..e532945e65310 100644 --- a/Mathlib/GroupTheory/GroupAction/Quotient.lean +++ b/Mathlib/GroupTheory/GroupAction/Quotient.lean @@ -320,10 +320,10 @@ noncomputable def equivSubgroupOrbitsSetoidComap (H : Subgroup α) (ω : Ω) : toFun := fun q ↦ q.liftOn' (fun x ↦ ⟦⟨↑x, by simp only [Set.mem_preimage, Set.mem_singleton_iff] have hx := x.property - rwa [orbitRel.Quotient.mem_orbit, @Quotient.mk''_eq_mk] at hx⟩⟧) fun a b h ↦ by - simp only [← Quotient.eq'', Quotient.mk''_eq_mk, + rwa [orbitRel.Quotient.mem_orbit] at hx⟩⟧) fun a b h ↦ by + simp only [← Quotient.eq, orbitRel.Quotient.subgroup_quotient_eq_iff] at h - simp only [← Quotient.mk''_eq_mk, Quotient.eq''] at h ⊢ + simp only [Quotient.eq] at h ⊢ exact h invFun := fun q ↦ q.liftOn' (fun x ↦ ⟦⟨↑x, by have hx := x.property diff --git a/Mathlib/GroupTheory/PGroup.lean b/Mathlib/GroupTheory/PGroup.lean index d882d7e22ca40..eb9cdfbf182a9 100644 --- a/Mathlib/GroupTheory/PGroup.lean +++ b/Mathlib/GroupTheory/PGroup.lean @@ -179,7 +179,7 @@ theorem card_modEq_card_fixedPoints : Nat.card α ≡ Nat.card (fixedPoints G α rw [Nat.card_eq_fintype_card] at hk have : k = 0 := by contrapose! hb - simp [-Quotient.eq'', key, hk, hb] + simp [-Quotient.eq, key, hk, hb] exact ⟨⟨b, mem_fixedPoints_iff_card_orbit_eq_one.2 <| by rw [hk, this, pow_zero]⟩, Finset.mem_univ _, ne_of_eq_of_ne Nat.cast_one one_ne_zero, rfl⟩