awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
Goal:
R : Type u_1
inst : CommRing R
a : R[X]
rw :
  HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) a : R[X]) -
      HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) a =
    0
rw₁ :
  HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) a -
      HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) a =
    0
⊢ a.wronskian a = 0
have rw₂ : Eq.{u_1 + 1} (α := R[X]) 0 0
Tactic: rw [wronskian, mul_comm, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ 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
have rw : (HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])).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: rw [max_lt_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])).degree < a.degree + b.degree ∧
    (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b).degree < a.degree + b.degree
have constructor : (HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])).degree < a.degree + b.degree
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
constructor : (HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])).degree < a.degree + b.degree
⊢ (HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])).degree < a.degree + b.degree ∧
    (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b).degree < a.degree + b.degree
have constructor₁ : (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b).degree < a.degree + b.degree
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])).degree < a.degree + b.degree
have hab : (HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])).degree ≤
  a.degree + degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) b)
Tactic: apply lt_of_le_of_lt
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
hab :
  (HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])).degree ≤
    a.degree + degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) b)
⊢ (HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])).degree < a.degree + b.degree
have hbc : a.degree + degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) b) < a.degree + b.degree
Tactic: apply lt_of_le_of_lt
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
hab :
  (HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])).degree ≤
    a.degree + degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) b)
hbc : a.degree + degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) b) < a.degree + b.degree
⊢ (HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])).degree < a.degree + b.degree
have b₁ : WithBot ℕ
Tactic: apply lt_of_le_of_lt
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ a.degree + degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) b) < a.degree + b.degree
have ha₁ : a.degree ≠ ⊥
Tactic: rw [← Polynomial.degree_ne_bot] at ha
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a.degree ≠ ⊥
hb : b ≠ 0
⊢ a.degree + degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) b) < a.degree + b.degree
have hbc : degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) b) < b.degree
Tactic: rw [WithBot.add_lt_add_iff_left ha]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
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 < a.degree + b.degree
have 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
Tactic: apply lt_of_le_of_lt
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
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
⊢ (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b).degree < a.degree + b.degree
have hbc : degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) a) + b.degree < a.degree + b.degree
Tactic: apply lt_of_le_of_lt
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
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
⊢ (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b).degree < a.degree + b.degree
have b₁ : WithBot ℕ
Tactic: apply lt_of_le_of_lt
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) a) + b.degree < a.degree + b.degree
have hb₁ : b.degree ≠ ⊥
Tactic: rw [← Polynomial.degree_ne_bot] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
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) + b.degree < a.degree + b.degree
have hbc : degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) a) < a.degree
Tactic: rw [WithBot.add_lt_add_iff_right hb]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
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 < a.degree + b.degree
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
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
⊢ (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b).degree < a.degree + b.degree
have hbc : degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) a) + 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
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
⊢ (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b).degree < a.degree + b.degree
have b₁ : WithBot ℕ
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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.wronskian b).degree < a.degree + b.degree
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
h : a = 0
⊢ False
have hw₁ : wronskian 0 b ≠ 0
Tactic: subst h
Cleared hypotheses: a, hw, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
b : R[X]
hw : wronskian 0 b ≠ 0
⊢ False
have hw₁ : Ne.{u_1 + 1} (α := R[X]) 0 0
Tactic: rw [wronskian_zero_left] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
⊢ (a.wronskian b).natDegree < a.natDegree + b.natDegree
have ha : a ≠ 0
Tactic: have ha : a ≠ 0 := by intro h; subst h; rw [wronskian_zero_left] at hw; exact hw rfl
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
h : b = 0
⊢ False
have hw₁ : a.wronskian 0 ≠ 0
Tactic: subst h
Cleared hypotheses: b, hw, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
a : R[X]
ha : a ≠ 0
hw : a.wronskian 0 ≠ 0
⊢ False
have hw₁ : Ne.{u_1 + 1} (α := R[X]) 0 0
Tactic: rw [wronskian_zero_right] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
⊢ (a.wronskian b).natDegree < a.natDegree + b.natDegree
have hb : b ≠ 0
Tactic: have hb : b ≠ 0 := by intro h; subst h; rw [wronskian_zero_right] at hw; exact hw rfl
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
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).natDegree < a.natDegree + b.natDegree
have rw : (↑(a.wronskian b).natDegree : WithBot ℕ) < (↑a.natDegree : WithBot ℕ) + (↑b.natDegree : WithBot ℕ)
Tactic: rw [← WithBot.coe_lt_coe, WithBot.coe_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
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).natDegree : WithBot ℕ) < (↑a.natDegree : WithBot ℕ) + (↑b.natDegree : WithBot ℕ)
have h : (a.wronskian b).degree = (↑(a.wronskian b).natDegree : WithBot ℕ)
Tactic: convert! ← degree_wronskian_lt_add ha hb
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
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 ℕ)
⊢ (↑(a.wronskian b).natDegree : WithBot ℕ) < (↑a.natDegree : WithBot ℕ) + (↑b.natDegree : WithBot ℕ)
have h₁ : a.degree = (↑a.natDegree : WithBot ℕ)
Tactic: convert! ← degree_wronskian_lt_add ha hb
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
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 ℕ)
⊢ (↑(a.wronskian b).natDegree : WithBot ℕ) < (↑a.natDegree : WithBot ℕ) + (↑b.natDegree : WithBot ℕ)
have h₂ : b.degree = (↑b.natDegree : WithBot ℕ)
Tactic: convert! ← degree_wronskian_lt_add ha hb
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (hypothesis)
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
⊢ 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])
have 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
Tactic: rw [wronskian, sub_eq_iff_eq_add, zero_add] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
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
⊢ 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])
have left : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) (0 : R[X])
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
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])
⊢ 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])
have right : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) b : R[X]) (0 : R[X])
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
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
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) (0 : R[X])
have left : a ∣ (derivative : (a : R[X]) → R[X]) a
Tactic: rw [← dvd_derivative_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
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 ∣ (derivative : (a : R[X]) → R[X]) a
have left : a ∣ HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b
Tactic: apply hc.dvd_of_dvd_mul_right
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
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]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b
have left : a ∣ HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])
Tactic: rw [← hw]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
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
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) b : R[X]) (0 : R[X])
have right : b ∣ (derivative : (a : R[X]) → R[X]) b
Tactic: rw [← dvd_derivative_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
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 ∣ (derivative : (a : R[X]) → R[X]) b
have right : b ∣ HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])
Tactic: apply hc.symm.dvd_of_dvd_mul_left
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
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]) a ((derivative : (a : R[X]) → R[X]) b : R[X])
have right : b ∣ HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b
Tactic: rw [hw]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (hypothesis)
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])
⊢ a.wronskian b = 0
have hda : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) (0 : R[X])
Tactic: obtain ⟨hda, hdb⟩ := hdab
Cleared hypotheses: hdab
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (hypothesis)
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])
⊢ a.wronskian b = 0
have hdb : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) b : R[X]) (0 : R[X])
Tactic: obtain ⟨hda, hdb⟩ := hdab
Cleared hypotheses: hdab
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
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])
⊢ 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
have rw : a * 0 - 0 * b = 0
Tactic: rw [hda, hdb]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialAlgebra (goal)
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
have rw : HSMul.hSMul (β := A[X]) a (∑ i ∈ p.support, Polynomial.map (algebraMap R A) ((monomial i : (a : R) → R[X]) (p.coeff i)))
Tactic: rw [toFunBilinear_apply_eq_smul, ← p.sum_monomial_eq, sum, Polynomial.map_sum]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialAlgebra (goal)
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])
    ((((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])
have 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))
Tactic: conv_lhs => rw [toFunBilinear_apply_eq_smul, ← p.sum_monomial_eq, sum, Polynomial.map_sum]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialAlgebra (goal)
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
⊢ (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)
have pos : p.coeff k = 0 → 0 = HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialAlgebra (goal)
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)
⊢ (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)
have 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)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialAlgebra (goal)
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
⊢ (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)
have pos : p.coeff k = 0 → 0 = HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) (p.coeff k) : A)
Tactic: classical split_ifs <;> simp [*]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialAlgebra (goal)
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)
⊢ (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)
have 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)
Tactic: classical split_ifs <;> simp [*]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialAlgebra (goal)
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]
⊢ 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)
have 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))
Tactic: simp_rw [mul_assoc, Algebra.commutes, ← Finset.mul_sum, mul_assoc, ← Finset.mul_sum]