Theorem: Matroid.Indep.of_contract (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 α
hI : (M ／ C).Indep I
⊢ M.Indep I
Tactic:
obtain ⟨J, R, hJ, -, -, hM⟩ := M.exists_eq_contract_indep_delete C
State after:
case intro.intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I J✝ R✝ B X Y Z K C C₁ C₂ : Set α
hI : (M ／ C).Indep I
J R : Set α
hJ : M.Basis J (C ∩ M.E)
hM : M ／ C = M ／ J ＼ R
⊢ M.Indep I

State before:
case intro.intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I J✝ R✝ B X Y Z K C C₁ C₂ : Set α
hI : (M ／ C).Indep I
J R : Set α
hJ : M.Basis J (C ∩ M.E)
hM : M ／ C = M ／ J ＼ R
⊢ M.Indep I
Tactic:
rw [hM, delete_indep_iff, hJ.indep.contract_indep_iff] at hI
State after:
case intro.intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I J✝ R✝ B X Y Z K C C₁ C₂ J R : Set α
hI : (Disjoint I J ∧ M.Indep (I ∪ J)) ∧ Disjoint I R
hJ : M.Basis J (C ∩ M.E)
hM : M ／ C = M ／ J ＼ R
⊢ M.Indep I

State before:
case intro.intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I J✝ R✝ B X Y Z K C C₁ C₂ J R : Set α
hI : (Disjoint I J ∧ M.Indep (I ∪ J)) ∧ Disjoint I R
hJ : M.Basis J (C ∩ M.E)
hM : M ／ C = M ／ J ＼ R
⊢ M.Indep I
Tactic:
exact hI.1.2.subset subset_union_left
State after:
no goals