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 : 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 ⋯
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

Tactic:
smul_eq_zero_of_left hs ((t a.2).coeff gh.2)

Premises used: smul_eq_zero_of_left, HahnSeries.coeff, Prod.snd, DFunLike.coe
-- 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 ⋯
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

Tactic:
exact smul_eq_zero_of_left hs ((t a.2).coeff gh.2)

Premises used: smul_eq_zero_of_left, HahnSeries.coeff, Prod.snd, DFunLike.coe
-- 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 ⋯
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

Tactic:
simp_all
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
simp :
  Eq.{u_8 + 1} (α := V)
    (∑ᶠ (i : α × β),
      ∑
        x ∈
          VAddAntidiagonal (s := support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) i.1)) (t :=
            support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) i.2)) g ⋯,
        HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i.1) x.1)
          (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i.2) x.2))
    (∑
      x ∈
        VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
          ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯,
      HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V)
        (∑ i ∈ (s.coeff x.1).support, HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1)
        (∑ i ∈ (t.coeff x.2).support, HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i) x.2))
⊢ Eq.{u_8 + 1} (α := V) (∑ᶠ (i : α × β), HahnSeries.coeff ((s.smul t : (a : α × β) → V⟦Γ'⟧) i) g)
    (∑
      gh ∈
        VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
          ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯,
      s.hsum.coeff gh.1 • t.hsum.coeff gh.2)

Tactic:
simp only [coeff_hsum_eq_sum, smul_toFun, HahnModule.coeff_smul, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, HahnSeries.SummableFamily.smul_toFun, HahnModule.coeff_smul, HahnSeries.SummableFamily.coeff_hsum_eq_sum
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
simp_rw :
  Eq.{u_8 + 1} (α := V)
    (∑ᶠ (i : α × β),
      ∑ x ∈ VAddAntidiagonal (s := ⋃ (a : α), (s.toFun a).support) (t := ⋃ (a : β), (t.toFun a).support) g ⋯,
        HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i.1) x.1)
          (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i.2) x.2))
    (∑
      x ∈
        VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
          ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯,
      ∑ x_1 ∈ (t.coeff x.2).support,
        ∑ i ∈ (s.coeff x.1).support,
          HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1)
            (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) x_1) x.2))
⊢ Eq.{u_8 + 1} (α := V)
    (∑ᶠ (i : α × β),
      ∑
        x ∈
          VAddAntidiagonal (s := support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) i.1)) (t :=
            support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) i.2)) g ⋯,
        HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i.1) x.1)
          (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i.2) x.2))
    (∑
      x ∈
        VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
          ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯,
      HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V)
        (∑ i ∈ (s.coeff x.1).support, HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1)
        (∑ i ∈ (t.coeff x.2).support, HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i) x.2))

Tactic:
simp_rw [sum_vAddAntidiagonal_eq, Finset.smul_sum, Finset.sum_smul]

Premises used: Finset.sum_smul, HahnSeries.SummableFamily.sum_vAddAntidiagonal_eq, Finset.smul_sum
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
rw :
  Eq.{u_8 + 1} (α := V)
    (∑ a ∈ VAddAntidiagonal (s := ⋃ (a : α), (s.toFun a).support) (t := ⋃ (a : β), (t.toFun a).support) g ⋯,
      ∑ᶠ (b : α × β),
        HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) b.1) a.1)
          (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) b.2) a.2))
    (∑
      x ∈
        VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
          ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯,
      ∑ x_1 ∈ (t.coeff x.2).support,
        ∑ i ∈ (s.coeff x.1).support,
          HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1)
            (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) x_1) x.2))
⊢ Eq.{u_8 + 1} (α := V)
    (∑ᶠ (i : α × β),
      ∑ x ∈ VAddAntidiagonal (s := ⋃ (a : α), (s.toFun a).support) (t := ⋃ (a : β), (t.toFun a).support) g ⋯,
        HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i.1) x.1)
          (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i.2) x.2))
    (∑
      x ∈
        VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
          ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯,
      ∑ x_1 ∈ (t.coeff x.2).support,
        ∑ i ∈ (s.coeff x.1).support,
          HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1)
            (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) x_1) x.2))

Tactic:
rw [← sum_finsum_comm _ _ <| fun gh _ => hasFiniteSupport_smul s t gh]

Premises used: sum_finsum_comm, HahnSeries.SummableFamily.hasFiniteSupport_smul
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
⊢ Eq.{u_8 + 1} (α := V)
    (∑ a ∈ VAddAntidiagonal (s := ⋃ (a : α), (s.toFun a).support) (t := ⋃ (a : β), (t.toFun a).support) g ⋯,
      ∑ᶠ (b : α × β),
        HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) b.1) a.1)
          (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) b.2) a.2))
    (∑
      x ∈
        VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
          ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯,
      ∑ x_1 ∈ (t.coeff x.2).support,
        ∑ i ∈ (s.coeff x.1).support,
          HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1)
            (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) x_1) x.2))

Tactic:
sum_congr rfl fun gh _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
refine :
  ∀
    gh ∈
      VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
        ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯,
    Eq.{u_8 + 1} (α := V)
      (∑ᶠ (b : α × β),
        HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) b.1) gh.1)
          (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) b.2) gh.2))
      (∑ x ∈ (t.coeff gh.2).support,
        ∑ i ∈ (s.coeff gh.1).support,
          HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) gh.1)
            (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) x) gh.2))
⊢ Eq.{u_8 + 1} (α := V)
    (∑ a ∈ VAddAntidiagonal (s := ⋃ (a : α), (s.toFun a).support) (t := ⋃ (a : β), (t.toFun a).support) g ⋯,
      ∑ᶠ (b : α × β),
        HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) b.1) a.1)
          (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) b.2) a.2))
    (∑
      x ∈
        VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
          ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯,
      ∑ x_1 ∈ (t.coeff x.2).support,
        ∑ i ∈ (s.coeff x.1).support,
          HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1)
            (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) x_1) x.2))

Tactic:
refine sum_congr rfl fun gh _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
gh : Γ × Γ'
h :
  gh ∈
    VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
      ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯
rw :
  Eq.{u_8 + 1} (α := V)
    (∑
      i ∈
        Set.Finite.toFinset (s :=
          Function.support (M := V) fun (i : α × β) ↦
            HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i.1) gh.1)
              (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i.2) gh.2))
          ⋯,
      HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i.1) gh.1)
        (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i.2) gh.2))
    (∑ x ∈ (s.coeff gh.1).support ×ˢ (t.coeff gh.2).support,
      HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) x.1) gh.1)
        (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) x.2) gh.2))
⊢ Eq.{u_8 + 1} (α := V)
    (∑ᶠ (b : α × β),
      HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) b.1) gh.1)
        (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) b.2) gh.2))
    (∑ x ∈ (t.coeff gh.2).support,
      ∑ i ∈ (s.coeff gh.1).support,
        HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) gh.1)
          (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) x) gh.2))

Tactic:
rw [finsum_eq_sum _ (hasFiniteSupport_smul s t gh), ← sum_product_right']

Premises used: finsum_eq_sum, HahnSeries.SummableFamily.hasFiniteSupport_smul, Finset.sum_product_right'
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
gh : Γ × Γ'
h :
  gh ∈
    VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
      ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯
ab : α × β
h_1 : ab ∈ (s.coeff gh.1).support ×ˢ (t.coeff gh.2).support
hab :
  ab ∉
    Set.Finite.toFinset (s :=
      Function.support (M := V) fun (i : α × β) ↦
        HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i.1) gh.1)
          (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i.2) gh.2))
      ⋯
⊢ HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) ab.1) gh.1)
      (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) ab.2) gh.2) =
    0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
gh : Γ × Γ'
h :
  gh ∈
    VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
      ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯
refine :
  ∀ (ab : α × β)
    (hab :
      ab ∈
        Set.Finite.toFinset (s :=
          Function.support (M := V) fun (i : α × β) ↦
            HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i.1) gh.1)
              (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i.2) gh.2))
          ⋯),
    ab ∈ (s.coeff gh.1).support ×ˢ (t.coeff gh.2).support
⊢ Eq.{u_8 + 1} (α := V)
    (∑
      i ∈
        Set.Finite.toFinset (s :=
          Function.support (M := V) fun (i : α × β) ↦
            HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i.1) gh.1)
              (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i.2) gh.2))
          ⋯,
      HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i.1) gh.1)
        (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i.2) gh.2))
    (∑ x ∈ (s.coeff gh.1).support ×ˢ (t.coeff gh.2).support,
      HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) x.1) gh.1)
        (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) x.2) gh.2))

Tactic:
refine sum_subset (fun ab hab => ?_) (fun ab _ hab => by simp_all)

Premises used: Finset.sum_subset
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
gh : Γ × Γ'
h :
  gh ∈
    VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
      ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯
ab : α × β
hab :
  ab ∈
    Set.Finite.toFinset (s :=
      Function.support (M := V) fun (i : α × β) ↦
        HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i.1) gh.1)
          (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i.2) gh.2))
      ⋯
⊢ (Function.support (M := V) fun (i : α × β) ↦
      HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i.1) gh.1)
        (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i.2) gh.2)) ⊆
    (↑(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:
have hsupp := smul_support_subset_prod s t gh
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
gh : Γ × Γ'
h :
  gh ∈
    VAddAntidiagonal (s := ⋃ (a : α), support.{u_1, u_7} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
      ⋃ (a : β), support.{u_2, u_8} (R := V) ((t : (a : β) → V⟦Γ'⟧) a)) g ⋯
ab : α × β
hab :
  ab ∈
    Set.Finite.toFinset (s :=
      Function.support (M := V) fun (i : α × β) ↦
        HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i.1) gh.1)
          (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i.2) gh.2))
      ⋯
hsupp :
  (Function.support (M := V) fun (i : α × β) ↦
      HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i.1) gh.1)
        (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i.2) gh.2)) ⊆
    (↑(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 (α × β))
simp_all :
  (∃ (i : α), ¬Eq.{u_7 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) gh.1) 0) ∧
      (∃ (i : β), ¬Eq.{u_8 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i) gh.2) 0) ∧ gh.1 +ᵥ gh.2 = g →
    ∀
      (hab :
        ¬HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) ab.1) gh.1)
              (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) ab.2) gh.2) =
            0)
      (hsupp :
        ∀ (a : α) (b : β),
          ¬HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) gh.1)
                  (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) b) gh.2) =
                0 →
            ¬(s.toFun a).coeff gh.1 = 0 ∧ ¬(t.toFun b).coeff gh.2 = 0),
      ¬Eq.{u_7 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) ab.1) gh.1) 0 ∧
        ¬Eq.{u_8 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) ab.2) gh.2) 0
⊢ ab ∈ (s.coeff gh.1).support ×ˢ (t.coeff gh.2).support

Tactic:
simp_all only [mem_vaddAntidiagonal, Set.mem_iUnion, mem_support, ne_eq, Set.Finite.mem_toFinset,
    Function.mem_support, Set.Finite.coe_toFinset, support_subset_iff, Set.mem_prod,
    Set.mem_setOf_eq, Prod.forall, coeff_support, mem_product]

Premises used: Set.Finite.mem_toFinset, Finset.mem_vaddAntidiagonal, Set.mem_iUnion, HahnSeries.SummableFamily.coeff_support, Set.Finite.coe_toFinset, Set.mem_setOf_eq, ne_eq, Set.mem_prod, Function.support_subset_iff, Function.mem_support, Prod.forall, Finset.mem_product, HahnSeries.mem_support
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
gh : Γ × Γ'
ab : α × β
h :
  (∃ (i : α), ¬Eq.{u_7 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) gh.1) 0) ∧
    (∃ (i : β), ¬Eq.{u_8 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i) gh.2) 0) ∧ gh.1 +ᵥ gh.2 = g
hab :
  ¬HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) ab.1) gh.1)
        (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) ab.2) gh.2) =
      0
hsupp :
  ∀ (a : α) (b : β),
    ¬HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) gh.1)
            (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) b) gh.2) =
          0 →
      ¬(s.toFun a).coeff gh.1 = 0 ∧ ¬(t.toFun b).coeff gh.2 = 0
⊢ ¬Eq.{u_7 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) ab.1) gh.1) 0 ∧
    ¬Eq.{u_8 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) ab.2) gh.2) 0

Tactic:
hsupp ab.1 ab.2 hab

Premises used: Prod.fst, Prod.snd
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
gh : Γ × Γ'
ab : α × β
h :
  (∃ (i : α), ¬Eq.{u_7 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) gh.1) 0) ∧
    (∃ (i : β), ¬Eq.{u_8 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i) gh.2) 0) ∧ gh.1 +ᵥ gh.2 = g
hab :
  ¬HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) ab.1) gh.1)
        (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) ab.2) gh.2) =
      0
hsupp :
  ∀ (a : α) (b : β),
    ¬HSMul.hSMul.{u_7, u_8, u_8} (α := R) (β := V) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) gh.1)
            (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) b) gh.2) =
          0 →
      ¬(s.toFun a).coeff gh.1 = 0 ∧ ¬(t.toFun b).coeff gh.2 = 0
⊢ ¬Eq.{u_7 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) ab.1) gh.1) 0 ∧
    ¬Eq.{u_8 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) ab.2) gh.2) 0

Tactic:
exact hsupp ab.1 ab.2 hab

Premises used: Prod.fst, Prod.snd
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst_4 : Semiring R
inst_5 : AddCommMonoid V
inst_6 : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
coeff :
  ∀ (g : Γ'),
    (s.smul t).hsum.coeff g =
      HahnSeries.coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
          (HSMul.hSMul (β := HahnModule Γ' R V) s.hsum
            ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) t.hsum : HahnModule Γ' R V)))
        g
⊢ (s.smul t).hsum =
    (Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (β := HahnModule Γ' R V) s.hsum
        ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) t.hsum : HahnModule Γ' R V))

Tactic:
ext g