Bump Lean and Mathlib to v4.34.0

Challenge/McKay.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Clawristotle contributors
 -/
 
-import Mathlib.Data.Complex.Basic
+import Mathlib.Basic.Complex.Basic
 import Mathlib.GroupTheory.Sylow
 import Mathlib.RepresentationTheory.Character
 

LeanPool/ABCExceptions/Section2.lean

@@ -414,8 +414,7 @@ theorem Finset.abcExceptionsBelow_subset_union_dyadicPoints (ε : ℝ) (X : ℕ)
     rw [← Real.rpow_le_rpow_left_iff (show 1 < (2 : ℝ) by norm_num)]
     norm_cast at this ⊢
     convert this using 2
-    · rfl
-    · ring_nf
+    ring
   have {a : ℕ} : (2 ^ n : ℝ) ^ (Nat.log 2 (radical a) / n : ℝ) =
       2 ^ Nat.log 2 (radical a) := by
     rw [← Real.rpow_natCast_mul (by norm_num)]
@@ -849,7 +848,7 @@ private theorem prod_y_large_le_X_pow : ∏ m ∈ Finset.Ioc d n, y m ≤ (X : 
     _ ≤ (∏ m ∈ Finset.Ioc d n, y m ^ m : ℝ) ^ (d⁻¹ : ℝ) := by
       rw [← Real.finsetProd_rpow]
       · push_cast
-        apply Finset.prod_le_prod
+        apply Finset.prod_le_prod₀
         · intros; positivity
         simp only [Finset.mem_Ioc, and_imp]
         intro i hMi hin
@@ -866,7 +865,7 @@ private theorem prod_y_large_le_X_pow : ∏ m ∈ Finset.Ioc d n, y m ≤ (X : 
       gcongr
       norm_cast
       conv => rhs; rw [← prod_y_pow_eq_n]
-      apply Finset.prod_le_prod_of_subset_of_one_le'
+      apply Finset.prod_le_prod_of_subset_of_one_le
       · simp
       simp only [Finset.mem_union, Finset.mem_Icc, y]
       intro i hi _
@@ -882,7 +881,7 @@ private theorem c_le_X_pow : c ≤ (X : ℝ) ^ ε := calc
   c ≤ ∏ m ∈ Finset.Ioc d n, (y m : ℝ) ^ K := by
     simp_rw [c]
     push_cast
-    apply Finset.prod_le_prod
+    apply Finset.prod_le_prod₀
     · intros; positivity
     simp only [Finset.mem_Ioc, and_imp]
     intro x hMx hxn
@@ -1057,7 +1056,7 @@ private theorem X_pow_mul_prod_le_radical : (X : ℝ)^(-ε) * ∏ j, x j ≤ (ra
         Fin.prod_univ_eq_prod_range (fun j ↦ if j + 1 ≠ K then y (j + 1) else 1) d]
     _ ≤ ∏ m ∈ Finset.range d, y (m+1) := by
       norm_cast
-      apply Finset.prod_le_prod_of_subset_of_one_le'
+      apply Finset.prod_le_prod_of_subset_of_one_le
       · exact Finset.filter_subset (fun m ↦ m + 1 ≠ K) (Finset.range d)
       · intros
         apply hy_pos
@@ -1071,7 +1070,7 @@ private theorem X_pow_mul_prod_le_radical : (X : ℝ)^(-ε) * ∏ j, x j ≤ (ra
       simp [← this, Finset.prod_map]
     _ ≤ ∏ m ∈ Finset.Icc 1 d ∪ Finset.Ioc d n, y m := by
       norm_cast
-      apply Finset.prod_le_prod_of_subset_of_one_le'
+      apply Finset.prod_le_prod_of_subset_of_one_le
       · simp_all
       · simp only [Finset.mem_union, Finset.mem_Icc, not_and]
         intro i _ _
@@ -1317,7 +1316,7 @@ theorem B_to_triple_surjOn {α β γ : ℝ} (x : ℕ) (ε : ℝ)
       ring
   have prod_log_pow_le_prod_pow {u : Fin d → ℕ} (hu : ∀ i, 0 < u i):
       ∏ i, (2 ^ Nat.log 2 (u i)) ^ (i.val + 1) ≤ ∏ i, u i ^ (i.val + 1) := by
-    apply Finset.prod_le_prod
+    apply Finset.prod_le_prod₀
     · simp
     simp only [Finset.mem_univ, forall_const]
     intro i
@@ -1371,7 +1370,7 @@ theorem B_to_triple_surjOn {α β γ : ℝ} (x : ℕ) (ε : ℝ)
         _ ≤ 2 * (∏ i, (2 ^ (Nat.log 2 (w i)+1))^(i.val+1) : ℝ):= by
           norm_cast
           gcongr _ * ?_
-          apply Finset.prod_le_prod
+          apply Finset.prod_le_prod₀
           · simp
           intro i _
           gcongr

LeanPool/AFormalizationOfBorelDeterminacyInLean/Applications/General.lean

@@ -28,11 +28,11 @@ namespace Filter
 variable {α β γ : Type*} {s t : Set α} {l : Filter α}
 lemma mem_congr (h : s =ᶠ[l] t) : s ∈ l ↔ t ∈ l := by
   apply congr_sets
-  rwa [eventuallyEq_set, eventually_iff] at h
+  rwa [eventuallyEqSet_iff, eventually_iff] at h
 lemma eventuallyEq_set' {α} {s t : Set α} {l : Filter α} :
-  l.EventuallyEq s t ↔ (s \ t)ᶜ ∈ l ∧ (t \ s)ᶜ ∈ l := by
+  l.EventuallyEqSet s t ↔ (s \ t)ᶜ ∈ l ∧ (t \ s)ᶜ ∈ l := by
   constructor <;> intro h
-  · simp [Filter.mem_congr (h.diff (Filter.EventuallyEq.refl _ t)).compl,
-      Filter.mem_congr ((Filter.EventuallyEq.refl _ t).diff h).compl]
-  · rw [Filter.eventuallyEq_set]; filter_upwards [h.1, h.2]; tauto_set
+  · simp [Filter.mem_congr (h.diff (Filter.EventuallyEqSet.refl _ t)).compl,
+      Filter.mem_congr ((Filter.EventuallyEqSet.refl _ t).diff h).compl]
+  · rw [Filter.eventuallyEqSet_iff]; filter_upwards [h.1, h.2]; tauto_set
 end Filter

LeanPool/AFormalizationOfBorelDeterminacyInLean/Applications/Meager.lean

@@ -279,7 +279,7 @@ lemma forces_trans (hU : U ⊩ V) (h : V ⊩ A) : U ⊩ A := by
   exact (hU.union h).mono diff_subset_union
 lemma forces_congr {U : tX.Opens} (h : A =ᵇ B) : U ⊩ A ↔ U ⊩ B := by
   simp_rw [forces_iff_isMeagre]
-  exact isMeagre_congr (Filter.EventuallyEq.rfl.diff h)
+  exact isMeagre_congr (Filter.EventuallyEqSet.rfl.diff h)
 private lemma forces_disjoint_iUnion_left {I} (U : I → tX.Opens)
   (hd : Pairwise (Function.onFun Disjoint (fun i ↦ (U i : Set X)))) (h : ∀ i, U i ⊩ A) :
   ⨆ i, U i ⊩ A := by

LeanPool/AFormalizationOfBorelDeterminacyInLean/Basic/General.lean

@@ -80,8 +80,8 @@ lemma Cardinal.choose_injection {α β : Type u} (f : α → Set β) (h : ∀ a,
         #(Set.range (uncurryProp recg)) ≤ _)
       (Cardinal.card_typein_lt (r := wo) a hwol)) (h a))
       (Cardinal.mk_le_mk_of_subset (Set.sdiff_eq_empty.mp hf))).some
-  refine ⟨hwo.fix (r := wo) recg, ?_, ?_⟩
+  refine ⟨hwo.wf.fix recg, ?_, ?_⟩
   · intro a a' he
     rcases trichotomous_of wo a a' with h | h | h <;> [symm at he; exact h; skip] <;>
-     (rw [hwo.fix_eq] at he; cases (equals_nonempty_some he.symm).2 ⟨⟨_, h⟩, rfl⟩)
-  · intro a; rw [hwo.fix_eq]; exact Set.sdiff_subset (Set.Nonempty.some_mem _)
+     (rw [hwo.wf.fix_eq] at he; cases (equals_nonempty_some he.symm).2 ⟨⟨_, h⟩, rfl⟩)
+  · intro a; rw [hwo.wf.fix_eq]; exact Set.sdiff_subset (Set.Nonempty.some_mem _)

LeanPool/AharoniKorman/Counterexample.lean

@@ -7,7 +7,7 @@ Authors: Bhavik Mehta
 import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Algebra.Order.Field.Rat
 import Mathlib.Algebra.Order.Star.Basic
-import Mathlib.Data.Countable.Basic
+import Mathlib.Basic.Countable.Basic
 import Mathlib.Data.Setoid.Partition
 import Mathlib.Order.Filter.AtTopBot.Basic
 import Mathlib.Order.Interval.Set.Infinite

LeanPool/AndersonConjecture/AdicKerEval.lean

@@ -133,8 +133,7 @@ lemma ker_evalₐ_le_smul_top (I : Ideal R) [IsNoetherianRing R] (n : ℕ)
         ofTensorProductEquivOfFiniteNoetherian_apply, ← LinearMap.comp_apply, nat,
         LinearMap.comp_apply]
     rw [key]
-    induction w using TensorProduct.induction_on with
-    | zero => simp
+    induction w using TensorProduct.inductionOn with
     | tmul a m =>
       simp only [TensorProduct.AlgebraTensorModule.map_tmul, LinearMap.id_apply]
       rw [ofTensorProduct_tmul]

LeanPool/AndersonConjecture/Jensen/Adjoin/Adjoin.lean

@@ -302,7 +302,7 @@ private def adjoin_surjectivity_proof
       have hf_bar_ne : f.map (φ P) ≠ 0 := by
         intro h_eq
         apply h_neg
-        have h := congr_fun (congr_arg Polynomial.coeff h_eq) i
+        have h := congr_arg (fun p => Polynomial.coeff p i) h_eq
         simp only [Polynomial.coeff_map, Polynomial.coeff_zero] at h
         exact Ideal.mem_comap.mpr (Ideal.Quotient.eq_zero_iff_mem.mp h)
       have hP_in_C : P ∈ C := by

LeanPool/AndersonConjecture/Jensen/Adjoin/FromPrime.lean

@@ -333,7 +333,7 @@ private def adjoin_from_prime_proof
       have hf_bar_ne : f.map (φ P) ≠ 0 := by
         intro h_eq
         apply h_neg
-        have h := congr_fun (congr_arg Polynomial.coeff h_eq) i
+        have h := congr_arg (fun p => Polynomial.coeff p i) h_eq
         simp only [Polynomial.coeff_map, Polynomial.coeff_zero] at h
         exact Ideal.mem_comap.mpr (Ideal.Quotient.eq_zero_iff_mem.mp h)
       -- P ∈ C: find nonzero r₀ ∈ P ∩ R, show P is minimal over (r₀)

LeanPool/AndersonConjecture/Jensen/Adjoin/Transcendental.lean

@@ -417,12 +417,11 @@ private lemma adjoinLoc_uniqueFactorizationMonoid
     exact ⟨f, 1, by simp_all,
       by rw [map_one, mul_one]⟩
   have : WfDvdMonoid S_sub := by
-    constructor
     apply Subrelation.wf (r := InvImage DvdNotUnit (fun (a : S_sub) => (a : T)))
     · intro a b ⟨ha_ne, c, hc_nu, hab_eq⟩
       refine ⟨fun h => ha_ne (Subtype.ext h), c.val, ?_, congrArg Subtype.val hab_eq⟩
       exact fun hcu_T => hc_nu (hinv c (IsLocalRing.notMem_maximalIdeal.mpr hcu_T))
-    · exact InvImage.wf _ IsWellFounded.wf
+    · exact InvImage.wf _ wellFounded_dvdNotUnit
   apply UniqueFactorizationMonoid.mk (fun {a} => ⟨fun ha_irr => ?_, Prime.irreducible⟩)
   have ha_M : (a : T) ∈ IsLocalRing.maximalIdeal T := by
     by_contra h

LeanPool/AndersonConjecture/Jensen/CloseUp/AvoidanceStep.lean

@@ -392,7 +392,7 @@ private def close_up_avoidance_step_proof
               have hf_bar_ne : f.map (φ P) ≠ 0 := by
                 intro h_eq
                 apply h_neg
-                have h := congr_fun (congr_arg Polynomial.coeff h_eq) i
+                have h := congr_arg (fun p => Polynomial.coeff p i) h_eq
                 simp only [Polynomial.coeff_map, Polynomial.coeff_zero] at h
                 exact Ideal.mem_comap.mpr (Ideal.Quotient.eq_zero_iff_mem.mp h)
               -- P is an associated prime of some T/(r₀)

LeanPool/AndersonConjecture/Jensen/CloseUp/NoCommonFactor.lean

@@ -521,7 +521,7 @@ private def close_up_aux_no_common_nonzero_proof
       have hf_bar_ne : f.map (φ P) ≠ 0 := by
         intro h_eq
         apply h_neg
-        have h := congr_fun (congr_arg Polynomial.coeff h_eq) i
+        have h := congr_arg (fun p => Polynomial.coeff p i) h_eq
         simp only [Polynomial.coeff_map, Polynomial.coeff_zero] at h
         exact Ideal.mem_comap.mpr (Ideal.Quotient.eq_zero_iff_mem.mp h)
       have hP_in_C_main : P ∈ C_main := by

LeanPool/AndersonConjecture/Jensen/CombinedStep.lean

@@ -243,7 +243,7 @@ private def close_up_all_one_pass_aux_proof
   set Pairs := Finset R'.carrier × R'.carrier with Pairs_def
   have cdec : ∀ (p : Prop), Decidable p := Classical.propDecidable
   let pairLO : LinearOrder Pairs := IsWellOrder.linearOrder WellOrderingRel
-  let pairWF : WellFoundedLT Pairs := ⟨WellOrderingRel.isWellOrder.wf⟩
+  let pairWF : WellFoundedLT Pairs := WellOrderingRel.isWellOrder.wf
   -- #Pairs ≤ max(ℵ₀, #R'): for infinite R', #(Finset R' × R') = #R'
   have hPairs_card : Cardinal.mk Pairs ≤ max Cardinal.aleph0 (Cardinal.mk R'.carrier) := by
     by_cases hfin : Finite R'.carrier
@@ -254,7 +254,7 @@ private def close_up_all_one_pass_aux_proof
     le_trans hPairs_card (max_le (le_max_left ..) R'.card_le)
   let build_union := @build_union_isNSubring T _ _ _ _
   -- Define f by well-founded recursion: f(p) closes the pair p over the union of all f(q), q < p
-  let f : Pairs → NSubring T := WellFounded.fix pairWF.wf (fun p IH =>
+  let f : Pairs → NSubring T := WellFounded.fix pairWF (fun p IH =>
     if hmono : ∀ q₁ q₂ (h₁ : q₁ < p) (h₂ : q₂ < p), q₁ ≤ q₂ →
         (IH q₁ h₁).carrier ≤ (IH q₂ h₂).carrier then
       if hprimes : ∀ q₁ q₂ (h₁ : q₁ < p) (h₂ : q₂ < p) (h12 : q₁ ≤ q₂)
@@ -311,8 +311,8 @@ private def close_up_all_one_pass_aux_proof
           (⟨(p.2 : T), hle p.2.2⟩ : (f p).carrier) ∈
             Ideal.map (Subring.inclusion hle) (Ideal.span ↑p.1)) := by
     intro p
-    induction p using pairWF.wf.induction with
-    | h p IHGood =>
+    induction p using pairWF.induction with
+    | ind p IHGood =>
     have hfq_R'_le : ∀ q (hq : q < p), R'.carrier ≤ (f q).carrier :=
       fun q hq => (IHGood q hq).1.choose
     have hfq_R'_primes : ∀ q (hq : q < p) (r : R'.carrier), Prime r →

LeanPool/AndersonConjecture/Jensen/Construction/Transfinite.lean

@@ -625,8 +625,12 @@ private def transfinite_construction_proof
                   (hprimes_lt (le_of_lt hlt') hγ_lt r
                     (((IH_wf hγ_ex.choose hγ_lt).1 β₁ hlt').trans
                       (data hγ_ex.choose).2.2.1.le r.2) hr)
+        have prime_of_eq : ∀ (S : NSubring T), S = prevF α (fun γ hγ => data γ) →
+            ∀ (hx : (r : T) ∈ S.carrier), Prime (⟨(r : T), hx⟩ : S.carrier) := by
+          rintro S rfl hx
+          exact hprime_prevF
         have hprime_prev : Prime (⟨(r : T), hmem_prev⟩ : (data α).2.1.carrier) :=
-          prime_transport _ _ h_nsub_eq.symm _ hmem_prevF_carrier hprime_prevF
+          prime_of_eq _ h_nsub_eq hmem_prev
         have hext := (data α).2.2.1
         have hprime_ring := hext.primes_preserved ⟨(r : T), hmem_prev⟩ hprime_prev
         cases heq_α

LeanPool/AndersonConjecture/Jensen/KrullDomain/HeightBound.lean

@@ -830,12 +830,11 @@ private def build_intersection_nsubring_proof
   -- WfDvdMonoid for S: divisibility in S embeds into divisibility in T (which is Noetherian)
   have : IsDomain S_sub := inferInstance
   have : WfDvdMonoid S_sub := by
-    constructor
     apply Subrelation.wf (r := InvImage DvdNotUnit (fun (a : S_sub) => (a : T)))
     · intro a b ⟨ha_ne, c, hc_nu, hab_eq⟩
       refine ⟨fun h => ha_ne (Subtype.ext h), c.val, ?_, congrArg Subtype.val hab_eq⟩
       exact fun hcu_T => hc_nu (hinv c (IsLocalRing.notMem_maximalIdeal.mpr hcu_T))
-    · exact InvImage.wf _ IsWellFounded.wf
+    · exact InvImage.wf _ wellFounded_dvdNotUnit
   have hS_mem_rep : ∀ s : S_sub,
       ∃ (a b : T), a ∈ Rbar ∧ b ∈ Rbar ∧
         b ∉ IsLocalRing.maximalIdeal T ∧ (s : T) * b = a := by

LeanPool/AndersonConjecture/Main.lean

@@ -297,10 +297,7 @@ lemma range_map_subtype_le_ideal_map {A : Type u_1} [CommRing A] [IsLocalRing A]
       (↥(IsLocalRing.maximalIdeal A : Submodule A A))).surjective z
   change (AdicCompletion.map _ (Submodule.subtype _))
     ((AdicCompletion.ofTensorProduct _ _) t) ∈ _
-  induction t using TensorProduct.induction_on with
-  | zero =>
-    rw [map_zero]
-    exact Submodule.zero_mem _
+  induction t using TensorProduct.inductionOn with
   | tmul a m =>
     rw [AdicCompletion.ofTensorProduct_tmul, map_smul, AdicCompletion.map_of]
     exact Ideal.mul_mem_left _ a (Ideal.mem_map_of_mem _ m.property)
@@ -425,10 +422,7 @@ lemma range_map_subtype_pow_le {A : Type u_1} [CommRing A] [IsLocalRing A]
       (↥(M ^ n : Submodule A A))).surjective z
   change (AdicCompletion.map _ (Submodule.subtype _))
     ((AdicCompletion.ofTensorProduct _ _) t) ∈ _
-  induction t using TensorProduct.induction_on with
-  | zero =>
-    rw [map_zero]
-    exact Submodule.zero_mem _
+  induction t using TensorProduct.inductionOn with
   | tmul a m =>
     rw [AdicCompletion.ofTensorProduct_tmul, map_smul, AdicCompletion.map_of]
     exact Ideal.mul_mem_left _ a (Ideal.mem_map_of_mem _ m.property)

LeanPool/ArchonFirstProofResults/FirstProof4/Auxiliary/Density.lean

@@ -57,7 +57,7 @@ lemma continuous_prodPoly_coeff (m : ℕ) :
     have hprod_eq : ∀ r : Fin (n + 1) → ℝ,
         (∏ i : Fin (n + 1), (X - C (r i))).coeff k =
         ((∏ i : Fin n, (X - C (r (Fin.castSucc i)))) * (X - C (r (Fin.last n)))).coeff k := by
-      intro r; congr 1; exact Fin.prod_univ_castSucc _
+      intro r; rw [Fin.prod_univ_castSucc]
     simp_rw [hprod_eq]
     cases k with
     | zero =>

LeanPool/ArchonFirstProofResults/FirstProof4/Problem4.lean

@@ -318,7 +318,7 @@ private lemma g_eval_lower_at_test_points (n : ℕ) (g : ℝ[X])
     · have hcard : (Finset.univ.erase i).card = n - 1 := by
         rw [Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ, Fintype.card_fin]
       rw [← hcard, ← Finset.prod_const]
-      exact Finset.prod_le_prod
+      exact Finset.prod_le_prod₀
         (fun _ _ => hgap_sub_δ_pos.le)
         (fun j hj => hfar j (Finset.ne_of_mem_erase hj))
     · apply pow_nonneg; linarith

LeanPool/ArchonFirstProofResults/FirstProof6/Auxiliary/DynamicColoring.lean

@@ -107,7 +107,7 @@ lemma pinv_pullback_eq
     have h_diff_nn : 0 ≤ star y ⬝ᵥ ((graphLaplacian G - L_S) *ᵥ y) :=
       (inducedLaplacian_le_graphLaplacian G S).dotProduct_mulVec_nonneg y
     rw [Matrix.sub_mulVec, hLy, zero_sub, dotProduct_neg] at h_diff_nn
-    exact (hLS_psd.dotProduct_mulVec_zero_iff y).mp
+    exact (hLS_psd.dotProduct_mulVec_zero_iff (x := y)).mp
       (le_antisymm (neg_nonneg.mp h_diff_nn) h_LS_nn)
   have hLP : L_S * P = L_S := by
     have key : ∀ v, (L_S * P) *ᵥ v = L_S *ᵥ v := by

LeanPool/ArchonFirstProofResults/FirstProof6/Problem6.lean

@@ -355,7 +355,7 @@ lemma cross_edge_sum_le_graphLaplacian
   have laplacian_row_sum : ∀ (H : SimpleGraph V) [DecidableRel H.Adj] (a : V),
       ∑ b, graphLaplacian H a b = 0 := by
     intro H _ a
-    have h := congrFun (SimpleGraph.lapMatrix_mulVec_const_eq_zero (R := ℝ) H) a
+    have h := congrFun (H.lapMatrix_mulVec_one_eq_zero ℝ) a
     rw [graphLaplacian_eq_lapMatrix]
     simpa [Matrix.mulVec, dotProduct] using h
   -- Helper: inducedLaplacian row sum = 0 (induced subgraph is itself a graph Laplacian)

LeanPool/ArtinWedderburn/ArtinWedderburnTheorem.lean

@@ -33,7 +33,7 @@ theorem ArtinWedderburnForPrime {R : Type u} [Ring R] [h_nontriv : Nontrivial R]
     ∃ (n : ℕ) (D : Type u) (_ : DivisionRing D),
       Nonempty (R ≃+* Matrix (Fin n) (Fin n) D) := by
   have top_acc : Acc (fun x y => x < y) (⊤ : Ideal R) :=
-    IsWellFounded.apply (fun x y ↦ x < y) ⊤
+    WellFounded.apply h_artinian ⊤
   have top_nice := accIdealNice h_prime h_artinian ⊤ top_acc
   have top_idem : IdemIdeal (⊤ : Ideal R) := by
     refine ⟨1, IsIdempotentElem.one, ?_⟩

LeanPool/ArtinWedderburn/CornerRing.lean

@@ -430,10 +430,7 @@ theorem lift_acc_then_ideal_acc (idem_e : IsIdempotentElem e) (J : Ideal R)
 -- a) If R is artinian, then the corner ring is artinian
 theorem corner_ring_artinian [h_ar : IsArtinian R R] :
     IsArtinian (CornerSubring idem_e) (CornerSubring idem_e) := by
-  unfold IsArtinian at *
-  unfold WellFoundedLT at *
-  have Iacc : ∀ I : Ideal R, Acc (fun x y => x < y) I := fun I ↦ WellFounded.apply h_ar.wf I
-  apply IsWellFounded.mk
+  have Iacc : ∀ I : Ideal R, Acc (fun x y => x < y) I := fun I ↦ WellFounded.apply h_ar I
   have allacc : ∀ I : Ideal (CornerSubring idem_e), Acc (fun x y => x < y) I := by
     intro I
     have h : Acc (fun x y => x < y) (idealPush idem_e (idealLift idem_e I)) :=

LeanPool/ArtinWedderburn/NonUnitalToUnital.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Matevz Miščič, Maša Žaucer, Job Petrovčič
 -/
 import Mathlib.Algebra.Ring.Basic
-import Mathlib.Algebra.Ring.MinimalAxioms
 
 /-!
 # Promoting a non-unital ring with a unit element to a unital ring
@@ -18,8 +17,7 @@ namespace LeanPool.ArtinWedderburn
 variable {R : Type*} [NonUnitalRing R]
 variable (e : R)
 
-/-- Designate `e` as the `1` element when building a unital `Ring` structure
-on `R` via `Ring.ofMinimalAxioms`. -/
+/-- Designate `e` as the `1` element when building a unital `Ring` structure on `R`. -/
 @[reducible]
 def eOne : One R := ⟨e⟩
 
@@ -28,17 +26,17 @@ variable (is_right_unit : ∀ x : R, x * e = x)
 
 -- if we have a nonunital ring where one element is the left and right unit simultaneously
 -- then it is a regular ring
-/-- Promote a non-unital ring `R` with a two-sided identity `e` to a unital `Ring R`. -/
+/-- Promote a non-unital ring `R` with a two-sided identity `e` to a unital `Ring R`.
+
+The additive structure is inherited verbatim from the `NonUnitalRing R` instance, so the
+`AddCommMonoid R` carried by the result is the one already in scope; rebuilding it (as
+`Ring.ofMinimalAxioms` would) yields `nsmulRec`/`zsmulRec` instead and makes the two
+incomparable during instance synthesis. -/
 @[reducible]
-def nonUnitalWEIsRing : Ring R :=
-  @Ring.ofMinimalAxioms R (by exact inferInstance) (by exact inferInstance) (by exact inferInstance)
-    (by exact inferInstance) (by exact eOne e)
-    (by intro a b c; rw [add_assoc])
-    (by intro a; exact AddZeroClass.zero_add a)
-    (by intro a; exact neg_add_cancel a)
-    (by intro a b c; exact mul_assoc a b c)
-    is_left_unit is_right_unit
-    (by intro a b c; exact LeftDistribClass.left_distrib a b c)
-    (by intro a b c; exact RightDistribClass.right_distrib a b c)
+def nonUnitalWEIsRing : Ring R where
+  __ := (inferInstance : NonUnitalRing R)
+  __ := eOne e
+  one_mul := is_left_unit
+  mul_one := is_right_unit
 
 end LeanPool.ArtinWedderburn