Theorem: Matroid.projectBy_indep_iff_of_ne_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
I : Set α
hU : U ≠ ⊤
⊢ (M.projectBy U).Indep I ↔ M.Indep I ∧ M.cl I ∉ U
Tactic:
simp [hU]
State after:
no goals