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

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b a' b' : ℕ
h : b ≤ a
⊢ unif a b = freeOn univ
Tactic:
simpa [eq_freeOn_iff]
State after:
no goals