internlm/Lean-Github huggingface dataset:
Theorem: Matroid.contract_eq_delete_of_subset_loops
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hX : X ⊆ M.cl ∅
⊢ X ⊆ M✶✶.cl ∅
Tactic:
rwa [dual_dual]
Proof state after:
no goals
Theorem: Matroid.Basis.contract_eq_contract_delete
Proof 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.Basis I X
⊢ M ／ X = M ／ I ＼ (X \ I)
Tactic:
nth_rw 1 [← diff_union_of_subset hI.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 α
hI : M.Basis I X
⊢ M ／ (X \ I ∪ I) = M ／ I ＼ (X \ I)
Theorem: Matroid.Basis.contract_eq_contract_delete
Proof 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.Basis I X
⊢ M ／ (X \ I ∪ I) = M ／ I ＼ (X \ I)
Tactic:
rw [union_comm, ← contract_contract]
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Basis I X
⊢ M ／ I ／ (X \ I) = M ／ I ＼ (X \ I)
Theorem: Matroid.Basis.contract_eq_contract_delete
Proof 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.Basis I X
⊢ M ／ I ／ (X \ I) = M ／ I ＼ (X \ I)
Tactic:
refine' contract_eq_delete_of_subset_loops fun e he ↦ _
Proof state after:
α : Type u_1
M M' N : Matroid α
e✝ f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Basis I X
e : α
he : e ∈ X \ I
⊢ e ∈ (M ／ I).cl ∅
Theorem: Matroid.Basis.contract_eq_contract_delete
Proof 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.Basis I X
e : α
he : e ∈ X \ I
⊢ e ∈ (M ／ I).cl ∅
Tactic:
rw [← loop_iff_mem_cl_empty, ← singleton_dep, hI.indep.contract_dep_iff,
  disjoint_singleton_left, and_iff_right he.2, singleton_union,
  ← hI.indep.mem_cl_iff_of_not_mem he.2]
Proof state after:
α : Type u_1
M M' N : Matroid α
e✝ f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Basis I X
e : α
he : e ∈ X \ I
⊢ e ∈ M.cl I
Theorem: Matroid.Basis.contract_eq_contract_delete
Proof 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.Basis I X
e : α
he : e ∈ X \ I
⊢ e ∈ M.cl I
Tactic:
exact hI.subset_cl he.1
Proof state after:
no goals
Theorem: Matroid.Basis'.contract_eq_contract_delete
Proof 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.Basis' I X
⊢ M ／ X = M ／ I ＼ (X \ I)
Tactic:
rw [← contract_inter_ground_eq, hI.basis_inter_ground.contract_eq_contract_delete, eq_comm,
  ← delete_inter_ground_eq, contract_ground, diff_eq, diff_eq, ← inter_inter_distrib_right,
  ← diff_eq]
Proof state after:
no goals
Theorem: Matroid.Basis'.contract_indep_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 α
hI : M.Basis' I X
⊢ (M ／ X).Indep J ↔ M.Indep (J ∪ I) ∧ Disjoint X J
Tactic:
rw [hI.contract_eq_contract_delete, delete_indep_iff, hI.indep.contract_indep_iff,
  and_comm, ← and_assoc, ← disjoint_union_right, diff_union_self,
  union_eq_self_of_subset_right hI.subset, and_comm, disjoint_comm]
Proof state after:
no goals
Theorem: Matroid.contract_cl_eq_contract_delete
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 : Set α
⊢ M ／ M.cl C = M ／ C ＼ (M.cl C \ C)
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis_inter_ground_basis_cl C
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₂ : Set α
M : Matroid α
C I : Set α
hI : M.Basis I (C ∩ M.E) ∧ M.Basis I (M.cl C)
⊢ M ／ M.cl C = M ／ C ＼ (M.cl C \ C)
Theorem: Matroid.contract_cl_eq_contract_delete
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₂ : Set α
M : Matroid α
C I : Set α
hI : M.Basis I (C ∩ M.E) ∧ M.Basis I (M.cl C)
⊢ M ／ M.cl C = M ／ C ＼ (M.cl C \ C)
Tactic:
rw [hI.2.contract_eq_contract_delete, ← M.contract_inter_ground_eq C,
  hI.1.contract_eq_contract_delete, delete_delete]
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₂ : Set α
M : Matroid α
C I : Set α
hI : M.Basis I (C ∩ M.E) ∧ M.Basis I (M.cl C)
⊢ M ／ I ＼ (M.cl C \ I) = M ／ I ＼ ((C ∩ M.E) \ I ∪ M.cl C \ C)
Theorem: Matroid.contract_cl_eq_contract_delete
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₂ : Set α
M : Matroid α
C I : Set α
hI : M.Basis I (C ∩ M.E) ∧ M.Basis I (M.cl C)
⊢ M ／ I ＼ (M.cl C \ I) = M ／ I ＼ ((C ∩ M.E) \ I ∪ M.cl C \ C)
Tactic:
convert rfl using 2
Proof state after:
case h.e'_3.h.e'_5
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C I : Set α
hI : M.Basis I (C ∩ M.E) ∧ M.Basis I (M.cl C)
⊢ (C ∩ M.E) \ I ∪ M.cl C \ C = M.cl C \ I
Theorem: Matroid.contract_cl_eq_contract_delete
Proof state before:
case h.e'_3.h.e'_5
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C I : Set α
hI : M.Basis I (C ∩ M.E) ∧ M.Basis I (M.cl C)
⊢ (C ∩ M.E) \ I ∪ M.cl C \ C = M.cl C \ I
Tactic:
rw [union_comm, diff_eq (t := I), union_inter_distrib_left, union_inter_distrib_left,
  diff_union_self, union_eq_self_of_subset_left (diff_subset.trans (M.cl_subset_ground _)),
    union_inter_distrib_right, diff_eq, inter_eq_self_of_subset_left (M.cl_subset_ground _),
    ← cl_inter_ground, union_eq_self_of_subset_right (M.subset_cl (C ∩ M.E)),
    inter_union_distrib_left, ← inter_assoc, inter_self, ← inter_union_distrib_left,
    ← compl_inter, ← diff_eq,
    inter_eq_self_of_subset_right (hI.1.subset.trans inter_subset_left)]
Proof state after:
no goals
Theorem: Matroid.exists_eq_contract_indep_delete
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 : Set α
⊢ ∃ I D, M.Basis I (C ∩ M.E) ∧ D ⊆ (M ／ I).E ∧ D ⊆ C ∧ M ／ C = M ／ I ＼ D
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis (C ∩ M.E)
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₂ : Set α
M : Matroid α
C I : Set α
hI : M.Basis I (C ∩ M.E)
⊢ ∃ I D, M.Basis I (C ∩ M.E) ∧ D ⊆ (M ／ I).E ∧ D ⊆ C ∧ M ／ C = M ／ I ＼ D
Theorem: Matroid.exists_eq_contract_indep_delete
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₂ : Set α
M : Matroid α
C I : Set α
hI : M.Basis I (C ∩ M.E)
⊢ ∃ I D, M.Basis I (C ∩ M.E) ∧ D ⊆ (M ／ I).E ∧ D ⊆ C ∧ M ／ C = M ／ I ＼ D
Tactic:
use I, C \ I ∩ M.E, hI
Proof state after:
case right
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C I : Set α
hI : M.Basis I (C ∩ M.E)
⊢ C \ I ∩ M.E ⊆ (M ／ I).E ∧ C \ I ∩ M.E ⊆ C ∧ M ／ C = M ／ I ＼ (C \ I ∩ M.E)
Theorem: Matroid.exists_eq_contract_indep_delete
Proof state before:
case right
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C I : Set α
hI : M.Basis I (C ∩ M.E)
⊢ C \ I ∩ M.E ⊆ (M ／ I).E ∧ C \ I ∩ M.E ⊆ C ∧ M ／ C = M ／ I ＼ (C \ I ∩ M.E)
Tactic:
rw [contract_ground, and_iff_right (inter_subset_left.trans diff_subset), diff_eq,
  diff_eq, inter_right_comm, inter_assoc, and_iff_right inter_subset_right,
  ← contract_inter_ground_eq, hI.contract_eq_contract_delete, diff_eq, inter_assoc]
Proof state after:
no goals
Theorem: Matroid.Indep.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 α
hI : (M ／ C).Indep I
⊢ M.Indep I
Tactic:
obtain ⟨J, R, hJ, -, -, hM⟩ := M.exists_eq_contract_indep_delete C
Proof 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
Theorem: Matroid.Indep.of_contract
Proof 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
Proof 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
Theorem: Matroid.Indep.of_contract
Proof 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
Proof state after:
no goals
Theorem: Matroid.contract_loop_iff_mem_cl
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).Loop e ↔ e ∈ M.cl C \ C
Tactic:
obtain ⟨I, D, hI, -, -, hM⟩ := M.exists_eq_contract_indep_delete C
Proof 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₂ I D : Set α
hI : M.Basis I (C ∩ M.E)
hM : M ／ C = M ／ I ＼ D
⊢ (M ／ C).Loop e ↔ e ∈ M.cl C \ C
Theorem: Matroid.contract_loop_iff_mem_cl
Proof 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₂ I D : Set α
hI : M.Basis I (C ∩ M.E)
hM : M ／ C = M ／ I ＼ D
⊢ (M ／ C).Loop e ↔ e ∈ M.cl C \ C
Tactic:
rw [hM, delete_loop_iff, ← singleton_dep, hI.indep.contract_dep_iff, disjoint_singleton_left,
  singleton_union, hI.indep.insert_dep_iff, mem_diff, ← M.cl_inter_ground C, hI.cl_eq_cl,
  and_comm (a := e ∉ I), and_self_right, ← mem_diff, ← mem_diff, diff_diff]
Proof 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₂ I D : Set α
hI : M.Basis I (C ∩ M.E)
hM : M ／ C = M ／ I ＼ D
⊢ e ∈ M.cl (C ∩ M.E) \ (I ∪ D) ↔ e ∈ M.cl (C ∩ M.E) \ C
Theorem: Matroid.contract_loop_iff_mem_cl
Proof 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₂ I D : Set α
hI : M.Basis I (C ∩ M.E)
hM : M ／ C = M ／ I ＼ D
⊢ e ∈ M.cl (C ∩ M.E) \ (I ∪ D) ↔ e ∈ M.cl (C ∩ M.E) \ C
Tactic:
apply_fun Matroid.E at hM
Proof 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₂ I D : Set α
hI : M.Basis I (C ∩ M.E)
hM : (M ／ C).E = (M ／ I ＼ D).E
⊢ e ∈ M.cl (C ∩ M.E) \ (I ∪ D) ↔ e ∈ M.cl (C ∩ M.E) \ C
Theorem: Matroid.contract_loop_iff_mem_cl
Proof 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₂ I D : Set α
hI : M.Basis I (C ∩ M.E)
hM : (M ／ C).E = (M ／ I ＼ D).E
⊢ e ∈ M.cl (C ∩ M.E) \ (I ∪ D) ↔ e ∈ M.cl (C ∩ M.E) \ C
Tactic:
rw [delete_ground, contract_ground, contract_ground, diff_diff, diff_eq_diff_iff_inter_eq_inter,
  inter_comm, inter_comm M.E] at hM
Proof 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₂ I D : Set α
hI : M.Basis I (C ∩ M.E)
hM : C ∩ M.E = (I ∪ D) ∩ M.E
⊢ e ∈ M.cl (C ∩ M.E) \ (I ∪ D) ↔ e ∈ M.cl (C ∩ M.E) \ C
Theorem: Matroid.contract_loop_iff_mem_cl
Proof 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₂ I D : Set α
hI : M.Basis I (C ∩ M.E)
hM : C ∩ M.E = (I ∪ D) ∩ M.E
⊢ e ∈ M.cl (C ∩ M.E) \ (I ∪ D) ↔ e ∈ M.cl (C ∩ M.E) \ C
Tactic:
exact
  ⟨fun h ↦ ⟨h.1, fun heC ↦ h.2 (hM.subset ⟨heC, M.cl_subset_ground _ h.1⟩).1⟩, fun h ↦
    ⟨h.1, fun h' ↦ h.2 (hM.symm.subset ⟨h', M.cl_subset_ground _ h.1⟩).1⟩⟩
Proof state after:
no goals
Theorem: Matroid.contract_loops_eq
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).cl ∅ = M.cl C \ C
Tactic:
simp [Set.ext_iff, ← loop_iff_mem_cl_empty, contract_loop_iff_mem_cl]
Proof state after:
no goals
Theorem: Matroid.contract_cl_eq
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).cl X = M.cl (X ∪ C) \ C
Tactic:
ext e
Proof state after:
case h
α : 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 α
e : α
⊢ e ∈ (M ／ C).cl X ↔ e ∈ M.cl (X ∪ C) \ C
Theorem: Matroid.contract_cl_eq
Proof state before:
case h
α : 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 α
e : α
⊢ e ∈ (M ／ C).cl X ↔ e ∈ M.cl (X ∪ C) \ C
Tactic:
by_cases heX : e ∈ X
Proof state after:
case pos
α : 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 α
e : α
heX : e ∈ X
⊢ e ∈ (M ／ C).cl X ↔ e ∈ M.cl (X ∪ C) \ C

case neg
α : 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 α
e : α
heX : e ∉ X
⊢ e ∈ (M ／ C).cl X ↔ e ∈ M.cl (X ∪ C) \ C
Theorem: Matroid.contract_cl_eq
Proof state before:
case neg
α : 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 α
e : α
heX : e ∉ X
⊢ e ∈ (M ／ C).cl X ↔ e ∈ M.cl (X ∪ C) \ C
Tactic:
suffices h' : e ∈ (M ／ C).cl X \ X ↔ e ∈ M.cl (X ∪ C) \ (X ∪ C) by
  rwa [mem_diff, and_iff_left heX, mem_diff, mem_union, or_iff_right heX, ← mem_diff] at h'
Proof state after:
case neg
α : 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 α
e : α
heX : e ∉ X
⊢ e ∈ (M ／ C).cl X \ X ↔ e ∈ M.cl (X ∪ C) \ (X ∪ C)
Theorem: Matroid.contract_cl_eq
Proof state before:
case neg
α : 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 α
e : α
heX : e ∉ X
⊢ e ∈ (M ／ C).cl X \ X ↔ e ∈ M.cl (X ∪ C) \ (X ∪ C)
Tactic:
rw [← contract_loop_iff_mem_cl, ← contract_loop_iff_mem_cl, contract_contract, union_comm]
Proof state after:
no goals
Theorem: Matroid.contract_cl_eq
Proof state before:
case pos
α : 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 α
e : α
heX : e ∈ X
⊢ e ∈ (M ／ C).cl X ↔ e ∈ M.cl (X ∪ C) \ C
Tactic:
by_cases he : e ∈ (M ／ C).E
Proof state after:
case pos
α : 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 α
e : α
heX : e ∈ X
he : e ∈ (M ／ C).E
⊢ e ∈ (M ／ C).cl X ↔ e ∈ M.cl (X ∪ C) \ C

case neg
α : 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 α
e : α
heX : e ∈ X
he : e ∉ (M ／ C).E
⊢ e ∈ (M ／ C).cl X ↔ e ∈ M.cl (X ∪ C) \ C
Theorem: Matroid.contract_cl_eq
Proof state before:
case neg
α : 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 α
e : α
heX : e ∈ X
he : e ∉ (M ／ C).E
⊢ e ∈ (M ／ C).cl X ↔ e ∈ M.cl (X ∪ C) \ C
Tactic:
refine' iff_of_false (he ∘ fun h ↦ cl_subset_ground _ _ h) (he ∘ fun h ↦ _)
Proof state after:
case neg
α : 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 α
e : α
heX : e ∈ X
he : e ∉ (M ／ C).E
h : e ∈ M.cl (X ∪ C) \ C
⊢ e ∈ (M ／ C).E
Theorem: Matroid.contract_cl_eq
Proof state before:
case neg
α : 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 α
e : α
heX : e ∈ X
he : e ∉ (M ／ C).E
h : e ∈ M.cl (X ∪ C) \ C
⊢ e ∈ (M ／ C).E
Tactic:
rw [contract_ground]
Proof state after:
case neg
α : 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 α
e : α
heX : e ∈ X
he : e ∉ (M ／ C).E
h : e ∈ M.cl (X ∪ C) \ C
⊢ e ∈ M.E \ C
Theorem: Matroid.contract_cl_eq
Proof state before:
case neg
α : 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 α
e : α
heX : e ∈ X
he : e ∉ (M ／ C).E
h : e ∈ M.cl (X ∪ C) \ C
⊢ e ∈ M.E \ C
Tactic:
exact ⟨M.cl_subset_ground _ h.1, h.2⟩
Proof state after:
no goals
Theorem: Matroid.contract_cl_eq
Proof state before:
case pos
α : 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 α
e : α
heX : e ∈ X
he : e ∈ (M ／ C).E
⊢ e ∈ (M ／ C).cl X ↔ e ∈ M.cl (X ∪ C) \ C
Tactic:
refine' iff_of_true (mem_cl_of_mem' _ heX) _
Proof state after:
case pos
α : 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 α
e : α
heX : e ∈ X
he : e ∈ (M ／ C).E
⊢ e ∈ M.cl (X ∪ C) \ C
Theorem: Matroid.contract_cl_eq
Proof state before:
case pos
α : 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 α
e : α
heX : e ∈ X
he : e ∈ (M ／ C).E
⊢ e ∈ M.cl (X ∪ C) \ C
Tactic:
rw [contract_ground] at he
Proof state after:
case pos
α : 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 α
e : α
heX : e ∈ X
he : e ∈ M.E \ C
⊢ e ∈ M.cl (X ∪ C) \ C
Theorem: Matroid.contract_cl_eq
Proof state before:
case pos
α : 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 α
e : α
heX : e ∈ X
he : e ∈ M.E \ C
⊢ e ∈ M.cl (X ∪ C) \ C
Tactic:
exact ⟨mem_cl_of_mem' _ (Or.inl heX) he.1, he.2⟩
Proof state after:
no goals
Theorem: Matroid.contract_cl_eq
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 α
e : α
heX : e ∉ X
h' : e ∈ (M ／ C).cl X \ X ↔ e ∈ M.cl (X ∪ C) \ (X ∪ C)
⊢ e ∈ (M ／ C).cl X ↔ e ∈ M.cl (X ∪ C) \ C
Tactic:
rwa [mem_diff, and_iff_left heX, mem_diff, mem_union, or_iff_right heX, ← mem_diff] at h'
Proof state after:
no goals
Theorem: Matroid.Circuit.contract_dep
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
hCK : Disjoint C K
⊢ (M ／ C).Dep K
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis (C ∩ M.E)
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₂ : Set α
hK : M.Circuit K
hCK : Disjoint C K
I : Set α
hI : M.Basis I (C ∩ M.E)
⊢ (M ／ C).Dep K
Theorem: Matroid.Circuit.contract_dep
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₂ : Set α
hK : M.Circuit K
hCK : Disjoint C K
I : Set α
hI : M.Basis I (C ∩ M.E)
⊢ (M ／ C).Dep K
Tactic:
rw [← contract_inter_ground_eq, Dep, hI.contract_indep_iff,
  and_iff_left (hCK.mono_left inter_subset_left), contract_ground, subset_diff,
  and_iff_left (hCK.symm.mono_right inter_subset_left), and_iff_left hK.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₂ : Set α
hK : M.Circuit K
hCK : Disjoint C K
I : Set α
hI : M.Basis I (C ∩ M.E)
⊢ ¬M.Indep (K ∪ I)
Theorem: Matroid.Circuit.contract_dep
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₂ : Set α
hK : M.Circuit K
hCK : Disjoint C K
I : Set α
hI : M.Basis I (C ∩ M.E)
⊢ ¬M.Indep (K ∪ I)
Tactic:
exact fun hi ↦ hK.dep.not_indep (hi.subset subset_union_left)
Proof state after:
no goals
Theorem: Matroid.Circuit.contract_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 α
hK : M.Circuit K
hC : C ⊂ K
⊢ (M ／ C).Circuit (K \ C)
Tactic:
have hCi := hK.ssubset_indep hC
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.Circuit K
hC : C ⊂ K
hCi : M.Indep C
⊢ (M ／ C).Circuit (K \ C)
Theorem: Matroid.Circuit.contract_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 α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
⊢ (M ／ C).Circuit (K \ C)
Tactic:
rw [circuit_iff_forall_ssubset, hCi.contract_dep_iff, and_iff_right (disjoint_sdiff_left),
  diff_union_self, union_eq_self_of_subset_right hC.subset, and_iff_right hK.dep]
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.Circuit K
hC : C ⊂ K
hCi : M.Indep C
⊢ ∀ ⦃I : Set α⦄, I ⊂ K \ C → (M ／ C).Indep I
Theorem: Matroid.Circuit.contract_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 α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
⊢ ∀ ⦃I : Set α⦄, I ⊂ K \ C → (M ／ C).Indep I
Tactic:
intro I 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 α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
I : Set α
hI : I ⊂ K \ C
⊢ (M ／ C).Indep I
Theorem: Matroid.Circuit.contract_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 α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
I : Set α
hI : I ⊂ K \ C
⊢ (M ／ C).Indep I
Tactic:
rw [ssubset_iff_subset_not_subset, subset_diff, diff_subset_iff, union_comm] at 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 α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
I : Set α
hI : (I ⊆ K ∧ Disjoint I C) ∧ ¬K ⊆ I ∪ C
⊢ (M ／ C).Indep I
Theorem: Matroid.Circuit.contract_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 α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
I : Set α
hI : (I ⊆ K ∧ Disjoint I C) ∧ ¬K ⊆ I ∪ C
⊢ (M ／ C).Indep I
Tactic:
rw [hCi.contract_indep_iff, and_iff_right hI.1.2]
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.Circuit K
hC : C ⊂ K
hCi : M.Indep C
I : Set α
hI : (I ⊆ K ∧ Disjoint I C) ∧ ¬K ⊆ I ∪ C
⊢ M.Indep (I ∪ C)
Theorem: Matroid.Circuit.contract_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 α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
I : Set α
hI : (I ⊆ K ∧ Disjoint I C) ∧ ¬K ⊆ I ∪ C
⊢ M.Indep (I ∪ C)
Tactic:
refine hK.ssubset_indep <| (union_subset hI.1.1 hC.subset).ssubset_of_ne ?_
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.Circuit K
hC : C ⊂ K
hCi : M.Indep C
I : Set α
hI : (I ⊆ K ∧ Disjoint I C) ∧ ¬K ⊆ I ∪ C
⊢ I ∪ C ≠ K
Theorem: Matroid.Circuit.contract_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 α
hK : M.Circuit K
hC : C ⊂ K
hCi : M.Indep C
I : Set α
hI : (I ⊆ K ∧ Disjoint I C) ∧ ¬K ⊆ I ∪ C
⊢ I ∪ C ≠ K
Tactic:
rintro rfl
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z C C₁ C₂ : Set α
hCi : M.Indep C
I : Set α
hK : M.Circuit (I ∪ C)
hC : C ⊂ I ∪ C
hI : (I ⊆ I ∪ C ∧ Disjoint I C) ∧ ¬I ∪ C ⊆ I ∪ C
⊢ False
Theorem: Matroid.Circuit.contract_circuit
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I✝ J R B X Y Z C C₁ C₂ : Set α
hCi : M.Indep C
I : Set α
hK : M.Circuit (I ∪ C)
hC : C ⊂ I ∪ C
hI : (I ⊆ I ∪ C ∧ Disjoint I C) ∧ ¬I ∪ C ⊆ I ∪ C
⊢ False
Tactic:
exact hI.2 Subset.rfl
Proof state after:
no goals
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
⊢ (M ／ C).Dep (K \ C)
Tactic:
have h' := hK.contract_circuit (C := C ∩ K) (inter_subset_right.ssubset_of_ne (by simpa))
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.Circuit K
C : Set α
hKC : ¬K ⊆ C
h' : (M ／ (C ∩ K)).Circuit (K \ (C ∩ K))
⊢ (M ／ C).Dep (K \ C)
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
h' : (M ／ (C ∩ K)).Circuit (K \ (C ∩ K))
⊢ (M ／ C).Dep (K \ C)
Tactic:
simp only [diff_inter_self_eq_diff] 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 α
hK : M.Circuit K
C : Set α
hKC : ¬K ⊆ C
h' : (M ／ (C ∩ K)).Circuit (K \ C)
⊢ (M ／ C).Dep (K \ C)
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
h' : (M ／ (C ∩ K)).Circuit (K \ C)
⊢ (M ／ C).Dep (K \ C)
Tactic:
have hwin := h'.contract_dep (C := C \ K) disjoint_sdiff_sdiff
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.Circuit K
C : Set α
hKC : ¬K ⊆ C
h' : (M ／ (C ∩ K)).Circuit (K \ C)
hwin : (M ／ (C ∩ K) ／ (C \ K)).Dep (K \ C)
⊢ (M ／ C).Dep (K \ C)
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
h' : (M ／ (C ∩ K)).Circuit (K \ C)
hwin : (M ／ (C ∩ K) ／ (C \ K)).Dep (K \ C)
⊢ (M ／ C).Dep (K \ C)
Tactic:
rwa [contract_contract, inter_union_diff] at hwin
Proof state after:
no goals