Theorem: Matroid.mem_ofDeleteElem_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
⊢ F ∈ ModularCut.ofDeleteElem M e ↔ e ∈ M.cl F \ F ∧ M.Flat (insert e F)
Tactic:
simp only [deleteElem, mem_ofDeleteElem_iff, mem_diff]
State after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ e ∉ F ∧ M.cl F = insert e F ↔ (e ∈ M.cl F ∧ e ∉ F) ∧ M.Flat (insert e F)

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

case refine_2
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : (e ∈ M.cl F ∧ e ∉ F) ∧ M.Flat (insert e F)
⊢ M.cl F = insert e F

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 : (e ∈ M.cl F ∧ e ∉ F) ∧ M.Flat (insert e F)
⊢ M.cl F = insert e F
Tactic:
rw [← h.2.cl, ← cl_insert_cl_eq_cl_insert, insert_eq_of_mem h.1.1, cl_cl]
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
h : e ∉ F ∧ M.cl F = insert e F
⊢ (e ∈ M.cl F ∧ e ∉ F) ∧ M.Flat (insert e F)
Tactic:
rw [← h.2, and_iff_left <| M.cl_flat F, and_iff_left h.1, h.2]
State after:
case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : e ∉ F ∧ M.cl F = insert e F
⊢ e ∈ insert e F

State before:
case refine_1
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
h : e ∉ F ∧ M.cl F = insert e F
⊢ e ∈ insert e F
Tactic:
exact mem_insert _ _
State after:
no goals