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

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
⊢ (M ＼ e).extendBy e (ofDeleteElem M e) = M
Tactic:
refine Eq.symm <| eq_of_indep_iff_indep_forall (by simp [he]) fun I hI ↦ ?_
State after:
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
hI : I ⊆ M.E
⊢ M.Indep I ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep I

State before:
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
hI : I ⊆ M.E
⊢ M.Indep I ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep I
Tactic:
obtain (heI | heI) := em' (e ∈ I)
State after:
case inl
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
hI : I ⊆ M.E
heI : e ∉ I
⊢ M.Indep I ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep I

case inr
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
hI : I ⊆ M.E
heI : e ∈ I
⊢ M.Indep I ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep I

State before:
case inl
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
hI : I ⊆ M.E
heI : e ∉ I
⊢ M.Indep I ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep I

case inr
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
hI : I ⊆ M.E
heI : e ∈ I
⊢ M.Indep I ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep I
Tactic:
simp [extIndep_iff_of_not_mem heI, heI]
State after:
case inr
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
hI : I ⊆ M.E
heI : e ∈ I
⊢ M.Indep I ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep I

State before:
case inr
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
hI : I ⊆ M.E
heI : e ∈ I
⊢ M.Indep I ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep I
Tactic:
obtain ⟨I, rfl, heI'⟩ : ∃ J, I = insert e J ∧ e ∉ J := ⟨I \ {e}, by simp [heI], by simp⟩
State after:
case inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
⊢ M.Indep (insert e I) ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep (insert e I)

State before:
case inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
⊢ M.Indep (insert e I) ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep (insert e I)
Tactic:
suffices
  M.Indep (insert e I) ↔ M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I))) by
  simpa [extIndep_iff_of_mem heI, heI']
State after:
case inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))

State before:
case inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
⊢ M.Indep (insert e I) ↔ M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
Tactic:
refine ⟨fun h ↦ ⟨h.subset (subset_insert _ _), fun he _ ↦ ?_⟩, fun ⟨hIi, h⟩ ↦ ?_⟩
State after:
case inr.intro.intro.refine_1
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he✝ : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
h : M.Indep (insert e I)
he : e ∈ M.cl (M.cl I \ {e})
x✝ : M.Flat (insert e (M.cl I))
⊢ False

case inr.intro.intro.refine_2
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
x✝ : M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
hIi : M.Indep I
h : e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I))
⊢ M.Indep (insert e I)

State before:
case inr.intro.intro.refine_2
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
x✝ : M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
hIi : M.Indep I
h : e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I))
⊢ M.Indep (insert e I)
Tactic:
rw [hIi.insert_indep_iff_of_not_mem heI', mem_diff, and_iff_right (hI (.inl rfl))]
State after:
case inr.intro.intro.refine_2
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
x✝ : M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
hIi : M.Indep I
h : e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I))
⊢ e ∉ M.cl I

State before:
case inr.intro.intro.refine_2
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
x✝ : M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
hIi : M.Indep I
h : e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I))
⊢ e ∉ M.cl I
Tactic:
refine fun heCl ↦ ?_
State after:
case inr.intro.intro.refine_2
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
x✝ : M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
hIi : M.Indep I
h : e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I))
heCl : e ∈ M.cl I
⊢ False

State before:
case inr.intro.intro.refine_2
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
x✝ : M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
hIi : M.Indep I
h : e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I))
heCl : e ∈ M.cl I
⊢ False
Tactic:
simp only [heCl, insert_eq_of_mem, cl_flat, not_true_eq_false, imp_false] at h
State after:
case inr.intro.intro.refine_2
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
x✝ : M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
hIi : M.Indep I
heCl : e ∈ M.cl I
h : e ∉ M.cl (M.cl I \ {e})
⊢ False

State before:
case inr.intro.intro.refine_2
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
x✝ : M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
hIi : M.Indep I
heCl : e ∈ M.cl I
h : e ∉ M.cl (M.cl I \ {e})
⊢ False
Tactic:
exact h <| (M.cl_subset_cl <| subset_diff_singleton (M.subset_cl I hIi.subset_ground) heI') heCl
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
he : e ∈ M.E
⊢ M.E = ((M ＼ e).extendBy e (ofDeleteElem M e)).E
Tactic:
simp [he]
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
he : e ∈ M.E
I : Set α
hI : I ⊆ M.E
heI : e ∈ I
⊢ I = insert e (I \ {e})
Tactic:
simp [heI]
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
he : e ∈ M.E
I : Set α
hI : I ⊆ M.E
heI : e ∈ I
⊢ e ∉ I \ {e}
Tactic:
simp
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
he : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
this : M.Indep (insert e I) ↔ M.Indep I ∧ (e ∈ M.cl (M.cl I \ {e}) → ¬M.Flat (insert e (M.cl I)))
⊢ M.Indep (insert e I) ↔ ((M ＼ e).extendBy e (ofDeleteElem M e)).Indep (insert e I)
Tactic:
simpa [extIndep_iff_of_mem heI, heI']
State after:
no goals

State before:
case inr.intro.intro.refine_1
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he✝ : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
h : M.Indep (insert e I)
he : e ∈ M.cl (M.cl I \ {e})
x✝ : M.Flat (insert e (M.cl I))
⊢ False
Tactic:
suffices e ∈ M.cl (M.cl I) from h.not_mem_cl_diff_of_mem (.inl rfl) <| by simpa [heI']
State after:
case inr.intro.intro.refine_1
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he✝ : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
h : M.Indep (insert e I)
he : e ∈ M.cl (M.cl I \ {e})
x✝ : M.Flat (insert e (M.cl I))
⊢ e ∈ M.cl (M.cl I)

State before:
case inr.intro.intro.refine_1
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
he✝ : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
h : M.Indep (insert e I)
he : e ∈ M.cl (M.cl I \ {e})
x✝ : M.Flat (insert e (M.cl I))
⊢ e ∈ M.cl (M.cl I)
Tactic:
exact (M.cl_subset_cl diff_subset) he
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
he✝ : e ∈ M.E
I : Set α
heI' : e ∉ I
hI : insert e I ⊆ M.E
heI : e ∈ insert e I
h : M.Indep (insert e I)
he : e ∈ M.cl (M.cl I \ {e})
x✝ : M.Flat (insert e (M.cl I))
this : e ∈ M.cl (M.cl I)
⊢ e ∈ M.cl (insert e I \ {e})
Tactic:
simpa [heI']
State after:
no goals