awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
⊢ x ^ (n + 1) * q.smeval y = q.smeval y * x ^ (n + 1)
have hxq : x * q.smeval y = q.smeval y * x
Tactic: have hxq : x * q.smeval y = q.smeval y * x := by
        refine (commute_iff_eq x (q.smeval y)).mp ?_
        exact Commute.symm (smeval_commute_left R q (Commute.symm hc))
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
hxq : x * q.smeval y = q.smeval y * x
⊢ x ^ (n + 1) * q.smeval y = q.smeval y * x ^ (n + 1)
have monomial : x ^ n * x * q.smeval y = q.smeval y * (x ^ n * x)
Tactic: rw [pow_succ, ← mul_assoc, ← ih, mul_assoc, hxq, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
hxq : x * q.smeval y = q.smeval y * x
monomial : x ^ n * x * q.smeval y = q.smeval y * (x ^ n * x)
⊢ x ^ (n + 1) * q.smeval y = q.smeval y * x ^ (n + 1)
have monomial₁ : x ^ n * x * q.smeval y = q.smeval y * x ^ n * x
Tactic: rw [pow_succ, ← mul_assoc, ← ih, mul_assoc, hxq, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
hxq : x * q.smeval y = q.smeval y * x
monomial : x ^ n * x * q.smeval y = q.smeval y * (x ^ n * x)
monomial₁ : x ^ n * x * q.smeval y = q.smeval y * x ^ n * x
⊢ x ^ (n + 1) * q.smeval y = q.smeval y * x ^ (n + 1)
have monomial₂ : x ^ n * x * q.smeval y = x ^ n * q.smeval y * x
Tactic: rw [pow_succ, ← mul_assoc, ← ih, mul_assoc, hxq, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
hxq : x * q.smeval y = q.smeval y * x
monomial : x ^ n * x * q.smeval y = q.smeval y * (x ^ n * x)
monomial₁ : x ^ n * x * q.smeval y = q.smeval y * x ^ n * x
monomial₂ : x ^ n * x * q.smeval y = x ^ n * q.smeval y * x
⊢ x ^ (n + 1) * q.smeval y = q.smeval y * x ^ (n + 1)
have monomial₃ : x ^ n * (x * q.smeval y) = x ^ n * q.smeval y * x
Tactic: rw [pow_succ, ← mul_assoc, ← ih, mul_assoc, hxq, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
hxq : x * q.smeval y = q.smeval y * x
monomial : x ^ n * x * q.smeval y = q.smeval y * (x ^ n * x)
monomial₁ : x ^ n * x * q.smeval y = q.smeval y * x ^ n * x
monomial₂ : x ^ n * x * q.smeval y = x ^ n * q.smeval y * x
monomial₃ : x ^ n * (x * q.smeval y) = x ^ n * q.smeval y * x
⊢ x ^ (n + 1) * q.smeval y = q.smeval y * x ^ (n + 1)
have monomial₄ : x ^ n * (q.smeval y * x) = x ^ n * q.smeval y * x
Tactic: rw [pow_succ, ← mul_assoc, ← ih, mul_assoc, hxq, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * q.smeval y = q.smeval y * x ^ n
hxq : x * q.smeval y = q.smeval y * x
monomial : x ^ n * x * q.smeval y = q.smeval y * (x ^ n * x)
monomial₁ : x ^ n * x * q.smeval y = q.smeval y * x ^ n * x
monomial₂ : x ^ n * x * q.smeval y = x ^ n * q.smeval y * x
monomial₃ : x ^ n * (x * q.smeval y) = x ^ n * q.smeval y * x
monomial₄ : x ^ n * (q.smeval y * x) = x ^ n * q.smeval y * x
⊢ x ^ (n + 1) * q.smeval y = q.smeval y * x ^ (n + 1)
have monomial₅ : x ^ n * (q.smeval y * x) = x ^ n * (q.smeval y * x)
Tactic: rw [pow_succ, ← mul_assoc, ← ih, mul_assoc, hxq, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
n : ℕ
a : R
⊢ Commute (x ^ n) (q.smeval y)
have monomial : Commute (HPow.hPow (β := ℕ) x 0) (q.smeval y)
Tactic: induction n with
    | zero => simp only [npow_zero, Commute.one_left]
    | succ n ih =>
      refine (commute_iff_eq (x ^ (n + 1)) (q.smeval y)).mpr ?_
      rw [commute_iff_eq (x ^ n) (q.smeval y)] at ih
      have hxq : x * q.smeval y = q.smeval y * x := by
        refine (commute_iff_eq x (q.smeval y)).mp ?_
        exact Commute.symm (smeval_commute_left R q (Commute.symm hc))
      rw [pow_succ, ← mul_assoc, ← ih, mul_assoc, hxq, mul_assoc]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
n : ℕ
a : R
monomial : Commute (HPow.hPow (β := ℕ) x 0) (q.smeval y)
⊢ Commute (x ^ n) (q.smeval y)
have monomial₁ : ∀ (n : ℕ) (ih : Commute (x ^ n) (q.smeval y)), Commute (x ^ (n + 1)) (q.smeval y)
Tactic: induction n with
    | zero => simp only [npow_zero, Commute.one_left]
    | succ n ih =>
      refine (commute_iff_eq (x ^ (n + 1)) (q.smeval y)).mpr ?_
      rw [commute_iff_eq (x ^ n) (q.smeval y)] at ih
      have hxq : x * q.smeval y = q.smeval y * x := by
        refine (commute_iff_eq x (q.smeval y)).mp ?_
        exact Commute.symm (smeval_commute_left R q (Commute.symm hc))
      rw [pow_succ, ← mul_assoc, ← ih, mul_assoc, hxq, mul_assoc]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
⊢ Commute (p.smeval x) (q.smeval y)
have add : ∀ (r s : R[X]) (hr : Commute (r.smeval x) (q.smeval y)) (hs : Commute (s.smeval x) (q.smeval y)),
  Commute ((r + s).smeval x) (q.smeval y)
Tactic: induction p using Polynomial.induction_on' with
  | add r s hr hs => exact (smeval_add R r s x) ▸ Commute.add_left hr hs
  | monomial n a =>
    simp only [smeval_monomial]
    refine Commute.smul_left ?_ a
    induction n with
    | zero => simp only [npow_zero, Commute.one_left]
    | succ n ih =>
      refine (commute_iff_eq (x ^ (n + 1)) (q.smeval y)).mpr ?_
      rw [commute_iff_eq (x ^ n) (q.smeval y)] at ih
      have hxq : x * q.smeval y = q.smeval y * x := by
        refine (commute_iff_eq x (q.smeval y)).mp ?_
        exact Commute.symm (smeval_commute_left R q (Commute.symm hc))
      rw [pow_succ, ← mul_assoc, ← ih, mul_assoc, hxq, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : SMulCommClass R S S
x y : S
hc : Commute x y
add :
  ∀ (r s : R[X]) (hr : Commute (r.smeval x) (q.smeval y)) (hs : Commute (s.smeval x) (q.smeval y)),
    Commute ((r + s).smeval x) (q.smeval y)
⊢ Commute (p.smeval x) (q.smeval y)
have monomial : ∀ (n : ℕ) (a : R), Commute (smeval.{u_1, u_2} (R := R) ((monomial n : (a : R) → R[X]) a) x) (q.smeval y)
Tactic: induction p using Polynomial.induction_on' with
  | add r s hr hs => exact (smeval_add R r s x) ▸ Commute.add_left hr hs
  | monomial n a =>
    simp only [smeval_monomial]
    refine Commute.smul_left ?_ a
    induction n with
    | zero => simp only [npow_zero, Commute.one_left]
    | succ n ih =>
      refine (commute_iff_eq (x ^ (n + 1)) (q.smeval y)).mpr ?_
      rw [commute_iff_eq (x ^ n) (q.smeval y)] at ih
      have hxq : x * q.smeval y = q.smeval y * x := by
        refine (commute_iff_eq x (q.smeval y)).mp ?_
        exact Commute.symm (smeval_commute_left R q (Commute.symm hc))
      rw [pow_succ, ← mul_assoc, ← ih, mul_assoc, hxq, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : Algebra R S
x : S
p : R[X]
⊢ (p.sum fun (e : ℕ) (a : R) ↦ (fun (r : R) ↦ HSMul.hSMul (β := S) r 1) a * x ^ e) = p.sum (smul_pow x)
have simp : (p.sum fun (e : ℕ) (a : R) ↦ a • x ^ e) = p.sum (smul_pow x)
Tactic: simp only [Algebra.smul_mul_assoc, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SpecificDegree (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
⊢ Irreducible p ↔ p.roots = 0
have hp0 : p ≠ 0
Tactic: have hp0 : p ≠ 0 := hp.ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SpecificDegree (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hp : Monic.{u_1} (R := R) 1
hp2 : 2 ≤ natDegree.{u_1} (R := R) 1
hp3 : natDegree.{u_1} (R := R) 1 ≤ 3
hp0 : Ne.{u_1 + 1} (α := R[X]) 1 0
⊢ False
have hp2₁ : LE.le (α := ℕ) 2 0
Tactic: rw [natDegree_one] at hp2
Cleared hypotheses: hp2, hp3, hp0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SpecificDegree (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ Irreducible p ↔ p.roots = 0
have hp1 : p ≠ 1
Tactic: have hp1 : p ≠ 1 := by rintro rfl; rw [natDegree_one] at hp2; cases hp2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SpecificDegree (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
⊢ Irreducible p ↔ p.roots = 0
have rw : (∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p) ↔ p.roots = 0
Tactic: rw [hp.irreducible_iff_lt_natDegree_lt hp1]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SpecificDegree (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p) ↔ p.roots = 0
have simp_rw : (∀ (q : R[X]), q.Monic → q.natDegree = 1 → ¬q ∣ p) ↔
  ∀ (a : R), ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ p
Tactic: simp_rw [show p.natDegree / 2 = 1 from
      (Nat.div_le_div_right hp3).antisymm
        (by apply Nat.div_le_div_right (c := 2) hp2),
    show Finset.Ioc 0 1 = {1} from rfl,
    Finset.mem_singleton, Multiset.eq_zero_iff_forall_notMem, mem_roots hp0, ← dvd_iff_isRoot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SpecificDegree (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → q.natDegree = 1 → ¬q ∣ p) ↔
    ∀ (a : R), ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ p
have refine : ∀ (h : ∀ (a : R), ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ p) (q : R[X]) (hq : q.Monic)
  (hq1 : q.natDegree = 1), ¬q ∣ p
Tactic: refine ⟨fun h r ↦ h _ (monic_X_sub_C r) (natDegree_X_sub_C r), fun h q hq hq1 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SpecificDegree (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
h : ∀ (a : R), ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ p
q : R[X]
hq : q.Monic
hq1 : q.natDegree = 1
⊢ ¬q ∣ p
have rw : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-q.coeff 0) : R[X]) ∣ p
Tactic: rw [hq.eq_X_add_C hq1, ← sub_neg_eq_add, ← C_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SpecificDegree (hypothesis)
Goal:
K : Type u_1
inst : Field K
hp2 : 2 ≤ natDegree.{u_1} (R := K) 0
hp3 : natDegree.{u_1} (R := K) 0 ≤ 3
⊢ False
have hp2₁ : LE.le (α := ℕ) 2 0
Tactic: rw [natDegree_zero] at hp2
Cleared hypotheses: hp2, hp3
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SpecificDegree (hypothesis)
Goal:
K : Type u_1
inst : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
⊢ Irreducible p ↔ p.roots = 0
have hp0 : p ≠ 0
Tactic: have hp0 : p ≠ 0 := by rintro rfl; rw [natDegree_zero] at hp2; cases hp2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SpecificDegree (goal)
Goal:
K : Type u_1
inst : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ Irreducible p ↔ p.roots = 0
have ha : p.leadingCoeff⁻¹ ≠ 0
Tactic: rw [← irreducible_mul_leadingCoeff_inv,
      (monic_mul_leadingCoeff_inv hp0).irreducible_iff_roots_eq_zero_of_degree_le_three,
      mul_comm, roots_C_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SpecificDegree (goal)
Goal:
K : Type u_1
inst : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
ha : p.leadingCoeff⁻¹ ≠ 0
⊢ Irreducible p ↔ p.roots = 0
have hp2₁ : 2 ≤ (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).natDegree
Tactic: rw [← irreducible_mul_leadingCoeff_inv,
      (monic_mul_leadingCoeff_inv hp0).irreducible_iff_roots_eq_zero_of_degree_le_three,
      mul_comm, roots_C_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SpecificDegree (goal)
Goal:
K : Type u_1
inst : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
ha : p.leadingCoeff⁻¹ ≠ 0
hp2₁ : 2 ≤ (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).natDegree
⊢ Irreducible p ↔ p.roots = 0
have hp3₁ : (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])).natDegree ≤ 3
Tactic: rw [← irreducible_mul_leadingCoeff_inv,
      (monic_mul_leadingCoeff_inv hp0).irreducible_iff_roots_eq_zero_of_degree_le_three,
      mul_comm, roots_C_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SpecificDegree (hypothesis)
Goal:
K : Type u_1
inst : Field K
p : K[X]
hdeg : Membership.mem (γ := Finset ℕ) (Finset.Icc 1 3) p.natDegree
hnot : ∀ (x : K), ¬p.IsRoot x
⊢ Irreducible p
have hdeg₁ : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
Tactic: rw [Finset.mem_Icc] at hdeg
Cleared hypotheses: hdeg, hnot
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SpecificDegree (goal)
Goal:
K : Type u_1
inst : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
⊢ Irreducible p
have pos : ∀ (hdeg2 : 2 ≤ p.natDegree), Irreducible p
Tactic: by_cases hdeg2 : 2 ≤ p.natDegree
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SpecificDegree (goal)
Goal:
K : Type u_1
inst : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
pos : ∀ (hdeg2 : 2 ≤ p.natDegree), Irreducible p
⊢ Irreducible p
have neg : ∀ (hdeg2 : ¬2 ≤ p.natDegree), Irreducible p
Tactic: by_cases hdeg2 : 2 ≤ p.natDegree
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SpecificDegree (goal)
Goal:
K : Type u_1
inst : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : 2 ≤ p.natDegree
⊢ Irreducible p
have pos : p.roots = 0
Tactic: rw [Polynomial.irreducible_iff_roots_eq_zero_of_degree_le_three hdeg2 hdeg.2]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SpecificDegree (goal)
Goal:
K : Type u_1
inst : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : 2 ≤ p.natDegree
⊢ p.roots = 0
have pos : ∀ (x : K), x ∉ p.roots
Tactic: apply Multiset.eq_zero_of_forall_notMem
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SpecificDegree (goal)
Goal:
K : Type u_1
inst : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : ¬2 ≤ p.natDegree
⊢ Irreducible p
have neg : p.degree = 1
Tactic: apply Polynomial.irreducible_of_degree_eq_one
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SpecificDegree (goal)
Goal:
K : Type u_1
inst : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : ¬2 ≤ p.natDegree
⊢ p.degree = 1
have neg : p.natDegree = 1
Tactic: rw [← Nat.cast_one, Polynomial.degree_eq_iff_natDegree_eq_of_pos (by simp)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SpecificDegree (goal)
Goal:
K : Type u_1
inst : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : ¬2 ≤ p.natDegree
⊢ p.natDegree ≤ 1
have rwa : ∀ (hdeg2 : p.natDegree < 2), p.natDegree ≤ 1
Tactic: rwa [not_le, Nat.lt_succ_iff] at hdeg2
Cleared hypotheses: hdeg2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.SpecificDegree (goal)
Goal:
K : Type u_1
inst : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : ¬2 ≤ p.natDegree
rwa : ∀ (hdeg2 : p.natDegree < 2), p.natDegree ≤ 1
⊢ p.natDegree ≤ 1
have rwa₁ : ∀ (hdeg2 : p.natDegree ≤ 1), p.natDegree ≤ 1
Tactic: rwa [not_le, Nat.lt_succ_iff] at hdeg2
Cleared hypotheses: hdeg2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.Splits
S : Type u_2
inst_1 : Semiring S
i : R →+* S
⊢ (map i f).Splits
have mem : ∀ (x : R[X]),
  Membership.mem (γ := Set R[X])
      ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
        {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
      x →
    (map i x).Splits
Tactic: induction hf using Submonoid.closure_induction
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.Splits
S : Type u_2
inst_1 : Semiring S
i : R →+* S
mem :
  ∀ (x : R[X]),
    Membership.mem (γ := Set R[X])
        ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
          {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
        x →
      (map i x).Splits
⊢ (map i f).Splits
have one : (map i 1).Splits
Tactic: induction hf using Submonoid.closure_induction
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.Splits
S : Type u_2
inst_1 : Semiring S
i : R →+* S
mem :
  ∀ (x : R[X]),
    Membership.mem (γ := Set R[X])
        ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
          {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
        x →
      (map i x).Splits
one : (map i 1).Splits
⊢ (map i f).Splits
have mul : ∀ (x y : R[X]),
  Membership.mem (γ := Submonoid R[X])
      (Submonoid.closure
        ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
          {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
      x →
    Membership.mem (γ := Submonoid R[X])
        (Submonoid.closure
          ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
            {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x}))
        y →
      (map i x).Splits → (map i y).Splits → (map i (x * y)).Splits
Tactic: induction hf using Submonoid.closure_induction
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.natDegree = 0
⊢ f.Splits
have rw : Splits.{u_1} (R := R) ((C : (a : R) → R[X]) (sorry.choose (p := fun (x : R) ↦ (C : (a : R) → R[X]) x = f)))
Tactic: rw [← (natDegree_eq_zero.mp hf).choose_spec]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.natDegree ≤ 1
h : Invertible f.leadingCoeff
⊢ f.Splits
have obtain : ∀ (a b : R)
  (hf :
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) b : R[X])).natDegree ≤
      1)
  (h :
    Invertible
      (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) b : R[X])).leadingCoeff),
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
      ((C : (a : R) → R[X]) b : R[X])).Splits
Tactic: obtain ⟨a, b, rfl⟩ := exists_eq_X_add_C_of_natDegree_le_one hf
Cleared hypotheses: f, hf, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
hf :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree ≤
    1
h :
  Invertible
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).leadingCoeff
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
      ((C : (a : R) → R[X]) b : R[X])).Splits
have inl : ∀
  (hf :
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 0) X)
          ((C : (a : R) → R[X]) b : R[X])).natDegree ≤
      1)
  (h :
    Invertible
      (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 0) X)
          ((C : (a : R) → R[X]) b : R[X])).leadingCoeff),
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 0) X) ((C : (a : R) → R[X]) b : R[X])).Splits
Tactic: rcases eq_or_ne a 0 with rfl | ha
Cleared hypotheses: a, hf, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
hf :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree ≤
    1
h :
  Invertible
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).leadingCoeff
inl :
  ∀
    (hf :
      (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 0) X)
            ((C : (a : R) → R[X]) b : R[X])).natDegree ≤
        1)
    (h :
      Invertible
        (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 0) X)
            ((C : (a : R) → R[X]) b : R[X])).leadingCoeff),
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 0) X) ((C : (a : R) → R[X]) b : R[X])).Splits
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
      ((C : (a : R) → R[X]) b : R[X])).Splits
have inr : ∀ (ha : a ≠ 0),
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
      ((C : (a : R) → R[X]) b : R[X])).Splits
Tactic: rcases eq_or_ne a 0 with rfl | ha
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
hf :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree ≤
    1
h :
  Invertible
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).leadingCoeff
ha : a ≠ 0
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
      ((C : (a : R) → R[X]) b : R[X])).Splits
have inr : ∀ (h : Invertible a),
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
      ((C : (a : R) → R[X]) b : R[X])).Splits
Tactic: replace h : Invertible a := by simpa [leadingCoeff, ha] using h
Cleared hypotheses: h