no goals
R : Type u_2
R₁ : Type ?u.1341382
R₂ : Type u_3
R₃ : Type ?u.1341388
R₄ : Type ?u.1341391
S : Type ?u.1341394
K : Type ?u.1341397
K₂ : Type ?u.1341400
M : Type u_1
M' : Type ?u.1341406
M₁ : Type ?u.1341409
M₂ : Type u_4
M₃ : Type ?u.1341415
M₄ : Type ?u.1341418
N : Type ?u.1341421
N₂ : Type ?u.1341424
ι : Type ?u.1341427
V : Type ?u.1341430
V₂ : Type ?u.1341433
inst✝⁹ : Ring R
inst✝⁸ : Ring R₂
inst✝⁷ : Ring R₃
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
x y : M
⊢ x - y ∈ ker f ↔ ↑f x = ↑f y
rw [mem_ker, map_sub, sub_eq_zero]