rw [← (hfin.inter_of_left E).eq_of_subset_of_encard_le' inter_subset_right h,
  inter_eq_self_of_subset_left hXE]
case intro.refine'_1.refine'_1
α : 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
hfin : X.Finite
⊢ X = E
no goals