have hJ_basis : M.Basis J B := by
  refine M.basis_of_maximal_extension hB hJ
case h
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
hIJ : I ⊆ J
hI_basis : M.Basis I A
⊢ I ⊆ J ∧
    (I ∈ maximals (fun x x_1 => x ⊆ x_1) {A_1 | M.Indep A_1 ∧ A_1 ⊆ A} ∧ A ⊆ M.E) ∧
      (J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.Indep A ∧ A ⊆ B} ∧ B ⊆ M.E) ∧ M.relRank A B = (J \ I).encard
case h
α : Type u_1
I✝ : Set α
M : Matroid α
A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I : Set α
hI : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset_A : I ⊆ A
right✝ : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
J : Set α
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {Y | M.Indep Y ∧ I ⊆ Y ∧ Y ⊆ B}
hIJ : I ⊆ J
hI_basis : M.Basis I A
hJ_basis : M.Basis J B
⊢ I ⊆ J ∧
    (I ∈ maximals (fun x x_1 => x ⊆ x_1) {A_1 | M.Indep A_1 ∧ A_1 ⊆ A} ∧ A ⊆ M.E) ∧
      (J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.Indep A ∧ A ⊆ B} ∧ B ⊆ M.E) ∧ M.relRank A B = (J \ I).encard