awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ¬0 < x.orderTop
⊢ powers x = single 0 1
have h : ∀ (a : ℕ) (x_1 : Γ),
  Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((powers x : (a : ℕ) → R⟦Γ⟧) a) x_1)
    (HahnSeries.coeff ((single 0 1 : (a : ℕ) → R⟦Γ⟧) a) x_1)
Tactic: ext a
-- 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 : ¬0 < x.orderTop
a : ℕ
x_1 : Γ
⊢ Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((powers x : (a : ℕ) → R⟦Γ⟧) a) x_1)
    (HahnSeries.coeff ((single 0 1 : (a : ℕ) → R⟦Γ⟧) a) x_1)
have h : Eq (α := R) (HahnSeries.coeff ((powers x : (a : ℕ) → R⟦Γ⟧) 0) x_1 : R)
  (HahnSeries.coeff ((single 0 1 : (a : ℕ) → R⟦Γ⟧) 0) x_1 : R)
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- 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 : ¬0 < x.orderTop
a : ℕ
x_1 : Γ
h :
  Eq (α := R) (HahnSeries.coeff ((powers x : (a : ℕ) → R⟦Γ⟧) 0) x_1 : R)
    (HahnSeries.coeff ((single 0 1 : (a : ℕ) → R⟦Γ⟧) 0) x_1 : R)
⊢ Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((powers x : (a : ℕ) → R⟦Γ⟧) a) x_1)
    (HahnSeries.coeff ((single 0 1 : (a : ℕ) → R⟦Γ⟧) a) x_1)
have h₁ : ∀ (ha : a ≠ 0),
  Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((powers x : (a : ℕ) → R⟦Γ⟧) a) x_1)
    (HahnSeries.coeff ((single 0 1 : (a : ℕ) → R⟦Γ⟧) a) x_1)
Tactic: obtain rfl | ha := eq_or_ne a 0
-- 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
⊢ Eq (α := SummableFamily Γ R ℕ) (powers 0) (single 0 1)
have h : ∀ (n : ℕ) (x : Γ),
  Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((powers 0 : (a : ℕ) → R⟦Γ⟧) n) x)
    (HahnSeries.coeff ((single 0 1 : (a : ℕ) → R⟦Γ⟧) n) x)
Tactic: ext n
-- 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
n : ℕ
x : Γ
⊢ Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((powers 0 : (a : ℕ) → R⟦Γ⟧) n) x)
    (HahnSeries.coeff ((single 0 1 : (a : ℕ) → R⟦Γ⟧) n) x)
have h : (HPow.hPow (α := R⟦Γ⟧) 0 n).coeff x = HahnSeries.coeff ((single 0 1 : (a : ℕ) → R⟦Γ⟧) n) x
Tactic: rw [powers_of_orderTop_pos (by simp)]
-- 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
n : ℕ
x : Γ
⊢ (HPow.hPow (α := R⟦Γ⟧) 0 n).coeff x = HahnSeries.coeff ((single 0 1 : (a : ℕ) → R⟦Γ⟧) n) x
have h : (HPow.hPow (α := R⟦Γ⟧) (β := ℕ) 0 0).coeff x = HahnSeries.coeff ((single 0 1 : (a : ℕ) → R⟦Γ⟧) 0) x
Tactic: obtain rfl | ha := eq_or_ne n 0
Cleared hypotheses: n
-- 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
n : ℕ
x : Γ
h : (HPow.hPow (α := R⟦Γ⟧) (β := ℕ) 0 0).coeff x = HahnSeries.coeff ((single 0 1 : (a : ℕ) → R⟦Γ⟧) 0) x
⊢ (HPow.hPow (α := R⟦Γ⟧) 0 n).coeff x = HahnSeries.coeff ((single 0 1 : (a : ℕ) → R⟦Γ⟧) n) x
have h₁ : ∀ (ha : n ≠ 0), (HPow.hPow (α := R⟦Γ⟧) 0 n).coeff x = HahnSeries.coeff ((single 0 1 : (a : ℕ) → R⟦Γ⟧) n) x
Tactic: obtain rfl | ha := eq_or_ne n 0
-- 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 : 0 < x.orderTop
⊢ Eq (α := (a : ℕ) → R⟦Γ⟧) (⇑(powers x) : (a : ℕ) → R⟦Γ⟧) (HPow.hPow x)
have h : ∀ (n : ℕ), (powers x : (a : ℕ) → R⟦Γ⟧) n = x ^ n
Tactic: ext1 n
-- 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 : 0 < x.orderTop
⊢ (x • powers x).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ } =
    powers x - ofFinsupp (Finsupp.single 0 1)
have h : ∀ (a : ℕ),
  Eq (α := R⟦Γ⟧)
    (((x • powers x).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ } : (a : ℕ) → R⟦Γ⟧) a : R⟦Γ⟧)
    ((powers x - ofFinsupp (Finsupp.single 0 1) : (a : ℕ) → R⟦Γ⟧) a : R⟦Γ⟧)
Tactic: apply SummableFamily.ext
-- 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 : 0 < x.orderTop
⊢ (1 - x) * (powers x).hsum = 1
have rw : (powers x).hsum - (powers x - ofFinsupp (Finsupp.single 0 1)).hsum = 1
Tactic: rw [← hsum_smul, sub_smul 1 x (powers x), one_smul, hsum_sub, ←
    hsum_embDomain (x • powers x) ⟨Nat.succ, Nat.succ_injective⟩, embDomain_succ_smul_powers hx]
-- 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 y : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
oinv : Γ
hxo : oinv + x.order = 0
⊢ 1 - HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
have nth_rw : 1 -
    HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
      (HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)) =
  -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
Tactic: nth_rw 1 [hxy]
-- 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 y : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
oinv : Γ
hxo : oinv + x.order = 0
⊢ 1 -
      HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
        (HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
have rw : 1 -
    (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y +
      HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
        ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)) =
  -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
Tactic: rw [mul_add, single_mul_single, hr, hxo,
    sub_add_eq_sub_sub_swap, sub_eq_neg_self, sub_eq_zero_of_eq single_zero_one.symm]
-- 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 y : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
oinv : Γ
hxo : oinv + x.order = 0
rw :
  1 -
      (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y +
        HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
          ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
⊢ 1 -
      HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
        (HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
have rw₁ : 1 -
    HAdd.hAdd (β := R⟦Γ⟧) (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y)
      ((single (oinv + x.order) : (a : R) → R⟦Γ⟧) (r * x.leadingCoeff) : R⟦Γ⟧) =
  -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
Tactic: rw [mul_add, single_mul_single, hr, hxo,
    sub_add_eq_sub_sub_swap, sub_eq_neg_self, sub_eq_zero_of_eq single_zero_one.symm]
-- 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 y : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
oinv : Γ
hxo : oinv + x.order = 0
rw :
  1 -
      (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y +
        HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
          ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
rw₁ :
  1 -
      HAdd.hAdd (β := R⟦Γ⟧) (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y)
        ((single (oinv + x.order) : (a : R) → R⟦Γ⟧) (r * x.leadingCoeff) : R⟦Γ⟧) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
⊢ 1 -
      HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
        (HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
have rw₂ : 1 - (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y + (single (oinv + x.order) : (a : R) → R⟦Γ⟧) 1) =
  -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
Tactic: rw [mul_add, single_mul_single, hr, hxo,
    sub_add_eq_sub_sub_swap, sub_eq_neg_self, sub_eq_zero_of_eq single_zero_one.symm]
-- 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 y : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
oinv : Γ
hxo : oinv + x.order = 0
rw :
  1 -
      (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y +
        HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
          ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
rw₁ :
  1 -
      HAdd.hAdd (β := R⟦Γ⟧) (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y)
        ((single (oinv + x.order) : (a : R) → R⟦Γ⟧) (r * x.leadingCoeff) : R⟦Γ⟧) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
rw₂ :
  1 -
      (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y +
        (single (oinv + x.order) : (a : R) → R⟦Γ⟧) 1) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
⊢ 1 -
      HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
        (HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
have rw₃ : 1 - (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y + (single 0 : (a : R) → R⟦Γ⟧) 1) =
  -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
Tactic: rw [mul_add, single_mul_single, hr, hxo,
    sub_add_eq_sub_sub_swap, sub_eq_neg_self, sub_eq_zero_of_eq single_zero_one.symm]
-- 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 y : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
oinv : Γ
hxo : oinv + x.order = 0
rw :
  1 -
      (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y +
        HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
          ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
rw₁ :
  1 -
      HAdd.hAdd (β := R⟦Γ⟧) (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y)
        ((single (oinv + x.order) : (a : R) → R⟦Γ⟧) (r * x.leadingCoeff) : R⟦Γ⟧) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
rw₂ :
  1 -
      (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y +
        (single (oinv + x.order) : (a : R) → R⟦Γ⟧) 1) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
rw₃ :
  1 - (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y + (single 0 : (a : R) → R⟦Γ⟧) 1) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
⊢ 1 -
      HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
        (HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
have rw₄ : HSub.hSub (α := R⟦Γ⟧) 1 ((single 0 : (a : R) → R⟦Γ⟧) 1) -
    HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y =
  -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
Tactic: rw [mul_add, single_mul_single, hr, hxo,
    sub_add_eq_sub_sub_swap, sub_eq_neg_self, sub_eq_zero_of_eq single_zero_one.symm]
-- 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 y : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
oinv : Γ
hxo : oinv + x.order = 0
rw :
  1 -
      (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y +
        HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
          ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
rw₁ :
  1 -
      HAdd.hAdd (β := R⟦Γ⟧) (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y)
        ((single (oinv + x.order) : (a : R) → R⟦Γ⟧) (r * x.leadingCoeff) : R⟦Γ⟧) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
rw₂ :
  1 -
      (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y +
        (single (oinv + x.order) : (a : R) → R⟦Γ⟧) 1) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
rw₃ :
  1 - (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y + (single 0 : (a : R) → R⟦Γ⟧) 1) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
rw₄ :
  HSub.hSub (α := R⟦Γ⟧) 1 ((single 0 : (a : R) → R⟦Γ⟧) 1) -
      HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
⊢ 1 -
      HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
        (HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
have rw₅ : HSub.hSub (α := R⟦Γ⟧) 1 ((single 0 : (a : R) → R⟦Γ⟧) 1) = 0
Tactic: rw [mul_add, single_mul_single, hr, hxo,
    sub_add_eq_sub_sub_swap, sub_eq_neg_self, sub_eq_zero_of_eq single_zero_one.symm]
-- 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 y : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
hxy : x = HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)
oinv : Γ
hxo : oinv + x.order = 0
rw :
  1 -
      (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y +
        HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
          ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
rw₁ :
  1 -
      HAdd.hAdd (β := R⟦Γ⟧) (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y)
        ((single (oinv + x.order) : (a : R) → R⟦Γ⟧) (r * x.leadingCoeff) : R⟦Γ⟧) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
rw₂ :
  1 -
      (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y +
        (single (oinv + x.order) : (a : R) → R⟦Γ⟧) 1) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
rw₃ :
  1 - (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y + (single 0 : (a : R) → R⟦Γ⟧) 1) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
rw₄ :
  HSub.hSub (α := R⟦Γ⟧) 1 ((single 0 : (a : R) → R⟦Γ⟧) 1) -
      HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
rw₅ : HSub.hSub (α := R⟦Γ⟧) 1 ((single 0 : (a : R) → R⟦Γ⟧) 1) = 0
⊢ 1 -
      HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
        (HAdd.hAdd (β := R⟦Γ⟧) y ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧)) =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y
have rw₆ : Eq (α := R⟦Γ⟧) 0 0
Tactic: rw [mul_add, single_mul_single, hr, hxo,
    sub_add_eq_sub_sub_swap, sub_eq_neg_self, sub_eq_zero_of_eq single_zero_one.symm]
-- 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⟦Γ⟧)
⊢ 0 < (1 - HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).orderTop
have pos : ∀ (hy : y = 0), 0 < (1 - HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).orderTop
Tactic: by_cases hy : y = 0
-- 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⟦Γ⟧)
pos : ∀ (hy : y = 0), 0 < (1 - HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).orderTop
⊢ 0 < (1 - HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).orderTop
have neg : ∀ (hy : ¬y = 0), 0 < (1 - HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).orderTop
Tactic: by_cases hy : y = 0
-- 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
⊢ HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x = 1
have rw : HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
    ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧) =
  1
Tactic: rw [eq_of_sub_eq_zero hy, single_mul_single, hxo, hr, single_zero_one]
-- 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
rw :
  HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
      ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧) =
    1
⊢ HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x = 1
have rw₁ : Eq (α := R⟦Γ⟧) ((single (oinv + x.order) : (a : R) → R⟦Γ⟧) (r * x.leadingCoeff) : R⟦Γ⟧) (1 : R⟦Γ⟧)
Tactic: rw [eq_of_sub_eq_zero hy, single_mul_single, hxo, hr, single_zero_one]
-- 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
rw :
  HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
      ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧) =
    1
rw₁ : Eq (α := R⟦Γ⟧) ((single (oinv + x.order) : (a : R) → R⟦Γ⟧) (r * x.leadingCoeff) : R⟦Γ⟧) (1 : R⟦Γ⟧)
⊢ HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x = 1
have rw₂ : Eq (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) (r * x.leadingCoeff) : R⟦Γ⟧) (1 : R⟦Γ⟧)
Tactic: rw [eq_of_sub_eq_zero hy, single_mul_single, hxo, hr, single_zero_one]
-- 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
rw :
  HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
      ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧) =
    1
rw₁ : Eq (α := R⟦Γ⟧) ((single (oinv + x.order) : (a : R) → R⟦Γ⟧) (r * x.leadingCoeff) : R⟦Γ⟧) (1 : R⟦Γ⟧)
rw₂ : Eq (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) (r * x.leadingCoeff) : R⟦Γ⟧) (1 : R⟦Γ⟧)
⊢ HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x = 1
have rw₃ : Eq (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) 1) 1
Tactic: rw [eq_of_sub_eq_zero hy, single_mul_single, hxo, hr, single_zero_one]
-- 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
rw :
  HMul.hMul (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
      ((single x.order : (a : R) → R⟦Γ⟧) x.leadingCoeff : R⟦Γ⟧) =
    1
rw₁ : Eq (α := R⟦Γ⟧) ((single (oinv + x.order) : (a : R) → R⟦Γ⟧) (r * x.leadingCoeff) : R⟦Γ⟧) (1 : R⟦Γ⟧)
rw₂ : Eq (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) (r * x.leadingCoeff) : R⟦Γ⟧) (1 : R⟦Γ⟧)
rw₃ : Eq (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) 1) 1
⊢ HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x = 1
have rw₄ : Eq (α := R⟦Γ⟧) 1 1
Tactic: rw [eq_of_sub_eq_zero hy, single_mul_single, hxo, hr, single_zero_one]
-- 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 hrx : HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x = 1
Tactic: have hrx : (single oinv) r * x = 1 := by
      rw [eq_of_sub_eq_zero hy, single_mul_single, hxo, hr, single_zero_one]