Theorem: Matroid.ModularCut.extendBy_deleteElem (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
he : e ∉ M.E
⊢ M.extendBy e U ＼ e = M
Tactic:
refine eq_of_indep_iff_indep_forall (by simpa) fun I hI ↦ ?_
State after:
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : e ∉ M.E
I : Set α
hI : I ⊆ (M.extendBy e U ＼ e).E
⊢ (M.extendBy e U ＼ e).Indep I ↔ M.Indep I

State before:
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : e ∉ M.E
I : Set α
hI : I ⊆ (M.extendBy e U ＼ e).E
⊢ (M.extendBy e U ＼ e).Indep I ↔ M.Indep I
Tactic:
obtain ⟨-, heI⟩ := show I ⊆ M.E ∧ e ∉ I by simpa [subset_diff] using hI
State after:
case intro
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : e ∉ M.E
I : Set α
hI : I ⊆ (M.extendBy e U ＼ e).E
heI : e ∉ I
⊢ (M.extendBy e U ＼ e).Indep I ↔ M.Indep I

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

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : e ∉ M.E
⊢ (M.extendBy e U ＼ e).E = M.E
Tactic:
simpa
State after:
no goals

State before:
α : Type u_1
M : Matroid α
I✝ J B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
he : e ∉ M.E
I : Set α
hI : I ⊆ (M.extendBy e U ＼ e).E
⊢ I ⊆ M.E ∧ e ∉ I
Tactic:
simpa [subset_diff] using hI
State after:
no goals