case coeff.h
Γ : Type u_3
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_1
f : α →₀ HahnSeries Γ R
g : Γ
⊢ coeff (hsum (ofFinsupp f)) g = coeff (Finsupp.sum f fun x => id) g
Γ : Type u_3
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_1
f : α →₀ HahnSeries Γ R
⊢ hsum (ofFinsupp f) = Finsupp.sum f fun x => id
ext g
case coeff.h
Γ : Type u_3
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_1
f : α →₀ HahnSeries Γ R
g : Γ
⊢ (∑ᶠ (i : α), coeff (↑f i) g) = coeff (∑ x in f.support, id (↑f x)) g
case coeff.h
Γ : Type u_3
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_1
f : α →₀ HahnSeries Γ R
g : Γ
⊢ coeff (hsum (ofFinsupp f)) g = coeff (Finsupp.sum f fun x => id) g
simp only [hsum_coeff, coe_ofFinsupp, Finsupp.sum, Ne.def]
case coeff.h
Γ : Type u_3
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_1
f : α →₀ HahnSeries Γ R
g : Γ
⊢ (∑ᶠ (i : α), ↑(coeff.addMonoidHom g) (↑f i)) = ↑(coeff.addMonoidHom g) (∑ x in f.support, ↑f x)
case coeff.h
Γ : Type u_3
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_1
f : α →₀ HahnSeries Γ R
g : Γ
⊢ (∑ᶠ (i : α), coeff (↑f i) g) = coeff (∑ x in f.support, id (↑f x)) g
simp_rw [← coeff.addMonoidHom_apply, id.def]
case coeff.h.h
Γ : Type u_3
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_1
f : α →₀ HahnSeries Γ R
g : Γ
⊢ (Function.support fun i => ↑(coeff.addMonoidHom g) (↑f i)) ⊆ ↑f.support
case coeff.h
Γ : Type u_3
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_1
f : α →₀ HahnSeries Γ R
g : Γ
⊢ (∑ᶠ (i : α), ↑(coeff.addMonoidHom g) (↑f i)) = ↑(coeff.addMonoidHom g) (∑ x in f.support, ↑f x)
rw [map_sum, finsum_eq_sum_of_support_subset]
case coeff.h.h
Γ : Type u_3
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_1
f : α →₀ HahnSeries Γ R
g : Γ
x : α
h : x ∈ Function.support fun i => ↑(coeff.addMonoidHom g) (↑f i)
⊢ x ∈ ↑f.support
case coeff.h.h
Γ : Type u_3
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_1
f : α →₀ HahnSeries Γ R
g : Γ
⊢ (Function.support fun i => ↑(coeff.addMonoidHom g) (↑f i)) ⊆ ↑f.support
intro x h
case coeff.h.h
Γ : Type u_3
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_1
f : α →₀ HahnSeries Γ R
g : Γ
x : α
h : x ∈ Function.support fun i => ↑(coeff.addMonoidHom g) (↑f i)
⊢ ¬↑f x = 0
case coeff.h.h
Γ : Type u_3
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_1
f : α →₀ HahnSeries Γ R
g : Γ
x : α
h : x ∈ Function.support fun i => ↑(coeff.addMonoidHom g) (↑f i)
⊢ x ∈ ↑f.support
simp only [coeff.addMonoidHom_apply, mem_coe, Finsupp.mem_support_iff, Ne.def]
case coeff.h.h
Γ : Type u_3
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_1
f : α →₀ HahnSeries Γ R
g : Γ
x : α
h : ↑f x = 0
⊢ ¬x ∈ Function.support fun i => ↑(coeff.addMonoidHom g) (↑f i)
case coeff.h.h
Γ : Type u_3
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_1
f : α →₀ HahnSeries Γ R
g : Γ
x : α
h : x ∈ Function.support fun i => ↑(coeff.addMonoidHom g) (↑f i)
⊢ ¬↑f x = 0
contrapose! h
no goals
case coeff.h.h
Γ : Type u_3
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_1
f : α →₀ HahnSeries Γ R
g : Γ
x : α
h : ↑f x = 0
⊢ ¬x ∈ Function.support fun i => ↑(coeff.addMonoidHom g) (↑f i)
simp [h]