-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem pow_finite_co_support {x : HahnSeries Γ R} (hx : 0 < x.orderTop) (g : Γ) :
    Set.Finite {a | ((fun n ↦ x ^ n) a).coeff g ≠ 0}

Proof state:
case pos.refine_2.succ.intro.intro.intro.intro
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
n : ℕ
i : Γ
hi : i ∈ (npowRec n x).support
j : Γ
hj : j ∈ x.support
ys : (fun x1 x2 => x1 + x2) i j ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < (fun x1 x2 => x1 + x2) i j → {a | ((fun n => x ^ n) a).coeff z ≠ 0}.Finite
hn : n + 1 ∈ {a | ((fun n => x ^ n) a).coeff ((fun x1 x2 => x1 + x2) i j) ≠ 0}
⊢ n + 1 ∈
    (Nat.succ ''
        ⋃ i_1 ∈ ↑(addAntidiagonal ⋯ hpwo ((fun x1 x2 => x1 + x2) i j)), {a | ((fun n => x ^ n) a).coeff i_1.2 ≠ 0}) ∪
      {0}

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

Result:
case pos.refine_2.succ.intro.intro.intro.intro
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
n : ℕ
i : Γ
hi : i ∈ (npowRec n x).support
j : Γ
hj : j ∈ x.support
ys : (fun x1 x2 => x1 + x2) i j ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < (fun x1 x2 => x1 + x2) i j → {a | ((fun n => x ^ n) a).coeff z ≠ 0}.Finite
hn : n + 1 ∈ {a | ((fun n => x ^ n) a).coeff ((fun x1 x2 => x1 + x2) i j) ≠ 0}
⊢ (j, i) ∈ ↑(addAntidiagonal ⋯ hpwo ((fun x1 x2 => x1 + x2) i j))

Proof state:
case pos.refine_2.succ.intro.intro.intro.intro
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
n : ℕ
i : Γ
hi : i ∈ (npowRec n x).support
j : Γ
hj : j ∈ x.support
ys : (fun x1 x2 => x1 + x2) i j ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < (fun x1 x2 => x1 + x2) i j → {a | ((fun n => x ^ n) a).coeff z ≠ 0}.Finite
hn : n + 1 ∈ {a | ((fun n => x ^ n) a).coeff ((fun x1 x2 => x1 + x2) i j) ≠ 0}
⊢ ¬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⟩

Result:
no goals

Proof state:
case pos.refine_1
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
y : Γ
ys : y ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < y → {a | ((fun n => x ^ n) a).coeff z ≠ 0}.Finite
ij : Γ × Γ
hij : ij ∈ ↑(addAntidiagonal ⋯ hpwo y)
⊢ ij.2 < y

Tactic:
obtain ⟨hi, _, rfl⟩ := mem_addAntidiagonal.1 (mem_coe.1 hij)

Result:
case pos.refine_1.intro.intro
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
ij : Γ × Γ
hi : ij.1 ∈ x.support
left✝ : ij.2 ∈ ⋃ n, (x ^ n).support
ys : ij.1 + ij.2 ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < ij.1 + ij.2 → {a | ((fun n => x ^ n) a).coeff z ≠ 0}.Finite
hij : ij ∈ ↑(addAntidiagonal ⋯ hpwo (ij.1 + ij.2))
⊢ ij.2 < ij.1 + ij.2

Proof state:
case pos.refine_2
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
y : Γ
ys : y ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < y → {a | ((fun n => x ^ n) a).coeff z ≠ 0}.Finite
⊢ {a | ((fun n => x ^ n) a).coeff y ≠ 0} ⊆
    (Nat.succ '' ⋃ i ∈ ↑(addAntidiagonal ⋯ hpwo y), {a | ((fun n => x ^ n) a).coeff i.2 ≠ 0}) ∪ {0}

Tactic:
rintro (_ | n) hn

Result:
case pos.refine_2.zero
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
y : Γ
ys : y ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < y → {a | ((fun n => x ^ n) a).coeff z ≠ 0}.Finite
hn : 0 ∈ {a | ((fun n => x ^ n) a).coeff y ≠ 0}
⊢ 0 ∈ (Nat.succ '' ⋃ i ∈ ↑(addAntidiagonal ⋯ hpwo y), {a | ((fun n => x ^ n) a).coeff i.2 ≠ 0}) ∪ {0}

case pos.refine_2.succ
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
y : Γ
ys : y ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < y → {a | ((fun n => x ^ n) a).coeff z ≠ 0}.Finite
n : ℕ
hn : n + 1 ∈ {a | ((fun n => x ^ n) a).coeff y ≠ 0}
⊢ n + 1 ∈ (Nat.succ '' ⋃ i ∈ ↑(addAntidiagonal ⋯ hpwo y), {a | ((fun n => x ^ n) a).coeff i.2 ≠ 0}) ∪ {0}

Proof state:
case pos.refine_2.succ
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
y : Γ
ys : y ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < y → {a | ((fun n => x ^ n) a).coeff z ≠ 0}.Finite
n : ℕ
hn : n + 1 ∈ {a | ((fun n => x ^ n) a).coeff y ≠ 0}
⊢ n + 1 ∈ (Nat.succ '' ⋃ i ∈ ↑(addAntidiagonal ⋯ hpwo y), {a | ((fun n => x ^ n) a).coeff i.2 ≠ 0}) ∪ {0}

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

Result:
case pos.refine_2.succ.intro.intro.intro.intro
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
n : ℕ
i : Γ
hi : i ∈ (npowRec n x).support
j : Γ
hj : j ∈ x.support
ys : (fun x1 x2 => x1 + x2) i j ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < (fun x1 x2 => x1 + x2) i j → {a | ((fun n => x ^ n) a).coeff z ≠ 0}.Finite
hn : n + 1 ∈ {a | ((fun n => x ^ n) a).coeff ((fun x1 x2 => x1 + x2) i j) ≠ 0}
⊢ n + 1 ∈
    (Nat.succ ''
        ⋃ i_1 ∈ ↑(addAntidiagonal ⋯ hpwo ((fun x1 x2 => x1 + x2) i j)), {a | ((fun n => x ^ n) a).coeff i_1.2 ≠ 0}) ∪
      {0}

Proof state:
case pos
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
⊢ {a | ((fun n => x ^ n) a).coeff g ≠ 0}.Finite

Tactic:
apply hpwo.isWF.induction hg

Result:
case pos
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
⊢ ∀ y ∈ ⋃ n, (x ^ n).support,
    (∀ z ∈ ⋃ n, (x ^ n).support, z < y → {a | ((fun n => x ^ n) a).coeff z ≠ 0}.Finite) →
      {a | ((fun n => x ^ n) a).coeff y ≠ 0}.Finite