Theorem: Matroid.Base.hyperplane_of_cl_diff_singleton (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 : α
hB : M.Base B
heB : e ∈ B
⊢ M.Hyperplane (M.cl (B \ {e}))
Tactic:
rw [hyperplane_iff_covBy, Flat.covBy_iff_eq_cl_insert (M.cl_flat _)]
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 : α
hB : M.Base B
heB : e ∈ B
⊢ ∃ e_1 ∈ M.E \ M.cl (B \ {e}), M.E = M.cl (insert e_1 (M.cl (B \ {e})))

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 : α
hB : M.Base B
heB : e ∈ B
⊢ ∃ e_1 ∈ M.E \ M.cl (B \ {e}), M.E = M.cl (insert e_1 (M.cl (B \ {e})))
Tactic:
refine' ⟨e, ⟨hB.subset_ground heB, _⟩, _⟩
State after:
case refine'_1
α : 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 : α
hB : M.Base B
heB : e ∈ B
⊢ e ∉ M.cl (B \ {e})

case refine'_2
α : 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 : α
hB : M.Base B
heB : e ∈ B
⊢ M.E = M.cl (insert e (M.cl (B \ {e})))

State before:
case refine'_2
α : 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 : α
hB : M.Base B
heB : e ∈ B
⊢ M.E = M.cl (insert e (M.cl (B \ {e})))
Tactic:
simpa [insert_eq_of_mem heB] using hB.cl_eq.symm
State after:
no goals

State before:
case refine'_1
α : 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 : α
hB : M.Base B
heB : e ∈ B
⊢ e ∉ M.cl (B \ {e})
Tactic:
rw [(hB.indep.diff {e}).not_mem_cl_iff (hB.subset_ground heB)]
State after:
case refine'_1
α : 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 : α
hB : M.Base B
heB : e ∈ B
⊢ M.Indep (insert e (B \ {e})) ∧ e ∉ B \ {e}

State before:
case refine'_1
α : 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 : α
hB : M.Base B
heB : e ∈ B
⊢ M.Indep (insert e (B \ {e})) ∧ e ∉ B \ {e}
Tactic:
simpa [insert_eq_of_mem heB] using hB.indep
State after:
no goals