simp only [matroid_Indep, Set.mem_setOf_eq, and_imp] at hI_basis_A hJ_basis_B
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
hI_basis_A :
  I ∈
    {a |
      a ∈ {A_1 | M.matroid.Indep A_1 ∧ A_1 ⊆ A} ∧
        ∀ ⦃b : Set α⦄,
          b ∈ {A_1 | M.matroid.Indep A_1 ∧ A_1 ⊆ A} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}
right✝¹ : A ⊆ M.matroid.E
hJ_basis_B :
  J ∈
    {a |
      a ∈ {A | M.matroid.Indep A ∧ A ⊆ B} ∧
        ∀ ⦃b : Set α⦄, b ∈ {A | M.matroid.Indep A ∧ A ⊆ B} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}
right✝ : B ⊆ M.matroid.E
⊢ M.relRank A B = (J \ I).encard
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_basis_A : (M.Indep I ∧ I ⊆ A) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hJ_basis_B : (M.Indep J ∧ J ⊆ B) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
⊢ M.relRank A B = (J \ I).encard