Theorem: Matroid.exists_mem_cl_not_mem_of_not_flat (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 : α
h : ¬M.Flat F
hF : autoParam (F ⊆ M.E) _auto✝
⊢ ∃ e, e ∈ M.cl F \ F
Tactic:
rw [flat_iff_cl_self, subset_antisymm_iff, and_iff_left (M.subset_cl F)] at h
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 : α
h : ¬M.cl F ⊆ F
hF : autoParam (F ⊆ M.E) _auto✝
⊢ ∃ e, e ∈ M.cl F \ F

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 : α
h : ¬M.cl F ⊆ F
hF : autoParam (F ⊆ M.E) _auto✝
⊢ ∃ e, e ∈ M.cl F \ F
Tactic:
exact not_subset.1 h
State after:
no goals