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

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
h : E.encard ≤ k
⊢ unifOn E k = freeOn E
Tactic:
rw [unifOn, truncate_eq_self_of_rk_le (by rwa [freeOn_erk_eq])]
State after:
no goals

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
h : E.encard ≤ k
⊢ (freeOn E).erk ≤ k
Tactic:
rwa [freeOn_erk_eq]
State after:
no goals