-- 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_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

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

Result:
no goals

Proof state:
case neg
Γ : 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:
exact Set.finite_empty.subset fun n hn => hg (Set.mem_iUnion.2 ⟨n, hn⟩)

Result:
no goals

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}
⊢ (j, i) ∈ ↑(addAntidiagonal ⋯ hpwo ((fun x1 x2 => x1 + x2) i j))

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

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}
⊢ ¬x.coeff j = 0 ∧ (∃ i_1, ¬(x ^ i_1).coeff i = 0) ∧ j + i = i + j

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
⊢ {a | ((fun n => x ^ n) a).coeff g ≠ 0}.Finite

Tactic:
exact h0 ▸ Set.Finite.subset (Set.finite_singleton 0) (co_support_zero g)

Result:
no goals

Proof state:
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}

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

Result:
no goals

Proof state:
case neg
Γ : 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
⊢ {a | ((fun n => x ^ n) a).coeff g ≠ 0}.Finite

Tactic:
by_cases hg : g ∈ ⋃ n : ℕ, { g | (x ^ n).coeff g ≠ 0 }

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}
⊢ {a | ((fun n => x ^ n) a).coeff g ≠ 0}.Finite

case neg
Γ : 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

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
g : Γ
⊢ {a | ((fun n => x ^ n) a).coeff g ≠ 0}.Finite

Tactic:
have hpwo : Set.IsPWO (⋃ n, support (x ^ n)) :=
  isPWO_iUnion_support_powers (zero_le_orderTop_iff.mp <| le_of_lt hx)

Result:
Γ : 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
⊢ {a | ((fun n => x ^ n) a).coeff g ≠ 0}.Finite

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}
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}.Finite

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 ?_

Result:
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

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}

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}
⊢ ∀ 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

Tactic:
intro y ys hy

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 : Γ
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}.Finite