awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
neg : ∀ (hy : ¬y = 0), (x * y).orderTop = x.orderTop + y.orderTop
⊢ (x * y).orderTop = x.orderTop + y.orderTop

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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

Tactic:
simp [hy]
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
neg : x.leadingCoeff * y.leadingCoeff ≠ 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop

Tactic:
apply orderTop_mul_of_ne_zero

Premises used: HahnSeries.orderTop_mul_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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.leadingCoeff * y.leadingCoeff ≠ 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
⊢ x.orderTop + y.orderTop ≤ (x • y).orderTop

Tactic:
HahnModule.orderTop_vAdd_le_orderTop_smul fun i j ↦ rfl

Premises used: HahnModule.orderTop_vAdd_le_orderTop_smul, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
⊢ x.orderTop + y.orderTop ≤ (x • y).orderTop

Tactic:
exact HahnModule.orderTop_vAdd_le_orderTop_smul fun i j ↦ rfl

Premises used: HahnModule.orderTop_vAdd_le_orderTop_smul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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.leadingCoeff ≠ 0

Tactic:
aesop
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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.leadingCoeff ≠ 0

Tactic:
have hx : x.leadingCoeff ≠ 0 := by aesop
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
⊢ y.leadingCoeff ≠ 0

Tactic:
aesop
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
⊢ y.leadingCoeff ≠ 0

Tactic:
have hy : y.leadingCoeff ≠ 0 := by aesop
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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).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
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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

Tactic:
le_antisymm (order_le_of_coeff_ne_zero
    (Eq.mpr (congrArg (fun _a ↦ _a ≠ 0) (coeff_mul_order_add_order x y)) h)) ?_

Premises used: Eq.mpr, congrArg, Ne, HahnSeries.order_le_of_coeff_ne_zero, HahnSeries.coeff_mul_order_add_order, le_antisymm, OfNat.ofNat
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
refine : x.order + y.order ≤ (x * y).order
⊢ (x * y).order = x.order + 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)) ?_

Premises used: Eq.mpr, congrArg, Ne, HahnSeries.order_le_of_coeff_ne_zero, HahnSeries.coeff_mul_order_add_order, le_antisymm, OfNat.ofNat
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
rw : Set.IsWF.min (s := x.support + y.support) ⋯ ⋯ ≤ ⋯.min (s := (x * y).support) ⋯
⊢ x.order + y.order ≤ (x * y).order

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]

Premises used: HahnSeries.leadingCoeff_ne_zero, HahnSeries.ne_zero_of_coeff_ne_zero, HahnSeries.order_of_ne, Set.IsWF.min_add, Iff.mp
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
⊢ Set.IsWF.min (s := x.support + y.support) ⋯ ⋯ ≤ ⋯.min (s := (x * y).support) ⋯

Tactic:
Set.IsWF.min_le_min_of_subset support_mul_subset

Premises used: Set.IsWF.min_le_min_of_subset, HahnSeries.support_mul_subset
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
⊢ Set.IsWF.min (s := x.support + y.support) ⋯ ⋯ ≤ ⋯.min (s := (x * y).support) ⋯

Tactic:
exact Set.IsWF.min_le_min_of_subset support_mul_subset

Premises used: Set.IsWF.min_le_min_of_subset, HahnSeries.support_mul_subset
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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).leadingCoeff = x.leadingCoeff * y.leadingCoeff

Tactic:
simp only [leadingCoeff_eq, order_mul_of_ne_zero h, coeff_mul_order_add_order]

Premises used: HahnSeries.coeff_mul_order_add_order, HahnSeries.leadingCoeff_eq, HahnSeries.order_mul_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
neg : ∀ (hx : ¬x = 0), (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff
⊢ (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
neg : ∀ (hy : ¬y = 0), (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff
⊢ (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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

Tactic:
simp [hy]
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
neg : x.leadingCoeff * y.leadingCoeff ≠ 0
⊢ (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff

Tactic:
apply leadingCoeff_mul_of_ne_zero

Premises used: HahnSeries.leadingCoeff_mul_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
inr : Nontrivial 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

Tactic:
obtain _ | _ := subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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 : Subsingleton R
⊢ (HMul.hMul (α := R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).order = g + x.order

Tactic:
(hx <| Subsingleton.eq_zero x).elim

Premises used: False.elim, Subsingleton.eq_zero
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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 : Subsingleton R
⊢ (HMul.hMul (α := R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).order = g + x.order

Tactic:
exact (hx <| Subsingleton.eq_zero x).elim

Premises used: False.elim, Subsingleton.eq_zero
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
rwa₃ rwa₄ rwa₅ rwa₆ : ¬x = 0
⊢ leadingCoeff.{u_1, u_3} (Γ := Γ) ((single g : (a : R) → R⟦Γ⟧) r) * x.leadingCoeff ≠ 0

Tactic:
rwa [leadingCoeff_of_single, ne_eq, hr.left.mul_left_eq_zero_iff, leadingCoeff_eq_zero]

Premises used: IsLeftRegular.mul_left_eq_zero_iff, ne_eq, HahnSeries.leadingCoeff_eq_zero, IsRegular.left, HahnSeries.leadingCoeff_of_single
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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

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]
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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
inr₁ inr₂ : g + x.order = g + x.order
⊢ (HMul.hMul (α := R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).order = g + x.order

Tactic:
rw [order_mul_of_ne_zero hrx, order_single <| IsRegular.ne_zero hr]

Premises used: IsRegular.ne_zero, HahnSeries.order_mul_of_ne_zero, HahnSeries.order_single
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalSemiring R
x y z : R⟦Γ⟧
coeff : ∀ (b : Γ), (x * y * z).coeff b = (x * (y * z)).coeff b
⊢ x * y * z = x * (y * z)

Tactic:
ext b
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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 :
  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)
⊢ (x * y * z).coeff b = (x * (y * z)).coeff b

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]

Premises used: HahnSeries.isPWO_support, HahnSeries.coeff_mul_left', HahnSeries.coeff_mul_right', Set.IsPWO.add, HahnSeries.support_mul_subset
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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 :
  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))
⊢ 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)

Tactic:
simp only [coeff_mul, sum_mul, mul_sum, sum_sigma']

Premises used: Finset.mul_sum, HahnSeries.coeff_mul, Finset.sum_sigma', Finset.sum_mul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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 : Γ
⊢ ∀ (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) :
          (_ : Γ × Γ) × Γ × Γ)

Tactic:
aesop (add safe Set.add_mem_add) (add simp [add_assoc, mul_assoc])

Premises used: add_assoc, mul_assoc, Set.add_mem_add
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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 : Γ
⊢ ∀ (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)
        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)
        (match (motive := (_ : Γ × Γ) × Γ × Γ → (_ : Γ × Γ) × Γ × Γ) a with
          | ⟨(i, _j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ) ↦ Γ × Γ) (i + k, l) (i, k) :
          (_ : Γ × Γ) × Γ × Γ)

Tactic:
aesop (add safe Set.add_mem_add) (add simp [add_assoc, mul_assoc])

Premises used: add_assoc, mul_assoc, Set.add_mem_add
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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 : Γ
⊢ ∀ (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 →
      (match (motive := (_ : Γ × Γ) × Γ × Γ → (_ : Γ × Γ) × Γ × Γ)
          match (motive := (_ : Γ × Γ) × Γ × Γ → (_ : Γ × Γ) × Γ × Γ) a with
          | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ) ↦ Γ × Γ) (k, l + j) (l, j) with
        | ⟨(i, _j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ) ↦ Γ × Γ) (i + k, l) (i, k)) =
        a

Tactic:
aesop (add safe Set.add_mem_add) (add simp [add_assoc, mul_assoc])

Premises used: add_assoc, mul_assoc, Set.add_mem_add
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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 : Γ
⊢ ∀ (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)
        a →
      (match (motive := (_ : Γ × Γ) × Γ × Γ → (_ : Γ × Γ) × Γ × Γ)
          match (motive := (_ : Γ × Γ) × Γ × Γ → (_ : Γ × Γ) × Γ × Γ) a with
          | ⟨(i, _j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ) ↦ Γ × Γ) (i + k, l) (i, k) with
        | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ) ↦ Γ × Γ) (k, l + j) (l, j)) =
        a

Tactic:
aesop (add safe Set.add_mem_add) (add simp [add_assoc, mul_assoc])

Premises used: add_assoc, mul_assoc, Set.add_mem_add
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
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 : Γ
⊢ ∀ (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 →
      x.coeff a.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ).1 * y.coeff a.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ).2 *
          z.coeff a.fst (β := fun (i : Γ × Γ) ↦ Γ × Γ).2 =
        x.coeff
            (Sigma.fst (β := fun (i : Γ × Γ) ↦ Γ × Γ)
                (match (motive := (_ : Γ × Γ) × Γ × Γ → (_ : Γ × Γ) × Γ × Γ) a with
                | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ) ↦ Γ × Γ) (k, l + j) (l, j))).1 *
          (y.coeff
              (Sigma.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ)
                  (match (motive := (_ : Γ × Γ) × Γ × Γ → (_ : Γ × Γ) × Γ × Γ) a with
                  | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ) ↦ Γ × Γ) (k, l + j) (l, j))).1 *
            z.coeff
              (Sigma.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ)
                  (match (motive := (_ : Γ × Γ) × Γ × Γ → (_ : Γ × Γ) × Γ × Γ) a with
                  | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ) ↦ Γ × Γ) (k, l + j) (l, j))).2)

Tactic:
aesop (add safe Set.add_mem_add) (add simp [add_assoc, mul_assoc])

Premises used: add_assoc, mul_assoc, Set.add_mem_add
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
x : R⟦Γ⟧
coeff : ∀ (x_1 : Γ), (1 * x).coeff x_1 = x.coeff x_1
⊢ 1 * x = x

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
x : R⟦Γ⟧
x_1 : Γ
⊢ (1 * x).coeff x_1 = x.coeff x_1

Tactic:
coeff_single_zero_mul.trans (one_mul _)

Premises used: HahnSeries.coeff_single_zero_mul, one_mul, Eq.trans
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
x : R⟦Γ⟧
x_1 : Γ
⊢ (1 * x).coeff x_1 = x.coeff x_1

Tactic:
exact coeff_single_zero_mul.trans (one_mul _)

Premises used: HahnSeries.coeff_single_zero_mul, Eq.trans
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
x : R⟦Γ⟧
coeff : ∀ (x_1 : Γ), (x * 1).coeff x_1 = x.coeff x_1
⊢ x * 1 = x

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
x : R⟦Γ⟧
x_1 : Γ
⊢ (x * 1).coeff x_1 = x.coeff x_1

Tactic:
coeff_mul_single_zero.trans (mul_one _)

Premises used: mul_one, HahnSeries.coeff_mul_single_zero, Eq.trans
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonAssocSemiring R
x : R⟦Γ⟧
x_1 : Γ
⊢ (x * 1).coeff x_1 = x.coeff x_1

Tactic:
exact coeff_mul_single_zero.trans (mul_one _)

Premises used: HahnSeries.coeff_mul_single_zero, Eq.trans