no goals
R : Type u_2
R₁ : Type ?u.1427240
R₂ : Type u_3
R₃ : Type ?u.1427246
R₄ : Type ?u.1427249
S : Type ?u.1427252
K : Type ?u.1427255
K₂ : Type ?u.1427258
M : Type u_1
M' : Type ?u.1427264
M₁ : Type ?u.1427267
M₂ : Type u_4
M₃ : Type ?u.1427273
M₄ : Type ?u.1427276
N : Type ?u.1427279
N₂ : Type ?u.1427282
ι : Type ?u.1427285
V : Type ?u.1427288
V₂ : Type ?u.1427291
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
⊢ ker f = ⊥ ↔ Injective ↑f
simpa [disjoint_iff_inf_le] using @disjoint_ker' _ _ _ _ _ _ _ _ _ _ _ _ _ f ⊤