Theorem: Matroid.loops_covBy_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 : α
⊢ M.cl ∅ ⋖[M] P ↔ M.Point P
Tactic:
simp only [covBy_iff_relRank_eq_one, cl_flat, relRank_cl_left, relRank_empty_left, true_and,
  and_congr_right_iff, and_iff_right_iff_imp]
State after:
α : 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 : α
⊢ M.Flat P → M.er P = 1 → M.cl ∅ ⊆ P

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 : α
⊢ M.Flat P → M.er P = 1 → M.cl ∅ ⊆ P
Tactic:
exact fun h _ ↦ h.cl_subset_of_subset (empty_subset _)
State after:
no goals