-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem support_pow_subset_closure [OrderedCancelAddCommMonoid Γ] [Semiring R] (x : HahnSeries Γ R)
    (n : ℕ) : support (x ^ n) ⊆ AddSubmonoid.closure (support x)

Proof state:
case succ
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
n : ℕ
ih : (x ^ n).support ⊆ ↑(AddSubmonoid.closure x.support)
g : Γ
hn : g ∈ (x ^ (n + 1)).support
⊢ g ∈ ↑(AddSubmonoid.closure x.support)

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

Result:
case succ.intro.intro.intro.intro
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
n : ℕ
ih : (x ^ n).support ⊆ ↑(AddSubmonoid.closure x.support)
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)

Proof state:
case succ.intro.intro.intro.intro
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
n : ℕ
ih : (x ^ n).support ⊆ ↑(AddSubmonoid.closure x.support)
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)

Tactic:
exact SetLike.mem_coe.2 (AddSubmonoid.add_mem _ (ih hi) (AddSubmonoid.subset_closure hj))

Result:
no goals

Proof state:
case zero
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
g : Γ
hn : g = 0 ∧ ¬1 = 0
⊢ g ∈ ↑(AddSubmonoid.closure x.support)

Tactic:
simp only [hn, SetLike.mem_coe]

Result:
case zero
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
g : Γ
hn : g = 0 ∧ ¬1 = 0
⊢ 0 ∈ AddSubmonoid.closure x.support

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
n : ℕ
⊢ (x ^ n).support ⊆ ↑(AddSubmonoid.closure x.support)

Tactic:
induction' n with n ih <;> intro g hn

Result:
case zero
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
g : Γ
hn : g ∈ (x ^ 0).support
⊢ g ∈ ↑(AddSubmonoid.closure x.support)

case succ
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
n : ℕ
ih : (x ^ n).support ⊆ ↑(AddSubmonoid.closure x.support)
g : Γ
hn : g ∈ (x ^ (n + 1)).support
⊢ g ∈ ↑(AddSubmonoid.closure x.support)

Proof state:
case zero
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
g : Γ
hn : g ∈ (x ^ 0).support
⊢ g ∈ ↑(AddSubmonoid.closure x.support)

Tactic:
simp only [pow_zero, mem_support, coeff_one, ne_eq, ite_eq_right_iff, Classical.not_imp] at hn

Result:
case zero
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
g : Γ
hn : g = 0 ∧ ¬1 = 0
⊢ g ∈ ↑(AddSubmonoid.closure x.support)

Proof state:
case zero
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
g : Γ
hn : g = 0 ∧ ¬1 = 0
⊢ 0 ∈ AddSubmonoid.closure x.support

Tactic:
exact AddSubmonoid.zero_mem _

Result:
no goals