no goals
S : Type ?u.440894
R : Type u_1
A : Type u_2
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type ?u.444063
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_3
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ ψ : Unitization R A →ₐ[R] C
h : NonUnitalAlgHom.comp (↑φ) (inrNonUnitalAlgHom R A) = NonUnitalAlgHom.comp (↑ψ) (inrNonUnitalAlgHom R A)
⊢ ∀ (r : R), ↑φ (↑(algebraMap R (Unitization R A)) r) = ↑ψ (↑(algebraMap R (Unitization R A)) r)
simp [AlgHom.commutes]