-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem sum_vAddAntidiagonal_eq (s : SummableFamily Γ R α) (t : SummableFamily Γ' V β) (g : Γ')
    (a : α × β) :
    ∑ x ∈ VAddAntidiagonal (s a.1).isPWO_support' (t a.2).isPWO_support' g, (s a.1).coeff x.1 •
      (t a.2).coeff x.2 = ∑ x ∈ VAddAntidiagonal s.isPWO_iUnion_support' t.isPWO_iUnion_support' g,
      (s a.1).coeff x.1 • (t a.2).coeff x.2

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

Tactic:
refine sum_subset (fun gh hgh => ?_) fun gh hgh h => ?_

Result:
case refine_1
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal ⋯ ⋯ g
⊢ gh ∈ VAddAntidiagonal ⋯ ⋯ g

case refine_2
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal ⋯ ⋯ g
h : gh ∉ VAddAntidiagonal ⋯ ⋯ g
⊢ (s a.1).coeff gh.1 • (t a.2).coeff gh.2 = 0

Proof state:
case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal ⋯ ⋯ g
h : gh ∉ VAddAntidiagonal ⋯ ⋯ g
hs : ¬(s a.1).coeff gh.1 = 0
⊢ (s a.1).coeff gh.1 • (t a.2).coeff gh.2 = 0

Tactic:
simp_all

Result:
no goals

Proof state:
case refine_2
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal ⋯ ⋯ g
h : gh ∉ VAddAntidiagonal ⋯ ⋯ g
⊢ (s a.1).coeff gh.1 • (t a.2).coeff gh.2 = 0

Tactic:
by_cases hs : (s a.1).coeff gh.1 = 0

Result:
case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal ⋯ ⋯ g
h : gh ∉ VAddAntidiagonal ⋯ ⋯ g
hs : (s a.1).coeff gh.1 = 0
⊢ (s a.1).coeff gh.1 • (t a.2).coeff gh.2 = 0

case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal ⋯ ⋯ g
h : gh ∉ VAddAntidiagonal ⋯ ⋯ g
hs : ¬(s a.1).coeff gh.1 = 0
⊢ (s a.1).coeff gh.1 • (t a.2).coeff gh.2 = 0

Proof state:
case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal ⋯ ⋯ g
h : gh ∉ VAddAntidiagonal ⋯ ⋯ g
hs : (s a.1).coeff gh.1 = 0
⊢ (s a.1).coeff gh.1 • (t a.2).coeff gh.2 = 0

Tactic:
exact smul_eq_zero_of_left hs ((t a.2).coeff gh.2)

Result:
no goals

Proof state:
case refine_1
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal ⋯ ⋯ g
⊢ gh ∈ VAddAntidiagonal ⋯ ⋯ g

Tactic:
simp_all only [mem_vaddAntidiagonal, Function.mem_support, Set.mem_iUnion, mem_support]

Result:
case refine_1
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
gh : Γ × Γ'
hgh : (s a.1).coeff gh.1 ≠ 0 ∧ (t a.2).coeff gh.2 ≠ 0 ∧ gh.1 +ᵥ gh.2 = g
⊢ (∃ i, (s.toFun i).coeff gh.1 ≠ 0) ∧ (∃ i, (t.toFun i).coeff gh.2 ≠ 0) ∧ True

Proof state:
case refine_1
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
gh : Γ × Γ'
hgh : (s a.1).coeff gh.1 ≠ 0 ∧ (t a.2).coeff gh.2 ≠ 0 ∧ gh.1 +ᵥ gh.2 = g
⊢ (∃ i, (s.toFun i).coeff gh.1 ≠ 0) ∧ (∃ i, (t.toFun i).coeff gh.2 ≠ 0) ∧ True

Tactic:
exact ⟨Exists.intro a.1 hgh.1, Exists.intro a.2 hgh.2.1, trivial⟩

Result:
no goals