-- 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 : Γ'
gh : Γ × Γ'
ab : α × β
x✝ : (∃ i, ¬(s i).coeff gh.1 = 0) ∧ (∃ i, ¬(t i).coeff gh.2 = 0) ∧ gh.1 +ᵥ gh.2 = g
hab : ¬(s ab.1).coeff gh.1 • (t ab.2).coeff gh.2 = 0
hsupp :
  ∀ (a : α) (b : β),
    ¬(s a).coeff gh.1 • (t b).coeff gh.2 = 0 → ¬(s.toFun a).coeff gh.1 = 0 ∧ ¬(t.toFun b).coeff gh.2 = 0
⊢ ¬(s ab.1).coeff gh.1 = 0 ∧ ¬(t ab.2).coeff gh.2 = 0

Tactic:
exact hsupp ab.1 ab.2 hab

Result:
no goals

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 : Γ'
gh : Γ × Γ'
x✝ : gh ∈ VAddAntidiagonal ⋯ ⋯ g
ab : α × β
hab : ab ∈ ⋯.toFinset
hsupp : (Function.support fun i => (s i.1).coeff gh.1 • (t i.2).coeff gh.2) ⊆ ↑⋯.toFinset
⊢ ab ∈ (s.coeff gh.1).support ×ˢ (t.coeff gh.2).support

Tactic:
simp_all only [mem_vaddAntidiagonal, Set.mem_iUnion, mem_support, ne_eq, Set.Finite.mem_toFinset,
  Function.mem_support, Set.Finite.coe_toFinset, support_subset_iff, Set.mem_prod,
  Set.mem_setOf_eq, Prod.forall, coeff_support, mem_product]

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 : Γ × Γ'
ab : α × β
x✝ : (∃ i, ¬(s i).coeff gh.1 = 0) ∧ (∃ i, ¬(t i).coeff gh.2 = 0) ∧ gh.1 +ᵥ gh.2 = g
hab : ¬(s ab.1).coeff gh.1 • (t ab.2).coeff gh.2 = 0
hsupp :
  ∀ (a : α) (b : β),
    ¬(s a).coeff gh.1 • (t b).coeff gh.2 = 0 → ¬(s.toFun a).coeff gh.1 = 0 ∧ ¬(t.toFun b).coeff gh.2 = 0
⊢ ¬(s ab.1).coeff gh.1 = 0 ∧ ¬(t ab.2).coeff gh.2 = 0

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 : α × β), ((s.smul t) i).coeff g = ∑ gh ∈ VAddAntidiagonal ⋯ ⋯ g, s.hsum.coeff gh.1 • t.hsum.coeff gh.2

Tactic:
simp only [coeff_hsum_eq_sum, smul_toFun, HahnModule.coeff_smul, Equiv.symm_apply_apply]

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,
      (∑ i ∈ (s.coeff x.1).support, (s i).coeff x.1) • ∑ i ∈ (t.coeff x.2).support, (t i).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 : Γ'
gh : Γ × Γ'
x✝¹ : gh ∈ VAddAntidiagonal ⋯ ⋯ g
ab : α × β
x✝ : ab ∈ (s.coeff gh.1).support ×ˢ (t.coeff gh.2).support
hab : ab ∉ ⋯.toFinset
⊢ (s ab.1).coeff gh.1 • (t ab.2).coeff gh.2 = 0

Tactic:
simp_all

Result:
no goals

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 : Γ'
gh : Γ × Γ'
x✝ : gh ∈ VAddAntidiagonal ⋯ ⋯ g
⊢ ∑ i ∈ ⋯.toFinset, (s i.1).coeff gh.1 • (t i.2).coeff gh.2 =
    ∑ x ∈ (s.coeff gh.1).support ×ˢ (t.coeff gh.2).support, (s x.1).coeff gh.1 • (t x.2).coeff gh.2

Tactic:
refine sum_subset (fun ab hab => ?_) (fun ab _ hab => by simp_all)

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
ab : α × β
hab : ab ∈ ⋯.toFinset
⊢ ab ∈ (s.coeff gh.1).support ×ˢ (t.coeff gh.2).support

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 : Γ'
gh : Γ × Γ'
x✝ : gh ∈ VAddAntidiagonal ⋯ ⋯ g
ab : α × β
hab : ab ∈ ⋯.toFinset
⊢ ab ∈ (s.coeff gh.1).support ×ˢ (t.coeff gh.2).support

Tactic:
have hsupp := smul_support_subset_prod 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 : Γ'
gh : Γ × Γ'
x✝ : gh ∈ VAddAntidiagonal ⋯ ⋯ g
ab : α × β
hab : ab ∈ ⋯.toFinset
hsupp : (Function.support fun i => (s i.1).coeff gh.1 • (t i.2).coeff gh.2) ⊆ ↑⋯.toFinset
⊢ ab ∈ (s.coeff gh.1).support ×ˢ (t.coeff gh.2).support

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 : Γ'
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

Tactic:
rw [finsum_eq_sum _ (smul_support_finite s t gh), ← sum_product_right']

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
⊢ ∑ i ∈ ⋯.toFinset, (s i.1).coeff gh.1 • (t i.2).coeff gh.2 =
    ∑ x ∈ (s.coeff gh.1).support ×ˢ (t.coeff gh.2).support, (s x.1).coeff gh.1 • (t x.2).coeff gh.2