rw [hinf.encard_eq]
case intro.refine'_1.refine'_2
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
x✝ : (E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard) ∧ X ⊆ E
h✝ : E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard
hXE : X ⊆ E
h : E.encard ≤ (X ∩ E).encard
hinf : X.Infinite
⊢ ↑k ≤ X.encard
case intro.refine'_1.refine'_2
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
x✝ : (E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard) ∧ X ⊆ E
h✝ : E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard
hXE : X ⊆ E
h : E.encard ≤ (X ∩ E).encard
hinf : X.Infinite
⊢ ↑k ≤ ⊤