diff --git a/LeanPool/ConwayRefinement/CombinatorialGames/Game/IGame.lean b/LeanPool/ConwayRefinement/CombinatorialGames/Game/IGame.lean index 151c73a717..86ef72d84f 100644 --- a/LeanPool/ConwayRefinement/CombinatorialGames/Game/IGame.lean +++ b/LeanPool/ConwayRefinement/CombinatorialGames/Game/IGame.lean @@ -17,9 +17,7 @@ public import Mathlib.Order.Comparable import LeanPool.ConwayRefinement.CombinatorialGames.Game.Functor import LeanPool.ConwayRefinement.CombinatorialGames.Mathlib.Small -import Mathlib.Lean.PrettyPrinter.Delaborator import Mathlib.Logic.Hydra -import Mathlib.Order.GameAdd /-! # Combinatorial (pre-)games diff --git a/LeanPool/ConwayRefinement/CombinatorialGames/Game/Ordinal.lean b/LeanPool/ConwayRefinement/CombinatorialGames/Game/Ordinal.lean index 99a5ea4000..6fd8833c87 100644 --- a/LeanPool/ConwayRefinement/CombinatorialGames/Game/Ordinal.lean +++ b/LeanPool/ConwayRefinement/CombinatorialGames/Game/Ordinal.lean @@ -10,7 +10,6 @@ public import LeanPool.ConwayRefinement.CombinatorialGames.NatOrdinal.Basic public import Mathlib.Algebra.Order.Hom.Monoid import LeanPool.ConwayRefinement.CombinatorialGames.Tactic.GameCmp -import Mathlib.Algebra.Order.Hom.Monoid import Mathlib.Data.Set.Finite.Lattice /-! diff --git a/LeanPool/ConwayRefinement/CombinatorialGames/Game/Player.lean b/LeanPool/ConwayRefinement/CombinatorialGames/Game/Player.lean index aa99e052b3..51ece89233 100644 --- a/LeanPool/ConwayRefinement/CombinatorialGames/Game/Player.lean +++ b/LeanPool/ConwayRefinement/CombinatorialGames/Game/Player.lean @@ -8,11 +8,10 @@ module public import Mathlib.Algebra.Ring.Defs public import Mathlib.Algebra.Group.Defs public import Mathlib.Data.Finset.Insert -import Mathlib.Algebra.Ring.Defs public import Mathlib.Data.Fintype.Defs public import Mathlib.Logic.Small.Defs -import Mathlib.Tactic.DeriveFintype + /-! # Type of players diff --git a/LeanPool/ConwayRefinement/CombinatorialGames/Mathlib/Small.lean b/LeanPool/ConwayRefinement/CombinatorialGames/Mathlib/Small.lean index c1429e0707..1fda9f72f9 100644 --- a/LeanPool/ConwayRefinement/CombinatorialGames/Mathlib/Small.lean +++ b/LeanPool/ConwayRefinement/CombinatorialGames/Mathlib/Small.lean @@ -8,8 +8,6 @@ module public import Mathlib.Logic.Small.Defs import Mathlib.Logic.Small.Set -import Mathlib.Logic.Relation -import Mathlib.Order.SetNotation /-! # Tree with small sets of branches is small diff --git a/LeanPool/ConwayRefinement/CombinatorialGames/Surreal/Basic.lean b/LeanPool/ConwayRefinement/CombinatorialGames/Surreal/Basic.lean index 7e52b91077..4dfb2ebb4b 100644 --- a/LeanPool/ConwayRefinement/CombinatorialGames/Surreal/Basic.lean +++ b/LeanPool/ConwayRefinement/CombinatorialGames/Surreal/Basic.lean @@ -7,7 +7,6 @@ module public import LeanPool.ConwayRefinement.CombinatorialGames.Game.Birthday -import LeanPool.ConwayRefinement.CombinatorialGames.Tactic.AddInstances import Mathlib.Data.Int.Cast.Lemmas /-! diff --git a/LeanPool/ConwayRefinement/CombinatorialGames/Surreal/Division.lean b/LeanPool/ConwayRefinement/CombinatorialGames/Surreal/Division.lean index 84d7c3a505..8f8193919a 100644 --- a/LeanPool/ConwayRefinement/CombinatorialGames/Surreal/Division.lean +++ b/LeanPool/ConwayRefinement/CombinatorialGames/Surreal/Division.lean @@ -12,7 +12,7 @@ public import Mathlib.Algebra.Order.Ring.Unbundled.Rat import Mathlib.Algebra.Order.Field.Basic import Mathlib.Data.Rat.Cast.Order import Mathlib.Tactic.Abel -import Mathlib.Tactic.Ring +import Mathlib.Tactic.Ring.RingNF /-! # Surreal division diff --git a/LeanPool/ConwayRefinement/CombinatorialGames/Surreal/Pow.lean b/LeanPool/ConwayRefinement/CombinatorialGames/Surreal/Pow.lean index 59b899e38f..f8c5245b2b 100644 --- a/LeanPool/ConwayRefinement/CombinatorialGames/Surreal/Pow.lean +++ b/LeanPool/ConwayRefinement/CombinatorialGames/Surreal/Pow.lean @@ -40,7 +40,12 @@ public section -- TODO: upstream theorem Set.image2_eq_range {α β γ : Type*} (f : α → β → γ) (s : Set α) (t : Set β) : Set.image2 f s t = Set.range (fun x : s × t ↦ f x.1 x.2) := by - aesop + ext x + constructor + · rintro ⟨a, ha, b, hb, rfl⟩ + exact ⟨(⟨a, ha⟩, ⟨b, hb⟩), rfl⟩ + · rintro ⟨⟨a, b⟩, rfl⟩ + exact ⟨a, a.property, b, b.property, rfl⟩ namespace ArchimedeanClass diff --git a/LeanPool/ConwayRefinement/CombinatorialGames/Tactic/GameCmp.lean b/LeanPool/ConwayRefinement/CombinatorialGames/Tactic/GameCmp.lean index 21ed1b3eec..ecc825b6a1 100644 --- a/LeanPool/ConwayRefinement/CombinatorialGames/Tactic/GameCmp.lean +++ b/LeanPool/ConwayRefinement/CombinatorialGames/Tactic/GameCmp.lean @@ -5,9 +5,10 @@ Authors: Violeta Hernández Palacios -/ module + public import LeanPool.ConwayRefinement.CombinatorialGames.Game.IGame -meta import LeanPool.ConwayRefinement.CombinatorialGames.Tactic.Register +import LeanPool.ConwayRefinement.CombinatorialGames.Tactic.Register /-! # Tactic for game inequalities diff --git a/LeanPool/ConwayRefinement/CombinatorialGames/Tactic/OrdinalAlias.lean b/LeanPool/ConwayRefinement/CombinatorialGames/Tactic/OrdinalAlias.lean index eb9e65f7b6..c142aca30c 100644 --- a/LeanPool/ConwayRefinement/CombinatorialGames/Tactic/OrdinalAlias.lean +++ b/LeanPool/ConwayRefinement/CombinatorialGames/Tactic/OrdinalAlias.lean @@ -5,7 +5,7 @@ Authors: Violeta Hernández Palacios -/ module -public import Mathlib.SetTheory.Ordinal.Family +public import Mathlib.SetTheory.Ordinal.Family -- shake: keep /-! # Declare type aliases of `Ordinal` diff --git a/LeanPool/ConwayRefinement/CombinatorialGames/Tactic/Register.lean b/LeanPool/ConwayRefinement/CombinatorialGames/Tactic/Register.lean index dbc4be836f..e77bdbfda5 100644 --- a/LeanPool/ConwayRefinement/CombinatorialGames/Tactic/Register.lean +++ b/LeanPool/ConwayRefinement/CombinatorialGames/Tactic/Register.lean @@ -7,7 +7,7 @@ module public import Mathlib.Init public meta import Lean.LabelAttribute -- TODO: `registerLabelAttr` should be marked `meta` -import Lean.Meta.Tactic.Simp.Attr +meta import Lean.Meta.Tactic.Simp.Attr /-! We register a `simp` attribute for the `game_cmp` tactic. This needs to be done in a separate file diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/DirectSum/GermSuccessorStep.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/DirectSum/GermSuccessorStep.lean index 5cf94918ae..6c49732727 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/DirectSum/GermSuccessorStep.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/DirectSum/GermSuccessorStep.lean @@ -614,7 +614,7 @@ theorem injectiveAt_of_forall_lt [CharZero K] (hgz : GradeZeroScalars A) rw [Finset.sum_comm] refine Finset.sum_congr rfl fun t ht ↦ ?_ rw [hsum' t ht, Finset.sum_mul] - exact Finset.sum_congr rfl fun b _ ↦ by ring + exact Finset.sum_congr rfl fun b _ ↦ by ac_rfl -- the evaluated syzygy, homogeneous of degree `δ` obtain ⟨u, hu'⟩ : ∃ u : ↥B → R, ∀ b, u b = aeval x (W b) := ⟨_, fun _ ↦ rfl⟩ have hsyz : ∑ b : ↥B, aeval x (c b) * u b = 0 := by diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/DirectSum/HomogeneousDivisibility.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/DirectSum/HomogeneousDivisibility.lean index 00dace4d95..e91b5439ab 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/DirectSum/HomogeneousDivisibility.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/DirectSum/HomogeneousDivisibility.lean @@ -8,7 +8,6 @@ module public import Mathlib.Algebra.DirectSum.Ring import Mathlib.Algebra.BigOperators.Ring.Finset -import Mathlib.Algebra.GroupWithZero.Divisibility /-! # Divisibility by homogeneous elements in graded direct sums diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/DirectSum/HomogeneousPrime.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/DirectSum/HomogeneousPrime.lean index 8e6b6befc9..5a5877862c 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/DirectSum/HomogeneousPrime.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/DirectSum/HomogeneousPrime.lean @@ -8,7 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.DirectSum.HomogeneousDivisibility public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.DirectSum.LeadingGrade -import Mathlib.Tactic.Abel import Mathlib.Algebra.Ring.Divisibility.Basic public import Mathlib.Algebra.Prime.Defs diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Divisibility/DenominatorIdeal.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Divisibility/DenominatorIdeal.lean index 6879eab0e2..61659230b9 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Divisibility/DenominatorIdeal.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Divisibility/DenominatorIdeal.lean @@ -10,7 +10,7 @@ public import Mathlib.Algebra.Ring.Subring.Basic public import Mathlib.RingTheory.Ideal.Defs import Mathlib.Tactic.FieldSimp -import Mathlib.Tactic.Ring +import Mathlib.Tactic.Ring.RingNF /-! # Denominator ideals and four-factor refinement @@ -80,12 +80,12 @@ theorem exists_common_divisor_denominatorIdeal_iff_exists_fourFactorRefinement change ξ * (y : R) = (g : K) * (h : K) rw [hyg] change ξ * ((s : K) * g) = (g : K) * (ξ * s) - ring + ac_rfl · apply Subtype.ext change ξ * (x : R) = (f : K) * (h : K) rw [hxf] change ξ * ((s : K) * f) = (f : K) * (ξ * s) - ring + ac_rfl · rintro ⟨e, f, g, h, hxf, _, hyg, hxh⟩ have hf0 : (f : K) ≠ 0 := by intro hf @@ -98,10 +98,10 @@ theorem exists_common_divisor_denominatorIdeal_iff_exists_fourFactorRefinement have hξe : ξ * (e : K) = (h : K) := by apply mul_right_cancel₀ hf0 calc - (ξ * (e : K)) * f = ξ * ((e : K) * f) := by ring + (ξ * (e : K)) * f = ξ * ((e : K) * f) := by ac_rfl _ = ξ * (x : K) := by rw [hxfK] _ = (f : K) * h := hxhK - _ = (h : K) * f := by ring + _ = (h : K) * f := by ac_rfl let s : denominatorIdeal R ξ := ⟨e, (mem_denominatorIdeal_iff R ξ e).2 (by rw [hξe]; exact h.2)⟩ exact ⟨s, ⟨f, hxf⟩, ⟨g, hyg⟩⟩ @@ -122,7 +122,7 @@ theorem hasFourFactorRefinement_iff_forall_denominatorIdeal_exists_common_diviso apply hR.refine apply Subtype.ext change (x : K) * (ξ * (y : R)) = (y : K) * (ξ * (x : R)) - ring + ac_rfl · intro h apply hasFourFactorRefinement_def.mpr intro a b c d habcd diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Divisibility/PrimalPreimage.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Divisibility/PrimalPreimage.lean index 07a0ccf19e..51a089e96e 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Divisibility/PrimalPreimage.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Divisibility/PrimalPreimage.lean @@ -10,9 +10,9 @@ public import Mathlib.Algebra.Algebra.Subalgebra.Basic public import Mathlib.Algebra.Ring.Subring.Basic public import Mathlib.Algebra.Field.Subfield.Basic public import Mathlib.Algebra.GroupWithZero.Divisibility -import Mathlib.Tactic.Ring import Mathlib.Tactic.FieldSimp import LeanPool.ConwayRefinement.ConwayRefinement.Blueprint +import Mathlib.Tactic.Ring.RingNF /-! # Primality in a ring cut out by a residue condition @@ -200,7 +200,7 @@ theorem fracSubring_eq_top_of_isPrimal_of_residue_eq_zero refine ⟨P, Subtype.ext ?_⟩ change algebraMap L A x * p * (algebraMap L A x⁻¹ * p) = p * p rw [show algebraMap L A x * p * (algebraMap L A x⁻¹ * p) = - algebraMap L A (x * x⁻¹) * (p * p) by rw [map_mul]; ring, + algebraMap L A (x * x⁻¹) * (p * p) by rw [map_mul]; ac_rfl, mul_inv_cancel₀ hx, map_one, one_mul] obtain ⟨p₁, p₂, hp₁, hp₂, hprod⟩ := hp hdiv have hprodA : p = (p₁ : A) * p₂ := congrArg Subtype.val hprod @@ -210,9 +210,9 @@ theorem fracSubring_eq_top_of_isPrimal_of_residue_eq_zero have hcancel : p * (algebraMap L A x⁻¹ * (p₁ : A)) = p * (q : A) := by calc p * (algebraMap L A x⁻¹ * (p₁ : A)) = - (p₁ : A) * (algebraMap L A x⁻¹ * p) := by ring + (p₁ : A) * (algebraMap L A x⁻¹ * p) := by ac_rfl _ = (p₁ : A) * ((p₂ : A) * q) := by rw [hDA] - _ = p * q := by rw [hprodA]; ring + _ = p * q := by rw [hprodA]; ac_rfl have hscalar : algebraMap L A x⁻¹ * (p₁ : A) = q := mul_left_cancel₀ hp0 hcancel have hres : x⁻¹ * π (p₁ : A) = π (q : A) := by @@ -229,9 +229,9 @@ theorem fracSubring_eq_top_of_isPrimal_of_residue_eq_zero have hcancel : p * (algebraMap L A x * (p₂ : A)) = p * (q : A) := by calc p * (algebraMap L A x * (p₂ : A)) = - (p₂ : A) * (algebraMap L A x * p) := by ring + (p₂ : A) * (algebraMap L A x * p) := by ac_rfl _ = (p₂ : A) * ((p₁ : A) * q) := by rw [hCA] - _ = p * q := by rw [hprodA]; ring + _ = p * q := by rw [hprodA]; ac_rfl have hscalar : algebraMap L A x * (p₂ : A) = q := mul_left_cancel₀ hp0 hcancel have hres : x * π (p₂ : A) = π (q : A) := by @@ -277,8 +277,8 @@ theorem isPrimal_residue_of_isPrimal {b : A} (hb : π b ∈ S) refine ⟨⟨algebraMap L A e, hmem3⟩, Subtype.ext ?_⟩ change algebraMap L A c * (algebraMap L A d * b') = b * algebraMap L A e calc algebraMap L A c * (algebraMap L A d * b') - = algebraMap L A (c * d * (π b)⁻¹) * b := by rw [hb', map_mul, map_mul]; ring - _ = b * algebraMap L A e := by rw [hce]; ring + = algebraMap L A (c * d * (π b)⁻¹) * b := by rw [hb', map_mul, map_mul]; ac_rfl + _ = b * algebraMap L A e := by rw [hce]; ac_rfl obtain ⟨b₁, b₂, h₁, h₂, hprod⟩ := h key refine ⟨residueHom π S b₁, residueHom π S b₂, ?_, ?_, ?_⟩ · simpa [residueHom, Subtype.ext_iff] using map_dvd (residueHom π S) h₁ @@ -305,11 +305,11 @@ theorem isPrimal_of_isPrimal_residueSubring {b : A} (hb : π b ∈ S) calc (nrm π c * nrm π d) * (algebraMap L A (scale π c) * algebraMap L A (scale π d)) = (nrm π c * algebraMap L A (scale π c)) - * (nrm π d * algebraMap L A (scale π d)) := by ring + * (nrm π d * algebraMap L A (scale π d)) := by ac_rfl _ = c * d := by rw [hc, hd] calc nrm π c * nrm π d = (nrm π c * nrm π d) * algebraMap L A σ * algebraMap L A σ⁻¹ := by rw [mul_assoc, ← map_mul, mul_inv_cancel₀ hσ0, map_one, mul_one] - _ = b * (e * algebraMap L A σ⁻¹) := by rw [this, hcd]; ring + _ = b * (e * algebraMap L A σ⁻¹) := by rw [this, hcd]; ac_rfl set w : A := e * algebraMap L A (σ⁻¹ * π b) with hw have hres : π w = π (nrm π c) * π (nrm π d) := by have h2 := congrArg π hsplit @@ -327,9 +327,9 @@ theorem isPrimal_of_isPrimal_residueSubring {b : A} (hb : π b ∈ S) refine ⟨⟨w, hmemw⟩, Subtype.ext ?_⟩ change nrm π c * algebraMap L A (π b) * nrm π d = b * w calc nrm π c * algebraMap L A (π b) * nrm π d - = (nrm π c * nrm π d) * algebraMap L A (π b) := by ring + = (nrm π c * nrm π d) * algebraMap L A (π b) := by ac_rfl _ = (b * (e * algebraMap L A σ⁻¹)) * algebraMap L A (π b) := by rw [hsplit] - _ = b * (e * algebraMap L A (σ⁻¹ * π b)) := by rw [map_mul]; ring + _ = b * (e * algebraMap L A (σ⁻¹ * π b)) := by rw [map_mul]; ac_rfl _ = b * w := by rw [hw] obtain ⟨b₁, b₂, h₁, h₂, hprod⟩ := h key refine ⟨(b₁ : A), (b₂ : A), ?_, ?_, ?_⟩ @@ -344,13 +344,13 @@ theorem isPrimal_of_isPrimal_residueSubring {b : A} (hb : π b ∈ S) rw [mul_inv_cancel₀ hb0, map_one, mul_one] _ = nrm π c * algebraMap L A (π b) * (algebraMap L A (scale π c) * algebraMap L A (π b)⁻¹) := by - rw [map_mul]; ring - _ = (b₁ : A) * ((u : A) * algebraMap L A (scale π c * (π b)⁻¹)) := by rw [hu']; ring + rw [map_mul]; ac_rfl + _ = (b₁ : A) * ((u : A) * algebraMap L A (scale π c * (π b)⁻¹)) := by rw [hu']; ac_rfl · obtain ⟨u, hu⟩ := h₂ refine ⟨(u : A) * algebraMap L A (scale π d), ?_⟩ have hu' : nrm π d = (b₂ : A) * u := congrArg Subtype.val hu calc d = nrm π d * algebraMap L A (scale π d) := hd.symm - _ = (b₂ : A) * ((u : A) * algebraMap L A (scale π d)) := by rw [hu']; ring + _ = (b₂ : A) * ((u : A) * algebraMap L A (scale π d)) := by rw [hu']; ac_rfl · exact congrArg Subtype.val hprod /-- Converse, case `π b ≠ 0`: primal residue plus primal in the ambient algebra gives primal @@ -365,7 +365,7 @@ theorem isPrimal_residueSubring_of_isPrimal {b : A} (hb : π b ∈ S) (hb0 : π obtain ⟨b₁, b₂, ⟨f, hf⟩, ⟨g, hg⟩, hprod⟩ := hA (Dvd.intro _ hcd.symm) -- cancellation, available because `A` is a domain and `b ≠ 0` have hefg : (e : A) = f * g := by - have : b * (e : A) = b * (f * g) := by rw [← hcd, hf, hg, hprod]; ring + have : b * (e : A) = b * (f * g) := by rw [← hcd, hf, hg, hprod]; ac_rfl exact mul_left_cancel₀ hbne this have hpb : π b = π b₁ * π b₂ := by rw [hprod, map_mul] have hb₁0 : π b₁ ≠ 0 := fun h ↦ hb0 (by rw [hpb, h, zero_mul]) @@ -389,12 +389,12 @@ theorem isPrimal_residueSubring_of_isPrimal {b : A} (hb : π b ∈ S) (hb0 : π field_simp have e₂ : π (b₂ * algebraMap L A η) = b₂' := by simp only [map_mul, AlgHom.commutes, Algebra.algebraMap_self, RingHom.id_apply, hη] - have : π b₂ * (π b₁ * b₁'⁻¹) = (π b₁ * π b₂) * b₁'⁻¹ := by ring + have : π b₂ * (π b₁ * b₁'⁻¹) = (π b₁ * π b₂) * b₁'⁻¹ := by ac_rfl rw [this, ← hpb, hbb]; field_simp have e₃ : π (f * algebraMap L A η) = s := by have hpc : π c = π b₁ * π f := by rw [hf, map_mul] simp only [map_mul, AlgHom.commutes, Algebra.algebraMap_self, RingHom.id_apply, hη] - have : π f * (π b₁ * b₁'⁻¹) = (π b₁ * π f) * b₁'⁻¹ := by ring + have : π f * (π b₁ * b₁'⁻¹) = (π b₁ * π f) * b₁'⁻¹ := by ac_rfl rw [this, ← hpc, hcs]; field_simp have hηinv : η⁻¹ = b₁' * (π b₁)⁻¹ := by rw [hη]; field_simp have e₄ : π (g * algebraMap L A η⁻¹) = u := by @@ -404,23 +404,23 @@ theorem isPrimal_residueSubring_of_isPrimal {b : A} (hb : π b ∈ S) (hb0 : π have h5 : π g * (b₁' * (π b₁)⁻¹) * (π b₁ * π b₂) = (π b₂ * π g) * b₁' := by field_simp rw [h5, hpd, hdu, show u * (π b₁ * π b₂) = u * π b by rw [hpb], hbb] - ring + ac_rfl refine ⟨⟨b₁ * algebraMap L A η⁻¹, mem_residueSubring.mpr (by rw [e₁]; exact hb₁')⟩, ⟨b₂ * algebraMap L A η, mem_residueSubring.mpr (by rw [e₂]; exact hb₂')⟩, ?_, ?_, ?_⟩ · exact ⟨⟨f * algebraMap L A η, mem_residueSubring.mpr (by rw [e₃]; exact hs)⟩, Subtype.ext (by change (c : A) = b₁ * algebraMap L A η⁻¹ * (f * algebraMap L A η) rw [hf, show b₁ * algebraMap L A η⁻¹ * (f * algebraMap L A η) - = b₁ * f * (algebraMap L A η⁻¹ * algebraMap L A η) by ring, ← map_mul, + = b₁ * f * (algebraMap L A η⁻¹ * algebraMap L A η) by ac_rfl, ← map_mul, inv_mul_cancel₀ hη0, map_one, mul_one])⟩ · exact ⟨⟨g * algebraMap L A η⁻¹, mem_residueSubring.mpr (by rw [e₄]; exact hu)⟩, Subtype.ext (by change (d : A) = b₂ * algebraMap L A η * (g * algebraMap L A η⁻¹) rw [hg, show b₂ * algebraMap L A η * (g * algebraMap L A η⁻¹) - = b₂ * g * (algebraMap L A η * algebraMap L A η⁻¹) by ring, ← map_mul, + = b₂ * g * (algebraMap L A η * algebraMap L A η⁻¹) by ac_rfl, ← map_mul, mul_inv_cancel₀ hη0, map_one, mul_one])⟩ · refine Subtype.ext ?_ change b = b₁ * algebraMap L A η⁻¹ * (b₂ * algebraMap L A η) rw [hprod, show b₁ * algebraMap L A η⁻¹ * (b₂ * algebraMap L A η) - = b₁ * b₂ * (algebraMap L A η⁻¹ * algebraMap L A η) by ring, ← map_mul, + = b₁ * b₂ * (algebraMap L A η⁻¹ * algebraMap L A η) by ac_rfl, ← map_mul, inv_mul_cancel₀ hη0, map_one, mul_one] /-! ### Lemma 9.2.1, case `π b = 0` -/ @@ -444,12 +444,12 @@ theorem isPrimal_fracSubring_of_isPrimal_residueSubring {b : A} (hb : π b ∈ S calc (nrm π (c : A) * nrm π (d : A)) * (algebraMap L A (scale π (c : A)) * algebraMap L A (scale π (d : A))) = (nrm π (c : A) * algebraMap L A (scale π (c : A))) - * (nrm π (d : A) * algebraMap L A (scale π (d : A))) := by ring + * (nrm π (d : A) * algebraMap L A (scale π (d : A))) := by ac_rfl _ = (c : A) * d := by rw [hc, hd] calc nrm π (c : A) * nrm π (d : A) = (nrm π (c : A) * nrm π (d : A)) * algebraMap L A σ * algebraMap L A σ⁻¹ := by rw [mul_assoc, ← map_mul, mul_inv_cancel₀ hσ0, map_one, mul_one] - _ = b * ((e : A) * algebraMap L A σ⁻¹) := by rw [h1, hcd]; ring + _ = b * ((e : A) * algebraMap L A σ⁻¹) := by rw [h1, hcd]; ac_rfl -- the quotient's residue lies in `Frac S`; clear its denominator set w : A := (e : A) * algebraMap L A σ⁻¹ with hw have hwF : π w ∈ fracSubring S := by @@ -468,9 +468,9 @@ theorem isPrimal_fracSubring_of_isPrimal_residueSubring {b : A} (hb : π b ∈ S refine ⟨⟨w * algebraMap L A s, hmemw⟩, Subtype.ext ?_⟩ change nrm π (c : A) * algebraMap L A s * nrm π (d : A) = b * (w * algebraMap L A s) calc nrm π (c : A) * algebraMap L A s * nrm π (d : A) - = (nrm π (c : A) * nrm π (d : A)) * algebraMap L A s := by ring + = (nrm π (c : A) * nrm π (d : A)) * algebraMap L A s := by ac_rfl _ = (b * w) * algebraMap L A s := by rw [hsplit, hw] - _ = b * (w * algebraMap L A s) := by ring + _ = b * (w * algebraMap L A s) := by ac_rfl obtain ⟨b₁, b₂, ⟨v, hv⟩, ⟨u, hu⟩, hprod⟩ := h key have hv' : nrm π (c : A) * algebraMap L A s = (b₁ : A) * v := congrArg Subtype.val hv have hu' : nrm π (d : A) = (b₂ : A) * u := congrArg Subtype.val hu @@ -489,15 +489,15 @@ theorem isPrimal_fracSubring_of_isPrimal_residueSubring {b : A} (hb : π b ∈ S rw [show nrm π (c : A) * algebraMap L A s * (algebraMap L A s⁻¹ * algebraMap L A (scale π (c : A))) = nrm π (c : A) * algebraMap L A (scale π (c : A)) - * (algebraMap L A s * algebraMap L A s⁻¹) by ring, hs', mul_one] + * (algebraMap L A s * algebraMap L A s⁻¹) by ac_rfl, hs', mul_one] _ = (b₁ : A) * ((v : A) * algebraMap L A (s⁻¹ * scale π (c : A))) := by - rw [hv', map_mul]; ring + rw [hv', map_mul]; ac_rfl · refine ⟨⟨(u : A) * algebraMap L A (scale π (d : A)), ?_⟩, Subtype.ext ?_⟩ · rw [mem_residueSubring, map_mul, AlgHom.commutes] exact (fracSubring S).mul_mem (le_fracSubring u.2) (mem_scale_frac π d.2) · change (d : A) = (b₂ : A) * ((u : A) * algebraMap L A (scale π (d : A))) calc (d : A) = nrm π (d : A) * algebraMap L A (scale π (d : A)) := hd.symm - _ = (b₂ : A) * ((u : A) * algebraMap L A (scale π (d : A))) := by rw [hu']; ring + _ = (b₂ : A) * ((u : A) * algebraMap L A (scale π (d : A))) := by rw [hu']; ac_rfl · refine Subtype.ext ?_ change b = (b₁ : A) * (b₂ : A) simpa using congrArg Subtype.val hprod @@ -520,8 +520,8 @@ private theorem eta_rescale {b c d e : A} (hb : π b ∈ S) (hc : π c ∈ S) (h · obtain ⟨s₁, hs₁, hs₁0, hs₁b⟩ := exists_den hb₂F obtain ⟨s₂, hs₂, hs₂0, hs₂f⟩ := exists_den hfF refine ⟨s₁ * s₂, mul_ne_zero hs₁0 hs₂0, ?_, ?_, ?_⟩ - · rw [show s₁ * s₂ * π b₂ = s₂ * (s₁ * π b₂) by ring]; exact S.mul_mem hs₂ hs₁b - · rw [show s₁ * s₂ * π f = s₁ * (s₂ * π f) by ring]; exact S.mul_mem hs₁ hs₂f + · rw [show s₁ * s₂ * π b₂ = s₂ * (s₁ * π b₂) by ac_rfl]; exact S.mul_mem hs₂ hs₁b + · rw [show s₁ * s₂ * π f = s₁ * (s₂ * π f) by ac_rfl]; exact S.mul_mem hs₁ hs₂f · rw [hg0, zero_mul]; exact S.zero_mem · refine ⟨π g, hg0, ?_, ?_, ?_⟩ · rw [mul_comm, ← map_mul, ← hdg]; exact hd @@ -537,16 +537,16 @@ private theorem eta_rescale {b c d e : A} (hb : π b ∈ S) (hc : π c ∈ S) (h · rw [mem_residueSubring, map_mul, AlgHom.commutes, mul_comm]; exact hηf · change c = b₁ * algebraMap L A η⁻¹ * (f * algebraMap L A η) rw [hcf, show b₁ * algebraMap L A η⁻¹ * (f * algebraMap L A η) - = b₁ * f * (algebraMap L A η⁻¹ * algebraMap L A η) by ring, hinv, mul_one] + = b₁ * f * (algebraMap L A η⁻¹ * algebraMap L A η) by ac_rfl, hinv, mul_one] · refine ⟨⟨g * algebraMap L A η⁻¹, ?_⟩, Subtype.ext ?_⟩ · rw [mem_residueSubring, map_mul, AlgHom.commutes]; exact hηg · change d = b₂ * algebraMap L A η * (g * algebraMap L A η⁻¹) rw [hdg, show b₂ * algebraMap L A η * (g * algebraMap L A η⁻¹) - = b₂ * g * (algebraMap L A η * algebraMap L A η⁻¹) by ring, hinv', mul_one] + = b₂ * g * (algebraMap L A η * algebraMap L A η⁻¹) by ac_rfl, hinv', mul_one] · refine Subtype.ext ?_ change b = b₁ * algebraMap L A η⁻¹ * (b₂ * algebraMap L A η) rw [hprod, show b₁ * algebraMap L A η⁻¹ * (b₂ * algebraMap L A η) - = b₁ * b₂ * (algebraMap L A η⁻¹ * algebraMap L A η) by ring, hinv, mul_one] + = b₁ * b₂ * (algebraMap L A η⁻¹ * algebraMap L A η) by ac_rfl, hinv, mul_one] /-- Converse, case `π b = 0`. -/ theorem isPrimal_residueSubring_of_isPrimal_pre_fracSubring {b : A} (hb : π b ∈ S) (hb0 : π b = 0) @@ -565,16 +565,16 @@ theorem isPrimal_residueSubring_of_isPrimal_pre_fracSubring {b : A} (hb : π b have hcf : (c : A) = (b₁ : A) * f := congrArg Subtype.val hf have hdg : (d : A) = (b₂ : A) * g := congrArg Subtype.val hg have hefg : (e : A) = (f : A) * g := by - have h6 : b * (e : A) = b * ((f : A) * g) := by rw [← hcd, hcf, hdg, hprod']; ring + have h6 : b * (e : A) = b * ((f : A) * g) := by rw [← hcd, hcf, hdg, hprod']; ac_rfl exact mul_left_cancel₀ hbne h6 have hzero : π (b₁ : A) = 0 ∨ π (b₂ : A) = 0 := mul_eq_zero.mp (by rw [← map_mul, ← hprod']; exact hb0) rcases hzero with h1 | h2 · exact eta_rescale hb c.2 d.2 e.2 b₂.2 f.2 hprod' hcf hdg hefg h1 · obtain ⟨B₁, B₂, hd1, hd2, hp⟩ := - eta_rescale hb d.2 c.2 e.2 b₁.2 g.2 (by rw [hprod']; ring) hdg hcf - (by rw [hefg]; ring) h2 - exact ⟨B₂, B₁, hd2, hd1, by rw [hp]; ring⟩ + eta_rescale hb d.2 c.2 e.2 b₁.2 g.2 (by rw [hprod']; ac_rfl) hdg hcf + (by rw [hefg]; ac_rfl) h2 + exact ⟨B₂, B₁, hd2, hd1, by rw [hp]; ac_rfl⟩ /-! ### Lemma 9.2.1 -/ @@ -651,7 +651,7 @@ theorem exists_refinement_residueSubring_of_ambient_of_residue_ne_zero dsimp only [η] have hae : π (a : A) = π e * π f := by rw [ha, map_mul] calc - π f * (π e * (e₀ : L)⁻¹) = (π e * π f) * (e₀ : L)⁻¹ := by ring + π f * (π e * (e₀ : L)⁻¹) = (π e * π f) * (e₀ : L)⁻¹ := by ac_rfl _ = π (a : A) * (e₀ : L)⁻¹ := by rw [hae] _ = (e₀ : L) * f₀ * (e₀ : L)⁻¹ := by rw [ha₀'] _ = f₀ := by field_simp @@ -659,7 +659,7 @@ theorem exists_refinement_residueSubring_of_ambient_of_residue_ne_zero simp only [map_mul, AlgHom.commutes, Algebra.algebraMap_self, RingHom.id_apply] dsimp only [η] have hce : π (c : A) = π e * π g := by rw [hc, map_mul] - rw [show π g * (π e * (e₀ : L)⁻¹) = (π e * π g) * (e₀ : L)⁻¹ by ring, + rw [show π g * (π e * (e₀ : L)⁻¹) = (π e * π g) * (e₀ : L)⁻¹ by ac_rfl, ← hce, hc₀'] field_simp have hH : π (h * algebraMap L A η⁻¹) = h₀ := by @@ -682,19 +682,19 @@ theorem exists_refinement_residueSubring_of_ambient_of_residue_ne_zero simp only [Subring.coe_mul] · rw [ha] rw [show (e * algebraMap L A η⁻¹) * (f * algebraMap L A η) = - e * f * (algebraMap L A η⁻¹ * algebraMap L A η) by ring, + e * f * (algebraMap L A η⁻¹ * algebraMap L A η) by ac_rfl, ← map_mul, inv_mul_cancel₀ hη0, map_one, mul_one] · rw [hb] rw [show (g * algebraMap L A η) * (h * algebraMap L A η⁻¹) = - g * h * (algebraMap L A η * algebraMap L A η⁻¹) by ring, + g * h * (algebraMap L A η * algebraMap L A η⁻¹) by ac_rfl, ← map_mul, mul_inv_cancel₀ hη0, map_one, mul_one] · rw [hc] rw [show (e * algebraMap L A η⁻¹) * (g * algebraMap L A η) = - e * g * (algebraMap L A η⁻¹ * algebraMap L A η) by ring, + e * g * (algebraMap L A η⁻¹ * algebraMap L A η) by ac_rfl, ← map_mul, inv_mul_cancel₀ hη0, map_one, mul_one] · rw [hd] rw [show (f * algebraMap L A η) * (h * algebraMap L A η⁻¹) = - f * h * (algebraMap L A η * algebraMap L A η⁻¹) by ring, + f * h * (algebraMap L A η * algebraMap L A η⁻¹) by ac_rfl, ← map_mul, mul_inv_cancel₀ hη0, map_one, mul_one] /-- A nonzero exact ambient four-factor refinement can be rescaled into the residue subring when @@ -733,11 +733,11 @@ theorem exists_refinement_residueSubring_of_ambient have haEF' := congrArg Subtype.val haEF simp only [Subring.coe_mul] at habcd' hcEG' hdFH' haEF' rw [habcd', hcEG', hdFH', haEF'] - ring + ac_rfl · obtain ⟨F, E, hFd, hEc, haFE⟩ := eta_rescale a.2 d.2 c.2 b.2 (by rw [hfrac]; exact Subring.mem_top _) (by rw [hfrac]; exact Subring.mem_top _) - (by rw [ha]; ring) hd hc (by rw [hb]; ring) hf0 + (by rw [ha]; ac_rfl) hd hc (by rw [hb]; ac_rfl) hf0 obtain ⟨H, hdFH⟩ := hFd obtain ⟨G, hcEG⟩ := hEc refine ⟨E, F, G, H, ?_, ?_, hcEG, hdFH⟩ @@ -751,7 +751,7 @@ theorem exists_refinement_residueSubring_of_ambient have haFE' := congrArg Subtype.val haFE simp only [Subring.coe_mul] at habcd' hcEG' hdFH' haFE' rw [habcd', hcEG', hdFH', haFE'] - ring + ac_rfl · exact exists_refinement_residueSubring_of_ambient_of_residue_ne_zero haS haπ habcd ha hb hc hd diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Divisibility/Tests/Refinement.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Divisibility/Tests/Refinement.lean index 0288326e7d..919a0c945f 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Divisibility/Tests/Refinement.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Divisibility/Tests/Refinement.lean @@ -8,7 +8,11 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Divisibility.Refinement import Mathlib.Algebra.GCDMonoid.Nat -import Mathlib.Tactic.NormNum +import Mathlib.Data.Rat.Cast.Order +import Mathlib.Tactic.NormNum.Abs +import Mathlib.Tactic.NormNum.DivMod +import Mathlib.Tactic.NormNum.OfScientific +import Mathlib.Tactic.NormNum.Pow /-! # Tests for four-factor refinement diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/GeometricIntegrality.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/GeometricIntegrality.lean index b60e7395b6..5478fb6498 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/GeometricIntegrality.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/GeometricIntegrality.lean @@ -14,9 +14,6 @@ import Mathlib.LinearAlgebra.Basis.VectorSpace import Mathlib.Algebra.Field.ULift import Mathlib.Algebra.Ring.Hom.InjSurj import Mathlib.RingTheory.Flat.Basic -import Mathlib.RingTheory.Ideal.Quotient.Basic -import Mathlib.RingTheory.Ideal.Quotient.Operations -import Mathlib.RingTheory.Localization.FractionRing import Mathlib.RingTheory.Polynomial.UniqueFactorization import Mathlib.RingTheory.TensorProduct.MvPolynomial import Mathlib.RingTheory.TensorProduct.Quotient diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/BaseChange.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/BaseChange.lean index d0572894f2..f3d7c3196e 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/BaseChange.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/BaseChange.lean @@ -10,7 +10,6 @@ public import Mathlib.RingTheory.GradedAlgebra.TensorProduct public import Mathlib.RingTheory.TensorProduct.Quotient import Mathlib.RingTheory.Flat.Basic -import Mathlib.Algebra.Module.Torsion.Field import Mathlib.LinearAlgebra.Basis.VectorSpace import Mathlib.Algebra.CharP.Algebra diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/Correction.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/Correction.lean index e1a0471508..94419d1bbb 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/Correction.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/Correction.lean @@ -8,7 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.LoweringDerivation.Mu import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.GradedRing.HomogeneousZeroDivisors -import Mathlib.Algebra.Module.Torsion.Field import Mathlib.LinearAlgebra.Basis.VectorSpace import Mathlib.RingTheory.Flat.Basic import Mathlib.Tactic.LinearCombination @@ -256,7 +255,7 @@ theorem exists_rep_coordinate_identity (h0 : GradeZeroScalars 𝒜) {j : ℕ} { rw [← RingHom.map_mul, ← RingHom.map_mul, ← RingHom.map_add] congr 1 simp only [nsmul_eq_mul] - ring + ac_rfl /-- The Leibniz rule as an identity between tensors, `(∂ ⊗ 1) ν_{j+1}(x^(r+1) y) = (1 ⊗ m)(ν_j(∂x), ν_j(∂y))`: `∂ ⊗ 1` applied to a tensor `T` with diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/FilteredModule.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/FilteredModule.lean index 43ca54becd..0b811804b4 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/FilteredModule.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/FilteredModule.lean @@ -11,7 +11,6 @@ public import Mathlib.LinearAlgebra.TensorProduct.Tower import Mathlib.LinearAlgebra.TensorProduct.Finiteness import Mathlib.RingTheory.TensorProduct.Free -import Mathlib.Algebra.BigOperators.Group.Finset.Preimage /-! # Freeness over the finite-degree part diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/Grading.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/Grading.lean index 43abcdd1b2..a06b2b1385 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/Grading.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/Grading.lean @@ -10,7 +10,7 @@ public import Mathlib.RingTheory.GradedAlgebra.Basic public import Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal public import Mathlib.RingTheory.Ideal.Quotient.Operations -import Mathlib.LinearAlgebra.DFinsupp + /-! # Graded algebras over countable ordinals: the ideals `I_{≥j}` and the quotient `A/I` diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/IdealGEGraded.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/IdealGEGraded.lean index f1daed64ac..9964d188d3 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/IdealGEGraded.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/IdealGEGraded.lean @@ -9,7 +9,8 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.LoweringDerivat public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.FiltrationDegree public import Mathlib.RingTheory.TensorProduct.Basic -import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.BasisOver +import Mathlib.RingTheory.TensorProduct.Maps +import Mathlib.Tactic.ContinuousFunctionalCalculus /-! # The associated graded ring `gr_{I_•} A` diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/Mu.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/Mu.lean index f85ff1be6c..c921a0e77a 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/Mu.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/LoweringDerivation/Mu.lean @@ -8,7 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.LoweringDerivation.Grading public import LeanPool.ConwayRefinement.ConwayRefinement.Order.Filter.FunAtZeroMinus -import Mathlib.LinearAlgebra.TensorProduct.RightExactness import Mathlib.LinearAlgebra.TensorProduct.Finiteness /-! @@ -269,7 +268,7 @@ theorem mu_lTensor_mulLeft (j : ℕ) (B : R) (T : 𝒜 (j : NatOrdinal) ⊗[E] F change Ideal.Quotient.mk _ ((a : R) * (B * b)) = Ideal.Quotient.mk _ ((a : R) * b) * _ rw [← map_mul] congr 1 - ring + ac_rfl | add x y hx hy => rw [map_add, map_add, hx, hy, map_add, add_mul] /-- `μ_j` is onto `I_{≥j}/I_{≥j+1}`: the class of an element of `I_{≥j}` modulo `I_{≥j+1}` is in diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/MonoidAlgebra/LatticeFunctional.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/MonoidAlgebra/LatticeFunctional.lean index c2e1c75e2a..4411995b95 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/MonoidAlgebra/LatticeFunctional.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/MonoidAlgebra/LatticeFunctional.lean @@ -9,8 +9,12 @@ public import Mathlib.Algebra.BigOperators.Fin public import Mathlib.Algebra.Order.Ring.Abs public import Mathlib.Data.Finsupp.Basic -import Mathlib.Tactic.Ring -import Mathlib.Tactic.Linarith +import Mathlib.Data.Rat.Cast.Order +import Mathlib.Tactic.Linarith.Frontend +import Mathlib.Tactic.NormNum.Abs +import Mathlib.Tactic.NormNum.DivMod +import Mathlib.Tactic.NormNum.OfScientific +import Mathlib.Tactic.Ring.RingNF /-! # A linear functional separating finitely many lattice points @@ -41,7 +45,7 @@ private theorem eq_zero_of_sum_mul_pow_eq_zero {k : ℕ} {N : ℤ} (hN : 0 < N) rw [Finset.mul_sum] refine Finset.sum_congr rfl fun i _ ↦ ?_ rw [pow_succ] - ring + ac_rfl simp only [Fin.val_zero, pow_zero, mul_one, Fin.val_succ] at hsum rw [hshift] at hsum have hd0 : d 0 = 0 := by diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/MvPolynomial/BaseChange.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/MvPolynomial/BaseChange.lean index 90bcb26fc9..be9d0dae3f 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/MvPolynomial/BaseChange.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/MvPolynomial/BaseChange.lean @@ -8,7 +8,7 @@ module public import Mathlib.RingTheory.TensorProduct.MvPolynomial public import Mathlib.RingTheory.Flat.Basic -import Mathlib.RingTheory.MvPolynomial.Tower + /-! # Algebraic independence under a flat extension of scalars diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/MvPolynomial/GCDMonoid.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/MvPolynomial/GCDMonoid.lean index 612e5c719e..98fbae49f6 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/MvPolynomial/GCDMonoid.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/MvPolynomial/GCDMonoid.lean @@ -10,7 +10,6 @@ public import Mathlib.Algebra.MvPolynomial.CommRing import LeanPool.ConwayRefinement.ConwayRefinement.Blueprint import Mathlib.Algebra.MvPolynomial.NoZeroDivisors -import Mathlib.RingTheory.Polynomial.Basic import Mathlib.RingTheory.Polynomial.Content /-! diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/MvPolynomial/OrdinalDerivation.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/MvPolynomial/OrdinalDerivation.lean index 1b9a4eae26..9f01ba6133 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/MvPolynomial/OrdinalDerivation.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/MvPolynomial/OrdinalDerivation.lean @@ -142,7 +142,7 @@ theorem pderiv_pderiv_comm (i j : σ) (p : MvPolynomial σ R) : | mul_X p k ih => rw [pderiv_mul, pderiv_mul, map_add, map_add, pderiv_mul, pderiv_mul, pderiv_mul, pderiv_mul, ih, hX, hX] - ring + ac_rfl /-- The variables of a partial derivative are among those of the polynomial. -/ theorem vars_pderiv_subset (i : σ) (p : MvPolynomial σ R) : (pderiv i p).vars ⊆ p.vars := by diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/MvPolynomial/RemainderBound.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/MvPolynomial/RemainderBound.lean index b09a62f335..ea5cf20eb4 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/MvPolynomial/RemainderBound.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/MvPolynomial/RemainderBound.lean @@ -9,7 +9,6 @@ module import LeanPool.ConwayRefinement.ConwayRefinement.Blueprint public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.TermDegree public import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.PairBounds -import Mathlib.Tactic.Abel /-! # A uniform degree bound for terms with two translated truncations diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Tests/GeometricIntegrality.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Tests/GeometricIntegrality.lean index cc4df20bf4..b8be8432e4 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Tests/GeometricIntegrality.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Tests/GeometricIntegrality.lean @@ -8,7 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.GeometricIntegrality import Mathlib.Algebra.MvPolynomial.Division -import Mathlib.RingTheory.TensorProduct.Maps import Mathlib.RingTheory.TensorProduct.MvPolynomial /-! diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/DegreeSum.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/DegreeSum.lean index 0888372117..be7a5c03fd 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/DegreeSum.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/DegreeSum.lean @@ -8,7 +8,7 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeInitialForm public import Mathlib.Algebra.Group.Subgroup.Finite -import Mathlib.Tactic.Ring +import Mathlib.Tactic.Ring.RingNF /-! # Degrees and homogeneous classes of finite sums diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/DegreeWeightedPolynomial.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/DegreeWeightedPolynomial.lean index 10f3287dfc..9bb78f6eb0 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/DegreeWeightedPolynomial.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/DegreeWeightedPolynomial.lean @@ -9,8 +9,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.Degre public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.WeightedTotalDegree public import Mathlib.Algebra.MvPolynomial.Eval -import Mathlib.Algebra.BigOperators.Ring.Finset -import Mathlib.Algebra.BigOperators.Finsupp.Basic + /-! # The degree of a polynomial in elements with independent initial forms diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/QuotientDegree.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/QuotientDegree.lean index a31b6cf899..70052e5c65 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/QuotientDegree.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/QuotientDegree.lean @@ -8,7 +8,7 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.MaxAddDegree public import Mathlib.RingTheory.Ideal.Quotient.Defs -import Mathlib.Order.Minimal + /-! # Least-representative degree on a quotient ring diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/AssociatedGraded.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/AssociatedGraded.lean index efa58de63e..e4e0c4253a 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/AssociatedGraded.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/AssociatedGraded.lean @@ -9,7 +9,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.Degre public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.OfValuation public import Mathlib.Algebra.Order.Ring.Rat -import Mathlib.Algebra.Ring.Prod + /-! # API checks for max-additive degrees and associated graded rings diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/AssociatedGradedValuation.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/AssociatedGradedValuation.lean index fabbf0d7cf..ba9bfec297 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/AssociatedGradedValuation.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/AssociatedGradedValuation.lean @@ -9,7 +9,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.Assoc public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.OfValuation public import Mathlib.Algebra.Order.Ring.Rat -import Mathlib.Algebra.Ring.Prod + /-! # API checks for leading-grade valuations diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/DegreeAssociatedGraded.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/DegreeAssociatedGraded.lean index 1321e7f9e6..f4c0f9ae3c 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/DegreeAssociatedGraded.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/DegreeAssociatedGraded.lean @@ -8,7 +8,11 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeAssociatedGradedDomain public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.Tests.Fixtures.PolynomialAssociatedGraded -import Mathlib.Algebra.Polynomial.Degree.Operations +import Mathlib.Data.Rat.Cast.Order +import Mathlib.Tactic.NormNum.Abs +import Mathlib.Tactic.NormNum.DivMod +import Mathlib.Tactic.NormNum.OfScientific +import Mathlib.Tactic.NormNum.Pow /-! # API checks for the associated graded ring of a degree function diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/DegreeAssociatedGradedQuotient.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/DegreeAssociatedGradedQuotient.lean index 7a92667f73..20de4eb556 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/DegreeAssociatedGradedQuotient.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/DegreeAssociatedGradedQuotient.lean @@ -10,7 +10,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.Tests public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.Tests.Fixtures.PolynomialQuotientDegree import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreePrincipalInitialIdeal -import Mathlib.Algebra.Polynomial.Degree.Operations +import Mathlib.Algebra.CharP.Defs /-! # API checks for the associated graded ring of a quotient diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/RV.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/RV.lean index ee0d3018af..51d0951266 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/RV.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/RV.lean @@ -9,7 +9,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.RV public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.OfValuation public import Mathlib.Algebra.Order.Ring.Rat -import Mathlib.Algebra.Ring.Prod + /-! # API checks for RV classes, initial forms, and the residue ring diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/Residue.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/Residue.lean index 7281ad5031..8a803531fa 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/Residue.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Algebra/Valuation/Tests/Residue.lean @@ -3,7 +3,7 @@ Copyright (c) 2026 Dan Abramov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Dan Abramov -/ -module +module -- shake: keep-all public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.ResidueMathlib public import Mathlib.Algebra.Order.Ring.Rat diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Data/Multiset/SelectionComplexity.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Data/Multiset/SelectionComplexity.lean index a03bb5f5ac..0974937b67 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Data/Multiset/SelectionComplexity.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Data/Multiset/SelectionComplexity.lean @@ -9,7 +9,6 @@ public import Mathlib.SetTheory.Cardinal.Order public import Mathlib.SetTheory.Ordinal.Basic public import Mathlib.Data.Multiset.DershowitzManna import Mathlib.Data.Finset.Max -import Lean.Elab.Tactic.Omega /-! # Selection and decreasing multiset complexity diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Data/Multiset/Tests/SelectionComplexity.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Data/Multiset/Tests/SelectionComplexity.lean index 602e0e4eab..e6ff2c2e51 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Data/Multiset/Tests/SelectionComplexity.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Data/Multiset/Tests/SelectionComplexity.lean @@ -5,7 +5,6 @@ Authors: Dan Abramov -/ module public import LeanPool.ConwayRefinement.ConwayRefinement.Data.Multiset.SelectionComplexity -import Mathlib.Tactic.Tauto /-! # Distinct-factor complexity checks diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Examples/OmnificInteger/DegreeTwoPrime.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Examples/OmnificInteger/DegreeTwoPrime.lean index de46f7c5bc..12164b1b78 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Examples/OmnificInteger/DegreeTwoPrime.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Examples/OmnificInteger/DegreeTwoPrime.lean @@ -12,11 +12,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Examples.OmnificInteger public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.DegreeTwo.DegreeTwoExample import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.CharZero -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.NonpositiveCoefficientMap -import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.Degree -import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ArchimedeanAssumptions -import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.DegreeTransfer -import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.IntegerPart import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.RealLeadingSplit /-! diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Examples/OmnificInteger/OneRowPrime.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Examples/OmnificInteger/OneRowPrime.lean index a363c40a9f..834b1a69ca 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Examples/OmnificInteger/OneRowPrime.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Examples/OmnificInteger/OneRowPrime.lean @@ -9,11 +9,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger. public import LeanPool.ConwayRefinement.ConwayRefinement.Examples.OmnificInteger.OneRowNormalForm import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.CharZero -import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.Degree import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OneRow -import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ArchimedeanAssumptions -import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.DegreeTransfer -import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.IntegerPart import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.RealLeadingSplit /-! diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/FieldTheory/MonicFactorCoefficients.lean b/LeanPool/ConwayRefinement/ConwayRefinement/FieldTheory/MonicFactorCoefficients.lean index c52212acda..db0cea5874 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/FieldTheory/MonicFactorCoefficients.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/FieldTheory/MonicFactorCoefficients.lean @@ -76,7 +76,7 @@ theorem exists_scalar_of_mul_eq_map rw [show algebraMap K L P.leadingCoeff⁻¹ = (q.leadingCoeff * r.leadingCoeff)⁻¹ by rw [← hlc, hPlc, map_inv₀]] rw [mul_inv, Polynomial.C_mul] - ring + ac_rfl refine ⟨q.leadingCoeff⁻¹, inv_ne_zero hc, fun j ↦ ?_⟩ have := coeff_mem_range_of_mul_eq_map hclosed hq1 hr1 hprod j rwa [Polynomial.coeff_C_mul] at this diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Degree/Statements/DegreeResidue.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Degree/Statements/DegreeResidue.lean index a07fb68f2d..75b01b0d91 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Degree/Statements/DegreeResidue.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Degree/Statements/DegreeResidue.lean @@ -10,7 +10,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSuppor public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrderType public import Mathlib.Basic.Real.Basic -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.DegreeValuation import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportResidue import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrderTypeMultiplicativity diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/AlmostIrreducible.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/AlmostIrreducible.lean index fc6fa22437..2b8844a2d2 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/AlmostIrreducible.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/AlmostIrreducible.lean @@ -10,7 +10,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.RealSupportS public import Mathlib.Algebra.Group.Irreducible.Defs public import Mathlib.GroupTheory.Divisible -import Mathlib.Algebra.GroupWithZero.Divisibility + /-! # Almost-irreducible Hahn series diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/DegreeTwo/DegreeTwo.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/DegreeTwo/DegreeTwo.lean index ce4dd821c6..ecfb42fa47 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/DegreeTwo/DegreeTwo.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/DegreeTwo/DegreeTwo.lean @@ -5,11 +5,11 @@ Authors: Dan Abramov -/ module + public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.DegreeTwo.Factorization import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueFinalSegment -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.GermDegree -import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.SetOrderType +import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueDegree /-! # Support and ordinal value in PS06 degree two diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/DegreeTwo/DegreeTwoExample.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/DegreeTwo/DegreeTwoExample.lean index efd1450143..d5263b8f7c 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/DegreeTwo/DegreeTwoExample.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/DegreeTwo/DegreeTwoExample.lean @@ -10,9 +10,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorizatio public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.NonpositiveCoefficientMap import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.TruncationIntegerPartPrimal import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Domain -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrderType -import Mathlib.Order.Prod.Lex.Basic -import Mathlib.SetTheory.Ordinal.Arithmetic /-! # An explicit PS06 degree-two irreducible diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/DegreeTwo/Factorization.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/DegreeTwo/Factorization.lean index 1f2da741c2..ae3a03fa59 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/DegreeTwo/Factorization.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/DegreeTwo/Factorization.lean @@ -5,9 +5,9 @@ Authors: Dan Abramov -/ module + public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.CriticalPointExistence -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueDegree import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.ProductValue /-! diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/DegreeTwo/FactorizationClassification.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/DegreeTwo/FactorizationClassification.lean index 8b130370e8..fb88a5495e 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/DegreeTwo/FactorizationClassification.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/DegreeTwo/FactorizationClassification.lean @@ -7,13 +7,11 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.DegreeTwo.DegreeTwo -import Mathlib.Topology.Compactness.Compact -import Mathlib.Topology.Instances.Real.Lemmas -import Mathlib.Topology.Order.OrderClosed import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueFinalSegment import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueImage -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueConstantMul import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.ProductValue +import Mathlib.Data.EReal.Operations +import Mathlib.Topology.MetricSpace.Bounded /-! # The degree-two factorisation classification diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/DegreeTwo/TranslatedSpanFactorization.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/DegreeTwo/TranslatedSpanFactorization.lean index 51409ee60f..ddad18d1dd 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/DegreeTwo/TranslatedSpanFactorization.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/DegreeTwo/TranslatedSpanFactorization.lean @@ -11,12 +11,10 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorizatio public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.DegreeTwo.TranslatedTruncationSpan public import Mathlib.LinearAlgebra.Dimension.Finrank -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Convolution import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Monomial -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.ProductValue import Mathlib.LinearAlgebra.Dimension.Constructions -import Mathlib.Topology.Instances.Real.Lemmas -import Mathlib.Topology.Order.OrderClosed +import Mathlib.Data.EReal.Operations +import Mathlib.Topology.MetricSpace.Bounded /-! # Translated-truncation spans of degree-two factorisations diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/FiniteSupportFactorUniqueness.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/FiniteSupportFactorUniqueness.lean index 3319138246..ac5699f57a 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/FiniteSupportFactorUniqueness.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/FiniteSupportFactorUniqueness.lean @@ -7,7 +7,7 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.InfiniteSupport -import Mathlib.Algebra.GroupWithZero.Associated + /-! # Uniqueness of the finite-support factor diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/GermLike.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/GermLike.lean index 7d517a20d6..5b1f1d2d90 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/GermLike.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/GermLike.lean @@ -5,12 +5,12 @@ Authors: Dan Abramov -/ module + public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.CriticalPointExistence import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.ProductValue import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.DegreeTwo.FactorizationClassification import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueFinalSegment -import Mathlib.Tactic.Linarith /-! # Factorisation of germ-like series diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/InfiniteSupport.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/InfiniteSupport.lean index 13dc96a195..32963175fc 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/InfiniteSupport.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/InfiniteSupport.lean @@ -194,7 +194,7 @@ theorem HasOnlyUnitFiniteSupportDivisors.exists_factorization refine ⟨kc * kd, cs ++ ds, mul_ne_zero hkc hkd, ?_, ?_, ?_⟩ · rw [hfactor, hcFactor, hdFactor, List.prod_append, map_mul, mul_assoc] - ring + ac_rfl · intro q hq rw [List.mem_append] at hq exact hq.elim (hcs q) (hds q) @@ -278,7 +278,7 @@ theorem exists_series_infinite_support_factorization_of_exists_gcd refine ⟨k, factors, hk, ?_, hfactors, ?_⟩ · change b = HahnSeries.Nonpositive.C k * (p : Series K) * factors.prod rw [hq, hqFactor] - ring + ac_rfl · apply hbound.trans_eq apply HahnSeries.degreeCantorTermCount_congr rw [hq, HahnSeries.Nonpositive.degree_mul] diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/MaximalFiniteMultiplicativity.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/MaximalFiniteMultiplicativity.lean index d9ce694253..fcc9add03c 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/MaximalFiniteMultiplicativity.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/MaximalFiniteMultiplicativity.lean @@ -7,7 +7,7 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.NormalizedMaximalFinite -import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.AssociatedGradedDivisibility +import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeAssociatedGradedDomain /-! # Multiplicativity of normalized maximal finite-support divisors diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/NormalizedHPart.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/NormalizedHPart.lean index d3f73fb7ab..dd67fd464a 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/NormalizedHPart.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/NormalizedHPart.lean @@ -8,7 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportConstantTermOne public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.RealSupportSupremum -import Mathlib.Algebra.GroupWithZero.Divisibility import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Monomial /-! diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/PrincipalMaximalFinite.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/PrincipalMaximalFinite.lean index 77e79a077d..57bcfd2400 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/PrincipalMaximalFinite.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/PrincipalMaximalFinite.lean @@ -8,8 +8,8 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.NormalizedMaximalFinite public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.RVMaximalFinite -import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.AssociatedGradedDivisibility import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.GradedDivisibility +import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeAssociatedGradedDomain /-! # Maximal finite-support divisors and principal factors diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/GradedIrreducible.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/GradedIrreducible.lean index 3fc64b7f1c..4812a304bf 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/GradedIrreducible.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/GradedIrreducible.lean @@ -15,11 +15,9 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorizatio import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random.PrincipalIrreducible import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Degree.SupportSupremumMultiplicativity -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalComponentDegree import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.AssociatedGradedDivisibility import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeSum import Mathlib.LinearAlgebra.Basis.VectorSpace -import Mathlib.RingTheory.TensorProduct.Basic /-! # Block forms in the degree-graded ring @@ -430,7 +428,7 @@ theorem exists_isMonomial_factor_of_mul_eq [CharZero K] {n : NatOrdinal} have hBeq : B = A' * C' := by apply mul_left_cancel₀ hγne rw [← hAC, hA', hC', ← hp₁, ← hp₂, hsplit, map_mul] - ring + ac_rfl rcases hBirr.isUnit_or_isUnit hBeq with hA'u | hC'u · obtain ⟨k, hk, hk'⟩ := exists_algebraMap_eq_of_isUnit hA'u refine ⟨p₁ * algebraMap K _ k, ?_, Or.inl ?_⟩ diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/HereditaryIndependence.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/HereditaryIndependence.lean index 1342c00654..72fe8d0b22 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/HereditaryIndependence.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/HereditaryIndependence.lean @@ -9,7 +9,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Truncation public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeInitialForm -import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeSum + /-! # Hereditary `rv_J`-independence at finite ordinal-value degrees diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/IndependenceWindow.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/IndependenceWindow.lean index 7add9d5043..c587dada4a 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/IndependenceWindow.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/IndependenceWindow.lean @@ -9,8 +9,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorizatio public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.StableInterval import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.NonpositiveCoefficientMap -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueImage -import Mathlib.Tactic.Linarith /-! # The support of a vanishing relation among classes diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/MainTheorem.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/MainTheorem.lean index 50d8652979..299c80c816 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/MainTheorem.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/MainTheorem.lean @@ -8,7 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random.RandomBlocks import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.PrincipalAddition -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalComponentDegree /-! # Irreducibility of random series of finite degree diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/NonPrincipalIrreducible.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/NonPrincipalIrreducible.lean index 3e85c4b6a3..da6deb4fec 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/NonPrincipalIrreducible.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/NonPrincipalIrreducible.lean @@ -9,11 +9,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorizatio public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random.GradedIrreducible public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.NormalForm -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalComponentDegree -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalComponentTensor -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Degree.Statements.Degree import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeSum -import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeInitialForm /-! # Irreducibility of non-principal series of finite degree @@ -190,7 +186,7 @@ theorem irreducible_blockSum {n : ℕ} (hn : 1 ≤ n) {ι : Type} [Fintype ι] ⟨(γm : ℝ) + ((δ i : exponentMonoid ℝ) : ℝ), (exponentMonoid ℝ).add_mem γm.2 (δ i).2⟩ from Subtype.ext (by change γ i = γ m + (γ i - γ m); ring), ← finiteSupportMonomial_mul, map_mul] - ring + ac_rfl -- The block form and the monomial are nonzero, so `B` has degree exactly `n`. have hBform_ne : Bform ≠ 0 := by intro h diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/NormalFormBlocks.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/NormalFormBlocks.lean index a0d8a7c0e5..613a921520 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/NormalFormBlocks.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/NormalFormBlocks.lean @@ -8,10 +8,7 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random.NonPrincipalIrreducible public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.NormalForm -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.SeparatedSupport -import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.AdditivelyPrincipal -import Mathlib.SetTheory.Ordinal.Principal -import Mathlib.Topology.Order.Monotone + /-! # The block decomposition of a series of order type `ω^n · m + β` diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/RandomBlocks.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/RandomBlocks.lean index 944cb74e14..d5c33c7eba 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/RandomBlocks.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/RandomBlocks.lean @@ -11,9 +11,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorizatio public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random.SupportRandom public import LeanPool.ConwayRefinement.ConwayRefinement.LinearAlgebra.IndicatorFinsupp -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalComponentDegree -import Mathlib.Topology.Algebra.Group.Basic -import Mathlib.Topology.Order.Monotone /-! # Randomness of a series passes to its blocks @@ -236,7 +233,7 @@ theorem isMutuallySupportRandom_block (hb : IsSupportRandom b) : apply hinjL rw [map_add, map_add, L.linearCombination_indicatorFinsupp_of_mem ℚ hxL, L.linearCombination_indicatorFinsupp_of_mem ℚ hx'L, hγcomb, hγcomb] - ring + ac_rfl have hpos : 0 < (L.indicatorFinsupp ℚ (d.exponent i + z) + L.indicatorFinsupp ℚ (d.exponent j)) ⟨_, hxL⟩ := by rw [Finsupp.add_apply, L.indicatorFinsupp_apply_self hxL] diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/ReducibleSpan.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/ReducibleSpan.lean index 1e3e7f6aa5..d394f8962a 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/ReducibleSpan.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/ReducibleSpan.lean @@ -8,10 +8,7 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random.HereditaryIndependence public import Mathlib.LinearAlgebra.Quotient.Basic -import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeSum import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueImage -import Mathlib.LinearAlgebra.Finsupp.LinearCombination -import Mathlib.LinearAlgebra.LinearIndependent.Basic /-! # The space of reducible classes and the property `(*)_α` diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/SuccessorStep.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/SuccessorStep.lean index e35fe76d16..774e05d6e9 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/SuccessorStep.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/SuccessorStep.lean @@ -11,9 +11,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue public import LeanPool.ConwayRefinement.ConwayRefinement.LinearAlgebra.FiniteSpanRelation import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.ResidualPointCofinality -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueImage -import Mathlib.Order.ConditionallyCompleteLattice.Finset -import Mathlib.Topology.Instances.Real.Lemmas /-! # The successor step `(*)_α ⇒ (*)_{α+1}` and `(*)_n` for finite `n` diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/SupportRandom.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/SupportRandom.lean index 6ddfe75851..d6a080045e 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/SupportRandom.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/SupportRandom.lean @@ -132,7 +132,7 @@ theorem IsMutuallySupportRandom.truncationsIndependent {ι : Type} {b : ι → S apply hinjL rw [map_add, map_add, L.linearCombination_indicatorFinsupp_of_mem ℚ hβL, L.linearCombination_indicatorFinsupp_of_mem ℚ hβ'L, hcomb k₁, hcomb k₀, hβ, hβ'] - ring + ac_rfl -- Evaluate at `β`: the right side must be nonzero there. have hpos : 0 < (L.indicatorFinsupp ℚ β + L.indicatorFinsupp ℚ (γ k₁)) ⟨β, hβL⟩ := by rw [Finsupp.add_apply, L.indicatorFinsupp_apply_self hβL] diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/TruncationIndependence.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/TruncationIndependence.lean index 1dcdddb0ad..10cff2de15 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/TruncationIndependence.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Random/TruncationIndependence.lean @@ -7,8 +7,7 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Random.HereditaryIndependence -import Mathlib.Data.Finset.Lattice.Fold -import Mathlib.Data.Finset.Max + /-! # Hereditary `rv_J`-independence from the independence of truncations diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/SeriesMaximalMultiplicativity.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/SeriesMaximalMultiplicativity.lean index 5f698c27b2..47a9853234 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/SeriesMaximalMultiplicativity.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/SeriesMaximalMultiplicativity.lean @@ -8,8 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.NormalizedSeriesMaximalFinite import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.RVGradedMaximalFinite -import Mathlib.Algebra.GCDMonoid.Basic -import Mathlib.Order.RelClasses /-! # Multiplicativity of maximal finite-support divisors of Hahn series @@ -384,7 +382,7 @@ theorem seriesNormalizedMaximalFiniteSupportDivisor_mul_of_graded ((pB * pC : FiniteSupportRing (K := K)) : Series K) * (b₀ * c₀) := by rw [hbFactor, hcFactor] simp only [Subring.coe_mul] - ring + ac_rfl have hrDiv : (r : Series K) ∣ b₀ * c₀ := by have hdiv : ((pB * pC * r : FiniteSupportRing (K := K)) : Series K) ∣ b * c := by diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/SeriesPrimality.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/SeriesPrimality.lean index 0713b96b0d..312485855a 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/SeriesPrimality.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/SeriesPrimality.lean @@ -7,7 +7,7 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.NormalizedSeriesMaximalFinite -import Mathlib.Algebra.GCDMonoid.Basic + /-! # Primality of finite-support elements in the Hahn-series ring diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/Factorization.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/Factorization.lean index fae37c9b55..dfcaa1d706 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/Factorization.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/Factorization.lean @@ -9,10 +9,8 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorizatio public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.DegreeTermCount import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.InfiniteSupport -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.ProductValue import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportUnit import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportGCDProof -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Degree.Statements.Degree /-! # LM24 factorisation statement diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/FiniteSupportFactorUniqueness.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/FiniteSupportFactorUniqueness.lean index b3dcc145ec..638dcb85f3 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/FiniteSupportFactorUniqueness.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/FiniteSupportFactorUniqueness.lean @@ -7,10 +7,8 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.FiniteSupportFactorUniqueness -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.ProductValue import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportUnit import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportGCDProof -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Degree.Statements.Degree import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Statements.MaximalFiniteMultiplicativity /-! diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/MaximalFiniteMultiplicativity.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/MaximalFiniteMultiplicativity.lean index 3ffc8a4580..e3a07d23f9 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/MaximalFiniteMultiplicativity.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/MaximalFiniteMultiplicativity.lean @@ -9,10 +9,8 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorizatio import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.MaximalFiniteMultiplicativity import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.SeriesMaximalMultiplicativity -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.ProductValue import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportUnit import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportGCDProof -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Degree.Statements.Degree import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Statements.PrincipalSubringPrimality /-! diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/MaximalFiniteSupportDivisor.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/MaximalFiniteSupportDivisor.lean index 98bb8b0b53..721952a0dd 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/MaximalFiniteSupportDivisor.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/MaximalFiniteSupportDivisor.lean @@ -8,7 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.NormalizedMaximalFinite public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.RVMaximalFinite -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.ProductValue import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportUnit import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportGCDProof diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/PrincipalMaximalDivisor.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/PrincipalMaximalDivisor.lean index 532d5d58f9..fad02088f2 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/PrincipalMaximalDivisor.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/PrincipalMaximalDivisor.lean @@ -9,7 +9,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorizatio public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.RVMaximalFinite import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.PrincipalMaximalFinite -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.ProductValue import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportGCDProof /-! diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/PrincipalSubringPrimality.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/PrincipalSubringPrimality.lean index ddb2e39abf..8779732eb7 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/PrincipalSubringPrimality.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/PrincipalSubringPrimality.lean @@ -8,7 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalSubringTensor import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.PrincipalSubringPrimality -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.ProductValue import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportGCDProof import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Statements.PrincipalScalarRedistribution diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/SeriesMaximalFiniteSupportDivisor.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/SeriesMaximalFiniteSupportDivisor.lean index ce99f480a8..983d5b9cf4 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/SeriesMaximalFiniteSupportDivisor.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/SeriesMaximalFiniteSupportDivisor.lean @@ -7,7 +7,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.NormalizedSeriesMaximalFinite -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.ProductValue import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportUnit import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportGCDProof diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/SeriesPrimality.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/SeriesPrimality.lean index dbe224a46c..8d4b799b2e 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/SeriesPrimality.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Statements/SeriesPrimality.lean @@ -11,9 +11,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Nonpositive public import Mathlib.Algebra.Divisibility.Basic import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.SeriesPrimality -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.ProductValue import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportGCDProof -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Degree.Statements.Degree import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Statements.MaximalFiniteMultiplicativity /-! diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Tests/GradedDivisibility.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Tests/GradedDivisibility.lean index b49c3a3163..770789d527 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Tests/GradedDivisibility.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Tests/GradedDivisibility.lean @@ -11,7 +11,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.GradedDivisibility public import Mathlib.Data.Rat.Defs -import Mathlib.Tactic.NormNum + /-! # API checks for graded divisibility diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Tests/PrincipalMaximalFiniteSupportDivisor.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Tests/PrincipalMaximalFiniteSupportDivisor.lean index b9a724f098..e99aeeb95a 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Tests/PrincipalMaximalFiniteSupportDivisor.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Tests/PrincipalMaximalFiniteSupportDivisor.lean @@ -10,7 +10,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorizatio import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.Fixtures.ApproachZero import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.PrincipalMaximalFinite -import Mathlib.Tactic.NormNum /-! # API checks for principal-factor invariance diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Tests/SectionSixFour.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Tests/SectionSixFour.lean index 5653e01daf..acac84d4f1 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Tests/SectionSixFour.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Factorization/Tests/SectionSixFour.lean @@ -7,7 +7,7 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.FiniteSupportFactorUniqueness -import Mathlib.Tactic.NormNum + /-! # API checks for LM24 Section 6.4 diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/FiniteSupportGCDProof.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/FiniteSupportGCDProof.lean index 61ac4e1c86..acfac90c61 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/FiniteSupportGCDProof.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/FiniteSupportGCDProof.lean @@ -15,8 +15,8 @@ import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.SubgroupAlgebra import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.SubgroupGCD import LeanPool.ConwayRefinement.ConwayRefinement.RingTheory.LaurentTower import Mathlib.LinearAlgebra.FreeModule.PID -import Mathlib.RingTheory.Int.Basic import Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid +import Mathlib.Algebra.EuclideanDomain.Int /-! # Greatest common divisors of finite-support nonpositive series diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/FiniteSupportScalarExtension.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/FiniteSupportScalarExtension.lean index b1bfb30e15..af923add58 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/FiniteSupportScalarExtension.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/FiniteSupportScalarExtension.lean @@ -159,14 +159,8 @@ theorem mem_range_finiteSupportMap_iff (f : K →+* L) have hcoeff : ∀ g, AddMonoidAlgebra.coeff (finiteSupportAddMonoidAlgebraEquiv b) g ∈ Set.range f.toAddMonoidHom := by - intro g - rw [show AddMonoidAlgebra.coeff - (finiteSupportAddMonoidAlgebraEquiv b) g = - finiteSupportCoefficients b g from - congrArg (fun q : exponentMonoid G →₀ L ↦ q g) - (coeff_finiteSupportAddMonoidAlgebraEquiv - (G := G) (K := L) b)] - exact hb g + rw [coeff_finiteSupportAddMonoidAlgebraEquiv] + exact hb have hrange : finiteSupportAddMonoidAlgebraEquiv b ∈ Set.range (AddMonoidAlgebra.map (M := exponentMonoid G) f.toAddMonoidHom) := by @@ -206,7 +200,7 @@ theorem coefficient_mem_range_of_map_mul_scalar_mem_range rw [map_mul, hcoeff] change f a * (B * f (finiteSupportCoefficients p g)) = B calc - _ = B * f (finiteSupportCoefficients p g * a) := by rw [map_mul]; ring + _ = B * f (finiteSupportCoefficients p g * a) := by rw [map_mul]; ac_rfl _ = B := by rw [ha, map_one, mul_one] section ScalarExtension diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Boundary.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Boundary.lean index e81a8be93f..09e7eeb84b 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Boundary.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Boundary.lean @@ -6,8 +6,6 @@ Authors: Dan Abramov module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Derivative -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Leibniz -import Mathlib.Tactic.Abel /-! # Boundary estimates for Cantor–Bendixson degrees of truncations diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Cancellation.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Cancellation.lean index 9c6f7ffa10..88ce374c39 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Cancellation.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Cancellation.lean @@ -8,7 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Power import LeanPool.ConwayRefinement.ConwayRefinement.Blueprint -import LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.LeftNeighborhood import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Nonpositive import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.NaturalPrincipal import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.NaturalPowerFactorization diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/CantorBendixsonRankLevels.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/CantorBendixsonRankLevels.lean index b568257bbd..8a0ffbc097 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/CantorBendixsonRankLevels.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/CantorBendixsonRankLevels.lean @@ -5,6 +5,7 @@ Authors: Dan Abramov -/ module + public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.TranslatedTruncationInterpolationOnSets import LeanPool.ConwayRefinement.ConwayRefinement.Blueprint diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/CantorBendixsonValueMultiplicativity.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/CantorBendixsonValueMultiplicativity.lean index 742429dadd..a2d301102f 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/CantorBendixsonValueMultiplicativity.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/CantorBendixsonValueMultiplicativity.lean @@ -191,7 +191,7 @@ private theorem value_eval (w : Multiset (Factor (G := G) (R := R))) : change V (translated x.1 γ * x.1 ^ m * (eval r * eval r)) = _ at h dsimp only at h rw [h] - ring + ac_rfl · have hone : V (translated x.1 γ) = 1 := by have hne : V (translated x.1 γ) ≠ 0 := by dsimp only @@ -207,7 +207,7 @@ private theorem value_eval (w : Multiset (Factor (G := G) (R := R))) : (NatOrdinal.of.injective hone)) dsimp only at hmul h hone rw [mul_assoc, hmul, h, hone] - ring + ac_rfl rcases eq_or_ne r 0 with hr0 | hr0 · rw [heval, hvp, hr0, eval_zero, valueProd_zero, mul_one, mul_one] apply cantorBendixsonValue_pow_eq_of_eventually (x.1 : HahnSeries G R) x.1.property diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/CofactorInduction.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/CofactorInduction.lean index aead30d0b4..5ce65031a5 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/CofactorInduction.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/CofactorInduction.lean @@ -10,9 +10,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.Algebra public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.SeparatedPieceCantorBendixson public import LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.CantorBendixsonConvexCover public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.ComponentsSpan -import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.Components import Mathlib.Algebra.MvPolynomial.CommRing -import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.GradedRing.HomogeneousSpan import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Boundary import LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.LeftNeighborhood diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Derivation.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Derivation.lean index 1635df58d9..e56def0071 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Derivation.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Derivation.lean @@ -6,7 +6,6 @@ Authors: Dan Abramov module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.SuccessorLeibniz import LeanPool.ConwayRefinement.ConwayRefinement.Order.Filter.Germ.LinearMap -import Mathlib.Tactic.Abel import LeanPool.ConwayRefinement.ConwayRefinement.Blueprint /-! diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Derivative.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Derivative.lean index ca2c3c6ddd..e325b95a80 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Derivative.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Derivative.lean @@ -7,7 +7,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Graded public import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.LeastTermSup public import Mathlib.Order.Filter.Germ.Basic -import LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.LeftNeighborhood /-! # Translated truncation from degree `α + 1` to degree `α` diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Lifts.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Lifts.lean index 57e46677a2..ce627bbe4b 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Lifts.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Lifts.lean @@ -9,7 +9,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.Algebra public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.TruncationIntegerPartPrimal public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeRepresentatives public import Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous -import Mathlib.Algebra.MvPolynomial.CommRing /-! # Representatives in the associated graded ring of the Cantor–Bendixson degree diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/LowerTruncationDegree.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/LowerTruncationDegree.lean index 8522b33ee1..30314a9eee 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/LowerTruncationDegree.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/LowerTruncationDegree.lean @@ -9,8 +9,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.Co public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Lifts public import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.PairBounds import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Boundary -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Convolution -import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.Separation import LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.LeftNeighborhood /-! @@ -458,7 +456,7 @@ theorem exists_lt_forall_degree_pow_leibniz_le {a : Nonpositive G K} {m : NatOrd rw [mul_smul_comm] congr 1 rw [pow_succ] - ring + ac_rfl rw [hpowsucc, mul_sub, hmulsmul, succ_nsmul, add_smul, one_smul] abel rw [hsplit] @@ -559,11 +557,10 @@ theorem exists_lt_forall_degree_monomial_leibniz_le (MvPolynomial.monomial d' (1 : K))) := by rw [map_mul, map_pow, MvPolynomial.aeval_X] rw [hsplit, MvPolynomial.pderiv_mul, map_add, e1, e2, add_mul] - congr 1 - · by_cases hji : j = i - · rw [ite_eq_left hji, ite_eq_left hji, hji] - · rw [ite_eq_right hji, ite_eq_right hji, zero_mul, zero_mul] - · ring + by_cases hji : j = i + · subst j + simp only [ite_true, mul_assoc] + · simp only [ite_eq_right hji, zero_mul, zero_add, mul_assoc] rw [Finset.sum_congr rfl hterm, Finset.sum_add_distrib, ← Finset.mul_sum, Finset.sum_ite_eq' t i (fun _ ↦ ((n + 1 : ℕ) • (V i ^ n) * aeval V (MvPolynomial.monomial d' (1 : K))) * translatedTruncLE γ (V i)), diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Power.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Power.lean index 347f5d9248..2560e4f6df 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Power.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Power.lean @@ -158,17 +158,17 @@ private theorem partial_product_truncation_bound (b c : HahnSeries G R) (max_le_max ((cantorBendixsonValue_add_le _ _).trans (max_le_max hA hD)) hP.le) have h1 : t * (V (T b, γ) * (v ^ m * w)) < v ^ (m + 1) * r * w := by calc - _ = (t * V (T b, γ)) * (v ^ m * w) := by ring + _ = (t * V (T b, γ)) * (v ^ m * w) := by ac_rfl _ < (r * v) * (v ^ m * w) := mul_lt_mul_of_pos_right (small_values_mul_lt B B le_rfl ht hbt) (mul_pos (pow_pos hv m) hw) _ = _ := by ring have h2 : t * (v ^ (m + 1) * V (T c, γ)) < v ^ (m + 1) * r * w := by calc - _ = v ^ (m + 1) * (t * V (T c, γ)) := by ring + _ = v ^ (m + 1) * (t * V (T c, γ)) := by ac_rfl _ < v ^ (m + 1) * (r * w) := mul_lt_mul_of_pos_left (small_values_mul_lt B C hp ht hct) (pow_pos hv (m + 1)) - _ = _ := by ring + _ = _ := by ac_rfl have h3 : t * (v ^ m * r * w) < v ^ (m + 1) * r * w := by calc _ < v * (v ^ m * r * w) := diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Scalar.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Scalar.lean index 5e3b703f65..93679d83a2 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Scalar.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/Scalar.lean @@ -8,7 +8,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.Algebra public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.Residue public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.DirectSum.InternalGrading public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.DirectSum.GermChainRule -import Mathlib.Tactic.Abel /-! # Coefficients in the associated graded ring of the Cantor–Bendixson degree diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/ScalarLeadingCoefficientAtLimitOrdinal.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/ScalarLeadingCoefficientAtLimitOrdinal.lean index 650ad3fc8d..a37a49179a 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/ScalarLeadingCoefficientAtLimitOrdinal.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/ScalarLeadingCoefficientAtLimitOrdinal.lean @@ -7,7 +7,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.LimitOrdinalEvaluation public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.TruncationPolynomial -import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.GradedRing.OrdinalGenerators /-! # Scalar leading coefficients when the degree is a limit ordinal diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/SeparatedPieceCantorBendixson.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/SeparatedPieceCantorBendixson.lean index c8c4a97dfc..ba5a5ab164 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/SeparatedPieceCantorBendixson.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/SeparatedPieceCantorBendixson.lean @@ -8,7 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.SeparatedPieceSum public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Derivative public import LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.SeparatedPieceFamily -import Mathlib.Topology.DerivedSet /-! # Cantor–Bendixson ranks of sums on separated pieces diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/SuccessorLeibniz.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/SuccessorLeibniz.lean index 349c318899..0b84d09173 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/SuccessorLeibniz.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/SuccessorLeibniz.lean @@ -5,9 +5,7 @@ Authors: Dan Abramov -/ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Derivative -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Leibniz public import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.FinitePart -import Mathlib.Tactic.Abel /-! # Product rule for translated truncations of homogeneous representatives diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/TruncationExpansion.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/TruncationExpansion.lean index 1c2ba6a026..40d9667108 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/TruncationExpansion.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Germ/AlgebraicIndependence/TruncationExpansion.lean @@ -169,7 +169,7 @@ theorem sum_mul_pderiv_monomial_add_single (d : ι →₀ ℕ) (i : ι) simp only [monomial_add_single_one, pderiv_mul, mul_add, Finset.sum_add_distrib] congr 1 · rw [Finset.sum_mul, ← Finset.sum_subset hsub] - · exact Finset.sum_congr rfl fun j _ ↦ by ring + · exact Finset.sum_congr rfl fun j _ ↦ by ac_rfl · intro j _ hj rw [pderiv_monomial, Finsupp.notMem_support_iff.mp hj, Nat.cast_zero, mul_zero, monomial_zero, zero_mul, mul_zero] diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/IntegerPart/Refinement/TruncationIntegerPartFractionField.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/IntegerPart/Refinement/TruncationIntegerPartFractionField.lean index e82aa955d2..a7c482e814 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/IntegerPart/Refinement/TruncationIntegerPartFractionField.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/IntegerPart/Refinement/TruncationIntegerPartFractionField.lean @@ -5,10 +5,10 @@ Authors: Dan Abramov -/ module + public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Refinement.CompleteGermRefinement public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.TruncationIntegerPartPrimal -import LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.ArchimedeanBallBase import Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic import LeanPool.ConwayRefinement.ConwayRefinement.Blueprint diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Iterate.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Iterate.lean index dd422b328d..f85a95fdd7 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Iterate.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Iterate.lean @@ -9,7 +9,6 @@ public import Mathlib.RingTheory.HahnSeries.Multiplication public import Mathlib.RingTheory.HahnSeries.Cardinal public import Mathlib.Algebra.Order.Monoid.Prod public import Mathlib.SetTheory.Cardinal.Regular -import Mathlib.Algebra.BigOperators.Group.Finset.Sigma /-! # Iterated Hahn series as Hahn series on a lexicographic product diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Monomial.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Monomial.lean index 22d1815588..3989ef7287 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Monomial.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Monomial.lean @@ -7,7 +7,7 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Nonpositive -import Mathlib.Algebra.GroupWithZero.Divisibility + /-! # Monomials in a nonpositive Hahn-series ring diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/BaseChange.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/BaseChange.lean index a50195fdc2..55bba86a6d 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/BaseChange.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/BaseChange.lean @@ -11,12 +11,7 @@ public import Mathlib.LinearAlgebra.FiniteDimensional.Defs public import Mathlib.RingTheory.TensorProduct.Basic public import Mathlib.LinearAlgebra.Basis.Defs -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.StableInterval -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueSupport -import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeAssociatedGradedMap -import Mathlib.LinearAlgebra.DirectSum.TensorProduct import Mathlib.LinearAlgebra.TensorProduct.Basis -import Mathlib.LinearAlgebra.FreeModule.Basic import Mathlib.Algebra.Ring.Hom.InjSurj import Mathlib.Algebra.CharP.Algebra import Mathlib.RingTheory.TensorProduct.Maps diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/CantorBendixsonRank.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/CantorBendixsonRank.lean index a65cdfa466..8ddc7a07c4 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/CantorBendixsonRank.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/CantorBendixsonRank.lean @@ -10,9 +10,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue public import Mathlib.Topology.Instances.Real.Lemmas import LeanPool.ConwayRefinement.ConwayRefinement.Blueprint -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Germ.AlgebraicIndependence.Additive import LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.ClosedPWO -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueDegree import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueFinalSegment import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueImage import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.StableInterval diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/DerivAt.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/DerivAt.lean index a3582e0473..0135c86f73 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/DerivAt.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/DerivAt.lean @@ -11,7 +11,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Order.Filter.FunAtZeroM public import LeanPool.ConwayRefinement.ConwayRefinement.Order.Filter.FunAtZeroMinus.Pointwise public import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.FinitePart -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueSubmultiplicative + /-! # The map `∂ : P_{α+1} → Fun_{0⁻}(P_α)` diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/DerivAtInjective.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/DerivAtInjective.lean index 059465ce67..c9a1ad6081 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/DerivAtInjective.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/DerivAtInjective.lean @@ -10,12 +10,7 @@ import LeanPool.ConwayRefinement.ConwayRefinement.Blueprint public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.DerivAt public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.UnboundedTruncations -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.StableInterval -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueFinalSegment import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueImage -import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.SetOrderType -import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.AdditivelyPrincipal -import Mathlib.Topology.Instances.Real.Lemmas /-! # Injectivity of translated truncation on `P_α` for successor `α` diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/DerivationIdeal.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/DerivationIdeal.lean index 6ba1b57496..01becb2c96 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/DerivationIdeal.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/DerivationIdeal.lean @@ -11,7 +11,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.GradedRing.HomogeneousSpan import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.SumAlongCutoffs import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.OmegaSupport -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.DerivAtInjective /-! # Ideal membership of a class from ideal membership of its derivative diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/LoweringDerivation.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/LoweringDerivation.lean index 3de8b68a55..9b614d0da3 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/LoweringDerivation.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/LoweringDerivation.lean @@ -17,8 +17,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.DerivAtInjective import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalSubringFraction -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Degree.Statements.Degree -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.ProductValue /-! # `(P̂, ∂)` is a graded domain over `K` with a lowering derivation diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/OmegaSupport.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/OmegaSupport.lean index e1d3ed19c9..dad83d87ec 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/OmegaSupport.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/OmegaSupport.lean @@ -9,10 +9,7 @@ module import LeanPool.ConwayRefinement.ConwayRefinement.Blueprint public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.DerivAt public import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.SetOrderType -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Germ -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueDegree import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.PrincipalAddition -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrderType import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.DerivAtInjective /-! diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/OrdinalValueCutoffs.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/OrdinalValueCutoffs.lean index 9d9268e263..85448e7413 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/OrdinalValueCutoffs.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/OrdinalValueCutoffs.lean @@ -12,8 +12,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.Components import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueFinalSegment import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.PrincipalAddition -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.SupportSupremum -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Germ /-! # Ordinal-value bounds at translated-truncation cutoffs diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/Pieces.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/Pieces.lean index 2e207d8729..3f1ecb560e 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/Pieces.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/Pieces.lean @@ -115,7 +115,7 @@ theorem translatedTruncation_window_sub_mem (a b : ℝ) (E : K⟦ℝ⟧) {ξ : · rw [ite_eq_left h0, ite_eq_left h0, ite_eq_left ⟨by linarith, by linarith⟩, show ξ + δ + b = b + ξ + δ by - ring, + ac_rfl, sub_self] · rw [ite_eq_right h0, ite_eq_right h0, sub_zero] diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/PrincipalGraded.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/PrincipalGraded.lean index 147e995999..2d605d50b2 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/PrincipalGraded.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/PrincipalGraded.lean @@ -13,10 +13,8 @@ public import Mathlib.Algebra.MvPolynomial.Eval public import Mathlib.LinearAlgebra.Basis.VectorSpace public import Mathlib.RingTheory.Ideal.Quotient.Operations -import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.AssociatedGradedValuation import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeAssociatedGradedDomain import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.OrdinalValueDegree -import Mathlib.LinearAlgebra.Projection /-! # The internal grading of `P̂`, its finite-degree part `P̂_{<ω}` and the quotient `P̂/I` diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/SuccessorLeibniz.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/SuccessorLeibniz.lean index d7d6719ae5..57dedfc01b 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/SuccessorLeibniz.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/SuccessorLeibniz.lean @@ -10,10 +10,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalSubring public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.LeibnizRemainder -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Convolution -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueSubmultiplicative import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueImage -import Mathlib.Topology.Instances.Real.Lemmas /-! # The Leibniz rule on the spaces `P_α` diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/SumAlongCutoffs.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/SumAlongCutoffs.lean index ad5f924c1b..8c5832f5c8 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/SumAlongCutoffs.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/SumAlongCutoffs.lean @@ -13,8 +13,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue public import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.IncreasingSequenceUnion public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Translation public import Mathlib.RingTheory.HahnSeries.Summable -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Germ -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueDegree import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.PrincipalAddition import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.TruncationPolynomial diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/TruncationExpansion.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/TruncationExpansion.lean index 317573f860..201d4d485b 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/TruncationExpansion.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/TruncationExpansion.lean @@ -185,7 +185,7 @@ theorem sum_mul_pderiv_monomial_add_single (d : ι →₀ ℕ) (i : ι) (T : ι simp only [monomial_add_single_one, pderiv_mul, mul_add, Finset.sum_add_distrib] congr 1 · rw [Finset.sum_mul, ← Finset.sum_subset hsub] - · exact Finset.sum_congr rfl fun j _ ↦ by ring + · exact Finset.sum_congr rfl fun j _ ↦ by ac_rfl · intro j _ hj rw [pderiv_monomial, Finsupp.notMem_support_iff.mp hj, Nat.cast_zero, mul_zero, monomial_zero, zero_mul, mul_zero] diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/TruncationPolynomial.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/TruncationPolynomial.lean index b5189a306b..ec40f87344 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/TruncationPolynomial.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/TruncationPolynomial.lean @@ -11,7 +11,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Convolution public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.TruncationDrop public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.OrdinalExpansion -import Mathlib.Topology.Order.LeftRightNhds /-! # The polynomial of a translated truncation, and the convolution formula read in polynomials diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/UnboundedTruncations.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/UnboundedTruncations.lean index a8fb04b4b5..3ef62ca0af 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/UnboundedTruncations.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/AlgebraicIndependence/UnboundedTruncations.lean @@ -11,11 +11,8 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValue import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.StableInterval import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueFinalSegment -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueImage import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.TruncationDrop -import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.SetOrderType import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.AdditivelyPrincipal -import Mathlib.Topology.Instances.Real.Lemmas /-! # Translated truncations of a series of ordinal value `ω^β` reach every `ω^ρ`, `ρ < β` diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Convolution.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Convolution.lean index e2763945f6..cf349ea3bd 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Convolution.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Convolution.lean @@ -11,7 +11,8 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue public import Mathlib.Topology.MetricSpace.Pseudo.Defs import LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.PWOSumset -import Mathlib.Topology.Instances.Real.Lemmas +import Mathlib.Data.EReal.Operations +import Mathlib.Topology.MetricSpace.Bounded /-! # Berarducci's convolution formula for germs diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/ConvolutionList.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/ConvolutionList.lean index 8d58b1b608..a92c4df8bf 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/ConvolutionList.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/ConvolutionList.lean @@ -7,8 +7,9 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Convolution -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.ResidualPointWellOrdered -import Mathlib.Topology.Instances.Real.Lemmas +import Mathlib.Data.EReal.Operations +import Mathlib.Topology.MetricSpace.Bounded +import Mathlib.Topology.Order.T5 /-! # The multi-factor convolution formula diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/ConvolutionRemainder.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/ConvolutionRemainder.lean index 54a19aec98..376e560752 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/ConvolutionRemainder.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/ConvolutionRemainder.lean @@ -10,11 +10,10 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Convolution import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.GermValueCut -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.ResidualPointWellOrdered -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueDegree -import Mathlib.Topology.Instances.Real.Lemmas import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueSubmultiplicative import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.NaturalPrincipal +import Mathlib.Data.EReal.Operations +import Mathlib.Topology.MetricSpace.Bounded /-! # The convolution remainder estimate diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/CriticalPoint.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/CriticalPoint.lean index a8bcf80f7c..dfa0bf903f 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/CriticalPoint.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/CriticalPoint.lean @@ -10,9 +10,9 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.ConvolutionRemainder import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.MainLemma -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.ResidualPointWellOrdered import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.ProductValue -import Mathlib.Topology.Instances.Real.Lemmas +import Mathlib.Data.EReal.Operations +import Mathlib.Topology.MetricSpace.Bounded /-! # Critical points of nonpositive real Hahn series diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/CriticalPointExistence.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/CriticalPointExistence.lean index ab6c1b8089..b7833579cd 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/CriticalPointExistence.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/CriticalPointExistence.lean @@ -7,14 +7,9 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.CriticalPoint -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.NormalForm -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.PrincipalAddition import LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.PWOSumset import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.GermDegree -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.MainLemma import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalComponentDegree -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.ResidualPointWellOrdered -import Mathlib.Tactic.Linarith /-! # Existence of Berarducci critical points diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Germ.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Germ.lean index 79d71f7d2d..11870c3b6b 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Germ.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Germ.lean @@ -8,7 +8,7 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.NegativeMonomialIdeal public import Mathlib.RingTheory.Ideal.Quotient.Defs -import Mathlib.Algebra.Group.Subgroup.Lattice + /-! # Berarducci germs of nonpositive real Hahn series diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Irreducibility.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Irreducibility.lean index f8a0098a9f..bbd61ad1ae 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Irreducibility.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Irreducibility.lean @@ -10,11 +10,8 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Monomial import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.NaturalPrincipal import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.CriticalPointExistence -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.MainLemma import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueFinalSegment import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.ProductValue -import Mathlib.Tactic.Linarith -import Mathlib.Tactic.Ring /-! # Irreducibility at multiplicatively principal support order types diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/LeibnizRemainder.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/LeibnizRemainder.lean index b6060535a3..d3ffb7517e 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/LeibnizRemainder.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/LeibnizRemainder.lean @@ -11,7 +11,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.Finit import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueSubmultiplicative import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueImage -import Mathlib.Topology.Instances.Real.Lemmas /-! # The Leibniz remainder of a product near zero diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/OrdinalValue.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/OrdinalValue.lean index 97bd0ef510..cd709a6384 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/OrdinalValue.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/OrdinalValue.lean @@ -8,7 +8,7 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Germ public import LeanPool.ConwayRefinement.CombinatorialGames.NatOrdinal.Basic -import Mathlib.Tactic.Abel + /-! # Berarducci's ordinal value diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/OrdinalValueDegree.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/OrdinalValueDegree.lean index 91e47a7886..e95887ea05 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/OrdinalValueDegree.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/OrdinalValueDegree.lean @@ -11,7 +11,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrderType public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueConstantMul import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueImage -import Mathlib.Tactic.Abel /-! # The exponent of Berarducci's ordinal value diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/OrdinalValueFinalSegment.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/OrdinalValueFinalSegment.lean index cf42da4747..e51e463bd6 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/OrdinalValueFinalSegment.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/OrdinalValueFinalSegment.lean @@ -9,7 +9,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Truncation import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Negative -import Mathlib.Tactic.Linarith /-! # Final support segments and Berarducci's ordinal value diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/OrdinalValueImage.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/OrdinalValueImage.lean index a83ff30d3f..c1b811628b 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/OrdinalValueImage.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/OrdinalValueImage.lean @@ -8,8 +8,7 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValue public import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.AdditivelyPrincipal -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrderType -import Mathlib.Tactic.Abel + /-! # Image of Berarducci's ordinal value diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/OrdinalValueSubmultiplicative.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/OrdinalValueSubmultiplicative.lean index fd1b0f90c3..6278df5083 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/OrdinalValueSubmultiplicative.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/OrdinalValueSubmultiplicative.lean @@ -8,7 +8,7 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValue public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueDegree -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueConstantMul + /-! # Submultiplicativity of Berarducci's ordinal value diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PowerRemainder.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PowerRemainder.lean index 632878c11d..f886dd597c 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PowerRemainder.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PowerRemainder.lean @@ -199,7 +199,7 @@ private theorem exists_mul_germOrdinalValue_powerProduct_lt (by rw [← NatOrdinal.of_val b.principalValue]; exact NatOrdinal.of.lt_iff_lt.mpr hα₁) (mul_pos hρpos hρpos) calc t * (NatOrdinal.of (b.residualValue.val * α₁) * (V ^ m * W)) - = t * NatOrdinal.of (b.residualValue.val * α₁) * (V ^ m * W) := by ring + = t * NatOrdinal.of (b.residualValue.val * α₁) * (V ^ m * W) := by ac_rfl _ < b.residualValue * b.residualValue * b.principalValue * (V ^ m * W) := mul_lt_mul_of_pos_right key hVmW _ = powerRemainderBound b c (m + 1) := by @@ -216,13 +216,13 @@ private theorem exists_mul_germOrdinalValue_powerProduct_lt (by rw [← NatOrdinal.of_val c.principalValue]; exact NatOrdinal.of.lt_iff_lt.mpr hα₂) (mul_pos hρpos hσpos) calc t * (V ^ (m + 1) * NatOrdinal.of (c.residualValue.val * α₂)) - = V ^ (m + 1) * (t * NatOrdinal.of (c.residualValue.val * α₂)) := by ring + = V ^ (m + 1) * (t * NatOrdinal.of (c.residualValue.val * α₂)) := by ac_rfl _ < V ^ (m + 1) * (b.residualValue * c.residualValue * c.principalValue) := mul_lt_mul_of_pos_left key hVm1 _ = powerRemainderBound b c (m + 1) := by rw [powerRemainderBound, mul_assoc b.residualValue c.residualValue, c.residualValue_mul_principalValue] - ring + ac_rfl have h3 : t * (V ^ m * b.residualValue * W) < powerRemainderBound b c (m + 1) := by have htV : t < V := by have hle : t ≤ b.residualValue * NatOrdinal.of α := by @@ -250,6 +250,15 @@ private theorem exists_mul_germOrdinalValue_powerProduct_lt rw [hmono.map_max, hmono.map_max] _ < powerRemainderBound b c (m + 1) := max_lt (max_lt h1 h2) h3 +/-- A term can be split off even outside the summation set if it vanishes there. -/ +private theorem sum_eq_add_sum_erase_of_eq_zero {ι M : Type*} [DecidableEq ι] + [AddCommMonoid M] (s : Finset ι) (f : ι → M) (a : ι) + (ha : a ∉ s → f a = 0) : + ∑ i ∈ s, f i = f a + ∑ i ∈ s.erase a, f i := by + by_cases h : a ∈ s + · exact (Finset.add_sum_erase s f h).symm + · rw [Finset.erase_eq_of_notMem h, ha h, zero_add] + private theorem powerRemainder_step (b c : SeriesWithOrdinalValueAboveOne K) (hp : b.principalValue ≤ c.principalValue) (m : ℕ) (hP : ∃ η < (0 : ℝ), ∀ γ : ℝ, η < γ → γ < 0 → @@ -295,17 +304,14 @@ private theorem powerRemainder_step by_cases hb : (0 : ℝ) ∈ closure (b.1 : K⟦ℝ⟧).support · rw [germAt_eq_zero_of_not_mem_closure_support (hmem hb), mul_zero] · rw [germAt_eq_zero_of_not_mem_closure_support hb, zero_mul] - have hstep1 : ∑ β ∈ T, f β = f γ + ∑ β ∈ T.erase γ, f β := by - by_cases hmem : γ ∈ T - · exact (Finset.add_sum_erase T f hmem).symm - · rw [Finset.erase_eq_of_notMem hmem, hfγzero hmem, zero_add] + have hstep1 : ∑ β ∈ T, f β = f γ + ∑ β ∈ T.erase γ, f β := + sum_eq_add_sum_erase_of_eq_zero T f γ hfγzero have hmem0 : (0 : ℝ) ∈ T.erase γ ↔ (0 : ℝ) ∈ T := by rw [Finset.mem_erase] exact ⟨fun h ↦ h.2, fun h ↦ ⟨(ne_of_lt hhigh).symm, h⟩⟩ - have hstep2 : ∑ β ∈ T.erase γ, f β = f 0 + ∑ β ∈ (T.erase γ).erase 0, f β := by - by_cases hmem : (0 : ℝ) ∈ T.erase γ - · exact (Finset.add_sum_erase _ f hmem).symm - · rw [Finset.erase_eq_of_notMem hmem, hf0zero (fun h ↦ hmem (hmem0.mpr h)), zero_add] + have hstep2 : ∑ β ∈ T.erase γ, f β = f 0 + ∑ β ∈ (T.erase γ).erase 0, f β := + sum_eq_add_sum_erase_of_eq_zero (T.erase γ) f 0 + (fun hmem ↦ hf0zero (fun h ↦ hmem (hmem0.mpr h))) have hSeries : (b.1 ^ (m + 1 + 1) * c.1 : Series K) = b.1 * d := by rw [hddef]; ring have hcoe : ((b.1 ^ (m + 1 + 1) * c.1 : Series K) : K⟦ℝ⟧) @@ -349,10 +355,7 @@ private theorem powerRemainder_step have hβle : β ≤ 0 := hclosb hβT.1 have hβneg : β < 0 := lt_of_le_of_ne hβle hβ0 have hγβle : γ - β ≤ 0 := hclosd hβT.2 - have hγβ : γ < β := by - rcases lt_or_eq_of_le (by linarith : γ ≤ β) with h | h - · exact h - · exact absurd h.symm hβγ + have hγβ : γ < β := lt_of_le_of_ne (sub_nonpos.mp hγβle) hβγ.symm obtain ⟨α, hα, hαle⟩ := hcutb β (hγb.trans hγβ) hβneg have hb₁ : germOrdinalValue (germAt (b.1 : K⟦ℝ⟧) β) ≤ NatOrdinal.of (b.residualValue.val * α) := by @@ -360,7 +363,9 @@ private theorem powerRemainder_step simpa using NatOrdinal.of.le_iff_le.mpr hαle refine lt_of_le_of_lt ((germOrdinalValue_mul_le_naturalMul _ _).trans (mul_le_mul_left hb₁ _)) ?_ - exact hQ (γ - β) (by linarith) (by linarith) α hα + exact hQ (γ - β) + (lt_sub_iff_add_lt.mpr ((add_lt_of_neg_right ηQ hβneg).trans hγQ)) + (sub_neg.mpr hγβ) α hα /-- Berarducci, Lemma 7.7 in the product-rule form used by Lemma 8.2: the germ of `b ^ (m + 1) * c` at a sufficiently high negative cutoff differs from `(m + 1) * b^{|γ} b^m c + b^{m+1} c^{|γ}` by a diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalComponent.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalComponent.lean index 8b5a50cedc..6f8840554e 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalComponent.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalComponent.lean @@ -12,7 +12,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.NormalForm import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.Residue -import Mathlib.Tactic.Abel /-! # The spaces `P_α` diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalComponentTensor.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalComponentTensor.lean index ffc631550f..dc5f915d17 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalComponentTensor.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalComponentTensor.lean @@ -10,7 +10,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSuppor public import Mathlib.LinearAlgebra.TensorProduct.Basic import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.GermDegree -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.NormalForm import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.PrincipalAddition import Mathlib.LinearAlgebra.TensorProduct.Basis @@ -54,7 +53,7 @@ private theorem coe_translatedTruncation_translate (p : Series K) (h g : ℝ) : rw [coe_translatedTruncation, HahnSeries.truncLE_translate, HahnSeries.translate_add_apply] congr 2 - · ring + · ac_rfl variable (K) in /-- On a series `b` of degree `≤ α`, the class of the translated truncation `b^{|γ}` in `P_α`, diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalSubringFraction.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalSubringFraction.lean index 4b808c0a5c..054654371f 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalSubringFraction.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalSubringFraction.lean @@ -8,7 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalSubring public import Mathlib.RingTheory.Localization.FractionRing -import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.AssociatedGradedDivisibility import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeAssociatedGradedDomain import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.OrdinalValueDegree diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalSubringFractionAlgebraic.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalSubringFractionAlgebraic.lean index a814b72068..9cffaf01ab 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalSubringFractionAlgebraic.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalSubringFractionAlgebraic.lean @@ -13,7 +13,6 @@ public import Mathlib.RingTheory.Algebraic.Defs public import Mathlib.FieldTheory.Minpoly.Basic import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.ProductValue /-! # Degrees in a homogenized algebraic relation @@ -599,7 +598,7 @@ theorem eval_scaleRoots_map {R : Type*} [CommRing R] [Nontrivial R] (g : K →+* exact Nat.lt_succ_self _)] refine Finset.sum_congr rfl fun i _ ↦ ?_ rw [Polynomial.coeff_scaleRoots, Polynomial.coeff_map, hdeg] - ring + ac_rfl omit [CharZero K] in /-- Coefficient extension carries the homogenized relation sum of a polynomial to that of the @@ -808,7 +807,7 @@ theorem exists_relation_of_aeval_eq_zero (Q : Polynomial K) rw [eval_scaleRoots_map] at heval rw [← heval] refine Finset.sum_congr rfl fun i _ ↦ ?_ - ring + ac_rfl /-! ### The minimal-polynomial bound -/ diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalSubringLocalization.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalSubringLocalization.lean index 4a6719c7d1..1d336e9ec4 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalSubringLocalization.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalSubringLocalization.lean @@ -10,8 +10,9 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportScalarTensor import Mathlib.LinearAlgebra.Basis.VectorSpace -import Mathlib.RingTheory.TensorProduct.Maps -import Mathlib.RingTheory.Flat.Domain +import Mathlib.RingTheory.Flat.Basic +import Mathlib.RingTheory.Localization.BaseChange +import Mathlib.Tactic.ContinuousFunctionalCalculus /-! # Localization of the degree-graded ring diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalSubringMonoidAlgebra.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalSubringMonoidAlgebra.lean index 8d56326648..098e4f6484 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalSubringMonoidAlgebra.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PrincipalSubringMonoidAlgebra.lean @@ -9,9 +9,8 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.FiniteSupportMonoidAlgebra import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MonoidAlgebra.SingleZeroFactors -import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.AssociatedGradedDivisibility -import Mathlib.Algebra.Algebra.Tower import Mathlib.RingTheory.TensorProduct.MonoidAlgebra +import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeAssociatedGradedDomain /-! # The degree-graded ring as a monoid algebra diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PurePowerRemainder.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PurePowerRemainder.lean index 172835b6bd..5a49e5585b 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PurePowerRemainder.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/PurePowerRemainder.lean @@ -57,7 +57,7 @@ theorem germAt_purePower_decomp (b : SeriesWithOrdinalValueAboveOne K) (m : ℕ) theorem powerRemainderBound_self (b : SeriesWithOrdinalValueAboveOne K) (m : ℕ) : powerRemainderBound b b m = powerRemainderBoundOne b (m + 1) := by rw [powerRemainderBound_eq, powerRemainderBoundOne_eq, pow_succ] - ring + ac_rfl /-- Taking both factors equal shifts the two-factor remainder by one exponent. -/ theorem powerRemainderOne_succ (b : SeriesWithOrdinalValueAboveOne K) (m : ℕ) (γ : ℝ) : diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/ResidualPointCofinality.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/ResidualPointCofinality.lean index bdc799e76e..9a7f13c6e9 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/ResidualPointCofinality.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/ResidualPointCofinality.lean @@ -8,9 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.ResidualPoint import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.StableInterval -import Mathlib.Order.Bounds.OrderIso -import Mathlib.SetTheory.Ordinal.Arithmetic -import Mathlib.Tactic.Linarith /-! # Cofinality of Berarducci residual points diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/ResidualPointOrderType.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/ResidualPointOrderType.lean index 595e6c2704..5c5b798406 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/ResidualPointOrderType.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/ResidualPointOrderType.lean @@ -13,7 +13,8 @@ import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Ordina import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.ResidualPointCofinality import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.OrderedUnion import LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.LeftNeighborhood -import Mathlib.Topology.Instances.Real.Lemmas +import Mathlib.Data.EReal.Operations +import Mathlib.Topology.MetricSpace.Bounded /-! # The residual-point tail order type diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/ResidualPointSupport.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/ResidualPointSupport.lean index 2fda4e66af..9ebb87b78e 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/ResidualPointSupport.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/ResidualPointSupport.lean @@ -8,7 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.ResidualPointTail import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueFinalSegment -import Mathlib.Tactic.Linarith /-! # Support families along Berarducci residual points diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Statements/MainLemma.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Statements/MainLemma.lean index 331c150300..85152ae9d6 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Statements/MainLemma.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Statements/MainLemma.lean @@ -12,10 +12,11 @@ import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Convol import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.MainLemma import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.ResidualPoint import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.GermValueCut -import Mathlib.Topology.Instances.Real.Lemmas import LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.LeftNeighborhood import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueSubmultiplicative import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.NaturalPrincipal +import Mathlib.Data.EReal.Operations +import Mathlib.Topology.MetricSpace.Bounded /-! # Berarducci's main lemma @@ -60,7 +61,7 @@ private theorem germ_mul_powerRemainder have h2 : toGerm c.1 * toGerm (b.1 ^ (m + 1)) = toGerm (b.1 ^ (m + 1) * c.1) := by rw [← map_mul] congr 1 - ring + ac_rfl rw [mul_add, mul_add, mul_smul_comm, ← mul_assoc, mul_comm (toGerm c.1) (germAt _ γ), mul_assoc, h1, ← mul_assoc, h2] diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Statements/ProductValue.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Statements/ProductValue.lean index 8f8e64acfc..74529fb6ad 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Statements/ProductValue.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Statements/ProductValue.lean @@ -11,11 +11,11 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue public import Mathlib.RingTheory.Ideal.Prime import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.MainLemma -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueConstantMul import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.ResidualPointValue import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.MainLemma import LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.LeftNeighborhood -import Mathlib.Topology.Instances.Real.Lemmas +import Mathlib.Data.EReal.Operations +import Mathlib.Topology.MetricSpace.Bounded /-! # Berarducci's induction on complexity @@ -160,7 +160,7 @@ theorem ordinalValue_eval [CharZero K] (w : FormalExpression K) : rw [eval_eq, valueProd, Multiset.map_singleton, Multiset.map_singleton, Multiset.prod_singleton, Multiset.prod_singleton] at h rw [h] - ring + ac_rfl · have hone : ordinalValue (translatedTruncation (x.1 : K⟦ℝ⟧) γ) = 1 := by have hne : ordinalValue (translatedTruncation (x.1 : K⟦ℝ⟧) γ) ≠ 0 := by rw [(mem_residualPointSet_iff.mp hγ).2] @@ -171,7 +171,7 @@ theorem ordinalValue_eval [CharZero K] (w : FormalExpression K) : have h := hIHred 0 (by simp) (by simp) rw [eval_zero, valueProd_zero, one_mul, one_mul] at h rw [mul_assoc, ordinalValue_mul_of_ordinalValue_eq_one hone, h, hone] - ring + ac_rfl rcases eq_or_ne r 0 with hr0 | hr0 · -- no other factor: the pure-power form of Lemma 8.2 rw [heval, hvp, hr0, eval_zero, valueProd_zero, mul_one, mul_one] diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/AlgebraicIndependence/FinitePowerFamily.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/AlgebraicIndependence/FinitePowerFamily.lean index dc1b9534d9..5211018406 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/AlgebraicIndependence/FinitePowerFamily.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/AlgebraicIndependence/FinitePowerFamily.lean @@ -3,7 +3,7 @@ Copyright (c) 2026 Dan Abramov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Dan Abramov -/ -module +module -- shake: keep-all public import LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Support.FinitePowerFamilyProof diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/AlgebraicIndependence/OmegaOmegaBoundary.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/AlgebraicIndependence/OmegaOmegaBoundary.lean index a617bffc9b..0901a9e7ef 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/AlgebraicIndependence/OmegaOmegaBoundary.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/AlgebraicIndependence/OmegaOmegaBoundary.lean @@ -3,7 +3,7 @@ Copyright (c) 2026 Dan Abramov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Dan Abramov -/ -module +module -- shake: keep-all public import LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Support.OmegaOmegaBoundary diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/AlgebraicIndependence/PrincipalIdealGE.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/AlgebraicIndependence/PrincipalIdealGE.lean index 634841cdbb..abdb9f9989 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/AlgebraicIndependence/PrincipalIdealGE.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/AlgebraicIndependence/PrincipalIdealGE.lean @@ -8,7 +8,8 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.PrincipalIdealGE import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.Fixtures.ApproachZero -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.LoweringDerivation +import Mathlib.Data.EReal.Operations +import Mathlib.Topology.MetricSpace.Bounded /-! # API checks for the filtration `I_{≥•}` diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/Convolution.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/Convolution.lean index e4b8153f3f..6abebc52ae 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/Convolution.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/Convolution.lean @@ -8,9 +8,8 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.Fixtures.ApproachZero public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Convolution -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.SupportSupremum -import Mathlib.Topology.Instances.Real.Lemmas -import Mathlib.Topology.Order.IsLUB +import Mathlib.Data.EReal.Operations +import Mathlib.Topology.MetricSpace.Bounded /-! # API checks for the convolution index diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/CriticalPoint.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/CriticalPoint.lean index 96708e5b29..79a2463ee0 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/CriticalPoint.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/CriticalPoint.lean @@ -8,8 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.CriticalPointExistence import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueDegree -import Mathlib.Tactic.Linarith -import Mathlib.Tactic.NormNum /-! # API checks for Berarducci critical points diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/OrdinalValueSubmultiplicative.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/OrdinalValueSubmultiplicative.lean index 524e77bc8e..ff62f17a28 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/OrdinalValueSubmultiplicative.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/OrdinalValueSubmultiplicative.lean @@ -8,8 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.Fixtures.ApproachZero public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValue -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueConstantMul -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueDegree import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.OrdinalValueSubmultiplicative import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.ProductValue diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/PrincipalComponentTensor.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/PrincipalComponentTensor.lean index a7654d7c20..449abd04dc 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/PrincipalComponentTensor.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/PrincipalComponentTensor.lean @@ -9,7 +9,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.Fixtur public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalComponentTensor public import Mathlib.LinearAlgebra.TensorProduct.Basis -import Mathlib.Tactic.NormNum + /-! # API checks for extension of scalars on a homogeneous component diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/PrincipalSubring.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/PrincipalSubring.lean index 7c0b1c0a1a..740d03eef3 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/PrincipalSubring.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/PrincipalSubring.lean @@ -7,7 +7,7 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalSubring -import Mathlib.Tactic.NormNum + /-! # API checks for `P̂` diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/PrincipalSubringFiniteSupport.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/PrincipalSubringFiniteSupport.lean index 2cca44d744..8412cc649b 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/PrincipalSubringFiniteSupport.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/PrincipalSubringFiniteSupport.lean @@ -176,7 +176,7 @@ theorem redistributionLeft_mul_right : outsideCoefficient * HahnSeries.Nonpositive.finiteSupportScalarHom (G := ℝ) outsideCoefficient⁻¹) * - extendedBinomial := by ring + extendedBinomial := by ac_rfl _ = extendedBinomial := by rw [← (HahnSeries.Nonpositive.finiteSupportScalarHom (G := ℝ) (K := Berarducci.PrincipalSubringFractionField ℚ)).map_mul] @@ -221,7 +221,7 @@ theorem inversePositiveDegree_is_redistributionWitness : outsideCoefficient * HahnSeries.Nonpositive.finiteSupportScalarHom (G := ℝ) outsideCoefficient⁻¹) * - extendedBinomial := by ring + extendedBinomial := by ac_rfl _ = extendedBinomial := by rw [← (HahnSeries.Nonpositive.finiteSupportScalarHom (G := ℝ) (K := Berarducci.PrincipalSubringFractionField ℚ)).map_mul] diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/PrincipalSubringTensor.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/PrincipalSubringTensor.lean index 85df89565b..df324be968 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/PrincipalSubringTensor.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/PrincipalSubringTensor.lean @@ -8,7 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalSubringTensor import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Tests.Fixtures.ApproachZero -import Mathlib.Tactic.NormNum /-! # API checks for the principal graded tensor decomposition diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/SectionSixThree.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/SectionSixThree.lean index 0d2646bdba..8f276875be 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/SectionSixThree.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Tests/SectionSixThree.lean @@ -12,7 +12,6 @@ import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.Maxim import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.PrincipalSubringPrimality import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.SeriesMaximalMultiplicativity import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorization.SeriesPrimality -import Mathlib.Tactic.NormNum /-! # API checks for LM24, Corollaries 6.3.6--6.3.9 diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Truncation.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Truncation.lean index 5e97cf344b..23b7d0e747 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Truncation.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/OrdinalValue/Truncation.lean @@ -8,7 +8,7 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Germ public import Mathlib.Topology.MetricSpace.Pseudo.Defs -import Mathlib.Tactic.Linarith + /-! # Berarducci germs at a real exponent diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/PolynomialAlgebra/InitialForms.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/PolynomialAlgebra/InitialForms.lean index 709fb4dd3b..1efb6d13b0 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/PolynomialAlgebra/InitialForms.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/PolynomialAlgebra/InitialForms.lean @@ -16,9 +16,7 @@ public import Mathlib.Data.Finsupp.Weight public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Valuation.DegreeWeightedPolynomial public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.MvPolynomial.BaseChange -import Mathlib.Algebra.MvPolynomial.Rename -import Mathlib.RingTheory.MvPolynomial.Tower -import Mathlib.Algebra.MvPolynomial.Basic + /-! # The series ring over the finite-support series and `RV̂ ≅ P̂ ⊗_K K_fin` diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/PolynomialAlgebra/PolynomialPresentation.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/PolynomialAlgebra/PolynomialPresentation.lean index 1c1d7e17fc..5fc949d758 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/PolynomialAlgebra/PolynomialPresentation.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/PolynomialAlgebra/PolynomialPresentation.lean @@ -11,11 +11,8 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Factorizatio public import Mathlib.RingTheory.Localization.FractionRing public import Mathlib.Algebra.Prime.Defs -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.DegreeValuation -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Statements.ProductValue import Mathlib.RingTheory.MvPolynomial.Localization import Mathlib.RingTheory.Polynomial.UniqueFactorization -import Mathlib.RingTheory.Ideal.Quotient.Operations /-! # Polynomial presentations of the series ring and primality @@ -236,7 +233,7 @@ theorem irreducible_coordinatePolynomialMap_of_irreducible_aeval coordinatePolynomialMap K ι (G' * H') := by rw [map_mul (coordinatePolynomialMap K ι), map_mul (coordinatePolynomialMap K ι), ← huG, ← hvH, hGH, coordinatePolynomialMap, MvPolynomial.map_C, map_mul, MvPolynomial.C_mul] - ring + ac_rfl have heq := hinj hmap have heval : ((u * v : Berarducci.FiniteSupportRing (K := K)) : Nonpositive ℝ K) * MvPolynomial.aeval b F = MvPolynomial.aeval b G' * MvPolynomial.aeval b H' := by @@ -253,7 +250,7 @@ theorem irreducible_coordinatePolynomialMap_of_irreducible_aeval have hprod : MvPolynomial.aeval b F = g₁ * h₁ := by refine mul_left_cancel₀ huv' ?_ rw [heval, hg₁, hh₁, huv₁₂] - ring + ac_rfl have hu₁dvd : u₁ ∣ ((u * v : Berarducci.FiniteSupportRing (K := K)) : Nonpositive ℝ K) := ⟨u₂, huv₁₂⟩ have hu₂dvd : u₂ ∣ ((u * v : Berarducci.FiniteSupportRing (K := K)) : @@ -284,7 +281,7 @@ theorem mem_span_of_coordinatePolynomialMap_mem_span have hmap : coordinatePolynomialMap K ι (MvPolynomial.C u * g) = coordinatePolynomialMap K ι (F * h) := by rw [map_mul, map_mul, coordinatePolynomialMap, MvPolynomial.map_C, ← huh, hq] - ring + ac_rfl have heq := hinj hmap have heval : (u : Nonpositive ℝ K) * MvPolynomial.aeval b g = MvPolynomial.aeval b F * MvPolynomial.aeval b h := by @@ -306,7 +303,7 @@ theorem mem_span_of_coordinatePolynomialMap_mem_span rw [ht, ht', hu₁₂] calc u₂ * t' = (u₁ * (hu₁unit.unit⁻¹ : Units (Nonpositive ℝ K))) * (u₂ * t') := by rw [hinv, one_mul] - _ = u₁ * u₂ * ((hu₁unit.unit⁻¹ : Units (Nonpositive ℝ K)) * t') := by ring + _ = u₁ * u₂ * ((hu₁unit.unit⁻¹ : Units (Nonpositive ℝ K)) * t') := by ac_rfl obtain ⟨t'', ht''⟩ := (AlgHom.mem_range _).mp (hb.mem_range_of_mul_mem_range u t hu (hht ▸ (MvPolynomial.aeval b).mem_range_self h)) have hh' : h = MvPolynomial.C u * t'' := by @@ -314,7 +311,7 @@ theorem mem_span_of_coordinatePolynomialMap_mem_span rw [map_mul, aeval_C_finiteSupport, ht'', hht] refine ⟨t'', mul_left_cancel₀ (MvPolynomial.C_ne_zero.mpr hu) ?_⟩ rw [heq, hh'] - ring + ac_rfl /-- The ideal `(F) ⊆ K_fin[X_i]` is the contraction of the ideal `(F) ⊆ L[X_i]`. -/ theorem span_singleton_eq_comap diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Primality/Consequences.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Primality/Consequences.lean index 58e7cd8e32..4c662cf537 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Primality/Consequences.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Primality/Consequences.lean @@ -11,7 +11,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.GradedRing.Extension public import Mathlib.RingTheory.Polynomial.UniqueFactorization -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.AlgebraicIndependence.PrincipalGraded import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.PrincipalSubringFraction /-! diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/PrincipalAddition.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/PrincipalAddition.lean index b11a1c1f13..320052c3bb 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/PrincipalAddition.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/PrincipalAddition.lean @@ -8,7 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.NormalForm import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Multiplicativity -import Mathlib.Tactic.Abel /-! # Addition of principal series diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Tests/NegativePresentation.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Tests/NegativePresentation.lean index 89dfee48f3..122f227a2f 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Tests/NegativePresentation.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Tests/NegativePresentation.lean @@ -7,7 +7,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Negative public import Mathlib.Algebra.Order.Ring.Rat -import Mathlib.Tactic.NormNum /-! # API checks for the strictly negative presentation diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Tests/OrderTypeDegree.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Tests/OrderTypeDegree.lean index 3e41db67a3..c83e00b800 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Tests/OrderTypeDegree.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Tests/OrderTypeDegree.lean @@ -10,8 +10,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.Degr public import Mathlib.Order.Prod.Lex.Basic public import Mathlib.Order.Sum.Order -import Mathlib.Data.Finsupp.Basic -import Mathlib.Data.Finsupp.Single + /-! # API checks for support order type and degree diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Tests/Truncation.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Tests/Truncation.lean index 6e9cc30d34..f32848ec85 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Tests/Truncation.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Tests/Truncation.lean @@ -7,9 +7,7 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrderType -import Mathlib.Data.Finsupp.Basic -import Mathlib.Data.Finsupp.Single -import Mathlib.Order.Sum.Order + /-! # API checks for Hahn-series truncations diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Tests/WeakNormalForm.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Tests/WeakNormalForm.lean index de31c61e72..9567da7c55 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Tests/WeakNormalForm.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/Tests/WeakNormalForm.lean @@ -8,7 +8,7 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.WeakNormalForm public import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.CantorTermCount -import Mathlib.Order.Sum.Order + /-! # API checks for LM24 weak normal forms diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/TruncationIntegerPartPrimal.lean b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/TruncationIntegerPartPrimal.lean index 0c7c5cd2ec..67049b13e6 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/TruncationIntegerPartPrimal.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/HahnSeries/TruncationIntegerPartPrimal.lean @@ -94,8 +94,8 @@ theorem isPrimal_truncationIntegerPart_iff (Z : Subring L) Subring.residueSubring constantCoeffAlgHom (Subring.fracSubring Z))) := by let e := truncationIntegerPartEquivResidueSubring (G := G) (L := L) Z - rw [← RingEquiv.isPrimal_iff e b] - exact Subring.isPrimal_residueSubring_iff (e b).2 + exact (RingEquiv.isPrimal_iff e b).symm.trans + (Subring.isPrimal_residueSubring_iff (e b).2) /-- At constant coefficient one, primality in the truncation integer part is exactly primality in the ambient nonpositive Hahn ring. This is the nonzero-residue case used in LM24, diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/LinearAlgebra/AlgebraicIndependentDet.lean b/LeanPool/ConwayRefinement/ConwayRefinement/LinearAlgebra/AlgebraicIndependentDet.lean index 1605e1e2c5..cc1fbf3721 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/LinearAlgebra/AlgebraicIndependentDet.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/LinearAlgebra/AlgebraicIndependentDet.lean @@ -8,7 +8,7 @@ module public import Mathlib.RingTheory.AlgebraicIndependent.Defs public import Mathlib.LinearAlgebra.Matrix.Determinant.Basic -import Mathlib.Algebra.MvPolynomial.Basic + /-! # Determinants of matrices of algebraically independent entries diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/LinearAlgebra/TensorProduct/Content.lean b/LeanPool/ConwayRefinement/ConwayRefinement/LinearAlgebra/TensorProduct/Content.lean index 2626069f0e..d2438d4132 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/LinearAlgebra/TensorProduct/Content.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/LinearAlgebra/TensorProduct/Content.lean @@ -178,7 +178,7 @@ private theorem contentCoordinates_mulRightFactor_apply simp only [contentCoordinates, TensorProduct.equivFinsuppOfBasisLeft_apply_tmul_apply] rw [_root_.Algebra.smul_def, _root_.Algebra.smul_def] - ring + ac_rfl | add x y hx hy => simp [map_add, hx, hy, mul_add] omit [IsDomain D] in diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Order/Archimedean.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Order/Archimedean.lean index 4e33117607..c7dcd46696 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Order/Archimedean.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Order/Archimedean.lean @@ -10,8 +10,8 @@ public import Mathlib.Data.Set.Countable public import Mathlib.Order.WellFoundedSet import Mathlib.Basic.Real.Embedding -import Mathlib.Topology.Order.Basic -import Mathlib.Topology.Instances.Real.Lemmas +import Mathlib.Data.EReal.Operations +import Mathlib.Topology.MetricSpace.Bounded /-! # Countability in Archimedean ordered groups diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Order/DifferenceAvoidance.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Order/DifferenceAvoidance.lean index 7b4f742da9..283823964e 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Order/DifferenceAvoidance.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Order/DifferenceAvoidance.lean @@ -9,7 +9,6 @@ public import Mathlib.Data.Set.Finite.Basic public import Mathlib.Data.Finset.Lattice.Fold public import Mathlib.Algebra.Group.Basic -import Mathlib.Data.Finset.Image import Mathlib.Data.Finset.Union /-! diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Order/Filter/FunAtZeroMinus.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Order/Filter/FunAtZeroMinus.lean index 5724abe19e..d5dfe8723f 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Order/Filter/FunAtZeroMinus.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Order/Filter/FunAtZeroMinus.lean @@ -11,11 +11,9 @@ public import Mathlib.Topology.MetricSpace.Pseudo.Defs public import Mathlib.LinearAlgebra.TensorProduct.Map import LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.LeftNeighborhood -import Mathlib.LinearAlgebra.TensorProduct.RightExactness import Mathlib.LinearAlgebra.Basis.VectorSpace import Mathlib.RingTheory.Flat.Basic import Mathlib.Topology.MetricSpace.Pseudo.Lemmas -import Mathlib.Tactic.Linarith /-! # Functions at `0⁻` with values in a vector space diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Order/Filter/FunAtZeroMinus/Pointwise.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Order/Filter/FunAtZeroMinus/Pointwise.lean index 8b8b6bdbf4..5c632463f7 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Order/Filter/FunAtZeroMinus/Pointwise.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Order/Filter/FunAtZeroMinus/Pointwise.lean @@ -8,7 +8,8 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.Order.Filter.FunAtZeroMinus import LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.LeftNeighborhood -import Mathlib.Topology.Instances.Real.Lemmas +import Mathlib.Data.EReal.Operations +import Mathlib.Topology.MetricSpace.Bounded /-! # Pointwise identities in `Fun_{0⁻}(V)` diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Order/Filter/Tests/FunAtZeroMinus.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Order/Filter/Tests/FunAtZeroMinus.lean index 53a6c9baef..01aa769643 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Order/Filter/Tests/FunAtZeroMinus.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Order/Filter/Tests/FunAtZeroMinus.lean @@ -8,8 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.Order.Filter.FunAtZeroMinus import Mathlib.Topology.MetricSpace.Pseudo.Lemmas -import Mathlib.Tactic.Linarith -import Mathlib.Tactic.NormNum /-! # API checks for functions at `0⁻` diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/RingTheory/LocalizationUFM.lean b/LeanPool/ConwayRefinement/ConwayRefinement/RingTheory/LocalizationUFM.lean index fa8ac216a9..d214114ba3 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/RingTheory/LocalizationUFM.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/RingTheory/LocalizationUFM.lean @@ -43,9 +43,9 @@ theorem exists_dvd_mul_of_dvd_algebraMap {p a : A} rw [map_mul, map_mul, hc, mul_assoc, hv] obtain ⟨w, hw⟩ := IsLocalization.exists_of_eq (M := S) hmap refine ⟨(v : A) * (w : A), mul_mem v.2 w.2, ⟨c₁ * (w : A), ?_⟩⟩ - calc a * ((v : A) * (w : A)) = (w : A) * (a * (v : A)) := by ring + calc a * ((v : A) * (w : A)) = (w : A) * (a * (v : A)) := by ac_rfl _ = (w : A) * (p * c₁) := hw - _ = p * (c₁ * (w : A)) := by ring + _ = p * (c₁ * (w : A)) := by ac_rfl omit [IsDomain A] [IsDomain B] in /-- A prime of the base ring stays prime after localization unless it becomes a unit. -/ @@ -59,7 +59,7 @@ theorem prime_algebraMap_of_prime (hS : S ≤ nonZeroDivisors A) {p : A} (hp : P have hrw : algebraMap A B (y₁ * z₁) = (y * z) * (algebraMap A B (t : A) * algebraMap A B (u : A)) := by rw [map_mul, ← ht, ← hu] - ring + ac_rfl rw [hrw] exact hyz.mul_right _ obtain ⟨s, hs, hps⟩ := exists_dvd_mul_of_dvd_algebraMap S hdvd @@ -90,7 +90,7 @@ private theorem exists_prime_factors_algebraMap by_cases hu : IsUnit (algebraMap A B p) · refine ⟨g, hgp, hga.trans ⟨hu.unit, ?_⟩⟩ rw [Multiset.prod_cons, map_mul, IsUnit.unit_spec] - ring + ac_rfl · refine ⟨algebraMap A B p ::ₘ g, ?_, ?_⟩ · intro q hq rcases Multiset.mem_cons.mp hq with rfl | hq diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/CantorBendixson.lean b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/CantorBendixson.lean index ee627ba173..1647983540 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/CantorBendixson.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/CantorBendixson.lean @@ -10,7 +10,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.PairB public import Mathlib.SetTheory.Ordinal.Exponential public import Mathlib.SetTheory.Ordinal.Topology -import Mathlib.Topology.Maps.Basic import Mathlib.Topology.Order.IsNormal /-! diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/CantorTermCount.lean b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/CantorTermCount.lean index 938fc7c60c..2de2815f03 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/CantorTermCount.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/CantorTermCount.lean @@ -7,7 +7,7 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.AdditivelyPrincipal -import Mathlib.Data.List.Sort + /-! # Number of terms in an uncompressed Cantor normal form diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Degree.lean b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Degree.lean index 5b389d4f66..68f72fe2cb 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Degree.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Degree.lean @@ -8,7 +8,6 @@ module public import LeanPool.ConwayRefinement.CombinatorialGames.NatOrdinal.Pow public import Mathlib.SetTheory.Ordinal.Exponential -import Mathlib.Algebra.Order.SuccPred import Mathlib.SetTheory.Ordinal.Principal /-! diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/LeastTermSup.lean b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/LeastTermSup.lean index a6270b336a..0ed9ca01a5 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/LeastTermSup.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/LeastTermSup.lean @@ -8,7 +8,6 @@ module import LeanPool.ConwayRefinement.ConwayRefinement.Blueprint public import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.LeastTerm -import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.CantorTermCount /-! # Approaching a natural sum from below in one summand diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/MultiplicativelyPrincipal.lean b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/MultiplicativelyPrincipal.lean index 821c395861..7d48fe64be 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/MultiplicativelyPrincipal.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/MultiplicativelyPrincipal.lean @@ -7,9 +7,11 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.AdditivelyPrincipal -import LeanPool.ConwayRefinement.CombinatorialGames.NatOrdinal.Pow -import Mathlib.Algebra.Order.SuccPred -import Mathlib.Tactic.NormNum +import Mathlib.Data.Rat.Cast.Order +import Mathlib.Tactic.NormNum.Abs +import Mathlib.Tactic.NormNum.DivMod +import Mathlib.Tactic.NormNum.OfScientific +import Mathlib.Tactic.NormNum.Pow /-! # Multiplicatively principal ordinal factors diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/NaturalPrincipal.lean b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/NaturalPrincipal.lean index ed97df5b95..81fa3d8ad8 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/NaturalPrincipal.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/NaturalPrincipal.lean @@ -9,7 +9,7 @@ public import LeanPool.ConwayRefinement.CombinatorialGames.NatOrdinal.Pow public import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.MultiplicativelyPrincipal import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.Degree -import Mathlib.Tactic.Ring +import Mathlib.Tactic.Ring.RingNF /-! # Principality of the natural operations @@ -127,7 +127,7 @@ theorem naturalMul_mul_lt_of_lt {ρ₁ ρ₂ π₁ π₂ α₁ α₂ : NatOrdina simpa using NatOrdinal.of.le_iff_le.mpr (NatOrdinal.omul_le_mul' ρ₂.val α₂.val) calc NatOrdinal.of (ρ₁.val * α₁.val) * NatOrdinal.of (ρ₂.val * α₂.val) ≤ (ρ₁ * α₁) * (ρ₂ * α₂) := mul_le_mul' h₁ h₂ - _ = (ρ₁ * ρ₂) * (α₁ * α₂) := by ring + _ = (ρ₁ * ρ₂) * (α₁ * α₂) := by ac_rfl _ < (ρ₁ * ρ₂) * π₂ := by refine mul_lt_mul_of_pos_left ?_ hρ exact mul_lt_of_isMultiplicativelyPrincipal hmp (hα₁.trans_le hπ) hα₂ diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/SetOrderType.lean b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/SetOrderType.lean index 00c31f0abf..20a31d8ce7 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/SetOrderType.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/SetOrderType.lean @@ -10,8 +10,7 @@ public import Mathlib.Order.WellFoundedSet public import Mathlib.SetTheory.Ordinal.Principal public import Mathlib.SetTheory.Cardinal.Aleph -import Mathlib.Order.Sum.Order -import Mathlib.Order.Hom.Set + /-! # Order type of a partially well-ordered set diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/SuccessorFactorization.lean b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/SuccessorFactorization.lean index 80a4c83d1d..0eddeea0db 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/SuccessorFactorization.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/SuccessorFactorization.lean @@ -8,7 +8,11 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.FinitePart public import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.MultiplicativelyPrincipal -import Mathlib.Tactic.NormNum +import Mathlib.Data.Rat.Cast.Order +import Mathlib.Tactic.NormNum.Abs +import Mathlib.Tactic.NormNum.DivMod +import Mathlib.Tactic.NormNum.OfScientific +import Mathlib.Tactic.NormNum.Pow /-! # Multiplicative factors at successor exponents diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Sumset.lean b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Sumset.lean index d2e26daf78..256f768677 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Sumset.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Sumset.lean @@ -9,9 +9,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.SetOr public import Mathlib.Data.Finset.MulAntidiagonal import LeanPool.ConwayRefinement.CombinatorialGames.NatOrdinal.Pow -import Mathlib.Order.Sum.Order -import Mathlib.Order.Hom.Lex -import Mathlib.SetTheory.Ordinal.Principal /-! # Order type of a sumset diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Tests/OrderedUnion.lean b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Tests/OrderedUnion.lean index 1e108ac689..2cc79b6158 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Tests/OrderedUnion.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Tests/OrderedUnion.lean @@ -8,7 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.SetOrderType import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.OrderedUnion -import Mathlib.SetTheory.Ordinal.Principal /-! # API certificate for the separated indexed-union estimate diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Tests/OrdinalFactors.lean b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Tests/OrdinalFactors.lean index b61ff3cfd6..d400735a72 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Tests/OrdinalFactors.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Tests/OrdinalFactors.lean @@ -7,7 +7,11 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.MultiplicativelyPrincipal -import Mathlib.Tactic.NormNum +import Mathlib.Data.Rat.Cast.Order +import Mathlib.Tactic.NormNum.Abs +import Mathlib.Tactic.NormNum.DivMod +import Mathlib.Tactic.NormNum.OfScientific +import Mathlib.Tactic.NormNum.Pow /-! # API checks for multiplicatively principal ordinal factors diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Tests/OrdinalFinitePart.lean b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Tests/OrdinalFinitePart.lean index 2b002a3c4e..c40fd65808 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Tests/OrdinalFinitePart.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Tests/OrdinalFinitePart.lean @@ -7,7 +7,11 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.FinitePart -import Mathlib.Tactic.NormNum +import Mathlib.Data.Rat.Cast.Order +import Mathlib.Tactic.NormNum.Abs +import Mathlib.Tactic.NormNum.DivMod +import Mathlib.Tactic.NormNum.OfScientific +import Mathlib.Tactic.NormNum.Pow /-! # API checks for finite Cantor coefficients diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Tests/OrdinalSuccessorFactorization.lean b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Tests/OrdinalSuccessorFactorization.lean index 7d445764a1..41f08096fc 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Tests/OrdinalSuccessorFactorization.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Tests/OrdinalSuccessorFactorization.lean @@ -7,7 +7,11 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.SuccessorFactorization -import Mathlib.Tactic.NormNum +import Mathlib.Data.Rat.Cast.Order +import Mathlib.Tactic.NormNum.Abs +import Mathlib.Tactic.NormNum.DivMod +import Mathlib.Tactic.NormNum.OfScientific +import Mathlib.Tactic.NormNum.Pow /-! # API checks for successor-exponent factorisation diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Tests/Sumset.lean b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Tests/Sumset.lean index 70382c85b3..fb35fc6e13 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Tests/Sumset.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/Ordinal/Tests/Sumset.lean @@ -12,7 +12,6 @@ public import Mathlib.Algebra.Order.Monoid.Prod public import Mathlib.Data.Finset.MulAntidiagonal import LeanPool.ConwayRefinement.CombinatorialGames.NatOrdinal.Pow -import Mathlib.Order.Sum.Order /-! # API check for order type of a sumset diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/ZFC/Tests/Game.lean b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/ZFC/Tests/Game.lean index 273fadaaa5..49492bdd27 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/ZFC/Tests/Game.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/ZFC/Tests/Game.lean @@ -3,7 +3,7 @@ Copyright (c) 2026 Dan Abramov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Dan Abramov -/ -module +module -- shake: keep-all import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.ZFC.Game import LeanPool.ConwayRefinement.CombinatorialGames.Game.Basic diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/ZFC/Tests/GameOperations.lean b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/ZFC/Tests/GameOperations.lean index 045422f727..741bbe2c9d 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/ZFC/Tests/GameOperations.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/SetTheory/ZFC/Tests/GameOperations.lean @@ -3,7 +3,7 @@ Copyright (c) 2026 Dan Abramov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Dan Abramov -/ -module +module -- shake: keep-all import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.ZFC.GameOperations diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/CombinatorialGames/Support/ConwayNormalForm.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/CombinatorialGames/Support/ConwayNormalForm.lean index a39277f0bc..0bc485119d 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/CombinatorialGames/Support/ConwayNormalForm.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/CombinatorialGames/Support/ConwayNormalForm.lean @@ -13,8 +13,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart. public import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.RefinementConjecture public import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Divisibility.DenominatorIdeal -import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.Degree -import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.DegreeTransfer import LeanPool.ConwayRefinement.ConwayRefinement.Blueprint /-! diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/CombinatorialGames/Support/OmegaOmegaBoundary.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/CombinatorialGames/Support/OmegaOmegaBoundary.lean index f99a77ee78..5b0473d452 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/CombinatorialGames/Support/OmegaOmegaBoundary.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/CombinatorialGames/Support/OmegaOmegaBoundary.lean @@ -8,9 +8,7 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Support.FinitePowerFamily public import Mathlib.Order.Sigma -import Mathlib.SetTheory.Ordinal.Family -import Mathlib.Tactic.Linarith -import Mathlib.Tactic.NormNum + /-! # An omnific integer at the `ω ^ ω` boundary diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Examples/NegativeMonomialRootsProof.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Examples/NegativeMonomialRootsProof.lean index 3266406c9e..fdf47254c7 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Examples/NegativeMonomialRootsProof.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Examples/NegativeMonomialRootsProof.lean @@ -8,7 +8,11 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Examples.NegativeMonomialRoots import Mathlib.Tactic.FieldSimp -import Mathlib.Tactic.Linarith +import Mathlib.Data.Rat.Cast.Order +import Mathlib.Tactic.Linarith.Frontend +import Mathlib.Tactic.NormNum.Abs +import Mathlib.Tactic.NormNum.DivMod +import Mathlib.Tactic.NormNum.OfScientific /-! # Negative Monomial Roots Proof -/ diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Support/CompleteHahnGermProof.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Support/CompleteHahnGermProof.lean index 82786c35fc..addd35f207 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Support/CompleteHahnGermProof.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Support/CompleteHahnGermProof.lean @@ -8,7 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.CompleteHahnGerm public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.Refinement.CompleteGermRefinement -import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Divisibility.Refinement import Mathlib.Algebra.Ring.Hom.InjSurj /-! # Complete Hahn Germ Proof -/ diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Support/GermPolynomialRingProof.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Support/GermPolynomialRingProof.lean index 8d7f5cb153..ed71ab8e34 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Support/GermPolynomialRingProof.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Support/GermPolynomialRingProof.lean @@ -12,8 +12,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Primality.OrdinalValueQuotient import Mathlib.Algebra.Ring.Hom.InjSurj -import Mathlib.RingTheory.Ideal.Quotient.Operations -import Mathlib.RingTheory.UniqueFactorizationDomain.Basic /-! # Proof that the ring of germs is a polynomial ring diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Support/HahnIntegerPartRefinementProof.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Support/HahnIntegerPartRefinementProof.lean index 5b9a110f68..cfc9d3f5ba 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Support/HahnIntegerPartRefinementProof.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Support/HahnIntegerPartRefinementProof.lean @@ -8,15 +8,9 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.HahnIntegerPartRefinement public import LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Examples.HahnIntegerPartRefinementCriterion -import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Divisibility.Refinement -import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Divisibility.PrimalPreimage -import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Order.Module.ArchimedeanBallSplitting import LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.CoinitialComplete import LeanPool.ConwayRefinement.ConwayRefinement.Blueprint public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.LimitTailPrimality -import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Order.ArchimedeanBall -import Mathlib.Algebra.Module.Rat -import Mathlib.Algebra.GCDMonoid.Nat import Mathlib.Basic.Real.Embedding import Mathlib.SetTheory.Cardinal.Rat diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Support/HahnSeriesGCDProof.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Support/HahnSeriesGCDProof.lean index 4651b9a0df..e6b4e98c45 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Support/HahnSeriesGCDProof.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Support/HahnSeriesGCDProof.lean @@ -9,7 +9,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Hahn public import LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Support.SeriesConsequences public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Nonpositive -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Primality.Primality +import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Primality.GCDMonoid /-! # Proofs of the Mathlib-only gcd and primality statements diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Support/InlineConwayRefinementProof.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Support/InlineConwayRefinementProof.lean index f1639a613a..55d49f41e1 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Support/InlineConwayRefinementProof.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Standalone/Mathlib/Support/InlineConwayRefinementProof.lean @@ -10,8 +10,12 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Standalone.Mathlib.Supp public import LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.ConwayRefinement public import LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Support.ConwayRefinementConsequences public import LeanPool.ConwayRefinement.CombinatorialGames.Game.Functor -import Mathlib.Tactic.Linarith import LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.ConwayRefinementProof +import Mathlib.Data.Rat.Cast.Order +import Mathlib.Tactic.Linarith.Frontend +import Mathlib.Tactic.NormNum.Abs +import Mathlib.Tactic.NormNum.DivMod +import Mathlib.Tactic.NormNum.OfScientific /-! # Inline Conway Refinement Proof -/ diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/DegreeTransfer.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/DegreeTransfer.lean index d8b12ac916..60e8fc368f 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/DegreeTransfer.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/DegreeTransfer.lean @@ -9,7 +9,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrderType public import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.Full public import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.Degree -import LeanPool.ConwayRefinement.ConwayRefinement.SetTheory.Ordinal.Degree + /-! # Degree of Conway normal forms in the full Hahn field diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/Full.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/Full.lean index efc81e2939..2fd8b83bb7 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/Full.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/Full.lean @@ -212,7 +212,7 @@ theorem toFullHahnSeries_mul_monomials (r s : ℝ) (i j : Surreal.{u}) : ((r : Surreal) * ω^ i) * ((s : Surreal) * ω^ j) = ((r * s : ℝ) : Surreal) * ω^ (i + j) := by rw [wpow_add, Real.toSurreal_mul] - ring + ac_rfl rw [hprod, toFullHahnSeries_realCast_mul_wpow, toFullHahnSeries_realCast_mul_wpow, toFullHahnSeries_realCast_mul_wpow, HahnSeries.single_mul_single] diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/NormalFormBasic.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/NormalFormBasic.lean index 723bb36cbc..367068ee7c 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/NormalFormBasic.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/NormalFormBasic.lean @@ -99,7 +99,10 @@ open Classical in private theorem toSurrealHahnSeries_aux (o : Ordinal.{u}) (f : Iio o → Surreal.{u} × ℝ) : Function.support (fun i ↦ if h : ∃ o, (f o).1 = i then (f <| Classical.choose h).2 else 0) ⊆ range (Prod.fst ∘ f) := by - aesop + intro i hi + by_cases h : ∃ o, (f o).1 = i + · exact h + · exact (hi (dite_eq_right h)).elim /-- Cast a sequence of terms into a `SurrealHahnSeries`. -/ @[coe] diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/NormalFormMul.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/NormalFormMul.lean index c510289053..c5decdb586 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/NormalFormMul.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/NormalFormMul.lean @@ -250,7 +250,7 @@ theorem term_zero_mul (x y : SurrealHahnSeries) : ofLex_coe_leadingCoeff_eq_coeffIdx_zero hy] at hcoeff rw [term_of_lt hxyLength, term_of_lt hxLength, term_of_lt hyLength, hcoeff, hexp', Real.toSurreal_mul, Surreal.wpow_add] - ring + ac_rfl /-- The leading term of the surreal represented by a series is its zeroth indexed term. -/ theorem leadingTerm_toSurreal (x : SurrealHahnSeries) : @@ -844,7 +844,7 @@ private theorem toSurreal_single_mul_of_one (p : Surreal.{u}) (r : ℝ) rw [single_mul_single] simp rw [hfactor, mul_assoc, toSurreal_single_zero_mul, hone] - ring + ac_rfl private theorem toSurreal_single_one_mul_succ (g : IGame.{u}) [Numeric g] {y : SurrealHahnSeries.{u}} {i : Surreal} {s : ℝ} diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/RealLeadingSplit.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/RealLeadingSplit.lean index 389957e09b..67806a58e5 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/RealLeadingSplit.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/RealLeadingSplit.lean @@ -19,8 +19,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.RealArchimedean import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.CardinalTruncationIrreducible import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.DomainEmbedding -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.DomainEquiv -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.ReducedCharacterization import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.DegreeTransfer /-! diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/Tests/Multiplication.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/Tests/Multiplication.lean index 5787890f8e..81e678565e 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/Tests/Multiplication.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/Tests/Multiplication.lean @@ -3,7 +3,7 @@ Copyright (c) 2026 Dan Abramov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Dan Abramov -/ -module +module -- shake: keep-all public import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.Multiplication diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/Tests/NormalFormMul.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/Tests/NormalFormMul.lean index e02242d56e..51fef962e3 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/Tests/NormalFormMul.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/HahnSeries/Tests/NormalFormMul.lean @@ -3,7 +3,7 @@ Copyright (c) 2026 Violeta Hernández Palacios. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Violeta Hernández Palacios -/ -module +module -- shake: keep-all public import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.NormalFormMul diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Basic.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Basic.lean index 4b30101c4b..31728b4a20 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Basic.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Basic.lean @@ -10,8 +10,6 @@ public import Mathlib.Algebra.Ring.Subring.Defs public import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.Round import LeanPool.ConwayRefinement.CombinatorialGames.Tactic.GameCmp -import Mathlib.Tactic.Abel -import Mathlib.Tactic.Ring /-! # Omnific integers diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Primality/FiniteClasses.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Primality/FiniteClasses.lean index 8ec0142c70..5be15ed498 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Primality/FiniteClasses.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Primality/FiniteClasses.lean @@ -10,7 +10,7 @@ import LeanPool.ConwayRefinement.ConwayRefinement.Blueprint public import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.Primality.IrreducibleOmnificIntegers public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.FiniteClassPrimality -import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.CardinalTruncationResidue + /-! # Primality for finitely many support classes diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Primality/IrreducibleOmnificIntegers.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Primality/IrreducibleOmnificIntegers.lean index 10a7072fc9..5f6724a5e6 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Primality/IrreducibleOmnificIntegers.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Primality/IrreducibleOmnificIntegers.lean @@ -14,7 +14,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart. public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.Monomial public import Mathlib.RingTheory.UniqueFactorizationDomain.Basic -import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ArchimedeanAssumptions + /-! # Every irreducible omnific integer is prime @@ -81,7 +81,8 @@ theorem eq_one_or_eq_neg_one_of_isUnit [CharZero R] rw [← HahnSeries.C_one] at h' rw [Int.cast_mul] exact HahnSeries.C_injective h' - have hm1 : m * n = 1 := by exact_mod_cast hmn + have hm1 : m * n = 1 := + Int.cast_injective (α := R) (hmn.trans Int.cast_one.symm) rcases Int.eq_one_or_neg_one_of_mul_eq_one hm1 with h1 | h1 · left apply CardSuppLTTruncationIntegerPart.toNonpositiveRingHom_injective Z @@ -283,13 +284,7 @@ theorem prime_intCast [CharZero R] {z : ℤ} (hz : Prime z) : rwa [map_intCast, Int.cast_id, map_zero] at this · intro h apply hz.not_isUnit - rcases eq_one_or_eq_neg_one_of_isUnit Z hZ h with h1 | h1 - · have := congrArg (intCoeffRingHom Z hZ) h1 - rw [map_intCast, Int.cast_id, map_one] at this - rw [this]; exact isUnit_one - · have := congrArg (intCoeffRingHom Z hZ) h1 - rw [map_intCast, Int.cast_id, map_neg, map_one] at this - rw [this]; exact isUnit_one.neg + simpa only [map_intCast, Int.cast_id] using h.map (intCoeffRingHom Z hZ) · rw [intCast_dvd_iff Z hZ hz.ne_zero, map_mul] at hab rcases hz.dvd_or_dvd hab with h | h · exact Or.inl ((intCast_dvd_iff Z hZ hz.ne_zero a).mpr h) @@ -304,21 +299,9 @@ theorem irreducible_int_of_irreducible_intCast [CharZero R] {z : ℤ} rw [hab, Int.cast_mul] rcases hz.isUnit_or_isUnit hab' with h | h · left - rcases eq_one_or_eq_neg_one_of_isUnit Z hZ h with h1 | h1 - · have := congrArg (intCoeffRingHom Z hZ) h1 - rw [map_intCast, Int.cast_id, map_one] at this - rw [this]; exact isUnit_one - · have := congrArg (intCoeffRingHom Z hZ) h1 - rw [map_intCast, Int.cast_id, map_neg, map_one] at this - rw [this]; exact isUnit_one.neg + simpa only [map_intCast, Int.cast_id] using h.map (intCoeffRingHom Z hZ) · right - rcases eq_one_or_eq_neg_one_of_isUnit Z hZ h with h1 | h1 - · have := congrArg (intCoeffRingHom Z hZ) h1 - rw [map_intCast, Int.cast_id, map_one] at this - rw [this]; exact isUnit_one - · have := congrArg (intCoeffRingHom Z hZ) h1 - rw [map_intCast, Int.cast_id, map_neg, map_one] at this - rw [this]; exact isUnit_one.neg + simpa only [map_intCast, Int.cast_id] using h.map (intCoeffRingHom Z hZ) end HahnSeries.Nonpositive diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Primality/OmnificIntegers.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Primality/OmnificIntegers.lean index 971c2a0e71..9a5f2a7d22 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Primality/OmnificIntegers.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Primality/OmnificIntegers.lean @@ -10,7 +10,7 @@ import LeanPool.ConwayRefinement.ConwayRefinement.Blueprint public import LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.IntegerPart.ReducedPrimality public import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.Primality.OrdinaryIntegers -import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ArchimedeanAssumptions + /-! # Every nonordinary reduced omnific integer is primal diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Primality/ZFC.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Primality/ZFC.lean index 68f8ade7ae..75a498dbad 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Primality/ZFC.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Primality/ZFC.lean @@ -13,6 +13,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger. import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Divisibility.PrimalPreimage + /-! # Factorisation in the class presentation of the omnific integers diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Refinement/ConwayRefinement.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Refinement/ConwayRefinement.lean index 4ef5faa1b3..f522b6aa25 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Refinement/ConwayRefinement.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Refinement/ConwayRefinement.lean @@ -10,7 +10,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.HahnSeries.Card public import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.RefinementConjecture public import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.RationalTailQuotient -import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Divisibility.PrimalPreimage import LeanPool.ConwayRefinement.ConwayRefinement.Blueprint /-! diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Tests/Basic.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Tests/Basic.lean index c08a5d5317..3eb55eb5c9 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Tests/Basic.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Tests/Basic.lean @@ -9,7 +9,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger. public import LeanPool.ConwayRefinement.CombinatorialGames.Surreal.Ordinal import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.Ordinal -import Mathlib.Algebra.Order.Ring.Cast /-! # API checks for omnific integers diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Tests/DegreeTwoOzPrime.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Tests/DegreeTwoOzPrime.lean index 8d02780882..6f31f8ee5b 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Tests/DegreeTwoOzPrime.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Tests/DegreeTwoOzPrime.lean @@ -3,7 +3,7 @@ Copyright (c) 2026 Dan Abramov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Dan Abramov -/ -module +module -- shake: keep-all public import LeanPool.ConwayRefinement.ConwayRefinement.Standalone.CombinatorialGames.Examples.DegreeTwoPrimeProof diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Tests/ZFC.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Tests/ZFC.lean index 8f9c34ca69..88a801afd3 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Tests/ZFC.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/OmnificInteger/Tests/ZFC.lean @@ -3,7 +3,7 @@ Copyright (c) 2026 Dan Abramov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Dan Abramov -/ -module +module -- shake: keep-all public import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.Primality.ZFC public import LeanPool.ConwayRefinement.ConwayRefinement.Examples.OmnificInteger.ZFCDegreeTwoPrime diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/ZFC/Cuts.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/ZFC/Cuts.lean index 582ea3bc50..edb6592c68 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/ZFC/Cuts.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/ZFC/Cuts.lean @@ -9,8 +9,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ZFC.Basic public import LeanPool.ConwayRefinement.CombinatorialGames.Surreal.Basic public import Mathlib.Logic.Small.Set -import LeanPool.ConwayRefinement.CombinatorialGames.Game.Basic -import Mathlib.Data.Set.Image + /-! # Small Conway cuts of class-coded surreal values diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/ZFC/OmnificCodes.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/ZFC/OmnificCodes.lean index e3bf08b379..069f1edd6f 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/ZFC/OmnificCodes.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/ZFC/OmnificCodes.lean @@ -9,7 +9,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ZFC.OmnificInte public import Mathlib.Algebra.Group.Irreducible.Defs public import Mathlib.Algebra.Prime.Defs -import Mathlib.Algebra.Divisibility.Units + /-! # Factorisation predicates quantified over omnific ZFC codes diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/ZFC/Properness.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/ZFC/Properness.lean index 83bd9daa12..b070ddcc7e 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/ZFC/Properness.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/ZFC/Properness.lean @@ -9,7 +9,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ZFC.OmnificCode public import Mathlib.SetTheory.ZFC.Class public import Mathlib.Logic.Small.Defs -import Mathlib.Logic.Small.Basic import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.Cardinal import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.OmnificInteger.Ordinal diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/ZFC/Tests/Properness.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/ZFC/Tests/Properness.lean index 45ae2e0810..8fe3733a11 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/ZFC/Tests/Properness.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Surreal/ZFC/Tests/Properness.lean @@ -3,7 +3,7 @@ Copyright (c) 2026 Dan Abramov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Dan Abramov -/ -module +module -- shake: keep-all import LeanPool.ConwayRefinement.ConwayRefinement.Surreal.ZFC.Properness import LeanPool.ConwayRefinement.CombinatorialGames.Game.Special diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Tests/SourceIndex.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Tests/SourceIndex.lean index 03b4bfed11..51257a551a 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Tests/SourceIndex.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Tests/SourceIndex.lean @@ -3,7 +3,7 @@ Copyright (c) 2026 Dan Abramov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Dan Abramov -/ -module +module -- shake: keep-all import LeanPool.ConwayRefinement.ConwayRefinement.Algebra.Divisibility.PrimalPreimage diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Tests/UpstreamReuse.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Tests/UpstreamReuse.lean index 66a1684a13..c2165eeb33 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Tests/UpstreamReuse.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Tests/UpstreamReuse.lean @@ -3,7 +3,7 @@ Copyright (c) 2026 Dan Abramov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Dan Abramov -/ -module +module -- shake: keep-all import Mathlib.Algebra.Divisibility.Basic import Mathlib.Algebra.DirectSum.Ring diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Topology/CantorBendixson.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Topology/CantorBendixson.lean index 5ac8d66bef..aa01366acb 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Topology/CantorBendixson.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Topology/CantorBendixson.lean @@ -10,7 +10,6 @@ public import Mathlib.Topology.Sets.Closeds public import Mathlib.SetTheory.Ordinal.Arithmetic import Mathlib.Order.TransfiniteIteration public import Mathlib.Topology.Maps.Basic -import Mathlib.Topology.Compactness.Compact /-! # Transfinite Cantor–Bendixson derivatives diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Topology/CantorBendixsonRank.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Topology/CantorBendixsonRank.lean index c462569513..d713159e8d 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Topology/CantorBendixsonRank.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Topology/CantorBendixsonRank.lean @@ -8,7 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.Topology.CantorBendixson public import LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.PWOAddition public import Mathlib.SetTheory.Ordinal.Basic -import Mathlib.Topology.DiscreteSubset /-! # Cantor–Bendixson point ranks of well-ordered supports diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Topology/CantorBendixsonReconstruction.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Topology/CantorBendixsonReconstruction.lean index c26348b809..688f982f15 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Topology/CantorBendixsonReconstruction.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Topology/CantorBendixsonReconstruction.lean @@ -9,7 +9,7 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Topology.CantorBendixso public import Mathlib.Topology.Homeomorph.Defs public import Mathlib.Topology.DiscreteSubset -import Mathlib.Topology.Maps.Basic + /-! # Local reconstruction of Cantor–Bendixson stages diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Order/CantorBendixsonConvexCover.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Order/CantorBendixsonConvexCover.lean index d3612a0c07..e52ccac249 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Order/CantorBendixsonConvexCover.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Order/CantorBendixsonConvexCover.lean @@ -6,7 +6,6 @@ Authors: Dan Abramov module public import LeanPool.ConwayRefinement.ConwayRefinement.Topology.CantorBendixsonRank -import Mathlib.Order.WellFounded import Mathlib.Tactic.Abel import Mathlib.Topology.Order.MonotoneContinuity diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Order/ClosedPWO.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Order/ClosedPWO.lean index 6e0d2a1885..8a828cde70 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Order/ClosedPWO.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Order/ClosedPWO.lean @@ -11,8 +11,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Topology.CantorBendixso public import LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.PWOAddition public import Mathlib.Topology.Instances.Real.Lemmas -import Mathlib.SetTheory.Ordinal.FixedPoint -import Mathlib.Topology.Order.Monotone import Mathlib.Topology.Order.MonotoneContinuity import LeanPool.ConwayRefinement.ConwayRefinement.Blueprint diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Order/PWOSumset.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Order/PWOSumset.lean index 41a5f58182..32ff724df6 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Order/PWOSumset.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Order/PWOSumset.lean @@ -9,9 +9,9 @@ public import Mathlib.Algebra.Group.Pointwise.Set.Basic public import Mathlib.Order.WellFoundedSet public import Mathlib.Topology.MetricSpace.Pseudo.Defs -import Mathlib.Topology.Instances.Real.Lemmas import Mathlib.Topology.Order.MonotoneConvergence import Mathlib.Topology.Sequences +import Mathlib.Topology.Algebra.Ring.Real /-! # Sumsets of well-ordered sets of reals diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Order/SmallClosedSubspace.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Order/SmallClosedSubspace.lean index 44ea34a263..ad50572e71 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Order/SmallClosedSubspace.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Order/SmallClosedSubspace.lean @@ -14,7 +14,6 @@ public import Mathlib.SetTheory.Cardinal.Rat public import Mathlib.Topology.Algebra.Module.Basic import LeanPool.ConwayRefinement.ConwayRefinement.Blueprint -import Mathlib.Tactic.NormNum.Inv import Mathlib.Tactic.NormNum.Ineq /-! diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Order/Tests/CantorBendixsonConvexCover.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Order/Tests/CantorBendixsonConvexCover.lean index 6f4dfc9d51..56b73388c5 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Order/Tests/CantorBendixsonConvexCover.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Order/Tests/CantorBendixsonConvexCover.lean @@ -9,7 +9,6 @@ public import LeanPool.ConwayRefinement.ConwayRefinement.Topology.Order.CantorBe public import Mathlib.Algebra.Order.Group.PiLex public import Mathlib.Basic.Real.Basic public import Mathlib.Topology.Instances.Real.Lemmas -import Mathlib.Order.Interval.Set.OrdConnected /-! # The Cantor–Bendixson convex cover has a nondegenerate model diff --git a/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Tests/CantorBendixson.lean b/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Tests/CantorBendixson.lean index 73e0e629aa..76d182be75 100644 --- a/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Tests/CantorBendixson.lean +++ b/LeanPool/ConwayRefinement/ConwayRefinement/Topology/Tests/CantorBendixson.lean @@ -8,7 +8,6 @@ module public import LeanPool.ConwayRefinement.ConwayRefinement.Topology.CantorBendixsonProduct public import LeanPool.ConwayRefinement.ConwayRefinement.Topology.CantorBendixsonReconstruction public import Mathlib.Topology.Instances.ENat -import Mathlib.Topology.DiscreteSubset public import Mathlib.Topology.Maps.Proper.Basic /-!