Theorem: Matroid.Circuit.subset_circuit_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₂ C K : Set α
hC : (M ／ K).Circuit C
⊢ ∃ C', M.Circuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis' K
State after:
case intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K : Set α
hC : (M ／ K).Circuit C
I : Set α
hI : M.Basis' I K
⊢ ∃ C', M.Circuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

State before:
case intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K : Set α
hC : (M ／ K).Circuit C
I : Set α
hI : M.Basis' I K
⊢ ∃ C', M.Circuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
Tactic:
rw [hI.contract_eq_contract_delete, delete_circuit_iff] at hC
State after:
case intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
⊢ ∃ C', M.Circuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

State before:
case intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
⊢ ∃ C', M.Circuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
Tactic:
have hCss := hC.1.subset_ground
State after:
case intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCss : C ⊆ (M ／ I).E
⊢ ∃ C', M.Circuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

State before:
case intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCss : C ⊆ (M ／ I).E
⊢ ∃ C', M.Circuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
Tactic:
rw [contract_ground, subset_diff] at hCss
State after:
case intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCss : C ⊆ M.E ∧ Disjoint C I
⊢ ∃ C', M.Circuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

State before:
case intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCss : C ⊆ M.E ∧ Disjoint C I
⊢ ∃ C', M.Circuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
Tactic:
obtain ⟨hCE, hCI⟩ := hCss
State after:
case intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
⊢ ∃ C', M.Circuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

State before:
case intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
⊢ ∃ C', M.Circuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
Tactic:
have hIE := hI.indep.subset_ground
State after:
case intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
⊢ ∃ C', M.Circuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

State before:
case intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
⊢ ∃ C', M.Circuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
Tactic:
have hCId : M.Dep (C ∪ I) := by
  rw [← not_indep_iff]; intro hd
  have hCi := hd.diff_indep_contract_of_subset subset_union_right
  rw [union_diff_right, sdiff_eq_left.2 hCI] at hCi
  exact hC.1.dep.not_indep hCi
State after:
case intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
hCId : M.Dep (C ∪ I)
⊢ ∃ C', M.Circuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

State before:
case intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
hCId : M.Dep (C ∪ I)
⊢ ∃ C', M.Circuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
Tactic:
obtain ⟨C', hC'CI, hC'⟩ := hCId.exists_circuit_subset
State after:
case intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
hCId : M.Dep (C ∪ I)
C' : Set α
hC'CI : C' ⊆ C ∪ I
hC' : M.Circuit C'
⊢ ∃ C', M.Circuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

State before:
case intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
hCId : M.Dep (C ∪ I)
C' : Set α
hC'CI : C' ⊆ C ∪ I
hC' : M.Circuit C'
⊢ ∃ C', M.Circuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
Tactic:
refine ⟨C', hC', ?_, hC'CI.trans (union_subset_union_right _ hI.subset)⟩
State after:
case intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
hCId : M.Dep (C ∪ I)
C' : Set α
hC'CI : C' ⊆ C ∪ I
hC' : M.Circuit C'
⊢ C ⊆ C'

State before:
case intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
hCId : M.Dep (C ∪ I)
C' : Set α
hC'CI : C' ⊆ C ∪ I
hC' : M.Circuit C'
⊢ C ⊆ C'
Tactic:
have hd := hC'.contract_dep_of_not_subset (C := I)
  (fun hC'I ↦ (hI.indep.subset hC'I).not_dep hC'.dep)
State after:
case intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
hCId : M.Dep (C ∪ I)
C' : Set α
hC'CI : C' ⊆ C ∪ I
hC' : M.Circuit C'
hd : (M ／ I).Dep (C' \ I)
⊢ C ⊆ C'

State before:
case intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
hCId : M.Dep (C ∪ I)
C' : Set α
hC'CI : C' ⊆ C ∪ I
hC' : M.Circuit C'
hd : (M ／ I).Dep (C' \ I)
⊢ C ⊆ C'
Tactic:
rw [← hC.1.eq_of_dep_subset hd (by simpa [diff_subset_iff, union_comm])]
State after:
case intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
hCId : M.Dep (C ∪ I)
C' : Set α
hC'CI : C' ⊆ C ∪ I
hC' : M.Circuit C'
hd : (M ／ I).Dep (C' \ I)
⊢ C' \ I ⊆ C'

State before:
case intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
hCId : M.Dep (C ∪ I)
C' : Set α
hC'CI : C' ⊆ C ∪ I
hC' : M.Circuit C'
hd : (M ／ I).Dep (C' \ I)
⊢ C' \ I ⊆ C'
Tactic:
exact diff_subset
State after:
no goals

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
⊢ M.Dep (C ∪ I)
Tactic:
rw [← not_indep_iff]
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
⊢ ¬M.Indep (C ∪ I)

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
⊢ ¬M.Indep (C ∪ I)
Tactic:
intro hd
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
hd : M.Indep (C ∪ I)
⊢ False

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
hd : M.Indep (C ∪ I)
⊢ False
Tactic:
have hCi := hd.diff_indep_contract_of_subset subset_union_right
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
hd : M.Indep (C ∪ I)
hCi : (M ／ I).Indep ((C ∪ I) \ I)
⊢ False

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
hd : M.Indep (C ∪ I)
hCi : (M ／ I).Indep ((C ∪ I) \ I)
⊢ False
Tactic:
rw [union_diff_right, sdiff_eq_left.2 hCI] at hCi
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
hd : M.Indep (C ∪ I)
hCi : (M ／ I).Indep C
⊢ False

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
hd : M.Indep (C ∪ I)
hCi : (M ／ I).Indep C
⊢ False
Tactic:
exact hC.1.dep.not_indep hCi
State after:
no goals

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z K✝ C✝ C₁ C₂ C K I : Set α
hC : (M ／ I).Circuit C ∧ Disjoint C (K \ I)
hI : M.Basis' I K
hCE : C ⊆ M.E
hCI : Disjoint C I
hIE : I ⊆ M.E
hCId : M.Dep (C ∪ I)
C' : Set α
hC'CI : C' ⊆ C ∪ I
hC' : M.Circuit C'
hd : (M ／ I).Dep (C' \ I)
⊢ C' \ I ⊆ C
Tactic:
simpa [diff_subset_iff, union_comm]
State after:
no goals