Theorem: Matroid.projectBy_top (Matroid/Extension.lean)

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ M.projectBy ⊤ = M
Tactic:
simp [eq_iff_indep_iff_indep_forall]
State after:
no goals