internlm/Lean-Github huggingface dataset:
Theorem: Matroid.contract_restrict_eq_restrict_contract
Proof state before:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
hJ' : M.Basis' J C
a✝ : M.Indep (I ∪ J)
hd : Disjoint C I
⊢ I ⊆ R ↔ I \ C ⊆ R
Tactic:
rw [hd.sdiff_eq_right]
Proof state after:
no goals
Theorem: Matroid.contract_restrict_eq_restrict_contract
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
⊢ (M ／ C ↾ R).E = ((M ↾ (R ∪ C)) ／ C).E
Tactic:
simp [h.sdiff_eq_right]
Proof state after:
no goals
Theorem: Matroid.contract_restrict_eq_restrict_contract
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
⊢ M.Basis' J C
Tactic:
have := (basis'_restrict_iff.1 hJ).1
Proof state after:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
this : M.Basis' J (C ∩ (R ∪ C))
⊢ M.Basis' J C
Theorem: Matroid.contract_restrict_eq_restrict_contract
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
this : M.Basis' J (C ∩ (R ∪ C))
⊢ M.Basis' J C
Tactic:
rwa [inter_eq_self_of_subset_left subset_union_right] at this
Proof state after:
no goals
Theorem: Matroid.restrict_contract_eq_contract_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₂ M : Matroid α
C R : Set α
hCR : C ⊆ R
⊢ (M ↾ R) ／ C = M ／ C ↾ R \ C
Tactic:
rw [contract_restrict_eq_restrict_contract _ _ _ disjoint_sdiff_right]
Proof state after:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
hCR : C ⊆ R
⊢ (M ↾ R) ／ C = (M ↾ (R \ C ∪ C)) ／ C
Theorem: Matroid.restrict_contract_eq_contract_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₂ M : Matroid α
C R : Set α
hCR : C ⊆ R
⊢ (M ↾ R) ／ C = (M ↾ (R \ C ∪ C)) ／ C
Tactic:
simp [union_eq_self_of_subset_right hCR]
Proof state after:
no goals
Theorem: Matroid.contract_delete_comm
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
⊢ M ／ C ＼ D = M ＼ D ／ C
Tactic:
refine eq_of_indep_iff_indep_forall (by simp [diff_diff_comm]) (fun I hI ↦ ?_)
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 D : Set α
hCD : Disjoint C D
I : Set α
hI : I ⊆ (M ／ C ＼ D).E
⊢ (M ／ C ＼ D).Indep I ↔ (M ＼ D ／ C).Indep I
Theorem: Matroid.contract_delete_comm
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
I : Set α
hI : I ⊆ (M ／ C ＼ D).E
⊢ (M ／ C ＼ D).Indep I ↔ (M ＼ D ／ C).Indep I
Tactic:
rw [delete_ground, contract_ground, subset_diff, subset_diff] at hI
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 D : Set α
hCD : Disjoint C D
I : Set α
hI : (I ⊆ M.E ∧ Disjoint I C) ∧ Disjoint I D
⊢ (M ／ C ＼ D).Indep I ↔ (M ＼ D ／ C).Indep I
Theorem: Matroid.contract_delete_comm
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
I : Set α
hI : (I ⊆ M.E ∧ Disjoint I C) ∧ Disjoint I D
⊢ (M ／ C ＼ D).Indep I ↔ (M ＼ D ／ C).Indep I
Tactic:
simp only [delete_ground, contract_ground, delete_indep_iff, and_iff_left hI.2]
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 D : Set α
hCD : Disjoint C D
I : Set α
hI : (I ⊆ M.E ∧ Disjoint I C) ∧ Disjoint I D
⊢ (M ／ C).Indep I ↔ (M ＼ D ／ C).Indep I
Theorem: Matroid.contract_delete_comm
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
I : Set α
hI : (I ⊆ M.E ∧ Disjoint I C) ∧ Disjoint I D
⊢ (M ／ C).Indep I ↔ (M ＼ D ／ C).Indep I
Tactic:
obtain ⟨J, hJ⟩ := (M ＼ D).exists_basis' C
Proof state after:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
I : Set α
hI : (I ⊆ M.E ∧ Disjoint I C) ∧ Disjoint I D
J : Set α
hJ : (M ＼ D).Basis' J C
⊢ (M ／ C).Indep I ↔ (M ＼ D ／ C).Indep I
Theorem: Matroid.contract_delete_comm
Proof state before:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
I : Set α
hI : (I ⊆ M.E ∧ Disjoint I C) ∧ Disjoint I D
J : Set α
hJ : (M ＼ D).Basis' J C
⊢ (M ／ C).Indep I ↔ (M ＼ D ／ C).Indep I
Tactic:
have hJ' := hJ
Proof state after:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
I : Set α
hI : (I ⊆ M.E ∧ Disjoint I C) ∧ Disjoint I D
J : Set α
hJ hJ' : (M ＼ D).Basis' J C
⊢ (M ／ C).Indep I ↔ (M ＼ D ／ C).Indep I
Theorem: Matroid.contract_delete_comm
Proof state before:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
I : Set α
hI : (I ⊆ M.E ∧ Disjoint I C) ∧ Disjoint I D
J : Set α
hJ hJ' : (M ＼ D).Basis' J C
⊢ (M ／ C).Indep I ↔ (M ＼ D ／ C).Indep I
Tactic:
rw [← restrict_compl, basis'_restrict_iff, subset_diff, diff_eq, inter_comm M.E, ← inter_assoc,
  ← diff_eq, sdiff_eq_left.2 hCD] at hJ'
Proof state after:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
I : Set α
hI : (I ⊆ M.E ∧ Disjoint I C) ∧ Disjoint I D
J : Set α
hJ : (M ＼ D).Basis' J C
hJ' : M.Basis' J (C ∩ M.E) ∧ J ⊆ M.E ∧ Disjoint J D
⊢ (M ／ C).Indep I ↔ (M ＼ D ／ C).Indep I
Theorem: Matroid.contract_delete_comm
Proof state before:
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
I : Set α
hI : (I ⊆ M.E ∧ Disjoint I C) ∧ Disjoint I D
J : Set α
hJ : (M ＼ D).Basis' J C
hJ' : M.Basis' J (C ∩ M.E) ∧ J ⊆ M.E ∧ Disjoint J D
⊢ (M ／ C).Indep I ↔ (M ＼ D ／ C).Indep I
Tactic:
rw [hJ.contract_eq_contract_delete, delete_indep_iff, hJ.indep.contract_indep_iff,
  delete_indep_iff, ← contract_inter_ground_eq, hJ'.1.contract_eq_contract_delete,
  delete_indep_iff,  hJ'.1.indep.contract_indep_iff, disjoint_union_left, and_iff_right hI.2,
  and_iff_left (disjoint_of_subset_right diff_subset hI.1.2), and_iff_left hJ'.2.2,
  and_iff_left
  (disjoint_of_subset_right (diff_subset.trans inter_subset_left) hI.1.2)]
Proof state after:
no goals
Theorem: Matroid.contract_delete_comm
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
⊢ (M ／ C ＼ D).E = (M ＼ D ／ C).E
Tactic:
simp [diff_diff_comm]
Proof state after:
no goals
Theorem: Matroid.contract_delete_comm'
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
⊢ M ／ C ＼ D = M ＼ (D \ C) ／ C
Tactic:
rw [contract_delete_diff, contract_delete_comm _ disjoint_sdiff_right]
Proof state after:
no goals
Theorem: Matroid.delete_contract_diff
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
D C : Set α
⊢ M ＼ D ／ C = M ＼ D ／ (C \ D)
Tactic:
rw [contract_eq_contract_iff, delete_ground, diff_inter_diff_right, diff_eq, diff_eq, inter_assoc]
Proof state after:
no goals
Theorem: Matroid.delete_contract_comm'
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 C : Set α
⊢ M ＼ D ／ C = M ／ (C \ D) ＼ D
Tactic:
rw [delete_contract_diff, ← contract_delete_comm _ disjoint_sdiff_left]
Proof state after:
no goals
Theorem: Matroid.contract_delete_contract'
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D C' : Set α
⊢ M ／ C ＼ D ／ C' = M ／ (C ∪ C' \ D) ＼ D
Tactic:
rw [delete_contract_diff, ← contract_delete_comm _ disjoint_sdiff_left, contract_contract]
Proof state after:
no goals
Theorem: Matroid.contract_delete_contract
Proof state before:
α : Type u_1
M✝ M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D C' : Set α
h : Disjoint C' D
⊢ M ／ C ＼ D ／ C' = M ／ (C ∪ C') ＼ D
Tactic:
rw [contract_delete_contract', sdiff_eq_left.mpr h]
Proof state after:
no goals
Theorem: Matroid.contract_delete_contract_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₂ M : Matroid α
C D C' D' : Set α
⊢ M ／ C ＼ D ／ C' ＼ D' = M ／ (C ∪ C' \ D) ＼ (D ∪ D')
Tactic:
rw [contract_delete_contract', delete_delete]
Proof state after:
no goals
Theorem: Matroid.contract_delete_contract_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₂ M : Matroid α
C D C' D' : Set α
h : Disjoint C' D
⊢ M ／ C ＼ D ／ C' ＼ D' = M ／ (C ∪ C') ＼ (D ∪ D')
Tactic:
rw [contract_delete_contract_delete', sdiff_eq_left.mpr h]
Proof state after:
no goals
Theorem: Matroid.delete_contract_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₂ M : Matroid α
D C D' : Set α
⊢ M ＼ D ／ C ＼ D' = M ／ (C \ D) ＼ (D ∪ D')
Tactic:
rw [delete_contract_comm', delete_delete]
Proof state after:
no goals
Theorem: Matroid.delete_contract_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₂ M : Matroid α
D C D' : Set α
h : Disjoint C D
⊢ M ＼ D ／ C ＼ D' = M ／ C ＼ (D ∪ D')
Tactic:
rw [delete_contract_delete', sdiff_eq_left.mpr h]
Proof state after:
no goals
Theorem: Matroid.contract_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 α
C D : Set α
⊢ M ／ C ＼ D ≤m M
Tactic:
rw [contract_delete_diff, ← contract_inter_ground_eq, ← delete_inter_ground_eq,
  contract_ground, diff_inter_self_eq_diff, diff_inter_diff_right, inter_diff_right_comm]
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 D : Set α
⊢ M ／ (C ∩ M.E) ＼ (D \ C ∩ M.E) ≤m M
Theorem: Matroid.contract_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 α
C D : Set α
⊢ M ／ (C ∩ M.E) ＼ (D \ C ∩ M.E) ≤m M
Tactic:
refine ⟨_,_, inter_subset_right, inter_subset_right, ?_, rfl⟩
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 D : Set α
⊢ Disjoint (C ∩ M.E) (D \ C ∩ M.E)
Theorem: Matroid.contract_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 α
C D : Set α
⊢ Disjoint (C ∩ M.E) (D \ C ∩ M.E)
Tactic:
exact disjoint_of_subset inter_subset_left inter_subset_left disjoint_sdiff_right
Proof state after:
no goals
Theorem: Matroid.minor_iff_exists_contract_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 α
x✝ : ∃ C D, N = M ／ C ＼ D
C D : Set α
h : N = M ／ C ＼ D
⊢ N ≤m M
Tactic:
rw [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 α
x✝ : ∃ C D, N = M ／ C ＼ D
C D : Set α
h : N = M ／ C ＼ D
⊢ M ／ C ＼ D ≤m M
Theorem: Matroid.minor_iff_exists_contract_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 α
x✝ : ∃ C D, N = M ／ C ＼ D
C D : Set α
h : N = M ／ C ＼ D
⊢ M ／ C ＼ D ≤m M
Tactic:
apply contract_delete_minor
Proof state after:
no goals
Theorem: Matroid.Indep.of_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 α
hI : N.Indep I
hNM : N ≤m M
⊢ M.Indep I
Tactic:
obtain ⟨C,D, rfl⟩ := minor_iff_exists_contract_delete.1 hNM
Proof state after:
case 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 α
hI : (M ／ C ＼ D).Indep I
hNM : M ／ C ＼ D ≤m M
⊢ M.Indep I
Theorem: Matroid.Indep.of_minor
Proof state before:
case 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 α
hI : (M ／ C ＼ D).Indep I
hNM : M ／ C ＼ D ≤m M
⊢ M.Indep I
Tactic:
exact hI.of_delete.of_contract
Proof state after:
no goals
Theorem: Matroid.Nonloop.of_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.Nonloop e
hNM : N ≤m M
⊢ M.Nonloop e
Tactic:
obtain ⟨C, D, rfl⟩ := minor_iff_exists_contract_delete.1 hNM
Proof state after:
case 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 α
h : (M ／ C ＼ D).Nonloop e
hNM : M ／ C ＼ D ≤m M
⊢ M.Nonloop e
Theorem: Matroid.Nonloop.of_minor
Proof state before:
case 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 α
h : (M ／ C ＼ D).Nonloop e
hNM : M ／ C ＼ D ≤m M
⊢ M.Nonloop e
Tactic:
exact h.of_delete.of_contract
Proof state after:
no goals
Theorem: Matroid.Loop.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 α
he : M.Loop e
heN : e ∈ N.E
hNM : N ≤m M
⊢ N.Loop e
Tactic:
rw [← not_nonloop_iff]
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 α
he : M.Loop e
heN : e ∈ N.E
hNM : N ≤m M
⊢ ¬N.Nonloop e
Theorem: Matroid.Loop.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 α
he : M.Loop e
heN : e ∈ N.E
hNM : N ≤m M
⊢ ¬N.Nonloop e
Tactic:
exact fun hnl ↦ he.not_nonloop <| hnl.of_minor hNM
Proof state after:
no goals
Theorem: Matroid.Minor.eq_of_ground_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₂ : Matroid α
h : N ≤m M
hE : M.E ⊆ N.E
⊢ M = N
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 α
hE : M.E ⊆ (M ／ C ＼ D).E
⊢ M = M ／ C ＼ D
Theorem: Matroid.Minor.eq_of_ground_subset
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 α
hE : M.E ⊆ (M ／ C ＼ D).E
⊢ M = M ／ C ＼ D
Tactic:
rw [delete_ground, contract_ground, subset_diff, subset_diff] at hE
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 α
hE : (M.E ⊆ M.E ∧ Disjoint M.E C) ∧ Disjoint M.E D
⊢ M = M ／ C ＼ D
Theorem: Matroid.Minor.eq_of_ground_subset
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 α
hE : (M.E ⊆ M.E ∧ Disjoint M.E C) ∧ Disjoint M.E D
⊢ M = M ／ C ＼ D
Tactic:
rw [← contract_inter_ground_eq, hE.1.2.symm.inter_eq, contract_empty, ← delete_inter_ground_eq,
  hE.2.symm.inter_eq, delete_empty]
Proof state after:
no goals
Theorem: Matroid.Minor.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₂ : Matroid α
h : N ≤m M
⊢ N.E ⊆ M.E
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).E ⊆ M.E
Theorem: Matroid.Minor.subset
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).E ⊆ M.E
Tactic:
exact diff_subset.trans diff_subset
Proof state after:
no goals
Theorem: Matroid.Minor.refl
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 α
⊢ M = M ／ ∅ ＼ ∅
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.Minor.trans
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₁ M₂ M₃ : Matroid α
h : M₁ ≤m M₂
h' : M₂ ≤m M₃
⊢ M₁ ≤m M₃
Tactic:
obtain ⟨C₁, D₁, -, -, -, rfl⟩ := h
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 : Set α
M₀ M₁ M₂✝ M₂ M₃ : Matroid α
h' : M₂ ≤m M₃
C₁ D₁ : Set α
⊢ M₂ ／ C₁ ＼ D₁ ≤m M₃
Theorem: Matroid.Minor.trans
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 : Set α
M₀ M₁ M₂✝ M₂ M₃ : Matroid α
h' : M₂ ≤m M₃
C₁ D₁ : Set α
⊢ M₂ ／ C₁ ＼ D₁ ≤m M₃
Tactic:
obtain ⟨C₂, D₂, -, -, -, rfl⟩ := h'
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M₃ : Matroid α
C₁ D₁ C₂ D₂ : Set α
⊢ M₃ ／ C₂ ＼ D₂ ／ C₁ ＼ D₁ ≤m M₃
Theorem: Matroid.Minor.trans
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M₃ : Matroid α
C₁ D₁ C₂ D₂ : Set α
⊢ M₃ ／ C₂ ＼ D₂ ／ C₁ ＼ D₁ ≤m M₃
Tactic:
rw [contract_delete_contract_delete']
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M₃ : Matroid α
C₁ D₁ C₂ D₂ : Set α
⊢ M₃ ／ (C₂ ∪ C₁ \ D₂) ＼ (D₂ ∪ D₁) ≤m M₃
Theorem: Matroid.Minor.trans
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M₃ : Matroid α
C₁ D₁ C₂ D₂ : Set α
⊢ M₃ ／ (C₂ ∪ C₁ \ D₂) ＼ (D₂ ∪ D₁) ≤m M₃
Tactic:
apply contract_delete_minor
Proof state after:
no goals
Theorem: Matroid.Minor.finiteRk
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
inst✝ : M.FiniteRk
⊢ N.FiniteRk
Tactic:
obtain ⟨C, D, rfl⟩ := minor_iff_exists_contract_delete.1 h
Proof state after:
case intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
inst✝ : M.FiniteRk
C D : Set α
h : M ／ C ＼ D ≤m M
⊢ (M ／ C ＼ D).FiniteRk
Theorem: Matroid.Minor.finiteRk
Proof state before:
case intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
inst✝ : M.FiniteRk
C D : Set α
h : M ／ C ＼ D ≤m M
⊢ (M ／ C ＼ D).FiniteRk
Tactic:
infer_instance
Proof state after:
no goals
Theorem: Matroid.Minor.finitary
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
inst✝ : M.Finitary
⊢ N.Finitary
Tactic:
obtain ⟨C, D, rfl⟩ := minor_iff_exists_contract_delete.1 h
Proof state after:
case intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
inst✝ : M.Finitary
C D : Set α
h : M ／ C ＼ D ≤m M
⊢ (M ／ C ＼ D).Finitary
Theorem: Matroid.Minor.finitary
Proof state before:
case intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
inst✝ : M.Finitary
C D : Set α
h : M ／ C ＼ D ≤m M
⊢ (M ／ C ＼ D).Finitary
Tactic:
infer_instance
Proof state after:
no goals
Theorem: Matroid.strictMinor_iff_minor_ssubset
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 α
x✝ : N ≤m M ∧ N.E ⊂ M.E
h : N ≤m M
hss : N.E ⊂ M.E
h' : M ≤m N
⊢ N.E = M.E
Tactic:
rw [h'.antisymm h]
Proof state after:
no goals
Theorem: Matroid.strictMinor_iff_exists_eq_contract_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 ↔ ∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ (C ∪ D).Nonempty ∧ N = M ／ C ＼ D
Tactic:
rw [strictMinor_iff_minor_ssubset, minor_def]
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 α
⊢ (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D) ∧ N.E ⊂ M.E ↔
    ∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ (C ∪ D).Nonempty ∧ N = M ／ C ＼ D
Theorem: Matroid.strictMinor_iff_exists_eq_contract_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 α
⊢ (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D) ∧ N.E ⊂ M.E ↔
    ∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ (C ∪ D).Nonempty ∧ N = M ／ C ＼ D
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
⊢ (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D) ∧ N.E ⊂ M.E →
    ∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ (C ∪ D).Nonempty ∧ N = M ／ C ＼ D

case mpr
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
⊢ (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ (C ∪ D).Nonempty ∧ N = M ／ C ＼ D) →
    (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D) ∧ N.E ⊂ M.E
Theorem: Matroid.strictMinor_iff_exists_eq_contract_delete
Proof state before:
case mp
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
⊢ (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D) ∧ N.E ⊂ M.E →
    ∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ (C ∪ D).Nonempty ∧ N = M ／ C ＼ D

case mpr
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
⊢ (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ (C ∪ D).Nonempty ∧ N = M ／ C ＼ D) →
    (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D) ∧ N.E ⊂ M.E
Tactic:
rintro ⟨⟨C, D, hC, hD, hCD, rfl⟩, 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 ／ 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

case mpr
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
⊢ (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ (C ∪ D).Nonempty ∧ N = M ／ C ＼ D) →
    (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D) ∧ N.E ⊂ M.E
Theorem: Matroid.strictMinor_iff_exists_eq_contract_delete
Proof state before:
case mpr
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
⊢ (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ (C ∪ D).Nonempty ∧ N = M ／ C ＼ D) →
    (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D) ∧ N.E ⊂ M.E
Tactic:
rintro ⟨C, D, hC, hD, hCD, ⟨e,he⟩, rfl⟩
Proof state after:
case mpr.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
e : α
he : e ∈ C ∪ D
⊢ (∃ C_1 D_1, C_1 ⊆ M.E ∧ D_1 ⊆ M.E ∧ Disjoint C_1 D_1 ∧ M ／ C ＼ D = M ／ C_1 ＼ D_1) ∧ (M ／ C ＼ D).E ⊂ M.E
Theorem: Matroid.strictMinor_iff_exists_eq_contract_delete
Proof state before:
case mpr.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
e : α
he : e ∈ C ∪ D
⊢ (∃ C_1 D_1, C_1 ⊆ M.E ∧ D_1 ⊆ M.E ∧ Disjoint C_1 D_1 ∧ M ／ C ＼ D = M ／ C_1 ＼ D_1) ∧ (M ／ C ＼ D).E ⊂ M.E
Tactic:
use ⟨C, D, hC, hD, hCD, rfl⟩
Proof state after:
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 ／ C ＼ D).E ⊂ M.E
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 ／ C ＼ D).E ⊂ M.E
Tactic:
rw [delete_ground, contract_ground, diff_diff, ssubset_iff_subset_not_subset,
  and_iff_right diff_subset]
Proof state after:
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)