Theorem: Matroid.ModularCut.mem_delete_elem_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 ∈ U.delete {e} ↔ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)
Tactic:
rw [ModularCut.delete, ModularCut.restrict, ModularCut.mem_mk_iff, mem_setOf_eq,
  ← delete_eq_restrict, ← deleteElem, flat_deleteElem_iff]
State after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U ↔ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl 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.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U ↔ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)
Tactic:
constructor
State after:
case mp
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U → e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)

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

State before:
case mp
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U → e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)

case mpr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F) → (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U
Tactic:
rintro ⟨⟨heF, (hF | hF)⟩, hFU⟩
State after:
case mp.intro.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat F
⊢ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)

case mp.intro.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
⊢ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)

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

State before:
case mpr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
⊢ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F) → (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U
Tactic:
rintro ⟨heF, (hFU | hFU)⟩
State after:
case mpr.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hFU : F ∈ U
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U

case mpr.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hFU : insert e F ∈ U ∧ e ∈ M.cl F
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U

State before:
case mpr.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hFU : insert e F ∈ U ∧ e ∈ M.cl F
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U
Tactic:
have hfl := U.flat_of_mem hFU.1
State after:
case mpr.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hFU : insert e F ∈ U ∧ e ∈ M.cl F
hfl : M.Flat (insert e F)
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U

State before:
case mpr.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hFU : insert e F ∈ U ∧ e ∈ M.cl F
hfl : M.Flat (insert e F)
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U
Tactic:
rw [← hfl.cl, ← cl_insert_cl_eq_cl_insert, insert_eq_of_mem hFU.2, cl_cl] at hFU
State after:
case mpr.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hFU : M.cl F ∈ U ∧ e ∈ M.cl F
hfl : M.Flat (insert e F)
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U

State before:
case mpr.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hFU : M.cl F ∈ U ∧ e ∈ M.cl F
hfl : M.Flat (insert e F)
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U
Tactic:
exact ⟨⟨heF, .inr hfl⟩, hFU.1⟩
State after:
no goals

State before:
case mp.intro.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat F
⊢ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)
Tactic:
rw [hF.cl] at hFU
State after:
case mp.intro.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : F ∈ U
heF : e ∉ F
hF : M.Flat F
⊢ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)

State before:
case mp.intro.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : F ∈ U
heF : e ∉ F
hF : M.Flat F
⊢ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)
Tactic:
exact ⟨heF, .inl hFU⟩
State after:
no goals

State before:
case mp.intro.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
⊢ e ∉ F ∧ (F ∈ U ∨ insert e F ∈ U ∧ e ∈ M.cl F)
Tactic:
rw [← hF.cl]
State after:
case mp.intro.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)

State before:
case mp.intro.intro.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Tactic:
obtain (heF' | heF') := em (e ∈ M.cl F)
State after:
case mp.intro.intro.inr.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∈ M.cl F
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)

case mp.intro.intro.inr.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)

State before:
case mp.intro.intro.inr.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Tactic:
have hF' : M.Flat F := by
  have hFE := ((subset_insert _ _).trans hF.subset_ground)
  rw [flat_iff_subset_cl_self]
  refine (subset_diff_singleton (M.cl_subset_cl (subset_insert e F)) heF').trans ?_
  simp [hF.cl]
State after:
case mp.intro.intro.inr.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
hF' : M.Flat F
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)

State before:
case mp.intro.intro.inr.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
hF' : M.Flat F
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Tactic:
rw [hF'.cl] at hFU
State after:
case mp.intro.intro.inr.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
hF' : M.Flat F
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)

State before:
case mp.intro.intro.inr.inr
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
hF' : M.Flat F
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Tactic:
exact ⟨heF, .inl hFU⟩
State after:
no goals

State before:
case mp.intro.intro.inr.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∈ M.cl F
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Tactic:
rw [← insert_eq_of_mem heF'] at hFU
State after:
case mp.intro.intro.inr.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : insert e (M.cl F) ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∈ M.cl F
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)

State before:
case mp.intro.intro.inr.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : insert e (M.cl F) ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∈ M.cl F
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Tactic:
replace hFU := U.cl_mem_of_mem hFU
State after:
case mp.intro.intro.inr.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∈ M.cl F
hFU : M.cl (insert e (M.cl F)) ∈ U
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)

State before:
case mp.intro.intro.inr.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∈ M.cl F
hFU : M.cl (insert e (M.cl F)) ∈ U
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Tactic:
rw [cl_insert_cl_eq_cl_insert] at hFU
State after:
case mp.intro.intro.inr.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∈ M.cl F
hFU : M.cl (insert e F) ∈ U
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)

State before:
case mp.intro.intro.inr.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∈ M.cl F
hFU : M.cl (insert e F) ∈ U
⊢ e ∉ F ∧ (F ∈ U ∨ M.cl (insert e F) ∈ U ∧ e ∈ M.cl F)
Tactic:
exact ⟨heF, .inr ⟨hFU, heF'⟩⟩
State after:
no goals

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
⊢ M.Flat F
Tactic:
have hFE := ((subset_insert _ _).trans hF.subset_ground)
State after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
hFE : F ⊆ M.E
⊢ M.Flat F

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
hFE : F ⊆ M.E
⊢ M.Flat F
Tactic:
rw [flat_iff_subset_cl_self]
State after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
hFE : F ⊆ M.E
⊢ M.cl F ⊆ F

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
hFE : F ⊆ M.E
⊢ M.cl F ⊆ F
Tactic:
refine (subset_diff_singleton (M.cl_subset_cl (subset_insert e F)) heF').trans ?_
State after:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
hFE : F ⊆ M.E
⊢ M.cl (insert e F) \ {e} ⊆ F

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hFU : M.cl F ∈ U
heF : e ∉ F
hF : M.Flat (insert e F)
heF' : e ∉ M.cl F
hFE : F ⊆ M.E
⊢ M.cl (insert e F) \ {e} ⊆ F
Tactic:
simp [hF.cl]
State after:
no goals

State before:
case mpr.intro.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heF : e ∉ F
hFU : F ∈ U
⊢ (e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))) ∧ M.cl F ∈ U
Tactic:
simpa [(U.flat_of_mem hFU), heF, (U.flat_of_mem hFU).cl]
State after:
no goals