awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this_1 : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x
this : Set.IsWF.{u_1} (α := Γ) {a : Γ | y.coeff a ≠ z.coeff a}
a : Γ := this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz
ha : y.coeff a ≠ z.coeff a
⊢ ∀
    x_1 ∈
      addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ (x.order + a) ∪
        addAntidiagonal (s := x.support) (t := z.support) ⋯ ⋯ (x.order + a),
    x_1 ∉ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ (x.order + a) → x.coeff x_1.1 * y.coeff x_1.2 = 0

Tactic:
simp +contextual [← and_or_left, ← or_and_right]

Premises used: and_or_left, or_and_right
-- 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 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
hyz : Eq (α := R⟦Γ⟧) ((fun (x_1 : R⟦Γ⟧) ↦ x_1 * x) y) ((fun (x_1 : R⟦Γ⟧) ↦ x_1 * x) z)
this : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
contrapose! : ∀ (hyz : y ≠ z), y * x ≠ z * x
⊢ y = z

Tactic:
contrapose! hyz
-- 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 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : y ≠ z
simp : ∀ (hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x), ∃ (x_1 : Γ), ¬(y * x).coeff x_1 = (z * x).coeff x_1
⊢ y * x ≠ z * x

Tactic:
simp only [ne_eq, ← coeff_inj, funext_iff, not_forall] at ⊢ hyz

Premises used: funext_iff, ne_eq, HahnSeries.coeff_inj, Classical.not_forall
-- 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 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this_1 : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x
this : Set.IsWF.{u_1} (α := Γ) {a : Γ | y.coeff a ≠ z.coeff a}
a : Γ := this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz
ha : y.coeff a ≠ z.coeff a
⊢ ∃ (x_1 : Γ), ¬(y * x).coeff x_1 = (z * x).coeff x_1

Tactic:
⟨a + x.order, ?_⟩

Premises used: HahnSeries.order, HAdd.hAdd, Exists.intro
-- 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 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this_1 : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x
this : Set.IsWF.{u_1} (α := Γ) {a : Γ | y.coeff a ≠ z.coeff a}
a : Γ := this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz
ha : y.coeff a ≠ z.coeff a
refine : ¬(y * x).coeff (a + x.order) = (z * x).coeff (a + x.order)
⊢ ∃ (x_1 : Γ), ¬(y * x).coeff x_1 = (z * x).coeff x_1

Tactic:
refine ⟨a + x.order, ?_⟩
-- 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 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this_1 : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x
this : Set.IsWF.{u_1} (α := Γ) {a : Γ | y.coeff a ≠ z.coeff a}
a : Γ := this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz
ha : y.coeff a ≠ z.coeff a
hi :
  (a, x.order) ∈
    addAntidiagonal (s := y.support) (t := x.support) ⋯ ⋯ (a + x.order) ∪
      addAntidiagonal (s := z.support) (t := x.support) ⋯ ⋯ (a + x.order)
hfg :
  ∀
    j ∈
      addAntidiagonal (s := y.support) (t := x.support) ⋯ ⋯ (a + x.order) ∪
        addAntidiagonal (s := z.support) (t := x.support) ⋯ ⋯ (a + x.order),
    j ≠ (a, x.order) → y.coeff j.1 * x.coeff j.2 = z.coeff j.1 * x.coeff j.2
rwa :
  ∀
    x_1 ∈
      addAntidiagonal (s := y.support) (t := x.support) ⋯ ⋯ (a + x.order) ∪
        addAntidiagonal (s := z.support) (t := x.support) ⋯ ⋯ (a + x.order),
    x_1 ∉ addAntidiagonal (s := z.support) (t := x.support) ⋯ ⋯ (a + x.order) → z.coeff x_1.1 * x.coeff x_1.2 = 0
rwa₁ :
  ∀
    x_1 ∈
      addAntidiagonal (s := y.support) (t := x.support) ⋯ ⋯ (a + x.order) ∪
        addAntidiagonal (s := z.support) (t := x.support) ⋯ ⋯ (a + x.order),
    x_1 ∉ addAntidiagonal (s := y.support) (t := x.support) ⋯ ⋯ (a + x.order) → y.coeff x_1.1 * x.coeff x_1.2 = 0
⊢ ¬(y * x).coeff (a + x.order) = (z * x).coeff (a + x.order)

Tactic:
rwa [coeff_mul, coeff_mul, sum_subset subset_union_left,
      sum_subset (s₁ := addAntidiagonal _ _ _) subset_union_right,
      sum_eq_sum_iff_single (i := (a, x.order)), mul_left_inj' (coeff_order_eq_zero.not.2 hx)]

Premises used: Iff.mpr, HahnSeries.coeff_mul, Iff.not, Finset.subset_union_left, HahnSeries.coeff_order_eq_zero, Finset.sum_subset, Finset.sum_eq_sum_iff_single, mul_left_inj', Finset.subset_union_right
-- 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 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this_1 : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x
this : Set.IsWF.{u_1} (α := Γ) {a : Γ | y.coeff a ≠ z.coeff a}
a : Γ := this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz
ha : y.coeff a ≠ z.coeff a
hi : ¬y.coeff a = 0 ∨ ¬z.coeff a = 0
⊢ (a, x.order) ∈
    addAntidiagonal (s := y.support) (t := x.support) ⋯ ⋯ (a + x.order) ∪
      addAntidiagonal (s := z.support) (t := x.support) ⋯ ⋯ (a + x.order)

Tactic:
simp [hx]
-- 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 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this_1 : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x
this : Set.IsWF.{u_1} (α := Γ) {a : Γ | y.coeff a ≠ z.coeff a}
a : Γ := this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz
ha : y.coeff a ≠ z.coeff a
hfg :
  ∀ (a_1 b : Γ),
    ¬y.coeff a_1 = 0 ∨ ¬z.coeff a_1 = 0 →
      ¬x.coeff b = 0 → a_1 + b = a + x.order → (a_1 = a → ¬b = x.order) → y.coeff a_1 = z.coeff a_1
⊢ ∀
    j ∈
      addAntidiagonal (s := y.support) (t := x.support) ⋯ ⋯ (a + x.order) ∪
        addAntidiagonal (s := z.support) (t := x.support) ⋯ ⋯ (a + x.order),
    j ≠ (a, x.order) → y.coeff j.1 * x.coeff j.2 = z.coeff j.1 * x.coeff j.2

Tactic:
simp +contextual only [mem_union, mem_addAntidiagonal, mul_eq_mul_right_iff, Prod.mk.injEq,
        ne_eq, ← or_and_right, or_false, and_imp, Prod.forall, mem_support, not_and]

Premises used: and_imp, mul_eq_mul_right_iff, ne_eq, Prod.mk.injEq, Prod.forall, Finset.mem_union, or_false, not_and, or_and_right, HahnSeries.mem_support, Finset.mem_addAntidiagonal
-- 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 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this_1 : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x
this : Set.IsWF.{u_1} (α := Γ) {a : Γ | y.coeff a ≠ z.coeff a}
a : Γ := this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz
ha : y.coeff a ≠ z.coeff a
b c : Γ
hxb : ¬x.coeff c = 0
hbc : b + c = a + x.order
hbc' : b = a → ¬c = x.order
hfg : ∀ (hbc' : y.coeff b ≠ z.coeff b), b = a ∧ c = x.order
⊢ y.coeff b = z.coeff b

Tactic:
contrapose! hbc'
-- 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 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this_1 : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x
this : Set.IsWF.{u_1} (α := Γ) {a : Γ | y.coeff a ≠ z.coeff a}
a : Γ := this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz
ha : y.coeff a ≠ z.coeff a
b c : Γ
hxb : ¬x.coeff c = 0
hbc : b + c = a + x.order
hbc' : y.coeff b ≠ z.coeff b
hfg : a = b ∧ c = x.order
hfg₁ : a = b ∧ x.order = c
hfg₂ : this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz + x.order = b + c
hfg₃ hfg₄ hfg₅ hfg₆ : b + c = this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz + x.order
⊢ b = a ∧ c = x.order

Tactic:
rwa [eq_comm, eq_comm (a := c), ← add_eq_add_iff_eq_and_eq
        (Set.IsWF.min_le _ _ hbc') (order_le_of_coeff_ne_zero hxb), eq_comm]

Premises used: add_eq_add_iff_eq_and_eq, HahnSeries.order_le_of_coeff_ne_zero, eq_comm, Set.IsWF.min_le
-- 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 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this_1 : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x
this : Set.IsWF.{u_1} (α := Γ) {a : Γ | y.coeff a ≠ z.coeff a}
a : Γ := this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz
ha : y.coeff a ≠ z.coeff a
⊢ ∀
    x_1 ∈
      addAntidiagonal (s := y.support) (t := x.support) ⋯ ⋯ (a + x.order) ∪
        addAntidiagonal (s := z.support) (t := x.support) ⋯ ⋯ (a + x.order),
    x_1 ∉ addAntidiagonal (s := z.support) (t := x.support) ⋯ ⋯ (a + x.order) → z.coeff x_1.1 * x.coeff x_1.2 = 0

Tactic:
simp +contextual [← or_and_right]

Premises used: or_and_right
-- 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 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : IsCancelAdd R
inst_5 : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this_1 : AddCancelCommMonoid R := { toAddCommMonoid := inst_3.toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ (x : Γ), ¬y.coeff x = z.coeff x
this : Set.IsWF.{u_1} (α := Γ) {a : Γ | y.coeff a ≠ z.coeff a}
a : Γ := this.min (s := {a : Γ | y.coeff a ≠ z.coeff a}) hyz
ha : y.coeff a ≠ z.coeff a
⊢ ∀
    x_1 ∈
      addAntidiagonal (s := y.support) (t := x.support) ⋯ ⋯ (a + x.order) ∪
        addAntidiagonal (s := z.support) (t := x.support) ⋯ ⋯ (a + x.order),
    x_1 ∉ addAntidiagonal (s := y.support) (t := x.support) ⋯ ⋯ (a + x.order) → y.coeff x_1.1 * x.coeff x_1.2 = 0

Tactic:
simp +contextual [← or_and_right]

Premises used: or_and_right
-- 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 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : NoZeroDivisors R
x_1 y_1 x y : R⟦Γ⟧
hxy : x * y = 0
contrapose! : ∀ (hxy : x ≠ 0 ∧ y ≠ 0), x * y ≠ 0
⊢ x = 0 ∨ y = 0

Tactic:
contrapose! hxy
-- 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 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : NoZeroDivisors R
x_1 y_1 x y : R⟦Γ⟧
hxy : x ≠ 0 ∧ y ≠ 0
simp : ∃ (x_2 : Γ), ¬(x * y).coeff x_2 = coeff 0 x_2
⊢ x * y ≠ 0

Tactic:
simp only [ne_eq, HahnSeries.ext_iff, funext_iff, not_forall]

Premises used: funext_iff, ne_eq, HahnSeries.ext_iff, Classical.not_forall
-- 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 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : NoZeroDivisors R
x_1 y_1 x y : R⟦Γ⟧
hxy : x ≠ 0 ∧ y ≠ 0
⊢ ¬(x * y).coeff (x.order + y.order) = coeff 0 (x.order + y.order)

Tactic:
simpa [coeff_mul_order_add_order]

Premises used: HahnSeries.coeff_mul_order_add_order
-- 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 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : NoZeroDivisors R
x_1 y_1 x y : R⟦Γ⟧
hxy : x ≠ 0 ∧ y ≠ 0
⊢ ∃ (x_2 : Γ), ¬(x * y).coeff x_2 = coeff 0 x_2

Tactic:
exact ⟨x.order + y.order, by simpa [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
inst_4 : NoZeroDivisors R
x y : R⟦Γ⟧
hx : x ≠ 0
hy : y ≠ 0
a : (x * y).order ≤ x.order + y.order
a₁ : x.order + y.order ≤ (x * y).order
⊢ (x * y).order = x.order + y.order

Tactic:
apply le_antisymm

Premises used: 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
inst_4 : NoZeroDivisors R
x y : R⟦Γ⟧
hx : x ≠ 0
hy : y ≠ 0
a : (x * y).coeff (x.order + y.order) ≠ 0
⊢ (x * y).order ≤ x.order + y.order

Tactic:
apply order_le_of_coeff_ne_zero

Premises used: HahnSeries.order_le_of_coeff_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
inst_4 : NoZeroDivisors R
x y : R⟦Γ⟧
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).coeff (x.order + y.order) ≠ 0

Tactic:
simp [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
inst_4 : NoZeroDivisors R
x y : R⟦Γ⟧
hx : x ≠ 0
hy : y ≠ 0
a : 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 hx, order_of_ne hy, order_of_ne (mul_ne_zero hx hy), ← Set.IsWF.min_add]

Premises used: HahnSeries.order_of_ne, Set.IsWF.min_add, mul_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
inst_4 : NoZeroDivisors R
x y : R⟦Γ⟧
hx : x ≠ 0
hy : 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
inst_4 : NoZeroDivisors R
x y : R⟦Γ⟧
hx : x ≠ 0
hy : 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 : Semiring R
inst_4 : NoZeroDivisors R
x : R⟦Γ⟧
⊢ (HPow.hPow (β := ℕ) x 0).order = HSMul.hSMul (α := ℕ) 0 x.order

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
inst_4 : NoZeroDivisors R
x : R⟦Γ⟧
n : ℕ
inl : (HPow.hPow (α := R⟦Γ⟧) 0 (n + 1)).order = HSMul.hSMul (β := Γ) (n + 1) (order.{u_1, u_3} (R := R) 0)
inr : ∀ (hx : x ≠ 0), (x ^ (n + 1)).order = (n + 1) • x.order
⊢ (x ^ (n + 1)).order = (n + 1) • x.order

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
inst_4 : NoZeroDivisors R
n : ℕ
⊢ (HPow.hPow (α := R⟦Γ⟧) 0 (n + 1)).order = HSMul.hSMul (β := Γ) (n + 1) (order.{u_1, u_3} (R := R) 0)

Tactic:
simp [pow_succ, succ_nsmul, order_pow, pow_ne_zero, *]

Premises used: pow_succ, pow_ne_zero, succ_nsmul
-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
inst_4 : NoZeroDivisors R
x : R⟦Γ⟧
n : ℕ
hx : x ≠ 0
⊢ (x ^ (n + 1)).order = (n + 1) • x.order

Tactic:
simp [pow_succ, succ_nsmul, order_pow, pow_ne_zero, *]

Premises used: pow_succ, pow_ne_zero, succ_nsmul
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
Goal:
Γ : Type u_1
R : Type u_2
inst : Semiring R
f : R⟦ℕ⟧
coeff :
  ∀ (x : ℕ),
    HahnSeries.coeff
        ((fun (f : PowerSeries R) ↦
            ({ coeff := fun (n : ℕ) ↦ (PowerSeries.coeff n : (a : PowerSeries R) → R) f, isPWO_support' := ⋯ } : R⟦ℕ⟧))
          ((fun (f : R⟦ℕ⟧) ↦ PowerSeries.mk f.coeff) f))
        x =
      f.coeff x
⊢ (fun (f : PowerSeries R) ↦
        ({ coeff := fun (n : ℕ) ↦ (PowerSeries.coeff n : (a : PowerSeries R) → R) f, isPWO_support' := ⋯ } : R⟦ℕ⟧))
      ((fun (f : R⟦ℕ⟧) ↦ PowerSeries.mk f.coeff) f) =
    f

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
Goal:
Γ : Type u_1
R : Type u_2
inst : Semiring R
f : R⟦ℕ⟧
x : ℕ
⊢ coeff
      ((fun (f : PowerSeries R) ↦
          ({ coeff := fun (n : ℕ) ↦ (PowerSeries.coeff n : (a : PowerSeries R) → R) f, isPWO_support' := ⋯ } : R⟦ℕ⟧))
        ((fun (f : R⟦ℕ⟧) ↦ PowerSeries.mk f.coeff) f))
      x =
    f.coeff x

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
Goal:
Γ : Type u_1
R : Type u_2
inst : Semiring R
f : PowerSeries R
h :
  ∀ (n : ℕ),
    Eq (α := R)
      ((PowerSeries.coeff n : (a : PowerSeries R) → R)
          ((fun (f : R⟦ℕ⟧) ↦ PowerSeries.mk f.coeff)
            ((fun (f : PowerSeries R) ↦
                ({ coeff := fun (n : ℕ) ↦ (PowerSeries.coeff n : (a : PowerSeries R) → R) f, isPWO_support' := ⋯ } :
                  R⟦ℕ⟧))
              f)) :
        R)
      ((PowerSeries.coeff n : (a : PowerSeries R) → R) f : R)
⊢ (fun (f : R⟦ℕ⟧) ↦ PowerSeries.mk f.coeff)
      ((fun (f : PowerSeries R) ↦
          ({ coeff := fun (n : ℕ) ↦ (PowerSeries.coeff n : (a : PowerSeries R) → R) f, isPWO_support' := ⋯ } : R⟦ℕ⟧))
        f) =
    f

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
Goal:
Γ : Type u_1
R : Type u_2
inst : Semiring R
f : PowerSeries R
n : ℕ
⊢ Eq (α := R)
    ((PowerSeries.coeff n : (a : PowerSeries R) → R)
        ((fun (f : R⟦ℕ⟧) ↦ PowerSeries.mk f.coeff)
          ((fun (f : PowerSeries R) ↦
              ({ coeff := fun (n : ℕ) ↦ (PowerSeries.coeff n : (a : PowerSeries R) → R) f, isPWO_support' := ⋯ } :
                R⟦ℕ⟧))
            f)) :
      R)
    ((PowerSeries.coeff n : (a : PowerSeries R) → R) f : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
Goal:
Γ : Type u_1
R : Type u_2
inst : Semiring R
f g : R⟦ℕ⟧
h :
  ∀ (n : ℕ),
    Eq (α := R) ((PowerSeries.coeff n : (a : PowerSeries R) → R) (PowerSeries.mk (f * g).coeff) : R)
      ((PowerSeries.coeff n : (a : PowerSeries R) → R) (PowerSeries.mk f.coeff * PowerSeries.mk g.coeff) : R)
⊢ PowerSeries.mk (f * g).coeff = PowerSeries.mk f.coeff * PowerSeries.mk g.coeff

Tactic:
ext n
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
Goal:
Γ : Type u_1
R : Type u_2
inst : Semiring R
f g : R⟦ℕ⟧
n : ℕ
h :
  Eq.{u_2 + 1} (α := R) (∑ ij ∈ addAntidiagonal (s := f.support) (t := g.support) ⋯ ⋯ n, f.coeff ij.1 * g.coeff ij.2)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, f.coeff x.1 * g.coeff x.2)
⊢ Eq (α := R) ((PowerSeries.coeff n : (a : PowerSeries R) → R) (PowerSeries.mk (f * g).coeff) : R)
    ((PowerSeries.coeff n : (a : PowerSeries R) → R) (PowerSeries.mk f.coeff * PowerSeries.mk g.coeff) : R)

Tactic:
simp only [PowerSeries.coeff_mul, PowerSeries.coeff_mk, coeff_mul]

Premises used: HahnSeries.coeff_mul, PowerSeries.coeff_mk, PowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
Goal:
Γ : Type u_1
R : Type u_2
inst : Semiring R
f g : R⟦ℕ⟧
n : ℕ
⊢ Eq.{u_2 + 1} (α := R) (∑ ij ∈ addAntidiagonal (s := f.support) (t := g.support) ⋯ ⋯ n, f.coeff ij.1 * g.coeff ij.2)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, f.coeff x.1 * g.coeff x.2)

Tactic:
(sum_filter_ne_zero _).symm.trans <| (sum_congr ?_ fun _ _ ↦ rfl).trans <|
      sum_filter_ne_zero _

Premises used: Finset.sum_filter_ne_zero, Eq.symm, Finset.sum_congr, rfl, Eq.trans
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
Goal:
Γ : Type u_1
R : Type u_2
inst : Semiring R
f g : R⟦ℕ⟧
n : ℕ
h :
  {x ∈ addAntidiagonal (s := f.support) (t := g.support) ⋯ ⋯ n | f.coeff x.1 * g.coeff x.2 ≠ 0} =
    {x ∈ @antidiagonal _ Nat.instAddMonoid _ n | f.coeff x.1 * g.coeff x.2 ≠ 0}
⊢ Eq.{u_2 + 1} (α := R) (∑ ij ∈ addAntidiagonal (s := f.support) (t := g.support) ⋯ ⋯ n, f.coeff ij.1 * g.coeff ij.2)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, f.coeff x.1 * g.coeff x.2)

Tactic:
refine (sum_filter_ne_zero _).symm.trans <| (sum_congr ?_ fun _ _ ↦ rfl).trans <|
      sum_filter_ne_zero _

Premises used: Finset.sum_filter_ne_zero, Eq.symm, Finset.sum_congr, rfl, Eq.trans
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
Goal:
Γ : Type u_1
R : Type u_2
inst : Semiring R
f g : R⟦ℕ⟧
n : ℕ
h :
  ∀ (m : ℕ × ℕ),
    m ∈ {x ∈ addAntidiagonal (s := f.support) (t := g.support) ⋯ ⋯ n | f.coeff x.1 * g.coeff x.2 ≠ 0} ↔
      m ∈ {x ∈ @antidiagonal _ Nat.instAddMonoid _ n | f.coeff x.1 * g.coeff x.2 ≠ 0}
⊢ {x ∈ addAntidiagonal (s := f.support) (t := g.support) ⋯ ⋯ n | f.coeff x.1 * g.coeff x.2 ≠ 0} =
    {x ∈ @antidiagonal _ Nat.instAddMonoid _ n | f.coeff x.1 * g.coeff x.2 ≠ 0}

Tactic:
ext m
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
Goal:
Γ : Type u_1
R : Type u_2
inst : Semiring R
f g : R⟦ℕ⟧
n : ℕ
m : ℕ × ℕ
h : f.coeff m.1 * g.coeff m.2 ≠ 0 → (f.coeff m.1 ≠ 0 ∧ g.coeff m.2 ≠ 0 ∧ m.1 + m.2 = n ↔ m.1 + m.2 = n)
⊢ m ∈ {x ∈ addAntidiagonal (s := f.support) (t := g.support) ⋯ ⋯ n | f.coeff x.1 * g.coeff x.2 ≠ 0} ↔
    m ∈ {x ∈ @antidiagonal _ Nat.instAddMonoid _ n | f.coeff x.1 * g.coeff x.2 ≠ 0}

Tactic:
simp only [mem_antidiagonal, mem_addAntidiagonal, and_congr_left_iff, mem_filter,
      mem_support]

Premises used: Finset.HasAntidiagonal.mem_antidiagonal, and_congr_left_iff, Finset.mem_filter, HahnSeries.mem_support, Finset.mem_addAntidiagonal