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
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
⊢ 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 (α × β))
have 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
Tactic: simp_all only [Function.mem_support, ne_eq, Set.Finite.coe_toFinset, Set.mem_prod,
    Set.mem_setOf_eq]
Cleared hypotheses: hab
-- 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 : α → R⟦Γ⟧
t : β → V⟦Γ'⟧
hs : Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), (s a).support)
ht : Set.IsPWO.{u_2} (α := Γ') (⋃ (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))
have 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)
Tactic: apply (hs.vadd ht).mono
-- 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 : α → 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
have 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 sorry).Nonempty} x
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)
-- 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 : α → 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
⊢ (VAddAntidiagonal (s := (s ab.1).support) (t := (t ab.2).support) x ⋯).Nonempty
have contrapose! : ∀ (hx : VAddAntidiagonal (s := (s ab.1).support) (t := (t ab.2).support) x sorry = ∅),
  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: contrapose! hx
Cleared hypotheses: hx
-- 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 : α → 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 ⋯ = ∅
⊢ 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)))
have 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
Tactic: rw [mem_support, not_not, HahnModule.coeff_smul, hx, sum_empty]
-- 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 : α → 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
⊢ 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)))
have 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
Tactic: rw [mem_support, not_not, HahnModule.coeff_smul, hx, sum_empty]
-- 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 : α → 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
⊢ 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)))
have 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 sorry,
    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
Tactic: rw [mem_support, not_not, HahnModule.coeff_smul, hx, sum_empty]
-- 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 : α → 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
⊢ 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)))
have 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
Tactic: rw [mem_support, not_not, HahnModule.coeff_smul, hx, sum_empty]
-- 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 : α → 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
⊢ 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)))
have rw₄ : Eq.{u_4 + 1} (α := V) 0 0
Tactic: rw [mem_support, not_not, HahnModule.coeff_smul, hx, sum_empty]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
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)
⊢ ⋃ (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)
have 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
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]
-- 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 : α → 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)
have 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)
Tactic: refine Set.Subset.trans (Set.iUnion_mono fun a => (hsupp a)) ?_
-- 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 : α → 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
⊢ ⋃ (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)
have 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)
Tactic: simp_all only [Set.iUnion_subset_iff, Prod.forall]
Cleared hypotheses: hsupp
-- 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 : Γ'
⊢ 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))
have apply : Subset (α := Set (α × β))
  {x : Prod.{u_5, u_6} α β |
    match (motive := Prod.{u_5, u_6} α β → 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 sorry) :
        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: 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 _
-- 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
⊢ 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 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 sorry)
        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 sorry) :
          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