no goals
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type ?u.819159
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R₁
inst✝⁵ : CommSemiring R₂
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R₁ A
inst✝¹ : Algebra R₂ A
inst✝ : Algebra R₁ B
f : A →ₐ[R₁] B
a : A
⊢ ↑(kerLiftAlg f) (↑(Quotient.mk (RingHom.ker f)) a) = ↑f a
rfl