Theorem: Matroid.ModularCut.eq_bot_or_ground_mem (Matroid/Extension.lean)

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
⊢ U = ⊥ ∨ M.E ∈ U
Tactic:
obtain (hU | ⟨F, hF⟩) := (U : Set (Set α)).eq_empty_or_nonempty
State after:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hU : ↑U = ∅
⊢ U = ⊥ ∨ M.E ∈ U

case inr.intro
α : Type u_1
M : Matroid α
I J B F₀ F✝ F' X Y : Set α
e f : α
U✝ U : M.ModularCut
F : Set α
hF : F ∈ ↑U
⊢ U = ⊥ ∨ M.E ∈ U

State before:
case inr.intro
α : Type u_1
M : Matroid α
I J B F₀ F✝ F' X Y : Set α
e f : α
U✝ U : M.ModularCut
F : Set α
hF : F ∈ ↑U
⊢ U = ⊥ ∨ M.E ∈ U
Tactic:
exact .inr <| U.superset_mem hF M.ground_flat (U.flat_of_mem hF).subset_ground
State after:
no goals

State before:
case inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hU : ↑U = ∅
⊢ U = ⊥ ∨ M.E ∈ U
Tactic:
left
State after:
case inl.h
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hU : ↑U = ∅
⊢ U = ⊥

State before:
case inl.h
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hU : ↑U = ∅
⊢ U = ⊥
Tactic:
ext x
State after:
case inl.h.carrier.h
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hU : ↑U = ∅
x : Set α
⊢ x ∈ U.carrier ↔ x ∈ ⊥.carrier

State before:
case inl.h.carrier.h
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hU : ↑U = ∅
x : Set α
⊢ x ∈ U.carrier ↔ x ∈ ⊥.carrier
Tactic:
change x ∈ (U : Set (Set α)) ↔ x ∈ ∅
State after:
case inl.h.carrier.h
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hU : ↑U = ∅
x : Set α
⊢ x ∈ ↑U ↔ x ∈ ∅

State before:
case inl.h.carrier.h
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hU : ↑U = ∅
x : Set α
⊢ x ∈ ↑U ↔ x ∈ ∅
Tactic:
simp [hU]
State after:
no goals