no goals
ι : Type u'
ι' : Type u_3
R : Type u_1
K : Type ?u.650261
M : Type u_2
M' : Type u_4
M'' : Type ?u.650270
V : Type u
V' : Type ?u.650275
v✝ : ι → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
⊢ Disjoint (span R (Set.range (↑(inl R M M') ∘ v))) (span R (Set.range (↑(inr R M M') ∘ v')))
refine' isCompl_range_inl_inr.disjoint.mono _ _ <;>
  simp only [span_le, range_coe, range_comp_subset_range]