-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem isPWO_iUnion_support_prod_smul {s : α → HahnSeries Γ R} {t : β → HahnSeries Γ' V}
    (hs : (⋃ a, (s a).support).IsPWO) (ht : (⋃ b, (t b).support).IsPWO) :
    (⋃ (a : α × β), ((fun a ↦ (of R).symm
      ((s a.1) • (of R) (t a.2))) a).support).IsPWO

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 : α → HahnSeries Γ R
t : β → HahnSeries Γ' V
hs : (⋃ a, (s a).support).IsPWO
ht : (⋃ b, (t b).support).IsPWO
ab : α × β
x : Γ'
hx : VAddAntidiagonal ⋯ ⋯ x = ∅
⊢ x ∉ ((of R).symm (s ab.1 • (of R) (t ab.2))).support

Tactic:
rw [mem_support, not_not, HahnModule.coeff_smul, hx, sum_empty]

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 : α → HahnSeries Γ R
t : β → HahnSeries Γ' V
hs : (⋃ a, (s a).support).IsPWO
ht : (⋃ b, (t b).support).IsPWO
hsupp :
  ∀ (ab : α × β), ((fun ab => (of R).symm (s ab.1 • (of R) (t ab.2))) ab).support ⊆ (s ab.1).support +ᵥ (t ab.2).support
⊢ ⋃ i, (s i.1).support +ᵥ (t i.2).support ⊆ (⋃ a, (s a).support) +ᵥ ⋃ b, (t b).support

Tactic:
simp_all only [Set.iUnion_subset_iff, Prod.forall]

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 : α → HahnSeries Γ R
t : β → HahnSeries Γ' V
hs : (⋃ a, (s a).support).IsPWO
ht : (⋃ b, (t b).support).IsPWO
hsupp : ∀ (a : α) (b : β), ((of R).symm (s a • (of R) (t b))).support ⊆ (s a).support +ᵥ (t b).support
⊢ ∀ (a : α) (b : β), (s a).support +ᵥ (t b).support ⊆ (⋃ a, (s a).support) +ᵥ ⋃ b, (t b).support

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 : α → HahnSeries Γ R
t : β → HahnSeries Γ' V
hs : (⋃ a, (s a).support).IsPWO
ht : (⋃ b, (t b).support).IsPWO
ab : α × β
x : Γ'
hx : x ∉ {a | (VAddAntidiagonal ⋯ ⋯ a).Nonempty}
⊢ x ∉ ((of R).symm (s ab.1 • (of R) (t ab.2))).support

Tactic:
simp only [Set.mem_setOf_eq, not_nonempty_iff_eq_empty] at hx

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 : α → HahnSeries Γ R
t : β → HahnSeries Γ' V
hs : (⋃ a, (s a).support).IsPWO
ht : (⋃ b, (t b).support).IsPWO
ab : α × β
x : Γ'
hx : VAddAntidiagonal ⋯ ⋯ x = ∅
⊢ x ∉ ((of R).symm (s ab.1 • (of R) (t ab.2))).support

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 : α → HahnSeries Γ R
t : β → HahnSeries Γ' V
hs : (⋃ a, (s a).support).IsPWO
ht : (⋃ b, (t b).support).IsPWO
hsupp :
  ∀ (ab : α × β), ((fun ab => (of R).symm (s ab.1 • (of R) (t ab.2))) ab).support ⊆ (s ab.1).support +ᵥ (t ab.2).support
⊢ ⋃ a, ((fun a => (of R).symm (s a.1 • (of R) (t a.2))) a).support ⊆ (⋃ a, (s a).support) +ᵥ ⋃ b, (t b).support

Tactic:
refine Set.Subset.trans (Set.iUnion_mono fun a => (hsupp a)) ?_

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 : α → HahnSeries Γ R
t : β → HahnSeries Γ' V
hs : (⋃ a, (s a).support).IsPWO
ht : (⋃ b, (t b).support).IsPWO
hsupp :
  ∀ (ab : α × β), ((fun ab => (of R).symm (s ab.1 • (of R) (t ab.2))) ab).support ⊆ (s ab.1).support +ᵥ (t ab.2).support
⊢ ⋃ i, (s i.1).support +ᵥ (t i.2).support ⊆ (⋃ a, (s a).support) +ᵥ ⋃ b, (t b).support

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 : α → HahnSeries Γ R
t : β → HahnSeries Γ' V
hs : (⋃ a, (s a).support).IsPWO
ht : (⋃ b, (t b).support).IsPWO
⊢ ∀ (ab : α × β), ((fun ab => (of R).symm (s ab.1 • (of R) (t ab.2))) ab).support ⊆ (s ab.1).support +ᵥ (t ab.2).support

Tactic:
intro ab

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 : α → HahnSeries Γ R
t : β → HahnSeries Γ' V
hs : (⋃ a, (s a).support).IsPWO
ht : (⋃ b, (t b).support).IsPWO
ab : α × β
⊢ ((fun ab => (of R).symm (s ab.1 • (of R) (t ab.2))) ab).support ⊆ (s ab.1).support +ᵥ (t ab.2).support

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 : α → HahnSeries Γ R
t : β → HahnSeries Γ' V
hs : (⋃ a, (s a).support).IsPWO
ht : (⋃ b, (t b).support).IsPWO
⊢ ⋃ a, ((fun a => (of R).symm (s a.1 • (of R) (t a.2))) a).support ⊆ (⋃ a, (s a).support) +ᵥ ⋃ b, (t b).support

Tactic:
have hsupp : ∀ ab : α × β, support ((fun ab ↦ (of R).symm (s ab.1 • (of R) (t ab.2))) ab) ⊆
    (s ab.1).support +ᵥ (t ab.2).support := by
  intro ab
  refine Set.Subset.trans (fun x hx => ?_) (support_vaddAntidiagonal_subset_vadd
    (hs := (s ab.1).isPWO_support) (ht := (t ab.2).isPWO_support))
  contrapose! hx
  simp only [Set.mem_setOf_eq, not_nonempty_iff_eq_empty] at hx
  rw [mem_support, not_not, HahnModule.coeff_smul, hx, sum_empty]

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 : α → HahnSeries Γ R
t : β → HahnSeries Γ' V
hs : (⋃ a, (s a).support).IsPWO
ht : (⋃ b, (t b).support).IsPWO
hsupp :
  ∀ (ab : α × β), ((fun ab => (of R).symm (s ab.1 • (of R) (t ab.2))) ab).support ⊆ (s ab.1).support +ᵥ (t ab.2).support
⊢ ⋃ a, ((fun a => (of R).symm (s a.1 • (of R) (t a.2))) a).support ⊆ (⋃ a, (s a).support) +ᵥ ⋃ b, (t b).support