obtain ⟨B', hB', hJB'⟩ := hB.exists_base_superset
case refine_1
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝ : (M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hB : M.Indep B
hBk : B.encard ≤ ↑k
h : ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hlt : B.encard < ↑k
⊢ False
case refine_1.intro.intro
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝ : (M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hB : M.Indep B
hBk : B.encard ≤ ↑k
h : ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I
hlt : B.encard < ↑k
B' : Set α
hB' : M.Base B'
hJB' : B ⊆ B'
⊢ False