rwa [inter_eq_self_of_subset_left hXE]
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
h : ↑k ≤ X.encard ∧ X ⊆ E ∨ X = E
x✝ : ↑k ≤ X.encard ∧ X ⊆ E
hle : ↑k ≤ X.encard
hXE : X ⊆ E
⊢ ↑k ≤ (X ∩ E).encard
no goals