-- 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 : α × β
⊢ ((fun ab => (of R).symm (s ab.1 • (of R) (t ab.2))) ab).support ⊆ (s ab.1).support +ᵥ (t ab.2).support

Tactic:
refine Set.Subset.trans (fun x hx => ?_) (support_vaddAntidiagonal_subset_vadd
  (hs := (s ab.1).isPWO_support) (ht := (t ab.2).isPWO_support))

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 : x ∈ ((fun ab => (of R).symm (s ab.1 • (of R) (t ab.2))) ab).support
⊢ x ∈ {a | (VAddAntidiagonal ⋯ ⋯ a).Nonempty}

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 ∈ ((fun ab => (of R).symm (s ab.1 • (of R) (t ab.2))) ab).support
⊢ x ∈ {a | (VAddAntidiagonal ⋯ ⋯ a).Nonempty}

Tactic:
contrapose! 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 : x ∉ {a | (VAddAntidiagonal ⋯ ⋯ a).Nonempty}
⊢ 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
⊢ (⋃ a, ((fun a => (of R).symm (s a.1 • (of R) (t a.2))) a).support).IsPWO

Tactic:
apply (hs.vadd ht).mono

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
⊢ ⋃ a, ((fun a => (of R).symm (s a.1 • (of R) (t a.2))) a).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
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

Tactic:
exact fun a b => Set.vadd_subset_vadd (Set.subset_iUnion_of_subset a fun x y ↦ y)
  (Set.subset_iUnion_of_subset b fun x y ↦ y)

Result:
no goals