by_contra! h_finite
case refine_3
α : 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 : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
h : (B \ A).encard = ⊤
⊢ M.relRank A B = ⊤
case refine_3
α : 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 : ℕ∞
hP : ∀ (n : ℕ), P ↑n
A B : Set α
hB : A ⊆ B
hA_indep : M.Indep B
h : (B \ A).encard = ⊤
h_finite : M.relRank A B ≠ ⊤
⊢ False