no goals
R : Type u_1
R₁ : Type ?u.1554584
R₂ : Type ?u.1554587
R₃ : Type ?u.1554590
R₄ : Type ?u.1554593
S : Type ?u.1554596
K : Type ?u.1554599
K₂ : Type ?u.1554602
M : Type u_2
M' : Type ?u.1554608
M₁ : Type ?u.1554611
M₂ : Type ?u.1554614
M₃ : Type ?u.1554617
M₄ : Type ?u.1554620
N : Type ?u.1554623
N₂ : Type ?u.1554626
ι : Type ?u.1554629
V : Type ?u.1554632
V₂ : Type ?u.1554635
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
p✝ p' : Submodule R M
q✝ : Submodule R₂ M₂
τ₁₂ : R →+* R₂
F : Type ?u.1554809
sc : SemilinearMapClass F τ₁₂ M M₂
p q : Submodule R M
⊢ Disjoint p q ↔ comap (Submodule.subtype p) q = ⊥
rw [← (map_injective_of_injective (show Injective p.subtype from Subtype.coe_injective)).eq_iff,
  map_comap_subtype, map_bot, disjoint_iff]