no goals
R : Type u
A₁ : Type v
A₂ : Type w
A₃ : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A₁
inst✝⁴ : Semiring A₂
inst✝³ : Semiring A₃
inst✝² : Algebra R A₁
inst✝¹ : Algebra R A₂
inst✝ : Algebra R A₃
e✝ e : A₁ ≃ₐ[R] A₂
y : R
x : A₁
h : ↑(algebraMap R A₂) y = ↑e x
⊢ ↑(algebraMap R A₁) y = x
simpa using e.symm.toAlgHom.algebraMap_eq_apply h