internlm/Lean-Github huggingface dataset:
Theorem: Matroid.delete_cl_eq
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X✝ Y Z K D✝ D₁ D₂ R : Set α
M : Matroid α
D X : Set α
⊢ M.cl (X \ D) \ D ⊆ M.E
Tactic:
exact diff_subset.trans (M.cl_subset_ground _)
Proof state after:
no goals
Theorem: Matroid.delete_loops_eq
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K D✝ D₁ D₂ R : Set α
M : Matroid α
D : Set α
⊢ (M ＼ D).cl ∅ = M.cl ∅ \ D
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.delete_empty
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
M : Matroid α
⊢ M ＼ ∅ = M
Tactic:
rw [delete_eq_self_iff]
Proof state after:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
M : Matroid α
⊢ Disjoint ∅ M.E
Theorem: Matroid.delete_empty
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
M : Matroid α
⊢ Disjoint ∅ M.E
Tactic:
exact empty_disjoint _
Proof state after:
no goals
Theorem: Matroid.delete_delete_diff
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁✝ D₂✝ R : Set α
M : Matroid α
D₁ D₂ : Set α
⊢ M ＼ D₁ ＼ D₂ = M ＼ D₁ ＼ (D₂ \ D₁)
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.removeLoops_eq_delete
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
M : Matroid α
⊢ M.removeLoops = M ＼ M.cl ∅
Tactic:
rw [← restrict_compl, removeLoops]
Proof state after:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
M : Matroid α
⊢ M ↾ {e | M.Nonloop e} = M ↾ M.E \ M.cl ∅
Theorem: Matroid.removeLoops_eq_delete
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
M : Matroid α
⊢ M ↾ {e | M.Nonloop e} = M ↾ M.E \ M.cl ∅
Tactic:
convert rfl using 2
Proof state after:
case h.e'_3.h.e'_3
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
M : Matroid α
⊢ M.E \ M.cl ∅ = {e | M.Nonloop e}
Theorem: Matroid.removeLoops_eq_delete
Proof state before:
case h.e'_3.h.e'_3
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
M : Matroid α
⊢ M.E \ M.cl ∅ = {e | M.Nonloop e}
Tactic:
simp [Set.ext_iff, mem_setOf, Nonloop, Loop, mem_diff, and_comm]
Proof state after:
no goals
Theorem: Matroid.removeLoops_del_eq_removeLoops
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
h : X ⊆ M.cl ∅
⊢ (M ＼ X).removeLoops = M.removeLoops
Tactic:
rw [removeLoops_eq_delete, delete_delete, removeLoops_eq_delete, delete_cl_eq, empty_diff,
  union_diff_self, union_eq_self_of_subset_left h]
Proof state after:
no goals
Theorem: Matroid.dual_contract_dual_eq_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 α
X : Set α
⊢ (M✶ ／ X)✶ = M ＼ X
Tactic:
rw [← dual_delete_dual_eq_contract, dual_dual, dual_dual]
Proof state after:
no goals
Theorem: Matroid.contract_dual_eq_dual_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 α
X : Set α
⊢ (M ／ X)✶ = M✶ ＼ X
Tactic:
rw [← dual_delete_dual_eq_contract, dual_dual]
Proof state after:
no goals
Theorem: Matroid.delete_dual_eq_dual_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 α
M : Matroid α
X : Set α
⊢ (M ＼ X)✶ = M✶ ／ X
Tactic:
rw [← dual_delete_dual_eq_contract, dual_dual]
Proof state after:
no goals
Theorem: Matroid.contract_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 α
M : Matroid α
C₁ C₂ : Set α
⊢ M ／ C₁ ／ C₂ = M ／ (C₁ ∪ C₂)
Tactic:
rw [eq_comm, ← dual_delete_dual_eq_contract, ← delete_delete, ← dual_contract_dual_eq_delete, ←
  dual_contract_dual_eq_delete, dual_dual, dual_dual, dual_dual]
Proof state after:
no goals
Theorem: Matroid.contract_comm
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₁ C₂ : Set α
⊢ M ／ C₁ ／ C₂ = M ／ C₂ ／ C₁
Tactic:
rw [contract_contract, union_comm, contract_contract]
Proof state after:
no goals
Theorem: Matroid.contract_eq_self_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 = M ↔ Disjoint C M.E
Tactic:
rw [← dual_delete_dual_eq_contract, ← dual_inj, dual_dual, delete_eq_self_iff, dual_ground]
Proof state after:
no goals
Theorem: Matroid.contract_empty
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 α
⊢ M ／ ∅ = M
Tactic:
rw [← dual_delete_dual_eq_contract, delete_empty, dual_dual]
Proof state after:
no goals
Theorem: Matroid.contract_contract_diff
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₁ C₂ : Set α
⊢ M ／ C₁ ／ C₂ = M ／ C₁ ／ (C₂ \ C₁)
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.contract_eq_contract_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₁ = M ／ C₂ ↔ C₁ ∩ M.E = C₂ ∩ M.E
Tactic:
rw [← dual_delete_dual_eq_contract, ← dual_delete_dual_eq_contract, dual_inj,
  delete_eq_delete_iff, dual_ground]
Proof state after:
no goals
Theorem: Matroid.contract_inter_ground_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 : Set α
⊢ M ／ (C ∩ M.E) = M ／ C
Tactic:
rw [← dual_delete_dual_eq_contract, (show M.E = M✶.E from rfl), delete_inter_ground_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 : Set α
⊢ (M✶ ＼ C)✶ = M ／ C
Theorem: Matroid.contract_inter_ground_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 : Set α
⊢ (M✶ ＼ C)✶ = M ／ C
Tactic:
rfl
Proof state after:
no goals
Theorem: Matroid.coindep_contract_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).Coindep X ↔ M.Coindep X ∧ Disjoint X C
Tactic:
rw [coindep_def, contract_dual_eq_dual_delete, delete_indep_iff, ← coindep_def]
Proof state after:
no goals
Theorem: Matroid.Indep.contract_base_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.Indep I
⊢ (M ／ I).Base B ↔ M.Base (B ∪ I) ∧ Disjoint B I
Tactic:
have hIE := hI.subset_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 α
hI : M.Indep I
hIE : I ⊆ M.E
⊢ (M ／ I).Base B ↔ M.Base (B ∪ I) ∧ Disjoint B I
Theorem: Matroid.Indep.contract_base_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.Indep I
hIE : I ⊆ M.E
⊢ (M ／ I).Base B ↔ M.Base (B ∪ I) ∧ Disjoint B I
Tactic:
rw [← dual_dual M, ← coindep_def, coindep_iff_exists] 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 α
hI : ∃ B, M✶.Base B ∧ B ⊆ M✶.E \ I
hIE : I ⊆ M.E
⊢ (M ／ I).Base B ↔ M.Base (B ∪ I) ∧ Disjoint B I
Theorem: Matroid.Indep.contract_base_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 : ∃ B, M✶.Base B ∧ B ⊆ M✶.E \ I
hIE : I ⊆ M.E
⊢ (M ／ I).Base B ↔ M.Base (B ∪ I) ∧ Disjoint B I
Tactic:
obtain ⟨B₀, hB₀, hfk⟩ := hI
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₂ : Set α
hIE : I ⊆ M.E
B₀ : Set α
hB₀ : M✶.Base B₀
hfk : B₀ ⊆ M✶.E \ I
⊢ (M ／ I).Base B ↔ M.Base (B ∪ I) ∧ Disjoint B I
Theorem: Matroid.Indep.contract_base_iff
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₂ : Set α
hIE : I ⊆ M.E
B₀ : Set α
hB₀ : M✶.Base B₀
hfk : B₀ ⊆ M✶.E \ I
⊢ (M ／ I).Base B ↔ M.Base (B ∪ I) ∧ Disjoint B I
Tactic:
rw [← dual_dual M, ← dual_delete_dual_eq_contract, dual_base_iff', dual_base_iff',
  delete_base_iff, dual_dual, delete_ground, diff_diff, union_comm, union_subset_iff,
  subset_diff, ← and_assoc, and_congr_left_iff, dual_ground, and_iff_left hIE, and_congr_left_iff]
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₂ : Set α
hIE : I ⊆ M.E
B₀ : Set α
hB₀ : M✶.Base B₀
hfk : B₀ ⊆ M✶.E \ I
⊢ Disjoint B I → B ⊆ M.E → (M✶.Basis (M.E \ (B ∪ I)) (M.E \ I) ↔ M✶.Base (M.E \ (B ∪ I)))
Theorem: Matroid.Indep.contract_base_iff
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₂ : Set α
hIE : I ⊆ M.E
B₀ : Set α
hB₀ : M✶.Base B₀
hfk : B₀ ⊆ M✶.E \ I
⊢ Disjoint B I → B ⊆ M.E → (M✶.Basis (M.E \ (B ∪ I)) (M.E \ I) ↔ M✶.Base (M.E \ (B ∪ I)))
Tactic:
refine' fun _ _ ↦
  ⟨fun h ↦ h.base_of_base_subset hB₀ (subset_diff.mpr ⟨hB₀.subset_ground, _⟩), fun hB ↦
    hB.basis_of_subset diff_subset (diff_subset_diff_right subset_union_right)⟩
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₂ : Set α
hIE : I ⊆ M.E
B₀ : Set α
hB₀ : M✶.Base B₀
hfk : B₀ ⊆ M✶.E \ I
x✝¹ : Disjoint B I
x✝ : B ⊆ M.E
h : M✶.Basis (M.E \ (B ∪ I)) (M.E \ I)
⊢ Disjoint B₀ I
Theorem: Matroid.Indep.contract_base_iff
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₂ : Set α
hIE : I ⊆ M.E
B₀ : Set α
hB₀ : M✶.Base B₀
hfk : B₀ ⊆ M✶.E \ I
x✝¹ : Disjoint B I
x✝ : B ⊆ M.E
h : M✶.Basis (M.E \ (B ∪ I)) (M.E \ I)
⊢ Disjoint B₀ I
Tactic:
exact disjoint_of_subset_left hfk disjoint_sdiff_left
Proof state after:
no goals
Theorem: Matroid.Indep.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.Indep I
⊢ (M ／ I).Indep J ↔ Disjoint J I ∧ M.Indep (J ∪ I)
Tactic:
simp_rw [indep_iff, hI.contract_base_iff, union_subset_iff]
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.Indep I
⊢ (∃ B, (M.Base (B ∪ I) ∧ Disjoint B I) ∧ J ⊆ B) ↔ Disjoint J I ∧ ∃ B, M.Base B ∧ J ⊆ B ∧ I ⊆ B
Theorem: Matroid.Indep.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.Indep I
⊢ (∃ B, (M.Base (B ∪ I) ∧ Disjoint B I) ∧ J ⊆ B) ↔ Disjoint J I ∧ ∃ B, M.Base B ∧ J ⊆ B ∧ I ⊆ B
Tactic:
exact ⟨fun ⟨B, ⟨hBI, hdj⟩, hJB⟩ ↦
  ⟨disjoint_of_subset_left hJB hdj, _, hBI, hJB.trans subset_union_left,
    subset_union_right⟩,
  fun ⟨hdj, B, hB, hJB, hIB⟩ ↦ ⟨B \ I,⟨by simpa [union_eq_self_of_subset_right hIB],
    disjoint_sdiff_left⟩, subset_diff.2 ⟨hJB, hdj⟩ ⟩⟩
Proof state after:
no goals
Theorem: Matroid.Indep.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.Indep I
x✝ : Disjoint J I ∧ ∃ B, M.Base B ∧ J ⊆ B ∧ I ⊆ B
hdj : Disjoint J I
B : Set α
hB : M.Base B
hJB : J ⊆ B
hIB : I ⊆ B
⊢ M.Base (B \ I ∪ I)
Tactic:
simpa [union_eq_self_of_subset_right hIB]
Proof state after:
no goals
Theorem: Matroid.Nonloop.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 α
he : M.Nonloop e
⊢ (M ／ e).Indep I ↔ e ∉ I ∧ M.Indep (insert e I)
Tactic:
simp [contract_elem, he.indep.contract_indep_iff]
Proof state after:
no goals
Theorem: Matroid.Indep.union_indep_iff_contract_indep
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.Indep I
⊢ M.Indep (I ∪ J) ↔ (M ／ I).Indep (J \ I)
Tactic:
rw [hI.contract_indep_iff, and_iff_right disjoint_sdiff_left, diff_union_self, union_comm]
Proof state after:
no goals
Theorem: Matroid.Indep.diff_indep_contract_of_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 α
hJ : M.Indep J
hIJ : I ⊆ J
⊢ (M ／ I).Indep (J \ I)
Tactic:
rwa [← (hJ.subset hIJ).union_indep_iff_contract_indep, union_eq_self_of_subset_left hIJ]
Proof state after:
no goals
Theorem: Matroid.Indep.contract_dep_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.Indep I
⊢ (M ／ I).Dep J ↔ Disjoint J I ∧ M.Dep (J ∪ I)
Tactic:
rw [dep_iff, hI.contract_indep_iff, dep_iff, contract_ground, subset_diff, disjoint_comm,
  union_subset_iff, and_iff_left hI.subset_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 α
hI : M.Indep I
⊢ ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
Theorem: Matroid.Indep.contract_dep_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.Indep I
⊢ ¬(Disjoint I J ∧ M.Indep (J ∪ I)) ∧ J ⊆ M.E ∧ Disjoint I J ↔ Disjoint I J ∧ ¬M.Indep (J ∪ I) ∧ J ⊆ M.E
Tactic:
tauto
Proof state after:
no goals
Theorem: Matroid.Indep.union_contract_basis_union_of_basis
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.Indep I
hB : (M ／ I).Basis J X
⊢ M.Basis (J ∪ I) (X ∪ I)
Tactic:
have hi := hB.indep
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.Indep I
hB : (M ／ I).Basis J X
hi : (M ／ I).Indep J
⊢ M.Basis (J ∪ I) (X ∪ I)
Theorem: Matroid.Indep.union_contract_basis_union_of_basis
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.Indep I
hB : (M ／ I).Basis J X
hi : (M ／ I).Indep J
⊢ M.Basis (J ∪ I) (X ∪ I)
Tactic:
rw [hI.contract_indep_iff] 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 α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
⊢ M.Basis (J ∪ I) (X ∪ I)
Theorem: Matroid.Indep.union_contract_basis_union_of_basis
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.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
⊢ M.Basis (J ∪ I) (X ∪ I)
Tactic:
refine' hi.2.basis_of_maximal_subset (union_subset_union_left _ hB.subset) _ _
Proof state after:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
⊢ ∀ ⦃J_1 : Set α⦄, M.Indep J_1 → J ∪ I ⊆ J_1 → J_1 ⊆ X ∪ I → J_1 ⊆ J ∪ I

case refine'_2
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
⊢ X ∪ I ⊆ M.E
Theorem: Matroid.Indep.union_contract_basis_union_of_basis
Proof state before:
case refine'_2
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
⊢ X ∪ I ⊆ M.E
Tactic:
exact union_subset (hB.subset_ground.trans (contract_ground_subset_ground _ _)) hI.subset_ground
Proof state after:
no goals
Theorem: Matroid.Indep.union_contract_basis_union_of_basis
Proof state before:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
⊢ ∀ ⦃J_1 : Set α⦄, M.Indep J_1 → J ∪ I ⊆ J_1 → J_1 ⊆ X ∪ I → J_1 ⊆ J ∪ I
Tactic:
intro K hK hJIK hKXI
Proof state after:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K✝ C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
K : Set α
hK : M.Indep K
hJIK : J ∪ I ⊆ K
hKXI : K ⊆ X ∪ I
⊢ K ⊆ J ∪ I
Theorem: Matroid.Indep.union_contract_basis_union_of_basis
Proof state before:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K✝ C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
K : Set α
hK : M.Indep K
hJIK : J ∪ I ⊆ K
hKXI : K ⊆ X ∪ I
⊢ K ⊆ J ∪ I
Tactic:
rw [union_subset_iff] at hJIK
Proof state after:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K✝ C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
K : Set α
hK : M.Indep K
hJIK : J ⊆ K ∧ I ⊆ K
hKXI : K ⊆ X ∪ I
⊢ K ⊆ J ∪ I
Theorem: Matroid.Indep.union_contract_basis_union_of_basis
Proof state before:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K✝ C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
K : Set α
hK : M.Indep K
hJIK : J ⊆ K ∧ I ⊆ K
hKXI : K ⊆ X ∪ I
⊢ K ⊆ J ∪ I
Tactic:
have hK' : (M ／ I).Indep (K \ I) := hK.diff_indep_contract_of_subset hJIK.2
Proof state after:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K✝ C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
K : Set α
hK : M.Indep K
hJIK : J ⊆ K ∧ I ⊆ K
hKXI : K ⊆ X ∪ I
hK' : (M ／ I).Indep (K \ I)
⊢ K ⊆ J ∪ I
Theorem: Matroid.Indep.union_contract_basis_union_of_basis
Proof state before:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K✝ C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
K : Set α
hK : M.Indep K
hJIK : J ⊆ K ∧ I ⊆ K
hKXI : K ⊆ X ∪ I
hK' : (M ／ I).Indep (K \ I)
⊢ K ⊆ J ∪ I
Tactic:
have hm := hB.eq_of_subset_indep hK'
Proof state after:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K✝ C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
K : Set α
hK : M.Indep K
hJIK : J ⊆ K ∧ I ⊆ K
hKXI : K ⊆ X ∪ I
hK' : (M ／ I).Indep (K \ I)
hm : J ⊆ K \ I → K \ I ⊆ X → J = K \ I
⊢ K ⊆ J ∪ I
Theorem: Matroid.Indep.union_contract_basis_union_of_basis
Proof state before:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K✝ C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
K : Set α
hK : M.Indep K
hJIK : J ⊆ K ∧ I ⊆ K
hKXI : K ⊆ X ∪ I
hK' : (M ／ I).Indep (K \ I)
hm : J ⊆ K \ I → K \ I ⊆ X → J = K \ I
⊢ K ⊆ J ∪ I
Tactic:
rw [subset_diff, and_iff_left hi.1, diff_subset_iff, union_comm, imp_iff_right hKXI,
  imp_iff_right hJIK.1] at hm
Proof state after:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K✝ C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
K : Set α
hK : M.Indep K
hJIK : J ⊆ K ∧ I ⊆ K
hKXI : K ⊆ X ∪ I
hK' : (M ／ I).Indep (K \ I)
hm : J = K \ I
⊢ K ⊆ J ∪ I
Theorem: Matroid.Indep.union_contract_basis_union_of_basis
Proof state before:
case refine'_1
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K✝ C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
K : Set α
hK : M.Indep K
hJIK : J ⊆ K ∧ I ⊆ K
hKXI : K ⊆ X ∪ I
hK' : (M ／ I).Indep (K \ I)
hm : J = K \ I
⊢ K ⊆ J ∪ I
Tactic:
simp [hm]
Proof state after:
no goals
Theorem: Matroid.Basis.contract_basis_union_union
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.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint (J ∪ X) I
⊢ (M ／ I).Basis J X
Tactic:
rw [disjoint_union_left] at hdj
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.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
⊢ (M ／ I).Basis J X
Theorem: Matroid.Basis.contract_basis_union_union
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.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
⊢ (M ／ I).Basis J X
Tactic:
have hI := h.indep.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₂ : Set α
h : M.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
⊢ (M ／ I).Basis J X
Theorem: Matroid.Basis.contract_basis_union_union
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.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
⊢ (M ／ I).Basis J X
Tactic:
simp_rw [Basis, mem_maximals_setOf_iff, hI.contract_indep_iff, and_iff_right hdj.1,
  and_iff_right h.indep, contract_ground, subset_diff, and_iff_left hdj.2,
  and_iff_left (subset_union_left.trans h.subset_ground), and_imp,
  and_iff_right
    (Disjoint.subset_left_of_subset_union (subset_union_left.trans h.subset) hdj.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 : M.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
⊢ ∀ ⦃y : Set α⦄, Disjoint y I → M.Indep (y ∪ I) → y ⊆ X → J ⊆ y → J = y
Theorem: Matroid.Basis.contract_basis_union_union
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.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
⊢ ∀ ⦃y : Set α⦄, Disjoint y I → M.Indep (y ∪ I) → y ⊆ X → J ⊆ y → J = y
Tactic:
intro Y hYI hYi hYX hJY
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.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
Y : Set α
hYI : Disjoint Y I
hYi : M.Indep (Y ∪ I)
hYX : Y ⊆ X
hJY : J ⊆ Y
⊢ J = Y
Theorem: Matroid.Basis.contract_basis_union_union
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.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
Y : Set α
hYI : Disjoint Y I
hYi : M.Indep (Y ∪ I)
hYX : Y ⊆ X
hJY : J ⊆ Y
⊢ J = Y
Tactic:
have hu :=
  h.eq_of_subset_indep hYi (union_subset_union_left _ hJY) (union_subset_union_left _ hYX)
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.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
Y : Set α
hYI : Disjoint Y I
hYi : M.Indep (Y ∪ I)
hYX : Y ⊆ X
hJY : J ⊆ Y
hu : J ∪ I = Y ∪ I
⊢ J = Y
Theorem: Matroid.Basis.contract_basis_union_union
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.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
Y : Set α
hYI : Disjoint Y I
hYi : M.Indep (Y ∪ I)
hYX : Y ⊆ X
hJY : J ⊆ Y
hu : J ∪ I = Y ∪ I
⊢ J = Y
Tactic:
apply_fun fun x : Set α ↦ x \ I at hu
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.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
Y : Set α
hYI : Disjoint Y I
hYi : M.Indep (Y ∪ I)
hYX : Y ⊆ X
hJY : J ⊆ Y
hu : (J ∪ I) \ I = (Y ∪ I) \ I
⊢ J = Y
Theorem: Matroid.Basis.contract_basis_union_union
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.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
Y : Set α
hYI : Disjoint Y I
hYi : M.Indep (Y ∪ I)
hYX : Y ⊆ X
hJY : J ⊆ Y
hu : (J ∪ I) \ I = (Y ∪ I) \ I
⊢ J = Y
Tactic:
simp_rw [union_diff_right, hdj.1.sdiff_eq_left, hYI.sdiff_eq_left] at hu
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.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
Y : Set α
hYI : Disjoint Y I
hYi : M.Indep (Y ∪ I)
hYX : Y ⊆ X
hJY : J ⊆ Y
hu : J = Y
⊢ J = Y
Theorem: Matroid.Basis.contract_basis_union_union
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.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
Y : Set α
hYI : Disjoint Y I
hYi : M.Indep (Y ∪ I)
hYX : Y ⊆ X
hJY : J ⊆ Y
hu : J = Y
⊢ J = Y
Tactic:
exact hu
Proof state after:
no goals
Theorem: Matroid.contract_eq_delete_of_subset_coloops
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 ∅
⊢ M ／ X = M ＼ X
Tactic:
refine' eq_of_indep_iff_indep_forall rfl fun 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 α
hX : X ⊆ M✶.cl ∅
I : Set α
x✝ : I ⊆ (M ／ X).E
⊢ (M ／ X).Indep I ↔ (M ＼ X).Indep I
Theorem: Matroid.contract_eq_delete_of_subset_coloops
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 ∅
I : Set α
x✝ : I ⊆ (M ／ X).E
⊢ (M ／ X).Indep I ↔ (M ＼ X).Indep I
Tactic:
rw [(indep_of_subset_coloops hX).contract_indep_iff, delete_indep_iff, and_comm,
  union_indep_iff_indep_of_subset_coloops hX]
Proof state after:
no goals
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 ∅
⊢ M ／ X = M ＼ X
Tactic:
rw [← dual_inj, contract_dual_eq_dual_delete, delete_dual_eq_dual_contract, eq_comm,
  contract_eq_delete_of_subset_coloops]
Proof state after:
α : 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 ∅