awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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) :
      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)
have 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))
Tactic: simp only [map_sum, map_mul, map_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
⊢ (mapAlgHom f).comp (mapAlgHom g) = mapAlgHom (f.comp g)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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)
⊢ (mapAlgHom f).comp (mapAlgHom g) = mapAlgHom (f.comp g)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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 : ℕ
⊢ (↑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)
have 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)
Tactic: ext f
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
⊢ (mapAlgEquiv f).trans (mapAlgEquiv g) = mapAlgEquiv (f.trans g)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
⊢ eval b (map (algebraMap R B) P) = (aeval b : (a : R[X]) → B) P
have rw : eval b (map (algebraMap R B) P) = eval₂ (algebraMap R B) b P
Tactic: rw [aeval_def, eval_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
⊢ eval b (map (algebraMap R B) P) = (aeval b : (a : R[X]) → B) P
have rw₁ : eval₂ (algebraMap R B) b P = eval₂ (algebraMap R B) b P
Tactic: rw [aeval_def, eval_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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) ((algebraMap B C : (a : B) → C) ((algebraMap A B : (a : A) → B) (p.coeff 0) : B) : C)
    (coeff (((mapAlg A C : AlgHom.{u_3, u_3, u_5} A A[X] C[X]) : (a : A[X]) → C[X]) p) 0 : C)
have rw : (algebraMap B C : (a : B) → C) ((algebraMap A B : (a : A) → B) (p.coeff 0) : B) = coeff (map (algebraMap A C) p) 0
Tactic: rw [mapAlg_eq_map, coeff_map, IsScalarTower.algebraMap_eq A B C, RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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]
rw : (algebraMap B C : (a : B) → C) ((algebraMap A B : (a : A) → B) (p.coeff 0) : B) = coeff (map (algebraMap A C) p) 0
⊢ Eq.{u_5 + 1} (α := C) ((algebraMap B C : (a : B) → C) ((algebraMap A B : (a : A) → B) (p.coeff 0) : B) : C)
    (coeff (((mapAlg A C : AlgHom.{u_3, u_3, u_5} A A[X] C[X]) : (a : A[X]) → C[X]) p) 0 : C)
have rw₁ : Eq.{u_5 + 1} (α := C) ((algebraMap B C : (a : B) → C) ((algebraMap A B : (a : A) → B) (p.coeff 0) : B) : C)
  ((algebraMap A C : (a : A) → C) (p.coeff 0) : C)
Tactic: rw [mapAlg_eq_map, coeff_map, IsScalarTower.algebraMap_eq A B C, RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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]
rw : (algebraMap B C : (a : B) → C) ((algebraMap A B : (a : A) → B) (p.coeff 0) : B) = coeff (map (algebraMap A C) p) 0
rw₁ :
  Eq.{u_5 + 1} (α := C) ((algebraMap B C : (a : B) → C) ((algebraMap A B : (a : A) → B) (p.coeff 0) : B) : C)
    ((algebraMap A C : (a : A) → C) (p.coeff 0) : C)
⊢ Eq.{u_5 + 1} (α := C) ((algebraMap B C : (a : B) → C) ((algebraMap A B : (a : A) → B) (p.coeff 0) : B) : C)
    (coeff (((mapAlg A C : AlgHom.{u_3, u_3, u_5} A A[X] C[X]) : (a : A[X]) → C[X]) p) 0 : C)
have rw₂ : Eq.{u_5 + 1} (α := C) ((algebraMap B C : (a : B) → C) ((algebraMap A B : (a : A) → B) (p.coeff 0) : B) : C)
  ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap A B) : (a : A) → C) (p.coeff 0) :
    C)
Tactic: rw [mapAlg_eq_map, coeff_map, IsScalarTower.algebraMap_eq A B C, RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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]
rw : (algebraMap B C : (a : B) → C) ((algebraMap A B : (a : A) → B) (p.coeff 0) : B) = coeff (map (algebraMap A C) p) 0
rw₁ :
  Eq.{u_5 + 1} (α := C) ((algebraMap B C : (a : B) → C) ((algebraMap A B : (a : A) → B) (p.coeff 0) : B) : C)
    ((algebraMap A C : (a : A) → C) (p.coeff 0) : C)
rw₂ :
  Eq.{u_5 + 1} (α := C) ((algebraMap B C : (a : B) → C) ((algebraMap A B : (a : A) → B) (p.coeff 0) : B) : C)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap A B) : (a : A) → C) (p.coeff 0) :
      C)
⊢ Eq.{u_5 + 1} (α := C) ((algebraMap B C : (a : B) → C) ((algebraMap A B : (a : A) → B) (p.coeff 0) : B) : C)
    (coeff (((mapAlg A C : AlgHom.{u_3, u_3, u_5} A A[X] C[X]) : (a : A[X]) → C[X]) p) 0 : C)
have rw₃ : Eq.{u_5 + 1} (α := C) ((algebraMap B C : (a : B) → C) ((algebraMap A B : (a : A) → B) (p.coeff 0) : B) : C)
  ((algebraMap B C : (a : B) → C) ((algebraMap A B : (a : A) → B) (p.coeff 0) : B) : C)
Tactic: rw [mapAlg_eq_map, coeff_map, IsScalarTower.algebraMap_eq A B C, RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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 : CommSemiring A'
inst_3 : Semiring B
inst_4 : Algebra R A
inst_5 : Algebra R B
p_1 q_1 : R[X]
x : A
p q : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
⊢ R[X] ≃ₐ[R] R[X]
have refine_1 : AlgHom.comp (aeval p) (aeval q) = AlgHom.id R R[X]
Tactic: refine AlgEquiv.ofAlgHom (aeval p) (aeval q) ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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 : CommSemiring A'
inst_3 : Semiring B
inst_4 : Algebra R A
inst_5 : Algebra R B
p_1 q_1 : R[X]
x : A
p q : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
refine_1 : AlgHom.comp (aeval p) (aeval q) = AlgHom.id R R[X]
⊢ R[X] ≃ₐ[R] R[X]
have refine_2 : AlgHom.comp (aeval q) (aeval p) = AlgHom.id R R[X]
Tactic: refine AlgEquiv.ofAlgHom (aeval p) (aeval q) ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
inst : CommSemiring R
p q p' q' : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
hpq' : p'.comp q' = X
hqp' : q'.comp p' = X
h : p = p'
⊢ p.algEquivOfCompEqX q hpq hqp = p'.algEquivOfCompEqX q' hpq' hqp'
have h₁ : ∀ (a : R[X]),
  Eq (α := R[X]) ((p.algEquivOfCompEqX q hpq hqp : (a : R[X]) → R[X]) a : R[X])
    ((p'.algEquivOfCompEqX q' hpq' hqp' : (a : R[X]) → R[X]) a : R[X])
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u_3
inst : CommRing R
a b : R
inst_1 : Invertible a
⊢ Eq (α := R[X] ≃ₐ[R] R[X]) (AlgEquiv.symm (algEquivCMulXAddC a b))
    (algEquivCMulXAddC (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _)
      (-@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b))
have h : ∀ (p : R[X]),
  Eq (α := R[X]) ((AlgEquiv.symm (algEquivCMulXAddC a b) : (a : R[X]) → R[X]) p : R[X])
    ((algEquivCMulXAddC (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _)
            (-@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b) :
          (a : R[X]) → R[X])
        p :
      R[X])
Tactic: ext p : 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u_3
inst : CommRing R
a b : R
inst_1 : Invertible a
p : R[X]
⊢ Eq (α := R[X]) ((AlgEquiv.symm (algEquivCMulXAddC a b) : (a : R[X]) → R[X]) p : R[X])
    ((algEquivCMulXAddC (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _)
            (-@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b) :
          (a : R[X]) → R[X])
        p :
      R[X])
have h : Eq (α := R[X])
  ((aeval
          (HMul.hMul (α := R[X])
            ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _) : R[X])
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))) :
        (a : R[X]) → R[X])
      p :
    R[X])
  ((aeval
          (HMul.hMul (α := R[X]) (β := R[X])
              ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _) : R[X]) X +
            -HMul.hMul (α := R[X]) (β := R[X])
                ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _) : R[X])
                ((C : (a : R) → R[X]) b : R[X])) :
        (a : R[X]) → R[X])
      p :
    R[X])
Tactic: simp only [algEquivCMulXAddC_symm_apply, neg_mul, algEquivCMulXAddC_apply, map_neg, map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u_3
inst : CommRing R
a b : R
inst_1 : Invertible a
p : R[X]
⊢ Eq (α := R[X])
    ((aeval
            (HMul.hMul (α := R[X])
              ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _) : R[X])
              (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))) :
          (a : R[X]) → R[X])
        p :
      R[X])
    ((aeval
            (HMul.hMul (α := R[X]) (β := R[X])
                ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _) : R[X]) X +
              -HMul.hMul (α := R[X]) (β := R[X])
                  ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _) : R[X])
                  ((C : (a : R) → R[X]) b : R[X])) :
          (a : R[X]) → R[X])
        p :
      R[X])
have h : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _) : R[X])
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])) =
  HMul.hMul (α := R[X]) (β := R[X])
      ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _) : R[X]) X +
    -HMul.hMul (α := R[X]) (β := R[X])
        ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _) : R[X])
        ((C : (a : R) → R[X]) b : R[X])
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u_3
inst : CommRing R
p : R[X]
⊢ (p.comp (-X)).comp (-X) = p
have rw : p.comp (comp (-X) (-X)) = p
Tactic: rw [comp_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
φ : R[X] →ₐ[R] A
p : R[X]
⊢ (φ : (a : R[X]) → A) p = eval₂ (algebraMap R A) ((φ : (a : R[X]) → A) X) p
have rw : Eq.{z + 1} (α := A) ((φ : (a : R[X]) → A) p : A)
  (((aeval ((φ : (a : R[X]) → A) X) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A)
Tactic: rw [← aeval_def, aeval_algHom, aeval_X_left, AlgHom.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
φ : R[X] →ₐ[R] A
p : R[X]
rw :
  Eq.{z + 1} (α := A) ((φ : (a : R[X]) → A) p : A)
    (((aeval ((φ : (a : R[X]) → A) X) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A)
⊢ (φ : (a : R[X]) → A) p = eval₂ (algebraMap R A) ((φ : (a : R[X]) → A) X) p
have rw₁ : Eq.{z + 1} (α := A) ((φ : (a : R[X]) → A) p : A) ((φ.comp (aeval X) : (a : R[X]) → A) p : A)
Tactic: rw [← aeval_def, aeval_algHom, aeval_X_left, AlgHom.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
φ : R[X] →ₐ[R] A
p : R[X]
rw :
  Eq.{z + 1} (α := A) ((φ : (a : R[X]) → A) p : A)
    (((aeval ((φ : (a : R[X]) → A) X) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A)
rw₁ : Eq.{z + 1} (α := A) ((φ : (a : R[X]) → A) p : A) ((φ.comp (aeval X) : (a : R[X]) → A) p : A)
⊢ (φ : (a : R[X]) → A) p = eval₂ (algebraMap R A) ((φ : (a : R[X]) → A) X) p
have rw₂ : Eq.{z + 1} (α := A) ((φ : (a : R[X]) → A) p : A) ((φ.comp (AlgHom.id R R[X]) : (a : R[X]) → A) p : A)
Tactic: rw [← aeval_def, aeval_algHom, aeval_X_left, AlgHom.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
A : Type z
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
φ : R[X] →ₐ[R] A
p : R[X]
rw :
  Eq.{z + 1} (α := A) ((φ : (a : R[X]) → A) p : A)
    (((aeval ((φ : (a : R[X]) → A) X) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A)
rw₁ : Eq.{z + 1} (α := A) ((φ : (a : R[X]) → A) p : A) ((φ.comp (aeval X) : (a : R[X]) → A) p : A)
rw₂ : Eq.{z + 1} (α := A) ((φ : (a : R[X]) → A) p : A) ((φ.comp (AlgHom.id R R[X]) : (a : R[X]) → A) p : A)
⊢ (φ : (a : R[X]) → A) p = eval₂ (algebraMap R A) ((φ : (a : R[X]) → A) X) p
have rw₃ : Eq.{z + 1} (α := A) ((φ : (a : R[X]) → A) p : A) ((φ : (a : R[X]) → A) p : A)
Tactic: rw [← aeval_def, aeval_algHom, aeval_X_left, AlgHom.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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 : Type u_3
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
f : F
x : A
p : R[X]
⊢ Eq.{u_2 + 1} (α := B) (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B)
    ((f : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B)
have refine : ∀ (p q : R[X])
  (hp :
    Eq.{u_2 + 1} (α := B) (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B)
      ((f : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B))
  (hq :
    Eq.{u_2 + 1} (α := B) (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) q : B)
      ((f : (a : A) → B) ((aeval x : (a : R[X]) → A) q : A) : B)),
  Eq.{u_2 + 1} (α := B) (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) (p + q) : B)
    ((f : (a : A) → B) ((aeval x : (a : R[X]) → A) (p + q) : A) : B)
Tactic: refine Polynomial.induction_on p (by simp [AlgHomClass.commutes]) (fun p q hp hq => ?_)
    (by simp [AlgHomClass.commutes])
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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 : Type u_3
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
f : F
x : A
p_1 p q : R[X]
hp :
  Eq.{u_2 + 1} (α := B) (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B)
    ((f : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B)
hq :
  Eq.{u_2 + 1} (α := B) (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) q : B)
    ((f : (a : A) → B) ((aeval x : (a : R[X]) → A) q : A) : B)
⊢ Eq.{u_2 + 1} (α := B) (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) (p + q) : B)
    ((f : (a : A) → B) ((aeval x : (a : R[X]) → A) (p + q) : A) : B)
have rw : HAdd.hAdd (α := B) (β := B) (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B)
    (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) q : B) =
  (f : (a : A) → B) ((aeval x : (a : R[X]) → A) (p + q) : A)
Tactic: rw [map_add, hp, hq, ← map_add, ← map_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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 : Type u_3
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
f : F
x : A
p_1 p q : R[X]
hp :
  Eq.{u_2 + 1} (α := B) (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B)
    ((f : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B)
hq :
  Eq.{u_2 + 1} (α := B) (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) q : B)
    ((f : (a : A) → B) ((aeval x : (a : R[X]) → A) q : A) : B)
rw :
  HAdd.hAdd (α := B) (β := B) (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B)
      (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) q : B) =
    (f : (a : A) → B) ((aeval x : (a : R[X]) → A) (p + q) : A)
⊢ Eq.{u_2 + 1} (α := B) (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) (p + q) : B)
    ((f : (a : A) → B) ((aeval x : (a : R[X]) → A) (p + q) : A) : B)
have rw₁ : HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B)
    (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) q : B) =
  (f : (a : A) → B) ((aeval x : (a : R[X]) → A) (p + q) : A)
Tactic: rw [map_add, hp, hq, ← map_add, ← map_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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 : Type u_3
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
f : F
x : A
p_1 p q : R[X]
hp :
  Eq.{u_2 + 1} (α := B) (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B)
    ((f : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B)
hq :
  Eq.{u_2 + 1} (α := B) (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) q : B)
    ((f : (a : A) → B) ((aeval x : (a : R[X]) → A) q : A) : B)
rw :
  HAdd.hAdd (α := B) (β := B) (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) p : B)
      (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) q : B) =
    (f : (a : A) → B) ((aeval x : (a : R[X]) → A) (p + q) : A)
rw₁ :
  HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B)
      (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) q : B) =
    (f : (a : A) → B) ((aeval x : (a : R[X]) → A) (p + q) : A)
⊢ Eq.{u_2 + 1} (α := B) (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) (p + q) : B)
    ((f : (a : A) → B) ((aeval x : (a : R[X]) → A) (p + q) : A) : B)
have rw₂ : HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) ((aeval x : (a : R[X]) → A) p : A) : B)
    ((f : (a : A) → B) ((aeval x : (a : R[X]) → A) q : A) : B) =
  (f : (a : A) → B) ((aeval x : (a : R[X]) → A) (p + q) : A)
Tactic: rw [map_add, hp, hq, ← map_add, ← map_add]