no goals
R : Type u_2
R₁ : Type ?u.1204225
R₂ : Type u_3
R₃ : Type ?u.1204231
R₄ : Type ?u.1204234
S : Type ?u.1204237
K : Type ?u.1204240
K₂ : Type ?u.1204243
M : Type u_1
M' : Type ?u.1204249
M₁ : Type ?u.1204252
M₂ : Type u_4
M₃ : Type ?u.1204258
M₄ : Type ?u.1204261
N : Type ?u.1204264
N₂ : Type ?u.1204267
ι : Type ?u.1204270
V : Type ?u.1204273
V₂ : Type ?u.1204276
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
σ₂₁ : R₂ →+* R
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type u_5
sc : SemilinearMapClass F τ₁₂ M M₂
f : F
⊢ ker f = ⊥ ↔ ∀ (m : M), ↑f m = 0 → m = 0
simpa [disjoint_iff_inf_le] using @disjoint_ker _ _ _ _ _ _ _ _ _ _ _ _ _ f ⊤