awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
f : R[X]
G : Type u_3
inst_3 : Monoid G
inst_4 : MulSemiringAction G A
inst_5 : SMulCommClass G R A
g : G
x : A
rw :
  ((aeval ((MulSemiringAction.toAlgHom R A g : (a : A) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A) f =
    HSMul.hSMul (β := A) g ((aeval x : (a : R[X]) → A) f : A)
rw₁ :
  (MulSemiringAction.toAlgHom R A g : (a : A) → A) ((aeval x : (a : R[X]) → A) f : A) =
    HSMul.hSMul (β := A) g ((aeval x : (a : R[X]) → A) f : A)
rw₂ rw₃ :
  HSMul.hSMul (β := A) g ((aeval x : (a : R[X]) → A) f : A) = HSMul.hSMul (β := A) g ((aeval x : (a : R[X]) → A) f : A)
⊢ (aeval (g • x) : (a : R[X]) → A) f = HSMul.hSMul (β := A) g ((aeval x : (a : R[X]) → A) f : A)

Tactic:
rw [← MulSemiringAction.toAlgHom_apply R, aeval_algHom_apply, MulSemiringAction.toAlgHom_apply]

Premises used: MulSemiringAction.toAlgHom_apply, Polynomial.aeval_algHom_apply
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p : R[X]
x : A
S : Subalgebra R A
h : x ∈ S
⊢ Eq.{z + 1} (α := A) ((↑((aeval (Subtype.mk (p := fun (x : A) ↦ x ∈ S) x h) : (a : R[X]) → ↥S) p) : A) : A)
    ((aeval x : (a : R[X]) → A) p : A)

Tactic:
(aeval_algHom_apply S.val (⟨x, h⟩ : S) p).symm

Premises used: Subalgebra.val, Subtype.mk, Polynomial.aeval_algHom_apply, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
A : Type z
B : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A ≃ₐ[R] B
x : A
⊢ aeval ((f : (a : A) → B) x) = (↑f : A →ₐ[R] B).comp (aeval x)

Tactic:
aeval_algHom (f : A →ₐ[R] B) x

Premises used: AlgEquiv.toAlgHom, Polynomial.aeval_algHom
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : R
p : R[X]
⊢ Eq.{z + 1} (α := A) (((aeval ((algebraMap R A : (a : R) → A) x) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A)
    ((algebraMap R A : (a : R) → A) (eval x p) : A)

Tactic:
aeval_algHom_apply (Algebra.ofId R A) x p

Premises used: Polynomial.eval, MonoidHomClass.toMonoidHom, Algebra.ofId, RingHomClass.toRingHom, Polynomial.aeval_algHom_apply
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
A : Type z
B : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A × B
⊢ Eq (α := R[X] →ₐ[R] A × B) (aeval x) (AlgHom.prod (aeval x.1) (aeval x.2))

Tactic:
aeval_algHom (.fst R A B) x ▸ aeval_algHom (.snd R A B) x ▸
    (aeval x).prod_comp (.fst R A B) (.snd R A B)

Premises used: AlgHom.snd, Eq.rec, Polynomial.aeval, Eq.symm, Polynomial.aeval_algHom, AlgHom.prod_comp, AlgHom.fst
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
A : Type z
B : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A × B
p : R[X]
⊢ Eq (α := A × B) ((aeval x : (a : R[X]) → A × B) p : A × B)
    (((aeval x.1 : (a : R[X]) → A) p, (aeval x.2 : (a : R[X]) → B) p) : A × B)

Tactic:
simp [aeval_prod]

Premises used: Polynomial.aeval_prod
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
I : Type u_3
A : I → Type u_4
inst_1 : (i : I) → Semiring (A i)
inst_2 : (i : I) → Algebra.{u, u_4} R (A i)
x : (i : I) → A i
⊢ Eq (α := R[X] →ₐ[R] (i : I) → A i) (aeval x) (Pi.algHom R A fun (i : I) ↦ aeval (x i))

Tactic:
(funext fun i ↦ aeval_algHom (Pi.evalAlgHom R A i) x) ▸
    (Pi.algHom_comp R A (Pi.evalAlgHom R A) (aeval x))

Premises used: Pi.algHom_comp, Eq.rec, funext, Pi.evalAlgHom, Polynomial.aeval, Eq.symm, Polynomial.aeval_algHom
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
I : Type u_3
A : I → Type u_4
inst_1 : (i : I) → Semiring (A i)
inst_2 : (i : I) → Algebra.{u, u_4} R (A i)
x : (i : I) → A i
p : R[X]
j : I
⊢ Eq.{u_4 + 1} (α := A j) ((aeval x : (a : R[X]) → (i : I) → A i) p j : A j) ((aeval (x j) : (a : R[X]) → A j) p : A j)

Tactic:
aeval_pi (R := R) x ▸ Pi.algHom_apply R A (fun i ↦ aeval (x i)) p j

Premises used: Eq.rec, Pi.algHom_apply, Polynomial.aeval_pi, Polynomial.aeval, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
I : Type u_3
A : I → Type u_4
inst_1 : (i : I) → Semiring (A i)
inst_2 : (i : I) → Algebra.{u, u_4} R (A i)
x : (i : I) → A i
p : R[X]
⊢ Eq (α := (i : I) → A i) ((aeval x : (a : R[X]) → (i : I) → A i) p : (i : I) → A i) fun (j : I) ↦
    ((aeval (x j) : (a : R[X]) → A j) p : A j)

Tactic:
funext fun j ↦ aeval_pi_apply₂ x p j

Premises used: funext, Polynomial.aeval_pi_apply₂
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
r : R
⊢ Eq (α := (a : R[X]) → R) (⇑(aeval r) : (a : R[X]) → R) (eval r)

Tactic:
rfl

Premises used: Polynomial.eval, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
x : R
⊢ (↑(aeval x) : R[X] →+* R) = evalRingHom x

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, Polynomial.eval₂RingHom, RingHomClass.toRingHom, Polynomial.evalRingHom, rfl
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
X : Type u_3
g : R[X]
f : X → R
x : X
⊢ Eq.{u + 1} (α := R) ((aeval f : (a : R[X]) → X → R) g x : R) ((aeval (f x) : (a : R[X]) → R) g : R)

Tactic:
(aeval_algHom_apply (Pi.evalAlgHom R (fun _ => R) x) f g).symm

Premises used: Pi.evalAlgHom, Polynomial.aeval_algHom_apply, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
g : R[X]
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
s : Subalgebra R A
f : ↥s
⊢ Eq.{u_3 + 1} (α := A) ((↑((aeval f : (a : R[X]) → ↥s) g) : A) : A) ((aeval (↑f : A) : (a : R[X]) → A) g : A)

Tactic:
(aeval_algHom_apply s.val f g).symm

Premises used: Subalgebra.val, Polynomial.aeval_algHom_apply, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
⊢ p.coeff 0 = (aeval 0 : (a : R[X]) → R) p

Tactic:
simp [coeff_zero_eq_eval_zero]

Premises used: Polynomial.coeff_zero_eq_eval_zero
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p : R[X]
⊢ Eq.{z + 1} (α := A) ((algebraMap R A : (a : R) → A) (p.coeff 0) : A) ((aeval 0 : (a : R[X]) → A) p : A)

Tactic:
simp [aeval_def]

Premises used: Polynomial.aeval_def
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
S : Type u_3
T : Type u_4
U : Type u_5
inst_1 : Semiring S
inst_2 : CommSemiring T
inst_3 : Semiring U
inst_4 : Algebra R S
inst_5 : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = ψ.comp (algebraMap R S)
p : R[X]
a : S
rw : (eval ((ψ : (a : S) → U) a) (map (algebraMap T U) (map φ p)) : U)
| (((aeval ((ψ : (a : S) → U) a) : T[X] →ₐ[T] U) : (a : T[X]) → U) (map φ p) : U)

Tactic:
rw [← eval_map_algebraMap]

Premises used: Polynomial.eval_map_algebraMap
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
S : Type u_3
T : Type u_4
U : Type u_5
inst_1 : Semiring S
inst_2 : CommSemiring T
inst_3 : Semiring U
inst_4 : Algebra R S
inst_5 : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = ψ.comp (algebraMap R S)
p : R[X]
a : S
conv_rhs :
  Eq.{u_5 + 1} (α := U) ((ψ : (a : S) → U) ((aeval a : (a : R[X]) → S) p : S) : U)
    (eval ((ψ : (a : S) → U) a) (map (algebraMap T U) (map φ p)) : U)
⊢ Eq.{u_5 + 1} (α := U) ((ψ : (a : S) → U) ((aeval a : (a : R[X]) → S) p : S) : U)
    (((aeval ((ψ : (a : S) → U) a) : T[X] →ₐ[T] U) : (a : T[X]) → U) (map φ p) : U)

Tactic:
conv_rhs => rw [← eval_map_algebraMap]

Premises used: Polynomial.eval_map_algebraMap
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
S : Type u_3
T : Type u_4
U : Type u_5
inst_1 : Semiring S
inst_2 : CommSemiring T
inst_3 : Semiring U
inst_4 : Algebra R S
inst_5 : Algebra T U
φ : R →+* T
ψ : S →+* U
h : RingHom.comp (algebraMap T U) φ = ψ.comp (algebraMap R S)
p : R[X]
a : S
rw :
  Eq.{u_5 + 1} (α := U) ((ψ : (a : S) → U) ((aeval a : (a : R[X]) → S) p : S) : U)
    (eval ((ψ : (a : S) → U) a) (map (RingHom.comp (algebraMap T U) φ) p) : U)
rw₁ :
  Eq.{u_5 + 1} (α := U) ((ψ : (a : S) → U) ((aeval a : (a : R[X]) → S) p : S) : U)
    (eval ((ψ : (a : S) → U) a) (map (ψ.comp (algebraMap R S)) p) : U)
rw₂ :
  Eq.{u_5 + 1} (α := U) ((ψ : (a : S) → U) ((aeval a : (a : R[X]) → S) p : S) : U)
    (eval ((ψ : (a : S) → U) a) (map ψ (map (algebraMap R S) p)) : U)
rw₃ : (ψ : (a : S) → U) ((aeval a : (a : R[X]) → S) p : S) = eval₂ ψ ((ψ : (a : S) → U) a) (map (algebraMap R S) p)
rw₄ :
  Eq.{u_5 + 1} (α := U) ((ψ : (a : S) → U) ((aeval a : (a : R[X]) → S) p : S) : U)
    ((ψ : (a : S) → U) (eval a (map (algebraMap R S) p)) : U)
rw₅ :
  Eq.{u_5 + 1} (α := U) ((ψ : (a : S) → U) (eval₂ (algebraMap R S) a p) : U)
    ((ψ : (a : S) → U) (eval a (map (algebraMap R S) p)) : U)
rw₆ rw₇ :
  Eq.{u_5 + 1} (α := U) ((ψ : (a : S) → U) (eval₂ (algebraMap R S) a p) : U)
    ((ψ : (a : S) → U) (eval₂ (algebraMap R S) a p) : U)
⊢ Eq.{u_5 + 1} (α := U) ((ψ : (a : S) → U) ((aeval a : (a : R[X]) → S) p : S) : U)
    (eval ((ψ : (a : S) → U) a) (map (algebraMap T U) (map φ p)) : U)

Tactic:
rw [map_map, h, ← map_map, eval_map, eval₂_at_apply, aeval_def, eval_map]

Premises used: Polynomial.eval_map, Polynomial.aeval_def, Polynomial.eval₂_at_apply, Polynomial.map_map
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
T : Type w
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : CommSemiring T
inst_3 : Algebra R S
inst_4 : Algebra T S
φ : R →+* T
h : Eq (α := R →+* S) (RingHom.comp (algebraMap T S) φ) (algebraMap R S)
p : R[X]
a : S
rwa rwa₁ rwa₂ rwa₃ : Eq (α := R →+* S) (RingHom.comp (algebraMap T S) φ) (algebraMap R S)
⊢ Eq (α := R →+* S) (RingHom.comp (algebraMap T S) φ) (RingHom.comp (RingHom.id S) (algebraMap R S))

Tactic:
rwa [RingHom.id_comp]

Premises used: RingHom.id_comp
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
T : Type w
inst : CommSemiring S
inst_1 : CommSemiring T
inst_2 : Algebra S T
p q : S[X]
h₁ : p ∣ q
a : T
h₂ : Eq.{w + 1} (α := T) ((aeval a : (a : S[X]) → T) p : T) (0 : T)
rw : ∀ (h₂ : eval a (map (algebraMap S T) p) = 0), eval a (map (algebraMap S T) q) = 0
⊢ Eq.{w + 1} (α := T) ((aeval a : (a : S[X]) → T) q : T) (0 : T)

Tactic:
rw [← eval_map_algebraMap] at h₂ ⊢

Premises used: Polynomial.eval_map_algebraMap
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
T : Type w
inst : CommSemiring S
inst_1 : CommSemiring T
inst_2 : Algebra S T
p q : S[X]
h₁ : p ∣ q
a : T
h₂ : eval a (map (algebraMap S T) p) = 0
⊢ eval a (map (algebraMap S T) q) = 0

Tactic:
eval_eq_zero_of_dvd_of_eval_eq_zero (Polynomial.map_dvd (algebraMap S T) h₁) h₂

Premises used: Polynomial.eval_eq_zero_of_dvd_of_eval_eq_zero, Algebra.algebraMap, Polynomial.map_dvd
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
T : Type w
inst : CommSemiring S
inst_1 : CommSemiring T
inst_2 : Algebra S T
p q : S[X]
h₁ : p ∣ q
a : T
h₂ : eval a (map (algebraMap S T) p) = 0
⊢ eval a (map (algebraMap S T) q) = 0

Tactic:
exact eval_eq_zero_of_dvd_of_eval_eq_zero (Polynomial.map_dvd (algebraMap S T) h₁) h₂

Premises used: Polynomial.eval_eq_zero_of_dvd_of_eval_eq_zero, Algebra.algebraMap, Polynomial.map_dvd
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
p : R[X]
x : S
simp_rw :
  Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S)
    (∑ x_1 ∈ range (p.natDegree + 1), HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (p.coeff x_1) : S) (x ^ x_1) :
      S)
⊢ Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (∑ i ∈ range (p.natDegree + 1), p.coeff i • x ^ i : S)

Tactic:
simp_rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
p : R[X]
x : S
⊢ Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S)
    (∑ x_1 ∈ range (p.natDegree + 1), HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (p.coeff x_1) : S) (x ^ x_1) :
      S)

Tactic:
eval₂_eq_sum_range (algebraMap R S) x

Premises used: Algebra.algebraMap, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Polynomial.eval₂_eq_sum_range
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
p : R[X]
x : S
⊢ Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S)
    (∑ x_1 ∈ range (p.natDegree + 1), HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (p.coeff x_1) : S) (x ^ x_1) :
      S)

Tactic:
exact eval₂_eq_sum_range (algebraMap R S) x

Premises used: Algebra.algebraMap, Polynomial.eval₂_eq_sum_range
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
simp_rw :
  Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S)
    (∑ x_1 ∈ range n, HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (p.coeff x_1) : S) (x ^ x_1) : S)
⊢ Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (∑ i ∈ range n, p.coeff i • x ^ i : S)

Tactic:
simp_rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
⊢ Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S)
    (∑ x_1 ∈ range n, HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (p.coeff x_1) : S) (x ^ x_1) : S)

Tactic:
eval₂_eq_sum_range' (algebraMap R S) hn x

Premises used: Algebra.algebraMap, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Polynomial.eval₂_eq_sum_range'
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
⊢ Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S)
    (∑ x_1 ∈ range n, HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (p.coeff x_1) : S) (x ^ x_1) : S)

Tactic:
exact eval₂_eq_sum_range' (algebraMap R S) hn x

Premises used: Algebra.algebraMap, Polynomial.eval₂_eq_sum_range'
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
inst : CommSemiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
r : R
h : eval₂ f ((f : (a : R) → S) r) p = 0
a : Eq.{v + 1} (α := S) ((f : (a : R) → S) (eval r p) : S) ((f : (a : R) → S) 0 : S)
⊢ p.IsRoot r

Tactic:
apply hf
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
inst : CommSemiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
r : R
h : eval₂ f ((f : (a : R) → S) r) p = 0
a : eval₂ f ((f : (a : R) → S) r) p = (f : (a : R) → S) 0
a₁ : Eq.{v + 1} (α := S) (0 : S) ((f : (a : R) → S) 0 : S)
a₂ a₃ : Eq.{v + 1} (α := S) 0 0
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (eval r p) : S) ((f : (a : R) → S) 0 : S)

Tactic:
rw [← eval₂_hom, h, f.map_zero]

Premises used: Polynomial.eval₂_hom, RingHom.map_zero
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
p : R[X]
r : R
hr : Eq.{v + 1} (α := S) (((aeval ((algebraMap R S : (a : R) → S) r) : R[X] →ₐ[R] S) : (a : R[X]) → S) p : S) (0 : S)
⊢ p.IsRoot r

Tactic:
isRoot_of_eval₂_map_eq_zero (FaithfulSMul.algebraMap_injective _ _) hr

Premises used: FaithfulSMul.algebraMap_injective, Polynomial.isRoot_of_eval₂_map_eq_zero
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
A' : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring A'
inst_2 : CommSemiring S
inst_3 : Algebra S R
inst_4 : Algebra S A'
g : R →ₐ[S] A'
y : A'
⊢ (aevalTower g y : (a : R[X]) → A') X = y

Tactic:
eval₂_X _ _

Premises used: Polynomial.eval₂_X
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
A' : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring A'
inst_2 : CommSemiring S
inst_3 : Algebra S R
inst_4 : Algebra S A'
g : R →ₐ[S] A'
y : A'
x : R
⊢ Eq.{u_1 + 1} (α := A') ((aevalTower g y : (a : R[X]) → A') ((C : (a : R) → R[X]) x : R[X]) : A')
    ((g : (a : R) → A') x : A')

Tactic:
eval₂_C _ _

Premises used: Polynomial.eval₂_C
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
A' : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring A'
inst_2 : CommSemiring S
inst_3 : Algebra S R
inst_4 : Algebra S A'
g : R →ₐ[S] A'
y : A'
⊢ Eq (α := R →+* A') (RingHom.comp (↑(aevalTower g y) : R[X] →+* A') C) (↑g : R →+* A')

Tactic:
RingHom.ext <| aevalTower_C _ _

Premises used: Polynomial.aevalTower_C, RingHom.ext
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
A' : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring A'
inst_2 : CommSemiring S
inst_3 : Algebra S R
inst_4 : Algebra S A'
g : R →ₐ[S] A'
y : A'
x : R
⊢ Eq.{u_1 + 1} (α := A') ((aevalTower g y : (a : R[X]) → A') ((algebraMap R R[X] : (a : R) → R[X]) x : R[X]) : A')
    ((g : (a : R) → A') x : A')

Tactic:
eval₂_C _ _

Premises used: Polynomial.eval₂_C
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
A' : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring A'
inst_2 : CommSemiring S
inst_3 : Algebra S R
inst_4 : Algebra S A'
g : R →ₐ[S] A'
y : A'
⊢ Eq (α := R →+* A')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(aevalTower g y) : R[X] →+* A') (algebraMap R R[X]))
    (↑g : R →+* A')

Tactic:
aevalTower_comp_C _ _

Premises used: Polynomial.C, Polynomial.aevalTower_comp_C
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
A' : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring A'
inst_2 : CommSemiring S
inst_3 : Algebra S R
inst_4 : Algebra S A'
g : R →ₐ[S] A'
y : A'
x : R
⊢ Eq.{u_1 + 1} (α := A')
    ((aevalTower g y : (a : R[X]) → A') ((IsScalarTower.toAlgHom S R R[X] : (a : R) → R[X]) x : R[X]) : A')
    ((g : (a : R) → A') x : A')

Tactic:
aevalTower_algebraMap _ _ _

Premises used: Polynomial.aevalTower_algebraMap
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
A' : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring A'
inst_2 : CommSemiring S
inst_3 : Algebra S R
inst_4 : Algebra S A'
g : R →ₐ[S] A'
y : A'
⊢ (aevalTower g y).comp (IsScalarTower.toAlgHom S R R[X]) = g

Tactic:
AlgHom.coe_ringHom_injective <| aevalTower_comp_algebraMap _ _

Premises used: AlgHom.coe_ringHom_injective, Polynomial.aevalTower_comp_algebraMap
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
inst : CommSemiring S
h : ∀ (s : S), Eq (α := S) ((aevalTower (AlgHom.id S S) s : (a : S[X]) → S) X : S) ((aeval s : (a : S[X]) → S) X : S)
⊢ Eq (α := (x : S) → S[X] →ₐ[S] S) (aevalTower (AlgHom.id S S)) aeval

Tactic:
ext s
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
inst : CommSemiring S
s : S
⊢ Eq (α := S) ((aevalTower (AlgHom.id S S) s : (a : S[X]) → S) X : S) ((aeval s : (a : S[X]) → S) X : S)

Tactic:
simp only [eval_X, aevalTower_X, coe_aeval_eq_eval]

Premises used: Polynomial.eval_X, Polynomial.aevalTower_X, Polynomial.coe_aeval_eq_eval
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
A' : Type u_1
inst : CommSemiring A'
inst_1 : CommSemiring S
inst_2 : Algebra S A'
h :
  ∀ (x : A'),
    Eq.{u_1 + 1} (α := A') ((aevalTower (Algebra.ofId S A') x : (a : S[X]) → A') X : A')
      ((aeval x : (a : S[X]) → A') X : A')
⊢ Eq (α := (x : A') → S[X] →ₐ[S] A') (aevalTower (Algebra.ofId S A')) aeval

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
A' : Type u_1
inst : CommSemiring A'
inst_1 : CommSemiring S
inst_2 : Algebra S A'
x : A'
⊢ Eq.{u_1 + 1} (α := A') ((aevalTower (Algebra.ofId S A') x : (a : S[X]) → A') X : A')
    ((aeval x : (a : S[X]) → A') X : A')

Tactic:
simp only [aeval_X, aevalTower_X]

Premises used: Polynomial.aevalTower_X, Polynomial.aeval_X
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
k : ℕ
⊢ HSMul.hSMul (β := TensorProduct.{u, v, u_3} R S[X] N) (HPow.hPow (α := S[X]) X k)
      ((rTensor N
            ((↑R :
                {S M M₂ : Type v} →
                  [inst : Semiring R] →
                    [inst_5 : Semiring S] →
                      [inst_6 : AddCommMonoid M] →
                        [inst_7 : AddCommMonoid M₂] →
                          [inst_8 : Module R M] →
                            [inst_9 : Module R M₂] →
                              [inst_10 : Module S M] →
                                [inst_11 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (monomial 0)) :
          (a : S ⊗[R] N) → S[X] ⊗[R] N)
        0) =
    (rTensor N
          ((↑R :
              {S M M₂ : Type v} →
                [inst : Semiring R] →
                  [inst_5 : Semiring S] →
                    [inst_6 : AddCommMonoid M] →
                      [inst_7 : AddCommMonoid M₂] →
                        [inst_8 : Module R M] →
                          [inst_9 : Module R M₂] →
                            [inst_10 : Module S M] →
                              [inst_11 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (monomial k)) :
        (a : S ⊗[R] N) → S[X] ⊗[R] N)
      0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
k : ℕ
s : S
n : N
tmul :
  HSMul.hSMul (β := TensorProduct.{u, v, u_3} R S[X] N) (HPow.hPow (α := S[X]) X k)
      ((C : (a : S) → S[X]) s ⊗ₜ[R] n : TensorProduct.{u, v, u_3} R S[X] N) =
    (monomial k : (a : S) → S[X]) s ⊗ₜ[R] n
⊢ HSMul.hSMul (β := TensorProduct.{u, v, u_3} R S[X] N) (HPow.hPow (α := S[X]) X k)
      ((rTensor N
              ((↑R :
                  {S M M₂ : Type v} →
                    [inst : Semiring R] →
                      [inst_5 : Semiring S] →
                        [inst_6 : AddCommMonoid M] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R M] →
                              [inst_9 : Module R M₂] →
                                [inst_10 : Module S M] →
                                  [inst_11 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (monomial 0)) :
            (a : S ⊗[R] N) → S[X] ⊗[R] N)
          (s ⊗ₜ[R] n) :
        TensorProduct.{u, v, u_3} R S[X] N) =
    (rTensor N
          ((↑R :
              {S M M₂ : Type v} →
                [inst : Semiring R] →
                  [inst_5 : Semiring S] →
                    [inst_6 : AddCommMonoid M] →
                      [inst_7 : AddCommMonoid M₂] →
                        [inst_8 : Module R M] →
                          [inst_9 : Module R M₂] →
                            [inst_10 : Module S M] →
                              [inst_11 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (monomial k)) :
        (a : S ⊗[R] N) → S[X] ⊗[R] N)
      (s ⊗ₜ[R] n)

Tactic:
simp only [rTensor_tmul, coe_restrictScalars, monomial_zero_left]

Premises used: LinearMap.rTensor_tmul, LinearMap.coe_restrictScalars, Polynomial.monomial_zero_left