awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
⊢ eval 1 (map f p) = (f : (a : R) → S) (eval 1 p)
have add : ∀ (p q : R[X]) (hp : eval 1 (map f p) = (f : (a : R) → S) (eval 1 p))
  (hq : eval 1 (map f q) = (f : (a : R) → S) (eval 1 q)), eval 1 (map f (p + q)) = (f : (a : R) → S) (eval 1 (p + q))
Tactic: induction p using Polynomial.induction_on' with
  | add p q hp hq => simp only [hp, hq, Polynomial.map_add, map_add, eval_add]
  | monomial n r => simp only [one_pow, mul_one, eval_monomial, map_monomial]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
add :
  ∀ (p q : R[X]) (hp : eval 1 (map f p) = (f : (a : R) → S) (eval 1 p))
    (hq : eval 1 (map f q) = (f : (a : R) → S) (eval 1 q)), eval 1 (map f (p + q)) = (f : (a : R) → S) (eval 1 (p + q))
⊢ eval 1 (map f p) = (f : (a : R) → S) (eval 1 p)
have monomial : ∀ (n : ℕ) (r : R),
  eval 1 (map f ((monomial n : (a : R) → R[X]) r)) = (f : (a : R) → S) (eval 1 ((monomial n : (a : R) → R[X]) r))
Tactic: induction p using Polynomial.induction_on' with
  | add p q hp hq => simp only [hp, hq, Polynomial.map_add, map_add, eval_add]
  | monomial n r => simp only [one_pow, mul_one, eval_monomial, map_monomial]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ eval (↑n : S) (map f p) = (f : (a : R) → S) (eval (↑n : R) p)
have add : ∀ (p q : R[X]) (hp : eval (↑n : S) (map f p) = (f : (a : R) → S) (eval (↑n : R) p))
  (hq : eval (↑n : S) (map f q) = (f : (a : R) → S) (eval (↑n : R) q)),
  eval (↑n : S) (map f (p + q)) = (f : (a : R) → S) (eval (↑n : R) (p + q))
Tactic: induction p using Polynomial.induction_on' with
  | add p q hp hq => simp only [hp, hq, Polynomial.map_add, map_add, eval_add]
  | monomial n r => simp only [map_natCast f, eval_monomial, map_monomial, f.map_pow, f.map_mul]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
n : ℕ
add :
  ∀ (p q : R[X]) (hp : eval (↑n : S) (map f p) = (f : (a : R) → S) (eval (↑n : R) p))
    (hq : eval (↑n : S) (map f q) = (f : (a : R) → S) (eval (↑n : R) q)),
    eval (↑n : S) (map f (p + q)) = (f : (a : R) → S) (eval (↑n : R) (p + q))
⊢ eval (↑n : S) (map f p) = (f : (a : R) → S) (eval (↑n : R) p)
have monomial : ∀ (n_1 : ℕ) (r : R),
  eval (↑n : S) (map f ((monomial n_1 : (a : R) → R[X]) r)) =
    (f : (a : R) → S) (eval (↑n : R) ((monomial n_1 : (a : R) → R[X]) r))
Tactic: induction p using Polynomial.induction_on' with
  | add p q hp hq => simp only [hp, hq, Polynomial.map_add, map_add, eval_add]
  | monomial n r => simp only [map_natCast f, eval_monomial, map_monomial, f.map_pow, f.map_mul]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
p : R[X]
i : ℤ
⊢ eval (↑i : S) (map f p) = (f : (a : R) → S) (eval (↑i : R) p)
have add : ∀ (p q : R[X]) (hp : eval (↑i : S) (map f p) = (f : (a : R) → S) (eval (↑i : R) p))
  (hq : eval (↑i : S) (map f q) = (f : (a : R) → S) (eval (↑i : R) q)),
  eval (↑i : S) (map f (p + q)) = (f : (a : R) → S) (eval (↑i : R) (p + q))
Tactic: induction p using Polynomial.induction_on' with
  | add p q hp hq => simp only [hp, hq, Polynomial.map_add, map_add, eval_add]
  | monomial n r => simp only [map_intCast, eval_monomial, map_monomial, map_pow, map_mul]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
p : R[X]
i : ℤ
add :
  ∀ (p q : R[X]) (hp : eval (↑i : S) (map f p) = (f : (a : R) → S) (eval (↑i : R) p))
    (hq : eval (↑i : S) (map f q) = (f : (a : R) → S) (eval (↑i : R) q)),
    eval (↑i : S) (map f (p + q)) = (f : (a : R) → S) (eval (↑i : R) (p + q))
⊢ eval (↑i : S) (map f p) = (f : (a : R) → S) (eval (↑i : R) p)
have monomial : ∀ (n : ℕ) (r : R),
  eval (↑i : S) (map f ((monomial n : (a : R) → R[X]) r)) =
    (f : (a : R) → S) (eval (↑i : R) ((monomial n : (a : R) → R[X]) r))
Tactic: induction p using Polynomial.induction_on' with
  | add p q hp hq => simp only [hp, hq, Polynomial.map_add, map_add, eval_add]
  | monomial n r => simp only [map_intCast, eval_monomial, map_monomial, map_pow, map_mul]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : Semiring R
p : R[X]
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
x : S
⊢ (g : (a : S) → T) (eval₂ f x p) = eval₂ (g.comp f) ((g : (a : S) → T) x) p
have rw : (g : (a : S) → T) (eval₂ f x p) = eval₂ g ((g : (a : S) → T) x) (map f p)
Tactic: rw [← eval₂_map, eval₂_at_apply, eval_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : Semiring R
p : R[X]
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
x : S
rw : (g : (a : S) → T) (eval₂ f x p) = eval₂ g ((g : (a : S) → T) x) (map f p)
⊢ (g : (a : S) → T) (eval₂ f x p) = eval₂ (g.comp f) ((g : (a : S) → T) x) p
have rw₁ : Eq.{w + 1} (α := T) ((g : (a : S) → T) (eval₂ f x p) : T) ((g : (a : S) → T) (eval x (map f p)) : T)
Tactic: rw [← eval₂_map, eval₂_at_apply, eval_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : Semiring R
p : R[X]
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
x : S
rw : (g : (a : S) → T) (eval₂ f x p) = eval₂ g ((g : (a : S) → T) x) (map f p)
rw₁ : Eq.{w + 1} (α := T) ((g : (a : S) → T) (eval₂ f x p) : T) ((g : (a : S) → T) (eval x (map f p)) : T)
⊢ (g : (a : S) → T) (eval₂ f x p) = eval₂ (g.comp f) ((g : (a : S) → T) x) p
have rw₂ : Eq.{w + 1} (α := T) ((g : (a : S) → T) (eval₂ f x p) : T) ((g : (a : S) → T) (eval₂ f x p) : T)
Tactic: rw [← eval₂_map, eval₂_at_apply, eval_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
x : ℕ
⊢ x ∈ (map f p).support → x ∈ p.support
have contrapose : x ∉ p.support → x ∉ (map f p).support
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ (map f p).support = p.support
have simp_rw : ∀ (a : ℕ), a ∈ (map f p).support ↔ a ∈ p.support
Tactic: simp_rw [Finset.ext_iff, mem_support_iff, coeff_map, ← map_zero f, hf.ne_iff,
    forall_const]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
simp_rw : ∀ (a : ℕ), a ∈ (map f p).support ↔ a ∈ p.support
⊢ (map f p).support = p.support
have simp_rw₁ : ∀ (a : ℕ), (map f p).coeff a ≠ 0 ↔ p.coeff a ≠ 0
Tactic: simp_rw [Finset.ext_iff, mem_support_iff, coeff_map, ← map_zero f, hf.ne_iff,
    forall_const]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
simp_rw : ∀ (a : ℕ), a ∈ (map f p).support ↔ a ∈ p.support
simp_rw₁ : ∀ (a : ℕ), (map f p).coeff a ≠ 0 ↔ p.coeff a ≠ 0
⊢ (map f p).support = p.support
have simp_rw₂ : ∀ (a : ℕ), Ne.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff a) : S) (0 : S) ↔ p.coeff a ≠ 0
Tactic: simp_rw [Finset.ext_iff, mem_support_iff, coeff_map, ← map_zero f, hf.ne_iff,
    forall_const]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
simp_rw : ∀ (a : ℕ), a ∈ (map f p).support ↔ a ∈ p.support
simp_rw₁ : ∀ (a : ℕ), (map f p).coeff a ≠ 0 ↔ p.coeff a ≠ 0
simp_rw₂ : ∀ (a : ℕ), Ne.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff a) : S) (0 : S) ↔ p.coeff a ≠ 0
⊢ (map f p).support = p.support
have simp_rw₃ : ∀ (a : ℕ), Ne.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff a) : S) ((f : (a : R) → S) 0 : S) ↔ p.coeff a ≠ 0
Tactic: simp_rw [Finset.ext_iff, mem_support_iff, coeff_map, ← map_zero f, hf.ne_iff,
    forall_const]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
simp_rw : ∀ (a : ℕ), a ∈ (map f p).support ↔ a ∈ p.support
simp_rw₁ : ∀ (a : ℕ), (map f p).coeff a ≠ 0 ↔ p.coeff a ≠ 0
simp_rw₂ : ∀ (a : ℕ), Ne.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff a) : S) (0 : S) ↔ p.coeff a ≠ 0
simp_rw₃ : ∀ (a : ℕ), Ne.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff a) : S) ((f : (a : R) → S) 0 : S) ↔ p.coeff a ≠ 0
⊢ (map f p).support = p.support
have simp_rw₄ : ∀ (a : ℕ), True
Tactic: simp_rw [Finset.ext_iff, mem_support_iff, coeff_map, ← map_zero f, hf.ne_iff,
    forall_const]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : R
p : R[X]
h : p.IsRoot x
⊢ (Polynomial.map f p).IsRoot ((f : (a : R) → S) x)
have rw : Eq.{v + 1} (α := S) (eval ((f : (a : R) → S) x) (Polynomial.map f p) : S) (0 : S)
Tactic: rw [IsRoot, eval_map, eval₂_hom, h.eq_zero, f.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : R
p : R[X]
h : p.IsRoot x
rw : Eq.{v + 1} (α := S) (eval ((f : (a : R) → S) x) (Polynomial.map f p) : S) (0 : S)
⊢ (Polynomial.map f p).IsRoot ((f : (a : R) → S) x)
have rw₁ : eval₂ f ((f : (a : R) → S) x) p = 0
Tactic: rw [IsRoot, eval_map, eval₂_hom, h.eq_zero, f.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : R
p : R[X]
h : p.IsRoot x
rw : Eq.{v + 1} (α := S) (eval ((f : (a : R) → S) x) (Polynomial.map f p) : S) (0 : S)
rw₁ : eval₂ f ((f : (a : R) → S) x) p = 0
⊢ (Polynomial.map f p).IsRoot ((f : (a : R) → S) x)
have rw₂ : Eq.{v + 1} (α := S) ((f : (a : R) → S) (eval x p) : S) (0 : S)
Tactic: rw [IsRoot, eval_map, eval₂_hom, h.eq_zero, f.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : R
p : R[X]
h : p.IsRoot x
rw : Eq.{v + 1} (α := S) (eval ((f : (a : R) → S) x) (Polynomial.map f p) : S) (0 : S)
rw₁ : eval₂ f ((f : (a : R) → S) x) p = 0
rw₂ : Eq.{v + 1} (α := S) ((f : (a : R) → S) (eval x p) : S) (0 : S)
⊢ (Polynomial.map f p).IsRoot ((f : (a : R) → S) x)
have rw₃ : Eq.{v + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)
Tactic: rw [IsRoot, eval_map, eval₂_hom, h.eq_zero, f.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : R
p : R[X]
h : p.IsRoot x
rw : Eq.{v + 1} (α := S) (eval ((f : (a : R) → S) x) (Polynomial.map f p) : S) (0 : S)
rw₁ : eval₂ f ((f : (a : R) → S) x) p = 0
rw₂ : Eq.{v + 1} (α := S) ((f : (a : R) → S) (eval x p) : S) (0 : S)
rw₃ : Eq.{v + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)
⊢ (Polynomial.map f p).IsRoot ((f : (a : R) → S) x)
have rw₄ : Eq.{v + 1} (α := S) 0 0
Tactic: rw [IsRoot, eval_map, eval₂_hom, h.eq_zero, f.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
S : Type v
inst : CommSemiring S
R : Type u_1
inst_1 : Ring R
f : R →+* S
x : R
p : R[X]
h : (Polynomial.map f p).IsRoot ((f : (a : R) → S) x)
hf : Function.Injective.{u_1 + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ p.IsRoot x
have rwa : eval x p = 0
Tactic: rwa [IsRoot, ← (injective_iff_map_eq_zero' f).mp hf, ← eval₂_hom, ← eval_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
S : Type v
inst : CommSemiring S
R : Type u_1
inst_1 : Ring R
f : R →+* S
x : R
p : R[X]
h : (Polynomial.map f p).IsRoot ((f : (a : R) → S) x)
hf : Function.Injective.{u_1 + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
rwa : eval x p = 0
⊢ p.IsRoot x
have rwa₁ : Eq.{v + 1} (α := S) ((f : (a : R) → S) (eval x p) : S) (0 : S)
Tactic: rwa [IsRoot, ← (injective_iff_map_eq_zero' f).mp hf, ← eval₂_hom, ← eval_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
S : Type v
inst : CommSemiring S
R : Type u_1
inst_1 : Ring R
f : R →+* S
x : R
p : R[X]
h : (Polynomial.map f p).IsRoot ((f : (a : R) → S) x)
hf : Function.Injective.{u_1 + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
rwa : eval x p = 0
rwa₁ : Eq.{v + 1} (α := S) ((f : (a : R) → S) (eval x p) : S) (0 : S)
⊢ p.IsRoot x
have rwa₂ : eval₂ f ((f : (a : R) → S) x) p = 0
Tactic: rwa [IsRoot, ← (injective_iff_map_eq_zero' f).mp hf, ← eval₂_hom, ← eval_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Coeff (goal)
Goal:
S : Type v
inst : CommSemiring S
R : Type u_1
inst_1 : Ring R
f : R →+* S
x : R
p : R[X]
h : (Polynomial.map f p).IsRoot ((f : (a : R) → S) x)
hf : Function.Injective.{u_1 + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
rwa : eval x p = 0
rwa₁ : Eq.{v + 1} (α := S) ((f : (a : R) → S) (eval x p) : S) (0 : S)
rwa₂ : eval₂ f ((f : (a : R) → S) x) p = 0
⊢ p.IsRoot x
have rwa₃ : Eq.{v + 1} (α := S) (eval ((f : (a : R) → S) x) (Polynomial.map f p) : S) (0 : S)
Tactic: rwa [IsRoot, ← (injective_iff_map_eq_zero' f).mp hf, ← eval₂_hom, ← eval_map]
-- 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 = p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((f : (a : R) → S) a : S) (x ^ e)
have rw : Eq.{v + 1} (α := S) (p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((f : (a : R) → S) a : S) (x ^ e))
  (p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((f : (a : R) → S) a : S) (x ^ e))
Tactic: rw [eval₂_def]
-- 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
n : ℕ
⊢ eval₂ f x (HPow.hPow (α := R[X]) X n) = x ^ n
have rw : eval₂ f x ((monomial n : (a : R) → R[X]) 1) = x ^ n
Tactic: rw [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
inst_1 : Semiring S
f : R →+* S
x : S
n : ℕ
⊢ eval₂ f x ((monomial n : (a : R) → R[X]) 1) = x ^ n
have h : x ^ n = HMul.hMul (α := S) ((f : (a : R) → S) 1 : S) (x ^ n)
Tactic: convert! eval₂_monomial f x (n := n) (r := 1)
-- 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
⊢ eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q
have simp : ((p + q).sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((f : (a : R) → S) a : S) (x ^ e)) =
  HAdd.hAdd (α := S) (p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((f : (a : R) → S) a : S) (x ^ e))
    (q.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((f : (a : R) → S) a : S) (x ^ e))
Tactic: simp only [eval₂_eq_sum]
-- 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
⊢ ((p + q).sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((f : (a : R) → S) a : S) (x ^ e)) =
    HAdd.hAdd (α := S) (p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((f : (a : R) → S) a : S) (x ^ e))
      (q.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((f : (a : R) → S) a : S) (x ^ e))
have hf : ∀ (i : ℕ), HMul.hMul (α := S) ((f : (a : R) → S) 0 : S) (x ^ i) = 0
Tactic: apply sum_add_index
-- 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 : ∀ (i : ℕ), HMul.hMul (α := S) ((f : (a : R) → S) 0 : S) (x ^ i) = 0
⊢ ((p + q).sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((f : (a : R) → S) a : S) (x ^ e)) =
    HAdd.hAdd (α := S) (p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((f : (a : R) → S) a : S) (x ^ e))
      (q.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((f : (a : R) → S) a : S) (x ^ e))
have h_add : ∀ (a : ℕ) (b₁ b₂ : R),
  HMul.hMul (α := S) ((f : (a : R) → S) (b₁ + b₂) : S) (x ^ a) =
    HMul.hMul (α := S) ((f : (a : R) → S) b₁ : S) (x ^ a) + HMul.hMul (α := S) ((f : (a : R) → S) b₂ : S) (x ^ a)
Tactic: apply sum_add_index
-- 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
⊢ eval₂ f x 1 = 1
have rw : eval₂ f x ((C : (a : R) → R[X]) 1) = 1
Tactic: rw [← C_1, eval₂_C, f.map_one]
-- 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
rw : eval₂ f x ((C : (a : R) → R[X]) 1) = 1
⊢ eval₂ f x 1 = 1
have rw₁ : Eq.{v + 1} (α := S) ((f : (a : R) → S) 1 : S) (1 : S)
Tactic: rw [← C_1, eval₂_C, f.map_one]
-- 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
rw : eval₂ f x ((C : (a : R) → R[X]) 1) = 1
rw₁ : Eq.{v + 1} (α := S) ((f : (a : R) → S) 1 : S) (1 : S)
⊢ eval₂ f x 1 = 1
have rw₂ : Eq.{v + 1} (α := S) 1 1
Tactic: rw [← C_1, eval₂_C, f.map_one]
-- 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
n : ℕ
ih : eval₂ f x (↑n : R[X]) = (↑n : S)
⊢ eval₂ f x (↑(n + 1) : R[X]) = (↑(n + 1) : S)
have succ : eval₂ f x (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1) = (↑(n + 1) : S)
Tactic: rw [n.cast_succ, eval₂_add, ih, eval₂_one, n.cast_succ]
-- 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
n : ℕ
ih : eval₂ f x (↑n : R[X]) = (↑n : S)
succ : eval₂ f x (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1) = (↑(n + 1) : S)
⊢ eval₂ f x (↑(n + 1) : R[X]) = (↑(n + 1) : S)
have succ₁ : eval₂ f x (↑n : R[X]) + eval₂ f x 1 = (↑(n + 1) : S)
Tactic: rw [n.cast_succ, eval₂_add, ih, eval₂_one, n.cast_succ]
-- 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
n : ℕ
ih : eval₂ f x (↑n : R[X]) = (↑n : S)
succ : eval₂ f x (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1) = (↑(n + 1) : S)
succ₁ : eval₂ f x (↑n : R[X]) + eval₂ f x 1 = (↑(n + 1) : S)
⊢ eval₂ f x (↑(n + 1) : R[X]) = (↑(n + 1) : S)
have succ₂ : (↑n : S) + eval₂ f x 1 = (↑(n + 1) : S)
Tactic: rw [n.cast_succ, eval₂_add, ih, eval₂_one, n.cast_succ]
-- 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
n : ℕ
ih : eval₂ f x (↑n : R[X]) = (↑n : S)
succ : eval₂ f x (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1) = (↑(n + 1) : S)
succ₁ : eval₂ f x (↑n : R[X]) + eval₂ f x 1 = (↑(n + 1) : S)
succ₂ : (↑n : S) + eval₂ f x 1 = (↑(n + 1) : S)
⊢ eval₂ f x (↑(n + 1) : R[X]) = (↑(n + 1) : S)
have succ₃ : HAdd.hAdd (α := S) (↑n : S) 1 = (↑(n + 1) : S)
Tactic: rw [n.cast_succ, eval₂_add, ih, eval₂_one, n.cast_succ]
-- 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
n : ℕ
ih : eval₂ f x (↑n : R[X]) = (↑n : S)
succ : eval₂ f x (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1) = (↑(n + 1) : S)
succ₁ : eval₂ f x (↑n : R[X]) + eval₂ f x 1 = (↑(n + 1) : S)
succ₂ : (↑n : S) + eval₂ f x 1 = (↑(n + 1) : S)
succ₃ : HAdd.hAdd (α := S) (↑n : S) 1 = (↑(n + 1) : S)
⊢ eval₂ f x (↑(n + 1) : R[X]) = (↑(n + 1) : S)
have succ₄ : HAdd.hAdd (α := S) (↑n : S) 1 = HAdd.hAdd (α := S) (↑n : S) 1
Tactic: rw [n.cast_succ, eval₂_add, ih, eval₂_one, n.cast_succ]
-- 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
n : ℕ
⊢ eval₂ f x (↑n : R[X]) = (↑n : S)
have zero : eval₂ f x (↑0 : R[X]) = (↑0 : S)
Tactic: induction n with
  | zero => simp only [eval₂_zero, Nat.cast_zero]
  | succ n ih => rw [n.cast_succ, eval₂_add, ih, eval₂_one, n.cast_succ]
Cleared hypotheses: n
-- 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
n : ℕ
zero : eval₂ f x (↑0 : R[X]) = (↑0 : S)
⊢ eval₂ f x (↑n : R[X]) = (↑n : S)
have succ : ∀ (n : ℕ) (ih : eval₂ f x (↑n : R[X]) = (↑n : S)), eval₂ f x (↑(n + 1) : R[X]) = (↑(n + 1) : S)
Tactic: induction n with
  | zero => simp only [eval₂_zero, Nat.cast_zero]
  | succ n ih => rw [n.cast_succ, eval₂_add, ih, eval₂_one, n.cast_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (hypothesis)
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' := ⋯ }
⊢ eval₂ f x (p.sum g) = p.sum fun (n : ℕ) (a : T_1) ↦ eval₂ f x (g n a)
have A : ∀ (y : R[X]), eval₂ f x y = (T : (a : R[X]) → S) y
Tactic: have A : ∀ y, eval₂ f x y = T y := fun y => rfl
-- 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
⊢ eval₂ f x (p.sum g) = p.sum fun (n : ℕ) (a : T_1) ↦ eval₂ f x (g n a)
have simp : 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)
Tactic: simp only [A]
-- 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
⊢ 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) ((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)
Tactic: rw [sum, map_sum, sum]
-- 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)
⊢ 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)))
  (p.sum fun (n : ℕ) (a : T_1) ↦ (T : (a : R[X]) → S) (g n a))
Tactic: rw [sum, map_sum, sum]