rintro _ I hI - rfl
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
⊢ ∀ ⦃a : ℕ⦄ (x : Set α), M₁.Indep x → M₂.Indep x → x.ncard = a → a ≤ M₁.E.ncard
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
I : Set α
hI : M₁.Indep I
⊢ I.ncard ≤ M₁.E.ncard