awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
pos :
  ∀ (hr : r = 0),
    coeff
        ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
          (HSMul.hSMul (α := R⟦Γ⟧) ((single b : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x))
        (b +ᵥ a) =
      HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)
⊢ coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (α := R⟦Γ⟧) ((single b : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x))
      (b +ᵥ a) =
    HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)
have neg : ∀ (hr : ¬r = 0),
  coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (α := R⟦Γ⟧) ((single b : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x))
      (b +ᵥ a) =
    HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
⊢ coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (α := R⟦Γ⟧) ((single b : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x))
      (b +ᵥ a) =
    HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)
have neg : ∑
    x_1 ∈
      VAddAntidiagonal (s := {b}) (t :=
        HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) sorry,
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.1)
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) x_1.2) =
  HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)
Tactic: simp only [hr, coeff_smul, coeff_smul, HahnSeries.support_single_of_ne, ne_eq, not_false_iff]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
⊢ ∑
      x_1 ∈
        VAddAntidiagonal (s := {b}) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) ⋯,
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) x_1.2) =
    HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)
have pos : ∀ (hx : Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0),
  ∑
      x_1 ∈
        VAddAntidiagonal (s := {b}) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) sorry,
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) x_1.2) =
    HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)
Tactic: by_cases hx : ((of R).symm x).coeff a = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
pos :
  ∀ (hx : Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0),
    ∑
        x_1 ∈
          VAddAntidiagonal (s := {b}) (t :=
            HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a)
            ⋯,
        HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.1)
          (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) x_1.2) =
      HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)
⊢ ∑
      x_1 ∈
        VAddAntidiagonal (s := {b}) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) ⋯,
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) x_1.2) =
    HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)
have neg : ∀ (hx : ¬Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0),
  ∑
      x_1 ∈
        VAddAntidiagonal (s := {b}) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) sorry,
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) x_1.2) =
    HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)
Tactic: by_cases hx : ((of R).symm x).coeff a = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0
⊢ ∑
      x_1 ∈
        VAddAntidiagonal (s := {b}) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) ⋯,
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) x_1.2) =
    HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)
have pos : Eq.{u_5 + 1} (α := V)
  (∑
    x_1 ∈
      VAddAntidiagonal (s := {b}) (t :=
        HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) sorry,
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.1)
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) x_1.2))
  0
Tactic: simp only [hx, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0
⊢ Eq.{u_5 + 1} (α := V)
    (∑
      x_1 ∈
        VAddAntidiagonal (s := {b}) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) ⋯,
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) x_1.2))
    0
have rw : Eq (α := Finset (Γ × Γ'))
  (VAddAntidiagonal (s := {b}) (t :=
    HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) sorry)
  ∅
Tactic: rw [sum_congr _ fun _ _ => rfl, sum_empty]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0
⊢ Eq (α := Finset (Γ × Γ'))
    (VAddAntidiagonal (s := {b}) (t :=
      HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) ⋯)
    ∅
have h : ∀ (a1 : Γ) (a2 : Γ'),
  Membership.mem (γ := Finset (Γ × Γ'))
      (VAddAntidiagonal (s := {b}) (t :=
        HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) sorry)
      (a1, a2) ↔
    Membership.mem (γ := Finset (Γ × Γ')) ∅ (a1, a2)
Tactic: ext ⟨a1, a2⟩
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0
a1 : Γ
a2 : Γ'
⊢ Membership.mem (γ := Finset (Γ × Γ'))
      (VAddAntidiagonal (s := {b}) (t :=
        HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) ⋯)
      (a1, a2) ↔
    Membership.mem (γ := Finset (Γ × Γ')) ∅ (a1, a2)
have h : a1 = b →
  Membership.mem (γ := Set Γ')
      (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) a2 →
    ¬a1 +ᵥ a2 = b +ᵥ a
Tactic: simp only [notMem_empty, not_and, Set.mem_singleton_iff,
      mem_vaddAntidiagonal, iff_false]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (hypothesis)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
hr : ¬r = 0
hx : Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0
a1 : Γ
a2 : Γ'
h2 :
  Membership.mem (γ := Set Γ')
    (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) a2
h1 : a1 +ᵥ a2 = a1 +ᵥ a
⊢ False
have h2₁ : Membership.mem (γ := Set Γ')
  (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) a
Tactic: rw [IsCancelVAdd.left_cancel a1 a2 a h1] at h2
Cleared hypotheses: h2, h1
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ¬Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0
⊢ ∑
      x_1 ∈
        VAddAntidiagonal (s := {b}) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) ⋯,
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) x_1.2) =
    HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)
have trans : Eq.{u_5 + 1} (α := V)
  (∑
    x_1 ∈
      VAddAntidiagonal (s := {b}) (t :=
        HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) sorry,
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.1)
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) x_1.2))
  (∑ ij ∈ {(b, a)},
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) ij.1)
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) ij.2))
Tactic: trans ∑ ij ∈ {(b, a)},
    (HahnSeries.single b r).coeff ij.fst • ((of R).symm x).coeff ij.snd
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ¬Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0
trans :
  Eq.{u_5 + 1} (α := V)
    (∑
      x_1 ∈
        VAddAntidiagonal (s := {b}) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) ⋯,
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) x_1.2))
    (∑ ij ∈ {(b, a)},
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) ij.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) ij.2))
⊢ ∑
      x_1 ∈
        VAddAntidiagonal (s := {b}) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) ⋯,
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) x_1.2) =
    HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)
have trans₁ : ∑ ij ∈ {(b, a)},
    HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) ij.1)
      (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) ij.2) =
  HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)
Tactic: trans ∑ ij ∈ {(b, a)},
    (HahnSeries.single b r).coeff ij.fst • ((of R).symm x).coeff ij.snd
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ¬Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0
⊢ Eq.{u_5 + 1} (α := V)
    (∑
      x_1 ∈
        VAddAntidiagonal (s := {b}) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) ⋯,
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) x_1.2))
    (∑ ij ∈ {(b, a)},
      HSMul.hSMul.{u_3, u_5, u_5} (α := R) (β := V) (coeff ((single b : (a : R) → R⟦Γ⟧) r) ij.1)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) ij.2))
have apply : Eq (α := Finset (Γ × Γ'))
  (VAddAntidiagonal (s := {b}) (t :=
    HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) sorry)
  {(b, a)}
Tactic: apply sum_congr _ fun _ _ => rfl
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ¬Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0
⊢ Eq (α := Finset (Γ × Γ'))
    (VAddAntidiagonal (s := {b}) (t :=
      HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) ⋯)
    {(b, a)}
have h : ∀ (a1 : Γ) (a2 : Γ'),
  Membership.mem (γ := Finset (Γ × Γ'))
      (VAddAntidiagonal (s := {b}) (t :=
        HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) sorry)
      (a1, a2) ↔
    Membership.mem (γ := Finset (Γ × Γ')) {(b, a)} (a1, a2)
Tactic: ext ⟨a1, a2⟩
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ¬Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0
a1 : Γ
a2 : Γ'
⊢ Membership.mem (γ := Finset (Γ × Γ'))
      (VAddAntidiagonal (s := {b}) (t :=
        HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) (b +ᵥ a) ⋯)
      (a1, a2) ↔
    Membership.mem (γ := Finset (Γ × Γ')) {(b, a)} (a1, a2)
have h : a1 = b ∧
    Membership.mem (γ := Set Γ')
        (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) a2 ∧
      a1 +ᵥ a2 = b +ᵥ a ↔
  a1 = b ∧ a2 = a
Tactic: simp only [Set.mem_singleton_iff, Prod.mk_inj, mem_vaddAntidiagonal, mem_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ¬Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0
a1 : Γ
a2 : Γ'
⊢ a1 = b ∧
      Membership.mem (γ := Set Γ')
          (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) a2 ∧
        a1 +ᵥ a2 = b +ᵥ a ↔
    a1 = b ∧ a2 = a
have h : a1 = b ∧
    Membership.mem (γ := Set Γ')
        (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) a2 ∧
      a1 +ᵥ a2 = b +ᵥ a →
  a1 = b ∧ a2 = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ¬Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a) 0
a1 : Γ
a2 : Γ'
h :
  a1 = b ∧
      Membership.mem (γ := Set Γ')
          (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) a2 ∧
        a1 +ᵥ a2 = b +ᵥ a →
    a1 = b ∧ a2 = a
⊢ a1 = b ∧
      Membership.mem (γ := Set Γ')
          (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) a2 ∧
        a1 +ᵥ a2 = b +ᵥ a ↔
    a1 = b ∧ a2 = a
have h₁ : a1 = b ∧ a2 = a →
  a1 = b ∧
    Membership.mem (γ := Set Γ')
        (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x)) a2 ∧
      a1 +ᵥ a2 = b +ᵥ a
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ'
inst_1 : AddCommMonoid V
Γ : Type u_6
inst_2 : AddCommMonoid Γ
inst_3 : PartialOrder Γ
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : MulZeroClass R
inst_7 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
⊢ coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x))
      a =
    HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)
have nth_rw : coeff
    ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      (HSMul.hSMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x))
    (HVAdd.hVAdd.{u_6, u_2, u_2} (α := Γ) 0 a) =
  HSMul.hSMul (β := V) r (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) a)
Tactic: nth_rw 1 [← zero_vadd Γ a]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ'
inst_1 : AddCommMonoid V
Γ : Type u_6
inst_2 : AddCommMonoid Γ
inst_3 : PartialOrder Γ
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : MulZeroClass R
inst_7 : SMulWithZero R V
r : R
x : HahnModule Γ' R V
⊢ HSMul.hSMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x = r • x
have h : ∀ (x_1 : Γ'),
  Eq.{u_5 + 1} (α := V)
    (coeff
      ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x))
      x_1)
    (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (r • x)) x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : Zero R
inst_6 : SMulWithZero R V
x : HahnModule Γ' R V
⊢ HSMul.hSMul (α := R⟦Γ⟧) 0 x = 0
have h : ∀ (x_1 : Γ'),
  Eq.{u_5 + 1} (α := V)
    (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (HSMul.hSMul (α := R⟦Γ⟧) 0 x)) x_1)
    (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) 0) x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ'
inst_1 : AddCommMonoid V
Γ : Type u_6
inst_2 : AddCommMonoid Γ
inst_3 : PartialOrder Γ
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : MonoidWithZero R
inst_7 : MulActionWithZero R V
x : HahnModule Γ' R V
⊢ HSMul.hSMul (α := R⟦Γ⟧) 1 x = x
have h : ∀ (g : Γ'),
  Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (HSMul.hSMul (α := R⟦Γ⟧) 1 x)) g)
    (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) x) g)
Tactic: ext g
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : MulZeroClass R
inst_6 : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
⊢ HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y)) ⊆
    HVAdd.hVAdd (β := Set Γ') x.support
      (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y))
have refine : ∀ (x_1 : Γ')
  (hx :
    Membership.mem (γ := Set Γ')
      (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y))) x_1),
  Membership.mem (γ := Set Γ')
    {a : Γ' |
      (VAddAntidiagonal (s := x.support) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) a
          sorry).Nonempty}
    x_1
Tactic: refine Set.Subset.trans (fun x hx => ?_) (support_vaddAntidiagonal_subset_vadd
    fun a ↦ Set.VAddAntidiagonal.finite_of_isPWO x.isPWO_support ((of R).symm y).isPWO_support a)