awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
h₁ : ∀ (ha : n ≠ 0), (HPow.hPow (α := R⟦Γ⟧) 0 n).coeff x = HahnSeries.coeff ((single 0 1 : (a : ℕ) → R⟦Γ⟧) n) x
⊢ (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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : Γ
⊢ (HPow.hPow (α := R⟦Γ⟧) (β := ℕ) 0 0).coeff x = HahnSeries.coeff ((single 0 1 : (a : ℕ) → R⟦Γ⟧) 0) x

Tactic:
simp [*]
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
n : ℕ
x : Γ
ha : n ≠ 0
⊢ (HPow.hPow (α := R⟦Γ⟧) 0 n).coeff x = HahnSeries.coeff ((single 0 1 : (a : ℕ) → R⟦Γ⟧) n) x

Tactic:
simp [*]
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
h : ∀ (n : ℕ), (powers x : (a : ℕ) → R⟦Γ⟧) n = x ^ n
⊢ Eq (α := (a : ℕ) → R⟦Γ⟧) (⇑(powers x) : (a : ℕ) → R⟦Γ⟧) (HPow.hPow x)

Tactic:
ext1 n
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
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⟦Γ⟧)
⊢ (x • powers x).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ } =
    powers x - ofFinsupp (Finsupp.single 0 1)

Tactic:
apply SummableFamily.ext

Premises used: HahnSeries.SummableFamily.ext
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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 (α := R⟦Γ⟧)
    (((x • powers x).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ } : (a : ℕ) → R⟦Γ⟧) 0 : R⟦Γ⟧)
    ((powers x - ofFinsupp (Finsupp.single 0 1) : (a : ℕ) → R⟦Γ⟧) 0 : R⟦Γ⟧)

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
n : ℕ
⊢ Eq (α := R⟦Γ⟧)
    (((x • powers x).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ } : (a : ℕ) → R⟦Γ⟧) (n + 1) :
      R⟦Γ⟧)
    ((powers x - ofFinsupp (Finsupp.single 0 1) : (a : ℕ) → R⟦Γ⟧) (n + 1) : R⟦Γ⟧)

Tactic:
simp [embDomain_apply, of_symm_smul_of_eq_mul, powers_of_orderTop_pos hx, pow_succ',
      -smul_eq_mul]

Premises used: HahnSeries.SummableFamily.embDomain_apply, HahnSeries.of_symm_smul_of_eq_mul, smul_eq_mul, HahnSeries.SummableFamily.powers_of_orderTop_pos, pow_succ'
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
rw : (powers x).hsum - (powers x - ofFinsupp (Finsupp.single 0 1)).hsum = 1
⊢ (1 - x) * (powers x).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]

Premises used: sub_smul, Function.Embedding.mk, HahnSeries.SummableFamily.embDomain_succ_smul_powers, HahnSeries.SummableFamily.hsum_embDomain, one_smul, Nat.succ_injective, HahnSeries.SummableFamily.hsum_smul, HSMul.hSMul, OfNat.ofNat, HahnSeries.SummableFamily.powers, Nat.succ, HahnSeries.SummableFamily.hsum_sub
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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).hsum - (powers x - ofFinsupp (Finsupp.single 0 1)).hsum = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
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
⊢ 1 - HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x =
    -HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y

Tactic:
nth_rw 1 [hxy]
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
rw₆ rw₇ : Eq (α := R⟦Γ⟧) 0 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

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]

Premises used: HahnSeries.single_mul_single, sub_eq_zero_of_eq, HahnSeries.single_zero_one, sub_eq_neg_self, mul_add, Eq.symm, sub_add_eq_sub_sub_swap
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
neg : ∀ (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

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
rw₄ rw₅ : Eq (α := R⟦Γ⟧) 1 1
⊢ HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x = 1

Tactic:
rw [eq_of_sub_eq_zero hy, single_mul_single, hxo, hr, single_zero_one]

Premises used: HahnSeries.single_mul_single, eq_of_sub_eq_zero, HahnSeries.single_zero_one
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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

Tactic:
have hrx : (single oinv) r * x = 1 := by
      rw [eq_of_sub_eq_zero hy, single_mul_single, hxo, hr, single_zero_one]
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
hrx : HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x = 1
⊢ 0 < (1 - HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).orderTop

Tactic:
simp only [hrx, sub_self, orderTop_zero, WithTop.top_pos]

Premises used: sub_self, WithTop.top_pos, HahnSeries.orderTop_zero
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
⊢ IsRegular r

Tactic:
have hr' : IsRegular r := IsUnit.isRegular <| .of_mul_eq_one x.leadingCoeff hr
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
rw : 0 < oinv + y.order
⊢ 0 < (HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) y).order

Tactic:
rw [(order_single_mul_of_isRegular hr' hy)]

Premises used: HahnSeries.order_single_mul_of_isRegular
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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

Tactic:
pos_of_lt_add_right (a := x.order) ?_

Premises used: pos_of_lt_add_right
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
refine : x.order < x.order + (oinv + y.order)
⊢ 0 < oinv + y.order

Tactic:
refine pos_of_lt_add_right (a := x.order) ?_

Premises used: pos_of_lt_add_right
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
rw : x.order < y.order
⊢ x.order < x.order + (oinv + y.order)

Tactic:
rw [← add_assoc, add_comm x.order, hxo, zero_add]

Premises used: HahnSeries.order, add_assoc, zero_add, add_comm
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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 < y.order

Tactic:
order_lt_order_of_eq_add_single (sub_add_cancel x _).symm hy

Premises used: HahnSeries.order_lt_order_of_eq_add_single, Eq.symm, sub_add_cancel
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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 < y.order

Tactic:
exact order_lt_order_of_eq_add_single (sub_add_cancel x _).symm hy

Premises used: HahnSeries.order_lt_order_of_eq_add_single, Eq.symm, sub_add_cancel
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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

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
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
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
⊢ 0 < (1 - HMul.hMul (α := R⟦Γ⟧) ((single oinv : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).orderTop

Tactic:
rw [one_minus_single_neg_mul hr (sub_add_cancel x _).symm _ hxo, orderTop_neg]

Premises used: HahnSeries.one_minus_single_neg_mul, HahnSeries.orderTop_neg, Eq.symm, sub_add_cancel
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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 <
    (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:
zero_lt_orderTop_of_order hy'

Premises used: HahnSeries.zero_lt_orderTop_of_order
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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 <
    (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:
exact zero_lt_orderTop_of_order hy'

Premises used: HahnSeries.zero_lt_orderTop_of_order
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
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
⊢ IsUnit x

Tactic:
let ⟨⟨u, i, ui, iu⟩, h⟩ := hx
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
⊢ u = x.leadingCoeff

Tactic:
rw [Units.val_mk] at h

Premises used: Units.val_mk
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
⊢ i * x.leadingCoeff = 1

Tactic:
rw [h] at iu
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
iu₁ : i * x.leadingCoeff = 1
⊢ u = x.leadingCoeff

Tactic:
rw [h] at iu
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
⊢ (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)
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
⊢ 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'

Premises used: sub_sub_cancel
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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' :
  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

Tactic:
isUnit_of_mul_isUnit_right (.of_mul_eq_one _ h')

Premises used: IsUnit.of_mul_eq_one, isUnit_of_mul_isUnit_right
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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' :
  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

Tactic:
exact isUnit_of_mul_isUnit_right (.of_mul_eq_one _ h')

Premises used: IsUnit.of_mul_eq_one, isUnit_of_mul_isUnit_right
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
inr : Nontrivial R → IsUnit x
⊢ IsUnit x

Tactic:
obtain _ | _ := subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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 : Subsingleton R
⊢ IsUnit x

Tactic:
isUnit_of_subsingleton x

Premises used: isUnit_of_subsingleton
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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 : Subsingleton R
⊢ IsUnit x

Tactic:
exact isUnit_of_subsingleton x

Premises used: isUnit_of_subsingleton
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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

Tactic:
isUnit_of_isUnit_leadingCoeff_AddUnitOrder ?_ ?_

Premises used: HahnSeries.isUnit_of_isUnit_leadingCoeff_AddUnitOrder
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
inr₁ : IsAddUnit x.order
⊢ IsUnit x

Tactic:
refine isUnit_of_isUnit_leadingCoeff_AddUnitOrder ?_ ?_

Premises used: HahnSeries.isUnit_of_isUnit_leadingCoeff_AddUnitOrder
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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.{u_3} (M := R) 1
⊢ IsUnit x.leadingCoeff

Tactic:
rw [(x.orderTop_self_sub_one_pos_iff.mp h).2]

Premises used: And.right, Iff.mp, HahnSeries.orderTop_self_sub_one_pos_iff