exact ncard_le_ncard hJ₁.subset_ground M₁.ground_finite
case h
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
J : Set α
hJ₁ : M₁.Indep J
⊢ J.ncard ≤ M₁.E.ncard
no goals