awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
pos :
  ∀ (hx : x.coeff a = 0),
    ∑ x_1 ∈ addAntidiagonal (s := x.support) (t := {b}) ⋯ ⋯ (a + b),
        x.coeff x_1.1 * coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.2 =
      x.coeff a * r
neg :
  ∀ (hx : ¬x.coeff a = 0),
    ∑ x_1 ∈ addAntidiagonal (s := x.support) (t := {b}) ⋯ ⋯ (a + b),
        x.coeff x_1.1 * coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.2 =
      x.coeff a * r
⊢ ∑ x_1 ∈ addAntidiagonal (s := x.support) (t := {b}) ⋯ ⋯ (a + b),
      x.coeff x_1.1 * coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.2 =
    x.coeff a * r

Tactic:
by_cases hx : x.coeff a = 0

Premises used: HahnSeries.coeff
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
hx : x.coeff a = 0
pos :
  Eq.{u_3 + 1} (α := R)
    (∑ x_1 ∈ addAntidiagonal (s := x.support) (t := {b}) ⋯ ⋯ (a + b),
      x.coeff x_1.1 * coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.2)
    0
⊢ ∑ x_1 ∈ addAntidiagonal (s := x.support) (t := {b}) ⋯ ⋯ (a + b),
      x.coeff x_1.1 * coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.2 =
    x.coeff a * r

Tactic:
simp only [hx, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
hx : x.coeff a = 0
rw : addAntidiagonal (s := x.support) (t := {b}) ⋯ ⋯ (a + b) = ∅
⊢ Eq.{u_3 + 1} (α := R)
    (∑ x_1 ∈ addAntidiagonal (s := x.support) (t := {b}) ⋯ ⋯ (a + b),
      x.coeff x_1.1 * coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.2)
    0

Tactic:
rw [sum_congr _ fun _ _ => rfl, sum_empty]

Premises used: Finset.sum_empty, Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
hx : x.coeff a = 0
h :
  ∀ (a1 a2 : Γ),
    (a1, a2) ∈ addAntidiagonal (s := x.support) (t := {b}) ⋯ ⋯ (a + b) ↔ Membership.mem (γ := Finset (Γ × Γ)) ∅ (a1, a2)
⊢ addAntidiagonal (s := x.support) (t := {b}) ⋯ ⋯ (a + b) = ∅

Tactic:
ext ⟨a1, a2⟩
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
hx : x.coeff a = 0
a1 a2 : Γ
h : a1 ∈ x.support → a2 = b → ¬a1 + a2 = a + b
⊢ (a1, a2) ∈ addAntidiagonal (s := x.support) (t := {b}) ⋯ ⋯ (a + b) ↔ Membership.mem (γ := Finset (Γ × Γ)) ∅ (a1, a2)

Tactic:
simp only [notMem_empty, not_and, Set.mem_singleton_iff,
      mem_addAntidiagonal, iff_false]

Premises used: iff_false, Finset.notMem_empty, Set.mem_singleton_iff, not_and, Finset.mem_addAntidiagonal
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a : Γ
hr : ¬r = 0
hx : x.coeff a = 0
a1 a2 : Γ
h2 : a1 ∈ x.support
h1 : a1 + a2 = a + a2
h : ∀ (hx : x.coeff a1 = 0) (a2 : Γ) (h2 : a1 ∈ x.support) (h1 : a1 + a2 = a + a2), False
⊢ False

Tactic:
rw [← add_right_cancel h1] at hx

Premises used: add_right_cancel
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a : Γ
hr : ¬r = 0
a1 : Γ
hx : x.coeff a1 = 0
a2 : Γ
h2 : a1 ∈ x.support
h1 : a1 + a2 = a + a2
⊢ False

Tactic:
h2 hx
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a : Γ
hr : ¬r = 0
a1 : Γ
hx : x.coeff a1 = 0
a2 : Γ
h2 : a1 ∈ x.support
h1 : a1 + a2 = a + a2
⊢ False

Tactic:
exact h2 hx
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
trans :
  Eq.{u_3 + 1} (α := R)
    (∑ x_1 ∈ addAntidiagonal (s := x.support) (t := {b}) ⋯ ⋯ (a + b),
      x.coeff x_1.1 * coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.2)
    (∑ ij ∈ {(a, b)}, x.coeff ij.1 * coeff ((single b : (a : R) → R⟦Γ⟧) r) ij.2)
trans₁ : ∑ ij ∈ {(a, b)}, x.coeff ij.1 * coeff ((single b : (a : R) → R⟦Γ⟧) r) ij.2 = x.coeff a * r
⊢ ∑ x_1 ∈ addAntidiagonal (s := x.support) (t := {b}) ⋯ ⋯ (a + b),
      x.coeff x_1.1 * coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.2 =
    x.coeff a * r

Tactic:
trans ∑ ij ∈ {(a, b)}, x.coeff ij.fst * (single b r).coeff ij.snd

Premises used: Prod.mk
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
apply : addAntidiagonal (s := x.support) (t := {b}) ⋯ ⋯ (a + b) = {(a, b)}
⊢ Eq.{u_3 + 1} (α := R)
    (∑ x_1 ∈ addAntidiagonal (s := x.support) (t := {b}) ⋯ ⋯ (a + b),
      x.coeff x_1.1 * coeff ((single b : (a : R) → R⟦Γ⟧) r) x_1.2)
    (∑ ij ∈ {(a, b)}, x.coeff ij.1 * coeff ((single b : (a : R) → R⟦Γ⟧) r) ij.2)

Tactic:
apply sum_congr _ fun _ _ => rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
h :
  ∀ (a1 a2 : Γ),
    (a1, a2) ∈ addAntidiagonal (s := x.support) (t := {b}) ⋯ ⋯ (a + b) ↔
      Membership.mem (γ := Finset (Γ × Γ)) {(a, b)} (a1, a2)
⊢ addAntidiagonal (s := x.support) (t := {b}) ⋯ ⋯ (a + b) = {(a, b)}

Tactic:
ext ⟨a1, a2⟩
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
a1 a2 : Γ
h : a1 ∈ x.support ∧ a2 = b ∧ a1 + a2 = a + b ↔ a1 = a ∧ a2 = b
⊢ (a1, a2) ∈ addAntidiagonal (s := x.support) (t := {b}) ⋯ ⋯ (a + b) ↔
    Membership.mem (γ := Finset (Γ × Γ)) {(a, b)} (a1, a2)

Tactic:
simp only [Set.mem_singleton_iff, Prod.mk_inj, mem_addAntidiagonal, mem_singleton]

Premises used: Finset.mem_singleton, Prod.mk_inj, Set.mem_singleton_iff, Finset.mem_addAntidiagonal
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
a1 a2 : Γ
h : a1 ∈ x.support ∧ a2 = b ∧ a1 + a2 = a + b → a1 = a ∧ a2 = b
h₁ : a1 = a ∧ a2 = b → a1 ∈ x.support ∧ a2 = b ∧ a1 + a2 = a + b
⊢ a1 ∈ x.support ∧ a2 = b ∧ a1 + a2 = a + b ↔ a1 = a ∧ a2 = b

Tactic:
constructor
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
a1 a2 : Γ
left : a1 ∈ x.support
h1 : a1 + a2 = a + a2
⊢ a1 = a ∧ a2 = a2

Tactic:
⟨add_right_cancel h1, rfl⟩

Premises used: add_right_cancel, And.intro, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
a1 a2 : Γ
left : a1 ∈ x.support
h1 : a1 + a2 = a + a2
⊢ a1 = a ∧ a2 = a2

Tactic:
exact ⟨add_right_cancel h1, rfl⟩
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
hr : ¬r = 0
a1 a2 : Γ
hx : ¬x.coeff a1 = 0
⊢ a1 ∈ x.support ∧ a2 = a2 ∧ a1 + a2 = a1 + a2

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
⊢ ∑ ij ∈ {(a, b)}, x.coeff ij.1 * coeff ((single b : (a : R) → R⟦Γ⟧) r) ij.2 = x.coeff a * r

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ' : Type u_2
R : Type u_3
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder Γ'
inst_2 : AddCommGroup Γ'
inst_3 : IsOrderedAddMonoid Γ'
r : R
x : R⟦Γ'⟧
a b : Γ'
⊢ (HMul.hMul (α := R⟦Γ'⟧) ((single b : (a : R) → R⟦Γ'⟧) r : R⟦Γ'⟧) x).coeff a = r * x.coeff (a - b)

Tactic:
simpa using coeff_single_mul_add (a := a - b) (b := b)

Premises used: HahnSeries.coeff_single_mul_add
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ' : Type u_2
R : Type u_3
inst : NonUnitalNonAssocSemiring R
inst_1 : PartialOrder Γ'
inst_2 : AddCommGroup Γ'
inst_3 : IsOrderedAddMonoid Γ'
r : R
x : R⟦Γ'⟧
a b : Γ'
⊢ (HMul.hMul (β := R⟦Γ'⟧) x ((single b : (a : R) → R⟦Γ'⟧) r : R⟦Γ'⟧)).coeff a = x.coeff (a - b) * r

Tactic:
simpa using coeff_mul_single_add (a := a - b) (b := b)

Premises used: HahnSeries.coeff_mul_single_add
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a : Γ
rw : (HMul.hMul (β := R⟦Γ⟧) x ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)).coeff (a + 0) = x.coeff (a + 0) * r
rw₁ : x.coeff a * r = x.coeff (a + 0) * r
rw₂ rw₃ : x.coeff a * r = x.coeff a * r
⊢ (HMul.hMul (β := R⟦Γ⟧) x ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)).coeff a = x.coeff a * r

Tactic:
rw [← add_zero a, coeff_mul_single_add, add_zero]

Premises used: HahnSeries.coeff_mul_single_add, add_zero
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a : Γ
rw : (HMul.hMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).coeff (a + 0) = r * x.coeff (a + 0)
rw₁ : r * x.coeff a = r * x.coeff (a + 0)
rw₂ rw₃ : r * x.coeff a = r * x.coeff a
⊢ (HMul.hMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).coeff a = r * x.coeff a

Tactic:
rw [← add_zero a, coeff_single_mul_add, add_zero]

Premises used: HahnSeries.coeff_single_mul_add, add_zero
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
r : R
x : R⟦Γ⟧
coeff : ∀ (x_1 : Γ), (HMul.hMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).coeff x_1 = (r • x).coeff x_1
⊢ HMul.hMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x = r • x

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
r : R
x : R⟦Γ⟧
x_1 : Γ
⊢ (HMul.hMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).coeff x_1 = (r • x).coeff x_1

Tactic:
coeff_single_zero_mul

Premises used: HahnSeries.coeff_single_zero_mul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
r : R
x : R⟦Γ⟧
x_1 : Γ
⊢ (HMul.hMul (α := R⟦Γ⟧) ((single 0 : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).coeff x_1 = (r • x).coeff x_1

Tactic:
exact coeff_single_zero_mul

Premises used: HahnSeries.coeff_single_zero_mul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
⊢ support.{u_1, u_3} (R := R)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
        (HSMul.hSMul (β := HahnModule Γ R R) x
          ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) y : HahnModule Γ R R))) ⊆
    x.support +ᵥ y.support

Tactic:
HahnModule.support_smul_subset_vadd_support

Premises used: HahnModule.support_smul_subset_vadd_support
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
⊢ support.{u_1, u_3} (R := R)
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
        (HSMul.hSMul (β := HahnModule Γ R R) x
          ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) y : HahnModule Γ R R))) ⊆
    x.support +ᵥ y.support

Tactic:
exact HahnModule.support_smul_subset_vadd_support

Premises used: HahnModule.support_smul_subset_vadd_support
-- 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 : NonUnitalNonAssocSemiring R
x : R⟦Γ⟧
coeff : ∀ (x_1 : Γ), (0 * x).coeff x_1 = HahnSeries.coeff 0 x_1
⊢ 0 * x = 0

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 : NonUnitalNonAssocSemiring R
x : R⟦Γ⟧
x_1 : Γ
⊢ (0 * x).coeff x_1 = coeff 0 x_1

Tactic:
simp [coeff_mul]

Premises used: HahnSeries.coeff_mul
-- 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 : NonUnitalNonAssocSemiring R
x : R⟦Γ⟧
coeff : ∀ (x_1 : Γ), (x * 0).coeff x_1 = HahnSeries.coeff 0 x_1
⊢ x * 0 = 0

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 : NonUnitalNonAssocSemiring R
x : R⟦Γ⟧
x_1 : Γ
⊢ (x * 0).coeff x_1 = coeff 0 x_1

Tactic:
simp [coeff_mul]

Premises used: HahnSeries.coeff_mul
-- 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⟦Γ⟧
simp :
  coeff
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
        (HSMul.hSMul (β := HahnModule Γ R R) x
          ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) y : HahnModule Γ R R)))
      (x.order + y.order) =
    x.leadingCoeff * y.leadingCoeff
⊢ (x * y).coeff (x.order + y.order) = x.leadingCoeff * y.leadingCoeff

Tactic:
simp only [← of_symm_smul_of_eq_mul]

Premises used: HahnSeries.of_symm_smul_of_eq_mul
-- 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⟦Γ⟧
⊢ coeff
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
        (HSMul.hSMul (β := HahnModule Γ R R) x
          ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) y : HahnModule Γ R R)))
      (x.order + y.order) =
    x.leadingCoeff * y.leadingCoeff

Tactic:
HahnModule.coeff_smul_order_add_order x y

Premises used: HahnModule.coeff_smul_order_add_order
-- 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⟦Γ⟧
⊢ coeff
      ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
        (HSMul.hSMul (β := HahnModule Γ R R) x
          ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) y : HahnModule Γ R R)))
      (x.order + y.order) =
    x.leadingCoeff * y.leadingCoeff

Tactic:
exact HahnModule.coeff_smul_order_add_order x y

Premises used: HahnModule.coeff_smul_order_add_order
-- 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
pos : ∀ (hx : x = 0), (x * y).orderTop = x.orderTop + y.orderTop
neg : ∀ (hx : ¬x = 0), (x * y).orderTop = x.orderTop + y.orderTop
⊢ (x * y).orderTop = x.orderTop + y.orderTop

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⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : x = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop

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⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
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⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
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⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : ¬y = 0
rwa rwa₁ rwa₂ rwa₃ : x.leadingCoeff * y.leadingCoeff ≠ 0
⊢ (x * y).coeff (x.order + y.order) ≠ 0

Tactic:
rwa [coeff_mul_order_add_order x y]

Premises used: HahnSeries.coeff_mul_order_add_order
-- 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 = 0
hy : ¬y = 0
⊢ (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]
-- 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_1 : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
h : x * y = 0
⊢ False

Tactic:
simp [h] at this
-- 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 = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
⊢ x * y ≠ 0

Tactic:
have hxy : x * y ≠ 0 := fun h ↦ (by simp [h] at this)
-- 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 = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
hxy : x * y ≠ 0
neg : (x * y).order = x.order + y.order
⊢ (x * y).orderTop = x.orderTop + y.orderTop

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]

Premises used: WithTop.coe_eq_coe, HahnSeries.order_eq_orderTop_of_ne_zero, WithTop.coe_add
-- 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 = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
hxy : x * y ≠ 0
⊢ (x * y).order = x.order + y.order

Tactic:
le_antisymm (order_le_of_coeff_ne_zero this) ?_

Premises used: HahnSeries.order_le_of_coeff_ne_zero, le_antisymm
-- 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 = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
hxy : x * y ≠ 0
neg : x.order + y.order ≤ (x * y).order
⊢ (x * y).order = x.order + y.order

Tactic:
refine le_antisymm (order_le_of_coeff_ne_zero this) ?_

Premises used: HahnSeries.order_le_of_coeff_ne_zero, le_antisymm
-- 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 = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
hxy : x * y ≠ 0
neg : Set.IsWF.min (s := x.support + y.support) ⋯ ⋯ ≤ ⋯.min (s := (x * y).support) ⋯
⊢ x.order + y.order ≤ (x * y).order

Tactic:
rw [HahnSeries.order_of_ne hx, HahnSeries.order_of_ne hy, HahnSeries.order_of_ne hxy,
    ← Set.IsWF.min_add]

Premises used: HahnSeries.order_of_ne, Set.IsWF.min_add
-- 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 = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
hxy : x * y ≠ 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 = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
hxy : x * y ≠ 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⟦Γ⟧
inst_4 : NoZeroDivisors R
pos : ∀ (hx : x = 0), (x * y).orderTop = x.orderTop + y.orderTop
neg : ∀ (hx : ¬x = 0), (x * y).orderTop = x.orderTop + y.orderTop
⊢ (x * y).orderTop = x.orderTop + y.orderTop

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).orderTop = x.orderTop + y.orderTop

Tactic:
simp [hx]