Theorem: Matroid.Flat.mem_covByPartition_iff (Matroid/Flat.lean)

State before:
α : Type u_1
M : Matroid α
I F X✝ Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
X : Set α
hF : M.Flat F
⊢ X ∈ hF.covByPartition ↔ ∃ F', (F ⋖[M] F') ∧ F' \ F = X
Tactic:
simp [Flat.covByPartition]
State after:
no goals