Theorem: Matroid.Hyperplane.basis_hyperplane_restrict (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 : α
hH : M.Hyperplane H
hI : M.Basis I H
⊢ (M ↾ (I ∪ M.E \ H)).Hyperplane I
Tactic:
convert hH.basis_hyperplane_delete hI using 1
State after:
case h.e'_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 : α
hH : M.Hyperplane H
hI : M.Basis I H
⊢ M ↾ (I ∪ M.E \ H) = M ＼ (H \ I)

State before:
case h.e'_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 : α
hH : M.Hyperplane H
hI : M.Basis I H
⊢ M ↾ (I ∪ M.E \ H) = M ＼ (H \ I)
Tactic:
rw [delete_eq_restrict, diff_diff_right, inter_eq_self_of_subset_right hI.indep.subset_ground,
  union_comm]
State after:
no goals