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
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
h0 : ¬x = 0
hg : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), {g : Γ | (x ^ n).coeff g ≠ 0}) g
ij : Γ × Γ
hi : ij.1 ∈ x.support
left : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) ij.2
ys : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) (ij.1 + ij.2)
hy :
  ∀ (z : Γ),
    Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) z →
      z < ij.1 + ij.2 →
        Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) z) 0}
hij : ij ∈ (↑(addAntidiagonal (s := x.support) (t := ⋃ (n : ℕ), (x ^ n).support) ⋯ hpwo (ij.1 + ij.2)) : Set (Γ × Γ))
⊢ ij.2 < ij.1 + ij.2

Tactic:
lt_add_of_pos_left ij.2 <| lt_of_lt_of_le ((zero_lt_orderTop_iff h0).mp hx) <|
      order_le_of_coeff_ne_zero <| Function.mem_support.mp hi

Premises used: HahnSeries.order_le_of_coeff_ne_zero, Iff.mp, Function.mem_support, lt_add_of_pos_left, HahnSeries.zero_lt_orderTop_iff, Prod.snd, lt_of_lt_of_le
-- 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
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
h0 : ¬x = 0
hg : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), {g : Γ | (x ^ n).coeff g ≠ 0}) g
ij : Γ × Γ
hi : ij.1 ∈ x.support
left : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) ij.2
ys : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) (ij.1 + ij.2)
hy :
  ∀ (z : Γ),
    Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) z →
      z < ij.1 + ij.2 →
        Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) z) 0}
hij : ij ∈ (↑(addAntidiagonal (s := x.support) (t := ⋃ (n : ℕ), (x ^ n).support) ⋯ hpwo (ij.1 + ij.2)) : Set (Γ × Γ))
⊢ ij.2 < ij.1 + ij.2

Tactic:
exact lt_add_of_pos_left ij.2 <| lt_of_lt_of_le ((zero_lt_orderTop_iff h0).mp hx) <|
      order_le_of_coeff_ne_zero <| Function.mem_support.mp hi

Premises used: HahnSeries.order_le_of_coeff_ne_zero, Iff.mp, Function.mem_support, lt_add_of_pos_left, HahnSeries.zero_lt_orderTop_iff, Prod.snd, lt_of_lt_of_le
-- 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
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
h0 : ¬x = 0
hg : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), {g : Γ | (x ^ n).coeff g ≠ 0}) g
y : Γ
ys : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) y
hy :
  ∀ (z : Γ),
    Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) z →
      z < y → Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) z) 0}
hn : Membership.mem (γ := Set ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) y) 0} 0
⊢ 0 ∈
    (Nat.succ ''
        ⋃ i ∈ (↑(addAntidiagonal (s := x.support) (t := ⋃ (n : ℕ), (x ^ n).support) ⋯ hpwo y) : Set (Γ × Γ)),
          {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) i.2) 0}) ∪
      {0}

Tactic:
Set.mem_union_right _ (Set.mem_singleton 0)

Premises used: Set.mem_singleton, Set.mem_union_right, OfNat.ofNat
-- 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
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
h0 : ¬x = 0
hg : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), {g : Γ | (x ^ n).coeff g ≠ 0}) g
y : Γ
ys : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) y
hy :
  ∀ (z : Γ),
    Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) z →
      z < y → Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) z) 0}
hn : Membership.mem (γ := Set ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) y) 0} 0
⊢ 0 ∈
    (Nat.succ ''
        ⋃ i ∈ (↑(addAntidiagonal (s := x.support) (t := ⋃ (n : ℕ), (x ^ n).support) ⋯ hpwo y) : Set (Γ × Γ)),
          {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) i.2) 0}) ∪
      {0}

Tactic:
exact Set.mem_union_right _ (Set.mem_singleton 0)

Premises used: Set.mem_singleton, Set.mem_union_right, OfNat.ofNat
-- 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
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
h0 : ¬x = 0
hg : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), {g : Γ | (x ^ n).coeff g ≠ 0}) g
y : Γ
ys : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) y
hy :
  ∀ (z : Γ),
    Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) z →
      z < y → Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) z) 0}
n : ℕ
hn :
  Membership.mem (γ := Set ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) y) 0} (n + 1)
pos :
  ∀ (i : Γ) (hi : i ∈ (npowRec n x).support) (j : Γ) (hj : j ∈ x.support)
    (ys : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) ((fun (x1 x2 : Γ) ↦ x1 + x2) i j))
    (hy :
      ∀ (z : Γ),
        Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) z →
          z < (fun (x1 x2 : Γ) ↦ x1 + x2) i j →
            Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) z) 0})
    (hn :
      Membership.mem (γ := Set ℕ)
        {a : ℕ |
          Ne.{u_3 + 1} (α := R)
            (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((fun (n : ℕ) ↦ x ^ n) a) ((fun (x1 x2 : Γ) ↦ x1 + x2) i j)) 0}
        (n + 1)),
    n + 1 ∈
      (Nat.succ ''
          ⋃
            i_1 ∈
              (↑(addAntidiagonal (s := x.support) (t := ⋃ (n : ℕ), (x ^ n).support) ⋯ hpwo
                    ((fun (x1 x2 : Γ) ↦ x1 + x2) i j)) :
                Set (Γ × Γ)),
            {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) i_1.2) 0}) ∪
        {0}
⊢ n + 1 ∈
    (Nat.succ ''
        ⋃ i ∈ (↑(addAntidiagonal (s := x.support) (t := ⋃ (n : ℕ), (x ^ n).support) ⋯ hpwo y) : Set (Γ × Γ)),
          {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) i.2) 0}) ∪
      {0}

Tactic:
obtain ⟨i, hi, j, hj, rfl⟩ := support_mul_subset hn

Premises used: HahnSeries.support_mul_subset, 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 : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
h0 : ¬x = 0
hg : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), {g : Γ | (x ^ n).coeff g ≠ 0}) g
n : ℕ
i : Γ
hi : i ∈ (npowRec n x).support
j : Γ
hj : j ∈ x.support
ys : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) ((fun (x1 x2 : Γ) ↦ x1 + x2) i j)
hy :
  ∀ (z : Γ),
    Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) z →
      z < (fun (x1 x2 : Γ) ↦ x1 + x2) i j →
        Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) z) 0}
hn :
  Membership.mem (γ := Set ℕ)
    {a : ℕ |
      Ne.{u_3 + 1} (α := R)
        (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((fun (n : ℕ) ↦ x ^ n) a) ((fun (x1 x2 : Γ) ↦ x1 + x2) i j)) 0}
    (n + 1)
⊢ n + 1 ∈
    (Nat.succ ''
        ⋃
          i_1 ∈
            (↑(addAntidiagonal (s := x.support) (t := ⋃ (n : ℕ), (x ^ n).support) ⋯ hpwo
                  ((fun (x1 x2 : Γ) ↦ x1 + x2) i j)) :
              Set (Γ × Γ)),
          {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) i_1.2) 0}) ∪
      {0}

Tactic:
Set.mem_union_left _ ⟨n, Set.mem_iUnion.2 ⟨⟨j, i⟩, Set.mem_iUnion.2 ⟨?_, hi⟩⟩, rfl⟩

Premises used: Iff.mpr, Set.mem_iUnion, Prod.mk, And.intro, Exists.intro, Set.mem_union_left, 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 : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
h0 : ¬x = 0
hg : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), {g : Γ | (x ^ n).coeff g ≠ 0}) g
n : ℕ
i : Γ
hi : i ∈ (npowRec n x).support
j : Γ
hj : j ∈ x.support
ys : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) ((fun (x1 x2 : Γ) ↦ x1 + x2) i j)
hy :
  ∀ (z : Γ),
    Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) z →
      z < (fun (x1 x2 : Γ) ↦ x1 + x2) i j →
        Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) z) 0}
hn :
  Membership.mem (γ := Set ℕ)
    {a : ℕ |
      Ne.{u_3 + 1} (α := R)
        (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((fun (n : ℕ) ↦ x ^ n) a) ((fun (x1 x2 : Γ) ↦ x1 + x2) i j)) 0}
    (n + 1)
pos :
  (j, i) ∈
    (↑(addAntidiagonal (s := x.support) (t := ⋃ (n : ℕ), (x ^ n).support) ⋯ hpwo ((fun (x1 x2 : Γ) ↦ x1 + x2) i j)) :
      Set (Γ × Γ))
⊢ n + 1 ∈
    (Nat.succ ''
        ⋃
          i_1 ∈
            (↑(addAntidiagonal (s := x.support) (t := ⋃ (n : ℕ), (x ^ n).support) ⋯ hpwo
                  ((fun (x1 x2 : Γ) ↦ x1 + x2) i j)) :
              Set (Γ × Γ)),
          {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) i_1.2) 0}) ∪
      {0}

Tactic:
refine Set.mem_union_left _ ⟨n, Set.mem_iUnion.2 ⟨⟨j, i⟩, Set.mem_iUnion.2 ⟨?_, hi⟩⟩, 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 : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
h0 : ¬x = 0
hg : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), {g : Γ | (x ^ n).coeff g ≠ 0}) g
n : ℕ
i : Γ
hi : i ∈ (npowRec n x).support
j : Γ
hj : j ∈ x.support
ys : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) ((fun (x1 x2 : Γ) ↦ x1 + x2) i j)
hy :
  ∀ (z : Γ),
    Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) z →
      z < (fun (x1 x2 : Γ) ↦ x1 + x2) i j →
        Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) z) 0}
hn :
  Membership.mem (γ := Set ℕ)
    {a : ℕ |
      Ne.{u_3 + 1} (α := R)
        (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((fun (n : ℕ) ↦ x ^ n) a) ((fun (x1 x2 : Γ) ↦ x1 + x2) i j)) 0}
    (n + 1)
pos : ¬x.coeff j = 0 ∧ (∃ (i_1 : ℕ), ¬(x ^ i_1).coeff i = 0) ∧ j + i = i + j
⊢ (j, i) ∈
    (↑(addAntidiagonal (s := x.support) (t := ⋃ (n : ℕ), (x ^ n).support) ⋯ hpwo ((fun (x1 x2 : Γ) ↦ x1 + x2) i j)) :
      Set (Γ × Γ))

Tactic:
simp only [mem_coe, mem_addAntidiagonal, mem_support, ne_eq, Set.mem_iUnion]

Premises used: Set.mem_iUnion, ne_eq, Finset.mem_coe, HahnSeries.mem_support, Finset.mem_addAntidiagonal
-- 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
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
h0 : ¬x = 0
hg : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), {g : Γ | (x ^ n).coeff g ≠ 0}) g
n : ℕ
i : Γ
hi : i ∈ (npowRec n x).support
j : Γ
hj : j ∈ x.support
ys : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) ((fun (x1 x2 : Γ) ↦ x1 + x2) i j)
hy :
  ∀ (z : Γ),
    Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) z →
      z < (fun (x1 x2 : Γ) ↦ x1 + x2) i j →
        Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) z) 0}
hn :
  Membership.mem (γ := Set ℕ)
    {a : ℕ |
      Ne.{u_3 + 1} (α := R)
        (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((fun (n : ℕ) ↦ x ^ n) a) ((fun (x1 x2 : Γ) ↦ x1 + x2) i j)) 0}
    (n + 1)
⊢ ¬x.coeff j = 0 ∧ (∃ (i_1 : ℕ), ¬(x ^ i_1).coeff i = 0) ∧ j + i = i + j

Tactic:
⟨hj, ⟨n, hi⟩, add_comm j i⟩

Premises used: add_comm, And.intro, Exists.intro
-- 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
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
h0 : ¬x = 0
hg : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), {g : Γ | (x ^ n).coeff g ≠ 0}) g
n : ℕ
i : Γ
hi : i ∈ (npowRec n x).support
j : Γ
hj : j ∈ x.support
ys : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) ((fun (x1 x2 : Γ) ↦ x1 + x2) i j)
hy :
  ∀ (z : Γ),
    Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) z →
      z < (fun (x1 x2 : Γ) ↦ x1 + x2) i j →
        Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) z) 0}
hn :
  Membership.mem (γ := Set ℕ)
    {a : ℕ |
      Ne.{u_3 + 1} (α := R)
        (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((fun (n : ℕ) ↦ x ^ n) a) ((fun (x1 x2 : Γ) ↦ x1 + x2) i j)) 0}
    (n + 1)
⊢ ¬x.coeff j = 0 ∧ (∃ (i_1 : ℕ), ¬(x ^ i_1).coeff i = 0) ∧ j + i = i + j

Tactic:
exact ⟨hj, ⟨n, hi⟩, add_comm j i⟩
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
pos : ∀ (h : 0 < x.orderTop), Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ℕ), ((if 0 < x.orderTop then x else 0) ^ a).support)
neg : ∀ (h : ¬0 < x.orderTop), Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ℕ), ((if 0 < x.orderTop then x else 0) ^ a).support)
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ℕ), ((if 0 < x.orderTop then x else 0) ^ a).support)

Tactic:
by_cases h : 0 < x.orderTop

Premises used: HahnSeries.orderTop
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : 0 < x.orderTop
pos : Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ℕ), (x ^ a).support)
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ℕ), ((if 0 < x.orderTop then x else 0) ^ a).support)

Tactic:
simp only [h, ↓reduceIte]

Premises used: reduceIte
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : 0 < x.orderTop
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ℕ), (x ^ a).support)

Tactic:
isPWO_iUnion_support_powers (zero_le_orderTop_iff.mp <| le_of_lt h)

Premises used: le_of_lt, HahnSeries.SummableFamily.isPWO_iUnion_support_powers, Iff.mp, HahnSeries.zero_le_orderTop_iff
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : 0 < x.orderTop
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ℕ), (x ^ a).support)

Tactic:
exact isPWO_iUnion_support_powers (zero_le_orderTop_iff.mp <| le_of_lt h)

Premises used: le_of_lt, HahnSeries.SummableFamily.isPWO_iUnion_support_powers, Iff.mp, HahnSeries.zero_le_orderTop_iff
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : ¬0 < x.orderTop
neg : Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ℕ), (HPow.hPow (α := R⟦Γ⟧) 0 a).support)
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ℕ), ((if 0 < x.orderTop then x else 0) ^ a).support)

Tactic:
simp only [h, ↓reduceIte]

Premises used: reduceIte
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : ¬0 < x.orderTop
neg : LE.le.{u_1} (α := Γ) 0 (order.{u_1, u_3} (R := R) 0)
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ℕ), (HPow.hPow (α := R⟦Γ⟧) 0 a).support)

Tactic:
apply isPWO_iUnion_support_powers

Premises used: HahnSeries.SummableFamily.isPWO_iUnion_support_powers
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : ¬0 < x.orderTop
neg neg₁ : LE.le.{u_1} (α := Γ) 0 0
⊢ LE.le.{u_1} (α := Γ) 0 (order.{u_1, u_3} (R := R) 0)

Tactic:
rw [order_zero]

Premises used: HahnSeries.order_zero
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
g : Γ
pos : ∀ (h : 0 < x.orderTop), Set.Finite (α := ℕ) {a : ℕ | ((if 0 < x.orderTop then x else 0) ^ a).coeff g ≠ 0}
neg : ∀ (h : ¬0 < x.orderTop), Set.Finite (α := ℕ) {a : ℕ | ((if 0 < x.orderTop then x else 0) ^ a).coeff g ≠ 0}
⊢ Set.Finite (α := ℕ) {a : ℕ | ((if 0 < x.orderTop then x else 0) ^ a).coeff g ≠ 0}

Tactic:
by_cases h : 0 < x.orderTop

Premises used: HahnSeries.orderTop
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
g : Γ
h : 0 < x.orderTop
pos : Set.Finite (α := ℕ) {a : ℕ | (x ^ a).coeff g ≠ 0}
⊢ Set.Finite (α := ℕ) {a : ℕ | ((if 0 < x.orderTop then x else 0) ^ a).coeff g ≠ 0}

Tactic:
simp only [h, ↓reduceIte]

Premises used: reduceIte
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
g : Γ
h : 0 < x.orderTop
⊢ Set.Finite (α := ℕ) {a : ℕ | (x ^ a).coeff g ≠ 0}

Tactic:
pow_finite_co_support h g

Premises used: setOf, HahnSeries.SummableFamily.pow_finite_co_support
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
g : Γ
h : 0 < x.orderTop
⊢ Set.Finite (α := ℕ) {a : ℕ | (x ^ a).coeff g ≠ 0}

Tactic:
exact pow_finite_co_support h g

Premises used: HahnSeries.SummableFamily.pow_finite_co_support
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
g : Γ
h : ¬0 < x.orderTop
neg : Set.Finite (α := ℕ) {a : ℕ | (HPow.hPow (α := R⟦Γ⟧) 0 a).coeff g ≠ 0}
⊢ Set.Finite (α := ℕ) {a : ℕ | ((if 0 < x.orderTop then x else 0) ^ a).coeff g ≠ 0}

Tactic:
simp only [h, ↓reduceIte]

Premises used: reduceIte
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
g : Γ
h : ¬0 < x.orderTop
⊢ Set.Finite (α := ℕ) {a : ℕ | (HPow.hPow (α := R⟦Γ⟧) 0 a).coeff g ≠ 0}

Tactic:
pow_finite_co_support (orderTop_zero (R := R) (Γ := Γ) ▸ WithTop.top_pos) g

Premises used: setOf, HahnSeries.SummableFamily.pow_finite_co_support
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
g : Γ
h : ¬0 < x.orderTop
⊢ Set.Finite (α := ℕ) {a : ℕ | (HPow.hPow (α := R⟦Γ⟧) 0 a).coeff g ≠ 0}

Tactic:
exact pow_finite_co_support (orderTop_zero (R := R) (Γ := Γ) ▸ WithTop.top_pos) g

Premises used: HahnSeries.SummableFamily.pow_finite_co_support
-- 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 : ℕ
⊢ (powers x : (a : ℕ) → R⟦Γ⟧) n = x ^ n

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
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)
⊢ powers x = single 0 1

Tactic:
ext a
-- 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
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)
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)
⊢ 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

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 : R⟦Γ⟧
hx : ¬0 < x.orderTop
x_1 : Γ
⊢ Eq (α := R) (HahnSeries.coeff ((powers x : (a : ℕ) → R⟦Γ⟧) 0) x_1 : R)
    (HahnSeries.coeff ((single 0 1 : (a : ℕ) → R⟦Γ⟧) 0) x_1 : R)

Tactic:
simp [powers, *]

Premises used: HahnSeries.SummableFamily.powers
-- 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
a : ℕ
x_1 : Γ
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:
simp [powers, *]

Premises used: HahnSeries.SummableFamily.powers
-- 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
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)
⊢ Eq (α := SummableFamily Γ R ℕ) (powers 0) (single 0 1)

Tactic:
ext 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
n : ℕ
x : Γ
⊢ LT.lt.{u_1} (α := WithTop Γ) 0 (orderTop.{u_1, u_3} (R := R) 0)

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 : Γ
h : (HPow.hPow (α := R⟦Γ⟧) 0 n).coeff x = HahnSeries.coeff ((single 0 1 : (a : ℕ) → 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)

Tactic:
rw [powers_of_orderTop_pos (by simp)]

Premises used: HahnSeries.SummableFamily.powers_of_orderTop_pos