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
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
g : Γ
⊢ (s.embDomain f).hsum.coeff g = s.hsum.coeff g
have coeff : Eq.{u_3 + 1} (α := R)
  (∑ᶠ (i : β),
    if h : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) i then
      HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = i) sorry)) g
    else 0)
  (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
Tactic: simp only [coeff_hsum, embDomain_apply, apply_dite HahnSeries.coeff, dite_apply, coeff_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
⊢ (s.embDomain f).hsum = s.hsum
have coeff : ∀ (g : Γ), (s.embDomain f).hsum.coeff g = s.hsum.coeff g
Tactic: classical
  ext g
  simp only [coeff_hsum, embDomain_apply, apply_dite HahnSeries.coeff, dite_apply, coeff_zero]
  exact finsum_emb_domain f fun a => (s a).coeff g
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
coeff : ∀ (g : Γ), (s.embDomain f).hsum.coeff g = s.hsum.coeff g
⊢ (s.embDomain f).hsum = s.hsum
have coeff₁ : ∀ (g : Γ),
  Eq.{u_3 + 1} (α := R)
    (∑ᶠ (i : β),
      if h : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) i then
        HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = i) sorry)) g
      else 0)
    (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
Tactic: classical
  ext g
  simp only [coeff_hsum, embDomain_apply, apply_dite HahnSeries.coeff, dite_apply, coeff_zero]
  exact finsum_emb_domain f fun a => (s a).coeff g
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
g : Γ
hn : g ∈ (HPow.hPow (β := ℕ) x 0).support
⊢ g ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)
have hn₁ : g = 0 ∧ ¬Eq.{u_3 + 1} (α := R) 1 0
Tactic: simp only [pow_zero, mem_support, coeff_one, ne_eq, ite_eq_right_iff, Classical.not_imp] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
g : Γ
hn : g = 0 ∧ ¬Eq.{u_3 + 1} (α := R) 1 0
⊢ g ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)
have zero : Membership.mem (γ := AddSubmonoid Γ) (AddSubmonoid.closure x.support) 0
Tactic: simp only [hn, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : ∀ ⦃g : Γ⦄ (hn : g ∈ (x ^ n).support), g ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)
g : Γ
hn : g ∈ (x ^ (n + 1)).support
⊢ g ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)
have succ : ∀ (i : Γ) (hi : i ∈ (npowRec n x).support) (j : Γ) (hj : j ∈ x.support)
  (hn : (fun (x1 x2 : Γ) ↦ x1 + x2) i j ∈ (x ^ (n + 1)).support),
  (fun (x1 x2 : Γ) ↦ x1 + x2) i j ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)
Tactic: obtain ⟨i, hi, j, hj, rfl⟩ := support_mul_subset hn
Cleared hypotheses: g, hn
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
n : ℕ
g : Γ
hn : g ∈ (x ^ n).support
⊢ g ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)
have zero : ∀ ⦃g : Γ⦄ (hn : g ∈ (HPow.hPow (β := ℕ) x 0).support), g ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)
Tactic: induction n generalizing g with
  | zero =>
    simp only [pow_zero, mem_support, coeff_one, ne_eq, ite_eq_right_iff, Classical.not_imp] at hn
    simp only [hn, SetLike.mem_coe]
    exact AddSubmonoid.zero_mem _
  | succ n ih =>
    obtain ⟨i, hi, j, hj, rfl⟩ := support_mul_subset hn
    exact SetLike.mem_coe.2 (AddSubmonoid.add_mem _ (ih hi) (AddSubmonoid.subset_closure hj))
Cleared hypotheses: n, g, hn
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
n : ℕ
g : Γ
hn : g ∈ (x ^ n).support
zero : ∀ ⦃g : Γ⦄ (hn : g ∈ (HPow.hPow (β := ℕ) x 0).support), g ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)
⊢ g ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)
have succ : ∀ (n : ℕ) (ih : ∀ ⦃g : Γ⦄ (hn : g ∈ (x ^ n).support), g ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)) ⦃g : Γ⦄
  (hn : g ∈ (x ^ (n + 1)).support), g ∈ (↑(AddSubmonoid.closure x.support) : Set Γ)
Tactic: induction n generalizing g with
  | zero =>
    simp only [pow_zero, mem_support, coeff_one, ne_eq, ite_eq_right_iff, Classical.not_imp] at hn
    simp only [hn, SetLike.mem_coe]
    exact AddSubmonoid.zero_mem _
  | succ n ih =>
    obtain ⟨i, hi, j, hj, rfl⟩ := support_mul_subset hn
    exact SetLike.mem_coe.2 (AddSubmonoid.add_mem _ (ih hi) (AddSubmonoid.subset_closure hj))
Cleared hypotheses: n, g, hn
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
g : Γ
n : ℕ
hn : ¬(HPow.hPow (α := R⟦Γ⟧) 0 n).coeff g = 0
⊢ n = 0
have by_contra : ∀ (h' : ¬n = 0), False
Tactic: by_contra 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 : 0 < x.orderTop
g : Γ
⊢ Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}
have hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
Tactic: have hpwo : Set.IsPWO (⋃ n, support (x ^ n)) :=
    isPWO_iUnion_support_powers (zero_le_orderTop_iff.mp <| le_of_lt 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 : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
⊢ Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}
have pos : ∀ (h0 : x = 0), Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}
Tactic: by_cases h0 : x = 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
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
pos :
  ∀ (h0 : x = 0), Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}
⊢ Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}
have neg : ∀ (h0 : ¬x = 0), Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}
Tactic: by_cases h0 : x = 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
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
h0 : ¬x = 0
⊢ Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}
have pos : ∀ (hg : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), {g : Γ | (x ^ n).coeff g ≠ 0}) g),
  Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}
Tactic: by_cases hg : g ∈ ⋃ n : ℕ, { g | (x ^ n).coeff g ≠ 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
g : Γ
hpwo : Set.IsPWO.{u_1} (α := Γ) (⋃ (n : ℕ), (x ^ n).support)
h0 : ¬x = 0
pos :
  ∀ (hg : Membership.mem (γ := Set Γ) (⋃ (n : ℕ), {g : Γ | (x ^ n).coeff g ≠ 0}) g),
    Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}
⊢ Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}
have neg : ∀ (hg : g ∉ ⋃ (n : ℕ), {g : Γ | (x ^ n).coeff g ≠ 0}),
  Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}
Tactic: by_cases hg : g ∈ ⋃ n : ℕ, { g | (x ^ n).coeff g ≠ 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
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
⊢ Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) g) 0}
have pos : ∀ (y : Γ),
  Membership.mem (γ := Set Γ) (⋃ (n : ℕ), (x ^ n).support) y →
    (∀ (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}) →
      Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) y) 0}
Tactic: apply hpwo.isWF.induction hg
-- 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
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}
⊢ Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) y) 0}
have pos : ∀ (ij : Γ × Γ)
  (hij : ij ∈ (↑(addAntidiagonal (s := x.support) (t := ⋃ (n : ℕ), (x ^ n).support) sorry hpwo y) : Set (Γ × Γ))), ij.2 < y
Tactic: refine ((((addAntidiagonal x.isPWO_support hpwo y).finite_toSet.biUnion
    fun ij hij => hy ij.snd (mem_addAntidiagonal.1 (mem_coe.1 hij)).2.1 ?_).image Nat.succ).union
      (Set.finite_singleton 0)).subset ?_
-- 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
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}
pos :
  ∀ (ij : Γ × Γ)
    (hij : ij ∈ (↑(addAntidiagonal (s := x.support) (t := ⋃ (n : ℕ), (x ^ n).support) ⋯ hpwo y) : Set (Γ × Γ))),
    ij.2 < y
⊢ Set.Finite (α := ℕ) {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) y) 0}
have pos₁ : {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) y) 0} ⊆
  (Nat.succ ''
      ⋃ i ∈ (↑(addAntidiagonal (s := x.support) (t := ⋃ (n : ℕ), (x ^ n).support) sorry hpwo y) : Set (Γ × Γ)),
        {a : ℕ | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((fun (n : ℕ) ↦ x ^ n) a) i.2) 0}) ∪
    {0}
Tactic: refine ((((addAntidiagonal x.isPWO_support hpwo y).finite_toSet.biUnion
    fun ij hij => hy ij.snd (mem_addAntidiagonal.1 (mem_coe.1 hij)).2.1 ?_).image Nat.succ).union
      (Set.finite_singleton 0)).subset ?_
-- 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
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}
ij : Γ × Γ
hij : ij ∈ (↑(addAntidiagonal (s := x.support) (t := ⋃ (n : ℕ), (x ^ n).support) ⋯ hpwo y) : Set (Γ × Γ))
⊢ ij.2 < y
have pos : ∀ (hi : ij.1 ∈ x.support),
  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) sorry hpwo (ij.1 + ij.2)) : Set (Γ × Γ))),
      ij.2 < ij.1 + ij.2
Tactic: obtain ⟨hi, _, rfl⟩ := mem_addAntidiagonal.1 (mem_coe.1 hij)
Cleared hypotheses: y, ys, hy, hij
-- 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
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)
⊢ 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}
have 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) sorry 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: obtain ⟨i, hi, j, hj, rfl⟩ := support_mul_subset hn
Cleared hypotheses: y, ys, hy, hn
-- 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
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}
have pos : (j, i) ∈
  (↑(addAntidiagonal (s := x.support) (t := ⋃ (n : ℕ), (x ^ n).support) sorry hpwo ((fun (x1 x2 : Γ) ↦ x1 + x2) i j)) :
    Set (Γ × Γ))
Tactic: refine Set.mem_union_left _ ⟨n, Set.mem_iUnion.2 ⟨⟨j, i⟩, Set.mem_iUnion.2 ⟨?_, hi⟩⟩, rfl⟩
-- 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
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)
⊢ (j, i) ∈
    (↑(addAntidiagonal (s := x.support) (t := ⋃ (n : ℕ), (x ^ n).support) ⋯ hpwo ((fun (x1 x2 : Γ) ↦ x1 + x2) i j)) :
      Set (Γ × Γ))
have pos : ¬x.coeff j = 0 ∧ (∃ (i_1 : ℕ), ¬(x ^ i_1).coeff i = 0) ∧ j + i = i + j
Tactic: simp only [mem_coe, mem_addAntidiagonal, mem_support, ne_eq, Set.mem_iUnion]
-- 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 : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ℕ), ((if 0 < x.orderTop then x else 0) ^ a).support)
have pos : ∀ (h : 0 < x.orderTop), Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ℕ), ((if 0 < x.orderTop then x else 0) ^ a).support)
Tactic: by_cases h : 0 < x.orderTop
-- 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 : 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)
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ℕ), ((if 0 < x.orderTop then x else 0) ^ a).support)
have neg : ∀ (h : ¬0 < x.orderTop), Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ℕ), ((if 0 < x.orderTop then x else 0) ^ a).support)
Tactic: by_cases h : 0 < x.orderTop
-- 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 : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : 0 < x.orderTop
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ℕ), ((if 0 < x.orderTop then x else 0) ^ a).support)
have pos : Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ℕ), (x ^ a).support)
Tactic: simp only [h, ↓reduceIte]
-- 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 : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : ¬0 < x.orderTop
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ℕ), ((if 0 < x.orderTop then x else 0) ^ a).support)
have neg : Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ℕ), (HPow.hPow (α := R⟦Γ⟧) 0 a).support)
Tactic: simp only [h, ↓reduceIte]
-- 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 : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : ¬0 < x.orderTop
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : ℕ), (HPow.hPow (α := R⟦Γ⟧) 0 a).support)
have neg : LE.le.{u_1} (α := Γ) 0 (order.{u_1, u_3} (R := R) 0)
Tactic: apply isPWO_iUnion_support_powers
-- 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 : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : ¬0 < x.orderTop
⊢ LE.le.{u_1} (α := Γ) 0 (order.{u_1, u_3} (R := R) 0)
have neg : LE.le.{u_1} (α := Γ) 0 0
Tactic: rw [order_zero]
-- 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 : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
g : Γ
⊢ Set.Finite (α := ℕ) {a : ℕ | ((if 0 < x.orderTop then x else 0) ^ a).coeff g ≠ 0}
have pos : ∀ (h : 0 < x.orderTop), Set.Finite (α := ℕ) {a : ℕ | ((if 0 < x.orderTop then x else 0) ^ a).coeff g ≠ 0}
Tactic: by_cases h : 0 < x.orderTop
-- 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 : 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}
⊢ Set.Finite (α := ℕ) {a : ℕ | ((if 0 < x.orderTop then x else 0) ^ a).coeff g ≠ 0}
have neg : ∀ (h : ¬0 < x.orderTop), Set.Finite (α := ℕ) {a : ℕ | ((if 0 < x.orderTop then x else 0) ^ a).coeff g ≠ 0}
Tactic: by_cases h : 0 < x.orderTop
-- 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 : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
g : Γ
h : 0 < x.orderTop
⊢ Set.Finite (α := ℕ) {a : ℕ | ((if 0 < x.orderTop then x else 0) ^ a).coeff g ≠ 0}
have pos : Set.Finite (α := ℕ) {a : ℕ | (x ^ a).coeff g ≠ 0}
Tactic: simp only [h, ↓reduceIte]
-- 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 : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
g : Γ
h : ¬0 < x.orderTop
⊢ Set.Finite (α := ℕ) {a : ℕ | ((if 0 < x.orderTop then x else 0) ^ a).coeff g ≠ 0}
have neg : Set.Finite (α := ℕ) {a : ℕ | (HPow.hPow (α := R⟦Γ⟧) 0 a).coeff g ≠ 0}
Tactic: simp only [h, ↓reduceIte]