clear h
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 ∈ maximals (fun x x_1 => x ⊆ x_1) {A_1 | M.matroid.Indep A_1 ∧ A_1 ⊆ A}
right✝¹ : A ⊆ M.matroid.E
h : M.matroid.relRank A B = (J \ I).encard
hJ_basis_B : J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.matroid.Indep A ∧ A ⊆ B}
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
hI_basis_A : I ∈ maximals (fun x x_1 => x ⊆ x_1) {A_1 | M.matroid.Indep A_1 ∧ A_1 ⊆ A}
right✝¹ : A ⊆ M.matroid.E
hJ_basis_B : J ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.matroid.Indep A ∧ A ⊆ B}
right✝ : B ⊆ M.matroid.E
⊢ M.relRank A B = (J \ I).encard