awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ 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₃ : 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)
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)
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)
⊢ 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₄ : 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)
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
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
p : R[X]
⊢ Eq.{z + 1} (α := Aᵐᵒᵖ) ((aeval (MulOpposite.op x) : (a : R[X]) → Aᵐᵒᵖ) p : Aᵐᵒᵖ)
    (MulOpposite.op ((aeval x : (a : R[X]) → A) p) : Aᵐᵒᵖ)
have 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ᵐᵒᵖ)
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]
Cleared hypotheses: p
-- 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
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ᵐᵒᵖ)
⊢ Eq.{z + 1} (α := Aᵐᵒᵖ) ((aeval (MulOpposite.op x) : (a : R[X]) → Aᵐᵒᵖ) p : Aᵐᵒᵖ)
    (MulOpposite.op ((aeval x : (a : R[X]) → A) p) : Aᵐᵒᵖ)
have monomial : ∀ (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: 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]
Cleared hypotheses: p
-- 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
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
⊢ (aeval (g • x) : (a : R[X]) → A) f = HSMul.hSMul (β := A) g ((aeval x : (a : R[X]) → A) f : A)
have 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)
Tactic: rw [← MulSemiringAction.toAlgHom_apply R, aeval_algHom_apply, MulSemiringAction.toAlgHom_apply]
-- 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
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)
⊢ (aeval (g • x) : (a : R[X]) → A) f = HSMul.hSMul (β := A) g ((aeval x : (a : R[X]) → A) f : A)
have 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)
Tactic: rw [← MulSemiringAction.toAlgHom_apply R, aeval_algHom_apply, MulSemiringAction.toAlgHom_apply]
-- 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
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)
⊢ (aeval (g • x) : (a : R[X]) → A) f = HSMul.hSMul (β := A) g ((aeval x : (a : R[X]) → A) f : A)
have 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)
Tactic: rw [← MulSemiringAction.toAlgHom_apply R, aeval_algHom_apply, MulSemiringAction.toAlgHom_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
| (((aeval ((ψ : (a : S) → U) a) : T[X] →ₐ[T] U) : (a : T[X]) → U) (map φ p) : U)
have rw : (eval ((ψ : (a : S) → U) a) (map (algebraMap T U) (map φ p)) : U)
Tactic: rw [← eval_map_algebraMap]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
⊢ 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)
have 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)
Tactic: conv_rhs => rw [← eval_map_algebraMap]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
⊢ 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)
have 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)
Tactic: rw [map_map, h, ← map_map, eval_map, eval₂_at_apply, aeval_def, eval_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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)
⊢ 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)
have 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)
Tactic: rw [map_map, h, ← map_map, eval_map, eval₂_at_apply, aeval_def, eval_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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)
⊢ 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)
have 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)
Tactic: rw [map_map, h, ← map_map, eval_map, eval₂_at_apply, aeval_def, eval_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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)
⊢ 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)
have rw₃ : (ψ : (a : S) → U) ((aeval a : (a : R[X]) → S) p : S) = eval₂ ψ ((ψ : (a : S) → U) a) (map (algebraMap R S) p)
Tactic: rw [map_map, h, ← map_map, eval_map, eval₂_at_apply, aeval_def, eval_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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)
⊢ 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)
have 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)
Tactic: rw [map_map, h, ← map_map, eval_map, eval₂_at_apply, aeval_def, eval_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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)
⊢ 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)
have 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)
Tactic: rw [map_map, h, ← map_map, eval_map, eval₂_at_apply, aeval_def, eval_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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)
⊢ 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)
have 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)
Tactic: rw [map_map, h, ← map_map, eval_map, eval₂_at_apply, aeval_def, eval_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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)
⊢ Eq.{w + 1} (α := T) ((aeval a : (a : S[X]) → T) q : T) (0 : T)
have rw : ∀ (h₂ : eval a (map (algebraMap S T) p) = 0), eval a (map (algebraMap S T) q) = 0
Tactic: rw [← eval_map_algebraMap] at h₂ ⊢
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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) (∑ i ∈ range (p.natDegree + 1), p.coeff i • x ^ i : S)
have 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)
Tactic: simp_rw [Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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) (∑ i ∈ range n, p.coeff i • x ^ i : S)
have 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)
Tactic: simp_rw [Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
⊢ p.IsRoot r
have a : Eq.{v + 1} (α := S) ((f : (a : R) → S) (eval r p) : S) ((f : (a : R) → S) 0 : S)
Tactic: apply hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (eval r p) : S) ((f : (a : R) → S) 0 : S)
have a : eval₂ f ((f : (a : R) → S) r) p = (f : (a : R) → S) 0
Tactic: rw [← eval₂_hom, h, f.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (eval r p) : S) ((f : (a : R) → S) 0 : S)
have a₁ : Eq.{v + 1} (α := S) (0 : S) ((f : (a : R) → S) 0 : S)
Tactic: rw [← eval₂_hom, h, f.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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)
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (eval r p) : S) ((f : (a : R) → S) 0 : S)
have a₂ : Eq.{v + 1} (α := S) 0 0
Tactic: rw [← eval₂_hom, h, f.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
S : Type v
inst : CommSemiring S
⊢ Eq (α := (x : S) → S[X] →ₐ[S] S) (aevalTower (AlgHom.id S S)) aeval
have 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)
Tactic: ext s
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
S : Type v
A' : Type u_1
inst : CommSemiring A'
inst_1 : CommSemiring S
inst_2 : Algebra S A'
⊢ Eq (α := (x : A') → S[X] →ₐ[S] A') (aevalTower (Algebra.ofId S A')) aeval
have 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')
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
⊢ 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)
have 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
Tactic: simp only [rTensor_tmul, coe_restrictScalars, monomial_zero_left]