awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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]
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)
rw₃ 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)
⊢ 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)

Tactic:
rw [mapAlg_eq_map, coeff_map, IsScalarTower.algebraMap_eq A B C, RingHom.comp_apply]

Premises used: Polynomial.coeff_map, Polynomial.mapAlg_eq_map, IsScalarTower.algebraMap_eq, RingHom.comp_apply
-- 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 : 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]
refine_2 : AlgHom.comp (aeval q) (aeval p) = AlgHom.id R R[X]
⊢ R[X] ≃ₐ[R] R[X]

Tactic:
refine AlgEquiv.ofAlgHom (aeval p) (aeval q) ?_ ?_

Premises used: AlgEquiv.ofAlgHom, Polynomial.aeval
-- 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 : 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
x_1 : R[X]
⊢ Eq (α := R[X]) ((AlgHom.comp (aeval p) (aeval q) : (a : R[X]) → R[X]) x_1 : R[X])
    ((AlgHom.id R R[X] : (a : R[X]) → R[X]) x_1 : R[X])

Tactic:
simp [← comp_eq_aeval, comp_assoc, hpq, hqp]

Premises used: Polynomial.comp_assoc, Polynomial.comp_eq_aeval
-- 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 : 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
⊢ AlgHom.comp (aeval p) (aeval q) = AlgHom.id R R[X]

Tactic:
exact AlgHom.ext fun _ ↦ by simp [← comp_eq_aeval, comp_assoc, hpq, hqp]

Premises used: AlgHom.ext
-- 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 : 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
x_1 : R[X]
⊢ Eq (α := R[X]) ((AlgHom.comp (aeval q) (aeval p) : (a : R[X]) → R[X]) x_1 : R[X])
    ((AlgHom.id R R[X] : (a : R[X]) → R[X]) x_1 : R[X])

Tactic:
simp [← comp_eq_aeval, comp_assoc, hpq, hqp]

Premises used: Polynomial.comp_assoc, Polynomial.comp_eq_aeval
-- 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 : 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
⊢ AlgHom.comp (aeval q) (aeval p) = AlgHom.id R R[X]

Tactic:
exact AlgHom.ext fun _ ↦ by simp [← comp_eq_aeval, comp_assoc, hpq, hqp]

Premises used: AlgHom.ext
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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.algEquivOfCompEqX q hpq hqp = p'.algEquivOfCompEqX q' hpq' hqp'
⊢ p = p'

Tactic:
simpa using congr($h X)
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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'
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])
⊢ p.algEquivOfCompEqX q hpq hqp = p'.algEquivOfCompEqX q' hpq' hqp'

Tactic:
ext1
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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'
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:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
⊢ (p.algEquivOfCompEqX q hpq hqp).symm = q.algEquivOfCompEqX p hqp hpq

Tactic:
rfl

Premises used: AlgEquiv.symm, Polynomial.algEquivOfCompEqX, AlgEquiv.ofAlgHom, Equiv.symm, rfl
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R_1 : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a_1 b_1 : R_1
n : ℕ
inst : CommSemiring R_1
inst_1 : Semiring A
inst_2 : CommSemiring A'
inst_3 : Semiring B
inst_4 : Algebra R_1 A
inst_5 : Algebra R_1 B
p q : R_1[X]
x : A
R : Type u_3
inst_6 : CommRing R
a b : R
inst_7 : Invertible a
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) b : R[X])).comp
      (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]))) =
    X

Tactic:
simp [← C_mul, ← mul_assoc]

Premises used: mul_assoc, Polynomial.C_mul
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R_1 : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a_1 b_1 : R_1
n : ℕ
inst : CommSemiring R_1
inst_1 : Semiring A
inst_2 : CommSemiring A'
inst_3 : Semiring B
inst_4 : Algebra R_1 A
inst_5 : Algebra R_1 B
p q : R_1[X]
x : A
R : Type u_3
inst_6 : CommRing R
a b : R
inst_7 : Invertible a
⊢ (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]))).comp
      (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])) =
    X

Tactic:
simp [← C_mul, ← mul_assoc]

Premises used: mul_assoc, Polynomial.C_mul
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u_3
inst : CommRing R
a b : R
inst_1 : Invertible a
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])
⊢ 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))

Tactic:
ext p : 1
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u_3
inst : CommRing R
a b : R
inst_1 : Invertible a
p : R[X]
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])
⊢ 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:
simp only [algEquivCMulXAddC_symm_apply, neg_mul, algEquivCMulXAddC_apply, map_neg, map_mul]

Premises used: Polynomial.algEquivCMulXAddC_apply, map_neg, map_mul, neg_mul, Polynomial.algEquivCMulXAddC_symm_apply
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u_3
inst : CommRing R
a b : R
inst_1 : Invertible a
p : R[X]
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])
⊢ 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:
congr
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u_3
inst : CommRing R
a b : R
inst_1 : Invertible a
p : R[X]
⊢ 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:
simp [mul_add, sub_eq_add_neg]

Premises used: sub_eq_add_neg, mul_add
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R_1 : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R_1
n : ℕ
inst : CommSemiring R_1
inst_1 : Semiring A
inst_2 : CommSemiring A'
inst_3 : Semiring B
inst_4 : Algebra R_1 A
inst_5 : Algebra R_1 B
p q : R_1[X]
x : A
R : Type u_3
inst_6 : CommRing R
t : R
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])).comp
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) =
    X

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R_1 : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R_1
n : ℕ
inst : CommSemiring R_1
inst_1 : Semiring A
inst_2 : CommSemiring A'
inst_3 : Semiring B
inst_4 : Algebra R_1 A
inst_5 : Algebra R_1 B
p q : R_1[X]
x : A
R : Type u_3
inst_6 : CommRing R
t : R
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])).comp
      (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) =
    X

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u_3
inst : CommRing R
t t' : R
⊢ Eq (α := R[X] ≃ₐ[R] R[X]) (algEquivAevalXAddC t) (algEquivAevalXAddC t') ↔ t = t'

Tactic:
simp [algEquivAevalXAddC]

Premises used: Polynomial.algEquivAevalXAddC
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u_3
inst : CommRing R
t : R
⊢ Eq (α := R[X] ≃ₐ[R] R[X]) (AlgEquiv.symm (algEquivAevalXAddC t)) (algEquivAevalXAddC (-t))

Tactic:
simp [algEquivAevalXAddC, sub_eq_add_neg]

Premises used: sub_eq_add_neg, Polynomial.algEquivAevalXAddC
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R_1 : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R_1
n : ℕ
inst : CommSemiring R_1
inst_1 : Semiring A
inst_2 : CommSemiring A'
inst_3 : Semiring B
inst_4 : Algebra R_1 A
inst_5 : Algebra R_1 B
p q : R_1[X]
x : A
R : Type u_3
inst_6 : CommRing R
⊢ Eq.{u_3 + 1} (α := R[X]) (comp (-X) (-X)) X

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u_3
inst : CommRing R
p : R[X]
rw : p.comp (comp (-X) (-X)) = p
⊢ (p.comp (-X)).comp (-X) = p

Tactic:
rw [comp_assoc]

Premises used: Polynomial.comp_assoc
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u_3
inst : CommRing R
p : R[X]
⊢ p.comp (comp (-X) (-X)) = p

Tactic:
simp only [neg_comp, X_comp, neg_neg, comp_X]

Premises used: Polynomial.X_comp, neg_neg, Polynomial.comp_X, Polynomial.neg_comp
-- 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
⊢ Eq.{u_2 + 1} (α := B) (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) X : B)
    ((f.comp (aeval x) : (a : R[X]) → B) X : B)

Tactic:
simp only [aeval_X, AlgHom.comp_apply]

Premises used: AlgHom.comp_apply, Polynomial.aeval_X
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := R[X] →ₐ[R] R[X]) (aeval X) (AlgHom.id R R[X])

Tactic:
algHom_ext <| aeval_X X

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

Tactic:
AlgHom.congr_fun (@aeval_X_left R _) p

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

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
φ : 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)
rw₃ rw₄ : Eq.{z + 1} (α := A) ((φ : (a : R[X]) → A) p : A) ((φ : (a : R[X]) → A) p : A)
⊢ (φ : (a : R[X]) → A) p = eval₂ (algebraMap R A) ((φ : (a : R[X]) → A) X) p

Tactic:
rw [← aeval_def, aeval_algHom, aeval_X_left, AlgHom.comp_id]

Premises used: Polynomial.aeval_X_left, Polynomial.aeval_def, AlgHom.comp_id, Polynomial.aeval_algHom
-- 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 : Type u_3
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
f : F
x : A
p : R[X]
⊢ ∀ (a : R),
    Eq.{u_2 + 1} (α := B)
      (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B) ((C : (a : R) → R[X]) a : R[X]) : B)
      ((f : (a : A) → B) ((aeval x : (a : R[X]) → A) ((C : (a : R) → R[X]) a : R[X]) : A) : B)

Tactic:
simp [AlgHomClass.commutes]

Premises used: AlgHomClass.commutes
-- 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 : Type u_3
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
f : F
x : A
p : R[X]
⊢ ∀ (n : ℕ) (a : R),
    Eq.{u_2 + 1} (α := B)
        (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B)
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) :
          B)
        ((f : (a : A) → B)
            ((aeval x : (a : R[X]) → A)
                (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) :
              A) :
          B) →
      Eq.{u_2 + 1} (α := B)
        (((aeval ((f : (a : A) → B) x) : R[X] →ₐ[R] B) : (a : R[X]) → B)
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
          B)
        ((f : (a : A) → B)
            ((aeval x : (a : R[X]) → A)
                (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
              A) :
          B)

Tactic:
simp [AlgHomClass.commutes]

Premises used: AlgHomClass.commutes
-- 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 : Type u_3
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
f : F
x : A
p : R[X]
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)
⊢ 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)

Tactic:
refine Polynomial.induction_on p (by simp [AlgHomClass.commutes]) (fun p q hp hq => ?_)
    (by simp [AlgHomClass.commutes])
-- 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 : 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)
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)
rw₃ :
  Eq.{u_2 + 1} (α := B)
    ((f : (a : A) → B)
        (HAdd.hAdd (α := A) (β := A) ((aeval x : (a : R[X]) → A) p : A) ((aeval x : (a : R[X]) → A) q : A)) :
      B)
    ((f : (a : A) → B) ((aeval x : (a : R[X]) → A) (p + q) : A) : B)
rw₄ rw₅ :
  Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) ((aeval x : (a : R[X]) → A) (p + q) : A) : B)
    ((f : (a : A) → B) ((aeval x : (a : R[X]) → A) (p + 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:
rw [map_add, hp, hq, ← map_add, ← 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
p q : R[X]
hp :
  Eq.{z + 1} (α := Aᵐᵒᵖ) ((aeval (MulOpposite.op x) : (a : R[X]) → Aᵐᵒᵖ) p : Aᵐᵒᵖ)
    (MulOpposite.op ((aeval x : (a : R[X]) → A) p) : Aᵐᵒᵖ)
hq :
  Eq.{z + 1} (α := Aᵐᵒᵖ) ((aeval (MulOpposite.op x) : (a : R[X]) → Aᵐᵒᵖ) q : Aᵐᵒᵖ)
    (MulOpposite.op ((aeval x : (a : R[X]) → A) q) : Aᵐᵒᵖ)
⊢ Eq.{z + 1} (α := Aᵐᵒᵖ) ((aeval (MulOpposite.op x) : (a : R[X]) → Aᵐᵒᵖ) (p + q) : Aᵐᵒᵖ)
    (MulOpposite.op ((aeval x : (a : R[X]) → A) (p + q)) : Aᵐᵒᵖ)

Tactic:
simp [map_add, hp, hq]

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
n : ℕ
c : R
⊢ Eq.{z + 1} (α := Aᵐᵒᵖ) ((aeval (MulOpposite.op x) : (a : R[X]) → Aᵐᵒᵖ) ((monomial n : (a : R) → R[X]) c) : Aᵐᵒᵖ)
    (MulOpposite.op ((aeval x : (a : R[X]) → A) ((monomial n : (a : R) → R[X]) c : R[X])) : Aᵐᵒᵖ)

Tactic:
simp [aeval_monomial, MulOpposite.op_pow, Algebra.commutes]

Premises used: MulOpposite.op_pow, Polynomial.aeval_monomial, Algebra.commutes
-- 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]
add :
  ∀ (p q : R[X])
    (hp :
      Eq.{z + 1} (α := Aᵐᵒᵖ) ((aeval (MulOpposite.op x) : (a : R[X]) → Aᵐᵒᵖ) p : Aᵐᵒᵖ)
        (MulOpposite.op ((aeval x : (a : R[X]) → A) p) : Aᵐᵒᵖ))
    (hq :
      Eq.{z + 1} (α := Aᵐᵒᵖ) ((aeval (MulOpposite.op x) : (a : R[X]) → Aᵐᵒᵖ) q : Aᵐᵒᵖ)
        (MulOpposite.op ((aeval x : (a : R[X]) → A) q) : Aᵐᵒᵖ)),
    Eq.{z + 1} (α := Aᵐᵒᵖ) ((aeval (MulOpposite.op x) : (a : R[X]) → Aᵐᵒᵖ) (p + q) : Aᵐᵒᵖ)
      (MulOpposite.op ((aeval x : (a : R[X]) → A) (p + q)) : Aᵐᵒᵖ)
monomial :
  ∀ (n : ℕ) (c : R),
    Eq.{z + 1} (α := Aᵐᵒᵖ)
      ((aeval (MulOpposite.op x) : (a : R[X]) → Aᵐᵒᵖ) ((Polynomial.monomial n : (a : R) → R[X]) c) : Aᵐᵒᵖ)
      (MulOpposite.op ((aeval x : (a : R[X]) → A) ((Polynomial.monomial n : (a : R) → R[X]) c : R[X])) : Aᵐᵒᵖ)
⊢ Eq.{z + 1} (α := Aᵐᵒᵖ) ((aeval (MulOpposite.op x) : (a : R[X]) → Aᵐᵒᵖ) p : Aᵐᵒᵖ)
    (MulOpposite.op ((aeval x : (a : R[X]) → A) p) : Aᵐᵒᵖ)

Tactic:
induction p using Polynomial.induction_on' with
  | add p q hp hq => simp [map_add, hp, hq]
  | monomial n c => simp [aeval_monomial, MulOpposite.op_pow, Algebra.commutes]

Premises used: MulOpposite.op_pow, map_add, Polynomial.monomial, Polynomial.aeval_monomial, Algebra.commutes