internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Circuit.contract_dep_of_not_subset
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C✝ C₁ C₂ : Set α
hK : M.Circuit K
C : Set α
hKC : ¬K ⊆ C
⊢ C ∩ K ≠ K
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Circuit.contract_diff_circuit
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hC : M.Circuit C
hK : K.Nonempty
hKC : K ⊆ C
⊢ (M ／ (C \ K)).Circuit K
Tactic:
simpa [inter_eq_self_of_subset_right hKC] using hC.contract_circuit (diff_ssubset hKC hK)
Proof state after:
no goals
Theorem: Matroid.Circuit.subset_circuit_of_contract
Proof 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
Proof 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
Theorem: Matroid.Circuit.subset_circuit_of_contract
Proof 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
Proof 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
Theorem: Matroid.Circuit.subset_circuit_of_contract
Proof 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
Proof 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
Theorem: Matroid.Circuit.subset_circuit_of_contract
Proof 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
Proof 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
Theorem: Matroid.Circuit.subset_circuit_of_contract
Proof 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
Proof 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
Theorem: Matroid.Circuit.subset_circuit_of_contract
Proof 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
Proof 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
Theorem: Matroid.Circuit.subset_circuit_of_contract
Proof 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
Proof 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
Theorem: Matroid.Circuit.subset_circuit_of_contract
Proof 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
Proof 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
Theorem: Matroid.Circuit.subset_circuit_of_contract
Proof 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)⟩
Proof 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'
Theorem: Matroid.Circuit.subset_circuit_of_contract
Proof 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)
Proof 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'
Theorem: Matroid.Circuit.subset_circuit_of_contract
Proof 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])]
Proof 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'
Theorem: Matroid.Circuit.subset_circuit_of_contract
Proof 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
Proof state after:
no goals
Theorem: Matroid.Circuit.subset_circuit_of_contract
Proof 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]
Proof 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)
Theorem: Matroid.Circuit.subset_circuit_of_contract
Proof 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
Proof 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
Theorem: Matroid.Circuit.subset_circuit_of_contract
Proof 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
Proof 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
Theorem: Matroid.Circuit.subset_circuit_of_contract
Proof 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
Proof 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
Theorem: Matroid.Circuit.subset_circuit_of_contract
Proof 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
Proof state after:
no goals
Theorem: Matroid.Circuit.subset_circuit_of_contract
Proof 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]
Proof state after:
no goals
Theorem: Matroid.Dep.of_contract
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : (M ／ C).Dep X
hC : autoParam (C ⊆ M.E) _auto✝
⊢ M.Dep (C ∪ X)
Tactic:
rw [Dep, and_iff_left (union_subset hC (h.subset_ground.trans diff_subset))]
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : (M ／ C).Dep X
hC : autoParam (C ⊆ M.E) _auto✝
⊢ ¬M.Indep (C ∪ X)
Theorem: Matroid.Dep.of_contract
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : (M ／ C).Dep X
hC : autoParam (C ⊆ M.E) _auto✝
⊢ ¬M.Indep (C ∪ X)
Tactic:
intro hi
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : (M ／ C).Dep X
hC : autoParam (C ⊆ M.E) _auto✝
hi : M.Indep (C ∪ X)
⊢ False
Theorem: Matroid.Dep.of_contract
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : (M ／ C).Dep X
hC : autoParam (C ⊆ M.E) _auto✝
hi : M.Indep (C ∪ X)
⊢ False
Tactic:
rw [Dep, (hi.subset subset_union_left).contract_indep_iff, union_comm,
  and_iff_left hi] at h
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : ¬Disjoint X C ∧ X ⊆ (M ／ C).E
hC : autoParam (C ⊆ M.E) _auto✝
hi : M.Indep (C ∪ X)
⊢ False
Theorem: Matroid.Dep.of_contract
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : ¬Disjoint X C ∧ X ⊆ (M ／ C).E
hC : autoParam (C ⊆ M.E) _auto✝
hi : M.Indep (C ∪ X)
⊢ False
Tactic:
exact h.1 (subset_diff.1 h.2).2
Proof state after:
no goals
Theorem: Matroid.Basis.diff_subset_loops_contract
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hIX : M.Basis I X
⊢ X \ I ⊆ (M ／ I).cl ∅
Tactic:
rw [diff_subset_iff, contract_loops_eq, union_diff_self,
  union_eq_self_of_subset_left (M.subset_cl I)]
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hIX : M.Basis I X
⊢ X ⊆ M.cl I
Theorem: Matroid.Basis.diff_subset_loops_contract
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hIX : M.Basis I X
⊢ X ⊆ M.cl I
Tactic:
exact hIX.subset_cl
Proof state after:
no goals
Theorem: Matroid.contract_spanning_iff'
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
⊢ (M ／ C).Spanning X ↔ M.Spanning (X ∪ C ∩ M.E) ∧ Disjoint X C
Tactic:
simp_rw [Spanning, contract_cl_eq, contract_ground, subset_diff, union_subset_iff,
  and_iff_left inter_subset_right, ← and_assoc, and_congr_left_iff,
  subset_antisymm_iff, subset_diff, diff_subset_iff, and_iff_left disjoint_sdiff_left,
  and_iff_right (M.cl_subset_ground _ ),
  and_iff_right (subset_union_of_subset_right (M.cl_subset_ground _) C)]
Proof state after:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
⊢ Disjoint X C → X ⊆ M.E → (M.E ⊆ C ∪ M.cl (X ∪ C) ↔ M.E ⊆ M.cl (X ∪ C ∩ M.E))
Theorem: Matroid.contract_spanning_iff'
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
⊢ Disjoint X C → X ⊆ M.E → (M.E ⊆ C ∪ M.cl (X ∪ C) ↔ M.E ⊆ M.cl (X ∪ C ∩ M.E))
Tactic:
rw [← inter_eq_left (s := M.E), inter_union_distrib_left,
  inter_eq_self_of_subset_right (M.cl_subset_ground _), subset_antisymm_iff, union_subset_iff,
  and_iff_right inter_subset_left, union_eq_self_of_subset_left (s := M.E ∩ C),
  and_iff_right (M.cl_subset_ground _), Iff.comm, ← cl_union_cl_right_eq,cl_inter_ground,
  cl_union_cl_right_eq]
Proof state after:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
⊢ Disjoint X C → X ⊆ M.E → (M.E ⊆ M.cl (X ∪ C) ↔ M.E ⊆ M.cl (X ∪ C))

α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
⊢ M.E ∩ C ⊆ M.cl (X ∪ C)
Theorem: Matroid.contract_spanning_iff'
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
⊢ M.E ∩ C ⊆ M.cl (X ∪ C)
Tactic:
exact (M.subset_cl _).trans
  (M.cl_subset_cl (inter_subset_right.trans subset_union_right))
Proof state after:
no goals
Theorem: Matroid.contract_spanning_iff'
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
⊢ Disjoint X C → X ⊆ M.E → (M.E ⊆ M.cl (X ∪ C) ↔ M.E ⊆ M.cl (X ∪ C))
Tactic:
exact fun _ _ ↦ Iff.rfl
Proof state after:
no goals
Theorem: Matroid.contract_spanning_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hC : autoParam (C ⊆ M.E) _auto✝
⊢ (M ／ C).Spanning X ↔ M.Spanning (X ∪ C) ∧ Disjoint X C
Tactic:
rw [contract_spanning_iff', inter_eq_self_of_subset_left hC]
Proof state after:
no goals
Theorem: Matroid.Nonloop.of_contract
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : (M ／ C).Nonloop e
⊢ M.Nonloop e
Tactic:
rw [← indep_singleton] at h ⊢
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : (M ／ C).Indep {e}
⊢ M.Indep {e}
Theorem: Matroid.Nonloop.of_contract
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : (M ／ C).Indep {e}
⊢ M.Indep {e}
Tactic:
exact h.of_contract
Proof state after:
no goals
Theorem: Matroid.contract_nonloop_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
⊢ (M ／ C).Nonloop e ↔ e ∈ M.E \ M.cl C
Tactic:
rw [nonloop_iff_mem_compl_loops, contract_ground, contract_loops_eq]
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
⊢ e ∈ (M.E \ C) \ (M.cl C \ C) ↔ e ∈ M.E \ M.cl C
Theorem: Matroid.contract_nonloop_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
⊢ e ∈ (M.E \ C) \ (M.cl C \ C) ↔ e ∈ M.E \ M.cl C
Tactic:
refine ⟨fun ⟨he,heC⟩ ↦ ⟨he.1, fun h ↦ heC ⟨h, he.2⟩⟩,
  fun h ↦ ⟨⟨h.1, fun heC ↦ h.2 ?_⟩, fun h' ↦ h.2 h'.1⟩⟩
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : e ∈ M.E \ M.cl C
heC : e ∈ C
⊢ e ∈ M.cl C
Theorem: Matroid.contract_nonloop_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : e ∈ M.E \ M.cl C
heC : e ∈ C
⊢ e ∈ M.cl C
Tactic:
rw [← cl_inter_ground]
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : e ∈ M.E \ M.cl C
heC : e ∈ C
⊢ e ∈ M.cl (C ∩ M.E)
Theorem: Matroid.contract_nonloop_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : e ∈ M.E \ M.cl C
heC : e ∈ C
⊢ e ∈ M.cl (C ∩ M.E)
Tactic:
exact (M.subset_cl (C ∩ M.E)) ⟨heC, h.1⟩
Proof state after:
no goals
Theorem: Matroid.Cocircuit.of_contract
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hK : (M ／ C).Cocircuit K
⊢ M.Cocircuit K
Tactic:
rw [cocircuit_def, contract_dual_eq_dual_delete] at hK
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hK : (M✶ ＼ C).Circuit K
⊢ M.Cocircuit K
Theorem: Matroid.Cocircuit.of_contract
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hK : (M✶ ＼ C).Circuit K
⊢ M.Cocircuit K
Tactic:
exact hK.of_delete
Proof state after:
no goals
Theorem: Matroid.Cocircuit.delete_cocircuit
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ D : Set α
hK : M.Cocircuit K
hD : D ⊂ K
⊢ (M ＼ D).Cocircuit (K \ D)
Tactic:
rw [cocircuit_def, delete_dual_eq_dual_contract]
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ D : Set α
hK : M.Cocircuit K
hD : D ⊂ K
⊢ (M✶ ／ D).Circuit (K \ D)
Theorem: Matroid.Cocircuit.delete_cocircuit
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ D : Set α
hK : M.Cocircuit K
hD : D ⊂ K
⊢ (M✶ ／ D).Circuit (K \ D)
Tactic:
exact hK.circuit.contract_circuit hD
Proof state after:
no goals
Theorem: Matroid.Cocircuit.delete_diff_cocircuit
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X✝ Y Z K C C₁ C₂ X : Set α
hK : M.Cocircuit K
hXK : X ⊆ K
hX : X.Nonempty
⊢ (M ＼ (K \ X)).Cocircuit X
Tactic:
rw [cocircuit_def, delete_dual_eq_dual_contract]
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X✝ Y Z K C C₁ C₂ X : Set α
hK : M.Cocircuit K
hXK : X ⊆ K
hX : X.Nonempty
⊢ (M✶ ／ (K \ X)).Circuit X
Theorem: Matroid.Cocircuit.delete_diff_cocircuit
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X✝ Y Z K C C₁ C₂ X : Set α
hK : M.Cocircuit K
hXK : X ⊆ K
hX : X.Nonempty
⊢ (M✶ ／ (K \ X)).Circuit X
Tactic:
exact hK.circuit.contract_diff_circuit hX hXK
Proof state after:
no goals
Theorem: Matroid.contract_delete_diff
Proof 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 α
⊢ M ／ C ＼ D = M ／ C ＼ (D \ C)
Tactic:
rw [delete_eq_delete_iff, contract_ground, diff_eq, diff_eq, ← inter_inter_distrib_right,
  inter_assoc]
Proof state after:
no goals
Theorem: Matroid.contract_restrict_eq_restrict_contract
Proof 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 R : Set α
h : Disjoint C R
⊢ M ／ C ↾ R = (M ↾ (R ∪ C)) ／ C
Tactic:
refine eq_of_indep_iff_indep_forall (by simp [h.sdiff_eq_right]) (fun I _ ↦ ?_)
Proof 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 R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
⊢ (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I
Theorem: Matroid.contract_restrict_eq_restrict_contract
Proof 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 R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
⊢ (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I
Tactic:
obtain ⟨J, hJ⟩ := (M ↾ (R ∪ C)).exists_basis' C
Proof 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 R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
⊢ (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I
Theorem: Matroid.contract_restrict_eq_restrict_contract
Proof 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 R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
⊢ (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I
Tactic:
have hJ' : M.Basis' J C := by
  have := (basis'_restrict_iff.1 hJ).1
  rwa [inter_eq_self_of_subset_left subset_union_right] at this
Proof 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 R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
hJ' : M.Basis' J C
⊢ (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I
Theorem: Matroid.contract_restrict_eq_restrict_contract
Proof 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 R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
hJ' : M.Basis' J C
⊢ (M ／ C ↾ R).Indep I ↔ ((M ↾ (R ∪ C)) ／ C).Indep I
Tactic:
rw [restrict_indep_iff, hJ.contract_indep_iff, hJ'.contract_indep_iff, restrict_indep_iff,
  union_subset_iff, and_iff_left (hJ.subset.trans subset_union_right), union_comm R C,
  ← diff_subset_iff, and_assoc, and_assoc, and_congr_right_iff, and_comm, and_congr_left_iff]
Proof 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 R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
hJ' : M.Basis' J C
⊢ M.Indep (I ∪ J) → Disjoint C I → (I ⊆ R ↔ I \ C ⊆ R)
Theorem: Matroid.contract_restrict_eq_restrict_contract
Proof 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 R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
hJ' : M.Basis' J C
⊢ M.Indep (I ∪ J) → Disjoint C I → (I ⊆ R ↔ I \ C ⊆ R)
Tactic:
intro _ hd
Proof 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 R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
hJ' : M.Basis' J C
a✝ : M.Indep (I ∪ J)
hd : Disjoint C I
⊢ I ⊆ R ↔ I \ C ⊆ R