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

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ U = ⊤ ↔ M.cl ∅ ∈ U
Tactic:
refine ⟨?_, fun h ↦ ?_⟩
State after:
case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ U = ⊤ → M.cl ∅ ∈ U

case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : M.cl ∅ ∈ U
⊢ U = ⊤

State before:
case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : M.cl ∅ ∈ U
⊢ U = ⊤
Tactic:
simp only [SetLike.ext_iff, mem_top_iff]
State after:
case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : M.cl ∅ ∈ U
⊢ ∀ (x : Set α), x ∈ U ↔ M.Flat x

State before:
case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : M.cl ∅ ∈ U
⊢ ∀ (x : Set α), x ∈ U ↔ M.Flat x
Tactic:
refine fun F ↦ ⟨U.flat_of_mem, fun h' ↦ U.superset_mem h h' h'.loops_subset⟩
State after:
no goals

State before:
case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ U = ⊤ → M.cl ∅ ∈ U
Tactic:
rintro rfl
State after:
case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
⊢ M.cl ∅ ∈ ⊤

State before:
case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
⊢ M.cl ∅ ∈ ⊤
Tactic:
exact ⟨M.cl_flat ∅, empty_subset _⟩
State after:
no goals