From 46840dd6db66bec979e5f84b45ebabc0654e5fd9 Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Mon, 16 Mar 2026 09:43:44 -0400 Subject: [PATCH 1/8] fix --- Mathlib/Data/Set/Basic.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean index 1a11e7891601fa..6b0d15d0441323 100644 --- a/Mathlib/Data/Set/Basic.lean +++ b/Mathlib/Data/Set/Basic.lean @@ -141,10 +141,13 @@ instance (s : Set α) : CoeTC s α := ⟨fun x => x.1⟩ theorem Set.coe_eq_subtype (s : Set α) : ↥s = { x // x ∈ s } := rfl -@[simp] theorem Set.coe_setOf (p : α → Prop) : ↥{ x | p x } = { x // p x } := rfl +@[simp] +theorem SetCoe.mk_eq_mk {s : Set α} {a : α} {h : a ∈ s} {a' : α} {h' : a' ∈ s} : + @Eq s ⟨a, h⟩ ⟨a', h'⟩ ↔ a = a' := Subtype.mk_eq_mk + theorem SetCoe.forall {s : Set α} {p : s → Prop} : (∀ x : s, p x) ↔ ∀ (x) (h : x ∈ s), p ⟨x, h⟩ := Subtype.forall From f5edda5116bcb454eeaece75a28353584af269f4 Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Tue, 19 May 2026 10:21:20 -0400 Subject: [PATCH 2/8] remove theorem --- Mathlib/Data/Set/Basic.lean | 4 ---- 1 file changed, 4 deletions(-) diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean index 6b0d15d0441323..9c1b117355263e 100644 --- a/Mathlib/Data/Set/Basic.lean +++ b/Mathlib/Data/Set/Basic.lean @@ -144,10 +144,6 @@ theorem Set.coe_eq_subtype (s : Set α) : ↥s = { x // x ∈ s } := theorem Set.coe_setOf (p : α → Prop) : ↥{ x | p x } = { x // p x } := rfl -@[simp] -theorem SetCoe.mk_eq_mk {s : Set α} {a : α} {h : a ∈ s} {a' : α} {h' : a' ∈ s} : - @Eq s ⟨a, h⟩ ⟨a', h'⟩ ↔ a = a' := Subtype.mk_eq_mk - theorem SetCoe.forall {s : Set α} {p : s → Prop} : (∀ x : s, p x) ↔ ∀ (x) (h : x ∈ s), p ⟨x, h⟩ := Subtype.forall From 14e4bd3aee6e372a270ce9a2ac33492a8b439dd9 Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Tue, 19 May 2026 11:48:40 -0400 Subject: [PATCH 3/8] fix problems --- Mathlib/CategoryTheory/GradedObject/Monoidal.lean | 1 + Mathlib/CategoryTheory/Sites/Sieves.lean | 4 ++-- Mathlib/Data/Set/Finite/Lattice.lean | 1 + 3 files changed, 4 insertions(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/GradedObject/Monoidal.lean b/Mathlib/CategoryTheory/GradedObject/Monoidal.lean index 5fe1ad5ce46d3e..a1232f70751d25 100644 --- a/Mathlib/CategoryTheory/GradedObject/Monoidal.lean +++ b/Mathlib/CategoryTheory/GradedObject/Monoidal.lean @@ -604,6 +604,7 @@ instance (n : ℕ) : Finite ((fun (i : ℕ × ℕ) => i.1 + i.2) ⁻¹' {n}) := rintro ⟨⟨_, _⟩, _⟩ ⟨⟨_, _⟩, _⟩ h simpa using h +set_option backward.isDefEq.respectTransparency false in instance (n : ℕ) : Finite ({ i : (ℕ × ℕ × ℕ) | i.1 + i.2.1 + i.2.2 = n }) := by refine Finite.of_injective (fun ⟨⟨i₁, i₂, i₃⟩, (hi : i₁ + i₂ + i₃ = n)⟩ => (⟨⟨i₁, by lia⟩, ⟨i₂, by lia⟩, ⟨i₃, by lia⟩⟩ : diff --git a/Mathlib/CategoryTheory/Sites/Sieves.lean b/Mathlib/CategoryTheory/Sites/Sieves.lean index 0c4c9d76e45d69..7b5ddc4c7c4b71 100644 --- a/Mathlib/CategoryTheory/Sites/Sieves.lean +++ b/Mathlib/CategoryTheory/Sites/Sieves.lean @@ -1334,7 +1334,7 @@ def shrinkFunctorUliftFunctorIso [LocallySmall.{w} C] [LocallySmall.{max w' w} C fun {U V} f ↦ by dsimp ext - dsimp [Equiv.subtypeEquiv] + dsimp [Equiv.subtypeEquiv_apply] rw [shrinkYonedaObjObjEquiv_obj_map, shrinkYonedaObjObjEquiv_symm_comp] simp @@ -1352,7 +1352,7 @@ variable (S) in noncomputable def shrinkFunctorIsoFunctor : (shrinkFunctor.{v₁} S).toFunctor ≅ S.functor := NatIso.ofComponents (fun Y ↦ Equiv.toIso <| Equiv.subtypeEquiv shrinkYonedaObjObjEquiv (by simp)) fun {U V} f ↦ by - dsimp [Equiv.subtypeEquiv] + dsimp [Equiv.subtypeEquiv_apply] ext simp [shrinkYonedaObjObjEquiv_obj_map] diff --git a/Mathlib/Data/Set/Finite/Lattice.lean b/Mathlib/Data/Set/Finite/Lattice.lean index 591f14dfd653bb..30f25af7ad4126 100644 --- a/Mathlib/Data/Set/Finite/Lattice.lean +++ b/Mathlib/Data/Set/Finite/Lattice.lean @@ -266,6 +266,7 @@ theorem eq_finite_iUnion_of_finite_subset_iUnion {ι} {s : ι → Set α} {t : S variable {s t : Set α} +set_option backward.isDefEq.respectTransparency false in theorem infinite_iUnion {ι : Type*} [Infinite ι] {s : ι → Set α} (hs : Function.Injective s) : (⋃ i, s i).Infinite := fun hfin ↦ @not_injective_infinite_finite ι _ _ hfin.finite_subsets.to_subtype From 65d205452fd2ff35f11e2a66d4e188342dec88d9 Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Tue, 19 May 2026 12:30:16 -0400 Subject: [PATCH 4/8] more problems fixed --- .../AlgebraicTopology/SimplicialSet/StdSimplex.lean | 6 ++---- .../SpecialFunctions/Trigonometric/Inverse.lean | 3 ++- .../CategoryTheory/Sites/Coherent/RegularSheaves.lean | 7 ++++--- Mathlib/CategoryTheory/Sites/IsSheafFor.lean | 2 +- .../Combinatorics/SimpleGraph/Connectivity/Finite.lean | 6 +++--- Mathlib/GroupTheory/Perm/Finite.lean | 10 +++------- 6 files changed, 15 insertions(+), 19 deletions(-) diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean b/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean index f6a9115000fb31..7755b1883d5589 100644 --- a/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean +++ b/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean @@ -599,12 +599,10 @@ identify to subsets of `Fin (n + 1)` of cardinality `d + 1`. -/ (Δ[n] : SSet.{u}).nonDegenerate d ≃ { S : Finset (Fin (n + 1)) | S.card = d + 1 } := Equiv.ofBijective _ (bijective_image_objEquiv_toOrderHom_univ n d) -set_option backward.isDefEq.respectTransparency false in lemma nonDegenerateEquiv'_iff {n d : ℕ} (x : (Δ[n] : SSet.{u}).nonDegenerate d) (j : Fin (n + 1)) : j ∈ (nonDegenerateEquiv' x).val ↔ ∃ (i : Fin (d + 1)), x.val i = j := by - simp only [Set.mem_setOf_eq, Set.coe_setOf] - dsimp [nonDegenerateEquiv'] - aesop + unfold nonDegenerateEquiv' + simp /-- If `x` is a nondegenerate `d`-simplex of `Δ[n]`, this is the order isomorphism between `Fin (d + 1)` and the corresponding subset of `Fin (n + 1)` of cardinality `d + 1`. -/ diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean index 2e2a96d53c67e8..0c7892ceb9a7ee 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean @@ -40,7 +40,8 @@ set_option backward.isDefEq.respectTransparency false in @[simp] theorem range_arcsin : range arcsin = Icc (-(π / 2)) (π / 2) := by rw [arcsin, range_comp Subtype.val] - simp [Icc] + ext + simp theorem arcsin_le_pi_div_two (x : ℝ) : arcsin x ≤ π / 2 := (arcsin_mem_Icc x).2 diff --git a/Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean b/Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean index 46eb44cd86094a..c1db21939377fa 100644 --- a/Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean +++ b/Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean @@ -106,7 +106,7 @@ theorem EqualizerCondition.bijective_mapToEqualizer_pullback' {P : Cᵒᵖ ⥤ T simpa [mapToEqualizer] using ha₁ · intro y h apply ha₂ y - simpa [mapToEqualizer, Subtype.ext_iff] using h + simpa [mapToEqualizer] using Subtype.ext_iff.1 h theorem EqualizerCondition.bijective_mapToEqualizer_pullback {P : Cᵒᵖ ⥤ Type*} (hP : EqualizerCondition P) {X B : C} (π : X ⟶ B) [EffectiveEpi π] [HasPullback π π] : @@ -125,10 +125,11 @@ theorem EqualizerCondition.mk' (P : Cᵒᵖ ⥤ Type*) intro b hb obtain ⟨a, ha₁, ha₂⟩ := hP ⟨b, hb⟩ refine ⟨a, ?_, ?_⟩ - · simpa [Subtype.ext_iff, mapToEqualizer] using ha₁ + · simpa [mapToEqualizer] using Subtype.ext_iff.1 ha₁ · intro y h apply ha₂ y - simpa [mapToEqualizer, Subtype.ext_iff] using h + ext + simpa [mapToEqualizer] using h set_option backward.isDefEq.respectTransparency false in theorem EqualizerCondition.mk (P : Cᵒᵖ ⥤ Type*) diff --git a/Mathlib/CategoryTheory/Sites/IsSheafFor.lean b/Mathlib/CategoryTheory/Sites/IsSheafFor.lean index 6c481804ee1e28..ddc18b141ee9e6 100644 --- a/Mathlib/CategoryTheory/Sites/IsSheafFor.lean +++ b/Mathlib/CategoryTheory/Sites/IsSheafFor.lean @@ -539,7 +539,7 @@ theorem isSheafFor_iff_yonedaSheafCondition {P : Cᵒᵖ ⥤ Type v₁} : dsimp [functor] simp only [Subtype.forall, shrinkYonedaObjObjEquiv.forall_congr_left, Equiv.apply_symm_apply] congr! - simp [Equiv.subtypeEquiv] + simp /-- If `P` is a sheaf for the sieve `S` on `X`, a natural transformation from `S` (viewed as a functor) diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Finite.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Finite.lean index c1359d16dac765..0c265c4bdd44f5 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Finite.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Finite.lean @@ -114,9 +114,9 @@ lemma ncard_oddComponents_mono [Finite V] {G' : SimpleGraph V} (h : G ≤ G') : G'.oddComponents.ncard ≤ G.oddComponents.ncard := by have aux (c : G'.ConnectedComponent) (hc : Odd c.supp.ncard) : {c' : G.ConnectedComponent | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp}.Nonempty := by - refine Set.nonempty_of_ncard_ne_zero fun h' ↦ ?_ - simpa [-Nat.card_eq_fintype_card, -Set.coe_setOf, h'] - using (c.odd_oddComponents_ncard_subset_supp _ h).2 hc + refine Set.nonempty_of_ncard_ne_zero fun h' ↦ Nat.not_odd_zero ?_ + rw [← h'] + exact (c.odd_oddComponents_ncard_subset_supp _ h).2 hc let f : G'.oddComponents → G.oddComponents := fun ⟨c, hc⟩ ↦ ⟨(aux c hc).choose, (aux c hc).choose_spec.1⟩ refine Nat.card_le_card_of_injective f fun c c' fcc' ↦ ?_ diff --git a/Mathlib/GroupTheory/Perm/Finite.lean b/Mathlib/GroupTheory/Perm/Finite.lean index 929c5833c09478..4fbb18d909c321 100644 --- a/Mathlib/GroupTheory/Perm/Finite.lean +++ b/Mathlib/GroupTheory/Perm/Finite.lean @@ -125,7 +125,6 @@ theorem perm_mapsTo_inl_iff_mapsTo_inr {m n : Type*} [Finite m] [Finite n] (σ : obtain ⟨y, hy⟩ := h ⟨r, rfl⟩ grind -set_option backward.isDefEq.respectTransparency false in theorem mem_sumCongrHom_range_of_perm_mapsTo_inl {m n : Type*} [Finite m] [Finite n] {σ : Perm (m ⊕ n)} (h : Set.MapsTo σ (Set.range Sum.inl) (Set.range Sum.inl)) : σ ∈ (sumCongrHom m n).range := by @@ -143,14 +142,11 @@ theorem mem_sumCongrHom_range_of_perm_mapsTo_inl {m n : Type*} [Finite m] [Finit rw [Perm.sumCongrHom_apply] ext (a | b) · rw [Equiv.sumCongr_apply, Sum.map_inl, permCongr_apply, Equiv.symm_symm, - apply_ofInjective_symm Sum.inl_injective] - rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk] - dsimp [Set.range] - rw [subtypePerm_apply] + apply_ofInjective_symm Sum.inl_injective, ofInjective_apply] + rfl · rw [Equiv.sumCongr_apply, Sum.map_inr, permCongr_apply, Equiv.symm_symm, apply_ofInjective_symm Sum.inr_injective, ofInjective_apply] - dsimp [Set.range] - rw [subtypePerm_apply] + rfl nonrec theorem Disjoint.orderOf {σ τ : Perm α} (hστ : Disjoint σ τ) : orderOf (σ * τ) = Nat.lcm (orderOf σ) (orderOf τ) := From bbe8752584d73af46a9ceb910bdfde13b89453ab Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Tue, 19 May 2026 12:37:27 -0400 Subject: [PATCH 5/8] undo `set_option backward.isDefEq.respectTransparency false in` --- Mathlib/CategoryTheory/GradedObject/Monoidal.lean | 5 ++--- Mathlib/Data/Set/Finite/Lattice.lean | 3 +-- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/Mathlib/CategoryTheory/GradedObject/Monoidal.lean b/Mathlib/CategoryTheory/GradedObject/Monoidal.lean index a1232f70751d25..5502098d6e0204 100644 --- a/Mathlib/CategoryTheory/GradedObject/Monoidal.lean +++ b/Mathlib/CategoryTheory/GradedObject/Monoidal.lean @@ -604,13 +604,12 @@ instance (n : ℕ) : Finite ((fun (i : ℕ × ℕ) => i.1 + i.2) ⁻¹' {n}) := rintro ⟨⟨_, _⟩, _⟩ ⟨⟨_, _⟩, _⟩ h simpa using h -set_option backward.isDefEq.respectTransparency false in instance (n : ℕ) : Finite ({ i : (ℕ × ℕ × ℕ) | i.1 + i.2.1 + i.2.2 = n }) := by refine Finite.of_injective (fun ⟨⟨i₁, i₂, i₃⟩, (hi : i₁ + i₂ + i₃ = n)⟩ => (⟨⟨i₁, by lia⟩, ⟨i₂, by lia⟩, ⟨i₃, by lia⟩⟩ : Fin (n + 1) × Fin (n + 1) × Fin (n + 1))) ?_ - rintro ⟨⟨_, _, _⟩, _⟩ ⟨⟨_, _, _⟩, _⟩ h - simpa using h + intro _ _ h + exact Subtype.ext (congrArg (fun x => (x.1.1, x.2.1.1, x.2.2.1)) h) /-! The monoidal category structure on `GradedObject ℕ C` can be inferred diff --git a/Mathlib/Data/Set/Finite/Lattice.lean b/Mathlib/Data/Set/Finite/Lattice.lean index 30f25af7ad4126..b1756f6f2888c3 100644 --- a/Mathlib/Data/Set/Finite/Lattice.lean +++ b/Mathlib/Data/Set/Finite/Lattice.lean @@ -266,11 +266,10 @@ theorem eq_finite_iUnion_of_finite_subset_iUnion {ι} {s : ι → Set α} {t : S variable {s t : Set α} -set_option backward.isDefEq.respectTransparency false in theorem infinite_iUnion {ι : Type*} [Infinite ι] {s : ι → Set α} (hs : Function.Injective s) : (⋃ i, s i).Infinite := fun hfin ↦ @not_injective_infinite_finite ι _ _ hfin.finite_subsets.to_subtype - (fun i ↦ ⟨s i, subset_iUnion _ _⟩) fun i j h_eq ↦ hs (by simpa using h_eq) + (fun i ↦ ⟨s i, subset_iUnion _ _⟩) fun _ _ h_eq ↦ hs (Subtype.ext_iff.1 h_eq) theorem Infinite.biUnion {ι : Type*} {s : ι → Set α} {a : Set ι} (ha : a.Infinite) (hs : a.InjOn s) : (⋃ i ∈ a, s i).Infinite := by From 98c315721a1087ce5cd57ea2d4aa0ae4d319a669 Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Sat, 23 May 2026 16:13:09 -0400 Subject: [PATCH 6/8] fix stuff --- Mathlib/FieldTheory/SeparablyGenerated.lean | 21 +++++++++++-------- .../LinearAlgebra/RootSystem/OfBilinear.lean | 4 ++-- .../DedekindDomain/Ideal/Lemmas.lean | 2 +- 3 files changed, 15 insertions(+), 12 deletions(-) diff --git a/Mathlib/FieldTheory/SeparablyGenerated.lean b/Mathlib/FieldTheory/SeparablyGenerated.lean index 7709e744bdd61f..a5d0caab61e6de 100644 --- a/Mathlib/FieldTheory/SeparablyGenerated.lean +++ b/Mathlib/FieldTheory/SeparablyGenerated.lean @@ -64,18 +64,21 @@ theorem aeval_toPolynomialAdjoinImageCompl_eq_zero simp_rw [toPolynomialAdjoinImageCompl, ← AlgEquiv.coe_algHom, ← AlgHom.comp_apply] congr; ext; aesop (add simp optionEquivLeft_X_some) (add simp optionEquivLeft_X_none) -set_option backward.isDefEq.respectTransparency false in theorem irreducible_toPolynomialAdjoinImageCompl {F : MvPolynomial ι k} (hF : Irreducible F) (i : ι) (H : AlgebraicIndependent k fun x : {j | j ≠ i} ↦ a x) : Irreducible (toPolynomialAdjoinImageCompl F a i) := by - have : a '' {i}ᶜ = Set.range (fun x : {j | j ≠ i} ↦ a x) := by ext; simp - delta toPolynomialAdjoinImageCompl - convert hF.map (renameEquiv k (Equiv.optionSubtypeNe i).symm) |>.map (optionEquivLeft k _) |>.map - (Polynomial.mapAlgEquiv (H.aevalEquiv.trans - (Subalgebra.equivOfEq _ _ congr(Algebra.adjoin k $this.symm)))) - rw [← AlgEquiv.coe_algHom] - congr - aesop + classical + unfold toPolynomialAdjoinImageCompl + have hc : a '' {i}ᶜ = Set.range (fun x : {j | j ≠ i} ↦ a x) := by ext; simp + let d : {j // j ≠ i} ≃ {j | j ≠ i} := .subtypeEquivRight (by simp) + refine (congrArg Irreducible ?_).mp <| + hF.map (renameEquiv k ((Equiv.optionSubtypeNe i).symm)) |>.map + (optionEquivLeft k _) |>.map (Polynomial.mapAlgEquiv <| + (renameEquiv k d).trans <| H.aevalEquiv.trans + (Subalgebra.equivOfEq _ _ congr(Algebra.adjoin k $hc.symm))) + rw [Polynomial.coe_mapAlgEquiv, Polynomial.coe_mapAlgHom] + refine congrFun (congrArg Polynomial.map ?_) _ + ext <;> simp [d] -- Suppose `F` has minimal total degree among the relations of `a`. variable {F : MvPolynomial ι k} diff --git a/Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean b/Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean index 6e3c62637c840b..ef492ed032e12a 100644 --- a/Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean +++ b/Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean @@ -160,8 +160,8 @@ def ofBilinear [IsReflexive R M] (B : M →ₗ[R] M →ₗ[R] R) (hNB : LinearMa right_inv := by intro y simp [involutive_reflection (coroot_apply_self B x.2) y] } - reflectionPerm_root x y := by - simp [Module.reflection_apply] + reflectionPerm_root := by + simp [coe_setOf, Module.reflection_apply] reflectionPerm_coroot x y := by simp only [coe_setOf, mem_setOf_eq, Embedding.coeFn_mk, Embedding.subtype_apply, Dual.eval_apply, Equiv.coe_fn_mk] diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean index 261fc6880813c5..559f6c12a38065 100644 --- a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean +++ b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean @@ -738,7 +738,7 @@ def normalizedFactorsEquivOfQuotEquiv (hI : I ≠ ⊥) (hJ : J ≠ ⊥) : idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors f.symm hI j.prop⟩ left_inv := fun ⟨j, hj⟩ => by simp - right_inv := fun ⟨j, hj⟩ => by simp [-Set.coe_setOf] + right_inv := fun ⟨j, hj⟩ => by simp @[deprecated (since := "2026-04-16")] alias _root_.normalizedFactorsEquivOfQuotEquiv := normalizedFactorsEquivOfQuotEquiv From 04d5da51ab0ac94ef68cdf02cc6bb9caabb06d6b Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Sat, 23 May 2026 16:13:48 -0400 Subject: [PATCH 7/8] how did this even happen --- Mathlib/NumberTheory/KummerDedekind.lean | 29 ++++++++++++------------ 1 file changed, 14 insertions(+), 15 deletions(-) diff --git a/Mathlib/NumberTheory/KummerDedekind.lean b/Mathlib/NumberTheory/KummerDedekind.lean index c94ea99c074d1f..a1308146eb8fe1 100644 --- a/Mathlib/NumberTheory/KummerDedekind.lean +++ b/Mathlib/NumberTheory/KummerDedekind.lean @@ -205,7 +205,6 @@ theorem Ideal.irreducible_map_of_irreducible_minpoly (hI : IsMaximal I) (hI' : I rw [Multiset.attach_map_val, Multiset.map_singleton, Subtype.coe_mk] exact normalizedFactors_irreducible hf -set_option backward.isDefEq.respectTransparency false in open Set Classical in /-- Let `Q` be a lift of factor of the minimal polynomial of `x`, a generator of `S` over `R`, taken `mod I`. Then (the reduction of) `Q` corresponds via @@ -217,19 +216,19 @@ theorem normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span (hI' : I ≠ ⊥) (hx : (conductor R x).comap (algebraMap R S) ⊔ I = ⊤) (hx' : IsIntegral R x) : ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm ⟨_, hQ⟩).val = span (I.map (algebraMap R S) ∪ {Q.aeval x}) := by - dsimp [normalizedFactorsMapEquivNormalizedFactorsMinPolyMk, - Ideal.normalizedFactorsEquivSpanNormalizedFactors] - rw [IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv_symm] - dsimp [IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv, - IsDedekindDomain.idealFactorsEquivOfQuotEquiv, OrderIso.ofHomInv] - simp only [map_span, image_singleton, coe_coe, quotMapEquivQuotQuotMap_symm_apply hx hx' Q] - refine le_antisymm (fun a ha ↦ ?_) (span_le.mpr <| union_subset_iff.mpr <| - ⟨le_comap_of_map_le (by simp), by simp⟩) - rw [mem_comap, Ideal.mem_span_singleton] at ha - obtain ⟨a', ha'⟩ := ha - obtain ⟨b, hb⟩ := Ideal.Quotient.mk_surjective a' - rw [← hb, ← map_mul, Quotient.mk_eq_mk_iff_sub_mem] at ha' - rw [union_comm, span_union, span_eq, mem_span_singleton_sup] - exact ⟨b, a - Q.aeval x * b, ha', by ring⟩ + unfold normalizedFactorsMapEquivNormalizedFactorsMinPolyMk + Ideal.normalizedFactorsEquivSpanNormalizedFactors + rw [Equiv.symm_trans_apply, IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv_symm] + unfold IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv + rw [Equiv.coe_fn_mk, Equiv.symm_symm, Equiv.ofBijective_apply] + dsimp only + unfold IsDedekindDomain.idealFactorsEquivOfQuotEquiv + rw [OrderIso.ofHomInv_apply] + erw [IsDedekindDomain.idealFactorsFunOfQuotHom_coe_coe] + dsimp only + rw [map_span, image_singleton, map_span, image_singleton, coe_coe, + quotMapEquivQuotQuotMap_symm_apply, span_union, span_eq, sup_comm, + ← image_singleton, ← map_span, Ideal.comap_map_of_surjective' _ Ideal.Quotient.mk_surjective, + Ideal.mk_ker] end KummerDedekind From 7bef264f84637939fcd293ddc3601922e6817bca Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Sat, 23 May 2026 17:31:27 -0400 Subject: [PATCH 8/8] fix archive --- Archive/Imo/Imo1987Q1.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Archive/Imo/Imo1987Q1.lean b/Archive/Imo/Imo1987Q1.lean index a305e520745fbd..a489c7420754bd 100644 --- a/Archive/Imo/Imo1987Q1.lean +++ b/Archive/Imo/Imo1987Q1.lean @@ -44,9 +44,10 @@ def fixedPointsEquiv : { σx : α × Perm α // σx.2 σx.1 = σx.1 } ≃ Σ x : theorem card_fixed_points : card { σx : α × Perm α // σx.2 σx.1 = σx.1 } = card α * (card α - 1)! := by simp only [card_congr (fixedPointsEquiv α), card_sigma, card_perm] - have (x : _) : ({x}ᶜ : Set α) = Finset.filter (· ≠ x) Finset.univ := by + have h (x : α) : ({x}ᶜ : Set α) = Finset.univ.erase x := by ext; simp - simp [this] + simp_rw [h, Fintype.card_subtype, SetLike.mem_coe, Finset.filter_univ_mem] + simp /-- Given `α : Type*` and `k : ℕ`, `fiber α k` is the set of permutations of `α` with exactly `k` fixed points. -/