R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
ha : a ∈ I
⊢ ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0
intro a ha
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
ha : a ∈ I
⊢ ↑C a ∈ map C I
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
ha : a ∈ I
⊢ ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0
rw [RingHom.comp_apply, Quotient.eq_zero_iff_mem]
no goals
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
ha : a ∈ I
⊢ ↑C a ∈ map C I
exact mem_map_of_mem _ ha