-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem hsum_ofFinsupp {f : α →₀ HahnSeries Γ R} : (ofFinsupp f).hsum = f.sum fun _ => id

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
f : α →₀ HahnSeries Γ R
g : Γ
⊢ ∑ᶠ (i : α), (f i).coeff g = (∑ x ∈ f.support, id (f x)).coeff g

Tactic:
simp_rw [← coeff.addMonoidHom_apply, id]

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
f : α →₀ HahnSeries Γ R
g : Γ
⊢ ∑ᶠ (i : α), (coeff.addMonoidHom g) (f i) = (coeff.addMonoidHom g) (∑ x ∈ f.support, f x)

Proof state:
case coeff.h.h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
f : α →₀ HahnSeries Γ R
g : Γ
⊢ (Function.support fun i => (coeff.addMonoidHom g) (f i)) ⊆ ↑f.support

Tactic:
intro x h

Result:
case coeff.h.h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
f : α →₀ HahnSeries Γ R
g : Γ
x : α
h : x ∈ Function.support fun i => (coeff.addMonoidHom g) (f i)
⊢ x ∈ ↑f.support

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
f : α →₀ HahnSeries Γ R
⊢ (ofFinsupp f).hsum = f.sum fun x => id

Tactic:
ext g

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
f : α →₀ HahnSeries Γ R
g : Γ
⊢ (ofFinsupp f).hsum.coeff g = (f.sum fun x => id).coeff g

Proof state:
case coeff.h.h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
f : α →₀ HahnSeries Γ R
g : Γ
x : α
h : f x = 0
⊢ x ∉ Function.support fun i => (coeff.addMonoidHom g) (f i)

Tactic:
simp [h]

Result:
no goals

Proof state:
case coeff.h.h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
f : α →₀ HahnSeries Γ R
g : Γ
x : α
h : x ∈ Function.support fun i => (coeff.addMonoidHom g) (f i)
⊢ x ∈ ↑f.support

Tactic:
simp only [coeff.addMonoidHom_apply, mem_coe, Finsupp.mem_support_iff, Ne]

Result:
case coeff.h.h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
f : α →₀ HahnSeries Γ R
g : Γ
x : α
h : x ∈ Function.support fun i => (coeff.addMonoidHom g) (f i)
⊢ ¬f x = 0

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
f : α →₀ HahnSeries Γ R
g : Γ
⊢ (ofFinsupp f).hsum.coeff g = (f.sum fun x => id).coeff g

Tactic:
simp only [coeff_hsum, coe_ofFinsupp, Finsupp.sum, Ne]

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
f : α →₀ HahnSeries Γ R
g : Γ
⊢ ∑ᶠ (i : α), (f i).coeff g = (∑ x ∈ f.support, id (f x)).coeff g

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
f : α →₀ HahnSeries Γ R
g : Γ
⊢ ∑ᶠ (i : α), (coeff.addMonoidHom g) (f i) = (coeff.addMonoidHom g) (∑ x ∈ f.support, f x)

Tactic:
rw [map_sum, finsum_eq_sum_of_support_subset]

Result:
case coeff.h.h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
f : α →₀ HahnSeries Γ R
g : Γ
⊢ (Function.support fun i => (coeff.addMonoidHom g) (f i)) ⊆ ↑f.support

Proof state:
case coeff.h.h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
f : α →₀ HahnSeries Γ R
g : Γ
x : α
h : x ∈ Function.support fun i => (coeff.addMonoidHom g) (f i)
⊢ ¬f x = 0

Tactic:
contrapose! h

Result:
case coeff.h.h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
f : α →₀ HahnSeries Γ R
g : Γ
x : α
h : f x = 0
⊢ x ∉ Function.support fun i => (coeff.addMonoidHom g) (f i)