awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ⋯
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 (α × β))
⊢ ab ∈ (s.coeff gh.1).support ×ˢ (t.coeff gh.2).support
have 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
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]
Cleared hypotheses: h, hab, hsupp
-- 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 β
⊢ (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))
have 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
Tactic: ext g
-- 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 : Γ'
⊢ (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
have coeff : Eq.{u_8 + 1} (α := V)
  (∑
    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,
    s.hsum.coeff gh.1 • t.hsum.coeff gh.2)
  (∑ ij ∈ VAddAntidiagonal (s := s.hsum.support) (t := t.hsum.support) g sorry, s.hsum.coeff ij.1 • t.hsum.coeff ij.2)
Tactic: rw [coeff_smul s t g, 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)
    (∑
      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)
    (∑ ij ∈ VAddAntidiagonal (s := s.hsum.support) (t := t.hsum.support) g ⋯, s.hsum.coeff ij.1 • t.hsum.coeff ij.2)
have coeff : ∀ (x : Γ × Γ') (hgh : x ∈ (↑(VAddAntidiagonal (s := s.hsum.support) (t := t.hsum.support) g sorry) : Set (Γ × Γ'))),
  (fun (a : Γ × Γ') ↦ a) 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) :
      Set (Γ × Γ'))
Tactic: refine Eq.symm (sum_of_injOn (fun a ↦ a) (fun _ _ _ _ h ↦ h) (fun _ hgh => ?_)
    (fun gh _ hgh => ?_) fun _ _ => by simp)
-- 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 : Γ'
coeff :
  ∀ (x : Γ × Γ') (hgh : x ∈ (↑(VAddAntidiagonal (s := s.hsum.support) (t := t.hsum.support) g ⋯) : Set (Γ × Γ'))),
    (fun (a : Γ × Γ') ↦ a) 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 ⋯) :
        Set (Γ × Γ'))
⊢ Eq.{u_8 + 1} (α := V)
    (∑
      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)
    (∑ ij ∈ VAddAntidiagonal (s := s.hsum.support) (t := t.hsum.support) g ⋯, s.hsum.coeff ij.1 • t.hsum.coeff ij.2)
have coeff₁ : ∀
  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,
  ∀
    (hgh :
      gh ∉
        (fun (a : Γ × Γ') ↦ a) '' (↑(VAddAntidiagonal (s := s.hsum.support) (t := t.hsum.support) g sorry) : Set (Γ × Γ'))),
    s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0
Tactic: refine Eq.symm (sum_of_injOn (fun a ↦ a) (fun _ _ _ _ h ↦ h) (fun _ hgh => ?_)
    (fun gh _ hgh => ?_) fun _ _ => by simp)
-- 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 : Γ'
x : Γ × Γ'
hgh : x ∈ (↑(VAddAntidiagonal (s := s.hsum.support) (t := t.hsum.support) g ⋯) : Set (Γ × Γ'))
⊢ (fun (a : Γ × Γ') ↦ a) 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 ⋯) :
      Set (Γ × Γ'))
have coeff : ∀ (hgh : ¬s.hsum.coeff x.1 = 0 ∧ ¬t.hsum.coeff x.2 = 0 ∧ x.1 +ᵥ x.2 = g),
  (∃ (i : α), ¬Eq.{u_7 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1) 0) ∧
    ∃ (i : β), ¬Eq.{u_8 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i) x.2) 0
Tactic: simp_all only [mem_coe, mem_vaddAntidiagonal, mem_support, ne_eq, Set.mem_iUnion, and_true]
Cleared hypotheses: hgh
-- 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 : Γ'
x : Γ × Γ'
hgh : ¬s.hsum.coeff x.1 = 0 ∧ ¬t.hsum.coeff x.2 = 0 ∧ x.1 +ᵥ x.2 = g
⊢ (∃ (i : α), ¬Eq.{u_7 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1) 0) ∧
    ∃ (i : β), ¬Eq.{u_8 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i) x.2) 0
have coeff : ∃ (i : α), ¬Eq.{u_7 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1) 0
Tactic: constructor
-- 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 : Γ'
x : Γ × Γ'
hgh : ¬s.hsum.coeff x.1 = 0 ∧ ¬t.hsum.coeff x.2 = 0 ∧ x.1 +ᵥ x.2 = g
coeff : ∃ (i : α), ¬Eq.{u_7 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1) 0
⊢ (∃ (i : α), ¬Eq.{u_7 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1) 0) ∧
    ∃ (i : β), ¬Eq.{u_8 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i) x.2) 0
have coeff₁ : ∃ (i : β), ¬Eq.{u_8 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i) x.2) 0
Tactic: constructor
-- 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 : Γ'
x : Γ × Γ'
hgh : ¬s.hsum.coeff x.1 = 0 ∧ ¬t.hsum.coeff x.2 = 0 ∧ x.1 +ᵥ x.2 = g
⊢ ∃ (i : α), ¬Eq.{u_7 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1) 0
have hgh₁ : ¬Eq.{u_7 + 1} (α := R) (∑ i ∈ (s.coeff x.1).support, HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1) 0 ∧
  ¬t.hsum.coeff x.2 = 0 ∧ x.1 +ᵥ x.2 = g
Tactic: rw [coeff_hsum_eq_sum] at hgh
Cleared hypotheses: hgh
-- 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 : Γ'
x : Γ × Γ'
hgh :
  ¬Eq.{u_7 + 1} (α := R) (∑ i ∈ (s.coeff x.1).support, HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1) 0 ∧
    ¬t.hsum.coeff x.2 = 0 ∧ x.1 +ᵥ x.2 = g
⊢ ∃ (i : α), ¬Eq.{u_7 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) x.1) 0
have h' : ∃ a ∈ (s.coeff x.1).support, Ne.{u_7 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) x.1) 0
Tactic: have h' := Finset.exists_ne_zero_of_sum_ne_zero hgh.1
-- 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 : Γ'
x : Γ × Γ'
hgh : ¬s.hsum.coeff x.1 = 0 ∧ ¬t.hsum.coeff x.2 = 0 ∧ x.1 +ᵥ x.2 = g
⊢ ∃ (i : β), ¬Eq.{u_8 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i) x.2) 0
have coeff : ∀ (hi : ¬∃ (i : β), ¬Eq.{u_8 + 1} (α := V) (HahnSeries.coeff ((t : (a : β) → V⟦Γ'⟧) i) x.2) 0), False
Tactic: by_contra hi
-- 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 ⋯
hgh :
  gh ∉ (fun (a : Γ × Γ') ↦ a) '' (↑(VAddAntidiagonal (s := s.hsum.support) (t := t.hsum.support) g ⋯) : Set (Γ × Γ'))
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0
have hgh₁ : ¬s.hsum.coeff gh.1 = 0 → ¬t.hsum.coeff gh.2 = 0 → ¬gh.1 +ᵥ gh.2 = g
Tactic: simp only [Set.image_id', mem_coe, mem_vaddAntidiagonal, mem_support, ne_eq, not_and] at hgh
Cleared hypotheses: hgh
-- 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 ⋯
hgh : ¬s.hsum.coeff gh.1 = 0 → ¬t.hsum.coeff gh.2 = 0 → ¬gh.1 +ᵥ gh.2 = g
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0
have pos : ∀ (h : s.hsum.coeff gh.1 = 0), s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0
Tactic: by_cases h : s.hsum.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 : Γ'
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 ⋯
hgh : ¬s.hsum.coeff gh.1 = 0 → ¬t.hsum.coeff gh.2 = 0 → ¬gh.1 +ᵥ gh.2 = g
pos : ∀ (h : s.hsum.coeff gh.1 = 0), s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0
have neg : ∀ (h : ¬s.hsum.coeff gh.1 = 0), s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0
Tactic: by_cases h : s.hsum.coeff gh.1 = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
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
x : R⟦Γ⟧
s : SummableFamily Γ' V α
⊢ (x • s).hsum =
    (Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V))
have rw : (Equiv (Equiv.punitProd α) ((const Unit x).smul s)).hsum =
  (Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
    (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V))
Tactic: rw [smul_eq, hsum_equiv, smul_hsum, hsum_unique, const_toFun]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
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
x : R⟦Γ⟧
s : SummableFamily Γ' V α
rw :
  (Equiv (Equiv.punitProd α) ((const Unit x).smul s)).hsum =
    (Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V))
⊢ (x • s).hsum =
    (Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V))
have rw₁ : ((const Unit x).smul s).hsum =
  (Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
    (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V))
Tactic: rw [smul_eq, hsum_equiv, smul_hsum, hsum_unique, const_toFun]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
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
x : R⟦Γ⟧
s : SummableFamily Γ' V α
rw :
  (Equiv (Equiv.punitProd α) ((const Unit x).smul s)).hsum =
    (Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V))
rw₁ :
  ((const Unit x).smul s).hsum =
    (Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V))
⊢ (x • s).hsum =
    (Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V))
have rw₂ : Eq (α := V⟦Γ'⟧)
  ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (β := HahnModule Γ' R V) (const Unit x).hsum
        ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V)) :
    V⟦Γ'⟧)
  ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V)) :
    V⟦Γ'⟧)
Tactic: rw [smul_eq, hsum_equiv, smul_hsum, hsum_unique, const_toFun]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
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
x : R⟦Γ⟧
s : SummableFamily Γ' V α
rw :
  (Equiv (Equiv.punitProd α) ((const Unit x).smul s)).hsum =
    (Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V))
rw₁ :
  ((const Unit x).smul s).hsum =
    (Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V))
rw₂ :
  Eq (α := V⟦Γ'⟧)
    ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (β := HahnModule Γ' R V) (const Unit x).hsum
          ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V)) :
      V⟦Γ'⟧)
    ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V)) :
      V⟦Γ'⟧)
⊢ (x • s).hsum =
    (Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V))
have rw₃ : Eq (α := V⟦Γ'⟧)
  ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (α := R⟦Γ⟧) (β := HahnModule Γ' R V) ((const Unit x : (a : PUnit.{1}) → R⟦Γ⟧) default : R⟦Γ⟧)
        ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V)) :
    V⟦Γ'⟧)
  ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V)) :
    V⟦Γ'⟧)
Tactic: rw [smul_eq, hsum_equiv, smul_hsum, hsum_unique, const_toFun]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
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
x : R⟦Γ⟧
s : SummableFamily Γ' V α
rw :
  (Equiv (Equiv.punitProd α) ((const Unit x).smul s)).hsum =
    (Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V))
rw₁ :
  ((const Unit x).smul s).hsum =
    (Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V))
rw₂ :
  Eq (α := V⟦Γ'⟧)
    ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (β := HahnModule Γ' R V) (const Unit x).hsum
          ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V)) :
      V⟦Γ'⟧)
    ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V)) :
      V⟦Γ'⟧)
rw₃ :
  Eq (α := V⟦Γ'⟧)
    ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (α := R⟦Γ⟧) (β := HahnModule Γ' R V) ((const Unit x : (a : PUnit.{1}) → R⟦Γ⟧) default : R⟦Γ⟧)
          ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V)) :
      V⟦Γ'⟧)
    ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V)) :
      V⟦Γ'⟧)
⊢ (x • s).hsum =
    (Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V))
have rw₄ : Eq (α := V⟦Γ'⟧)
  ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V)) :
    V⟦Γ'⟧)
  ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (β := HahnModule Γ' R V) x ((of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) s.hsum : HahnModule Γ' R V)) :
    V⟦Γ'⟧)
Tactic: rw [smul_eq, hsum_equiv, smul_hsum, hsum_unique, const_toFun]
-- 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 : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : Semiring R
inst_7 : AddCommMonoid V
inst_8 : Module R V
x : SummableFamily Γ' V α
x_1 : α
⊢ Eq (α := V⟦Γ'⟧) ((HSMul.hSMul (α := R⟦Γ⟧) 1 x : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧) ((x : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧)
have rw : Eq (α := V⟦Γ'⟧)
  ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (α := R⟦Γ⟧) (β := HahnModule Γ' R V) 1
        ((HahnModule.of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) ((x : (a : α) → V⟦Γ'⟧) x_1) : HahnModule Γ' R V)) :
    V⟦Γ'⟧)
  ((x : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧)
Tactic: rw [smul_apply, HahnModule.one_smul', Equiv.symm_apply_apply]