awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop
have pos : ∀ (hx : x = 0), (x * y).orderTop = x.orderTop + y.orderTop
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
pos : ∀ (hx : x = 0), (x * y).orderTop = x.orderTop + y.orderTop
⊢ (x * y).orderTop = x.orderTop + y.orderTop
have neg : ∀ (hx : ¬x = 0), (x * y).orderTop = x.orderTop + y.orderTop
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop
have pos : ∀ (hy : y = 0), (x * y).orderTop = x.orderTop + y.orderTop
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
pos : ∀ (hy : y = 0), (x * y).orderTop = x.orderTop + y.orderTop
⊢ (x * y).orderTop = x.orderTop + y.orderTop
have neg : ∀ (hy : ¬y = 0), (x * y).orderTop = x.orderTop + y.orderTop
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop
have this : (x * y).coeff (x.order + y.order) ≠ 0
Tactic: have : (x * y).coeff (x.order + y.order) ≠ 0 := by rwa [coeff_mul_order_add_order x y]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop
have hxy : x * y ≠ 0
Tactic: have hxy : x * y ≠ 0 := fun h ↦ (by simp [h] at this)
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
hxy : x * y ≠ 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop
have neg : (x * y).order = x.order + y.order
Tactic: rw [← order_eq_orderTop_of_ne_zero hx, ← order_eq_orderTop_of_ne_zero hy,
    ← order_eq_orderTop_of_ne_zero hxy, ← WithTop.coe_add, WithTop.coe_eq_coe]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
hxy : x * y ≠ 0
⊢ (x * y).order = x.order + y.order
have neg : x.order + y.order ≤ (x * y).order
Tactic: refine le_antisymm (order_le_of_coeff_ne_zero this) ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
hxy : x * y ≠ 0
⊢ x.order + y.order ≤ (x * y).order
have neg : Set.IsWF.min (s := x.support + y.support) sorry sorry ≤ sorry.min (s := (x * y).support) sorry
Tactic: rw [HahnSeries.order_of_ne hx, HahnSeries.order_of_ne hy, HahnSeries.order_of_ne hxy,
    ← Set.IsWF.min_add]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst_4 : NoZeroDivisors R
⊢ (x * y).orderTop = x.orderTop + y.orderTop
have pos : ∀ (hx : x = 0), (x * y).orderTop = x.orderTop + y.orderTop
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst_4 : NoZeroDivisors R
pos : ∀ (hx : x = 0), (x * y).orderTop = x.orderTop + y.orderTop
⊢ (x * y).orderTop = x.orderTop + y.orderTop
have neg : ∀ (hx : ¬x = 0), (x * y).orderTop = x.orderTop + y.orderTop
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst_4 : NoZeroDivisors R
hx : ¬x = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop
have pos : ∀ (hy : y = 0), (x * y).orderTop = x.orderTop + y.orderTop
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst_4 : NoZeroDivisors R
hx : ¬x = 0
pos : ∀ (hy : y = 0), (x * y).orderTop = x.orderTop + y.orderTop
⊢ (x * y).orderTop = x.orderTop + y.orderTop
have neg : ∀ (hy : ¬y = 0), (x * y).orderTop = x.orderTop + y.orderTop
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst_4 : NoZeroDivisors R
hx : ¬x = 0
hy : ¬y = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop
have neg : x.leadingCoeff * y.leadingCoeff ≠ 0
Tactic: apply orderTop_mul_of_ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
⊢ (x * y).order = x.order + y.order
have hx : x.leadingCoeff ≠ 0
Tactic: have hx : x.leadingCoeff ≠ 0 := by aesop
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : x.leadingCoeff ≠ 0
⊢ (x * y).order = x.order + y.order
have hy : y.leadingCoeff ≠ 0
Tactic: have hy : y.leadingCoeff ≠ 0 := by aesop
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : x.leadingCoeff ≠ 0
hy : y.leadingCoeff ≠ 0
⊢ (x * y).order = x.order + y.order
have hxy : (x * y).coeff (x.order + y.order) ≠ 0
Tactic: have hxy : (x * y).coeff (x.order + y.order) ≠ 0 :=
    ne_of_eq_of_ne (coeff_mul_order_add_order x y) h
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : x.leadingCoeff ≠ 0
hy : y.leadingCoeff ≠ 0
hxy : (x * y).coeff (x.order + y.order) ≠ 0
⊢ (x * y).order = x.order + y.order
have refine : x.order + y.order ≤ (x * y).order
Tactic: refine le_antisymm (order_le_of_coeff_ne_zero
    (Eq.mpr (congrArg (fun _a ↦ _a ≠ 0) (coeff_mul_order_add_order x y)) h)) ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : x.leadingCoeff ≠ 0
hy : y.leadingCoeff ≠ 0
hxy : (x * y).coeff (x.order + y.order) ≠ 0
⊢ x.order + y.order ≤ (x * y).order
have rw : Set.IsWF.min (s := x.support + y.support) sorry sorry ≤ sorry.min (s := (x * y).support) sorry
Tactic: rw [order_of_ne <| leadingCoeff_ne_zero.mp hx, order_of_ne <| leadingCoeff_ne_zero.mp hy,
    order_of_ne <| ne_zero_of_coeff_ne_zero hxy, ← Set.IsWF.min_add]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst_4 : NoZeroDivisors R
⊢ (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff
have pos : ∀ (hx : x = 0), (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst_4 : NoZeroDivisors R
pos : ∀ (hx : x = 0), (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff
⊢ (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff
have neg : ∀ (hx : ¬x = 0), (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst_4 : NoZeroDivisors R
hx : ¬x = 0
⊢ (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff
have pos : ∀ (hy : y = 0), (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst_4 : NoZeroDivisors R
hx : ¬x = 0
pos : ∀ (hy : y = 0), (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff
⊢ (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff
have neg : ∀ (hy : ¬y = 0), (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
inst_4 : NoZeroDivisors R
hx : ¬x = 0
hy : ¬y = 0
⊢ (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff
have neg : x.leadingCoeff * y.leadingCoeff ≠ 0
Tactic: apply leadingCoeff_mul_of_ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : R⟦Γ⟧
hx : x ≠ 0
⊢ (HMul.hMul (α := R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).order = g + x.order
have inl : Subsingleton R → (HMul.hMul (α := R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).order = g + x.order
Tactic: obtain _ | _ := subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : R⟦Γ⟧
hx : x ≠ 0
inl : Subsingleton R → (HMul.hMul (α := R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).order = g + x.order
⊢ (HMul.hMul (α := R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).order = g + x.order
have inr : Nontrivial R → (HMul.hMul (α := R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).order = g + x.order
Tactic: obtain _ | _ := subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : R⟦Γ⟧
hx : x ≠ 0
h : Nontrivial R
⊢ leadingCoeff.{u_1, u_3} (Γ := Γ) ((single g : (a : R) → R⟦Γ⟧) r) * x.leadingCoeff ≠ 0
have rwa : r * x.leadingCoeff ≠ 0
Tactic: rwa [leadingCoeff_of_single, ne_eq, hr.left.mul_left_eq_zero_iff, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : R⟦Γ⟧
hx : x ≠ 0
h : Nontrivial R
rwa : r * x.leadingCoeff ≠ 0
⊢ leadingCoeff.{u_1, u_3} (Γ := Γ) ((single g : (a : R) → R⟦Γ⟧) r) * x.leadingCoeff ≠ 0
have rwa₁ : ¬r * x.leadingCoeff = 0
Tactic: rwa [leadingCoeff_of_single, ne_eq, hr.left.mul_left_eq_zero_iff, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : R⟦Γ⟧
hx : x ≠ 0
h : Nontrivial R
rwa : r * x.leadingCoeff ≠ 0
rwa₁ : ¬r * x.leadingCoeff = 0
⊢ leadingCoeff.{u_1, u_3} (Γ := Γ) ((single g : (a : R) → R⟦Γ⟧) r) * x.leadingCoeff ≠ 0
have rwa₂ : ¬x.leadingCoeff = 0
Tactic: rwa [leadingCoeff_of_single, ne_eq, hr.left.mul_left_eq_zero_iff, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : R⟦Γ⟧
hx : x ≠ 0
h : Nontrivial R
rwa : r * x.leadingCoeff ≠ 0
rwa₁ : ¬r * x.leadingCoeff = 0
rwa₂ : ¬x.leadingCoeff = 0
⊢ leadingCoeff.{u_1, u_3} (Γ := Γ) ((single g : (a : R) → R⟦Γ⟧) r) * x.leadingCoeff ≠ 0
have rwa₃ : ¬x = 0
Tactic: rwa [leadingCoeff_of_single, ne_eq, hr.left.mul_left_eq_zero_iff, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : R⟦Γ⟧
hx : x ≠ 0
h : Nontrivial R
⊢ (HMul.hMul (α := R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).order = g + x.order
have hrx : leadingCoeff.{u_1, u_3} (Γ := Γ) ((single g : (a : R) → R⟦Γ⟧) r) * x.leadingCoeff ≠ 0
Tactic: have hrx : ((single g) r).leadingCoeff * x.leadingCoeff ≠ 0 := by
    rwa [leadingCoeff_of_single, ne_eq, hr.left.mul_left_eq_zero_iff, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : R⟦Γ⟧
hx : x ≠ 0
h : Nontrivial R
hrx : leadingCoeff.{u_1, u_3} (Γ := Γ) ((single g : (a : R) → R⟦Γ⟧) r) * x.leadingCoeff ≠ 0
⊢ (HMul.hMul (α := R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).order = g + x.order
have inr : order.{u_1, u_3} (R := R) ((single g : (a : R) → R⟦Γ⟧) r) + x.order = g + x.order
Tactic: rw [order_mul_of_ne_zero hrx, order_single <| IsRegular.ne_zero hr]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : R⟦Γ⟧
hx : x ≠ 0
h : Nontrivial R
hrx : leadingCoeff.{u_1, u_3} (Γ := Γ) ((single g : (a : R) → R⟦Γ⟧) r) * x.leadingCoeff ≠ 0
inr : order.{u_1, u_3} (R := R) ((single g : (a : R) → R⟦Γ⟧) r) + x.order = g + x.order
⊢ (HMul.hMul (α := R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).order = g + x.order
have inr₁ : g + x.order = g + x.order
Tactic: rw [order_mul_of_ne_zero hrx, order_single <| IsRegular.ne_zero hr]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalSemiring R
x y z : R⟦Γ⟧
⊢ x * y * z = x * (y * z)
have coeff : ∀ (b : Γ), (x * y * z).coeff b = (x * (y * z)).coeff b
Tactic: ext b
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ (x * y * z).coeff b = (x * (y * z)).coeff b
have coeff : Eq.{u_3 + 1} (α := R)
  (∑ ij ∈ addAntidiagonal (s := x.support + y.support) (t := z.support) sorry sorry b, (x * y).coeff ij.1 * z.coeff ij.2)
  (∑ ij ∈ addAntidiagonal (s := x.support) (t := y.support + z.support) sorry sorry b, x.coeff ij.1 * (y * z).coeff ij.2)
Tactic: rw [coeff_mul_left' (x.isPWO_support.add y.isPWO_support) support_mul_subset,
    coeff_mul_right' (y.isPWO_support.add z.isPWO_support) support_mul_subset]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ Eq.{u_3 + 1} (α := R)
    (∑ ij ∈ addAntidiagonal (s := x.support + y.support) (t := z.support) ⋯ ⋯ b, (x * y).coeff ij.1 * z.coeff ij.2)
    (∑ ij ∈ addAntidiagonal (s := x.support) (t := y.support + z.support) ⋯ ⋯ b, x.coeff ij.1 * (y * z).coeff ij.2)
have coeff : Eq.{u_3 + 1} (α := R)
  (∑
    x_1 ∈
      (addAntidiagonal (s := x.support + y.support) (t := z.support) sorry sorry b).sigma (α := fun (a : Γ × Γ) ↦ Γ × Γ)
        fun (a : Γ × Γ) ↦ addAntidiagonal (s := x.support) (t := y.support) sorry sorry a.1,
    x.coeff x_1.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ).1 * y.coeff x_1.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ).2 *
      z.coeff x_1.fst (β := fun (i : Γ × Γ) ↦ Γ × Γ).2)
  (∑
    x_1 ∈
      (addAntidiagonal (s := x.support) (t := y.support + z.support) sorry sorry b).sigma (α := fun (a : Γ × Γ) ↦ Γ × Γ)
        fun (a : Γ × Γ) ↦ addAntidiagonal (s := y.support) (t := z.support) sorry sorry a.2,
    x.coeff x_1.fst (β := fun (i : Γ × Γ) ↦ Γ × Γ).1 *
      (y.coeff x_1.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ).1 * z.coeff x_1.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ).2))
Tactic: simp only [coeff_mul, sum_mul, mul_sum, sum_sigma']
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ Eq.{u_3 + 1} (α := R)
    (∑
      x_1 ∈
        (addAntidiagonal (s := x.support + y.support) (t := z.support) ⋯ ⋯ b).sigma (α := fun (a : Γ × Γ) ↦ Γ × Γ)
          fun (a : Γ × Γ) ↦ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ a.1,
      x.coeff x_1.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ).1 * y.coeff x_1.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ).2 *
        z.coeff x_1.fst (β := fun (i : Γ × Γ) ↦ Γ × Γ).2)
    (∑
      x_1 ∈
        (addAntidiagonal (s := x.support) (t := y.support + z.support) ⋯ ⋯ b).sigma (α := fun (a : Γ × Γ) ↦ Γ × Γ)
          fun (a : Γ × Γ) ↦ addAntidiagonal (s := y.support) (t := z.support) ⋯ ⋯ a.2,
      x.coeff x_1.fst (β := fun (i : Γ × Γ) ↦ Γ × Γ).1 *
        (y.coeff x_1.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ).1 * z.coeff x_1.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ).2))
have coeff : ∀ (a : (_ : Γ × Γ) × Γ × Γ),
  Membership.mem (γ := Finset ((_ : Γ × Γ) × Γ × Γ))
      ((addAntidiagonal (s := x.support + y.support) (t := z.support) sorry sorry b).sigma (α := fun (a : Γ × Γ) ↦ Γ × Γ)
        fun (a : Γ × Γ) ↦ addAntidiagonal (s := x.support) (t := y.support) sorry sorry a.1)
      a →
    Membership.mem (α := (_ : Γ × Γ) × Γ × Γ) (γ := Finset ((_ : Γ × Γ) × Γ × Γ))
      ((addAntidiagonal (s := x.support) (t := y.support + z.support) sorry sorry b).sigma (α := fun (a : Γ × Γ) ↦ Γ × Γ)
        fun (a : Γ × Γ) ↦ addAntidiagonal (s := y.support) (t := z.support) sorry sorry a.2)
      (match (motive := (_ : Γ × Γ) × Γ × Γ → (_ : Γ × Γ) × Γ × Γ) a with
        | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ) ↦ Γ × Γ) (k, l + j) (l, j) :
        (_ : Γ × Γ) × Γ × Γ)
Tactic: apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l + j), (l, j)⟩)
    (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i + k, l), (i, k)⟩)
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
coeff :
  ∀ (a : (_ : Γ × Γ) × Γ × Γ),
    Membership.mem (γ := Finset ((_ : Γ × Γ) × Γ × Γ))
        ((addAntidiagonal (s := x.support + y.support) (t := z.support) ⋯ ⋯ b).sigma (α := fun (a : Γ × Γ) ↦ Γ × Γ)
          fun (a : Γ × Γ) ↦ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ a.1)
        a →
      Membership.mem (α := (_ : Γ × Γ) × Γ × Γ) (γ := Finset ((_ : Γ × Γ) × Γ × Γ))
        ((addAntidiagonal (s := x.support) (t := y.support + z.support) ⋯ ⋯ b).sigma (α := fun (a : Γ × Γ) ↦ Γ × Γ)
          fun (a : Γ × Γ) ↦ addAntidiagonal (s := y.support) (t := z.support) ⋯ ⋯ a.2)
        (match (motive := (_ : Γ × Γ) × Γ × Γ → (_ : Γ × Γ) × Γ × Γ) a with
          | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ) ↦ Γ × Γ) (k, l + j) (l, j) :
          (_ : Γ × Γ) × Γ × Γ)
⊢ Eq.{u_3 + 1} (α := R)
    (∑
      x_1 ∈
        (addAntidiagonal (s := x.support + y.support) (t := z.support) ⋯ ⋯ b).sigma (α := fun (a : Γ × Γ) ↦ Γ × Γ)
          fun (a : Γ × Γ) ↦ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ a.1,
      x.coeff x_1.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ).1 * y.coeff x_1.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ).2 *
        z.coeff x_1.fst (β := fun (i : Γ × Γ) ↦ Γ × Γ).2)
    (∑
      x_1 ∈
        (addAntidiagonal (s := x.support) (t := y.support + z.support) ⋯ ⋯ b).sigma (α := fun (a : Γ × Γ) ↦ Γ × Γ)
          fun (a : Γ × Γ) ↦ addAntidiagonal (s := y.support) (t := z.support) ⋯ ⋯ a.2,
      x.coeff x_1.fst (β := fun (i : Γ × Γ) ↦ Γ × Γ).1 *
        (y.coeff x_1.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ).1 * z.coeff x_1.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ).2))
have coeff₁ : ∀ (a : (_ : Γ × Γ) × Γ × Γ),
  Membership.mem (γ := Finset ((_ : Γ × Γ) × Γ × Γ))
      ((addAntidiagonal (s := x.support) (t := y.support + z.support) sorry sorry b).sigma (α := fun (a : Γ × Γ) ↦ Γ × Γ)
        fun (a : Γ × Γ) ↦ addAntidiagonal (s := y.support) (t := z.support) sorry sorry a.2)
      a →
    Membership.mem (α := (_ : Γ × Γ) × Γ × Γ) (γ := Finset ((_ : Γ × Γ) × Γ × Γ))
      ((addAntidiagonal (s := x.support + y.support) (t := z.support) sorry sorry b).sigma (α := fun (a : Γ × Γ) ↦ Γ × Γ)
        fun (a : Γ × Γ) ↦ addAntidiagonal (s := x.support) (t := y.support) sorry sorry a.1)
      (match (motive := (_ : Γ × Γ) × Γ × Γ → (_ : Γ × Γ) × Γ × Γ) a with
        | ⟨(i, _j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ) ↦ Γ × Γ) (i + k, l) (i, k) :
        (_ : Γ × Γ) × Γ × Γ)
Tactic: apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l + j), (l, j)⟩)
    (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i + k, l), (i, k)⟩)