Optimize ConwayRefinement private imports and algebra proofs

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

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
 
 /-!

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

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

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
 
 /-!

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

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
 

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

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`

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

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

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

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
 

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