Theorem: AlgHom.comp_rangeRestrict (DividedPowers/PolynomialMap/Basic.lean)

State before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Semiring S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
⊢ φ.range.val.comp φ.rangeRestrict = φ
Tactic:
ext
State after:
case H
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Semiring S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
x✝ : S
⊢ (φ.range.val.comp φ.rangeRestrict) x✝ = φ x✝

State before:
case H
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Semiring S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
x✝ : S
⊢ (φ.range.val.comp φ.rangeRestrict) x✝ = φ x✝
Tactic:
rfl
State after:
no goals