awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
p q r : R[X]
inst_5 : Nontrivial A
x : R
⊢ ¬Eq.{z + 1} (α := A) (coeff ((C : (a : A) → A[X]) ((algebraMap R A : (a : R) → A) x)) 1) (coeff X 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
p : R[X]
f : A →ₐ[R] B
a : A
simp :
  Eq.{u_5 + 1} (α := B)
    ((f : (a : A) → B) (∑ n ∈ p.support, HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) (p.coeff n) : A) (a ^ n)) :
      B)
    (∑ n ∈ p.support,
        HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) (p.coeff n) : B)
          (HPow.hPow (α := B) ((f : (a : A) → B) a : B) n) :
      B)
⊢ (f : (a : A) → B) (eval₂ (algebraMap R A) a p) = eval₂ (algebraMap R B) ((f : (a : A) → B) a) p

Tactic:
simp only [eval₂_eq_sum, sum_def]

Premises used: Polynomial.sum_def, Polynomial.eval₂_eq_sum
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
p : R[X]
f : A →ₐ[R] B
a : A
⊢ Eq.{u_5 + 1} (α := B)
    ((f : (a : A) → B) (∑ n ∈ p.support, HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) (p.coeff n) : A) (a ^ n)) :
      B)
    (∑ n ∈ p.support,
        HMul.hMul (α := B) ((algebraMap R B : (a : R) → B) (p.coeff n) : B)
          (HPow.hPow (α := B) ((f : (a : A) → B) a : B) n) :
      B)

Tactic:
simp only [map_sum, map_mul, map_pow, AlgHom.commutes]

Premises used: map_pow, map_sum, map_mul, AlgHom.commutes
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
rw :
  ((f : (a : R[X]) → A)
      (p.sum fun (n : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) :
    A)
| ((f : (a : R[X]) → A) p : A)

Tactic:
rw [← Polynomial.sum_C_mul_X_pow_eq p]

Premises used: Polynomial.sum_C_mul_X_pow_eq
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
conv_rhs :
  eval₂ (algebraMap R A) ((f : (a : R[X]) → A) X) p =
    (f : (a : R[X]) → A)
      (p.sum fun (n : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ eval₂ (algebraMap R A) ((f : (a : R[X]) → A) X) p = (f : (a : R[X]) → A) p

Tactic:
conv_rhs => rw [← Polynomial.sum_C_mul_X_pow_eq p]

Premises used: Polynomial.sum_C_mul_X_pow_eq
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
simp :
  Eq.{u_4 + 1} (α := A)
    (∑ n ∈ p.support,
        HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) (p.coeff n) : A)
          (HPow.hPow (α := A) ((f : (a : R[X]) → A) X : A) n) :
      A)
    ((f : (a : R[X]) → A)
        (∑ n ∈ p.support, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n)) :
      A)
⊢ eval₂ (algebraMap R A) ((f : (a : R[X]) → A) X) p =
    (f : (a : R[X]) → A)
      (p.sum fun (n : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))

Tactic:
simp only [eval₂_eq_sum, sum_def]

Premises used: Polynomial.sum_def, Polynomial.eval₂_eq_sum
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
simp :
  Eq.{u_4 + 1} (α := A)
    (∑ n ∈ p.support,
      HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) (p.coeff n) : A)
        (HPow.hPow (α := A) ((f : (a : R[X]) → A) X : A) n))
    (∑ x ∈ p.support,
      HMul.hMul (α := A) ((f : (a : R[X]) → A) ((C : (a : R) → R[X]) (p.coeff x) : R[X]) : A)
        (HPow.hPow (α := A) ((f : (a : R[X]) → A) X : A) x))
⊢ Eq.{u_4 + 1} (α := A)
    (∑ n ∈ p.support,
        HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) (p.coeff n) : A)
          (HPow.hPow (α := A) ((f : (a : R[X]) → A) X : A) n) :
      A)
    ((f : (a : R[X]) → A)
        (∑ n ∈ p.support, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n)) :
      A)

Tactic:
simp only [map_sum, map_mul, map_pow]

Premises used: map_pow, map_sum, map_mul
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
⊢ Eq.{u_4 + 1} (α := A)
    (∑ n ∈ p.support,
      HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) (p.coeff n) : A)
        (HPow.hPow (α := A) ((f : (a : R[X]) → A) X : A) n))
    (∑ x ∈ p.support,
      HMul.hMul (α := A) ((f : (a : R[X]) → A) ((C : (a : R) → R[X]) (p.coeff x) : R[X]) : A)
        (HPow.hPow (α := A) ((f : (a : R[X]) → A) X : A) x))

Tactic:
simp [Polynomial.C_eq_algebraMap]

Premises used: Polynomial.C_eq_algebraMap
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : Ring S
p : ℤ[X]
f : R →+* S
r : R
⊢ Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (eval₂ (Int.castRingHom R) r p) : S)
    (eval₂ (Int.castRingHom S) ((f : (a : R) → S) r) p : S)

Tactic:
algHom_eval₂_algebraMap p f.toIntAlgHom r

Premises used: RingHom.toIntAlgHom, Polynomial.algHom_eval₂_algebraMap
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u_3
inst : Ring R
p : ℤ[X]
f : ℤ[X] →+* R
⊢ Eq (α := R) (eval₂ (Int.castRingHom R) ((f : (a : ℤ[X]) → R) X) p : R) ((f : (a : ℤ[X]) → R) p : R)

Tactic:
eval₂_algebraMap_X p f.toIntAlgHom

Premises used: RingHom.toIntAlgHom, Polynomial.eval₂_algebraMap_X
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
p q r : R[X]
f : A →ₐ[R] B
⊢ ∀ (r : R),
    (↑(↑(mapRingHom f.toRingHom) : A[X] →* B[X]) : OneHom A[X] B[X]).toFun ((algebraMap R A[X] : (a : R) → A[X]) r) =
      (algebraMap R B[X] : (a : R) → B[X]) r

Tactic:
simp
-- 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
⊢ Eq (α := (a : A[X]) → B[X]) (⇑(mapAlgHom f) : (a : A[X]) → B[X]) (map (↑f : A →+* B))

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Polynomial.map, rfl
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq (α := A[X] →ₐ[R] A[X]) (mapAlgHom (AlgHom.id R A)) (AlgHom.id R A[X])

Tactic:
AlgHom.ext fun _x => map_id

Premises used: Polynomial.map_id, AlgHom.ext
-- 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
⊢ (↑(mapAlgHom f) : A[X] →+* B[X]) = mapRingHom (↑f : A →+* B)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Polynomial.mapRingHom, Polynomial.map, rfl
-- 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
C : Type u_3
inst_5 : Semiring C
inst_6 : Algebra R C
f : B →ₐ[R] C
g : A →ₐ[R] B
hC :
  ∀ (x : A) (n : ℕ),
    Eq.{u_3 + 1} (α := C) (coeff ((((mapAlgHom f).comp (mapAlgHom g)).comp CAlgHom : (a : A) → C[X]) x) n)
      (coeff (((mapAlgHom (f.comp g)).comp CAlgHom : (a : A) → C[X]) x) n)
hX :
  ∀ (n : ℕ),
    Eq.{u_3 + 1} (α := C) (coeff (((mapAlgHom f).comp (mapAlgHom g) : (a : A[X]) → C[X]) X) n)
      (coeff ((mapAlgHom (f.comp g) : (a : A[X]) → C[X]) X) n)
⊢ (mapAlgHom f).comp (mapAlgHom g) = mapAlgHom (f.comp g)

Tactic:
ext
-- 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
C : Type u_3
inst_5 : Semiring C
inst_6 : Algebra R C
f : B →ₐ[R] C
g : A →ₐ[R] B
x : A
n : ℕ
⊢ Eq.{u_3 + 1} (α := C) (coeff ((((mapAlgHom f).comp (mapAlgHom g)).comp CAlgHom : (a : A) → C[X]) x) n)
    (coeff (((mapAlgHom (f.comp g)).comp CAlgHom : (a : A) → C[X]) x) n)

Tactic:
simp
-- 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
C : Type u_3
inst_5 : Semiring C
inst_6 : Algebra R C
f : B →ₐ[R] C
g : A →ₐ[R] B
n : ℕ
⊢ Eq.{u_3 + 1} (α := C) (coeff (((mapAlgHom f).comp (mapAlgHom g) : (a : A[X]) → C[X]) X) n)
    (coeff ((mapAlgHom (f.comp g) : (a : A[X]) → C[X]) X) n)

Tactic:
simp
-- 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
⊢ mapAlgHom f = eval₂AlgHom (AlgHom.comp CAlgHom f) X ⋯

Tactic:
rfl
-- 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
p : A[X]
n : ℕ
⊢ Eq.{u_2 + 1} (α := B) (coeff ((mapAlgHom f : (a : A[X]) → B[X]) p) n : B) ((f : (a : A) → B) (p.coeff n) : B)

Tactic:
simp
-- 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
n : ℕ
h :
  ∀ (f_1 : A[X]),
    Eq.{u_2 + 1} (α := B)
      (((↑R :
                  {S M M₂ : Type u_2} →
                    [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₂)
                (lcoeff B n) ∘ₗ
              (mapAlgHom f).toLinearMap :
            (a : A[X]) → B)
          f_1 :
        B)
      ((f.toLinearMap ∘ₗ
              (↑R :
                  {S M M₂ : Type z} →
                    [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₂)
                (lcoeff A n) :
            (a : A[X]) → B)
          f_1 :
        B)
⊢ (↑R :
          {S M M₂ : Type u_2} →
            [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₂)
        (lcoeff B n) ∘ₗ
      (mapAlgHom f).toLinearMap =
    f.toLinearMap ∘ₗ
      (↑R :
          {S M M₂ : Type z} →
            [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₂)
        (lcoeff A n)

Tactic:
ext f
-- 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_1 : A →ₐ[R] B
n : ℕ
f : A[X]
⊢ Eq.{u_2 + 1} (α := B)
    (((↑R :
                {S M M₂ : Type u_2} →
                  [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₂)
              (lcoeff B n) ∘ₗ
            (mapAlgHom f_1).toLinearMap :
          (a : A[X]) → B)
        f :
      B)
    ((f_1.toLinearMap ∘ₗ
            (↑R :
                {S M M₂ : Type z} →
                  [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₂)
              (lcoeff A n) :
          (a : A[X]) → B)
        f :
      B)

Tactic:
simp
-- 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
n : ℕ
a : A
⊢ Eq (α := B[X]) ((mapAlgHom f : (a : A[X]) → B[X]) ((monomial n : (a : A) → A[X]) a) : B[X])
    ((monomial n : (a : B) → B[X]) ((f : (a : A) → B) a) : B[X])

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
p q r : R[X]
f : A ≃ₐ[R] B
⊢ (mapAlgHom (↑f : A →ₐ[R] B)).comp (mapAlgHom (↑f.symm : B →ₐ[R] A)) = AlgHom.id R B[X]

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
p q r : R[X]
f : A ≃ₐ[R] B
⊢ (mapAlgHom (↑f.symm : B →ₐ[R] A)).comp (mapAlgHom (↑f : A →ₐ[R] B)) = AlgHom.id R A[X]

Tactic:
simp
-- 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
⊢ Eq (α := (a : A[X]) → B[X]) (⇑(mapAlgEquiv f) : (a : A[X]) → B[X]) (map (↑f : A →+* B))

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Polynomial.map, rfl
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq.{z + 1} (α := A[X] ≃ₐ[R] A[X]) (mapAlgEquiv AlgEquiv.refl) AlgEquiv.refl

Tactic:
AlgEquiv.ext fun _x => map_id

Premises used: Polynomial.map_id, AlgEquiv.ext
-- 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
⊢ (↑(mapAlgEquiv f) : A[X] →+* B[X]) = mapRingHom (↑f : A →+* B)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Polynomial.mapRingHom, Polynomial.map, rfl
-- 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
⊢ (↑(mapAlgEquiv f) : A[X] →ₐ[R] B[X]) = mapAlgHom (↑f : A →ₐ[R] B)

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, Polynomial.mapAlgHom, Polynomial.mapRingHom, Polynomial.map, rfl
-- 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
C : Type u_3
inst_5 : Semiring C
inst_6 : Algebra R C
f : A ≃ₐ[R] B
g : B ≃ₐ[R] C
h :
  ∀ (a : A[X]) (n : ℕ),
    Eq.{u_3 + 1} (α := C) (coeff (((mapAlgEquiv f).trans (mapAlgEquiv g) : (a : A[X]) → C[X]) a) n)
      (coeff ((mapAlgEquiv (f.trans g) : (a : A[X]) → C[X]) a) n)
⊢ (mapAlgEquiv f).trans (mapAlgEquiv g) = mapAlgEquiv (f.trans g)

Tactic:
ext
-- 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
C : Type u_3
inst_5 : Semiring C
inst_6 : Algebra R C
f : A ≃ₐ[R] B
g : B ≃ₐ[R] C
a : A[X]
n : ℕ
⊢ Eq.{u_3 + 1} (α := C) (coeff (((mapAlgEquiv f).trans (mapAlgEquiv g) : (a : A[X]) → C[X]) a) n)
    (coeff ((mapAlgEquiv (f.trans g) : (a : A[X]) → C[X]) a) n)

Tactic:
simp
-- 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 : A
⊢ Eq (α := R[X] →ₐ[R] A) ((aevalEquiv R A : (a : A) → R[X] →ₐ[R] A) x : R[X] →ₐ[R] A) (aeval x : R[X] →ₐ[R] A)

Tactic:
rfl

Premises used: Polynomial.aeval, rfl
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
B : Type u_2
inst : CommSemiring R
inst_1 : Semiring B
inst_2 : Algebra R B
f g : R[X] →ₐ[R] B
hX : Eq.{u_2 + 1} (α := B) ((f : (a : R[X]) → B) X : B) ((g : (a : R[X]) → B) X : B)
⊢ f = g

Tactic:
algHom_ext' (Subsingleton.elim ..) hX

Premises used: Polynomial.algHom_ext', Subsingleton.elim
-- 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 : A
p : R[X]
⊢ (aeval x : (a : R[X]) → A) p = eval₂ (algebraMap R A) x p

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
B : Type u_2
inst : CommSemiring R
inst_1 : Semiring B
inst_2 : Algebra R B
P : R[X]
b : B
rw : eval b (map (algebraMap R B) P) = eval₂ (algebraMap R B) b P
rw₁ rw₂ : eval₂ (algebraMap R B) b P = eval₂ (algebraMap R B) b P
⊢ eval b (map (algebraMap R B) P) = (aeval b : (a : R[X]) → B) P

Tactic:
rw [aeval_def, eval_map]

Premises used: Polynomial.eval_map, Polynomial.aeval_def
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : Semiring S
inst_2 : Algebra R S
p : R[X]
⊢ Eq.{v + 1} (α := S[X]) (((mapAlg R S : AlgHom.{u, u, v} R R[X] S[X]) : (a : R[X]) → S[X]) p : S[X])
    (map (algebraMap R S) p : S[X])

Tactic:
rfl
-- 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 : A
⊢ Eq.{z + 1} (α := A) ((aeval x : (a : R[X]) → A) 0 : A) (0 : A)

Tactic:
map_zero (aeval x)

Premises used: map_zero, Polynomial.aeval
-- 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 : A
⊢ (aeval x : (a : R[X]) → A) X = x

Tactic:
eval₂_X _ x

Premises used: Polynomial.eval₂_X
-- 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 : A
r : R
⊢ Eq.{z + 1} (α := A) ((aeval x : (a : R[X]) → A) ((C : (a : R) → R[X]) r : R[X]) : A)
    ((algebraMap R A : (a : R) → A) r : A)

Tactic:
eval₂_C _ x

Premises used: Polynomial.eval₂_C
-- 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 : A
n : ℕ
r : R
⊢ (aeval x : (a : R[X]) → A) ((monomial n : (a : R) → R[X]) r : R[X]) =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (x ^ n)

Tactic:
eval₂_monomial _ _

Premises used: Polynomial.eval₂_monomial
-- 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 : A
n : ℕ
⊢ (aeval x : (a : R[X]) → A) (HPow.hPow (α := R[X]) X n) = x ^ n

Tactic:
eval₂_X_pow _ _

Premises used: Polynomial.eval₂_X_pow
-- 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 q : R[X]
x : A
⊢ (aeval x : (a : R[X]) → A) (p + q) =
    HAdd.hAdd (α := A) (β := A) ((aeval x : (a : R[X]) → A) p : A) ((aeval x : (a : R[X]) → A) q : A)

Tactic:
map_add _ _ _

Premises used: map_add
-- 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 : A
⊢ Eq.{z + 1} (α := A) ((aeval x : (a : R[X]) → A) 1 : A) (1 : A)

Tactic:
map_one _

Premises used: map_one
-- 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 : A
n : ℕ
⊢ Eq.{z + 1} (α := A) ((aeval x : (a : R[X]) → A) (↑n : R[X]) : A) ((↑n : A) : A)

Tactic:
map_natCast _ _

Premises used: map_natCast
-- 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 q : R[X]
x : A
⊢ (aeval x : (a : R[X]) → A) (p * q) =
    HMul.hMul (α := A) (β := A) ((aeval x : (a : R[X]) → A) p : A) ((aeval x : (a : R[X]) → A) q : A)

Tactic:
map_mul _ _ _

Premises used: map_mul
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
⊢ p.comp q = (aeval q : (a : R[X]) → R[X]) p

Tactic:
rfl

Premises used: Polynomial.C, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Polynomial.comp, rfl
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
⊢ Eq.{u_3 + 1} (α := A) ((aeval x : (a : R[X]) → A) (p.comp q) : A)
    (((aeval ((aeval x : (a : R[X]) → A) q) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A)

Tactic:
eval₂_comp' x p q

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Polynomial.eval₂_comp'
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
A : Type u_3
B : Type u_4
C : Type u_5
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra A C
inst_5 : Algebra B C
inst_6 : IsScalarTower A B C
p : A[X]
⊢ Eq.{u_5 + 1} (α := C[X]) (((mapAlg A C : AlgHom.{u_3, u_3, u_5} A A[X] C[X]) : (a : A[X]) → C[X]) p : C[X])
    (((mapAlg B C : AlgHom.{u_4, u_4, u_5} B B[X] C[X]) : (a : B[X]) → C[X])
        (((mapAlg A B : AlgHom.{u_3, u_3, u_4} A A[X] B[X]) : (a : A[X]) → B[X]) p) :
      C[X])

Tactic:
simp [mapAlg_eq_map, map_map, IsScalarTower.algebraMap_eq A B C]

Premises used: Polynomial.mapAlg_eq_map, IsScalarTower.algebraMap_eq, Polynomial.map_map