refine ⟨fun ⟨⟨hB, hBk⟩, h⟩ ↦ ⟨hB, hBk.antisymm (le_of_not_lt fun hlt ↦ ?_)⟩,
  fun ⟨hB, hBk⟩ ↦ ⟨⟨ hB, hBk.le⟩,
    fun I _ hIk hBI ↦ ?_⟩ ⟩
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
⊢ ((M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I) ↔ M.Indep B ∧ B.encard = ↑k
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_2
α : Type u_1
M : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
x✝¹ : M.Indep B ∧ B.encard = ↑k
hB : M.Indep B
hBk : B.encard = ↑k
I : Set α
x✝ : M.Indep I
hIk : I.encard ≤ ↑k
hBI : B ⊆ I
⊢ B = I