Theorem: DividedPowerAlgebra.gamma_toFun (DividedPowers/DPAlgebra/PolynomialMap.lean)

State before:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
m : S ⊗[R] M
⊢ (gamma R M n).toFun S m = (dpScalarExtensionEquiv R S M).symm (dp S n m)
Tactic:
obtain ⟨k, ψ, p, rfl⟩ := PolynomialMap.exists_lift m
State after:
case intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
ψ : MvPolynomial (Fin k) R →ₐ[R] S
p : MvPolynomial (Fin k) R ⊗[R] M
⊢ (gamma R M n).toFun S ((LinearMap.rTensor M ψ.toLinearMap) p) =
    (dpScalarExtensionEquiv R S M).symm (dp S n ((LinearMap.rTensor M ψ.toLinearMap) p))

State before:
case intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
ψ : MvPolynomial (Fin k) R →ₐ[R] S
p : MvPolynomial (Fin k) R ⊗[R] M
⊢ (gamma R M n).toFun S ((LinearMap.rTensor M ψ.toLinearMap) p) =
    (dpScalarExtensionEquiv R S M).symm (dp S n ((LinearMap.rTensor M ψ.toLinearMap) p))
Tactic:
rw [← (gamma R M n).isCompat_apply, PolynomialMap.toFun_eq_toFun']
State after:
case intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
ψ : MvPolynomial (Fin k) R →ₐ[R] S
p : MvPolynomial (Fin k) R ⊗[R] M
⊢ (LinearMap.rTensor (DividedPowerAlgebra R M) ψ.toLinearMap) ((gamma R M n).toFun' (MvPolynomial (Fin k) R) p) =
    (dpScalarExtensionEquiv R S M).symm (dp S n ((LinearMap.rTensor M ψ.toLinearMap) p))

State before:
case intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
n : ℕ
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
ψ : MvPolynomial (Fin k) R →ₐ[R] S
p : MvPolynomial (Fin k) R ⊗[R] M
⊢ (LinearMap.rTensor (DividedPowerAlgebra R M) ψ.toLinearMap) ((gamma R M n).toFun' (MvPolynomial (Fin k) R) p) =
    (dpScalarExtensionEquiv R S M).symm (dp S n ((LinearMap.rTensor M ψ.toLinearMap) p))
Tactic:
simp only [gamma, rTensor_comp_dpScalarExtensionEquiv_symm_eq]
State after:
no goals