awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b).degree ≤
    degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) a) + b.degree

Tactic:
degree_mul_le (derivative a) b

Premises used: Polynomial.degree_mul_le, Polynomial.derivative, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b).degree ≤
    degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) a) + b.degree

Tactic:
exact degree_mul_le (derivative a) b

Premises used: Polynomial.degree_mul_le, Polynomial.derivative, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ b.degree ≠ ⊥

Tactic:
rw [← Polynomial.degree_ne_bot] at hb

Premises used: Polynomial.degree_ne_bot
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b.degree ≠ ⊥
hbc : degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) a) < a.degree
⊢ degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) a) + b.degree < a.degree + b.degree

Tactic:
rw [WithBot.add_lt_add_iff_right hb]

Premises used: WithBot.add_lt_add_iff_right
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b.degree ≠ ⊥
⊢ degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) a) < a.degree

Tactic:
Polynomial.degree_derivative_lt ha

Premises used: Polynomial.degree_derivative_lt
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b.degree ≠ ⊥
⊢ degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) a) < a.degree

Tactic:
exact Polynomial.degree_derivative_lt ha

Premises used: Polynomial.degree_derivative_lt
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
hab :
  (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b).degree ≤
    degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) a) + b.degree
hbc : degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) a) + b.degree < a.degree + b.degree
b₁ : WithBot ℕ
hbc₁ : degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) a) + b.degree < a.degree + b.degree
⊢ (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b).degree < a.degree + b.degree

Tactic:
case right =>
        apply lt_of_le_of_lt
        · exact degree_mul_le (derivative a) b
        · rw [← Polynomial.degree_ne_bot] at hb
          rw [WithBot.add_lt_add_iff_right hb]
          exact Polynomial.degree_derivative_lt ha

Premises used: Polynomial.degree_mul_le, Polynomial.derivative, lt_of_le_of_lt, Polynomial.degree_derivative_lt, Polynomial.degree_ne_bot, DFunLike.coe, WithBot.add_lt_add_iff_right
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
a₁ :
  max (HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])).degree
      (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b).degree <
    a.degree + b.degree
⊢ (a.wronskian b).degree < a.degree + b.degree

Tactic:
calc
    (wronskian a b).degree ≤ max (a * derivative b).degree (derivative a * b).degree :=
      Polynomial.degree_sub_le _ _
    _ < a.degree + b.degree := by
      rw [max_lt_iff]
      constructor
      case left =>
        apply lt_of_le_of_lt
        · exact degree_mul_le a (derivative b)
        · rw [← Polynomial.degree_ne_bot] at ha
          rw [WithBot.add_lt_add_iff_left ha]
          exact Polynomial.degree_derivative_lt hb
      case right =>
        apply lt_of_le_of_lt
        · exact degree_mul_le (derivative a) b
        · rw [← Polynomial.degree_ne_bot] at hb
          rw [WithBot.add_lt_add_iff_right hb]
          exact Polynomial.degree_derivative_lt ha

Premises used: Polynomial.derivative, HMul.hMul, Polynomial.degree, Max.max, Polynomial.degree_sub_le, Polynomial.wronskian, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
h : a = 0
⊢ wronskian 0 b ≠ 0

Tactic:
subst h
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
b : R[X]
hw : wronskian 0 b ≠ 0
⊢ Ne.{u_1 + 1} (α := R[X]) 0 0

Tactic:
rw [wronskian_zero_left] at hw

Premises used: Polynomial.wronskian_zero_left
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
b : R[X]
hw : Ne.{u_1 + 1} (α := R[X]) 0 0
⊢ False

Tactic:
hw rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
b : R[X]
hw : Ne.{u_1 + 1} (α := R[X]) 0 0
⊢ False

Tactic:
exact hw rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
⊢ a ≠ 0

Tactic:
have ha : a ≠ 0 := by intro h; subst h; rw [wronskian_zero_left] at hw; exact hw rfl
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
h : b = 0
⊢ a.wronskian 0 ≠ 0

Tactic:
subst h
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a : R[X]
ha : a ≠ 0
hw : a.wronskian 0 ≠ 0
⊢ Ne.{u_1 + 1} (α := R[X]) 0 0

Tactic:
rw [wronskian_zero_right] at hw

Premises used: Polynomial.wronskian_zero_right
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a : R[X]
ha : a ≠ 0
hw : Ne.{u_1 + 1} (α := R[X]) 0 0
⊢ False

Tactic:
hw rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a : R[X]
ha : a ≠ 0
hw : Ne.{u_1 + 1} (α := R[X]) 0 0
⊢ False

Tactic:
exact hw rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
⊢ b ≠ 0

Tactic:
have hb : b ≠ 0 := by intro h; subst h; rw [wronskian_zero_right] at hw; exact hw rfl
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
rw : (↑(a.wronskian b).natDegree : WithBot ℕ) < (↑a.natDegree : WithBot ℕ) + (↑b.natDegree : WithBot ℕ)
⊢ (a.wronskian b).natDegree < a.natDegree + b.natDegree

Tactic:
rw [← WithBot.coe_lt_coe, WithBot.coe_add]

Premises used: WithBot.coe_lt_coe, WithBot.coe_add
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.wronskian b).degree < a.degree + b.degree

Tactic:
degree_wronskian_lt_add ha hb

Premises used: Polynomial.degree_wronskian_lt_add
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
h : (a.wronskian b).degree = (↑(a.wronskian b).natDegree : WithBot ℕ)
h₁ : a.degree = (↑a.natDegree : WithBot ℕ)
h₂ : b.degree = (↑b.natDegree : WithBot ℕ)
⊢ (↑(a.wronskian b).natDegree : WithBot ℕ) < (↑a.natDegree : WithBot ℕ) + (↑b.natDegree : WithBot ℕ)

Tactic:
convert! ← degree_wronskian_lt_add ha hb

Premises used: Polynomial.degree_wronskian_lt_add
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.wronskian b).degree = (↑(a.wronskian b).natDegree : WithBot ℕ)

Tactic:
Polynomial.degree_eq_natDegree hw

Premises used: Polynomial.degree_eq_natDegree
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.wronskian b).degree = (↑(a.wronskian b).natDegree : WithBot ℕ)

Tactic:
exact Polynomial.degree_eq_natDegree hw

Premises used: Polynomial.degree_eq_natDegree
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a.degree = (↑a.natDegree : WithBot ℕ)

Tactic:
Polynomial.degree_eq_natDegree ha

Premises used: Polynomial.degree_eq_natDegree
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a.degree = (↑a.natDegree : WithBot ℕ)

Tactic:
exact Polynomial.degree_eq_natDegree ha

Premises used: Polynomial.degree_eq_natDegree
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ b.degree = (↑b.natDegree : WithBot ℕ)

Tactic:
Polynomial.degree_eq_natDegree hb

Premises used: Polynomial.degree_eq_natDegree
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ b.degree = (↑b.natDegree : WithBot ℕ)

Tactic:
exact Polynomial.degree_eq_natDegree hb

Premises used: Polynomial.degree_eq_natDegree
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a.wronskian b = 0
⊢ HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X]) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b

Tactic:
rw [wronskian, sub_eq_iff_eq_add, zero_add] at hw

Premises used: zero_add, sub_eq_iff_eq_add, Polynomial.wronskian
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw :
  HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X]) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b
left : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) (0 : R[X])
right : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) b : R[X]) (0 : R[X])
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) (0 : R[X]) ∧
    Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) b : R[X]) (0 : R[X])

Tactic:
constructor
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw :
  HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X]) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b
left : a ∣ (derivative : (a : R[X]) → R[X]) a
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) (0 : R[X])

Tactic:
rw [← dvd_derivative_iff]

Premises used: Polynomial.dvd_derivative_iff
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw :
  HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X]) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b
left : a ∣ HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b
⊢ a ∣ (derivative : (a : R[X]) → R[X]) a

Tactic:
apply hc.dvd_of_dvd_mul_right

Premises used: IsCoprime.dvd_of_dvd_mul_right
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw :
  HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X]) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b
left : a ∣ HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])
⊢ a ∣ HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b

Tactic:
rw [← hw]
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw :
  HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X]) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b
⊢ a ∣ HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])

Tactic:
dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw :
  HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X]) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b
⊢ a ∣ HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])

Tactic:
exact dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw :
  HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X]) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b
right : b ∣ (derivative : (a : R[X]) → R[X]) b
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) b : R[X]) (0 : R[X])

Tactic:
rw [← dvd_derivative_iff]

Premises used: Polynomial.dvd_derivative_iff
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw :
  HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X]) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b
right : b ∣ HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])
⊢ b ∣ (derivative : (a : R[X]) → R[X]) b

Tactic:
apply hc.symm.dvd_of_dvd_mul_left

Premises used: IsCoprime.symm, IsCoprime.dvd_of_dvd_mul_left
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw :
  HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X]) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b
right : b ∣ HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b
⊢ b ∣ HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])

Tactic:
rw [hw]
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw :
  HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X]) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b
⊢ b ∣ HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b

Tactic:
dvd_mul_left _ _

Premises used: dvd_mul_left
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw :
  HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X]) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b
⊢ b ∣ HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b

Tactic:
exact dvd_mul_left _ _

Premises used: dvd_mul_left
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hdab :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) (0 : R[X]) ∧
    Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) b : R[X]) (0 : R[X])
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) (0 : R[X])

Tactic:
obtain ⟨hda, hdb⟩ := hdab
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hdab :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) (0 : R[X]) ∧
    Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) b : R[X]) (0 : R[X])
hda : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) (0 : R[X])
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) b : R[X]) (0 : R[X])

Tactic:
obtain ⟨hda, hdb⟩ := hdab
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hda : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) (0 : R[X])
hdb : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) b : R[X]) (0 : R[X])
rw : a * 0 - 0 * b = 0
⊢ HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X]) -
      HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b =
    0

Tactic:
rw [hda, hdb]
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hda : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) (0 : R[X])
hdb : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) b : R[X]) (0 : R[X])
⊢ a * 0 - 0 * b = 0

Tactic:
simp only [mul_zero, zero_mul, sub_self]

Premises used: sub_self, MulZeroClass.zero_mul, MulZeroClass.mul_zero
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
p : R[X]
⊢ (((toFunBilinear R A : (a : A) → R[X] →ₗ[R] A[X]) a : LinearMap.{u_1, u_1, u_1, u_3} (RingHom.id R) R[X] A[X]) :
        (a : R[X]) → A[X])
      p =
    HSMul.hSMul (β := A[X]) a ((aeval X : (a : R[X]) → A[X]) p : A[X])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
p : R[X]
⊢ (((toFunBilinear R A : (a : A) → R[X] →ₗ[R] A[X]) a : LinearMap.{u_1, u_1, u_1, u_3} (RingHom.id R) R[X] A[X]) :
        (a : R[X]) → A[X])
      p =
    HSMul.hSMul (β := A[X]) a (Polynomial.map (algebraMap R A) p)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
p : R[X]
rw :
  HSMul.hSMul (β := A[X]) a
    (∑ i ∈ p.support, Polynomial.map (algebraMap R A) ((monomial i : (a : R) → R[X]) (p.coeff i)))
| (((toFunBilinear R A : (a : A) → R[X] →ₗ[R] A[X]) a : LinearMap.{u_1, u_1, u_1, u_3} (RingHom.id R) R[X] A[X]) :
      (a : R[X]) → A[X])
    p

Tactic:
rw [toFunBilinear_apply_eq_smul, ← p.sum_monomial_eq, sum, Polynomial.map_sum]

Premises used: Polynomial.sum, Polynomial.sum_monomial_eq, PolyEquivTensor.toFunBilinear_apply_eq_smul, Polynomial.map_sum
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
p : R[X]
conv_lhs :
  HSMul.hSMul (β := A[X]) a
      (∑ i ∈ p.support, Polynomial.map (algebraMap R A) ((monomial i : (a : R) → R[X]) (p.coeff i))) =
    p.sum fun (n : ℕ) (r : R) ↦
      (monomial n : (a : A) → A[X]) (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A))
⊢ Eq.{u_3 + 1} (α := A[X])
    ((((toFunBilinear R A : (a : A) → R[X] →ₗ[R] A[X]) a : LinearMap.{u_1, u_1, u_1, u_3} (RingHom.id R) R[X] A[X]) :
          (a : R[X]) → A[X])
        p :
      A[X])
    (p.sum fun (n : ℕ) (r : R) ↦
        (monomial n : (a : A) → A[X]) (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A)) :
      A[X])

Tactic:
conv_lhs => rw [toFunBilinear_apply_eq_smul, ← p.sum_monomial_eq, sum, Polynomial.map_sum]

Premises used: Polynomial.sum, Polynomial.sum_monomial_eq, PolyEquivTensor.toFunBilinear_apply_eq_smul, Polynomial.map_sum
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
p : R[X]
⊢ HSMul.hSMul (β := A[X]) a
      (∑ i ∈ p.support, Polynomial.map (algebraMap R A) ((monomial i : (a : R) → R[X]) (p.coeff i))) =
    p.sum fun (n : ℕ) (r : R) ↦
      (monomial n : (a : A) → A[X]) (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A))

Tactic:
simp [Finset.smul_sum, sum, ← smul_eq_mul]

Premises used: Polynomial.sum, Finset.smul_sum, smul_eq_mul
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
p : R[X]
⊢ Eq.{u_3 + 1} (α := A[X]) ((toFunLinear R A : (a : A ⊗[R] R[X]) → A[X]) (a ⊗ₜ[R] p) : A[X])
    ((((toFunBilinear R A : (a : A) → R[X] →ₗ[R] A[X]) a : LinearMap.{u_1, u_1, u_1, u_3} (RingHom.id R) R[X] A[X]) :
          (a : R[X]) → A[X])
        p :
      A[X])

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p : R[X]
k : ℕ
h : Decidable ¬p.coeff k = 0
a : A
pos : p.coeff k = 0 → 0 = HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A)
neg :
  ¬p.coeff k = 0 →
    HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A) =
      HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A)
⊢ (if ¬p.coeff k = 0 then HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A) else 0) =
    HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A)

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p : R[X]
k : ℕ
h : Decidable ¬p.coeff k = 0
a : A
h_1 : p.coeff k = 0
⊢ 0 = HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A)

Tactic:
simp [*]
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p : R[X]
k : ℕ
h : Decidable ¬p.coeff k = 0
a : A
h_1 : ¬p.coeff k = 0
⊢ HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A) =
    HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A)

Tactic:
simp [*]
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p : R[X]
k : ℕ
h : Decidable ¬p.coeff k = 0
a : A
pos : p.coeff k = 0 → 0 = HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A)
neg :
  ¬p.coeff k = 0 →
    HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A) =
      HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A)
pos₁ : p.coeff k = 0 → 0 = HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A)
neg₁ :
  ¬p.coeff k = 0 →
    HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A) =
      HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A)
pos₂ : p.coeff k = 0 → 0 = HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A)
neg₂ :
  ¬p.coeff k = 0 →
    HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A) =
      HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A)
pos₃ : p.coeff k = 0 → 0 = HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A)
neg₃ :
  ¬p.coeff k = 0 →
    HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A) =
      HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A)
⊢ (if ¬p.coeff k = 0 then HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A) else 0) =
    HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A)

Tactic:
classical split_ifs <;> simp [*]
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
k : ℕ
a₁ a₂ : A
p₁ p₂ : R[X]
simp_rw :
  a₁ * HMul.hMul (β := A) a₂ ((algebraMap R A : (a : R) → A) ((p₁ * p₂).coeff k) : A) =
    a₁ *
      (a₂ *
        ∑ i ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k,
          HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (p₂.coeff i.2) : A)
            ((algebraMap R A : (a : R) → A) (p₁.coeff i.1) : A))
⊢ HMul.hMul (β := A) (a₁ * a₂) ((algebraMap R A : (a : R) → A) ((p₁ * p₂).coeff k) : A) =
    ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k,
      HMul.hMul (β := A) a₁ ((algebraMap R A : (a : R) → A) (p₁.coeff x.1) : A) *
        HMul.hMul (β := A) a₂ ((algebraMap R A : (a : R) → A) (p₂.coeff x.2) : A)

Tactic:
simp_rw [mul_assoc, Algebra.commutes, ← Finset.mul_sum, mul_assoc, ← Finset.mul_sum]

Premises used: Finset.mul_sum, mul_assoc, Algebra.commutes