awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
S : Type v
T_1 : Type w
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
inst_2 : Semiring T_1
p : T_1[X]
g : ℕ → T_1 → R[X]
x : S
T : AddMonoidHom.{u, v} R[X] S := { toFun := eval₂ f x, map_zero' := ⋯, map_add' := ⋯ }
A : ∀ (y : R[X]), eval₂ f x y = (T : (a : R[X]) → S) y
rw :
  Eq.{v + 1} (α := S) ((T : (a : R[X]) → S) (∑ n ∈ p.support, g n (p.coeff n)) : S)
    (p.sum fun (n : ℕ) (a : T_1) ↦ (T : (a : R[X]) → S) (g n a) : S)
rw₁ :
  Eq.{v + 1} (α := S) (∑ x ∈ p.support, (T : (a : R[X]) → S) (g x (p.coeff x)))
    (p.sum fun (n : ℕ) (a : T_1) ↦ (T : (a : R[X]) → S) (g n a))
⊢ Eq.{v + 1} (α := S) ((T : (a : R[X]) → S) (p.sum g) : S)
    (p.sum fun (n : ℕ) (a : T_1) ↦ (T : (a : R[X]) → S) (g n a) : S)
have rw₂ : Eq.{v + 1} (α := S) (∑ x ∈ p.support, (T : (a : R[X]) → S) (g x (p.coeff x)))
  (∑ n ∈ p.support, (T : (a : R[X]) → S) (g n (p.coeff n)))
Tactic: rw [sum, map_sum, sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : S
p : R[ℕ]
⊢ eval₂ f x { toFinsupp := p : R[X] } =
    (liftNC (↑f : R →+ S)
          (⇑((powersHom S : (a : S) → Multiplicative ℕ →* S) x : Multiplicative ℕ →* S) : (a : Multiplicative ℕ) → S) :
        (a : R[ℕ]) → S)
      p
have simp : Eq.{v + 1} (α := S)
  (∑ x_1 ∈ p.support, HMul.hMul (α := S) ((f : (a : R) → S) ((p : (a : ℕ) → R) x_1 : R) : S) (x ^ x_1) : S)
  ((liftNC (↑f : R →+ S)
          (⇑((powersHom S : (a : S) → Multiplicative ℕ →* S) x : Multiplicative ℕ →* S) : (a : Multiplicative ℕ) → S) :
        (a : R[ℕ]) → S)
      p :
    S)
Tactic: simp only [eval₂_eq_sum, sum, support, coeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
p q : R[X]
inst_1 : Semiring S
f : R →+* S
x : S
hf : ∀ (k : ℕ), Commute ((f : (a : R) → S) (q.coeff k)) x
⊢ eval₂ f x (p * q) = eval₂ f x p * eval₂ f x q
have rcases : ∀ (p : R[ℕ]), eval₂ f x ({ toFinsupp := p : R[X] } * q) = eval₂ f x { toFinsupp := p : R[X] } * eval₂ f x q
Tactic: rcases p with ⟨p⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
q : R[X]
inst_1 : Semiring S
f : R →+* S
x : S
hf : ∀ (k : ℕ), Commute ((f : (a : R) → S) (q.coeff k)) x
p : R[ℕ]
⊢ eval₂ f x ({ toFinsupp := p : R[X] } * q) = eval₂ f x { toFinsupp := p : R[X] } * eval₂ f x q
have rcases : ∀ (q : R[ℕ]) (hf : ∀ (k : ℕ), Commute ((f : (a : R) → S) ({ toFinsupp := q : R[X] }.coeff k)) x),
  eval₂ f x ({ toFinsupp := p : R[X] } * { toFinsupp := q : R[X] }) =
    eval₂ f x { toFinsupp := p : R[X] } * eval₂ f x { toFinsupp := q : R[X] }
Tactic: rcases q with ⟨q⟩
Cleared hypotheses: q, hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : S
p q : R[ℕ]
hf : ∀ (k : ℕ), Commute ((f : (a : R) → S) ((q : (a : ℕ) → R) k : R)) x
⊢ eval₂ f x ({ toFinsupp := p : R[X] } * { toFinsupp := q : R[X] }) =
    eval₂ f x { toFinsupp := p : R[X] } * eval₂ f x { toFinsupp := q : R[X] }
have simp : (liftNC (↑f : R →+ S)
        (⇑((powersHom S : (a : S) → Multiplicative ℕ →* S) x : Multiplicative ℕ →* S) : (a : Multiplicative ℕ) → S) :
      (a : R[ℕ]) → S)
    (p * q) =
  HMul.hMul (α := S) (β := S)
    ((liftNC (↑f : R →+ S)
            (⇑((powersHom S : (a : S) → Multiplicative ℕ →* S) x : Multiplicative ℕ →* S) :
              (a : Multiplicative ℕ) → S) :
          (a : R[ℕ]) → S)
        p :
      S)
    ((liftNC (↑f : R →+ S)
            (⇑((powersHom S : (a : S) → Multiplicative ℕ →* S) x : Multiplicative ℕ →* S) :
              (a : Multiplicative ℕ) → S) :
          (a : R[ℕ]) → S)
        q :
      S)
Tactic: simp only [← ofFinsupp_mul, eval₂_ofFinsupp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x p * eval₂ f x X = eval₂ f x p * x
have rw : eval₂ f x p * x = eval₂ f x p * x
Tactic: rw [eval₂_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x (p * X) = eval₂ f x p * x
have refine : ∀ (k : ℕ), Commute ((f : (a : R) → S) (coeff X k)) x
Tactic: refine _root_.trans (eval₂_mul_noncomm _ _ fun k => ?_) (by rw [eval₂_X])
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
x : S
k : ℕ
⊢ Commute ((f : (a : R) → S) (coeff X k)) x
have inl : Commute ((f : (a : R) → S) (coeff X 1)) x
Tactic: rcases em (k = 1) with (rfl | hk)
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
x : S
k : ℕ
inl : Commute ((f : (a : R) → S) (coeff X 1)) x
⊢ Commute ((f : (a : R) → S) (coeff X k)) x
have inr : ∀ (hk : ¬k = 1), Commute ((f : (a : R) → S) (coeff X k)) x
Tactic: rcases em (k = 1) with (rfl | hk)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x (X * p) = eval₂ f x p * x
have rw : eval₂ f x (p * X) = eval₂ f x p * x
Tactic: rw [X_mul, eval₂_mul_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
x : S
rw : eval₂ f x (p * X) = eval₂ f x p * x
⊢ eval₂ f x (X * p) = eval₂ f x p * x
have rw₁ : eval₂ f x p * x = eval₂ f x p * x
Tactic: rw [X_mul, eval₂_mul_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
S : Type v
a : R
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
x : S
h : Commute ((f : (a : R) → S) a) x
⊢ eval₂ f x (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])) =
    HMul.hMul (β := S) (eval₂ f x p) ((f : (a : R) → S) a : S)
have hf : ∀ (k : ℕ), Commute ((f : (a : R) → S) (coeff ((C : (a : R) → R[X]) a) k)) x
Tactic: rw [eval₂_mul_noncomm, eval₂_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
S : Type v
a : R
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
x : S
h : Commute ((f : (a : R) → S) a) x
k : ℕ
⊢ Commute ((f : (a : R) → S) (coeff ((C : (a : R) → R[X]) a) k)) x
have pos : ∀ (hk : k = 0), Commute ((f : (a : R) → S) (coeff ((C : (a : R) → R[X]) a) k)) x
Tactic: by_cases hk : k = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
S : Type v
a : R
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
x : S
h : Commute ((f : (a : R) → S) a) x
k : ℕ
pos : ∀ (hk : k = 0), Commute ((f : (a : R) → S) (coeff ((C : (a : R) → R[X]) a) k)) x
⊢ Commute ((f : (a : R) → S) (coeff ((C : (a : R) → R[X]) a) k)) x
have neg : ∀ (hk : ¬k = 0), Commute ((f : (a : R) → S) (coeff ((C : (a : R) → R[X]) a) k)) x
Tactic: by_cases hk : k = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (hypothesis)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : S
ps : List R[X]
p : R[X]
ihp :
  ∀ (hf : ∀ p ∈ ps, ∀ (k : ℕ), Commute ((f : (a : R) → S) (p.coeff k)) x),
    eval₂ f x ps.prod = (List.map (eval₂ f x) ps).prod
hf : ∀ p_1 ∈ ps ++ [p], ∀ (k : ℕ), Commute ((f : (a : R) → S) (p_1.coeff k)) x
⊢ eval₂ f x (ps ++ [p]).prod = (List.map (eval₂ f x) (ps ++ [p])).prod
have hf₁ : (∀ x_1 ∈ ps, ∀ (k : ℕ), Commute ((f : (a : R) → S) (x_1.coeff k)) x) ∧
  ∀ (k : ℕ), Commute ((f : (a : R) → S) (p.coeff k)) x
Tactic: simp only [List.forall_mem_append, List.forall_mem_singleton] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : S
ps : List R[X]
hf : ∀ p ∈ ps, ∀ (k : ℕ), Commute ((f : (a : R) → S) (p.coeff k)) x
⊢ eval₂ f x ps.prod = (List.map (eval₂ f x) ps).prod
have nil : ∀ (hf : ∀ (p : R[X]), Membership.mem (γ := List R[X]) [] p → ∀ (k : ℕ), Commute ((f : (a : R) → S) (p.coeff k)) x),
  eval₂ f x (List.prod []) = (List.map (eval₂ f x) []).prod
Tactic: induction ps using List.reverseRecOn with
  | nil => simp
  | append_singleton ps p ihp =>
    simp only [List.forall_mem_append, List.forall_mem_singleton] at hf
    simp [eval₂_mul_noncomm _ _ hf.2, ihp hf.1]
Cleared hypotheses: ps, hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : S
ps : List R[X]
hf : ∀ p ∈ ps, ∀ (k : ℕ), Commute ((f : (a : R) → S) (p.coeff k)) x
nil :
  ∀ (hf : ∀ (p : R[X]), Membership.mem (γ := List R[X]) [] p → ∀ (k : ℕ), Commute ((f : (a : R) → S) (p.coeff k)) x),
    eval₂ f x (List.prod []) = (List.map (eval₂ f x) []).prod
⊢ eval₂ f x ps.prod = (List.map (eval₂ f x) ps).prod
have append_singleton : ∀ (ps : List R[X]) (p : R[X])
  (ihp :
    ∀ (hf : ∀ p ∈ ps, ∀ (k : ℕ), Commute ((f : (a : R) → S) (p.coeff k)) x),
      eval₂ f x ps.prod = (List.map (eval₂ f x) ps).prod)
  (hf : ∀ p_1 ∈ ps ++ [p], ∀ (k : ℕ), Commute ((f : (a : R) → S) (p_1.coeff k)) x),
  eval₂ f x (ps ++ [p]).prod = (List.map (eval₂ f x) (ps ++ [p])).prod
Tactic: induction ps using List.reverseRecOn with
  | nil => simp
  | append_singleton ps p ihp =>
    simp only [List.forall_mem_append, List.forall_mem_singleton] at hf
    simp [eval₂_mul_noncomm _ _ hf.2, ihp hf.1]
Cleared hypotheses: ps, hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : CommSemiring S
f : R →+* S
x : S
q : R[X]
hp : eval₂ f x p = 0
⊢ eval₂ f x (p * q) = 0
have rw : eval₂ f x p * eval₂ f x q = 0
Tactic: rw [eval₂_mul f x]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
q : R[X]
inst_1 : CommSemiring S
f : R →+* S
x : S
p : R[X]
hq : eval₂ f x q = 0
⊢ eval₂ f x (p * q) = 0
have rw : eval₂ f x p * eval₂ f x q = 0
Tactic: rw [eval₂_mul f x]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : R
⊢ eval x p = p.sum fun (e : ℕ) (a : R) ↦ a * x ^ e
have rw : Eq (α := R) (p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) a : R) (x ^ e))
  (p.sum fun (e : ℕ) (a : R) ↦ a * x ^ e)
Tactic: rw [eval, eval₂_eq_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
f : R →+* S
r : R
⊢ eval₂ f ((f : (a : R) → S) r) p = (f : (a : R) → S) (eval r p)
have rw : Eq.{u_1 + 1} (α := S)
  (∑ n ∈ p.support,
    HMul.hMul (α := S) ((f : (a : R) → S) (p.coeff n) : S) (HPow.hPow (α := S) ((f : (a : R) → S) r : S) n))
  (∑ x ∈ p.support, (f : (a : R) → S) (p.coeff x * r ^ x))
Tactic: rw [eval₂_eq_sum, eval_eq_sum, sum, sum, map_sum f]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
f : R →+* S
⊢ eval₂ f 1 p = (f : (a : R) → S) (eval 1 p)
have h : Eq.{u_1 + 1} (α := S) (1 : S) ((f : (a : R) → S) 1 : S)
Tactic: convert! eval₂_at_apply (p := p) f 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
f : R →+* S
n : ℕ
⊢ eval₂ f (↑n : S) p = (f : (a : R) → S) (eval (↑n : R) p)
have h : Eq.{u_1 + 1} (α := S) ((↑n : S) : S) ((f : (a : R) → S) (↑n : R) : S)
Tactic: convert! eval₂_at_apply (p := p) f n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
x : R
⊢ eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p) = a * eval x p
have add : ∀ (p q : R[X]) (ph : eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p) = a * eval x p)
  (qh : eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q) = a * eval x q),
  eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (p + q)) = a * eval x (p + q)
Tactic: induction p using Polynomial.induction_on' with
  | add p q ph qh => simp only [mul_add, eval_add, ph, qh]
  | monomial n b => simp only [mul_assoc, C_mul_monomial, eval_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
x : R
add :
  ∀ (p q : R[X]) (ph : eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p) = a * eval x p)
    (qh : eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q) = a * eval x q),
    eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (p + q)) = a * eval x (p + q)
⊢ eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p) = a * eval x p
have monomial : ∀ (n : ℕ) (b : R),
  eval x (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X])) =
    a * eval x ((monomial n : (a : R) → R[X]) b)
Tactic: induction p using Polynomial.induction_on' with
  | add p q ph qh => simp only [mul_add, eval_add, ph, qh]
  | monomial n b => simp only [mul_assoc, C_mul_monomial, eval_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : R
n : ℕ
⊢ eval x ((↑n : R[X]) * p) = (↑n : R) * eval x p
have rw : eval x ((C : (a : R) → R[X]) (↑n : R) * p) = (↑n : R) * eval x p
Tactic: rw [← C_eq_natCast, eval_C_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : R
n : ℕ
rw : eval x ((C : (a : R) → R[X]) (↑n : R) * p) = (↑n : R) * eval x p
⊢ eval x ((↑n : R[X]) * p) = (↑n : R) * eval x p
have rw₁ : (↑n : R) * eval x p = (↑n : R) * eval x p
Tactic: rw [← C_eq_natCast, eval_C_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : R
k : ℕ
⊢ eval x (p * HPow.hPow (α := R[X]) X k) = eval x p * x ^ k
have zero : eval x (p * HPow.hPow (α := R[X]) (β := ℕ) X 0) = eval x p * HPow.hPow (β := ℕ) x 0
Tactic: induction k with
  | zero => simp
  | succ k ih => simp [pow_succ, ← mul_assoc, ih]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : R
k : ℕ
zero : eval x (p * HPow.hPow (α := R[X]) (β := ℕ) X 0) = eval x p * HPow.hPow (β := ℕ) x 0
⊢ eval x (p * HPow.hPow (α := R[X]) X k) = eval x p * x ^ k
have succ : ∀ (k : ℕ) (ih : eval x (p * HPow.hPow (α := R[X]) X k) = eval x p * x ^ k),
  eval x (p * HPow.hPow (α := R[X]) X (k + 1)) = eval x p * x ^ (k + 1)
Tactic: induction k with
  | zero => simp
  | succ k ih => simp [pow_succ, ← mul_assoc, ih]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
x : R
h : Commute a x
⊢ eval x (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])) = eval x p * a
have rw : HMul.hMul (β := R) (eval₂ (RingHom.id R) x p) ((RingHom.id R : (a : R) → R) a : R) = eval x p * a
Tactic: rw [eval, eval₂_mul_C']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
x : R
h : Commute a x
rw : HMul.hMul (β := R) (eval₂ (RingHom.id R) x p) ((RingHom.id R : (a : R) → R) a : R) = eval x p * a
⊢ eval x (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])) = eval x p * a
have h₁ : Commute ((RingHom.id R : (a : R) → R) a) x
Tactic: rw [eval, eval₂_mul_C']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
x : R
h : p.IsRoot x
hpq : p ∣ q
⊢ q.IsRoot x
have rwa : eval x q = 0
Tactic: rwa [IsRoot, eval, eval₂_eq_zero_of_dvd_of_eval₂_eq_zero _ _ hpq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
x : R
h : p.IsRoot x
hpq : p ∣ q
rwa : eval x q = 0
⊢ q.IsRoot x
have rwa₁ : eval₂ (RingHom.id R) x q = 0
Tactic: rwa [IsRoot, eval, eval₂_eq_zero_of_dvd_of_eval₂_eq_zero _ _ hpq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
x : R
h : p.IsRoot x
hpq : p ∣ q
rwa : eval x q = 0
rwa₁ : eval₂ (RingHom.id R) x q = 0
⊢ q.IsRoot x
have rwa₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rwa [IsRoot, eval, eval₂_eq_zero_of_dvd_of_eval₂_eq_zero _ _ hpq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p q : R[X]
x : R
h : p.IsRoot x
hpq : p ∣ q
rwa : eval x q = 0
rwa₁ : eval₂ (RingHom.id R) x q = 0
rwa₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ q.IsRoot x
have rwa₃ : eval₂ (RingHom.id R) x p = 0
Tactic: rwa [IsRoot, eval, eval₂_eq_zero_of_dvd_of_eval₂_eq_zero _ _ hpq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ p.comp q = p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (q ^ e)
have rw : eval₂ C q p = p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (q ^ e)
Tactic: rw [comp, eval₂_eq_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
rw : eval₂ C q p = p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (q ^ e)
⊢ p.comp q = p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (q ^ e)
have rw₁ : Eq (α := R[X]) (p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (q ^ e))
  (p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (q ^ e))
Tactic: rw [comp, eval₂_eq_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.comp X = p
have simp : (p.sum fun (e : ℕ) (a : R) ↦ (monomial e : (a : R) → R[X]) a) = p
Tactic: simp only [comp, eval₂_def, C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ comp (↑n : R[X]) p = (↑n : R[X])
have rw : comp ((C : (a : R) → R[X]) (↑n : R)) p = (C : (a : R) → R[X]) (↑n : R)
Tactic: rw [← C_eq_natCast, C_comp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
rw : comp ((C : (a : R) → R[X]) (↑n : R)) p = (C : (a : R) → R[X]) (↑n : R)
⊢ comp (↑n : R[X]) p = (↑n : R[X])
have rw₁ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (↑n : R)) ((C : (a : R) → R[X]) (↑n : R))
Tactic: rw [← C_eq_natCast, C_comp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.comp 0 = (C : (a : R) → R[X]) (eval 0 p)
have rw : p.comp ((C : (a : R) → R[X]) 0) = (C : (a : R) → R[X]) (eval 0 p)
Tactic: rw [← C_0, comp_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : p.comp ((C : (a : R) → R[X]) 0) = (C : (a : R) → R[X]) (eval 0 p)
⊢ p.comp 0 = (C : (a : R) → R[X]) (eval 0 p)
have rw₁ : Eq (α := R[X]) ((C : (a : R) → R[X]) (eval 0 p) : R[X]) ((C : (a : R) → R[X]) (eval 0 p) : R[X])
Tactic: rw [← C_0, comp_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ comp 0 p = 0
have rw : comp ((C : (a : R) → R[X]) 0) p = (C : (a : R) → R[X]) 0
Tactic: rw [← C_0, C_comp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : comp ((C : (a : R) → R[X]) 0) p = (C : (a : R) → R[X]) 0
⊢ comp 0 p = 0
have rw₁ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 0) ((C : (a : R) → R[X]) 0)
Tactic: rw [← C_0, C_comp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.comp 1 = (C : (a : R) → R[X]) (eval 1 p)
have rw : p.comp ((C : (a : R) → R[X]) 1) = (C : (a : R) → R[X]) (eval 1 p)
Tactic: rw [← C_1, comp_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : p.comp ((C : (a : R) → R[X]) 1) = (C : (a : R) → R[X]) (eval 1 p)
⊢ p.comp 1 = (C : (a : R) → R[X]) (eval 1 p)
have rw₁ : Eq (α := R[X]) ((C : (a : R) → R[X]) (eval 1 p) : R[X]) ((C : (a : R) → R[X]) (eval 1 p) : R[X])
Tactic: rw [← C_1, comp_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ comp 1 p = 1
have rw : comp ((C : (a : R) → R[X]) 1) p = (C : (a : R) → R[X]) 1
Tactic: rw [← C_1, C_comp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : comp ((C : (a : R) → R[X]) 1) p = (C : (a : R) → R[X]) 1
⊢ comp 1 p = 1
have rw₁ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 1) ((C : (a : R) → R[X]) 1)
Tactic: rw [← C_1, C_comp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p r : R[X]
⊢ (p * X).comp r = p.comp r * r
have add : ∀ (p q : R[X]) (hp : (p * X).comp r = p.comp r * r) (hq : (q * X).comp r = q.comp r * r),
  ((p + q) * X).comp r = (p + q).comp r * r
Tactic: induction p using Polynomial.induction_on' with
  | add p q hp hq => simp only [hp, hq, add_mul, add_comp]
  | monomial n b => simp only [pow_succ, mul_assoc, monomial_mul_X, monomial_comp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p r : R[X]
add :
  ∀ (p q : R[X]) (hp : (p * X).comp r = p.comp r * r) (hq : (q * X).comp r = q.comp r * r),
    ((p + q) * X).comp r = (p + q).comp r * r
⊢ (p * X).comp r = p.comp r * r
have monomial : ∀ (n : ℕ) (b : R),
  (HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) b : R[X]) X).comp r =
    comp ((monomial n : (a : R) → R[X]) b) r * r
Tactic: induction p using Polynomial.induction_on' with
  | add p q hp hq => simp only [hp, hq, add_mul, add_comp]
  | monomial n b => simp only [pow_succ, mul_assoc, monomial_mul_X, monomial_comp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
⊢ (HPow.hPow (α := R[X]) X k).comp p = p ^ k
have zero : (HPow.hPow (α := R[X]) (β := ℕ) X 0).comp p = HPow.hPow (β := ℕ) p 0
Tactic: induction k with
  | zero => simp
  | succ k ih => simp [pow_succ, mul_X_comp, ih]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
zero : (HPow.hPow (α := R[X]) (β := ℕ) X 0).comp p = HPow.hPow (β := ℕ) p 0
⊢ (HPow.hPow (α := R[X]) X k).comp p = p ^ k
have succ : ∀ (k : ℕ) (ih : (HPow.hPow (α := R[X]) X k).comp p = p ^ k), (HPow.hPow (α := R[X]) X (k + 1)).comp p = p ^ (k + 1)
Tactic: induction k with
  | zero => simp
  | succ k ih => simp [pow_succ, mul_X_comp, ih]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p r : R[X]
k : ℕ
⊢ (p * HPow.hPow (α := R[X]) X k).comp r = p.comp r * r ^ k
have zero : (p * HPow.hPow (α := R[X]) (β := ℕ) X 0).comp r = p.comp r * HPow.hPow (β := ℕ) r 0
Tactic: induction k with
  | zero => simp
  | succ k ih => simp [ih, pow_succ, ← mul_assoc, mul_X_comp]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p r : R[X]
k : ℕ
zero : (p * HPow.hPow (α := R[X]) (β := ℕ) X 0).comp r = p.comp r * HPow.hPow (β := ℕ) r 0
⊢ (p * HPow.hPow (α := R[X]) X k).comp r = p.comp r * r ^ k
have succ : ∀ (k : ℕ) (ih : (p * HPow.hPow (α := R[X]) X k).comp r = p.comp r * r ^ k),
  (p * HPow.hPow (α := R[X]) X (k + 1)).comp r = p.comp r * r ^ (k + 1)
Tactic: induction k with
  | zero => simp
  | succ k ih => simp [ih, pow_succ, ← mul_assoc, mul_X_comp]
Cleared hypotheses: k