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.432772
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'
p : R[X]
q : PolynomialModule R M
⊢ ↑(map R' f) (p • 0) = Polynomial.map (algebraMap R R') p • ↑(map R' f) 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.432772
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'
p : R[X]
q : PolynomialModule R M
⊢ ∀ (f_1 g : PolynomialModule R M),
    ↑(map R' f) (p • f_1) = Polynomial.map (algebraMap R R') p • ↑(map R' f) f_1 →
      ↑(map R' f) (p • g) = Polynomial.map (algebraMap R R') p • ↑(map R' f) g →
        ↑(map R' f) (p • (f_1 + g)) = Polynomial.map (algebraMap R R') p • ↑(map R' f) (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.432772
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'
p : R[X]
q : PolynomialModule R M
⊢ ∀ (a : ℕ) (b : M),
    ↑(map R' f) (p • ↑(single R a) b) = Polynomial.map (algebraMap R R') p • ↑(map R' f) (↑(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.432772
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'
p : R[X]
q : PolynomialModule R M
⊢ ↑(map R' f) (p • q) = Polynomial.map (algebraMap R R') p • ↑(map R' f) q
apply induction_linear q
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.432772
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'
p : R[X]
q : PolynomialModule R M
i : ℕ
m : M
⊢ ↑(map R' f) (p • ↑(single R i) m) = Polynomial.map (algebraMap R R') p • ↑(map R' f) (↑(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.432772
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'
p : R[X]
q : PolynomialModule R M
⊢ ∀ (a : ℕ) (b : M),
    ↑(map R' f) (p • ↑(single R a) b) = Polynomial.map (algebraMap R R') p • ↑(map R' f) (↑(single R a) b)
intro i m
case hsingle.h_add
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type ?u.432772
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
i : ℕ
m : M
p✝ q✝ : R[X]
e₁ : ↑(map R' f) (p✝ • ↑(single R i) m) = Polynomial.map (algebraMap R R') p✝ • ↑(map R' f) (↑(single R i) m)
e₂ : ↑(map R' f) (q✝ • ↑(single R i) m) = Polynomial.map (algebraMap R R') q✝ • ↑(map R' f) (↑(single R i) m)
⊢ ↑(map R' f) ((p✝ + q✝) • ↑(single R i) m) = Polynomial.map (algebraMap R R') (p✝ + q✝) • ↑(map R' f) (↑(single R i) m)

case hsingle.h_monomial
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type ?u.432772
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
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ ↑(map R' f) (↑(monomial n✝) a✝ • ↑(single R i) m) =
    Polynomial.map (algebraMap R R') (↑(monomial n✝) a✝) • ↑(map R' f) (↑(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.432772
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'
p : R[X]
q : PolynomialModule R M
i : ℕ
m : M
⊢ ↑(map R' f) (p • ↑(single R i) m) = Polynomial.map (algebraMap R R') p • ↑(map R' f) (↑(single R i) m)
induction' p using Polynomial.induction_on' with _ _ e₁ e₂
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.432772
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'
p : R[X]
q : PolynomialModule R M
⊢ ↑(map R' f) (p • 0) = Polynomial.map (algebraMap R R') p • ↑(map R' f) 0
rw [smul_zero, map_zero, smul_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.432772
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'
p : R[X]
q f g : PolynomialModule R M
e₁ : ↑(map R' f✝) (p • f) = Polynomial.map (algebraMap R R') p • ↑(map R' f✝) f
e₂ : ↑(map R' f✝) (p • g) = Polynomial.map (algebraMap R R') p • ↑(map R' f✝) g
⊢ ↑(map R' f✝) (p • (f + g)) = Polynomial.map (algebraMap R R') p • ↑(map R' f✝) (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.432772
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'
p : R[X]
q : PolynomialModule R M
⊢ ∀ (f_1 g : PolynomialModule R M),
    ↑(map R' f) (p • f_1) = Polynomial.map (algebraMap R R') p • ↑(map R' f) f_1 →
      ↑(map R' f) (p • g) = Polynomial.map (algebraMap R R') p • ↑(map R' f) g →
        ↑(map R' f) (p • (f_1 + g)) = Polynomial.map (algebraMap R R') p • ↑(map R' f) (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.432772
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'
p : R[X]
q f g : PolynomialModule R M
e₁ : ↑(map R' f✝) (p • f) = Polynomial.map (algebraMap R R') p • ↑(map R' f✝) f
e₂ : ↑(map R' f✝) (p • g) = Polynomial.map (algebraMap R R') p • ↑(map R' f✝) g
⊢ ↑(map R' f✝) (p • (f + g)) = Polynomial.map (algebraMap R R') p • ↑(map R' f✝) (f + g)
rw [smul_add, map_add, e₁, e₂, map_add, smul_add]
no goals
case hsingle.h_add
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type ?u.432772
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
i : ℕ
m : M
p✝ q✝ : R[X]
e₁ : ↑(map R' f) (p✝ • ↑(single R i) m) = Polynomial.map (algebraMap R R') p✝ • ↑(map R' f) (↑(single R i) m)
e₂ : ↑(map R' f) (q✝ • ↑(single R i) m) = Polynomial.map (algebraMap R R') q✝ • ↑(map R' f) (↑(single R i) m)
⊢ ↑(map R' f) ((p✝ + q✝) • ↑(single R i) m) = Polynomial.map (algebraMap R R') (p✝ + q✝) • ↑(map R' f) (↑(single R i) m)
rw [add_smul, map_add, e₁, e₂, Polynomial.map_add, add_smul]
no goals
case hsingle.h_monomial
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type ?u.432772
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
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ ↑(map R' f) (↑(monomial n✝) a✝ • ↑(single R i) m) =
    Polynomial.map (algebraMap R R') (↑(monomial n✝) a✝) • ↑(map R' f) (↑(single R i) m)
rw [monomial_smul_single, map_single, Polynomial.map_monomial, map_single, monomial_smul_single,
  f.map_smul, algebraMap_smul]