Theorem: Matroid.principal_ground_ne_top (Matroid/Extension.lean)

State before:
α : Type u_1
M✝ : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M✝.ModularCut
M : Matroid α
inst✝ : M.RkPos
⊢ ModularCut.principal M M.E ≠ ⊤
Tactic:
simp only [Ne, ModularCut.eq_top_iff, ModularCut.mem_principal_iff, cl_flat, true_and]
State after:
α : Type u_1
M✝ : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M✝.ModularCut
M : Matroid α
inst✝ : M.RkPos
⊢ ¬M.E ⊆ M.cl ∅

State before:
α : Type u_1
M✝ : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M✝.ModularCut
M : Matroid α
inst✝ : M.RkPos
⊢ ¬M.E ⊆ M.cl ∅
Tactic:
obtain ⟨B, hB⟩ := M.exists_base
State after:
case intro
α : Type u_1
M✝ : Matroid α
I J B✝ F₀ F F' X Y : Set α
e f : α
U : M✝.ModularCut
M : Matroid α
inst✝ : M.RkPos
B : Set α
hB : M.Base B
⊢ ¬M.E ⊆ M.cl ∅

State before:
case intro
α : Type u_1
M✝ : Matroid α
I J B✝ F₀ F F' X Y : Set α
e f : α
U : M✝.ModularCut
M : Matroid α
inst✝ : M.RkPos
B : Set α
hB : M.Base B
⊢ ¬M.E ⊆ M.cl ∅
Tactic:
obtain ⟨e, heB⟩ := hB.nonempty
State after:
case intro.intro
α : Type u_1
M✝ : Matroid α
I J B✝ F₀ F F' X Y : Set α
e✝ f : α
U : M✝.ModularCut
M : Matroid α
inst✝ : M.RkPos
B : Set α
hB : M.Base B
e : α
heB : e ∈ B
⊢ ¬M.E ⊆ M.cl ∅

State before:
case intro.intro
α : Type u_1
M✝ : Matroid α
I J B✝ F₀ F F' X Y : Set α
e✝ f : α
U : M✝.ModularCut
M : Matroid α
inst✝ : M.RkPos
B : Set α
hB : M.Base B
e : α
heB : e ∈ B
⊢ ¬M.E ⊆ M.cl ∅
Tactic:
exact fun h ↦ (hB.indep.nonloop_of_mem heB).not_loop <| h (hB.subset_ground heB)
State after:
no goals