Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
⊢ ∀ (x_1 : Γ), x_1 ∈ support x → 0 ≤ x_1

Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
⊢ (⋃ (n : ℕ), support (x ^ n)) ⊆ ↑(AddSubmonoid.closure (support x))
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
⊢ Set.IsPwo (⋃ (n : ℕ), support (x ^ n))
apply (x.isWf_support.isPwo.addSubmonoid_closure _).mono _
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
n : ℕ
⊢ support (x ^ n) ⊆ ↑(AddSubmonoid.closure (support x))
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
⊢ (⋃ (n : ℕ), support (x ^ n)) ⊆ ↑(AddSubmonoid.closure (support x))
refine' Set.iUnion_subset fun n => _
case zero
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
g : Γ
hn : g ∈ support (x ^ Nat.zero)
⊢ g ∈ ↑(AddSubmonoid.closure (support x))

case succ
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
n : ℕ
ih : support (x ^ n) ⊆ ↑(AddSubmonoid.closure (support x))
g : Γ
hn : g ∈ support (x ^ Nat.succ n)
⊢ g ∈ ↑(AddSubmonoid.closure (support x))
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
n : ℕ
⊢ support (x ^ n) ⊆ ↑(AddSubmonoid.closure (support x))
induction' n with n ih <;> intro g hn
no goals
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
⊢ ∀ (x_1 : Γ), x_1 ∈ support x → 0 ≤ x_1
exact fun g hg => WithTop.coe_le_coe.1 (le_trans (le_of_lt hx) (addVal_le_of_coeff_ne_zero hg))
case zero
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
g : Γ
hn : g = 0
⊢ g ∈ ↑(AddSubmonoid.closure (support x))
case zero
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
g : Γ
hn : g ∈ support (x ^ Nat.zero)
⊢ g ∈ ↑(AddSubmonoid.closure (support x))
simp only [Nat.zero_eq, pow_zero, support_one, Set.mem_singleton_iff] at hn
case zero
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
g : Γ
hn : g = 0
⊢ 0 ∈ AddSubmonoid.closure (support x)
case zero
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
g : Γ
hn : g = 0
⊢ g ∈ ↑(AddSubmonoid.closure (support x))
rw [hn, SetLike.mem_coe]
no goals
case zero
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
g : Γ
hn : g = 0
⊢ 0 ∈ AddSubmonoid.closure (support x)
exact AddSubmonoid.zero_mem _
case succ.intro.intro.intro.intro
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
n : ℕ
ih : support (x ^ n) ⊆ ↑(AddSubmonoid.closure (support x))
i j : Γ
hi : i ∈ support x
hj : j ∈ support (npowRec n x)
hn : (fun x x_1 => x + x_1) i j ∈ support (x ^ Nat.succ n)
⊢ (fun x x_1 => x + x_1) i j ∈ ↑(AddSubmonoid.closure (support x))
case succ
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
n : ℕ
ih : support (x ^ n) ⊆ ↑(AddSubmonoid.closure (support x))
g : Γ
hn : g ∈ support (x ^ Nat.succ n)
⊢ g ∈ ↑(AddSubmonoid.closure (support x))
obtain ⟨i, j, hi, hj, rfl⟩ := support_mul_subset_add_support hn
no goals
case succ.intro.intro.intro.intro
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x : HahnSeries Γ R
hx : 0 < ↑(addVal Γ R) x
n : ℕ
ih : support (x ^ n) ⊆ ↑(AddSubmonoid.closure (support x))
i j : Γ
hi : i ∈ support x
hj : j ∈ support (npowRec n x)
hn : (fun x x_1 => x + x_1) i j ∈ support (x ^ Nat.succ n)
⊢ (fun x x_1 => x + x_1) i j ∈ ↑(AddSubmonoid.closure (support x))
exact SetLike.mem_coe.2 (AddSubmonoid.add_mem _ (AddSubmonoid.subset_closure hi) (ih hj))