Theorem: Matroid.exists_eq_contract_indep_delete (Matroid/Minor/Basic.lean)

State before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C : Set α
⊢ ∃ I D, M.Basis I (C ∩ M.E) ∧ D ⊆ (M ／ I).E ∧ D ⊆ C ∧ M ／ C = M ／ I ＼ D
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis (C ∩ M.E)
State after:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C I : Set α
hI : M.Basis I (C ∩ M.E)
⊢ ∃ I D, M.Basis I (C ∩ M.E) ∧ D ⊆ (M ／ I).E ∧ D ⊆ C ∧ M ／ C = M ／ I ＼ D

State before:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C I : Set α
hI : M.Basis I (C ∩ M.E)
⊢ ∃ I D, M.Basis I (C ∩ M.E) ∧ D ⊆ (M ／ I).E ∧ D ⊆ C ∧ M ／ C = M ／ I ＼ D
Tactic:
use I, C \ I ∩ M.E, hI
State after:
case right
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C I : Set α
hI : M.Basis I (C ∩ M.E)
⊢ C \ I ∩ M.E ⊆ (M ／ I).E ∧ C \ I ∩ M.E ⊆ C ∧ M ／ C = M ／ I ＼ (C \ I ∩ M.E)

State before:
case right
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C I : Set α
hI : M.Basis I (C ∩ M.E)
⊢ C \ I ∩ M.E ⊆ (M ／ I).E ∧ C \ I ∩ M.E ⊆ C ∧ M ／ C = M ／ I ＼ (C \ I ∩ M.E)
Tactic:
rw [contract_ground, and_iff_right (inter_subset_left.trans diff_subset), diff_eq,
  diff_eq, inter_right_comm, inter_assoc, and_iff_right inter_subset_right,
  ← contract_inter_ground_eq, hI.contract_eq_contract_delete, diff_eq, inter_assoc]
State after:
no goals