awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
oinv : Γ
hxo : oinv + x.order = 0
y : R⟦Γ⟧ := HSub.hSub (β := R⟦Γ⟧) x ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : ¬y = 0
⊢ 0 < (1 - HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).orderTop
have hr' : IsRegular r
Tactic: have hr' : IsRegular r := IsUnit.isRegular <| .of_mul_eq_one x.leadingCoeff hr
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
oinv : Γ
hxo : oinv + x.order = 0
y : R⟦Γ⟧ := HSub.hSub (β := R⟦Γ⟧) x ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : ¬y = 0
hr' : IsRegular r
⊢ 0 < (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y).order
have rw : 0 < oinv + y.order
Tactic: rw [(order_single_mul_of_isRegular hr' hy)]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
oinv : Γ
hxo : oinv + x.order = 0
y : R⟦Γ⟧ := HSub.hSub (β := R⟦Γ⟧) x ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : ¬y = 0
hr' : IsRegular r
⊢ 0 < oinv + y.order
have refine : x.order < x.order + (oinv + y.order)
Tactic: refine pos_of_lt_add_right (a := x.order) ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
oinv : Γ
hxo : oinv + x.order = 0
y : R⟦Γ⟧ := HSub.hSub (β := R⟦Γ⟧) x ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : ¬y = 0
hr' : IsRegular r
⊢ x.order < x.order + (oinv + y.order)
have rw : x.order < y.order
Tactic: rw [← add_assoc, add_comm x.order, hxo, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
oinv : Γ
hxo : oinv + x.order = 0
y : R⟦Γ⟧ := HSub.hSub (β := R⟦Γ⟧) x ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : ¬y = 0
hr' : IsRegular r
⊢ 0 < (1 - HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).orderTop
have hy' : 0 < (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y).order
Tactic: have hy' : 0 < (single oinv r * y).order := by
      rw [(order_single_mul_of_isRegular hr' hy)]
      refine pos_of_lt_add_right (a := x.order) ?_
      rw [← add_assoc, add_comm x.order, hxo, zero_add]
      exact order_lt_order_of_eq_add_single (sub_add_cancel x _).symm hy
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
oinv : Γ
hxo : oinv + x.order = 0
y : R⟦Γ⟧ := HSub.hSub (β := R⟦Γ⟧) x ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
hy : ¬y = 0
hr' : IsRegular r
hy' : 0 < (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y).order
⊢ 0 < (1 - HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).orderTop
have neg : 0 <
  (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
      (HSub.hSub (β := R⟦Γ⟧) x ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧))).orderTop
Tactic: rw [one_minus_single_neg_mul hr (sub_add_cancel x _).symm _ hxo, orderTop_neg]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
⊢ IsUnit x
have let : ∀ (u i : R) (ui : u * i = 1) (iu : i * u = 1)
  (h : (↑{ val := u, inv := i, val_inv := ui, inv_val := iu : Rˣ } : R) = x.leadingCoeff), IsUnit x
Tactic: let ⟨⟨u, i, ui, iu⟩, h⟩ := hx
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
u i : R
ui : u * i = 1
iu : i * u = 1
h : (↑{ val := u, inv := i, val_inv := ui, inv_val := iu : Rˣ } : R) = x.leadingCoeff
⊢ IsUnit x
have h₁ : u = x.leadingCoeff
Tactic: rw [Units.val_mk] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
u i : R
ui : u * i = 1
iu : i * u = 1
h : u = x.leadingCoeff
⊢ IsUnit x
have iu₁ : i * x.leadingCoeff = 1
Tactic: rw [h] at iu
Cleared hypotheses: iu, h
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
h : u = x.leadingCoeff
⊢ IsUnit x
have h' : (1 - (1 - HMul.hMul (α := R⟦Γ⟧) ((single (↑(-hxo.addUnit) : Γ) : (a : R) → R⟦Γ⟧) i : R⟦Γ⟧) x)) *
    (SummableFamily.powers
        (1 - HMul.hMul (α := R⟦Γ⟧) ((single (↑(-hxo.addUnit) : Γ) : (a : R) → R⟦Γ⟧) i : R⟦Γ⟧) x)).hsum =
  1
Tactic: have h' := SummableFamily.one_sub_self_mul_hsum_powers (unit_aux x iu _ hxo.addUnit.neg_add)
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
h : u = x.leadingCoeff
h' :
  (1 - (1 - HMul.hMul (α := R⟦Γ⟧) ((single (↑(-hxo.addUnit) : Γ) : (a : R) → R⟦Γ⟧) i : R⟦Γ⟧) x)) *
      (SummableFamily.powers
          (1 - HMul.hMul (α := R⟦Γ⟧) ((single (↑(-hxo.addUnit) : Γ) : (a : R) → R⟦Γ⟧) i : R⟦Γ⟧) x)).hsum =
    1
⊢ IsUnit x
have h'₁ : HMul.hMul (α := R⟦Γ⟧) ((single (↑(-hxo.addUnit) : Γ) : (a : R) → R⟦Γ⟧) i : R⟦Γ⟧) x *
    (SummableFamily.powers
        (1 - HMul.hMul (α := R⟦Γ⟧) ((single (↑(-hxo.addUnit) : Γ) : (a : R) → R⟦Γ⟧) i : R⟦Γ⟧) x)).hsum =
  1
Tactic: rw [sub_sub_cancel] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
⊢ IsUnit x
have inl : Subsingleton R → IsUnit x
Tactic: obtain _ | _ := subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
inl : Subsingleton R → IsUnit x
⊢ IsUnit x
have inr : Nontrivial R → IsUnit x
Tactic: obtain _ | _ := subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
h_1 : Nontrivial R
⊢ IsUnit x
have inr : IsUnit x.leadingCoeff
Tactic: refine isUnit_of_isUnit_leadingCoeff_AddUnitOrder ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
h_1 : Nontrivial R
inr : IsUnit x.leadingCoeff
⊢ IsUnit x
have inr₁ : IsAddUnit x.order
Tactic: refine isUnit_of_isUnit_leadingCoeff_AddUnitOrder ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
h_1 : Nontrivial R
⊢ IsUnit x.leadingCoeff
have inr : IsUnit.{u_3} (M := R) 1
Tactic: rw [(x.orderTop_self_sub_one_pos_iff.mp h).2]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
h_1 : Nontrivial R
⊢ IsAddUnit x.order
have this : x.orderTop = 0
Tactic: have := (x.orderTop_self_sub_one_pos_iff.mp h).1
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
h_1 : Nontrivial R
this : x.orderTop = 0
⊢ IsAddUnit x.order
have this₁ : x.order = 0
Tactic: rw [← order_eq_orderTop_of_ne_zero
        (fun h ↦ WithTop.top_ne_zero (orderTop_eq_top.mpr h ▸ this)), WithTop.coe_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
h_1 : Nontrivial R
this : x.order = 0
⊢ IsAddUnit x.order
have inr : IsAddUnit.{u_1} (M := Γ) 0
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
x : R⟦Γ⟧
⊢ IsUnit x ↔ IsUnit x.leadingCoeff
have mp : IsUnit x → IsUnit x.leadingCoeff
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
x : R⟦Γ⟧
mp : IsUnit x → IsUnit x.leadingCoeff
⊢ IsUnit x ↔ IsUnit x.leadingCoeff
have mpr : IsUnit x.leadingCoeff → IsUnit x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
u i : R⟦Γ⟧
ui : u * i = 1
iu : i * u = 1
⊢ IsUnit (↑{ val := u, inv := i, val_inv := ui, inv_val := iu : R⟦Γ⟧ˣ } : R⟦Γ⟧).leadingCoeff
have mp : (u * i).coeff (u.order + i.order) = 1
Tactic: refine
      .of_mul_eq_one (i.leadingCoeff)
        ((coeff_mul_order_add_order u i).symm.trans ?_)
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
u i : R⟦Γ⟧
ui : u * i = 1
iu : i * u = 1
⊢ (u * i).coeff (u.order + i.order) = 1
have mp : u.order + i.order = 0
Tactic: rw [ui, coeff_one, if_pos]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
u i : R⟦Γ⟧
ui : u * i = 1
iu : i * u = 1
⊢ u.order + i.order = 0
have mp : (u * i).order = 0
Tactic: rw [← order_mul (left_ne_zero_of_mul_eq_one ui) (right_ne_zero_of_mul_eq_one ui), ui, order_one]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
u i : R⟦Γ⟧
ui : u * i = 1
iu : i * u = 1
mp : (u * i).order = 0
⊢ u.order + i.order = 0
have mp₁ : Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) 1) 0
Tactic: rw [← order_mul (left_ne_zero_of_mul_eq_one ui) (right_ne_zero_of_mul_eq_one ui), ui, order_one]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
u i : R⟦Γ⟧
ui : u * i = 1
iu : i * u = 1
mp : (u * i).order = 0
mp₁ : Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) 1) 0
⊢ u.order + i.order = 0
have mp₂ : Eq.{u_1 + 1} (α := Γ) 0 0
Tactic: rw [← order_mul (left_ne_zero_of_mul_eq_one ui) (right_ne_zero_of_mul_eq_one ui), ui, order_one]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
x : R⟦Γ⟧
u i : R
ui : u * i = 1
iu : i * u = 1
hx : (↑{ val := u, inv := i, val_inv := ui, inv_val := iu : Rˣ } : R) = x.leadingCoeff
⊢ IsUnit x
have hx₁ : u = x.leadingCoeff
Tactic: rw [Units.val_mk] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
x : R⟦Γ⟧
u i : R
ui : u * i = 1
iu : i * u = 1
hx : u = x.leadingCoeff
⊢ IsUnit x
have iu₁ : i * x.leadingCoeff = 1
Tactic: rw [hx] at iu
Cleared hypotheses: iu, hx
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
x : R⟦Γ⟧
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
hx : u = x.leadingCoeff
⊢ IsUnit x
have h : (1 - (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) i : R⟦Γ⟧) x)) *
    (SummableFamily.powers (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) i : R⟦Γ⟧) x)).hsum =
  1
Tactic: have h :=
      SummableFamily.one_sub_self_mul_hsum_powers (unit_aux x iu _ (neg_add_cancel x.order))
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : CommRing R
inst_4 : IsDomain R
x : R⟦Γ⟧
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
hx : u = x.leadingCoeff
h :
  (1 - (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) i : R⟦Γ⟧) x)) *
      (SummableFamily.powers (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) i : R⟦Γ⟧) x)).hsum =
    1
⊢ IsUnit x
have h₁ : HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) i : R⟦Γ⟧) x *
    (SummableFamily.powers (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) i : R⟦Γ⟧) x)).hsum =
  1
Tactic: rw [sub_sub_cancel] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
a : Γ
r : R
⊢ Eq (α := R⟦Γ⟧) (((single a : (a : R) → R⟦Γ⟧) r)⁻¹ : R⟦Γ⟧) ((single (-a) : (a : R) → R⟦Γ⟧) r⁻¹ : R⟦Γ⟧)
have inl : Eq (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) 0)⁻¹ ((single (-a) : (a : R) → R⟦Γ⟧) 0⁻¹)
Tactic: obtain rfl | hr := eq_or_ne r 0
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
a : Γ
r : R
inl : Eq (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) 0)⁻¹ ((single (-a) : (a : R) → R⟦Γ⟧) 0⁻¹)
⊢ Eq (α := R⟦Γ⟧) (((single a : (a : R) → R⟦Γ⟧) r)⁻¹ : R⟦Γ⟧) ((single (-a) : (a : R) → R⟦Γ⟧) r⁻¹ : R⟦Γ⟧)
have inr : ∀ (hr : r ≠ 0), Eq (α := R⟦Γ⟧) (((single a : (a : R) → R⟦Γ⟧) r)⁻¹ : R⟦Γ⟧) ((single (-a) : (a : R) → R⟦Γ⟧) r⁻¹ : R⟦Γ⟧)
Tactic: obtain rfl | hr := eq_or_ne r 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
a b : Γ
r s : R
⊢ HDiv.hDiv (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((single b : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧) =
    (single (a - b) : (a : R) → R⟦Γ⟧) (r / s)
have rw : HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (((single b : (a : R) → R⟦Γ⟧) s)⁻¹ : R⟦Γ⟧) =
  (single (a - b) : (a : R) → R⟦Γ⟧) (r / s)
Tactic: rw [div_eq_mul_inv, sub_eq_add_neg, div_eq_mul_inv, inv_single, single_mul_single]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
a b : Γ
r s : R
rw :
  HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (((single b : (a : R) → R⟦Γ⟧) s)⁻¹ : R⟦Γ⟧) =
    (single (a - b) : (a : R) → R⟦Γ⟧) (r / s)
⊢ HDiv.hDiv (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((single b : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧) =
    (single (a - b) : (a : R) → R⟦Γ⟧) (r / s)
have rw₁ : HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (((single b : (a : R) → R⟦Γ⟧) s)⁻¹ : R⟦Γ⟧) =
  (single (a + -b) : (a : R) → R⟦Γ⟧) (r / s)
Tactic: rw [div_eq_mul_inv, sub_eq_add_neg, div_eq_mul_inv, inv_single, single_mul_single]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
a b : Γ
r s : R
rw :
  HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (((single b : (a : R) → R⟦Γ⟧) s)⁻¹ : R⟦Γ⟧) =
    (single (a - b) : (a : R) → R⟦Γ⟧) (r / s)
rw₁ :
  HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (((single b : (a : R) → R⟦Γ⟧) s)⁻¹ : R⟦Γ⟧) =
    (single (a + -b) : (a : R) → R⟦Γ⟧) (r / s)
⊢ HDiv.hDiv (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((single b : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧) =
    (single (a - b) : (a : R) → R⟦Γ⟧) (r / s)
have rw₂ : HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (((single b : (a : R) → R⟦Γ⟧) s)⁻¹ : R⟦Γ⟧) =
  (single (a + -b) : (a : R) → R⟦Γ⟧) (r * s⁻¹)
Tactic: rw [div_eq_mul_inv, sub_eq_add_neg, div_eq_mul_inv, inv_single, single_mul_single]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
a b : Γ
r s : R
rw :
  HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (((single b : (a : R) → R⟦Γ⟧) s)⁻¹ : R⟦Γ⟧) =
    (single (a - b) : (a : R) → R⟦Γ⟧) (r / s)
rw₁ :
  HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (((single b : (a : R) → R⟦Γ⟧) s)⁻¹ : R⟦Γ⟧) =
    (single (a + -b) : (a : R) → R⟦Γ⟧) (r / s)
rw₂ :
  HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (((single b : (a : R) → R⟦Γ⟧) s)⁻¹ : R⟦Γ⟧) =
    (single (a + -b) : (a : R) → R⟦Γ⟧) (r * s⁻¹)
⊢ HDiv.hDiv (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((single b : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧) =
    (single (a - b) : (a : R) → R⟦Γ⟧) (r / s)
have rw₃ : HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((single (-b) : (a : R) → R⟦Γ⟧) s⁻¹ : R⟦Γ⟧) =
  (single (a + -b) : (a : R) → R⟦Γ⟧) (r * s⁻¹)
Tactic: rw [div_eq_mul_inv, sub_eq_add_neg, div_eq_mul_inv, inv_single, single_mul_single]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
a b : Γ
r s : R
rw :
  HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (((single b : (a : R) → R⟦Γ⟧) s)⁻¹ : R⟦Γ⟧) =
    (single (a - b) : (a : R) → R⟦Γ⟧) (r / s)
rw₁ :
  HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (((single b : (a : R) → R⟦Γ⟧) s)⁻¹ : R⟦Γ⟧) =
    (single (a + -b) : (a : R) → R⟦Γ⟧) (r / s)
rw₂ :
  HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) (((single b : (a : R) → R⟦Γ⟧) s)⁻¹ : R⟦Γ⟧) =
    (single (a + -b) : (a : R) → R⟦Γ⟧) (r * s⁻¹)
rw₃ :
  HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((single (-b) : (a : R) → R⟦Γ⟧) s⁻¹ : R⟦Γ⟧) =
    (single (a + -b) : (a : R) → R⟦Γ⟧) (r * s⁻¹)
⊢ HDiv.hDiv (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((single b : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧) =
    (single (a - b) : (a : R) → R⟦Γ⟧) (r / s)
have rw₄ : Eq (α := R⟦Γ⟧) ((single (a + -b) : (a : R) → R⟦Γ⟧) (r * s⁻¹) : R⟦Γ⟧)
  ((single (a + -b) : (a : R) → R⟦Γ⟧) (r * s⁻¹) : R⟦Γ⟧)
Tactic: rw [div_eq_mul_inv, sub_eq_add_neg, div_eq_mul_inv, inv_single, single_mul_single]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
x : R⟦Γ⟧
x0 : x ≠ 0
⊢ x * x⁻¹ = 1
have h : (1 - (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)) *
    (SummableFamily.powers
        (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)).hsum =
  1
Tactic: have h :=
      SummableFamily.one_sub_self_mul_hsum_powers
        (unit_aux x (inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr x0)) _ (neg_add_cancel x.order))
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
x : R⟦Γ⟧
x0 : x ≠ 0
h :
  (1 - (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)) *
      (SummableFamily.powers
          (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)).hsum =
    1
⊢ x * x⁻¹ = 1
have h₁ : HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x *
    (SummableFamily.powers
        (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)).hsum =
  1
Tactic: rw [sub_sub_cancel] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
x : R⟦Γ⟧
x0 : x ≠ 0
h :
  HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x *
      (SummableFamily.powers
          (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)).hsum =
    1
⊢ x * x⁻¹ = 1
have rw : x *
    HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧)
      (SummableFamily.powers
          (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)).hsum =
  1
Tactic: rw [inv_def, ← mul_assoc, mul_comm x, h]