obtain ⟨I, hI⟩ := M.maximality A (hA.trans hB) ∅ M.empty_indep (Set.empty_subset A)
α : Type u_1
I : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
⊢ ∃ I J, I ⊆ J ∧ M.Basis I A ∧ M.Basis J B ∧ M.relRank A B = (J \ I).encard
case intro
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : I ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ ∅ ⊆ Y ∧ Y ⊆ A}
⊢ ∃ I J, I ⊆ J ∧ M.Basis I A ∧ M.Basis J B ∧ M.relRank A B = (J \ I).encard