-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem smul_hsum {R} {V} [Semiring R] [AddCommMonoid V] [Module R V]
    (s : SummableFamily Γ R α) (t : SummableFamily Γ' V β) :
    (smul s t).hsum = (of R).symm (s.hsum • (of R) (t.hsum))

Proof state:
case coeff.h.refine_2
Γ : 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
hgh : ¬s.hsum.coeff gh.1 = 0 → ¬t.hsum.coeff gh.2 = 0 → ¬gh.1 +ᵥ gh.2 = g
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0

Tactic:
by_cases h : s.hsum.coeff gh.1 = 0

Result:
case pos
Γ : 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
hgh : ¬s.hsum.coeff gh.1 = 0 → ¬t.hsum.coeff gh.2 = 0 → ¬gh.1 +ᵥ gh.2 = g
h : s.hsum.coeff gh.1 = 0
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0

case neg
Γ : 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
hgh : ¬s.hsum.coeff gh.1 = 0 → ¬t.hsum.coeff gh.2 = 0 → ¬gh.1 +ᵥ gh.2 = g
h : ¬s.hsum.coeff gh.1 = 0
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0

Proof state:
case coeff.h.refine_1.left
Γ : 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 : Γ'
x✝ : Γ × Γ'
hgh : ¬∑ i ∈ (s.coeff x✝.1).support, (s i).coeff x✝.1 = 0 ∧ ¬t.hsum.coeff x✝.2 = 0 ∧ x✝.1 +ᵥ x✝.2 = g
h' : ∃ a ∈ (s.coeff x✝.1).support, (s a).coeff x✝.1 ≠ 0
⊢ ∃ i, ¬(s i).coeff x✝.1 = 0

Tactic:
simpa using h'

Result:
no goals

Proof state:
case coeff.h.refine_2
Γ : 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
hgh : gh ∉ (fun a => a) '' ↑(VAddAntidiagonal ⋯ ⋯ g)
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0

Tactic:
simp only [Set.image_id', mem_coe, mem_vaddAntidiagonal, mem_support, ne_eq, not_and] at hgh

Result:
case coeff.h.refine_2
Γ : 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
hgh : ¬s.hsum.coeff gh.1 = 0 → ¬t.hsum.coeff gh.2 = 0 → ¬gh.1 +ᵥ gh.2 = g
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0

Proof state:
case pos
Γ : 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
hgh : ¬s.hsum.coeff gh.1 = 0 → ¬t.hsum.coeff gh.2 = 0 → ¬gh.1 +ᵥ gh.2 = g
h : s.hsum.coeff gh.1 = 0
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0

Tactic:
exact smul_eq_zero_of_left h (t.hsum.coeff gh.2)

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 β
⊢ (s.smul t).hsum = (of R).symm (s.hsum • (of R) t.hsum)

Tactic:
ext g

Result:
case coeff.h
Γ : 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 = ((of R).symm (s.hsum • (of R) t.hsum)).coeff g

Proof state:
case coeff.h.refine_1
Γ : 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 : Γ'
x✝ : Γ × Γ'
hgh : x✝ ∈ ↑(VAddAntidiagonal ⋯ ⋯ g)
⊢ (fun a => a) x✝ ∈ ↑(VAddAntidiagonal ⋯ ⋯ g)

Tactic:
simp_all only [mem_coe, mem_vaddAntidiagonal, mem_support, ne_eq, Set.mem_iUnion, and_true]

Result:
case coeff.h.refine_1
Γ : 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 : Γ'
x✝ : Γ × Γ'
hgh : ¬s.hsum.coeff x✝.1 = 0 ∧ ¬t.hsum.coeff x✝.2 = 0 ∧ x✝.1 +ᵥ x✝.2 = g
⊢ (∃ i, ¬(s i).coeff x✝.1 = 0) ∧ ∃ i, ¬(t i).coeff x✝.2 = 0

Proof state:
case coeff.h.refine_1.right
Γ : 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 : Γ'
x✝ : Γ × Γ'
hgh : ¬s.hsum.coeff x✝.1 = 0 ∧ ¬t.hsum.coeff x✝.2 = 0 ∧ x✝.1 +ᵥ x✝.2 = g
hi : ¬∃ i, ¬(t i).coeff x✝.2 = 0
⊢ False

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 : Γ'
x✝¹ : Γ × Γ'
x✝ : x✝¹ ∈ VAddAntidiagonal ⋯ ⋯ g
⊢ s.hsum.coeff x✝¹.1 • t.hsum.coeff x✝¹.2 = s.hsum.coeff ((fun a => a) x✝¹).1 • t.hsum.coeff ((fun a => a) x✝¹).2

Tactic:
simp

Result:
no goals