clean up

leanprover-community · Feb 25, 2025 · 81f5dc5 · 81f5dc5
1 parent 9c54771
commit 81f5dc5
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 32 deletions.
diff --git a/Mathlib/RingTheory/HahnSeries/Addition.lean b/Mathlib/RingTheory/HahnSeries/Addition.lean
@@ -250,9 +250,6 @@ theorem order_lt_order_of_eq_add_single {R} {Γ} [LinearOrder Γ] [Zero Γ] [Add
       simpa [this] using hg
   exact Set.IsWF.min_le_min_of_subset this
 
-  --rw [← WithTop.coe_lt_coe, order_eq_orderTop_of_ne hy, order_eq_orderTop_of_ne]
-
-
 /-- `single` as an additive monoid/group homomorphism -/
 @[simps!]
 def single.addMonoidHom (a : Γ) : R →+ HahnSeries Γ R :=

diff --git a/Mathlib/RingTheory/HahnSeries/Summable.lean b/Mathlib/RingTheory/HahnSeries/Summable.lean
@@ -692,14 +692,14 @@ theorem unit_aux (x : HahnSeries Γ R) {r : R} (hr : r * x.leadingCoeff = 1)
       simp only [AddUnits.neg_eq_val_neg, ← leadingCoeff_eq, single_mul_single,
         IsAddUnit.val_neg_add, hr, single_zero_one]
     simp only [hrx, sub_self, orderTop_zero, WithTop.top_pos]
-  have hr' : IsRegular r := IsUnit.isRegular <| isUnit_of_mul_eq_one r x.leadingCoeff hr
-  have hy' : 0 < (single (IsAddUnit.addUnit hxo).neg r * y).order := by
-    rw [(order_mul_single_of_isRegular hr' hy)]
-    refine pos_of_lt_add_right (a := x.order) ?_
-    rw [← add_assoc, add_comm x.order, AddUnits.neg_eq_val_neg, IsAddUnit.val_neg_add, zero_add]
-    exact order_lt_order_of_eq_add_single (sub_add_cancel x _).symm hy
-  rw [one_minus_single_neg_mul hr (sub_add_cancel x _).symm, orderTop_neg]
-  exact zero_lt_orderTop_of_order hy'
+  · have hr' : IsRegular r := IsUnit.isRegular <| isUnit_of_mul_eq_one r x.leadingCoeff hr
+    have hy' : 0 < (single (IsAddUnit.addUnit hxo).neg r * y).order := by
+      rw [(order_mul_single_of_isRegular hr' hy)]
+      refine pos_of_lt_add_right (a := x.order) ?_
+      rw [← add_assoc, add_comm x.order, AddUnits.neg_eq_val_neg, IsAddUnit.val_neg_add, zero_add]
+      exact order_lt_order_of_eq_add_single (sub_add_cancel x _).symm hy
+    rw [one_minus_single_neg_mul hr (sub_add_cancel x _).symm, orderTop_neg]
+    exact zero_lt_orderTop_of_order hy'
 
 theorem isUnit_of_isUnit_leadingCoeff_AddUnitOrder {x : HahnSeries Γ R} (hx : IsUnit x.leadingCoeff)
     (hxo : IsAddUnit x.order) : IsUnit x := by
@@ -716,27 +716,6 @@ section IsDomain
 
 variable [LinearOrderedAddCommGroup Γ] [CommRing R] [IsDomain R]
 
-theorem unit_aux' (x : HahnSeries Γ R) {r : R} (hr : r * x.leadingCoeff = 1) :
-    0 < (1 - single (-x.order) r * x).orderTop := by
-  by_cases hx : x = 0; · simp_all [hx]
-  have hrz : r ≠ 0 := by
-    intro h
-    rw [h, zero_mul] at hr
-    exact (zero_ne_one' R) hr
-  refine lt_of_le_of_ne (le_trans ?_ min_orderTop_le_orderTop_sub) fun h => ?_
-  · refine le_min (by rw [orderTop_one]) ?_
-    refine le_trans ?_ orderTop_add_orderTop_le_orderTop_mul
-    by_cases h : x = 0; · simp [h]
-    rw [← order_eq_orderTop_of_ne h, orderTop_single
-      (fun _ => by simp_all only [zero_mul, zero_ne_one]), ← @WithTop.coe_add,
-      WithTop.coe_nonneg, neg_add_cancel]
-  · apply coeff_orderTop_ne h.symm
-    simp only [C_apply, single_mul_single, zero_add, mul_one, coeff_sub', Pi.sub_apply, coeff_one,
-      ↓reduceIte]
-    have hrc := coeff_mul_order_add_order ((single (-x.order)) r) x
-    rw [order_single hrz, leadingCoeff_of_single, neg_add_cancel, hr] at hrc
-    rw [hrc, sub_self]
-
 theorem isUnit_iff {x : HahnSeries Γ R} : IsUnit x ↔ IsUnit (x.leadingCoeff) := by
   constructor
   · rintro ⟨⟨u, i, ui, iu⟩, rfl⟩