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 : 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 :
  ∀ (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)

Tactic:
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)

Premises used: Set.vadd_subset_vadd, Set.subset_iUnion_of_subset
-- 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 :
  ∀ (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)

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)

Premises used: Set.vadd_subset_vadd, Set.subset_iUnion_of_subset
-- 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 : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
apply :
  Subset (α := Set (α × β))
    {x : α × β |
      match (motive := α × β → Prop) x with
      | ab =>
        Ne.{u_4 + 1} (α := V)
          (HahnSeries.coeff
            ((fun (ab : α × β) ↦
                ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
                    (HSMul.hSMul (α := R⟦Γ⟧) (β := HahnModule Γ' R V) ((s : (a : α) → R⟦Γ⟧) ab.1 : R⟦Γ⟧)
                      ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) ((t : (a : β) → V⟦Γ'⟧) ab.2) : HahnModule Γ' R V)) :
                  V⟦Γ'⟧))
              ab)
            g)
          0}
    (⋃
      i ∈
        (↑(VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
              ⋃ (a : β), support.{u_2, u_4} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯) :
          Set (Γ × Γ')),
      Function.support (M := V) fun (i_1 : α × β) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i_1.1) i.1)
          (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i_1.2) i.2))
⊢ Finite
    (↑{x : α × β |
          match (motive := α × β → Prop) x with
          | ab =>
            Ne.{u_4 + 1} (α := V)
              (HahnSeries.coeff
                ((fun (ab : α × β) ↦
                    ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
                        (HSMul.hSMul (α := R⟦Γ⟧) (β := HahnModule Γ' R V) ((s : (a : α) → R⟦Γ⟧) ab.1 : R⟦Γ⟧)
                          ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) ((t : (a : β) → V⟦Γ'⟧) ab.2) : HahnModule Γ' R V)) :
                      V⟦Γ'⟧))
                  ab)
                g)
              0} :
      Type (max u_5 u_6))

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

Premises used: Set.Finite.biUnion', Finset.VAddAntidiagonal, HahnSeries.SummableFamily.isPWO_iUnion_support, Set.VAddAntidiagonal.finite_of_isPWO, Set.Finite.subset, HahnSeries.SummableFamily.hasFiniteSupport_smul, Finset.finite_toSet
-- 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 : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
ab : α × β
hab :
  ¬Eq.{u_4 + 1} (α := V)
      (HahnSeries.coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
          (HSMul.hSMul (α := R⟦Γ⟧) (β := HahnModule Γ' R V) ((s : (a : α) → R⟦Γ⟧) ab.1 : R⟦Γ⟧)
            ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) ((t : (a : β) → V⟦Γ'⟧) ab.2) : HahnModule Γ' R V)))
        g)
      0
obtain :
  ∀ (ij : Γ × Γ')
    (hij :
      Membership.mem (γ := Finset (Γ × Γ'))
          (VAddAntidiagonal (s := support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) ab.1)) (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 : (a : β) → V⟦Γ'⟧) ab.2))))
            g ⋯)
          ij ∧
        HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) ab.1) ij.1)
            (HahnSeries.coeff
              ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
                ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) ((t : (a : β) → V⟦Γ'⟧) ab.2)))
              ij.2) ≠
          0),
    Membership.mem (γ := Set (α × β))
      (⋃
        i ∈
          (↑(VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
                ⋃ (a : β), support.{u_2, u_4} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯) :
            Set (Γ × Γ')),
        Function.support (M := V) fun (i_1 : α × β) ↦
          HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i_1.1) i.1)
            (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i_1.2) i.2))
      ab
⊢ Membership.mem (γ := Set (α × β))
    (⋃
      i ∈
        (↑(VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
              ⋃ (a : β), support.{u_2, u_4} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯) :
          Set (Γ × Γ')),
      Function.support (M := V) fun (i_1 : α × β) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i_1.1) i.1)
          (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i_1.2) i.2))
    ab

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

Premises used: Finset.exists_ne_zero_of_sum_ne_zero
-- 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 : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
ab : α × β
hab :
  ¬Eq.{u_4 + 1} (α := V)
      (HahnSeries.coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
          (HSMul.hSMul (α := R⟦Γ⟧) (β := HahnModule Γ' R V) ((s : (a : α) → R⟦Γ⟧) ab.1 : R⟦Γ⟧)
            ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) ((t : (a : β) → V⟦Γ'⟧) ab.2) : HahnModule Γ' R V)))
        g)
      0
ij : Γ × Γ'
hij :
  Membership.mem (γ := Finset (Γ × Γ'))
      (VAddAntidiagonal (s := support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) ab.1)) (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 : (a : β) → V⟦Γ'⟧) ab.2))))
        g ⋯)
      ij ∧
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) ab.1) ij.1)
        (HahnSeries.coeff
          ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
            ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) ((t : (a : β) → V⟦Γ'⟧) ab.2)))
          ij.2) ≠
      0
simp :
  ∃ (a : Γ) (b : Γ'),
    ((∃ (i : α), ¬Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) a) 0) ∧
        (∃ (i : β), ¬Eq.{u_4 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i) b) 0) ∧ a +ᵥ b = g) ∧
      ¬HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) ab.1) a)
            (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) ab.2) b) =
          0
⊢ Membership.mem (γ := Set (α × β))
    (⋃
      i ∈
        (↑(VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
              ⋃ (a : β), support.{u_2, u_4} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯) :
          Set (Γ × Γ')),
      Function.support (M := V) fun (i_1 : α × β) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i_1.1) i.1)
          (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i_1.2) i.2))
    ab

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

Premises used: Finset.mem_vaddAntidiagonal, Set.mem_iUnion, exists_prop, ne_eq, Function.mem_support, Prod.exists, Finset.mem_coe, 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 : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
ab : α × β
hab :
  ¬Eq.{u_4 + 1} (α := V)
      (HahnSeries.coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
          (HSMul.hSMul (α := R⟦Γ⟧) (β := HahnModule Γ' R V) ((s : (a : α) → R⟦Γ⟧) ab.1 : R⟦Γ⟧)
            ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) ((t : (a : β) → V⟦Γ'⟧) ab.2) : HahnModule Γ' R V)))
        g)
      0
ij : Γ × Γ'
hij :
  Membership.mem (γ := Finset (Γ × Γ'))
      (VAddAntidiagonal (s := support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) ab.1)) (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 : (a : β) → V⟦Γ'⟧) ab.2))))
        g ⋯)
      ij ∧
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) ab.1) ij.1)
        (HahnSeries.coeff
          ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
            ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) ((t : (a : β) → V⟦Γ'⟧) ab.2)))
          ij.2) ≠
      0
⊢ ∃ (a : Γ) (b : Γ'),
    ((∃ (i : α), ¬Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) a) 0) ∧
        (∃ (i : β), ¬Eq.{u_4 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i) b) 0) ∧ a +ᵥ b = g) ∧
      ¬HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) ab.1) a)
            (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) ab.2) b) =
          0

Tactic:
⟨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⟩

Premises used: right_ne_zero_of_smul, Finset.mem_vaddAntidiagonal, Prod.fst, left_ne_zero_of_smul, And.right, And.left, And.intro, Exists.intro, Iff.mp, 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 : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
ab : α × β
hab :
  ¬Eq.{u_4 + 1} (α := V)
      (HahnSeries.coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
          (HSMul.hSMul (α := R⟦Γ⟧) (β := HahnModule Γ' R V) ((s : (a : α) → R⟦Γ⟧) ab.1 : R⟦Γ⟧)
            ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) ((t : (a : β) → V⟦Γ'⟧) ab.2) : HahnModule Γ' R V)))
        g)
      0
ij : Γ × Γ'
hij :
  Membership.mem (γ := Finset (Γ × Γ'))
      (VAddAntidiagonal (s := support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) ab.1)) (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 : (a : β) → V⟦Γ'⟧) ab.2))))
        g ⋯)
      ij ∧
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) ab.1) ij.1)
        (HahnSeries.coeff
          ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
            ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) ((t : (a : β) → V⟦Γ'⟧) ab.2)))
          ij.2) ≠
      0
⊢ ∃ (a : Γ) (b : Γ'),
    ((∃ (i : α), ¬Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) a) 0) ∧
        (∃ (i : β), ¬Eq.{u_4 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i) b) 0) ∧ a +ᵥ b = g) ∧
      ¬HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) ab.1) a)
            (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) ab.2) 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⟩
-- 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 : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
⊢ Subset (α := Set (α × β))
    {x : α × β |
      match (motive := α × β → Prop) x with
      | ab =>
        Ne.{u_4 + 1} (α := V)
          (HahnSeries.coeff
            ((fun (ab : α × β) ↦
                ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
                    (HSMul.hSMul (α := R⟦Γ⟧) (β := HahnModule Γ' R V) ((s : (a : α) → R⟦Γ⟧) ab.1 : R⟦Γ⟧)
                      ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) ((t : (a : β) → V⟦Γ'⟧) ab.2) : HahnModule Γ' R V)) :
                  V⟦Γ'⟧))
              ab)
            g)
          0}
    (⋃
      i ∈
        (↑(VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
              ⋃ (a : β), support.{u_2, u_4} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯) :
          Set (Γ × Γ')),
      Function.support (M := V) fun (i_1 : α × β) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i_1.1) i.1)
          (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i_1.2) i.2))

Tactic:
exact fun ab hab => by
    simp only [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⟩
-- 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 : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
⊢ Eq.{u_4 + 1} (α := V)
    (∑
      x ∈
        VAddAntidiagonal (s := Function.support.{u_1, u_3} (M := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a.1))) (t :=
          Function.support.{u_2, u_4} (M := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) a.2))) g ⋯,
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a.1) x.1)
        (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) a.2) x.2))
    (∑ x ∈ VAddAntidiagonal (s := ⋃ (a : α), (s.toFun a).support) (t := ⋃ (a : β), (t.toFun a).support) g ⋯,
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a.1) x.1)
        (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) a.2) x.2))

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

Premises used: Finset.sum_subset
-- 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 : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
refine_1 :
  ∀ (gh : Γ × Γ')
    (hgh :
      Membership.mem (γ := Finset (Γ × Γ'))
        (VAddAntidiagonal (s := Function.support.{u_1, u_3} (M := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a.1)))
          (t := Function.support.{u_2, u_4} (M := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) a.2))) g ⋯)
        gh),
    gh ∈ VAddAntidiagonal (s := ⋃ (a : α), (s.toFun a).support) (t := ⋃ (a : β), (t.toFun a).support) g ⋯
refine_2 :
  ∀ (gh : Γ × Γ')
    (hgh : gh ∈ VAddAntidiagonal (s := ⋃ (a : α), (s.toFun a).support) (t := ⋃ (a : β), (t.toFun a).support) g ⋯)
    (h :
      gh ∉
        VAddAntidiagonal (s := Function.support.{u_1, u_3} (M := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a.1))) (t :=
          Function.support.{u_2, u_4} (M := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) a.2))) g ⋯),
    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
⊢ Eq.{u_4 + 1} (α := V)
    (∑
      x ∈
        VAddAntidiagonal (s := Function.support.{u_1, u_3} (M := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a.1))) (t :=
          Function.support.{u_2, u_4} (M := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) a.2))) g ⋯,
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a.1) x.1)
        (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) a.2) x.2))
    (∑ x ∈ VAddAntidiagonal (s := ⋃ (a : α), (s.toFun a).support) (t := ⋃ (a : β), (t.toFun a).support) g ⋯,
      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a.1) x.1)
        (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) a.2) x.2))

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

Premises used: Finset.sum_subset
-- 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 : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
gh : Γ × Γ'
hgh :
  Membership.mem (γ := Finset (Γ × Γ'))
    (VAddAntidiagonal (s := Function.support.{u_1, u_3} (M := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a.1))) (t :=
      Function.support.{u_2, u_4} (M := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) a.2))) g ⋯)
    gh
refine_1 :
  ∀
    (hgh :
      Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a.1) gh.1) 0 ∧
        Ne.{u_4 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) a.2) 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
⊢ gh ∈ VAddAntidiagonal (s := ⋃ (a : α), (s.toFun a).support) (t := ⋃ (a : β), (t.toFun a).support) g ⋯

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

Premises used: Finset.mem_vaddAntidiagonal, Set.mem_iUnion, Function.mem_support, 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 : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
gh : Γ × Γ'
hgh :
  Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a.1) gh.1) 0 ∧
    Ne.{u_4 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) a.2) 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:
⟨Exists.intro a.1 hgh.1, Exists.intro a.2 hgh.2.1, trivial⟩

Premises used: trivial, Prod.fst, And.right, And.left, And.intro, Exists.intro, 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 : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
gh : Γ × Γ'
hgh :
  Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a.1) gh.1) 0 ∧
    Ne.{u_4 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) a.2) 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⟩
-- 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 : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
a : α × β
gh : Γ × Γ'
hgh : gh ∈ VAddAntidiagonal (s := ⋃ (a : α), (s.toFun a).support) (t := ⋃ (a : β), (t.toFun a).support) g ⋯
h :
  gh ∉
    VAddAntidiagonal (s := Function.support.{u_1, u_3} (M := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a.1))) (t :=
      Function.support.{u_2, u_4} (M := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) a.2))) g ⋯
pos :
  ∀ (hs : Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a.1) gh.1) 0),
    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
neg :
  ∀ (hs : ¬Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a.1) gh.1) 0),
    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
⊢ 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

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

Premises used: Prod.fst, HahnSeries.coeff, DFunLike.coe