no goals
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
d : Derivation R A { x // x ∈ I }
x : A
⊢ ↑(Ideal.Quotient.mk I) ↑(↑d x) + ↑(algebraMap A (B ⧸ I)) x = ↑(algebraMap A (B ⧸ I)) x
simp only [Ideal.Quotient.eq_zero_iff_mem.mpr (d x).prop, zero_add]