awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommGroup R
s_1 t : SummableFamily Γ R α
a : α
s : SummableFamily Γ R α
g : Γ
simp : Set.Finite.{u_5} (α := α) {a : α | ¬Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) 0}
⊢ Set.Finite.{u_5} (α := α) {a : α | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff (-(s : (a : α) → R⟦Γ⟧) a) g) 0}

Tactic:
simp only [coeff_neg', Pi.neg_apply, Ne, neg_eq_zero]

Premises used: neg_eq_zero, Ne, HahnSeries.coeff_neg', Pi.neg_apply
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommGroup R
s_1 t : SummableFamily Γ R α
a : α
s : SummableFamily Γ R α
g : Γ
⊢ Set.Finite.{u_5} (α := α) {a : α | ¬Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) 0}

Tactic:
s.finite_co_support g

Premises used: Function.HasFiniteSupport, setOf, Function.support, HahnSeries.SummableFamily.finite_co_support
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommGroup R
s_1 t : SummableFamily Γ R α
a : α
s : SummableFamily Γ R α
g : Γ
⊢ Set.Finite.{u_5} (α := α) {a : α | ¬Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) 0}

Tactic:
exact s.finite_co_support g

Premises used: HahnSeries.SummableFamily.finite_co_support
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommGroup R
s : SummableFamily Γ R α
⊢ Eq (α := (a : α) → R⟦Γ⟧) (⇑(-s) : (a : α) → R⟦Γ⟧) (-(⇑s : (a : α) → R⟦Γ⟧))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommGroup R
s : SummableFamily Γ R α
a : α
⊢ Eq (α := R⟦Γ⟧) ((-s : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧) (-(s : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧)

Tactic:
rfl

Premises used: HahnSeries.map, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommGroup R
s_1 t : SummableFamily Γ R α
a : α
s s' : SummableFamily Γ R α
simp_rw :
  Set.IsPWO.{u_1} (α := Γ)
    (⋃ (a : α),
      (HAdd.hAdd (α := (a : α) → R⟦Γ⟧) (β := (a : α) → R⟦Γ⟧) (⇑s : (a : α) → R⟦Γ⟧) (-(⇑s' : (a : α) → R⟦Γ⟧)) a).support)
⊢ Set.IsPWO.{u_1} (α := Γ)
    (⋃ (a : α),
      (HSub.hSub (α := (a : α) → R⟦Γ⟧) (β := (a : α) → R⟦Γ⟧) (⇑s : (a : α) → R⟦Γ⟧) (⇑s' : (a : α) → R⟦Γ⟧) a).support)

Tactic:
simp_rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommGroup R
s_1 t : SummableFamily Γ R α
a : α
s s' : SummableFamily Γ R α
⊢ Set.IsPWO.{u_1} (α := Γ)
    (⋃ (a : α),
      (HAdd.hAdd (α := (a : α) → R⟦Γ⟧) (β := (a : α) → R⟦Γ⟧) (⇑s : (a : α) → R⟦Γ⟧) (-(⇑s' : (a : α) → R⟦Γ⟧)) a).support)

Tactic:
(s + -s').isPWO_iUnion_support

Premises used: HahnSeries.SummableFamily.isPWO_iUnion_support, HAdd.hAdd, Neg.neg
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommGroup R
s_1 t : SummableFamily Γ R α
a : α
s s' : SummableFamily Γ R α
⊢ Set.IsPWO.{u_1} (α := Γ)
    (⋃ (a : α),
      (HAdd.hAdd (α := (a : α) → R⟦Γ⟧) (β := (a : α) → R⟦Γ⟧) (⇑s : (a : α) → R⟦Γ⟧) (-(⇑s' : (a : α) → R⟦Γ⟧)) a).support)

Tactic:
exact (s + -s').isPWO_iUnion_support

Premises used: HahnSeries.SummableFamily.isPWO_iUnion_support, HAdd.hAdd, Neg.neg
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommGroup R
s_1 t : SummableFamily Γ R α
a : α
s s' : SummableFamily Γ R α
g : Γ
simp_rw :
  Set.Finite.{u_5} (α := α)
    {a : α |
      (HAdd.hAdd (α := (a : α) → R⟦Γ⟧) (β := (a : α) → R⟦Γ⟧) (⇑s : (a : α) → R⟦Γ⟧) (-(⇑s' : (a : α) → R⟦Γ⟧)) a).coeff
          g ≠
        0}
⊢ Set.Finite.{u_5} (α := α)
    {a : α |
      (HSub.hSub (α := (a : α) → R⟦Γ⟧) (β := (a : α) → R⟦Γ⟧) (⇑s : (a : α) → R⟦Γ⟧) (⇑s' : (a : α) → R⟦Γ⟧) a).coeff g ≠
        0}

Tactic:
simp_rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommGroup R
s_1 t : SummableFamily Γ R α
a : α
s s' : SummableFamily Γ R α
g : Γ
⊢ Set.Finite.{u_5} (α := α)
    {a : α |
      (HAdd.hAdd (α := (a : α) → R⟦Γ⟧) (β := (a : α) → R⟦Γ⟧) (⇑s : (a : α) → R⟦Γ⟧) (-(⇑s' : (a : α) → R⟦Γ⟧)) a).coeff
          g ≠
        0}

Tactic:
(s + -s').finite_co_support' _

Premises used: setOf, HAdd.hAdd, HahnSeries.SummableFamily.finite_co_support', Neg.neg
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommGroup R
s_1 t : SummableFamily Γ R α
a : α
s s' : SummableFamily Γ R α
g : Γ
⊢ Set.Finite.{u_5} (α := α)
    {a : α |
      (HAdd.hAdd (α := (a : α) → R⟦Γ⟧) (β := (a : α) → R⟦Γ⟧) (⇑s : (a : α) → R⟦Γ⟧) (-(⇑s' : (a : α) → R⟦Γ⟧)) a).coeff
          g ≠
        0}

Tactic:
exact (s + -s').finite_co_support' _

Premises used: HAdd.hAdd, HahnSeries.SummableFamily.finite_co_support', Neg.neg
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommGroup R
s t : SummableFamily Γ R α
⊢ (⇑(s - t) : (a : α) → R⟦Γ⟧) = HSub.hSub (α := (a : α) → R⟦Γ⟧) (⇑s : (a : α) → R⟦Γ⟧) (⇑t : (a : α) → R⟦Γ⟧)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommGroup R
s t : SummableFamily Γ R α
a : α
⊢ (s - t : (a : α) → R⟦Γ⟧) a =
    HSub.hSub (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((s : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧) ((t : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid R
inst_4 : SMulWithZero R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
gh : Γ × Γ'
a : α × β
hab :
  Membership.mem (γ := Set (α × β))
    (Function.support (M := V) fun (i : α × β) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i.1) gh.1)
        (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i.2) gh.2))
    a
simp_all :
  ∀
    (hab :
      ¬HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a.1) gh.1)
            (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) a.2) gh.2) =
          0),
    ¬(s.toFun a.1).coeff gh.1 = 0 ∧ ¬(t.toFun a.2).coeff gh.2 = 0
⊢ a ∈
    (↑(Set.Finite.toFinset (s :=
          SProd.sprod (α := Set α) (β := Set β) {a : α | (s.toFun a).coeff gh.1 ≠ 0}
            {a : β | (t.toFun a).coeff gh.2 ≠ 0})
          ⋯) :
      Set (α × β))

Tactic:
simp_all only [Function.mem_support, ne_eq, Set.Finite.coe_toFinset, Set.mem_prod,
    Set.mem_setOf_eq]

Premises used: Set.Finite.coe_toFinset, Set.mem_setOf_eq, ne_eq, Set.mem_prod, Function.mem_support
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid R
inst_4 : SMulWithZero R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
gh : Γ × Γ'
a : α × β
hab :
  ¬HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a.1) gh.1)
        (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) a.2) gh.2) =
      0
⊢ ¬(s.toFun a.1).coeff gh.1 = 0 ∧ ¬(t.toFun a.2).coeff gh.2 = 0

Tactic:
⟨left_ne_zero_of_smul hab, right_ne_zero_of_smul hab⟩

Premises used: right_ne_zero_of_smul, left_ne_zero_of_smul, And.intro
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid R
inst_4 : SMulWithZero R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
gh : Γ × Γ'
a : α × β
hab :
  ¬HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a.1) gh.1)
        (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) a.2) gh.2) =
      0
⊢ ¬(s.toFun a.1).coeff gh.1 = 0 ∧ ¬(t.toFun a.2).coeff gh.2 = 0

Tactic:
exact ⟨left_ne_zero_of_smul hab, right_ne_zero_of_smul hab⟩
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid R
inst_4 : SMulWithZero R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
gh : Γ × Γ'
⊢ HasFiniteSupport (M := V) fun (i : α × β) ↦
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i.1) gh.1)
      (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i.2) gh.2)

Tactic:
Set.Finite.subset (Set.toFinite ((s.finite_co_support' gh.1).prod
    (t.finite_co_support' gh.2)).toFinset) (smul_support_subset_prod s t gh)

Premises used: Function.HasFiniteSupport, Set.Finite.subset, Set.toFinite
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid R
inst_4 : SMulWithZero R V
inst_5 : VAdd Γ Γ'
inst_6 : IsOrderedCancelVAdd Γ Γ'
s : α → R⟦Γ⟧
t : β → V⟦Γ'⟧
hs : Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), (s a).support)
ht : Set.IsPWO.{u_2} (α := Γ') (⋃ (b : β), (t b).support)
apply :
  ⋃ (a : α × β),
      support.{u_2, u_4} (R := V)
        ((fun (a : α × β) ↦
            ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
                (HSMul.hSMul (β := HahnModule Γ' R V) (s a.1)
                  ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) (t a.2) : HahnModule Γ' R V)) :
              V⟦Γ'⟧))
          a) ⊆
    HVAdd.hVAdd.{u_1, u_2, u_2} (α := Set Γ) (β := Set Γ') (⋃ (a : α), (s a).support) (⋃ (b : β), (t b).support)
⊢ Set.IsPWO.{u_2} (α := Γ')
    (⋃ (a : α × β),
      support.{u_2, u_4} (R := V)
        ((fun (a : α × β) ↦
            ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
                (HSMul.hSMul (β := HahnModule Γ' R V) (s a.1)
                  ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) (t a.2) : HahnModule Γ' R V)) :
              V⟦Γ'⟧))
          a))

Tactic:
apply (hs.vadd ht).mono

Premises used: Set.IsPWO.vadd, Set.IsPWO.mono
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid R
inst_4 : SMulWithZero R V
inst_5 : VAdd Γ Γ'
inst_6 : IsOrderedCancelVAdd Γ Γ'
s : α → R⟦Γ⟧
t : β → V⟦Γ'⟧
hs : Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), (s a).support)
ht : Set.IsPWO.{u_2} (α := Γ') (⋃ (b : β), (t b).support)
ab : α × β
⊢ support.{u_2, u_4} (R := V)
      ((fun (ab : α × β) ↦
          ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
              (HSMul.hSMul (β := HahnModule Γ' R V) (s ab.1)
                ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) (t ab.2) : HahnModule Γ' R V)) :
            V⟦Γ'⟧))
        ab) ⊆
    (s ab.1).support +ᵥ (t ab.2).support

Tactic:
Set.Subset.trans (fun x hx => ?_) (support_vaddAntidiagonal_subset_vadd fun a ↦
      Set.VAddAntidiagonal.finite_of_isPWO (s ab.1).isPWO_support (t ab.2).isPWO_support a)

Premises used: HahnSeries.isPWO_support, Finset.support_vaddAntidiagonal_subset_vadd, Set.Subset.trans, Set.VAddAntidiagonal.finite_of_isPWO, Prod.fst, Prod.snd
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid R
inst_4 : SMulWithZero R V
inst_5 : VAdd Γ Γ'
inst_6 : IsOrderedCancelVAdd Γ Γ'
s : α → R⟦Γ⟧
t : β → V⟦Γ'⟧
hs : Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), (s a).support)
ht : Set.IsPWO.{u_2} (α := Γ') (⋃ (b : β), (t b).support)
ab : α × β
refine :
  ∀ (x : Γ')
    (hx :
      Membership.mem (γ := Set Γ')
        (support.{u_2, u_4} (R := V)
          ((fun (ab : α × β) ↦
              ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
                  (HSMul.hSMul (β := HahnModule Γ' R V) (s ab.1)
                    ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) (t ab.2) : HahnModule Γ' R V)) :
                V⟦Γ'⟧))
            ab))
        x),
    Membership.mem (γ := Set Γ')
      {a : Γ' | (VAddAntidiagonal (s := (s ab.1).support) (t := (t ab.2).support) a ⋯).Nonempty} x
⊢ support.{u_2, u_4} (R := V)
      ((fun (ab : α × β) ↦
          ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
              (HSMul.hSMul (β := HahnModule Γ' R V) (s ab.1)
                ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) (t ab.2) : HahnModule Γ' R V)) :
            V⟦Γ'⟧))
        ab) ⊆
    (s ab.1).support +ᵥ (t ab.2).support

Tactic:
refine Set.Subset.trans (fun x hx => ?_) (support_vaddAntidiagonal_subset_vadd fun a ↦
      Set.VAddAntidiagonal.finite_of_isPWO (s ab.1).isPWO_support (t ab.2).isPWO_support a)

Premises used: HahnSeries.isPWO_support, Finset.support_vaddAntidiagonal_subset_vadd, Set.Subset.trans, Set.VAddAntidiagonal.finite_of_isPWO, Prod.fst, Prod.snd
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid R
inst_4 : SMulWithZero R V
inst_5 : VAdd Γ Γ'
inst_6 : IsOrderedCancelVAdd Γ Γ'
s : α → R⟦Γ⟧
t : β → V⟦Γ'⟧
hs : Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), (s a).support)
ht : Set.IsPWO.{u_2} (α := Γ') (⋃ (b : β), (t b).support)
ab : α × β
x : Γ'
hx :
  Membership.mem (γ := Set Γ')
    (support.{u_2, u_4} (R := V)
      ((fun (ab : α × β) ↦
          ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
              (HSMul.hSMul (β := HahnModule Γ' R V) (s ab.1)
                ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) (t ab.2) : HahnModule Γ' R V)) :
            V⟦Γ'⟧))
        ab))
    x
contrapose! :
  ∀ (hx : VAddAntidiagonal (s := (s ab.1).support) (t := (t ab.2).support) x ⋯ = ∅),
    x ∉
      support.{u_2, u_4} (R := V)
        ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
          (HSMul.hSMul (β := HahnModule Γ' R V) (s ab.1)
            ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) (t ab.2) : HahnModule Γ' R V)))
⊢ (VAddAntidiagonal (s := (s ab.1).support) (t := (t ab.2).support) x ⋯).Nonempty

Tactic:
contrapose! hx
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid R
inst_4 : SMulWithZero R V
inst_5 : VAdd Γ Γ'
inst_6 : IsOrderedCancelVAdd Γ Γ'
s : α → R⟦Γ⟧
t : β → V⟦Γ'⟧
hs : Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), (s a).support)
ht : Set.IsPWO.{u_2} (α := Γ') (⋃ (b : β), (t b).support)
ab : α × β
x : Γ'
hx : VAddAntidiagonal (s := (s ab.1).support) (t := (t ab.2).support) x ⋯ = ∅
rw :
  ¬Ne.{u_4 + 1} (α := V)
      (HahnSeries.coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
          (HSMul.hSMul (β := HahnModule Γ' R V) (s ab.1)
            ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) (t ab.2) : HahnModule Γ' R V)))
        x)
      0
rw₁ :
  Eq.{u_4 + 1} (α := V)
    (HahnSeries.coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (β := HahnModule Γ' R V) (s ab.1)
          ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) (t ab.2) : HahnModule Γ' R V)))
      x)
    0
rw₂ :
  Eq.{u_4 + 1} (α := V)
    (∑
      ij ∈
        VAddAntidiagonal (s := (s ab.1).support) (t :=
          support.{u_2, u_4} (R := V)
            ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) (t ab.2))))
          x ⋯,
      HSMul.hSMul (β := V) ((s ab.1).coeff ij.1)
        (HahnSeries.coeff
          ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) (t ab.2)))
          ij.2))
    0
rw₃ :
  Eq.{u_4 + 1} (α := V)
    (∑ ij ∈ ∅,
      HSMul.hSMul (β := V) ((s ab.1).coeff ij.1)
        (HahnSeries.coeff
          ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) (t ab.2)))
          ij.2))
    0
rw₄ rw₅ : Eq.{u_4 + 1} (α := V) 0 0
⊢ x ∉
    support.{u_2, u_4} (R := V)
      ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (β := HahnModule Γ' R V) (s ab.1)
          ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) (t ab.2) : HahnModule Γ' R V)))

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

Premises used: Classical.not_not, HahnModule.coeff_smul, Finset.sum_empty, HahnSeries.mem_support
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid R
inst_4 : SMulWithZero R V
inst_5 : VAdd Γ Γ'
inst_6 : IsOrderedCancelVAdd Γ Γ'
s : α → R⟦Γ⟧
t : β → V⟦Γ'⟧
hs : Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), (s a).support)
ht : Set.IsPWO.{u_2} (α := Γ') (⋃ (b : β), (t b).support)
⊢ ∀ (ab : α × β),
    support.{u_2, u_4} (R := V)
        ((fun (ab : α × β) ↦
            ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
                (HSMul.hSMul (β := HahnModule Γ' R V) (s ab.1)
                  ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) (t ab.2) : HahnModule Γ' R V)) :
              V⟦Γ'⟧))
          ab) ⊆
      (s ab.1).support +ᵥ (t ab.2).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 fun a ↦
      Set.VAddAntidiagonal.finite_of_isPWO (s ab.1).isPWO_support (t ab.2).isPWO_support a)
    simp only [Set.mem_setOf_eq]
    contrapose! hx
    rw [mem_support, not_not, HahnModule.coeff_smul, hx, sum_empty]
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid R
inst_4 : SMulWithZero R V
inst_5 : VAdd Γ Γ'
inst_6 : IsOrderedCancelVAdd Γ Γ'
s : α → R⟦Γ⟧
t : β → V⟦Γ'⟧
hs : Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), (s a).support)
ht : Set.IsPWO.{u_2} (α := Γ') (⋃ (b : β), (t b).support)
hsupp :
  ∀ (ab : α × β),
    support.{u_2, u_4} (R := V)
        ((fun (ab : α × β) ↦
            ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
                (HSMul.hSMul (β := HahnModule Γ' R V) (s ab.1)
                  ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) (t ab.2) : HahnModule Γ' R V)) :
              V⟦Γ'⟧))
          ab) ⊆
      (s ab.1).support +ᵥ (t ab.2).support
⊢ ⋃ (a : α × β),
      support.{u_2, u_4} (R := V)
        ((fun (a : α × β) ↦
            ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
                (HSMul.hSMul (β := HahnModule Γ' R V) (s a.1)
                  ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) (t a.2) : HahnModule Γ' R V)) :
              V⟦Γ'⟧))
          a) ⊆
    HVAdd.hVAdd.{u_1, u_2, u_2} (α := Set Γ) (β := Set Γ') (⋃ (a : α), (s a).support) (⋃ (b : β), (t b).support)

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

Premises used: Set.Subset.trans, Set.iUnion_mono
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid R
inst_4 : SMulWithZero R V
inst_5 : VAdd Γ Γ'
inst_6 : IsOrderedCancelVAdd Γ Γ'
s : α → R⟦Γ⟧
t : β → V⟦Γ'⟧
hs : Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), (s a).support)
ht : Set.IsPWO.{u_2} (α := Γ') (⋃ (b : β), (t b).support)
hsupp :
  ∀ (ab : α × β),
    support.{u_2, u_4} (R := V)
        ((fun (ab : α × β) ↦
            ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
                (HSMul.hSMul (β := HahnModule Γ' R V) (s ab.1)
                  ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) (t ab.2) : HahnModule Γ' R V)) :
              V⟦Γ'⟧))
          ab) ⊆
      (s ab.1).support +ᵥ (t ab.2).support
refine :
  ⋃ (i : α × β), (s i.1).support +ᵥ (t i.2).support ⊆
    HVAdd.hVAdd.{u_1, u_2, u_2} (α := Set Γ) (β := Set Γ') (⋃ (a : α), (s a).support) (⋃ (b : β), (t b).support)
⊢ ⋃ (a : α × β),
      support.{u_2, u_4} (R := V)
        ((fun (a : α × β) ↦
            ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
                (HSMul.hSMul (β := HahnModule Γ' R V) (s a.1)
                  ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) (t a.2) : HahnModule Γ' R V)) :
              V⟦Γ'⟧))
          a) ⊆
    HVAdd.hVAdd.{u_1, u_2, u_2} (α := Set Γ) (β := Set Γ') (⋃ (a : α), (s a).support) (⋃ (b : β), (t b).support)

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

Premises used: Set.Subset.trans, Set.iUnion_mono
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid R
inst_4 : SMulWithZero R V
inst_5 : VAdd Γ Γ'
inst_6 : IsOrderedCancelVAdd Γ Γ'
s : α → R⟦Γ⟧
t : β → V⟦Γ'⟧
hs : Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), (s a).support)
ht : Set.IsPWO.{u_2} (α := Γ') (⋃ (b : β), (t b).support)
hsupp :
  ∀ (ab : α × β),
    support.{u_2, u_4} (R := V)
        ((fun (ab : α × β) ↦
            ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
                (HSMul.hSMul (β := HahnModule Γ' R V) (s ab.1)
                  ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) (t ab.2) : HahnModule Γ' R V)) :
              V⟦Γ'⟧))
          ab) ⊆
      (s ab.1).support +ᵥ (t ab.2).support
simp_all :
  ∀
    (hsupp :
      ∀ (a : α) (b : β),
        support.{u_2, u_4} (R := V)
            ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
              (HSMul.hSMul (β := HahnModule Γ' R V) (s a)
                ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) (t b) : HahnModule Γ' R V))) ⊆
          (s a).support +ᵥ (t b).support)
    (a : α) (b : β),
    (s a).support +ᵥ (t b).support ⊆
      HVAdd.hVAdd.{u_1, u_2, u_2} (α := Set Γ) (β := Set Γ') (⋃ (a : α), (s a).support) (⋃ (b : β), (t b).support)
⊢ ⋃ (i : α × β), (s i.1).support +ᵥ (t i.2).support ⊆
    HVAdd.hVAdd.{u_1, u_2, u_2} (α := Set Γ) (β := Set Γ') (⋃ (a : α), (s a).support) (⋃ (b : β), (t b).support)

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

Premises used: Set.iUnion_subset_iff, Prod.forall