internlm/Lean-Github huggingface dataset:
Theorem: Matroid.strictMinor_iff_exists_eq_contract_delete
Proof state before:
case right
α : 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
e : α
he : e ∈ C ∪ D
⊢ ¬M.E ⊆ M.E \ (C ∪ D)
Tactic:
exact fun hss ↦ (hss ((union_subset hC hD) he)).2 he
Proof state after:
no goals
Theorem: Matroid.strictMinor_iff_exists_eq_contract_delete
Proof state before:
case mp.intro.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 : C ⊆ M.E
hD : D ⊆ M.E
hCD : Disjoint C D
hss : (M ／ C ＼ D).E ⊂ M.E
⊢ ∃ C_1 D_1, C_1 ⊆ M.E ∧ D_1 ⊆ M.E ∧ Disjoint C_1 D_1 ∧ (C_1 ∪ D_1).Nonempty ∧ M ／ C ＼ D = M ／ C_1 ＼ D_1
Tactic:
refine ⟨C, D, hC, hD, hCD, ?_, rfl⟩
Proof state after:
case mp.intro.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 : C ⊆ M.E
hD : D ⊆ M.E
hCD : Disjoint C D
hss : (M ／ C ＼ D).E ⊂ M.E
⊢ (C ∪ D).Nonempty
Theorem: Matroid.strictMinor_iff_exists_eq_contract_delete
Proof state before:
case mp.intro.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 : C ⊆ M.E
hD : D ⊆ M.E
hCD : Disjoint C D
hss : (M ／ C ＼ D).E ⊂ M.E
⊢ (C ∪ D).Nonempty
Tactic:
rw [nonempty_iff_ne_empty]
Proof state after:
case mp.intro.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 : C ⊆ M.E
hD : D ⊆ M.E
hCD : Disjoint C D
hss : (M ／ C ＼ D).E ⊂ M.E
⊢ C ∪ D ≠ ∅
Theorem: Matroid.strictMinor_iff_exists_eq_contract_delete
Proof state before:
case mp.intro.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 : C ⊆ M.E
hD : D ⊆ M.E
hCD : Disjoint C D
hss : (M ／ C ＼ D).E ⊂ M.E
⊢ C ∪ D ≠ ∅
Tactic:
rintro hCD
Proof state after:
case mp.intro.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 : C ⊆ M.E
hD : D ⊆ M.E
hCD✝ : Disjoint C D
hss : (M ／ C ＼ D).E ⊂ M.E
hCD : C ∪ D = ∅
⊢ False
Theorem: Matroid.strictMinor_iff_exists_eq_contract_delete
Proof state before:
case mp.intro.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 : C ⊆ M.E
hD : D ⊆ M.E
hCD✝ : Disjoint C D
hss : (M ／ C ＼ D).E ⊂ M.E
hCD : C ∪ D = ∅
⊢ False
Tactic:
rw [delete_ground, contract_ground, diff_diff, hCD, diff_empty] at hss
Proof state after:
case mp.intro.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 : C ⊆ M.E
hD : D ⊆ M.E
hCD✝ : Disjoint C D
hss : M.E ⊂ M.E
hCD : C ∪ D = ∅
⊢ False
Theorem: Matroid.strictMinor_iff_exists_eq_contract_delete
Proof state before:
case mp.intro.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 : C ⊆ M.E
hD : D ⊆ M.E
hCD✝ : Disjoint C D
hss : M.E ⊂ M.E
hCD : C ∪ D = ∅
⊢ False
Tactic:
exact hss.ne rfl
Proof state after:
no goals
Theorem: Matroid.contract_minor
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 : Set α
⊢ M ／ C ≤m M
Tactic:
rw [← (M ／ C).delete_empty]
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 : Set α
⊢ M ／ C ＼ ∅ ≤m M
Theorem: Matroid.contract_minor
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 : Set α
⊢ M ／ C ＼ ∅ ≤m M
Tactic:
apply contract_delete_minor
Proof state after:
no goals
Theorem: Matroid.contract_minor_of_subset
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 C' : Set α
hCC' : C ⊆ C'
⊢ M ／ C' ≤m M ／ C
Tactic:
rw [← diff_union_of_subset hCC', union_comm, ← contract_contract]
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 C' : Set α
hCC' : C ⊆ C'
⊢ M ／ C ／ (C' \ C) ≤m M ／ C
Theorem: Matroid.contract_minor_of_subset
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 C' : Set α
hCC' : C ⊆ C'
⊢ M ／ C ／ (C' \ C) ≤m M ／ C
Tactic:
apply contract_minor
Proof state after:
no goals
Theorem: Matroid.delete_minor
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 α
D : Set α
⊢ M ＼ D ≤m M
Tactic:
nth_rw 1 [← M.contract_empty]
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 α
D : Set α
⊢ M ／ ∅ ＼ D ≤m M
Theorem: Matroid.delete_minor
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 α
D : Set α
⊢ M ／ ∅ ＼ D ≤m M
Tactic:
apply contract_delete_minor
Proof state after:
no goals
Theorem: Matroid.restrict_minor
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 α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ M ↾ R ≤m M
Tactic:
rw [← delete_compl]
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 α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ M ＼ (M.E \ R) ≤m M
Theorem: Matroid.restrict_minor
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 α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ M ＼ (M.E \ R) ≤m M
Tactic:
apply delete_minor
Proof state after:
no goals
Theorem: Matroid.Restriction.minor
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 ≤r M
⊢ N ≤m M
Tactic:
rw [← h.eq_restrict, ← delete_compl h.subset]
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 ≤r M
⊢ M ＼ (M.E \ N.E) ≤m M
Theorem: Matroid.Restriction.minor
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 ≤r M
⊢ M ＼ (M.E \ N.E) ≤m M
Tactic:
apply delete_minor
Proof state after:
no goals
Theorem: Matroid.contract_restrict_minor
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 : Set α
hR : R ⊆ M.E \ C
⊢ M ／ C ↾ R ≤m M
Tactic:
rw [← delete_compl]
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 : Set α
hR : R ⊆ M.E \ C
⊢ M ／ C ＼ ((M ／ C).E \ R) ≤m M
Theorem: Matroid.contract_restrict_minor
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 : Set α
hR : R ⊆ M.E \ C
⊢ M ／ C ＼ ((M ／ C).E \ R) ≤m M
Tactic:
apply contract_delete_minor
Proof state after:
no goals
Theorem: Matroid.strictMinor_iff_minor_contract_or_delete
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 α
⊢ N <m M ↔ ∃ e ∈ M.E, N ≤m M ／ e ∨ N ≤m M ＼ e
Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
Proof state after:
case refine_1
α : 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
⊢ ∃ e ∈ M.E, N ≤m M ／ e ∨ N ≤m M ＼ e

case refine_2
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
⊢ (∃ e ∈ M.E, N ≤m M ／ e ∨ N ≤m M ＼ e) → N <m M
Theorem: Matroid.strictMinor_iff_minor_contract_or_delete
Proof state before:
case refine_2
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
⊢ (∃ e ∈ M.E, N ≤m M ／ e ∨ N ≤m M ＼ e) → N <m M
Tactic:
rintro ⟨e, he, (hc | hd)⟩
Proof state after:
case refine_2.intro.intro.inl
α : Type u_1
M M' N : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
e : α
he : e ∈ M.E
hc : N ≤m M ／ e
⊢ N <m M

case refine_2.intro.intro.inr
α : Type u_1
M M' N : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
e : α
he : e ∈ M.E
hd : N ≤m M ＼ e
⊢ N <m M
Theorem: Matroid.strictMinor_iff_minor_contract_or_delete
Proof state before:
case refine_2.intro.intro.inr
α : Type u_1
M M' N : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
e : α
he : e ∈ M.E
hd : N ≤m M ＼ e
⊢ N <m M
Tactic:
exact hd.trans_strictMinor (deleteElem_strictMinor he)
Proof state after:
no goals
Theorem: Matroid.strictMinor_iff_minor_contract_or_delete
Proof state before:
case refine_1
α : 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
⊢ ∃ e ∈ M.E, N ≤m M ／ e ∨ N ≤m M ＼ e
Tactic:
obtain ⟨C, D, hC, hD, hCD, ⟨e,(heC | heD)⟩, rfl⟩ :=
  strictMinor_iff_exists_eq_contract_delete.1 h
Proof state after:
case refine_1.intro.intro.intro.intro.intro.intro.intro.inl
α : 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
e : α
heC : e ∈ C
h : M ／ C ＼ D <m M
⊢ ∃ e ∈ M.E, M ／ C ＼ D ≤m M ／ e ∨ M ／ C ＼ D ≤m M ＼ e

case refine_1.intro.intro.intro.intro.intro.intro.intro.inr
α : 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
e : α
heD : e ∈ D
h : M ／ C ＼ D <m M
⊢ ∃ e ∈ M.E, M ／ C ＼ D ≤m M ／ e ∨ M ／ C ＼ D ≤m M ＼ e
Theorem: Matroid.strictMinor_iff_minor_contract_or_delete
Proof state before:
case refine_1.intro.intro.intro.intro.intro.intro.intro.inr
α : 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
e : α
heD : e ∈ D
h : M ／ C ＼ D <m M
⊢ ∃ e ∈ M.E, M ／ C ＼ D ≤m M ／ e ∨ M ／ C ＼ D ≤m M ＼ e
Tactic:
refine ⟨e, hD heD, Or.inr ?_⟩
Proof state after:
case refine_1.intro.intro.intro.intro.intro.intro.intro.inr
α : 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
e : α
heD : e ∈ D
h : M ／ C ＼ D <m M
⊢ M ／ C ＼ D ≤m M ＼ e
Theorem: Matroid.strictMinor_iff_minor_contract_or_delete
Proof state before:
case refine_1.intro.intro.intro.intro.intro.intro.intro.inr
α : 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
e : α
heD : e ∈ D
h : M ／ C ＼ D <m M
⊢ M ／ C ＼ D ≤m M ＼ e
Tactic:
rw [contract_delete_comm _ hCD, ← insert_eq_of_mem heD, ← singleton_union, ← delete_delete]
Proof state after:
case refine_1.intro.intro.intro.intro.intro.intro.intro.inr
α : 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
e : α
heD : e ∈ D
h : M ／ C ＼ D <m M
⊢ M ＼ {e} ＼ D ／ C ≤m M ＼ e
Theorem: Matroid.strictMinor_iff_minor_contract_or_delete
Proof state before:
case refine_1.intro.intro.intro.intro.intro.intro.intro.inr
α : 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
e : α
heD : e ∈ D
h : M ／ C ＼ D <m M
⊢ M ＼ {e} ＼ D ／ C ≤m M ＼ e
Tactic:
apply delete_contract_minor
Proof state after:
no goals
Theorem: Matroid.strictMinor_iff_minor_contract_or_delete
Proof state before:
case refine_1.intro.intro.intro.intro.intro.intro.intro.inl
α : 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
e : α
heC : e ∈ C
h : M ／ C ＼ D <m M
⊢ ∃ e ∈ M.E, M ／ C ＼ D ≤m M ／ e ∨ M ／ C ＼ D ≤m M ＼ e
Tactic:
refine ⟨e, hC heC, Or.inl ?_⟩
Proof state after:
case refine_1.intro.intro.intro.intro.intro.intro.intro.inl
α : 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
e : α
heC : e ∈ C
h : M ／ C ＼ D <m M
⊢ M ／ C ＼ D ≤m M ／ e
Theorem: Matroid.strictMinor_iff_minor_contract_or_delete
Proof state before:
case refine_1.intro.intro.intro.intro.intro.intro.intro.inl
α : 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
e : α
heC : e ∈ C
h : M ／ C ＼ D <m M
⊢ M ／ C ＼ D ≤m M ／ e
Tactic:
rw [← insert_eq_of_mem heC, ← singleton_union, ← contract_contract, contract_elem ]
Proof state after:
case refine_1.intro.intro.intro.intro.intro.intro.intro.inl
α : 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
e : α
heC : e ∈ C
h : M ／ C ＼ D <m M
⊢ M ／ {e} ／ C ＼ D ≤m M ／ {e}
Theorem: Matroid.strictMinor_iff_minor_contract_or_delete
Proof state before:
case refine_1.intro.intro.intro.intro.intro.intro.intro.inl
α : 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
e : α
heC : e ∈ C
h : M ／ C ＼ D <m M
⊢ M ／ {e} ／ C ＼ D ≤m M ／ {e}
Tactic:
apply contract_delete_minor
Proof state after:
no goals
Theorem: Matroid.strictMinor_iff_minor_contract_or_delete
Proof state before:
case refine_2.intro.intro.inl
α : Type u_1
M M' N : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
e : α
he : e ∈ M.E
hc : N ≤m M ／ e
⊢ N <m M
Tactic:
exact hc.trans_strictMinor (contractElem_strictMinor he)
Proof state after:
no goals
Theorem: Matroid.Minor.strictMinor_or_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
⊢ N <m M ∨ N = M
Tactic:
rw [strictMinor_iff_minor_ne, and_iff_right h]
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
⊢ N ≠ M ∨ N = M
Theorem: Matroid.Minor.strictMinor_or_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
⊢ N ≠ M ∨ N = M
Tactic:
exact ne_or_eq N M
Proof state after:
no goals
Theorem: Matroid.Minor.dual
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 M✶
Tactic:
obtain ⟨C, D, -, -, -, rfl⟩ := h
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 α
⊢ (M ／ C ＼ D)✶ ≤m M✶
Theorem: Matroid.Minor.dual
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 α
⊢ (M ／ C ＼ D)✶ ≤m M✶
Tactic:
rw [delete_dual_eq_dual_contract, contract_dual_eq_dual_delete]
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 α
⊢ M✶ ＼ C ／ D ≤m M✶
Theorem: Matroid.Minor.dual
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 α
⊢ M✶ ＼ C ／ D ≤m M✶
Tactic:
apply delete_contract_minor
Proof state after:
no goals
Theorem: Matroid.Minor.of_dual
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 M
Tactic:
simpa using h.dual
Proof state after:
no goals
Theorem: Matroid.minor_dual_iff_dual_minor
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 α
⊢ N ≤m M✶ ↔ N✶ ≤m M
Tactic:
rw [← dual_minor_iff, dual_dual]
Proof state after:
no goals
Theorem: Matroid.StrictMinor.dual
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 M✶
Tactic:
rwa [StrictMinor, dual_minor_iff, dual_minor_iff]
Proof state after:
no goals
Theorem: Matroid.StrictMinor.of_dual
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 M
Tactic:
simpa using h.dual
Proof state after:
no goals
Theorem: Matroid.strictMinor_dual_iff_dual_strictMinor
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 α
⊢ N <m M✶ ↔ N✶ <m M
Tactic:
rw [← dual_strictMinor_iff, dual_dual]
Proof state after:
no goals
Theorem: Matroid.Minor.exists_contract_indep_delete_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
⊢ ∃ C D, M.Indep C ∧ M.Coindep D ∧ Disjoint C D ∧ N = M ／ C ＼ D
Tactic:
obtain ⟨C', D', hC', hD', hCD', rfl⟩ := h
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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
⊢ ∃ C D, M.Indep C ∧ M.Coindep D ∧ Disjoint C D ∧ M ／ C' ＼ D' = M ／ C ＼ D
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
⊢ ∃ C D, M.Indep C ∧ M.Coindep D ∧ Disjoint C D ∧ M ／ C' ＼ D' = M ／ C ＼ D
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis C'
Proof state after:
case intro.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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
⊢ ∃ C D, M.Indep C ∧ M.Coindep D ∧ Disjoint C D ∧ M ／ C' ＼ D' = M ／ C ＼ D
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof state before:
case intro.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' : C' ⊆ M.E
hD' : D' ⊆ M.E
hCD' : Disjoint C' D'
I : Set α
hI : M.Basis I C'
⊢ ∃ C D, M.Indep C ∧ M.Coindep D ∧ Disjoint C D ∧ M ／ C' ＼ D' = M ／ C ＼ D
Tactic:
obtain ⟨K, hK⟩ := M✶.exists_basis D'
Proof state after:
case intro.intro.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' : 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'
⊢ ∃ C D, M.Indep C ∧ M.Coindep D ∧ Disjoint C D ∧ M ／ C' ＼ D' = M ／ C ＼ D
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof state before:
case intro.intro.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' : 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'
⊢ ∃ C D, M.Indep C ∧ M.Coindep D ∧ Disjoint C D ∧ M ／ C' ＼ D' = M ／ C ＼ D
Tactic:
have hIK : Disjoint I K := disjoint_of_subset hI.subset hK.subset hCD'
Proof state after:
case intro.intro.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' : 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 D, M.Indep C ∧ M.Coindep D ∧ Disjoint C D ∧ M ／ C' ＼ D' = M ／ C ＼ D
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof state before:
case intro.intro.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' : 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 D, M.Indep C ∧ M.Coindep D ∧ Disjoint C D ∧ M ／ C' ＼ D' = M ／ C ＼ D
Tactic:
use I ∪ D' \ K, C' \ I ∪ K
Proof state after:
case 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
⊢ M.Indep (I ∪ D' \ K) ∧
    M.Coindep (C' \ I ∪ K) ∧ Disjoint (I ∪ D' \ K) (C' \ I ∪ K) ∧ M ／ C' ＼ D' = M ／ (I ∪ D' \ K) ＼ (C' \ I ∪ K)
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof state before:
case 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
⊢ M.Indep (I ∪ D' \ K) ∧
    M.Coindep (C' \ I ∪ K) ∧ Disjoint (I ∪ D' \ K) (C' \ I ∪ K) ∧ M ／ C' ＼ D' = M ／ (I ∪ D' \ K) ＼ (C' \ I ∪ K)
Tactic:
refine' ⟨_, _, _, _⟩
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
⊢ M.Indep (I ∪ D' \ K)

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)

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)

case h.refine'_4
α : 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' ＼ D' = M ／ (I ∪ D' \ K) ＼ (C' \ I ∪ K)
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof state before:
case h.refine'_4
α : 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' ＼ D' = M ／ (I ∪ D' \ K) ＼ (C' \ I ∪ K)
Tactic:
have hb : (M ／ C')✶.Basis K D' :=
  by
  rw [contract_dual_eq_dual_delete, delete_basis_iff, and_iff_right hK]
  exact hCD'.symm
Proof state after:
case h.refine'_4
α : 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'
⊢ M ／ C' ＼ D' = M ／ (I ∪ D' \ K) ＼ (C' \ I ∪ K)
Theorem: Matroid.Minor.exists_contract_indep_delete_coindep
Proof state before:
case h.refine'_4
α : 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'
⊢ M ／ C' ＼ D' = M ／ (I ∪ D' \ K) ＼ (C' \ I ∪ K)
Tactic:
rw [← dual_dual (M ／ C' ＼ D'), delete_dual_eq_dual_contract, hb.contract_eq_contract_delete,
  hI.contract_eq_contract_delete, delete_dual_eq_dual_contract, contract_dual_eq_dual_delete,
  dual_dual, delete_delete, contract_delete_contract]
Proof state after:
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 ∪ K)
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 ∪ K)
Tactic:
rw [disjoint_union_right, and_iff_left disjoint_sdiff_left]
Proof state after:
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)