case intro
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type ?u.775415
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
r : R₁
a : A
⊢ ↑(RingHom.kerLift ↑f) (r • ↑(Quotient.mkₐ R₁ (RingHom.ker ↑f)) a) =
    r • ↑(RingHom.kerLift ↑f) (↑(Quotient.mkₐ R₁ (RingHom.ker ↑f)) a)
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type ?u.775415
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
r : R₁
x : A ⧸ RingHom.ker ↑f
⊢ ↑(RingHom.kerLift ↑f) (r • x) = r • ↑(RingHom.kerLift ↑f) x
obtain ⟨a, rfl⟩ := Quotient.mkₐ_surjective R₁ _ x
no goals
case intro
R : Type u
S : Type v
F : Type w
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
R₁ : Type u_1
R₂ : Type ?u.775415
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
r : R₁
a : A
⊢ ↑(RingHom.kerLift ↑f) (r • ↑(Quotient.mkₐ R₁ (RingHom.ker ↑f)) a) =
    r • ↑(RingHom.kerLift ↑f) (↑(Quotient.mkₐ R₁ (RingHom.ker ↑f)) a)
exact f.map_smul _ _