awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p r : R[X]
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).comp r =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (p.comp r)
have add : ∀ (p q : R[X])
  (hp :
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).comp r =
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (p.comp r))
  (hq :
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q).comp r =
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (q.comp r)),
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (p + q)).comp r =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((p + q).comp r)
Tactic: induction p using Polynomial.induction_on' with
  | add p q hp hq => simp [hp, hq, mul_add]
  | monomial n b => simp [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p r : R[X]
add :
  ∀ (p q : R[X])
    (hp :
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).comp r =
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (p.comp r))
    (hq :
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q).comp r =
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (q.comp r)),
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (p + q)).comp r =
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((p + q).comp r)
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).comp r =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (p.comp r)
have monomial : ∀ (n : ℕ) (b : R),
  (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X])).comp r =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (comp ((monomial n : (a : R) → R[X]) b) r)
Tactic: induction p using Polynomial.induction_on' with
  | add p q hp hq => simp [hp, hq, mul_add]
  | monomial n b => simp [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p r : R[X]
n : ℕ
⊢ ((↑n : R[X]) * p).comp r = (↑n : R[X]) * p.comp r
have rw : ((C : (a : R) → R[X]) (↑n : R) * p).comp r = (C : (a : R) → R[X]) (↑n : R) * p.comp r
Tactic: rw [← C_eq_natCast, C_mul_comp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p r : R[X]
n : ℕ
rw : ((C : (a : R) → R[X]) (↑n : R) * p).comp r = (C : (a : R) → R[X]) (↑n : R) * p.comp r
⊢ ((↑n : R[X]) * p).comp r = (↑n : R[X]) * p.comp r
have rw₁ : (C : (a : R) → R[X]) (↑n : R) * p.comp r = (C : (a : R) → R[X]) (↑n : R) * p.comp r
Tactic: rw [← C_eq_natCast, C_mul_comp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
⊢ (p * HAdd.hAdd (α := R[X]) X (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
have rw : (p * X + p * (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
Tactic: rw [mul_add, add_comp, mul_X_comp, ← Nat.cast_comm, natCast_mul_comp, Nat.cast_comm, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
rw : (p * X + p * (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
⊢ (p * HAdd.hAdd (α := R[X]) X (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
have rw₁ : (p * X).comp q + (p * (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
Tactic: rw [mul_add, add_comp, mul_X_comp, ← Nat.cast_comm, natCast_mul_comp, Nat.cast_comm, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
rw : (p * X + p * (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
rw₁ : (p * X).comp q + (p * (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
⊢ (p * HAdd.hAdd (α := R[X]) X (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
have rw₂ : p.comp q * q + (p * (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
Tactic: rw [mul_add, add_comp, mul_X_comp, ← Nat.cast_comm, natCast_mul_comp, Nat.cast_comm, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
rw : (p * X + p * (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
rw₁ : (p * X).comp q + (p * (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
rw₂ : p.comp q * q + (p * (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
⊢ (p * HAdd.hAdd (α := R[X]) X (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
have rw₃ : p.comp q * q + ((↑n : R[X]) * p).comp q = p.comp q * (q + (↑n : R[X]))
Tactic: rw [mul_add, add_comp, mul_X_comp, ← Nat.cast_comm, natCast_mul_comp, Nat.cast_comm, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
rw : (p * X + p * (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
rw₁ : (p * X).comp q + (p * (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
rw₂ : p.comp q * q + (p * (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
rw₃ : p.comp q * q + ((↑n : R[X]) * p).comp q = p.comp q * (q + (↑n : R[X]))
⊢ (p * HAdd.hAdd (α := R[X]) X (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
have rw₄ : p.comp q * q + (↑n : R[X]) * p.comp q = p.comp q * (q + (↑n : R[X]))
Tactic: rw [mul_add, add_comp, mul_X_comp, ← Nat.cast_comm, natCast_mul_comp, Nat.cast_comm, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
rw : (p * X + p * (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
rw₁ : (p * X).comp q + (p * (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
rw₂ : p.comp q * q + (p * (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
rw₃ : p.comp q * q + ((↑n : R[X]) * p).comp q = p.comp q * (q + (↑n : R[X]))
rw₄ : p.comp q * q + (↑n : R[X]) * p.comp q = p.comp q * (q + (↑n : R[X]))
⊢ (p * HAdd.hAdd (α := R[X]) X (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
have rw₅ : p.comp q * q + p.comp q * (↑n : R[X]) = p.comp q * (q + (↑n : R[X]))
Tactic: rw [mul_add, add_comp, mul_X_comp, ← Nat.cast_comm, natCast_mul_comp, Nat.cast_comm, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
rw : (p * X + p * (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
rw₁ : (p * X).comp q + (p * (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
rw₂ : p.comp q * q + (p * (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
rw₃ : p.comp q * q + ((↑n : R[X]) * p).comp q = p.comp q * (q + (↑n : R[X]))
rw₄ : p.comp q * q + (↑n : R[X]) * p.comp q = p.comp q * (q + (↑n : R[X]))
rw₅ : p.comp q * q + p.comp q * (↑n : R[X]) = p.comp q * (q + (↑n : R[X]))
⊢ (p * HAdd.hAdd (α := R[X]) X (↑n : R[X])).comp q = p.comp q * (q + (↑n : R[X]))
have rw₆ : p.comp q * q + p.comp q * (↑n : R[X]) = p.comp q * q + p.comp q * (↑n : R[X])
Tactic: rw [mul_add, add_comp, mul_X_comp, ← Nat.cast_comm, natCast_mul_comp, Nat.cast_comm, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
φ ψ χ : R[X]
⊢ (φ.comp ψ).comp χ = φ.comp (ψ.comp χ)
have refine_1 : ∀ (a : R), (comp ((C : (a : R) → R[X]) a) ψ).comp χ = comp ((C : (a : R) → R[X]) a) (ψ.comp χ)
Tactic: refine Polynomial.induction_on φ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
φ ψ χ : R[X]
refine_1 : ∀ (a : R), (comp ((C : (a : R) → R[X]) a) ψ).comp χ = comp ((C : (a : R) → R[X]) a) (ψ.comp χ)
⊢ (φ.comp ψ).comp χ = φ.comp (ψ.comp χ)
have refine_2 : ∀ (p q : R[X]),
  (p.comp ψ).comp χ = p.comp (ψ.comp χ) →
    (q.comp ψ).comp χ = q.comp (ψ.comp χ) → ((p + q).comp ψ).comp χ = (p + q).comp (ψ.comp χ)
Tactic: refine Polynomial.induction_on φ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
φ ψ χ : R[X]
refine_1 : ∀ (a : R), (comp ((C : (a : R) → R[X]) a) ψ).comp χ = comp ((C : (a : R) → R[X]) a) (ψ.comp χ)
refine_2 :
  ∀ (p q : R[X]),
    (p.comp ψ).comp χ = p.comp (ψ.comp χ) →
      (q.comp ψ).comp χ = q.comp (ψ.comp χ) → ((p + q).comp ψ).comp χ = (p + q).comp (ψ.comp χ)
⊢ (φ.comp ψ).comp χ = φ.comp (ψ.comp χ)
have refine_3 : ∀ (n : ℕ) (a : R),
  ((HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).comp ψ).comp χ =
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).comp (ψ.comp χ) →
    ((HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).comp ψ).comp χ =
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).comp (ψ.comp χ)
Tactic: refine Polynomial.induction_on φ ?_ ?_ ?_
-- 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
n : ℕ
a : R
⊢ eval₂ (RingHom.comp C f) X ((monomial n : (a : R) → R[X]) a) = (monomial n : (a : S) → S[X]) ((f : (a : R) → S) a)
have rw : HMul.hMul (α := S[X]) ((RingHom.comp C f : (a : R) → S[X]) a : S[X]) (HPow.hPow (α := S[X]) X n) =
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) a) : S[X]) (HPow.hPow (α := S[X]) X n)
Tactic: rw [eval₂_monomial, ← C_mul_X_pow_eq_monomial]
-- 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
⊢ map f (p * q) = map f p * map f q
have hf : ∀ (k : ℕ), Commute.{v} (S := S[X]) ((RingHom.comp C f : (a : R) → S[X]) (q.coeff k) : S[X]) (X : S[X])
Tactic: rw [map, eval₂_mul_noncomm]
-- 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
n : ℕ
inst_2 : n.AtLeastTwo
⊢ map f (↑n : R[X]) = (↑n : S[X])
have rw : Eq.{v + 1} (α := S[X]) (↑n : S[X]) (↑n : S[X])
Tactic: rw [Polynomial.map_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
⊢ (mapRingHom f).comp C = RingHom.comp C f
have a : ∀ (x : R) (n : ℕ),
  Eq.{u_2 + 1} (α := S) (coeff (((mapRingHom f).comp C : (a : R) → S[X]) x) n)
    (coeff ((RingHom.comp C f : (a : R) → S[X]) x) n)
Tactic: ext
-- 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 x (map f p)
have add : ∀ (p q : R[X]) (hp : eval₂ f x p = eval x (map f p)) (hq : eval₂ f x q = eval x (map f q)),
  eval₂ f x (p + q) = eval x (map f (p + q))
Tactic: induction p using Polynomial.induction_on' with
  | add p q hp hq => simp [hp, hq]
  | monomial n r => simp
-- 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
add :
  ∀ (p q : R[X]) (hp : eval₂ f x p = eval x (map f p)) (hq : eval₂ f x q = eval x (map f q)),
    eval₂ f x (p + q) = eval x (map f (p + q))
⊢ eval₂ f x p = eval x (map f p)
have monomial : ∀ (n : ℕ) (r : R), eval₂ f x ((monomial n : (a : R) → R[X]) r) = eval x (map f ((monomial n : (a : R) → R[X]) r))
Tactic: induction p using Polynomial.induction_on' with
  | add p q hp hq => simp [hp, hq]
  | monomial n r => simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
x : R
⊢ eval x (p.comp q) = eval (eval x q) p
have add : ∀ (r s : R[X]) (hr : eval x (r.comp q) = eval (eval x q) r) (hs : eval x (s.comp q) = eval (eval x q) s),
  eval x ((r + s).comp q) = eval (eval x q) (r + s)
Tactic: induction p using Polynomial.induction_on' with
  | add r s hr hs => simp [add_comp, hr, hs]
  | monomial n a => simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
x : R
add :
  ∀ (r s : R[X]) (hr : eval x (r.comp q) = eval (eval x q) r) (hs : eval x (s.comp q) = eval (eval x q) s),
    eval x ((r + s).comp q) = eval (eval x q) (r + s)
⊢ eval x (p.comp q) = eval (eval x q) p
have monomial : ∀ (n : ℕ) (a : R), eval x (comp ((monomial n : (a : R) → R[X]) a) q) = eval (eval x q) ((monomial n : (a : R) → R[X]) a)
Tactic: induction p using Polynomial.induction_on' with
  | add r s hr hs => simp [add_comp, hr, hs]
  | monomial n a => simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
a : R
inst : CommSemiring R
p q : R[X]
H : q.IsRoot a
⊢ (p * q).IsRoot a
have rw : eval a (p * q) = 0
Tactic: rw [IsRoot, eval_mul, IsRoot.def.1 H, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
a : R
inst : CommSemiring R
p q : R[X]
H : q.IsRoot a
rw : eval a (p * q) = 0
⊢ (p * q).IsRoot a
have rw₁ : eval a p * eval a q = 0
Tactic: rw [IsRoot, eval_mul, IsRoot.def.1 H, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
a : R
inst : CommSemiring R
p q : R[X]
H : q.IsRoot a
rw : eval a (p * q) = 0
rw₁ : eval a p * eval a q = 0
⊢ (p * q).IsRoot a
have rw₂ : eval a p * 0 = 0
Tactic: rw [IsRoot, eval_mul, IsRoot.def.1 H, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
a : R
inst : CommSemiring R
p q : R[X]
H : q.IsRoot a
rw : eval a (p * q) = 0
rw₁ : eval a p * eval a q = 0
rw₂ : eval a p * 0 = 0
⊢ (p * q).IsRoot a
have rw₃ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [IsRoot, eval_mul, IsRoot.def.1 H, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
a : R
inst : CommSemiring R
p q : R[X]
H : p.IsRoot a
⊢ (p * q).IsRoot a
have rw : eval a (p * q) = 0
Tactic: rw [IsRoot, eval_mul, IsRoot.def.1 H, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
a : R
inst : CommSemiring R
p q : R[X]
H : p.IsRoot a
rw : eval a (p * q) = 0
⊢ (p * q).IsRoot a
have rw₁ : eval a p * eval a q = 0
Tactic: rw [IsRoot, eval_mul, IsRoot.def.1 H, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
a : R
inst : CommSemiring R
p q : R[X]
H : p.IsRoot a
rw : eval a (p * q) = 0
rw₁ : eval a p * eval a q = 0
⊢ (p * q).IsRoot a
have rw₂ : 0 * eval a q = 0
Tactic: rw [IsRoot, eval_mul, IsRoot.def.1 H, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
a : R
inst : CommSemiring R
p q : R[X]
H : p.IsRoot a
rw : eval a (p * q) = 0
rw₁ : eval a p * eval a q = 0
rw₂ : 0 * eval a q = 0
⊢ (p * q).IsRoot a
have rw₃ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [IsRoot, eval_mul, IsRoot.def.1 H, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
a : R
inst : CommSemiring R
p q : R[X]
inst_1 : NoZeroDivisors R
⊢ (p * q).IsRoot a ↔ p.IsRoot a ∨ q.IsRoot a
have simp_rw : eval a (p * q) = 0 ↔ eval a p = 0 ∨ eval a q = 0
Tactic: simp_rw [IsRoot, eval_mul, mul_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
a : R
inst : CommSemiring R
p q : R[X]
inst_1 : NoZeroDivisors R
simp_rw : eval a (p * q) = 0 ↔ eval a p = 0 ∨ eval a q = 0
⊢ (p * q).IsRoot a ↔ p.IsRoot a ∨ q.IsRoot a
have simp_rw₁ : eval a p * eval a q = 0 ↔ eval a p = 0 ∨ eval a q = 0
Tactic: simp_rw [IsRoot, eval_mul, mul_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
S : Type u_1
inst_1 : Ring S
f : R →+* S
x : S
⊢ eval₂ f x (-p) = -eval₂ f x p
have rw : eval₂ f x (-p) + eval₂ f x p = 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← eval₂_add, neg_add_cancel, eval₂_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
S : Type u_1
inst_1 : Ring S
f : R →+* S
x : S
rw : eval₂ f x (-p) + eval₂ f x p = 0
⊢ eval₂ f x (-p) = -eval₂ f x p
have rw₁ : eval₂ f x (-p + p) = 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← eval₂_add, neg_add_cancel, eval₂_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
S : Type u_1
inst_1 : Ring S
f : R →+* S
x : S
rw : eval₂ f x (-p) + eval₂ f x p = 0
rw₁ : eval₂ f x (-p + p) = 0
⊢ eval₂ f x (-p) = -eval₂ f x p
have rw₂ : eval₂ f x 0 = 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← eval₂_add, neg_add_cancel, eval₂_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
S : Type u_1
inst_1 : Ring S
f : R →+* S
x : S
rw : eval₂ f x (-p) + eval₂ f x p = 0
rw₁ : eval₂ f x (-p + p) = 0
rw₂ : eval₂ f x 0 = 0
⊢ eval₂ f x (-p) = -eval₂ f x p
have rw₃ : Eq.{u_1 + 1} (α := S) 0 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← eval₂_add, neg_add_cancel, eval₂_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
S : Type u_1
inst_1 : Ring S
f : R →+* S
x : S
⊢ eval₂ f x (p - q) = eval₂ f x p - eval₂ f x q
have rw : eval₂ f x (p + -q) = eval₂ f x p - eval₂ f x q
Tactic: rw [sub_eq_add_neg, eval₂_add, eval₂_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
S : Type u_1
inst_1 : Ring S
f : R →+* S
x : S
rw : eval₂ f x (p + -q) = eval₂ f x p - eval₂ f x q
⊢ eval₂ f x (p - q) = eval₂ f x p - eval₂ f x q
have rw₁ : eval₂ f x p + eval₂ f x (-q) = eval₂ f x p - eval₂ f x q
Tactic: rw [sub_eq_add_neg, eval₂_add, eval₂_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
S : Type u_1
inst_1 : Ring S
f : R →+* S
x : S
rw : eval₂ f x (p + -q) = eval₂ f x p - eval₂ f x q
rw₁ : eval₂ f x p + eval₂ f x (-q) = eval₂ f x p - eval₂ f x q
⊢ eval₂ f x (p - q) = eval₂ f x p - eval₂ f x q
have rw₂ : eval₂ f x p + -eval₂ f x q = eval₂ f x p - eval₂ f x q
Tactic: rw [sub_eq_add_neg, eval₂_add, eval₂_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
S : Type u_1
inst_1 : Ring S
f : R →+* S
x : S
rw : eval₂ f x (p + -q) = eval₂ f x p - eval₂ f x q
rw₁ : eval₂ f x p + eval₂ f x (-q) = eval₂ f x p - eval₂ f x q
rw₂ : eval₂ f x p + -eval₂ f x q = eval₂ f x p - eval₂ f x q
⊢ eval₂ f x (p - q) = eval₂ f x p - eval₂ f x q
have rw₃ : eval₂ f x p + -eval₂ f x q = eval₂ f x p + -eval₂ f x q
Tactic: rw [sub_eq_add_neg, eval₂_add, eval₂_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
a b : R
inst : Ring R
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).IsRoot b ↔ a = b
have rw : eval b (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = 0 ↔ a = b
Tactic: rw [IsRoot.def, eval_sub, eval_X, eval_C, sub_eq_zero, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
a b : R
inst : Ring R
rw : eval b (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = 0 ↔ a = b
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).IsRoot b ↔ a = b
have rw₁ : eval b X - eval b ((C : (a : R) → R[X]) a) = 0 ↔ a = b
Tactic: rw [IsRoot.def, eval_sub, eval_X, eval_C, sub_eq_zero, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
a b : R
inst : Ring R
rw : eval b (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = 0 ↔ a = b
rw₁ : eval b X - eval b ((C : (a : R) → R[X]) a) = 0 ↔ a = b
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).IsRoot b ↔ a = b
have rw₂ : b - eval b ((C : (a : R) → R[X]) a) = 0 ↔ a = b
Tactic: rw [IsRoot.def, eval_sub, eval_X, eval_C, sub_eq_zero, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
a b : R
inst : Ring R
rw : eval b (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = 0 ↔ a = b
rw₁ : eval b X - eval b ((C : (a : R) → R[X]) a) = 0 ↔ a = b
rw₂ : b - eval b ((C : (a : R) → R[X]) a) = 0 ↔ a = b
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).IsRoot b ↔ a = b
have rw₃ : b - a = 0 ↔ a = b
Tactic: rw [IsRoot.def, eval_sub, eval_X, eval_C, sub_eq_zero, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
a b : R
inst : Ring R
rw : eval b (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = 0 ↔ a = b
rw₁ : eval b X - eval b ((C : (a : R) → R[X]) a) = 0 ↔ a = b
rw₂ : b - eval b ((C : (a : R) → R[X]) a) = 0 ↔ a = b
rw₃ : b - a = 0 ↔ a = b
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).IsRoot b ↔ a = b
have rw₄ : b = a ↔ a = b
Tactic: rw [IsRoot.def, eval_sub, eval_X, eval_C, sub_eq_zero, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
a b : R
inst : Ring R
rw : eval b (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = 0 ↔ a = b
rw₁ : eval b X - eval b ((C : (a : R) → R[X]) a) = 0 ↔ a = b
rw₂ : b - eval b ((C : (a : R) → R[X]) a) = 0 ↔ a = b
rw₃ : b - a = 0 ↔ a = b
rw₄ : b = a ↔ a = b
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).IsRoot b ↔ a = b
have rw₅ : a = b ↔ a = b
Tactic: rw [IsRoot.def, eval_sub, eval_X, eval_C, sub_eq_zero, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
i : ℤ
⊢ comp (↑i : R[X]) p = (↑i : R[X])
have ofNat : ∀ (a : ℕ), comp (↑(Int.ofNat a) : R[X]) p = (↑(Int.ofNat a) : R[X])
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
i : ℤ
ofNat : ∀ (a : ℕ), comp (↑(Int.ofNat a) : R[X]) p = (↑(Int.ofNat a) : R[X])
⊢ comp (↑i : R[X]) p = (↑i : R[X])
have negSucc : ∀ (a : ℕ), comp (↑(Int.negSucc a) : R[X]) p = (↑(Int.negSucc a) : R[X])
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
S : Type u_1
inst_1 : Ring 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
inst : Ring R
p q : R[X]
n : ℕ
⊢ (p * HSub.hSub (α := R[X]) X (↑n : R[X])).comp q = p.comp q * (q - (↑n : R[X]))
have rw : (p * X - p * (↑n : R[X])).comp q = p.comp q * (q - (↑n : R[X]))
Tactic: rw [mul_sub, sub_comp, mul_X_comp, ← Nat.cast_comm, natCast_mul_comp, Nat.cast_comm, mul_sub]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
n : ℕ
rw : (p * X - p * (↑n : R[X])).comp q = p.comp q * (q - (↑n : R[X]))
⊢ (p * HSub.hSub (α := R[X]) X (↑n : R[X])).comp q = p.comp q * (q - (↑n : R[X]))
have rw₁ : (p * X).comp q - (p * (↑n : R[X])).comp q = p.comp q * (q - (↑n : R[X]))
Tactic: rw [mul_sub, sub_comp, mul_X_comp, ← Nat.cast_comm, natCast_mul_comp, Nat.cast_comm, mul_sub]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
n : ℕ
rw : (p * X - p * (↑n : R[X])).comp q = p.comp q * (q - (↑n : R[X]))
rw₁ : (p * X).comp q - (p * (↑n : R[X])).comp q = p.comp q * (q - (↑n : R[X]))
⊢ (p * HSub.hSub (α := R[X]) X (↑n : R[X])).comp q = p.comp q * (q - (↑n : R[X]))
have rw₂ : p.comp q * q - (p * (↑n : R[X])).comp q = p.comp q * (q - (↑n : R[X]))
Tactic: rw [mul_sub, sub_comp, mul_X_comp, ← Nat.cast_comm, natCast_mul_comp, Nat.cast_comm, mul_sub]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
n : ℕ
rw : (p * X - p * (↑n : R[X])).comp q = p.comp q * (q - (↑n : R[X]))
rw₁ : (p * X).comp q - (p * (↑n : R[X])).comp q = p.comp q * (q - (↑n : R[X]))
rw₂ : p.comp q * q - (p * (↑n : R[X])).comp q = p.comp q * (q - (↑n : R[X]))
⊢ (p * HSub.hSub (α := R[X]) X (↑n : R[X])).comp q = p.comp q * (q - (↑n : R[X]))
have rw₃ : p.comp q * q - ((↑n : R[X]) * p).comp q = p.comp q * (q - (↑n : R[X]))
Tactic: rw [mul_sub, sub_comp, mul_X_comp, ← Nat.cast_comm, natCast_mul_comp, Nat.cast_comm, mul_sub]