-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem finite_co_support_prod_smul (s : SummableFamily Γ R α)
    (t : SummableFamily Γ' V β) (g : Γ') :
    Finite {(ab : α × β) |
      ((fun (ab : α × β) ↦ (of R).symm (s ab.1 • (of R) (t ab.2))) ab).coeff g ≠ 0}

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 : Γ'
ab : α × β
hab : ¬((of R).symm (s ab.1 • (of R) (t ab.2))).coeff g = 0
⊢ ab ∈ ⋃ i ∈ ↑(VAddAntidiagonal ⋯ ⋯ g), Function.support fun i_1 => (s i_1.1).coeff i.1 • (t i_1.2).coeff i.2

Tactic:
obtain ⟨ij, hij⟩ := Finset.exists_ne_zero_of_sum_ne_zero hab

Result:
case intro
Γ : 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 : Γ'
ab : α × β
hab : ¬((of R).symm (s ab.1 • (of R) (t ab.2))).coeff g = 0
ij : Γ × Γ'
hij : ij ∈ VAddAntidiagonal ⋯ ⋯ g ∧ (s ab.1).coeff ij.1 • ((of R).symm ((of R) (t ab.2))).coeff ij.2 ≠ 0
⊢ ab ∈ ⋃ i ∈ ↑(VAddAntidiagonal ⋯ ⋯ g), Function.support fun i_1 => (s i_1.1).coeff i.1 • (t i_1.2).coeff i.2

Proof state:
case intro
Γ : 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 : Γ'
ab : α × β
hab : ¬((of R).symm (s ab.1 • (of R) (t ab.2))).coeff g = 0
ij : Γ × Γ'
hij : ij ∈ VAddAntidiagonal ⋯ ⋯ g ∧ (s ab.1).coeff ij.1 • ((of R).symm ((of R) (t ab.2))).coeff ij.2 ≠ 0
⊢ ∃ a b, ((∃ i, ¬(s i).coeff a = 0) ∧ (∃ i, ¬(t i).coeff b = 0) ∧ a +ᵥ b = g) ∧ ¬(s ab.1).coeff a • (t ab.2).coeff b = 0

Tactic:
exact ⟨ij.1, ij.2, ⟨⟨ab.1, left_ne_zero_of_smul hij.2⟩, ⟨ab.2, right_ne_zero_of_smul hij.2⟩,
  ((mem_vaddAntidiagonal _ _ _).mp hij.1).2.2⟩, hij.2⟩

Result:
no goals

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 : Γ'
⊢ {ab | ((fun ab => (of R).symm (s ab.1 • (of R) (t ab.2))) ab).coeff g ≠ 0} ⊆
    ⋃ i ∈ ↑(VAddAntidiagonal ⋯ ⋯ g), Function.support fun i_1 => (s i_1.1).coeff i.1 • (t i_1.2).coeff i.2

Tactic:
exact fun ab hab => by
  simp only [coeff_smul, ne_eq, Set.mem_setOf_eq] at hab
  obtain ⟨ij, hij⟩ := Finset.exists_ne_zero_of_sum_ne_zero hab
  simp only [mem_coe, mem_vaddAntidiagonal, Set.mem_iUnion, mem_support, ne_eq,
    Function.mem_support, exists_prop, Prod.exists]
  exact ⟨ij.1, ij.2, ⟨⟨ab.1, left_ne_zero_of_smul hij.2⟩, ⟨ab.2, right_ne_zero_of_smul hij.2⟩,
    ((mem_vaddAntidiagonal _ _ _).mp hij.1).2.2⟩, hij.2⟩

Result:
no goals

Proof state:
case intro
Γ : 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 : Γ'
ab : α × β
hab : ¬((of R).symm (s ab.1 • (of R) (t ab.2))).coeff g = 0
ij : Γ × Γ'
hij : ij ∈ VAddAntidiagonal ⋯ ⋯ g ∧ (s ab.1).coeff ij.1 • ((of R).symm ((of R) (t ab.2))).coeff ij.2 ≠ 0
⊢ ab ∈ ⋃ i ∈ ↑(VAddAntidiagonal ⋯ ⋯ g), Function.support fun i_1 => (s i_1.1).coeff i.1 • (t i_1.2).coeff i.2

Tactic:
simp only [mem_coe, mem_vaddAntidiagonal, Set.mem_iUnion, mem_support, ne_eq,
  Function.mem_support, exists_prop, Prod.exists]

Result:
case intro
Γ : 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 : Γ'
ab : α × β
hab : ¬((of R).symm (s ab.1 • (of R) (t ab.2))).coeff g = 0
ij : Γ × Γ'
hij : ij ∈ VAddAntidiagonal ⋯ ⋯ g ∧ (s ab.1).coeff ij.1 • ((of R).symm ((of R) (t ab.2))).coeff ij.2 ≠ 0
⊢ ∃ a b, ((∃ i, ¬(s i).coeff a = 0) ∧ (∃ i, ¬(t i).coeff b = 0) ∧ a +ᵥ b = g) ∧ ¬(s ab.1).coeff a • (t ab.2).coeff b = 0

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 : Γ'
⊢ Finite ↑{ab | ((fun ab => (of R).symm (s ab.1 • (of R) (t ab.2))) ab).coeff g ≠ 0}

Tactic:
apply ((VAddAntidiagonal s.isPWO_iUnion_support t.isPWO_iUnion_support g).finite_toSet.biUnion'
  (fun gh _ => smul_support_finite s t gh)).subset _

Result:
Γ : 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 : Γ'
⊢ {ab | ((fun ab => (of R).symm (s ab.1 • (of R) (t ab.2))) ab).coeff g ≠ 0} ⊆
    ⋃ i ∈ ↑(VAddAntidiagonal ⋯ ⋯ g), Function.support fun i_1 => (s i_1.1).coeff i.1 • (t i_1.2).coeff i.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 : Γ'
ab : α × β
hab : ab ∈ {ab | ((fun ab => (of R).symm (s ab.1 • (of R) (t ab.2))) ab).coeff g ≠ 0}
⊢ ab ∈ ⋃ i ∈ ↑(VAddAntidiagonal ⋯ ⋯ g), Function.support fun i_1 => (s i_1.1).coeff i.1 • (t i_1.2).coeff i.2

Tactic:
simp only [coeff_smul, ne_eq, Set.mem_setOf_eq] at hab

Result:
Γ : 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 : Γ'
ab : α × β
hab : ¬((of R).symm (s ab.1 • (of R) (t ab.2))).coeff g = 0
⊢ ab ∈ ⋃ i ∈ ↑(VAddAntidiagonal ⋯ ⋯ g), Function.support fun i_1 => (s i_1.1).coeff i.1 • (t i_1.2).coeff i.2