rintro rfl
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
hk : ↑k ≤ E.encard
hX : X ⊆ E
⊢ X = E → ↑k ≤ X.encard
α : Type u_1
M : Matroid α
I B X C : Set α
k✝ : ℕ∞
k : ℕ
hk : ↑k ≤ X.encard
hX : X ⊆ X
⊢ ↑k ≤ X.encard