Theorem: PolynomialMap.toFun'_eq_of_inclusion (DividedPowers/PolynomialMap/Basic.lean)

State before:
R : Type u
inst✝¹⁰ : CommRing R
M : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type u_2
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A : Type u
inst✝³ : CommRing A
inst✝² : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] S
q : B ⊗[R] M
h : φ.range ≤ ψ.range
hpq :
  (LinearMap.rTensor M ((Subalgebra.inclusion h).comp φ.rangeRestrict).toLinearMap) p =
    (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
⊢ ψ.range.val.comp (Subalgebra.inclusion h) = (AlgHom.id R S).comp φ.range.val
Tactic:
ext x
State after:
case H
R : Type u
inst✝¹⁰ : CommRing R
M : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type u_2
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A : Type u
inst✝³ : CommRing A
inst✝² : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] S
q : B ⊗[R] M
h : φ.range ≤ ψ.range
hpq :
  (LinearMap.rTensor M ((Subalgebra.inclusion h).comp φ.rangeRestrict).toLinearMap) p =
    (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
x : ↥φ.range
⊢ (ψ.range.val.comp (Subalgebra.inclusion h)) x = ((AlgHom.id R S).comp φ.range.val) x

State before:
case H
R : Type u
inst✝¹⁰ : CommRing R
M : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type u_2
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A : Type u
inst✝³ : CommRing A
inst✝² : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] S
q : B ⊗[R] M
h : φ.range ≤ ψ.range
hpq :
  (LinearMap.rTensor M ((Subalgebra.inclusion h).comp φ.rangeRestrict).toLinearMap) p =
    (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
x : ↥φ.range
⊢ (ψ.range.val.comp (Subalgebra.inclusion h)) x = ((AlgHom.id R S).comp φ.range.val) x
Tactic:
simp
State after:
no goals