Theorem: Matroid.contract_delete_comm (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₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
⊢ M ／ C ＼ D = M ＼ D ／ C
Tactic:
refine eq_of_indep_iff_indep_forall (by simp [diff_diff_comm]) (fun I hI ↦ ?_)
State after:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
I : Set α
hI : I ⊆ (M ／ C ＼ D).E
⊢ (M ／ C ＼ D).Indep I ↔ (M ＼ D ／ C).Indep I

State before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
I : Set α
hI : I ⊆ (M ／ C ＼ D).E
⊢ (M ／ C ＼ D).Indep I ↔ (M ＼ D ／ C).Indep I
Tactic:
rw [delete_ground, contract_ground, subset_diff, subset_diff] at hI
State after:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
I : Set α
hI : (I ⊆ M.E ∧ Disjoint I C) ∧ Disjoint I D
⊢ (M ／ C ＼ D).Indep I ↔ (M ＼ D ／ C).Indep I

State before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
I : Set α
hI : (I ⊆ M.E ∧ Disjoint I C) ∧ Disjoint I D
⊢ (M ／ C ＼ D).Indep I ↔ (M ＼ D ／ C).Indep I
Tactic:
simp only [delete_ground, contract_ground, delete_indep_iff, and_iff_left hI.2]
State after:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
I : Set α
hI : (I ⊆ M.E ∧ Disjoint I C) ∧ Disjoint I D
⊢ (M ／ C).Indep I ↔ (M ＼ D ／ C).Indep I

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

State before:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
I : Set α
hI : (I ⊆ M.E ∧ Disjoint I C) ∧ Disjoint I D
J : Set α
hJ : (M ＼ D).Basis' J C
⊢ (M ／ C).Indep I ↔ (M ＼ D ／ C).Indep I
Tactic:
have hJ' := hJ
State after:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
I : Set α
hI : (I ⊆ M.E ∧ Disjoint I C) ∧ Disjoint I D
J : Set α
hJ hJ' : (M ＼ D).Basis' J C
⊢ (M ／ C).Indep I ↔ (M ＼ D ／ C).Indep I

State before:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
I : Set α
hI : (I ⊆ M.E ∧ Disjoint I C) ∧ Disjoint I D
J : Set α
hJ hJ' : (M ＼ D).Basis' J C
⊢ (M ／ C).Indep I ↔ (M ＼ D ／ C).Indep I
Tactic:
rw [← restrict_compl, basis'_restrict_iff, subset_diff, diff_eq, inter_comm M.E, ← inter_assoc,
  ← diff_eq, sdiff_eq_left.2 hCD] at hJ'
State after:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
I : Set α
hI : (I ⊆ M.E ∧ Disjoint I C) ∧ Disjoint I D
J : Set α
hJ : (M ＼ D).Basis' J C
hJ' : M.Basis' J (C ∩ M.E) ∧ J ⊆ M.E ∧ Disjoint J D
⊢ (M ／ C).Indep I ↔ (M ＼ D ／ C).Indep I

State before:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
I : Set α
hI : (I ⊆ M.E ∧ Disjoint I C) ∧ Disjoint I D
J : Set α
hJ : (M ＼ D).Basis' J C
hJ' : M.Basis' J (C ∩ M.E) ∧ J ⊆ M.E ∧ Disjoint J D
⊢ (M ／ C).Indep I ↔ (M ＼ D ／ C).Indep I
Tactic:
rw [hJ.contract_eq_contract_delete, delete_indep_iff, hJ.indep.contract_indep_iff,
  delete_indep_iff, ← contract_inter_ground_eq, hJ'.1.contract_eq_contract_delete,
  delete_indep_iff,  hJ'.1.indep.contract_indep_iff, disjoint_union_left, and_iff_right hI.2,
  and_iff_left (disjoint_of_subset_right diff_subset hI.1.2), and_iff_left hJ'.2.2,
  and_iff_left
  (disjoint_of_subset_right (diff_subset.trans inter_subset_left) hI.1.2)]
State after:
no goals

State before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
⊢ (M ／ C ＼ D).E = (M ＼ D ／ C).E
Tactic:
simp [diff_diff_comm]
State after:
no goals