Theorem: Matroid.unifOn_indep_iff (Matroid/Constructions/Uniform.lean)

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
⊢ (unifOn E k).Indep I ↔ I.encard ≤ k ∧ I ⊆ E
Tactic:
simp [unifOn, and_comm]
State after:
no goals