awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
h : ∀ (n : ℕ), (map f p).coeff n = ((⇑f : (a : R) → S) ∘ p.coeff) n
⊢ (map f p).coeff = (⇑f : (a : R) → S) ∘ p.coeff

Tactic:
ext n
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n : ℕ
⊢ (map f p).coeff n = ((⇑f : (a : R) → S) ∘ p.coeff) n

Tactic:
coeff_map ..

Premises used: Polynomial.coeff_map
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n : ℕ
⊢ (map f p).coeff n = ((⇑f : (a : R) → S) ∘ p.coeff) n

Tactic:
exact coeff_map ..

Premises used: Polynomial.coeff_map
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
T : Type w
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
inst_2 : Semiring T
g : S →+* T
p : R[X]
⊢ ∀ (n : ℕ), (map g (map f p)).coeff n = (map (g.comp f) p).coeff n

Tactic:
simp [coeff_map]

Premises used: Polynomial.coeff_map
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ map (RingHom.id R) p = p

Tactic:
simp [Polynomial.ext_iff, coeff_map]

Premises used: Polynomial.coeff_map, Polynomial.ext_iff
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R_1 : Type u
S : Type v
T : Type w
ι_1 : Type y
a b : R_1
m n : ℕ
inst : Semiring R_1
p_1 q_1 r : R_1[X]
inst_1 : Semiring S
f : R_1 →+* S
ι : Type u_2
inst_2 : Finite ι
R : ι → Type u_1
inst_3 : (i : ι) → Semiring (R i)
p q : ((i : ι) → R i)[X]
h :
  Eq (α := (i : ι) → (R i)[X])
    ((Pi.ringHom (f := fun (i : ι) ↦ (R i)[X]) fun (i : ι) ↦ mapRingHom (Pi.evalRingHom R i) :
          (a : ((i : ι) → R i)[X]) → (i : ι) → (R i)[X])
        p :
      (i : ι) → (R i)[X])
    ((Pi.ringHom (f := fun (i : ι) ↦ (R i)[X]) fun (i : ι) ↦ mapRingHom (Pi.evalRingHom R i) :
          (a : ((i : ι) → R i)[X]) → (i : ι) → (R i)[X])
        q :
      (i : ι) → (R i)[X])
a₁ : ∀ (n : ℕ) (i : ι), p.coeff n i = q.coeff n i
⊢ p = q

Tactic:
ext n i
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R_1 : Type u
S : Type v
T : Type w
ι_1 : Type y
a b : R_1
m n_1 : ℕ
inst : Semiring R_1
p_1 q_1 r : R_1[X]
inst_1 : Semiring S
f : R_1 →+* S
ι : Type u_2
inst_2 : Finite ι
R : ι → Type u_1
inst_3 : (i : ι) → Semiring (R i)
p q : ((i : ι) → R i)[X]
h :
  Eq (α := (i : ι) → (R i)[X])
    ((Pi.ringHom (f := fun (i : ι) ↦ (R i)[X]) fun (i : ι) ↦ mapRingHom (Pi.evalRingHom R i) :
          (a : ((i : ι) → R i)[X]) → (i : ι) → (R i)[X])
        p :
      (i : ι) → (R i)[X])
    ((Pi.ringHom (f := fun (i : ι) ↦ (R i)[X]) fun (i : ι) ↦ mapRingHom (Pi.evalRingHom R i) :
          (a : ((i : ι) → R i)[X]) → (i : ι) → (R i)[X])
        q :
      (i : ι) → (R i)[X])
n : ℕ
i : ι
⊢ p.coeff n i = q.coeff n i

Tactic:
simpa using congr_arg (fun p ↦ coeff (p i) n) h

Premises used: Polynomial.coeff, congr_arg
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R_1 : Type u
S : Type v
T : Type w
ι_1 : Type y
a b : R_1
m n_1 : ℕ
inst : Semiring R_1
p_1 q r : R_1[X]
inst_1 : Semiring S
f : R_1 →+* S
ι : Type u_2
inst_2 : Finite ι
R : ι → Type u_1
inst_3 : (i : ι) → Semiring (R i)
p : (i : ι) → (R i)[X]
n : ℕ
hn : Membership.mem (γ := Set ℕ) (Function.support (M := (i : ι) → R i) fun (n : ℕ) (i : ι) ↦ (p i).coeff n) n
simp : ∀ (hn : Ne (α := (i : ι) → R i) (fun (i : ι) ↦ (p i).coeff n) 0), ∃ (i : ι), (p i).coeff n ≠ 0
⊢ Membership.mem (γ := Set ℕ) (⋃ (i : ι), (↑(p i).support : Set ℕ)) n

Tactic:
simp only [Set.mem_iUnion, Finset.mem_coe, mem_support_iff, Function.mem_support] at hn ⊢

Premises used: Set.mem_iUnion, Polynomial.mem_support_iff, Function.mem_support, Finset.mem_coe
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R_1 : Type u
S : Type v
T : Type w
ι_1 : Type y
a b : R_1
m n_1 : ℕ
inst : Semiring R_1
p_1 q r : R_1[X]
inst_1 : Semiring S
f : R_1 →+* S
ι : Type u_2
inst_2 : Finite ι
R : ι → Type u_1
inst_3 : (i : ι) → Semiring (R i)
p : (i : ι) → (R i)[X]
n : ℕ
hn : Ne (α := (i : ι) → R i) (fun (i : ι) ↦ (p i).coeff n) 0
contrapose! : ∀ (hn : ∀ (i : ι), (p i).coeff n = 0), Eq (α := (i : ι) → R i) (fun (i : ι) ↦ (p i).coeff n) 0
⊢ ∃ (i : ι), (p i).coeff n ≠ 0

Tactic:
contrapose! hn
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R_1 : Type u
S : Type v
T : Type w
ι_1 : Type y
a b : R_1
m n_1 : ℕ
inst : Semiring R_1
p_1 q r : R_1[X]
inst_1 : Semiring S
f : R_1 →+* S
ι : Type u_2
inst_2 : Finite ι
R : ι → Type u_1
inst_3 : (i : ι) → Semiring (R i)
p : (i : ι) → (R i)[X]
n : ℕ
hn : ∀ (i : ι), (p i).coeff n = 0
⊢ Eq (α := (i : ι) → R i) (fun (i : ι) ↦ (p i).coeff n) 0

Tactic:
funext hn

Premises used: funext
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R_1 : Type u
S : Type v
T : Type w
ι_1 : Type y
a b : R_1
m n_1 : ℕ
inst : Semiring R_1
p_1 q r : R_1[X]
inst_1 : Semiring S
f : R_1 →+* S
ι : Type u_2
inst_2 : Finite ι
R : ι → Type u_1
inst_3 : (i : ι) → Semiring (R i)
p : (i : ι) → (R i)[X]
n : ℕ
hn : ∀ (i : ι), (p i).coeff n = 0
⊢ Eq (α := (i : ι) → R i) (fun (i : ι) ↦ (p i).coeff n) 0

Tactic:
exact funext hn

Premises used: funext
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R_1 : Type u
S : Type v
T : Type w
ι_1 : Type y
a b : R_1
m n : ℕ
inst : Semiring R_1
p_1 q r : R_1[X]
inst_1 : Semiring S
f : R_1 →+* S
ι : Type u_2
inst_2 : Finite ι
R : ι → Type u_1
inst_3 : (i : ι) → Semiring (R i)
p : (i : ι) → (R i)[X]
h :
  ∀ (i : ι) (n : ℕ),
    coeff
        ((Pi.ringHom (f := fun (i : ι) ↦ (R i)[X]) fun (i : ι) ↦ mapRingHom (Pi.evalRingHom R i) :
            (a : ((i : ι) → R i)[X]) → (i : ι) → (R i)[X])
          { toFinsupp := Finsupp.ofSupportFinite (fun (n : ℕ) (i : ι) ↦ (p i).coeff n) ⋯ } i)
        n =
      (p i).coeff n
⊢ (Pi.ringHom (f := fun (i : ι) ↦ (R i)[X]) fun (i : ι) ↦ mapRingHom (Pi.evalRingHom R i) :
        (a : ((i : ι) → R i)[X]) → (i : ι) → (R i)[X])
      { toFinsupp := Finsupp.ofSupportFinite (fun (n : ℕ) (i : ι) ↦ (p i).coeff n) ⋯ } =
    p

Tactic:
ext i n
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R_1 : Type u
S : Type v
T : Type w
ι_1 : Type y
a b : R_1
m n_1 : ℕ
inst : Semiring R_1
p_1 q r : R_1[X]
inst_1 : Semiring S
f : R_1 →+* S
ι : Type u_2
inst_2 : Finite ι
R : ι → Type u_1
inst_3 : (i : ι) → Semiring (R i)
p : (i : ι) → (R i)[X]
i : ι
n : ℕ
⊢ coeff
      ((Pi.ringHom (f := fun (i : ι) ↦ (R i)[X]) fun (i : ι) ↦ mapRingHom (Pi.evalRingHom R i) :
          (a : ((i : ι) → R i)[X]) → (i : ι) → (R i)[X])
        { toFinsupp := Finsupp.ofSupportFinite (fun (n : ℕ) (i : ι) ↦ (p i).coeff n) ⋯ } i)
      n =
    (p i).coeff n

Tactic:
coeff_map _ _

Premises used: Polynomial.coeff_map, Polynomial.coeff, Polynomial.map
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R_1 : Type u
S : Type v
T : Type w
ι_1 : Type y
a b : R_1
m n_1 : ℕ
inst : Semiring R_1
p_1 q r : R_1[X]
inst_1 : Semiring S
f : R_1 →+* S
ι : Type u_2
inst_2 : Finite ι
R : ι → Type u_1
inst_3 : (i : ι) → Semiring (R i)
p : (i : ι) → (R i)[X]
i : ι
n : ℕ
⊢ coeff
      ((Pi.ringHom (f := fun (i : ι) ↦ (R i)[X]) fun (i : ι) ↦ mapRingHom (Pi.evalRingHom R i) :
          (a : ((i : ι) → R i)[X]) → (i : ι) → (R i)[X])
        { toFinsupp := Finsupp.ofSupportFinite (fun (n : ℕ) (i : ι) ↦ (p i).coeff n) ⋯ } i)
      n =
    (p i).coeff n

Tactic:
exact coeff_map _ _

Premises used: Polynomial.coeff_map
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p q : R[X]
h : map f p = map f q
m : ℕ
rw : (map f p).coeff m = (f : (a : R) → S) (q.coeff m)
rw₁ : (map f p).coeff m = (map f q).coeff m
rw₂ rw₃ : (map f q).coeff m = (map f q).coeff m
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff m) : S) ((f : (a : R) → S) (q.coeff m) : S)

Tactic:
rw [← coeff_map f, ← coeff_map f, h]

Premises used: Polynomial.coeff_map
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
h : Function.Injective (map f)
r r' : R
eq : Eq.{v + 1} (α := S) ((f : (a : R) → S) r : S) ((f : (a : R) → S) r' : S)
⊢ map f ((C : (a : R) → R[X]) r) = map f ((C : (a : R) → R[X]) r')

Tactic:
simpa
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
h : Function.Injective (map f)
r r' : R
eq : Eq.{v + 1} (α := S) ((f : (a : R) → S) r : S) ((f : (a : R) → S) r' : S)
⊢ r = r'

Tactic:
simpa using h (a₁ := C r) (a₂ := C r') (by simpa)
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p_1 : S[X]
p q : R[X]
⊢ ∃ (a : R[X]), map f a = map f p + map f q

Tactic:
⟨p + q, Polynomial.map_add f⟩

Premises used: Polynomial.map_add, HAdd.hAdd, Exists.intro
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p_1 : S[X]
p q : R[X]
⊢ ∃ (a : R[X]), map f a = map f p + map f q

Tactic:
exact ⟨p + q, Polynomial.map_add f⟩
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : S[X]
n : ℕ
s : S
r : R
hr : (f : (a : R) → S) r = s
rw :
  Eq.{v + 1} (α := S[X]) ((monomial n : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X])
    ((monomial n : (a : S) → S[X]) s : S[X])
rw₁ rw₂ : Eq (α := S[X]) ((monomial n : (a : S) → S[X]) s : S[X]) ((monomial n : (a : S) → S[X]) s : S[X])
⊢ map f ((monomial n : (a : R) → R[X]) r) = (monomial n : (a : S) → S[X]) s

Tactic:
rw [map_monomial f, hr]

Premises used: Polynomial.map_monomial
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
h_1 : Function.Surjective (map f)
s : S
p : R[X]
h : map f p = (C : (a : S) → S[X]) s
⊢ (f : (a : R) → S) (p.coeff 0) = s

Tactic:
simpa using congr(coeff $h 0)
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ map f p = 0 ↔ p = 0

Tactic:
map_eq_zero_iff (mapRingHom f) (map_injective f hf)

Premises used: Polynomial.map_injective, map_eq_zero_iff, Polynomial.mapRingHom, Polynomial.map
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ map f p ≠ 0 ↔ p ≠ 0

Tactic:
(Polynomial.map_eq_zero_iff hf).not

Premises used: Iff.not, Polynomial.map_eq_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
inst : Semiring R
⊢ Eq (α := R[X] →+* R[X]) (mapRingHom (RingHom.id R)) (RingHom.id R[X])

Tactic:
RingHom.ext fun _x => map_id

Premises used: Polynomial.map_id, RingHom.ext
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
T : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : S →+* T
g : R →+* S
⊢ (mapRingHom f).comp (mapRingHom g) = mapRingHom (f.comp g)

Tactic:
RingHom.ext <| Polynomial.map_map g f

Premises used: RingHom.ext, Polynomial.map_map
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
T : Type w
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
inst_2 : Semiring T
g : S →+* T
x : T
rw : eval x (map g (map f p)) = eval₂ (g.comp f) x p
rw₁ : eval x (map g (map f p)) = eval x (map (g.comp f) p)
rw₂ rw₃ : eval x (map (g.comp f) p) = eval x (map (g.comp f) p)
⊢ eval₂ g x (map f p) = eval₂ (g.comp f) x p

Tactic:
rw [eval₂_eq_eval_map, eval₂_eq_eval_map, map_map]

Premises used: Polynomial.map_map, Polynomial.eval₂_eq_eval_map
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
⊢ eval 0 (map f p) = (f : (a : R) → S) (eval 0 p)

Tactic:
simp [← coeff_zero_eq_eval_zero]

Premises used: Polynomial.coeff_zero_eq_eval_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
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:
simp only [hp, hq, Polynomial.map_add, map_add, eval_add]

Premises used: Polynomial.map_add, map_add, Polynomial.eval_add
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
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:
simp only [one_pow, mul_one, eval_monomial, map_monomial]

Premises used: one_pow, Polynomial.map_monomial, mul_one, Polynomial.eval_monomial
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
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))
monomial :
  ∀ (n : ℕ) (r : R),
    eval 1 (map f ((Polynomial.monomial n : (a : R) → R[X]) r)) =
      (f : (a : R) → S) (eval 1 ((Polynomial.monomial n : (a : R) → R[X]) r))
⊢ eval 1 (map f p) = (f : (a : R) → S) (eval 1 p)

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]

Premises used: one_pow, Polynomial.map_monomial, Polynomial.map_add, map_add, Polynomial.monomial, Polynomial.eval_add, mul_one, Polynomial.eval_monomial
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
n : ℕ
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:
simp only [hp, hq, Polynomial.map_add, map_add, eval_add]

Premises used: Polynomial.map_add, map_add, Polynomial.eval_add
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
n_1 n : ℕ
r : R
⊢ eval (↑n_1 : S) (map f ((monomial n : (a : R) → R[X]) r)) =
    (f : (a : R) → S) (eval (↑n_1 : R) ((monomial n : (a : R) → R[X]) r))

Tactic:
simp only [map_natCast f, eval_monomial, map_monomial, f.map_pow, f.map_mul]

Premises used: Polynomial.map_monomial, map_natCast, RingHom.map_mul, Polynomial.eval_monomial, RingHom.map_pow
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
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))
monomial :
  ∀ (n_1 : ℕ) (r : R),
    eval (↑n : S) (map f ((Polynomial.monomial n_1 : (a : R) → R[X]) r)) =
      (f : (a : R) → S) (eval (↑n : R) ((Polynomial.monomial n_1 : (a : R) → R[X]) r))
⊢ eval (↑n : S) (map f p) = (f : (a : R) → S) (eval (↑n : R) p)

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]

Premises used: Polynomial.map_monomial, Polynomial.map_add, map_add, Polynomial.monomial, map_natCast, Polynomial.eval_add, RingHom.map_mul, Polynomial.eval_monomial, RingHom.map_pow
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
i : ℤ
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:
simp only [hp, hq, Polynomial.map_add, map_add, eval_add]

Premises used: Polynomial.map_add, map_add, Polynomial.eval_add
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
i : ℤ
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:
simp only [map_intCast, eval_monomial, map_monomial, map_pow, map_mul]

Premises used: Polynomial.map_monomial, map_intCast, map_pow, map_mul, Polynomial.eval_monomial
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
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))
monomial :
  ∀ (n : ℕ) (r : R),
    eval (↑i : S) (map f ((Polynomial.monomial n : (a : R) → R[X]) r)) =
      (f : (a : R) → S) (eval (↑i : R) ((Polynomial.monomial n : (a : R) → R[X]) r))
⊢ eval (↑i : S) (map f p) = (f : (a : R) → S) (eval (↑i : R) p)

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]

Premises used: Polynomial.map_monomial, map_intCast, Polynomial.map_add, map_add, Polynomial.monomial, map_pow, map_mul, Polynomial.eval_add, Polynomial.eval_monomial
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
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)
rw₂ rw₃ : Eq.{w + 1} (α := T) ((g : (a : S) → T) (eval₂ f x p) : T) ((g : (a : S) → T) (eval₂ f x p) : T)
⊢ (g : (a : S) → T) (eval₂ f x p) = eval₂ (g.comp f) ((g : (a : S) → T) x) p

Tactic:
rw [← eval₂_map, eval₂_at_apply, eval_map]

Premises used: Polynomial.eval_map, Polynomial.eval₂_map, Polynomial.eval₂_at_apply
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
x : R
⊢ eval₂ f ((f : (a : R) → S) x) p = (f : (a : R) → S) (eval x p)

Tactic:
RingHom.comp_id f ▸ (hom_eval₂ p (RingHom.id R) f x).symm

Premises used: Polynomial.hom_eval₂, Eq.rec, RingHom.comp_id, Eq.symm, RingHom.id
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
⊢ Eq (α := ℕ[X] →+* ℕ) (evalRingHom 0) constantCoeff

Tactic:
DFunLike.ext _ _ fun p => p.coeff_zero_eq_eval_zero.symm

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
x : ℕ
contrapose : x ∉ p.support → x ∉ (map f p).support
⊢ x ∈ (map f p).support → x ∈ p.support

Tactic:
contrapose
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
x : ℕ
⊢ x ∉ p.support → x ∉ (map f p).support

Tactic:
simp +contextual
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
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
simp_rw₄ : ∀ (a : ℕ), True
⊢ (map f p).support = p.support

Tactic:
simp_rw [Finset.ext_iff, mem_support_iff, coeff_map, ← map_zero f, hf.ne_iff,
    forall_const]

Premises used: Polynomial.coeff_map, map_zero, Polynomial.mem_support_iff, Function.Injective.ne_iff, Finset.ext_iff, forall_const
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
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)
rw₄ rw₅ : Eq.{v + 1} (α := S) 0 0
⊢ (Polynomial.map f p).IsRoot ((f : (a : R) → S) x)

Tactic:
rw [IsRoot, eval_map, eval₂_hom, h.eq_zero, f.map_zero]

Premises used: Polynomial.eval_map, Polynomial.eval₂_hom, Polynomial.IsRoot, RingHom.map_zero, Polynomial.IsRoot.eq_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
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
rwa₃ rwa₄ rwa₅ rwa₆ : Eq.{v + 1} (α := S) (eval ((f : (a : R) → S) x) (Polynomial.map f p) : S) (0 : S)
⊢ p.IsRoot x

Tactic:
rwa [IsRoot, ← (injective_iff_map_eq_zero' f).mp hf, ← eval₂_hom, ← eval_map]

Premises used: Polynomial.eval_map, Polynomial.eval₂_hom, Polynomial.IsRoot, injective_iff_map_eq_zero', Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Eval.Coeff
Goal:
S : Type v
inst : CommSemiring S
R : Type u_1
inst_1 : CommRing R
f : R →+* S
x : R
p : R[X]
hf : Function.Injective.{u_1 + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ (map f p).IsRoot ((f : (a : R) → S) x) ↔ p.IsRoot x

Tactic:
⟨fun h => h.of_map hf, fun h => h.map⟩

Premises used: Polynomial.IsRoot.of_map, Iff.intro, Polynomial.IsRoot.map
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
x : S
rw 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))
⊢ eval₂ f x p = p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((f : (a : R) → S) a : S) (x ^ e)

Tactic:
rw [eval₂_def]

Premises used: Polynomial.eval₂_def
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
s : S
φ : R[X]
⊢ eval₂ f s φ = eval₂ f s φ

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x 0 = 0

Tactic:
simp [eval₂_eq_sum]

Premises used: Polynomial.eval₂_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
a : R
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x ((C : (a : R) → R[X]) a) = (f : (a : R) → S) a

Tactic:
simp [eval₂_eq_sum]

Premises used: Polynomial.eval₂_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x X = x

Tactic:
simp [eval₂_eq_sum]

Premises used: Polynomial.eval₂_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : S
n : ℕ
r : R
⊢ eval₂ f x ((monomial n : (a : R) → R[X]) r) = HMul.hMul (α := S) ((f : (a : R) → S) r : S) (x ^ n)

Tactic:
simp [eval₂_eq_sum]

Premises used: Polynomial.eval₂_eq_sum