case h0
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type ?u.548565
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
r : R
⊢ ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) 0) = ↑f (↑(eval r) 0)

case hadd
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type ?u.548565
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
r : R
⊢ ∀ (f_1 g : PolynomialModule R M),
    ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) f_1) = ↑f (↑(eval r) f_1) →
      ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) g) = ↑f (↑(eval r) g) →
        ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) (f_1 + g)) = ↑f (↑(eval r) (f_1 + g))

case hsingle
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type ?u.548565
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
r : R
⊢ ∀ (a : ℕ) (b : M), ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) (↑(single R a) b)) = ↑f (↑(eval r) (↑(single R a) b))
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type ?u.548565
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
r : R
⊢ ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) q) = ↑f (↑(eval r) q)
apply induction_linear q
no goals
case h0
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type ?u.548565
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
r : R
⊢ ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) 0) = ↑f (↑(eval r) 0)
simp_rw [map_zero]
case hadd
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type ?u.548565
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f✝ : M →ₗ[R] M'
q : PolynomialModule R M
r : R
f g : PolynomialModule R M
e₁ : ↑(eval (↑(algebraMap R R') r)) (↑(map R' f✝) f) = ↑f✝ (↑(eval r) f)
e₂ : ↑(eval (↑(algebraMap R R') r)) (↑(map R' f✝) g) = ↑f✝ (↑(eval r) g)
⊢ ↑(eval (↑(algebraMap R R') r)) (↑(map R' f✝) (f + g)) = ↑f✝ (↑(eval r) (f + g))
case hadd
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type ?u.548565
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
r : R
⊢ ∀ (f_1 g : PolynomialModule R M),
    ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) f_1) = ↑f (↑(eval r) f_1) →
      ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) g) = ↑f (↑(eval r) g) →
        ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) (f_1 + g)) = ↑f (↑(eval r) (f_1 + g))
intro f g e₁ e₂
no goals
case hadd
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type ?u.548565
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f✝ : M →ₗ[R] M'
q : PolynomialModule R M
r : R
f g : PolynomialModule R M
e₁ : ↑(eval (↑(algebraMap R R') r)) (↑(map R' f✝) f) = ↑f✝ (↑(eval r) f)
e₂ : ↑(eval (↑(algebraMap R R') r)) (↑(map R' f✝) g) = ↑f✝ (↑(eval r) g)
⊢ ↑(eval (↑(algebraMap R R') r)) (↑(map R' f✝) (f + g)) = ↑f✝ (↑(eval r) (f + g))
simp_rw [map_add, e₁, e₂]
case hsingle
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type ?u.548565
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
r : R
i : ℕ
m : M
⊢ ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) (↑(single R i) m)) = ↑f (↑(eval r) (↑(single R i) m))
case hsingle
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type ?u.548565
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
r : R
⊢ ∀ (a : ℕ) (b : M), ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) (↑(single R a) b)) = ↑f (↑(eval r) (↑(single R a) b))
intro i m
no goals
case hsingle
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type ?u.548565
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
r : R
i : ℕ
m : M
⊢ ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) (↑(single R i) m)) = ↑f (↑(eval r) (↑(single R i) m))
rw [map_single, eval_single, eval_single, f.map_smul, ← map_pow, algebraMap_smul]