internlm/Lean-Github huggingface dataset:
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof 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
Proof state after:
no goals
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof 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
Proof 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)
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof 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
Proof 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)
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof 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
Proof 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)
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof 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
Proof 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)
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof 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
Proof state after:
no goals
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof 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]
Proof 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
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof 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
Proof state after:
no goals
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof 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]
Proof 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)
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof 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
Proof 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)
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof 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
Proof 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)
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof 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
Proof 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)
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof 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
Proof state after:
no goals
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof 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]
Proof 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
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof 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
Proof state after:
no goals
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof 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]
Proof 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)
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof 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
Proof state after:
no goals
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof 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]
Proof 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'
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof 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
Proof state after:
no goals
Theorem: Matroid.Minor.exists_contract_spanning_restrict
Proof 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, M.Indep C ∧ N ≤r M ／ C ∧ (M ／ C).cl N.E = (M ／ C).E
Tactic:
obtain ⟨C, D, hC, hD, hCD, rfl⟩ := h.exists_contract_indep_delete_coindep
Proof 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 : M.Indep C
hD : M.Coindep D
hCD : Disjoint C D
h : M ／ C ＼ D ≤m M
⊢ ∃ C_1, M.Indep C_1 ∧ M ／ C ＼ D ≤r M ／ C_1 ∧ (M ／ C_1).cl (M ／ C ＼ D).E = (M ／ C_1).E
Theorem: Matroid.Minor.exists_contract_spanning_restrict
Proof 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 : M.Indep C
hD : M.Coindep D
hCD : Disjoint C D
h : M ／ C ＼ D ≤m M
⊢ ∃ C_1, M.Indep C_1 ∧ M ／ C ＼ D ≤r M ／ C_1 ∧ (M ／ C_1).cl (M ／ C ＼ D).E = (M ／ C_1).E
Tactic:
refine' ⟨C, hC, delete_restriction _ _, _⟩
Proof 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 : M.Indep C
hD : M.Coindep D
hCD : Disjoint C D
h : M ／ C ＼ D ≤m M
⊢ (M ／ C).cl (M ／ C ＼ D).E = (M ／ C).E
Theorem: Matroid.Minor.exists_contract_spanning_restrict
Proof 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 : M.Indep C
hD : M.Coindep D
hCD : Disjoint C D
h : M ／ C ＼ D ≤m M
⊢ (M ／ C).cl (M ／ C ＼ D).E = (M ／ C).E
Tactic:
rw [← (hD.coindep_contract_of_disjoint hCD.symm).cl_compl, delete_ground]
Proof state after:
no goals
Theorem: Matroid.Minor.C_indep
Proof 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
⊢ M.Indep h.C
Tactic:
obtain ⟨-,h,-⟩ := h.exists_contract_indep_delete_coindep.choose_spec
Proof state after:
case intro.intro
α : 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
h : M.Indep ⋯.choose
⊢ M.Indep h✝.C
Theorem: Matroid.Minor.C_indep
Proof state before:
case intro.intro
α : 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
h : M.Indep ⋯.choose
⊢ M.Indep h✝.C
Tactic:
exact h
Proof state after:
no goals
Theorem: Matroid.Minor.D_coindep
Proof 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
⊢ M.Coindep h.D
Tactic:
obtain ⟨-,h,-⟩ := h.exists_contract_indep_delete_coindep.choose_spec.choose_spec
Proof state after:
case intro.intro
α : 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
h : M.Coindep ⋯.choose
⊢ M.Coindep h✝.D
Theorem: Matroid.Minor.D_coindep
Proof state before:
case intro.intro
α : 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
h : M.Coindep ⋯.choose
⊢ M.Coindep h✝.D
Tactic:
exact h
Proof state after:
no goals
Theorem: Matroid.Minor.disjoint
Proof 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
⊢ Disjoint h.C h.D
Tactic:
obtain ⟨-,-,h,-⟩ := h.exists_contract_indep_delete_coindep.choose_spec.choose_spec
Proof state after:
case intro.intro.intro
α : 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
h : Disjoint ⋯.choose ⋯.choose
⊢ Disjoint h✝.C h✝.D
Theorem: Matroid.Minor.disjoint
Proof state before:
case intro.intro.intro
α : 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
h : Disjoint ⋯.choose ⋯.choose
⊢ Disjoint h✝.C h✝.D
Tactic:
exact h
Proof state after:
no goals
Theorem: Matroid.Minor.eq_con_del
Proof 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
⊢ N = M ／ h.C ＼ h.D
Tactic:
obtain ⟨-,-,-,h⟩ := h.exists_contract_indep_delete_coindep.choose_spec.choose_spec
Proof state after:
case intro.intro.intro
α : 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
h : N = M ／ ⋯.choose ＼ ⋯.choose
⊢ N = M ／ h✝.C ＼ h✝.D
Theorem: Matroid.Minor.eq_con_del
Proof state before:
case intro.intro.intro
α : 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
h : N = M ／ ⋯.choose ＼ ⋯.choose
⊢ N = M ／ h✝.C ＼ h✝.D
Tactic:
exact h
Proof state after:
no goals
Theorem: Matroid.Minor.C_union_D_eq
Proof 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
⊢ h.C ∪ h.D = M.E \ N.E
Tactic:
simp only [h.eq_con_del, delete_ground, contract_ground, diff_diff]
Proof state after:
α : 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
⊢ h.C ∪ h.D = M.E \ (M.E \ (h.C ∪ h.D))
Theorem: Matroid.Minor.C_union_D_eq
Proof 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
⊢ h.C ∪ h.D = M.E \ (M.E \ (h.C ∪ h.D))
Tactic:
rw [Set.diff_diff_cancel_left]
Proof state after:
α : 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
⊢ h.C ∪ h.D ⊆ M.E
Theorem: Matroid.Minor.C_union_D_eq
Proof 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
⊢ h.C ∪ h.D ⊆ M.E
Tactic:
exact union_subset h.C_indep.subset_ground h.D_coindep.subset_ground
Proof state after:
no goals
Theorem: Matroid.Minor.eq_con_restr
Proof 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
⊢ N = M ／ h.C ↾ N.E
Tactic:
simp [h.eq_con_del, ← restrict_compl]
Proof state after:
no goals
Theorem: Matroid.StrictMinor.C_union_D_nonempty
Proof 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).Nonempty
Tactic:
rw [h.minor.C_union_D_eq]
Proof state after:
α : 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
⊢ (M.E \ N.E).Nonempty
Theorem: Matroid.StrictMinor.C_union_D_nonempty
Proof 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
⊢ (M.E \ N.E).Nonempty
Tactic:
exact nonempty_of_ssubset h.ssubset
Proof state after:
no goals
Theorem: Matroid.delete_ground_self
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
M : Matroid α
⊢ M ＼ M.E = emptyOn α
Tactic:
simp [← ground_eq_empty_iff]
Proof state after:
no goals
Theorem: Matroid.contract_ground_self
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
M : Matroid α
⊢ M ／ M.E = emptyOn α
Tactic:
simp [← ground_eq_empty_iff]
Proof state after:
no goals
Theorem: Matroid.emptyOn_restriction
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
M : Matroid α
⊢ emptyOn α = M ↾ ∅
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.minor_emptyOn_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
⊢ M = emptyOn α → M ≤m emptyOn α
Tactic:
rintro rfl
Proof state after:
α : Type u_1
M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
⊢ emptyOn α ≤m emptyOn α
Theorem: Matroid.minor_emptyOn_iff
Proof state before:
α : Type u_1
M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
⊢ emptyOn α ≤m emptyOn α
Tactic:
apply emptyOn_minor
Proof state after:
no goals
Theorem: Matroid.restriction_emptyOn_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
⊢ M ≤r emptyOn α ↔ M = emptyOn α
Tactic:
refine ⟨fun h ↦ minor_emptyOn_iff.1 h.minor, ?_⟩
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
⊢ M = emptyOn α → M ≤r emptyOn α
Theorem: Matroid.restriction_emptyOn_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
⊢ M = emptyOn α → M ≤r emptyOn α
Tactic:
rintro rfl
Proof state after:
α : Type u_1
M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
⊢ emptyOn α ≤r emptyOn α
Theorem: Matroid.restriction_emptyOn_iff
Proof state before:
α : Type u_1
M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
⊢ emptyOn α ≤r emptyOn α
Tactic:
exact Restriction.refl
Proof state after:
no goals
Theorem: Matroid.loopyOn_delete
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X✝ Y Z K E✝ E X : Set α
⊢ loopyOn E ＼ X = loopyOn (E \ X)
Tactic:
rw [← restrict_compl, loopyOn_restrict, loopyOn_ground]
Proof state after:
no goals
Theorem: Matroid.loopyOn_contract
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X✝ Y Z K E✝ E X : Set α
⊢ loopyOn E ／ X = loopyOn (E \ X)
Tactic:
simp_rw [eq_loopyOn_iff_cl, contract_cl_eq, empty_union, loopyOn_cl_eq, contract_ground,
  loopyOn_ground, true_and]
Proof state after:
no goals
Theorem: Matroid.minor_loopyOn_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
⊢ M ≤m loopyOn E ↔ M = loopyOn M.E ∧ M.E ⊆ E
Tactic:
refine ⟨fun h ↦ ⟨by obtain ⟨C, D, _, _, _, rfl⟩ := h; simp, h.subset⟩, fun ⟨h, hss⟩ ↦ ?_⟩
Proof state after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
x✝ : M = loopyOn M.E ∧ M.E ⊆ E
h : M = loopyOn M.E
hss : M.E ⊆ E
⊢ M ≤m loopyOn E
Theorem: Matroid.minor_loopyOn_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
x✝ : M = loopyOn M.E ∧ M.E ⊆ E
h : M = loopyOn M.E
hss : M.E ⊆ E
⊢ M ≤m loopyOn E
Tactic:
convert (loopyOn E).restrict_minor hss using 1
Proof state after:
case h.e'_2
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
x✝ : M = loopyOn M.E ∧ M.E ⊆ E
h : M = loopyOn M.E
hss : M.E ⊆ E
⊢ M = loopyOn E ↾ M.E
Theorem: Matroid.minor_loopyOn_iff
Proof state before:
case h.e'_2
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
x✝ : M = loopyOn M.E ∧ M.E ⊆ E
h : M = loopyOn M.E
hss : M.E ⊆ E
⊢ M = loopyOn E ↾ M.E
Tactic:
rw [h, loopyOn_ground, loopyOn_restrict]
Proof state after:
no goals
Theorem: Matroid.minor_loopyOn_iff
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E : Set α
h : M ≤m loopyOn E
⊢ M = loopyOn M.E
Tactic:
obtain ⟨C, D, _, _, _, rfl⟩ := h
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
M' N : Matroid α
e f : α
I J R B X Y Z K E C D : Set α
left✝² : C ⊆ (loopyOn E).E
left✝¹ : D ⊆ (loopyOn E).E
left✝ : Disjoint C D
⊢ loopyOn E ／ C ＼ D = loopyOn (loopyOn E ／ C ＼ D).E
Theorem: Matroid.minor_loopyOn_iff
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
M' N : Matroid α
e f : α
I J R B X Y Z K E C D : Set α
left✝² : C ⊆ (loopyOn E).E
left✝¹ : D ⊆ (loopyOn E).E
left✝ : Disjoint C D
⊢ loopyOn E ／ C ＼ D = loopyOn (loopyOn E ／ C ＼ D).E
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.contract_eq_loopyOn_of_spanning
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K E C : Set α
h : M.Spanning C
⊢ M ／ C = loopyOn (M.E \ C)
Tactic:
rw [eq_loopyOn_iff_cl, contract_ground, and_iff_left rfl, contract_cl_eq, empty_union, h.cl_eq]
Proof state after:
no goals
Theorem: Matroid.freeOn_delete
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X✝ Y Z K E✝ E X : Set α
⊢ freeOn E ＼ X = freeOn (E \ X)
Tactic:
rw [← loopyOn_dual_eq, ← contract_dual_eq_dual_delete, loopyOn_contract, loopyOn_dual_eq]
Proof state after:
no goals
Theorem: Matroid.freeOn_contract
Proof state before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X✝ Y Z K E✝ E X : Set α
⊢ freeOn E ／ X = freeOn (E \ X)
Tactic:
rw [← loopyOn_dual_eq, ← delete_dual_eq_dual_contract, loopyOn_delete, loopyOn_dual_eq]
Proof state after:
no goals