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

State before:
α : Type u_1
M : Matroid α
E I B X C : Set α
k : ℕ∞
a b✝ a' b' b : ℕ
⊢ unif 0 b = loopyOn univ
Tactic:
simp [eq_loopyOn_iff]
State after:
no goals