Theorem: Matroid.flat_deleteElem_iff (Matroid/Flat.lean)

State before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
⊢ (M ＼ e).Flat F ↔ e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))
Tactic:
rw [deleteElem, flat_delete_iff]
State after:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
⊢ (∃ F', M.Flat F' ∧ F = F' \ {e}) ↔ e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))

State before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
⊢ (∃ F', M.Flat F' ∧ F = F' \ {e}) ↔ e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))
Tactic:
constructor
State after:
case mp
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
⊢ (∃ F', M.Flat F' ∧ F = F' \ {e}) → e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))

case mpr
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
⊢ e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F)) → ∃ F', M.Flat F' ∧ F = F' \ {e}

State before:
case mpr
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
⊢ e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F)) → ∃ F', M.Flat F' ∧ F = F' \ {e}
Tactic:
rintro ⟨heF, (hF | hF)⟩ <;> exact ⟨_, hF, by simp [heF]⟩
State after:
no goals

State before:
case mp
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
⊢ (∃ F', M.Flat F' ∧ F = F' \ {e}) → e ∉ F ∧ (M.Flat F ∨ M.Flat (insert e F))
Tactic:
rintro ⟨F, hF, rfl⟩
State after:
case mp.intro.intro
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
F : Set α
hF : M.Flat F
⊢ e ∉ F \ {e} ∧ (M.Flat (F \ {e}) ∨ M.Flat (insert e (F \ {e})))

State before:
case mp.intro.intro
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
F : Set α
hF : M.Flat F
⊢ e ∉ F \ {e} ∧ (M.Flat (F \ {e}) ∨ M.Flat (insert e (F \ {e})))
Tactic:
obtain (heF | heF) := em (e ∈ F) <;> simp [heF, hF]
State after:
no goals

State before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
heF : e ∉ F
hF : M.Flat (insert e F)
⊢ F = insert e F \ {e}
Tactic:
simp [heF]
State after:
no goals