Theorem: Matroid.exists_of_cl_ssubset (Matroid/Closure.lean)

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hXY : M.cl X ⊂ M.cl Y
⊢ ∃ e ∈ Y, e ∉ M.cl X
Tactic:
by_contra! hcon
State after:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hXY : M.cl X ⊂ M.cl Y
hcon : ∀ e ∈ Y, e ∈ M.cl X
⊢ False

State before:
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e f x y : α
hXY : M.cl X ⊂ M.cl Y
hcon : ∀ e ∈ Y, e ∈ M.cl X
⊢ False
Tactic:
exact hXY.not_subset (M.cl_subset_cl_of_subset_cl hcon)
State after:
no goals