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

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
h : N ≤m M
⊢ ∃ C, M.Indep C ∧ N ≤r M ／ C ∧ (M ／ C).cl N.E = (M ／ C).E
Tactic:
obtain ⟨C, D, hC, hD, hCD, rfl⟩ := h.exists_contract_indep_delete_coindep
State after:
case intro.intro.intro.intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
C D : Set α
hC : M.Indep C
hD : M.Coindep D
hCD : Disjoint C D
h : M ／ C ＼ D ≤m M
⊢ ∃ C_1, M.Indep C_1 ∧ M ／ C ＼ D ≤r M ／ C_1 ∧ (M ／ C_1).cl (M ／ C ＼ D).E = (M ／ C_1).E

State before:
case intro.intro.intro.intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
C D : Set α
hC : M.Indep C
hD : M.Coindep D
hCD : Disjoint C D
h : M ／ C ＼ D ≤m M
⊢ ∃ C_1, M.Indep C_1 ∧ M ／ C ＼ D ≤r M ／ C_1 ∧ (M ／ C_1).cl (M ／ C ＼ D).E = (M ／ C_1).E
Tactic:
refine' ⟨C, hC, delete_restriction _ _, _⟩
State after:
case intro.intro.intro.intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
C D : Set α
hC : M.Indep C
hD : M.Coindep D
hCD : Disjoint C D
h : M ／ C ＼ D ≤m M
⊢ (M ／ C).cl (M ／ C ＼ D).E = (M ／ C).E

State before:
case intro.intro.intro.intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
C D : Set α
hC : M.Indep C
hD : M.Coindep D
hCD : Disjoint C D
h : M ／ C ＼ D ≤m M
⊢ (M ／ C).cl (M ／ C ＼ D).E = (M ／ C).E
Tactic:
rw [← (hD.coindep_contract_of_disjoint hCD.symm).cl_compl, delete_ground]
State after:
no goals