rw [h _ (hB'.indep.subset hJB') h'.le hBJ] at hlt
case refine_1.intro.intro.intro.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'
J : Set α
hBJ : B ⊆ J
hJB' : J ⊆ B'
h' : J.encard = ↑k
⊢ False
case refine_1.intro.intro.intro.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
B' : Set α
hB' : M.Base B'
hJB'✝ : B ⊆ B'
J : Set α
hlt : J.encard < ↑k
hBJ : B ⊆ J
hJB' : J ⊆ B'
h' : J.encard = ↑k
⊢ False