Theorem: Matroid.cocircuit_iff_mem_minimals_compl_nonspanning (Matroid/Circuit.lean)

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ M.Cocircuit K ↔ K ∈ minimals (fun x x_1 => x ⊆ x_1) {X | ¬M.Spanning (M.E \ X)}
Tactic:
convert cocircuit_iff_mem_minimals with K
State after:
case h.e'_2.h.e'_5.h.e'_3.h.e'_2.h.a
α : Type u_1
M : Matroid α
C C' I X K✝ C₁ C₂ R : Set α
e f x y : α
B K : Set α
⊢ ¬M.Spanning (M.E \ K) ↔ ∀ (B : Set α), M.Base B → (K ∩ B).Nonempty

State before:
case h.e'_2.h.e'_5.h.e'_3.h.e'_2.h.a
α : Type u_1
M : Matroid α
C C' I X K✝ C₁ C₂ R : Set α
e f x y : α
B K : Set α
⊢ ¬M.Spanning (M.E \ K) ↔ ∀ (B : Set α), M.Base B → (K ∩ B).Nonempty
Tactic:
simp_rw [spanning_iff_superset_base (S := M.E \ K), not_exists, subset_diff, not_and,
  not_disjoint_iff_nonempty_inter, ← and_imp, and_iff_left_of_imp Base.subset_ground,
    inter_comm K]
State after:
no goals