awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
⊢ (map f p).degree ≤ p.degree
have refine : ∀ (m : ℕ) (hm : p.degree < (↑m : WithBot ℕ)), (map f p).coeff m = 0
Tactic: refine (degree_le_iff_coeff_zero _ _).2 fun m hm => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (hypothesis)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
m : ℕ
hm : p.degree < (↑m : WithBot ℕ)
⊢ (map f p).coeff m = 0
have hm₁ : ∀ (m_1 : ℕ), m ≤ m_1 → p.coeff m_1 = 0
Tactic: rw [degree_lt_iff_coeff_zero] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp₀ : p ≠ 0
⊢ (map f p).degree < p.degree
have refine : ∀ (hpq : (map f p).degree = p.degree), p = 0
Tactic: refine degree_map_le.lt_of_ne fun hpq ↦ hp₀ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (hypothesis)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ p = 0
have hp₁ : map f p = 0
Tactic: rw [leadingCoeff, ← coeff_map, ← natDegree_eq_natDegree hpq, ← leadingCoeff, leadingCoeff_eq_zero]
    at hp
Cleared hypotheses: hp, hp₀, hpq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : map f p = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ p = 0
have rw : p.degree = ⊥
Tactic: rw [← degree_eq_bot, ← hpq, hp, degree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : map f p = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
rw : p.degree = ⊥
⊢ p = 0
have rw₁ : (map f p).degree = ⊥
Tactic: rw [← degree_eq_bot, ← hpq, hp, degree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : map f p = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
rw : p.degree = ⊥
rw₁ : (map f p).degree = ⊥
⊢ p = 0
have rw₂ : degree.{v} (R := S) 0 = ⊥
Tactic: rw [← degree_eq_bot, ← hpq, hp, degree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : map f p = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
rw : p.degree = ⊥
rw₁ : (map f p).degree = ⊥
rw₂ : degree.{v} (R := S) 0 = ⊥
⊢ p = 0
have rw₃ : Eq (α := WithBot ℕ) ⊥ ⊥
Tactic: rw [← degree_eq_bot, ← hpq, hp, degree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp₀ : 0 < p.natDegree
⊢ (map f p).natDegree < p.natDegree
have pos : ∀ (H : map f p = 0), (map f p).natDegree < p.natDegree
Tactic: by_cases H : map f p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp₀ : 0 < p.natDegree
pos : ∀ (H : map f p = 0), (map f p).natDegree < p.natDegree
⊢ (map f p).natDegree < p.natDegree
have neg : ∀ (H : ¬map f p = 0), (map f p).natDegree < p.natDegree
Tactic: by_cases H : map f p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
hp : Eq.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp₀ : 0 < p.natDegree
H : map f p = 0
⊢ (map f p).natDegree < p.natDegree
have pos : natDegree.{v} (R := S) 0 < p.natDegree
Tactic: rwa [H, natDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
⊢ (map f p).degree = p.degree
have refine : p.degree ≤ (map f p).degree
Tactic: refine degree_map_le.antisymm ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (hypothesis)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
⊢ p.degree ≤ (map f p).degree
have hp0 : p ≠ 0
Tactic: have hp0 : p ≠ 0 :=
    leadingCoeff_ne_zero.mp fun hp0 => hf (_root_.trans (congr_arg _ hp0) f.map_zero)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp0 : p ≠ 0
⊢ p.degree ≤ (map f p).degree
have rw : (↑p.natDegree : WithBot ℕ) ≤ (map f p).degree
Tactic: rw [degree_eq_natDegree hp0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp0 : p ≠ 0
⊢ (↑p.natDegree : WithBot ℕ) ≤ (map f p).degree
have refine : (map f p).coeff p.natDegree ≠ 0
Tactic: refine le_degree_of_ne_zero ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
hp0 : p ≠ 0
⊢ (map f p).coeff p.natDegree ≠ 0
have rw : Ne.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff p.natDegree) : S) (0 : S)
Tactic: rw [coeff_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
⊢ (map f p).leadingCoeff = (f : (a : R) → S) p.leadingCoeff
have unfold : (map f p).coeff (map f p).natDegree = (f : (a : R) → S) (p.coeff p.natDegree)
Tactic: unfold leadingCoeff
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
⊢ (map f p).coeff (map f p).natDegree = (f : (a : R) → S) (p.coeff p.natDegree)
have rw : Eq.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff (map f p).natDegree) : S) ((f : (a : R) → S) (p.coeff p.natDegree) : S)
Tactic: rw [coeff_map, natDegree_map_of_leadingCoeff_ne_zero f hf]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Ne.{v + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
rw :
  Eq.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff (map f p).natDegree) : S)
    ((f : (a : R) → S) (p.coeff p.natDegree) : S)
⊢ (map f p).coeff (map f p).natDegree = (f : (a : R) → S) (p.coeff p.natDegree)
have rw₁ : Eq.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff p.natDegree) : S) ((f : (a : R) → S) (p.coeff p.natDegree) : S)
Tactic: rw [coeff_map, natDegree_map_of_leadingCoeff_ne_zero f hf]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
p q : R[X]
inst_1 : CommSemiring S
f : R →+* S
x : S
⊢ eval₂ f x (p.comp q) = eval₂ f (eval₂ f x q) p
have rw : eval₂ f x (eval₂ C q (∑ i ∈ range (p.natDegree + 1), (monomial i : (a : R) → R[X]) (p.coeff i))) =
  eval₂ f (eval₂ f x q) (∑ i ∈ range (p.natDegree + 1), (monomial i : (a : R) → R[X]) (p.coeff i))
Tactic: rw [comp, p.as_sum_range]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
p q : R[X]
inst_1 : CommSemiring S
f : R →+* S
t : S
k : ℕ
IH : eval₂ f t (p.comp^[k] q) = (fun (x : S) ↦ eval₂ f x p)^[k] (eval₂ f t q)
⊢ eval₂ f t (p.comp^[k + 1] q) = (fun (x : S) ↦ eval₂ f x p)^[k + 1] (eval₂ f t q)
have succ : eval₂ f t (p.comp (p.comp^[k] q)) = (fun (x : S) ↦ eval₂ f x p)^[k + 1] (eval₂ f t q)
Tactic: rw [Function.iterate_succ_apply', Function.iterate_succ_apply', eval₂_comp, IH]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
p q : R[X]
inst_1 : CommSemiring S
f : R →+* S
t : S
k : ℕ
IH : eval₂ f t (p.comp^[k] q) = (fun (x : S) ↦ eval₂ f x p)^[k] (eval₂ f t q)
succ : eval₂ f t (p.comp (p.comp^[k] q)) = (fun (x : S) ↦ eval₂ f x p)^[k + 1] (eval₂ f t q)
⊢ eval₂ f t (p.comp^[k + 1] q) = (fun (x : S) ↦ eval₂ f x p)^[k + 1] (eval₂ f t q)
have succ₁ : eval₂ f t (p.comp (p.comp^[k] q)) = eval₂ f ((fun (x : S) ↦ eval₂ f x p)^[k] (eval₂ f t q)) p
Tactic: rw [Function.iterate_succ_apply', Function.iterate_succ_apply', eval₂_comp, IH]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
p q : R[X]
inst_1 : CommSemiring S
f : R →+* S
t : S
k : ℕ
IH : eval₂ f t (p.comp^[k] q) = (fun (x : S) ↦ eval₂ f x p)^[k] (eval₂ f t q)
succ : eval₂ f t (p.comp (p.comp^[k] q)) = (fun (x : S) ↦ eval₂ f x p)^[k + 1] (eval₂ f t q)
succ₁ : eval₂ f t (p.comp (p.comp^[k] q)) = eval₂ f ((fun (x : S) ↦ eval₂ f x p)^[k] (eval₂ f t q)) p
⊢ eval₂ f t (p.comp^[k + 1] q) = (fun (x : S) ↦ eval₂ f x p)^[k + 1] (eval₂ f t q)
have succ₂ : eval₂ f (eval₂ f t (p.comp^[k] q)) p = eval₂ f ((fun (x : S) ↦ eval₂ f x p)^[k] (eval₂ f t q)) p
Tactic: rw [Function.iterate_succ_apply', Function.iterate_succ_apply', eval₂_comp, IH]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
p q : R[X]
inst_1 : CommSemiring S
f : R →+* S
t : S
k : ℕ
IH : eval₂ f t (p.comp^[k] q) = (fun (x : S) ↦ eval₂ f x p)^[k] (eval₂ f t q)
succ : eval₂ f t (p.comp (p.comp^[k] q)) = (fun (x : S) ↦ eval₂ f x p)^[k + 1] (eval₂ f t q)
succ₁ : eval₂ f t (p.comp (p.comp^[k] q)) = eval₂ f ((fun (x : S) ↦ eval₂ f x p)^[k] (eval₂ f t q)) p
succ₂ : eval₂ f (eval₂ f t (p.comp^[k] q)) p = eval₂ f ((fun (x : S) ↦ eval₂ f x p)^[k] (eval₂ f t q)) p
⊢ eval₂ f t (p.comp^[k + 1] q) = (fun (x : S) ↦ eval₂ f x p)^[k + 1] (eval₂ f t q)
have succ₃ : eval₂ f ((fun (x : S) ↦ eval₂ f x p)^[k] (eval₂ f t q)) p = eval₂ f ((fun (x : S) ↦ eval₂ f x p)^[k] (eval₂ f t q)) p
Tactic: rw [Function.iterate_succ_apply', Function.iterate_succ_apply', eval₂_comp, IH]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
p q : R[X]
inst_1 : CommSemiring S
f : R →+* S
k : ℕ
t : S
⊢ eval₂ f t (p.comp^[k] q) = (fun (x : S) ↦ eval₂ f x p)^[k] (eval₂ f t q)
have zero : eval₂ f t (p.comp^[0] q) = (fun (x : S) ↦ eval₂ f x p)^[0] (eval₂ f t q)
Tactic: induction k with
  | zero => simp
  | succ k IH => rw [Function.iterate_succ_apply', Function.iterate_succ_apply', eval₂_comp, IH]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
p q : R[X]
inst_1 : CommSemiring S
f : R →+* S
k : ℕ
t : S
zero : eval₂ f t (p.comp^[0] q) = (fun (x : S) ↦ eval₂ f x p)^[0] (eval₂ f t q)
⊢ eval₂ f t (p.comp^[k] q) = (fun (x : S) ↦ eval₂ f x p)^[k] (eval₂ f t q)
have succ : ∀ (k : ℕ) (IH : eval₂ f t (p.comp^[k] q) = (fun (x : S) ↦ eval₂ f x p)^[k] (eval₂ f t q)),
  eval₂ f t (p.comp^[k + 1] q) = (fun (x : S) ↦ eval₂ f x p)^[k + 1] (eval₂ f t q)
Tactic: induction k with
  | zero => simp
  | succ k IH => rw [Function.iterate_succ_apply', Function.iterate_succ_apply', eval₂_comp, IH]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (hypothesis)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
⊢ IsUnit f
have dz : (map φ f).degree = 0
Tactic: have dz := degree_eq_zero_of_isUnit H
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : (map φ f).degree = 0
⊢ IsUnit f
have rw : ∀ (dz : f.degree = 0), IsUnit f
Tactic: rw [degree_map_eq_of_leadingCoeff_ne_zero] at dz
Cleared hypotheses: dz
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : (map φ f).degree = 0
rw : ∀ (dz : f.degree = 0), IsUnit f
⊢ IsUnit f
have hf₁ : Ne.{v + 1} (α := S) ((φ : (a : R) → S) f.leadingCoeff : S) (0 : S)
Tactic: rw [degree_map_eq_of_leadingCoeff_ne_zero] at dz
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : f.degree = 0
⊢ IsUnit f
have rw : IsUnit (M := R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])
Tactic: rw [eq_C_of_degree_eq_zero dz]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : f.degree = 0
⊢ IsUnit (M := R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])
have refine : IsUnit (f.coeff 0)
Tactic: refine IsUnit.map C ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : f.degree = 0
⊢ IsUnit (f.coeff 0)
have h : f.coeff 0 = f.leadingCoeff
Tactic: convert! hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : f.degree = 0
⊢ f.coeff 0 = f.coeff f.natDegree
have h : f.coeff 0 = f.coeff Zero.zero
Tactic: rw [(degree_eq_iff_natDegree_eq _).1 dz]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : f.degree = 0
h : f.coeff 0 = f.coeff Zero.zero
⊢ f.coeff 0 = f.coeff f.natDegree
have rw : f ≠ 0
Tactic: rw [(degree_eq_iff_natDegree_eq _).1 dz]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (hypothesis)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : (map φ f).degree = 0
h : Eq.{v + 1} (α := S) ((φ : (a : R) → S) f.leadingCoeff : S) (0 : S)
⊢ False
have u : IsUnit.{v} (M := S) ((φ : (a : R) → S) f.leadingCoeff : S)
Tactic: have u : IsUnit (φ f.leadingCoeff) := IsUnit.map φ hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (hypothesis)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : CommRing S
inst_2 : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : (map φ f).degree = 0
h : Eq.{v + 1} (α := S) ((φ : (a : R) → S) f.leadingCoeff : S) (0 : S)
u : IsUnit.{v} (M := S) ((φ : (a : R) → S) f.leadingCoeff : S)
⊢ False
have u₁ : IsUnit.{v} (M := S) 0
Tactic: rw [h] at u
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.SMul (hypothesis)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
⊢ eval₂ g x (s • p) = HMul.hMul (α := S) ((g : (a : R) → S) s : S) (eval₂ g x p)
have A : p.natDegree < p.natDegree.succ
Tactic: have A : p.natDegree < p.natDegree.succ := Nat.lt_succ_self _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.SMul (hypothesis)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
⊢ eval₂ g x (s • p) = HMul.hMul (α := S) ((g : (a : R) → S) s : S) (eval₂ g x p)
have B : (s • p).natDegree < p.natDegree.succ
Tactic: have B : (s • p).natDegree < p.natDegree.succ := (natDegree_smul_le _ _).trans_lt A
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.SMul (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ eval₂ g x (s • p) = HMul.hMul (α := S) ((g : (a : R) → S) s : S) (eval₂ g x p)
have rw : ∑ a ∈ range p.natDegree.succ, HMul.hMul (α := S) ((g : (a : R) → S) ((s • p).coeff a) : S) (x ^ a) =
  HMul.hMul (α := S) (β := S) ((g : (a : R) → S) s : S)
    (∑ a ∈ range p.natDegree.succ, HMul.hMul (α := S) ((g : (a : R) → S) (p.coeff a) : S) (x ^ a) : S)
Tactic: rw [eval₂_eq_sum, eval₂_eq_sum, sum_over_range' _ _ _ A, sum_over_range' _ _ _ B]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.SMul (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
rw :
  ∑ a ∈ range p.natDegree.succ, HMul.hMul (α := S) ((g : (a : R) → S) ((s • p).coeff a) : S) (x ^ a) =
    HMul.hMul (α := S) (β := S) ((g : (a : R) → S) s : S)
      (∑ a ∈ range p.natDegree.succ, HMul.hMul (α := S) ((g : (a : R) → S) (p.coeff a) : S) (x ^ a) : S)
⊢ eval₂ g x (s • p) = HMul.hMul (α := S) ((g : (a : R) → S) s : S) (eval₂ g x p)
have rw₁ : ∀ (n : ℕ), HMul.hMul (α := S) ((g : (a : R) → S) 0 : S) (x ^ n) = 0
Tactic: rw [eval₂_eq_sum, eval₂_eq_sum, sum_over_range' _ _ _ A, sum_over_range' _ _ _ B]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.SMul (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : SMulZeroClass S R
inst_2 : IsScalarTower S R R
s : S
p : R[X]
x : R
⊢ eval x (s • p) = s • eval x p
have rw : eval x (HSMul.hSMul (β := R) s 1 • p) = s • eval x p
Tactic: rw [← smul_one_smul R s p, eval, eval₂_smul, RingHom.id_apply, smul_one_mul, eval₂_id]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.SMul (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : SMulZeroClass S R
inst_2 : IsScalarTower S R R
s : S
p : R[X]
x : R
rw : eval x (HSMul.hSMul (β := R) s 1 • p) = s • eval x p
⊢ eval x (s • p) = s • eval x p
have rw₁ : eval₂ (RingHom.id R) x (HSMul.hSMul (β := R) s 1 • p) = s • eval x p
Tactic: rw [← smul_one_smul R s p, eval, eval₂_smul, RingHom.id_apply, smul_one_mul, eval₂_id]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.SMul (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : SMulZeroClass S R
inst_2 : IsScalarTower S R R
s : S
p : R[X]
x : R
rw : eval x (HSMul.hSMul (β := R) s 1 • p) = s • eval x p
rw₁ : eval₂ (RingHom.id R) x (HSMul.hSMul (β := R) s 1 • p) = s • eval x p
⊢ eval x (s • p) = s • eval x p
have rw₂ : HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) (HSMul.hSMul (β := R) s 1) : R) (eval₂ (RingHom.id R) x p) =
  s • eval x p
Tactic: rw [← smul_one_smul R s p, eval, eval₂_smul, RingHom.id_apply, smul_one_mul, eval₂_id]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.SMul (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : SMulZeroClass S R
inst_2 : IsScalarTower S R R
s : S
p : R[X]
x : R
rw : eval x (HSMul.hSMul (β := R) s 1 • p) = s • eval x p
rw₁ : eval₂ (RingHom.id R) x (HSMul.hSMul (β := R) s 1 • p) = s • eval x p
rw₂ :
  HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) (HSMul.hSMul (β := R) s 1) : R) (eval₂ (RingHom.id R) x p) =
    s • eval x p
⊢ eval x (s • p) = s • eval x p
have rw₃ : HSMul.hSMul (β := R) s 1 * eval₂ (RingHom.id R) x p = s • eval x p
Tactic: rw [← smul_one_smul R s p, eval, eval₂_smul, RingHom.id_apply, smul_one_mul, eval₂_id]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.SMul (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : SMulZeroClass S R
inst_2 : IsScalarTower S R R
s : S
p : R[X]
x : R
rw : eval x (HSMul.hSMul (β := R) s 1 • p) = s • eval x p
rw₁ : eval₂ (RingHom.id R) x (HSMul.hSMul (β := R) s 1 • p) = s • eval x p
rw₂ :
  HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) (HSMul.hSMul (β := R) s 1) : R) (eval₂ (RingHom.id R) x p) =
    s • eval x p
rw₃ : HSMul.hSMul (β := R) s 1 * eval₂ (RingHom.id R) x p = s • eval x p
⊢ eval x (s • p) = s • eval x p
have rw₄ : s • eval₂ (RingHom.id R) x p = s • eval x p
Tactic: rw [← smul_one_smul R s p, eval, eval₂_smul, RingHom.id_apply, smul_one_mul, eval₂_id]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.SMul (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : SMulZeroClass S R
inst_2 : IsScalarTower S R R
s : S
p : R[X]
x : R
rw : eval x (HSMul.hSMul (β := R) s 1 • p) = s • eval x p
rw₁ : eval₂ (RingHom.id R) x (HSMul.hSMul (β := R) s 1 • p) = s • eval x p
rw₂ :
  HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) (HSMul.hSMul (β := R) s 1) : R) (eval₂ (RingHom.id R) x p) =
    s • eval x p
rw₃ : HSMul.hSMul (β := R) s 1 * eval₂ (RingHom.id R) x p = s • eval x p
rw₄ : s • eval₂ (RingHom.id R) x p = s • eval x p
⊢ eval x (s • p) = s • eval x p
have rw₅ : s • eval x p = s • eval x p
Tactic: rw [← smul_one_smul R s p, eval, eval₂_smul, RingHom.id_apply, smul_one_mul, eval₂_id]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.SMul (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : SMulZeroClass S R
inst_2 : IsScalarTower S R R
s : S
p q : R[X]
⊢ (s • p).comp q = s • p.comp q
have rw : (HSMul.hSMul (β := R) s 1 • p).comp q = s • p.comp q
Tactic: rw [← smul_one_smul R s p, comp, comp, eval₂_smul, ← smul_eq_C_mul, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.SMul (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : SMulZeroClass S R
inst_2 : IsScalarTower S R R
s : S
p q : R[X]
rw : (HSMul.hSMul (β := R) s 1 • p).comp q = s • p.comp q
⊢ (s • p).comp q = s • p.comp q
have rw₁ : eval₂ C q (HSMul.hSMul (β := R) s 1 • p) = s • p.comp q
Tactic: rw [← smul_one_smul R s p, comp, comp, eval₂_smul, ← smul_eq_C_mul, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.SMul (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : SMulZeroClass S R
inst_2 : IsScalarTower S R R
s : S
p q : R[X]
rw : (HSMul.hSMul (β := R) s 1 • p).comp q = s • p.comp q
rw₁ : eval₂ C q (HSMul.hSMul (β := R) s 1 • p) = s • p.comp q
⊢ (s • p).comp q = s • p.comp q
have rw₂ : eval₂ C q (HSMul.hSMul (β := R) s 1 • p) = s • eval₂ C q p
Tactic: rw [← smul_one_smul R s p, comp, comp, eval₂_smul, ← smul_eq_C_mul, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.SMul (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : SMulZeroClass S R
inst_2 : IsScalarTower S R R
s : S
p q : R[X]
rw : (HSMul.hSMul (β := R) s 1 • p).comp q = s • p.comp q
rw₁ : eval₂ C q (HSMul.hSMul (β := R) s 1 • p) = s • p.comp q
rw₂ : eval₂ C q (HSMul.hSMul (β := R) s 1 • p) = s • eval₂ C q p
⊢ (s • p).comp q = s • p.comp q
have rw₃ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HSMul.hSMul (β := R) s 1) : R[X]) (eval₂ C q p) = s • eval₂ C q p
Tactic: rw [← smul_one_smul R s p, comp, comp, eval₂_smul, ← smul_eq_C_mul, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.SMul (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : SMulZeroClass S R
inst_2 : IsScalarTower S R R
s : S
p q : R[X]
rw : (HSMul.hSMul (β := R) s 1 • p).comp q = s • p.comp q
rw₁ : eval₂ C q (HSMul.hSMul (β := R) s 1 • p) = s • p.comp q
rw₂ : eval₂ C q (HSMul.hSMul (β := R) s 1 • p) = s • eval₂ C q p
rw₃ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HSMul.hSMul (β := R) s 1) : R[X]) (eval₂ C q p) = s • eval₂ C q p
⊢ (s • p).comp q = s • p.comp q
have rw₄ : HSMul.hSMul (β := R) s 1 • eval₂ C q p = s • eval₂ C q p
Tactic: rw [← smul_one_smul R s p, comp, comp, eval₂_smul, ← smul_eq_C_mul, smul_assoc, one_smul]