-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem coeff_smul {R} {V} [Semiring R] [AddCommMonoid V] [Module R V]
    (s : SummableFamily Γ R α) (t : SummableFamily Γ' V β) (g : Γ') :
    (smul s t).hsum.coeff g = ∑ gh ∈ VAddAntidiagonal s.isPWO_iUnion_support
      t.isPWO_iUnion_support g, (s.hsum.coeff gh.1) • (t.hsum.coeff gh.2)

Proof state:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
⊢ ∑ᶠ (i : α × β), ∑ x ∈ VAddAntidiagonal ⋯ ⋯ g, (s i.1).coeff x.1 • (t i.2).coeff x.2 =
    ∑ x ∈ VAddAntidiagonal ⋯ ⋯ g,
      ∑ x_1 ∈ (t.coeff x.2).support, ∑ i ∈ (s.coeff x.1).support, (s i).coeff x.1 • (t x_1).coeff x.2

Tactic:
rw [← sum_finsum_comm _ _ <| fun gh _ => smul_support_finite s t gh]

Result:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
⊢ ∑ a ∈ VAddAntidiagonal ⋯ ⋯ g, ∑ᶠ (b : α × β), (s b.1).coeff a.1 • (t b.2).coeff a.2 =
    ∑ x ∈ VAddAntidiagonal ⋯ ⋯ g,
      ∑ x_1 ∈ (t.coeff x.2).support, ∑ i ∈ (s.coeff x.1).support, (s i).coeff x.1 • (t x_1).coeff x.2

Proof state:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
⊢ ∑ a ∈ VAddAntidiagonal ⋯ ⋯ g, ∑ᶠ (b : α × β), (s b.1).coeff a.1 • (t b.2).coeff a.2 =
    ∑ x ∈ VAddAntidiagonal ⋯ ⋯ g,
      ∑ x_1 ∈ (t.coeff x.2).support, ∑ i ∈ (s.coeff x.1).support, (s i).coeff x.1 • (t x_1).coeff x.2

Tactic:
refine sum_congr rfl fun gh _ => ?_

Result:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
gh : Γ × Γ'
x✝ : gh ∈ VAddAntidiagonal ⋯ ⋯ g
⊢ ∑ᶠ (b : α × β), (s b.1).coeff gh.1 • (t b.2).coeff gh.2 =
    ∑ x ∈ (t.coeff gh.2).support, ∑ i ∈ (s.coeff gh.1).support, (s i).coeff gh.1 • (t x).coeff gh.2

Proof state:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
⊢ ∑ᶠ (i : α × β), ∑ x ∈ VAddAntidiagonal ⋯ ⋯ g, (s i.1).coeff x.1 • (t i.2).coeff x.2 =
    ∑ x ∈ VAddAntidiagonal ⋯ ⋯ g,
      (∑ i ∈ (s.coeff x.1).support, (s i).coeff x.1) • ∑ i ∈ (t.coeff x.2).support, (t i).coeff x.2

Tactic:
simp_rw [sum_vAddAntidiagonal_eq, Finset.smul_sum, Finset.sum_smul]

Result:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
⊢ ∑ᶠ (i : α × β), ∑ x ∈ VAddAntidiagonal ⋯ ⋯ g, (s i.1).coeff x.1 • (t i.2).coeff x.2 =
    ∑ x ∈ VAddAntidiagonal ⋯ ⋯ g,
      ∑ x_1 ∈ (t.coeff x.2).support, ∑ i ∈ (s.coeff x.1).support, (s i).coeff x.1 • (t x_1).coeff x.2

Proof state:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
⊢ (s.smul t).hsum.coeff g = ∑ gh ∈ VAddAntidiagonal ⋯ ⋯ g, s.hsum.coeff gh.1 • t.hsum.coeff gh.2

Tactic:
rw [coeff_hsum]

Result:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
⊢ ∑ᶠ (i : α × β), ((s.smul t) i).coeff g = ∑ gh ∈ VAddAntidiagonal ⋯ ⋯ g, s.hsum.coeff gh.1 • t.hsum.coeff gh.2