Theorem: Matroid.Minor.exists_contract_indep_delete_coindep (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 D, M.Indep C ∧ M.Coindep D ∧ Disjoint C D ∧ N = M ／ C ＼ D
Tactic:
obtain ⟨C', D', hC', hD', hCD', rfl⟩ := h
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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
⊢ ∃ C D, M.Indep C ∧ M.Coindep D ∧ Disjoint C D ∧ M ／ C' ＼ D' = M ／ C ＼ D

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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
⊢ ∃ C D, M.Indep C ∧ M.Coindep D ∧ Disjoint C D ∧ M ／ C' ＼ D' = M ／ C ＼ D
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis C'
State after:
case intro.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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
⊢ ∃ C D, M.Indep C ∧ M.Coindep D ∧ Disjoint C D ∧ M ／ C' ＼ D' = M ／ C ＼ D

State before:
case intro.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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
⊢ ∃ C D, M.Indep C ∧ M.Coindep D ∧ Disjoint C D ∧ M ／ C' ＼ D' = M ／ C ＼ D
Tactic:
obtain ⟨K, hK⟩ := M✶.exists_basis D'
State after:
case intro.intro.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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
⊢ ∃ C D, M.Indep C ∧ M.Coindep D ∧ Disjoint C D ∧ M ／ C' ＼ D' = M ／ C ＼ D

State before:
case intro.intro.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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
⊢ ∃ C D, M.Indep C ∧ M.Coindep D ∧ Disjoint C D ∧ M ／ C' ＼ D' = M ／ C ＼ D
Tactic:
have hIK : Disjoint I K := disjoint_of_subset hI.subset hK.subset hCD'
State after:
case intro.intro.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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ ∃ C D, M.Indep C ∧ M.Coindep D ∧ Disjoint C D ∧ M ／ C' ＼ D' = M ／ C ＼ D

State before:
case intro.intro.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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ ∃ C D, M.Indep C ∧ M.Coindep D ∧ Disjoint C D ∧ M ／ C' ＼ D' = M ／ C ＼ D
Tactic:
use I ∪ D' \ K, C' \ I ∪ K
State after:
case h
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ M.Indep (I ∪ D' \ K) ∧
    M.Coindep (C' \ I ∪ K) ∧ Disjoint (I ∪ D' \ K) (C' \ I ∪ K) ∧ M ／ C' ＼ D' = M ／ (I ∪ D' \ K) ＼ (C' \ I ∪ K)

State before:
case h
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ M.Indep (I ∪ D' \ K) ∧
    M.Coindep (C' \ I ∪ K) ∧ Disjoint (I ∪ D' \ K) (C' \ I ∪ K) ∧ M ／ C' ＼ D' = M ／ (I ∪ D' \ K) ＼ (C' \ I ∪ K)
Tactic:
refine' ⟨_, _, _, _⟩
State after:
case h.refine'_1
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ M.Indep (I ∪ D' \ K)

case h.refine'_2
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ M.Coindep (C' \ I ∪ K)

case h.refine'_3
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ Disjoint (I ∪ D' \ K) (C' \ I ∪ K)

case h.refine'_4
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ M ／ C' ＼ D' = M ／ (I ∪ D' \ K) ＼ (C' \ I ∪ K)

State before:
case h.refine'_4
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ M ／ C' ＼ D' = M ／ (I ∪ D' \ K) ＼ (C' \ I ∪ K)
Tactic:
have hb : (M ／ C')✶.Basis K D' :=
  by
  rw [contract_dual_eq_dual_delete, delete_basis_iff, and_iff_right hK]
  exact hCD'.symm
State after:
case h.refine'_4
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
hb : (M ／ C')✶.Basis K D'
⊢ M ／ C' ＼ D' = M ／ (I ∪ D' \ K) ＼ (C' \ I ∪ K)

State before:
case h.refine'_4
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
hb : (M ／ C')✶.Basis K D'
⊢ M ／ C' ＼ D' = M ／ (I ∪ D' \ K) ＼ (C' \ I ∪ K)
Tactic:
rw [← dual_dual (M ／ C' ＼ D'), delete_dual_eq_dual_contract, hb.contract_eq_contract_delete,
  hI.contract_eq_contract_delete, delete_dual_eq_dual_contract, contract_dual_eq_dual_delete,
  dual_dual, delete_delete, contract_delete_contract]
State after:
case h.refine'_4.h
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
hb : (M ／ C')✶.Basis K D'
⊢ Disjoint (D' \ K) (C' \ I ∪ K)

State before:
case h.refine'_4.h
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
hb : (M ／ C')✶.Basis K D'
⊢ Disjoint (D' \ K) (C' \ I ∪ K)
Tactic:
rw [disjoint_union_right, and_iff_left disjoint_sdiff_left]
State after:
case h.refine'_4.h
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
hb : (M ／ C')✶.Basis K D'
⊢ Disjoint (D' \ K) (C' \ I)

State before:
case h.refine'_4.h
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
hb : (M ／ C')✶.Basis K D'
⊢ Disjoint (D' \ K) (C' \ I)
Tactic:
exact disjoint_of_subset diff_subset diff_subset hCD'.symm
State after:
no goals

State before:
case h.refine'_1
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ M.Indep (I ∪ D' \ K)
Tactic:
have hss : (D' \ K) \ I ⊆ (M✶ ／ K ＼ I).cl ∅ := by
  rw [delete_loops_eq];
  exact diff_subset_diff_left hK.diff_subset_loops_contract
State after:
case h.refine'_1
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
hss : (D' \ K) \ I ⊆ (M✶ ／ K ＼ I).cl ∅
⊢ M.Indep (I ∪ D' \ K)

State before:
case h.refine'_1
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
hss : (D' \ K) \ I ⊆ (M✶ ／ K ＼ I).cl ∅
⊢ M.Indep (I ∪ D' \ K)
Tactic:
rw [← delete_dual_eq_dual_contract, ← contract_dual_eq_dual_delete] at hss
State after:
case h.refine'_1
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
hss : (D' \ K) \ I ⊆ (M ＼ K ／ I)✶.cl ∅
⊢ M.Indep (I ∪ D' \ K)

State before:
case h.refine'_1
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
hss : (D' \ K) \ I ⊆ (M ＼ K ／ I)✶.cl ∅
⊢ M.Indep (I ∪ D' \ K)
Tactic:
have hi := indep_of_subset_coloops hss
State after:
case h.refine'_1
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
hss : (D' \ K) \ I ⊆ (M ＼ K ／ I)✶.cl ∅
hi : (M ＼ K ／ I).Indep ((D' \ K) \ I)
⊢ M.Indep (I ∪ D' \ K)

State before:
case h.refine'_1
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
hss : (D' \ K) \ I ⊆ (M ＼ K ／ I)✶.cl ∅
hi : (M ＼ K ／ I).Indep ((D' \ K) \ I)
⊢ M.Indep (I ∪ D' \ K)
Tactic:
rw [← contract_delete_comm _ hIK, delete_indep_iff, hI.indep.contract_indep_iff,
  diff_union_self, union_comm] at hi
State after:
case h.refine'_1
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
hss : (D' \ K) \ I ⊆ (M ＼ K ／ I)✶.cl ∅
hi : (Disjoint ((D' \ K) \ I) I ∧ M.Indep (I ∪ D' \ K)) ∧ Disjoint ((D' \ K) \ I) K
⊢ M.Indep (I ∪ D' \ K)

State before:
case h.refine'_1
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
hss : (D' \ K) \ I ⊆ (M ＼ K ／ I)✶.cl ∅
hi : (Disjoint ((D' \ K) \ I) I ∧ M.Indep (I ∪ D' \ K)) ∧ Disjoint ((D' \ K) \ I) K
⊢ M.Indep (I ∪ D' \ K)
Tactic:
exact hi.1.2
State after:
no goals

State before:
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ (D' \ K) \ I ⊆ (M✶ ／ K ＼ I).cl ∅
Tactic:
rw [delete_loops_eq]
State after:
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ (D' \ K) \ I ⊆ (M✶ ／ K).cl ∅ \ I

State before:
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ (D' \ K) \ I ⊆ (M✶ ／ K).cl ∅ \ I
Tactic:
exact diff_subset_diff_left hK.diff_subset_loops_contract
State after:
no goals

State before:
case h.refine'_2
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ M.Coindep (C' \ I ∪ K)
Tactic:
rw [coindep_def]
State after:
case h.refine'_2
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ M✶.Indep (C' \ I ∪ K)

State before:
case h.refine'_2
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ M✶.Indep (C' \ I ∪ K)
Tactic:
have hss : (C' \ I) \ K ⊆ (M ／ I ＼ K)✶✶.cl ∅ := by
  rw [dual_dual, delete_loops_eq];
  exact diff_subset_diff_left hI.diff_subset_loops_contract
State after:
case h.refine'_2
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
hss : (C' \ I) \ K ⊆ (M ／ I ＼ K)✶✶.cl ∅
⊢ M✶.Indep (C' \ I ∪ K)

State before:
case h.refine'_2
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
hss : (C' \ I) \ K ⊆ (M ／ I ＼ K)✶✶.cl ∅
⊢ M✶.Indep (C' \ I ∪ K)
Tactic:
have hi := indep_of_subset_coloops hss
State after:
case h.refine'_2
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
hss : (C' \ I) \ K ⊆ (M ／ I ＼ K)✶✶.cl ∅
hi : (M ／ I ＼ K)✶.Indep ((C' \ I) \ K)
⊢ M✶.Indep (C' \ I ∪ K)

State before:
case h.refine'_2
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
hss : (C' \ I) \ K ⊆ (M ／ I ＼ K)✶✶.cl ∅
hi : (M ／ I ＼ K)✶.Indep ((C' \ I) \ K)
⊢ M✶.Indep (C' \ I ∪ K)
Tactic:
rw [delete_dual_eq_dual_contract, contract_dual_eq_dual_delete, ←
  contract_delete_comm _ hIK.symm, delete_indep_iff, hK.indep.contract_indep_iff,
  diff_union_self] at hi
State after:
case h.refine'_2
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
hss : (C' \ I) \ K ⊆ (M ／ I ＼ K)✶✶.cl ∅
hi : (Disjoint ((C' \ I) \ K) K ∧ M✶.Indep (C' \ I ∪ K)) ∧ Disjoint ((C' \ I) \ K) I
⊢ M✶.Indep (C' \ I ∪ K)

State before:
case h.refine'_2
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
hss : (C' \ I) \ K ⊆ (M ／ I ＼ K)✶✶.cl ∅
hi : (Disjoint ((C' \ I) \ K) K ∧ M✶.Indep (C' \ I ∪ K)) ∧ Disjoint ((C' \ I) \ K) I
⊢ M✶.Indep (C' \ I ∪ K)
Tactic:
exact hi.1.2
State after:
no goals

State before:
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ (C' \ I) \ K ⊆ (M ／ I ＼ K)✶✶.cl ∅
Tactic:
rw [dual_dual, delete_loops_eq]
State after:
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ (C' \ I) \ K ⊆ (M ／ I).cl ∅ \ K

State before:
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ (C' \ I) \ K ⊆ (M ／ I).cl ∅ \ K
Tactic:
exact diff_subset_diff_left hI.diff_subset_loops_contract
State after:
no goals

State before:
case h.refine'_3
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ Disjoint (I ∪ D' \ K) (C' \ I ∪ K)
Tactic:
rw [disjoint_union_left, disjoint_union_right, disjoint_union_right,
  and_iff_right disjoint_sdiff_right, and_iff_right hIK, and_iff_left disjoint_sdiff_left]
State after:
case h.refine'_3
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ Disjoint (D' \ K) (C' \ I)

State before:
case h.refine'_3
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ Disjoint (D' \ K) (C' \ I)
Tactic:
exact disjoint_of_subset diff_subset diff_subset hCD'.symm
State after:
no goals

State before:
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ (M ／ C')✶.Basis K D'
Tactic:
rw [contract_dual_eq_dual_delete, delete_basis_iff, and_iff_right hK]
State after:
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ Disjoint D' C'

State before:
α : 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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
K : Set α
hK : M✶.Basis K D'
hIK : Disjoint I K
⊢ Disjoint D' C'
Tactic:
exact hCD'.symm
State after:
no goals