set B' := B \ {x}
case refine_2.intro
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x✝ : α
M : RankMatroid α
A✝ B✝ : Set α
hA✝ : A✝ ⊆ B✝
hB : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n✝ : ℕ∞
n : ℕ
hPn : P ↑n
A B : Set α
hA : A ⊆ B
hB_indep : M.Indep B
h : (B \ A).encard = ↑n.succ
this : (B \ A).encard > 0
x : α
hx : x ∈ B \ A
⊢ M.relRank A B = ↑n.succ
case refine_2.intro
α : Type u_1
A✝¹ B✝¹ I J X : Set α
M✝ : RankMatroid α
x✝ : α
M : RankMatroid α
A✝ B✝ : Set α
hA✝ : A✝ ⊆ B✝
hB : M.Indep B✝
P : ℕ∞ → Prop := fun n => ∀ (A B : Set α), A ⊆ B → M.Indep B → (B \ A).encard = n → M.relRank A B = n
n✝ : ℕ∞
n : ℕ
hPn : P ↑n
A B : Set α
hA : A ⊆ B
hB_indep : M.Indep B
h : (B \ A).encard = ↑n.succ
this : (B \ A).encard > 0
x : α
hx : x ∈ B \ A
B' : Set α := B \ {x}
⊢ M.relRank A B = ↑n.succ