Theorem: PolynomialMap.isHomogeneousOfDegree_toFun (DividedPowers/PolynomialMap/Homogeneous.lean)

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
p : ℕ
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree p f
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
m : S ⊗[R] M
⊢ f.toFun S (r • m) = r ^ p • f.toFun S m
Tactic:
choose n ψ  m' r' hm' hr' using PolynomialMap.exists_lift' m r
State after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
p : ℕ
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree p f
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
m : S ⊗[R] M
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
m' : MvPolynomial (Fin n) R ⊗[R] M
r' : MvPolynomial (Fin n) R
hm' : (LinearMap.rTensor M ψ.toLinearMap) m' = m
hr' : ψ r' = r
⊢ f.toFun S (r • m) = r ^ p • f.toFun S m

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
p : ℕ
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree p f
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
m : S ⊗[R] M
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
m' : MvPolynomial (Fin n) R ⊗[R] M
r' : MvPolynomial (Fin n) R
hm' : (LinearMap.rTensor M ψ.toLinearMap) m' = m
hr' : ψ r' = r
⊢ f.toFun S (r • m) = r ^ p • f.toFun S m
Tactic:
simp only [← hm', ← hr', ← isCompat_apply, toFun_eq_toFun', TensorProduct.smul_rTensor]
State after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
p : ℕ
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree p f
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
m : S ⊗[R] M
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
m' : MvPolynomial (Fin n) R ⊗[R] M
r' : MvPolynomial (Fin n) R
hm' : (LinearMap.rTensor M ψ.toLinearMap) m' = m
hr' : ψ r' = r
⊢ (LinearMap.rTensor N ψ.toLinearMap) (f.toFun' (MvPolynomial (Fin n) R) (r' • m')) =
    ψ r' ^ p • (LinearMap.rTensor N ψ.toLinearMap) (f.toFun' (MvPolynomial (Fin n) R) m')

State before:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
p : ℕ
f : M →ₚ[R] N
hf : IsHomogeneousOfDegree p f
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : S
m : S ⊗[R] M
n : ℕ
ψ : MvPolynomial (Fin n) R →ₐ[R] S
m' : MvPolynomial (Fin n) R ⊗[R] M
r' : MvPolynomial (Fin n) R
hm' : (LinearMap.rTensor M ψ.toLinearMap) m' = m
hr' : ψ r' = r
⊢ (LinearMap.rTensor N ψ.toLinearMap) (f.toFun' (MvPolynomial (Fin n) R) (r' • m')) =
    ψ r' ^ p • (LinearMap.rTensor N ψ.toLinearMap) (f.toFun' (MvPolynomial (Fin n) R) m')
Tactic:
rw [hf, ← TensorProduct.smul_rTensor, map_pow]
State after:
no goals