awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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
⊢ 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
have 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
Tactic: simp only [mem_coe, mem_vaddAntidiagonal, Set.mem_iUnion, mem_support, ne_eq,
      Function.mem_support, exists_prop, Prod.exists]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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))
have 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 sorry)
      gh),
  gh ∈ VAddAntidiagonal (s := ⋃ (a : α), (s.toFun a).support) (t := ⋃ (a : β), (t.toFun a).support) g sorry
Tactic: refine sum_subset (fun gh hgh => ?_) fun gh hgh h => ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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 ⋯
⊢ 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))
have refine_2 : ∀ (gh : Γ × Γ')
  (hgh : gh ∈ VAddAntidiagonal (s := ⋃ (a : α), (s.toFun a).support) (t := ⋃ (a : β), (t.toFun a).support) g sorry)
  (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 sorry),
  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: refine sum_subset (fun gh hgh => ?_) fun gh hgh h => ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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
⊢ gh ∈ VAddAntidiagonal (s := ⋃ (a : α), (s.toFun a).support) (t := ⋃ (a : β), (t.toFun a).support) g ⋯
have 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
Tactic: simp_all only [mem_vaddAntidiagonal, Function.mem_support, Set.mem_iUnion, mem_support]
Cleared hypotheses: hgh
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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 ⋯
⊢ 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
have 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
Tactic: by_cases hs : (s a.1).coeff gh.1 = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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
⊢ 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
have 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
Tactic: by_cases hs : (s a.1).coeff gh.1 = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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) (∑ᶠ (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)
have 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 sorry,
      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 sorry,
    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 only [coeff_hsum_eq_sum, smul_toFun, HahnModule.coeff_smul, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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)
    (∑ᶠ (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))
have simp_rw : Eq.{u_8 + 1} (α := V)
  (∑ᶠ (i : α × β),
    ∑ x ∈ VAddAntidiagonal (s := ⋃ (a : α), (s.toFun a).support) (t := ⋃ (a : β), (t.toFun a).support) g sorry,
      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 sorry,
    ∑ 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: simp_rw [sum_vAddAntidiagonal_eq, Finset.smul_sum, Finset.sum_smul]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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)
    (∑ᶠ (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))
have rw : Eq.{u_8 + 1} (α := V)
  (∑ a ∈ VAddAntidiagonal (s := ⋃ (a : α), (s.toFun a).support) (t := ⋃ (a : β), (t.toFun a).support) g sorry,
    ∑ᶠ (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 sorry,
    ∑ 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]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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))
have 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 sorry,
  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: refine sum_congr rfl fun gh _ => ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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 ⋯
⊢ 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))
have 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))
        sorry,
    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: rw [finsum_eq_sum _ (hasFiniteSupport_smul s t gh), ← sum_product_right']
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
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 ⋯
⊢ 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))
have 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))
        sorry),
  ab ∈ (s.coeff gh.1).support ×ˢ (t.coeff gh.2).support
Tactic: refine sum_subset (fun ab hab => ?_) (fun ab _ hab => by simp_all)
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
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))
      ⋯
⊢ ab ∈ (s.coeff gh.1).support ×ˢ (t.coeff gh.2).support
have 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})
        sorry) :
    Set (α × β))
Tactic: have hsupp := smul_support_subset_prod s t gh