internlm/Lean-Github huggingface dataset:
Theorem: Matroid.cl_diff_eq_of_subset_coloops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
hK : K ⊆ M✶.cl ∅
⊢ ∀ ⦃a : α⦄, a ∈ K → ∀ ⦃b : α⦄, b ∈ M.cl (X \ K) → a ≠ b
Tactic:
rintro e heK _ heX rfl
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I X✝ Y Z F C K X : Set α
hK : K ⊆ M✶.cl ∅
e : α
heK : e ∈ K
heX : e ∈ M.cl (X \ K)
⊢ False
Theorem: Matroid.cl_diff_eq_of_subset_coloops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I X✝ Y Z F C K X : Set α
hK : K ⊆ M✶.cl ∅
e : α
heK : e ∈ K
heX : e ∈ M.cl (X \ K)
⊢ False
Tactic:
have he : M.Coloop e := hK heK
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I X✝ Y Z F C K X : Set α
hK : K ⊆ M✶.cl ∅
e : α
heK : e ∈ K
heX : e ∈ M.cl (X \ K)
he : M.Coloop e
⊢ False
Theorem: Matroid.cl_diff_eq_of_subset_coloops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I X✝ Y Z F C K X : Set α
hK : K ⊆ M✶.cl ∅
e : α
heK : e ∈ K
heX : e ∈ M.cl (X \ K)
he : M.Coloop e
⊢ False
Tactic:
rw [he.mem_cl_iff_mem] at heX
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I X✝ Y Z F C K X : Set α
hK : K ⊆ M✶.cl ∅
e : α
heK : e ∈ K
heX : e ∈ X \ K
he : M.Coloop e
⊢ False
Theorem: Matroid.cl_diff_eq_of_subset_coloops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I X✝ Y Z F C K X : Set α
hK : K ⊆ M✶.cl ∅
e : α
heK : e ∈ K
heX : e ∈ X \ K
he : M.Coloop e
⊢ False
Tactic:
exact heX.2 heK
Proof state after:
no goals
Theorem: Matroid.cl_disjoint_of_disjoint_of_subset_coloops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hXK : Disjoint X K
hK : K ⊆ M✶.cl ∅
⊢ Disjoint (M.cl X) K
Tactic:
rwa [disjoint_iff_inter_eq_empty, cl_inter_eq_of_subset_coloops X hK,
  ← disjoint_iff_inter_eq_empty]
Proof state after:
no goals
Theorem: Matroid.Coloop.insert_indep_of_indep
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Coloop e
hI : M.Indep I
⊢ M.Indep (insert e I)
Tactic:
refine (em (e ∈ I)).elim (fun h ↦ by rwa [insert_eq_of_mem h]) fun h ↦ ?_
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Coloop e
hI : M.Indep I
h : e ∉ I
⊢ M.Indep (insert e I)
Theorem: Matroid.Coloop.insert_indep_of_indep
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Coloop e
hI : M.Indep I
h : e ∉ I
⊢ M.Indep (insert e I)
Tactic:
rw [← hI.not_mem_cl_iff_of_not_mem h]
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Coloop e
hI : M.Indep I
h : e ∉ I
⊢ e ∉ M.cl I
Theorem: Matroid.Coloop.insert_indep_of_indep
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Coloop e
hI : M.Indep I
h : e ∉ I
⊢ e ∉ M.cl I
Tactic:
exact he.not_mem_cl_of_not_mem h
Proof state after:
no goals
Theorem: Matroid.Coloop.insert_indep_of_indep
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Coloop e
hI : M.Indep I
h : e ∈ I
⊢ M.Indep (insert e I)
Tactic:
rwa [insert_eq_of_mem h]
Proof state after:
no goals
Theorem: Matroid.union_indep_iff_indep_of_subset_coloops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hK : K ⊆ M✶.cl ∅
⊢ M.Indep (I ∪ K) ↔ M.Indep I
Tactic:
refine ⟨fun h ↦ h.subset subset_union_left, fun h ↦ ?_⟩
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hK : K ⊆ M✶.cl ∅
h : M.Indep I
⊢ M.Indep (I ∪ K)
Theorem: Matroid.union_indep_iff_indep_of_subset_coloops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hK : K ⊆ M✶.cl ∅
h : M.Indep I
⊢ M.Indep (I ∪ K)
Tactic:
obtain ⟨B, hB, hIB⟩ := h.exists_base_superset
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hK : K ⊆ M✶.cl ∅
h : M.Indep I
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ M.Indep (I ∪ K)
Theorem: Matroid.union_indep_iff_indep_of_subset_coloops
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hK : K ⊆ M✶.cl ∅
h : M.Indep I
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ M.Indep (I ∪ K)
Tactic:
exact hB.indep.subset (union_subset hIB (hK.trans fun e he ↦ Coloop.mem_of_base he hB))
Proof state after:
no goals
Theorem: Matroid.diff_indep_iff_indep_of_subset_coloops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hK : K ⊆ M✶.cl ∅
⊢ M.Indep (I \ K) ↔ M.Indep I
Tactic:
rw [← union_indep_iff_indep_of_subset_coloops hK, diff_union_self,
  union_indep_iff_indep_of_subset_coloops hK]
Proof state after:
no goals
Theorem: Matroid.coloops_indep
Proof state before:
α : Type u_1
β : Type u_2
M✝ N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
M : Matroid α
⊢ M.Indep (M✶.cl ∅)
Tactic:
rw [indep_iff_diff_coloops_indep, diff_self]
Proof state after:
α : Type u_1
β : Type u_2
M✝ N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
M : Matroid α
⊢ M.Indep ∅
Theorem: Matroid.coloops_indep
Proof state before:
α : Type u_1
β : Type u_2
M✝ N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
M : Matroid α
⊢ M.Indep ∅
Tactic:
exact M.empty_indep
Proof state after:
no goals
Theorem: Matroid.eq_of_indep_iff_indep_forall_disjoint_loops_coloops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
⊢ M₁ = M₂
Tactic:
refine' eq_of_indep_iff_indep_forall hE fun I hI ↦ _
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I
Theorem: Matroid.eq_of_indep_iff_indep_forall_disjoint_loops_coloops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I
Tactic:
rw [indep_iff_diff_coloops_indep, @indep_iff_diff_coloops_indep _ M₂, ← hc]
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep (I \ M₁✶.cl ∅) ↔ M₂.Indep (I \ M₁✶.cl ∅)
Theorem: Matroid.eq_of_indep_iff_indep_forall_disjoint_loops_coloops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep (I \ M₁✶.cl ∅) ↔ M₂.Indep (I \ M₁✶.cl ∅)
Tactic:
obtain hdj | hndj := em (Disjoint I (M₁.cl ∅))
Proof state after:
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I (M₁.cl ∅)
⊢ M₁.Indep (I \ M₁✶.cl ∅) ↔ M₂.Indep (I \ M₁✶.cl ∅)

case inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I (M₁.cl ∅)
⊢ M₁.Indep (I \ M₁✶.cl ∅) ↔ M₂.Indep (I \ M₁✶.cl ∅)
Theorem: Matroid.eq_of_indep_iff_indep_forall_disjoint_loops_coloops
Proof state before:
case inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I (M₁.cl ∅)
⊢ M₁.Indep (I \ M₁✶.cl ∅) ↔ M₂.Indep (I \ M₁✶.cl ∅)
Tactic:
obtain ⟨e, heI, hel : M₁.Loop e⟩ := not_disjoint_iff_nonempty_inter.mp hndj
Proof state after:
case inr.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I (M₁.cl ∅)
e : α
heI : e ∈ I
hel : M₁.Loop e
⊢ M₁.Indep (I \ M₁✶.cl ∅) ↔ M₂.Indep (I \ M₁✶.cl ∅)
Theorem: Matroid.eq_of_indep_iff_indep_forall_disjoint_loops_coloops
Proof state before:
case inr.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I (M₁.cl ∅)
e : α
heI : e ∈ I
hel : M₁.Loop e
⊢ M₁.Indep (I \ M₁✶.cl ∅) ↔ M₂.Indep (I \ M₁✶.cl ∅)
Tactic:
refine' iff_of_false (hel.not_indep_of_mem ⟨heI, hel.not_coloop⟩) _
Proof state after:
case inr.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I (M₁.cl ∅)
e : α
heI : e ∈ I
hel : M₁.Loop e
⊢ ¬M₂.Indep (I \ M₁✶.cl ∅)
Theorem: Matroid.eq_of_indep_iff_indep_forall_disjoint_loops_coloops
Proof state before:
case inr.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I (M₁.cl ∅)
e : α
heI : e ∈ I
hel : M₁.Loop e
⊢ ¬M₂.Indep (I \ M₁✶.cl ∅)
Tactic:
rw [loop_iff_mem_cl_empty, hl, ← loop_iff_mem_cl_empty] at hel
Proof state after:
case inr.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I (M₁.cl ∅)
e : α
heI : e ∈ I
hel : M₂.Loop e
⊢ ¬M₂.Indep (I \ M₁✶.cl ∅)
Theorem: Matroid.eq_of_indep_iff_indep_forall_disjoint_loops_coloops
Proof state before:
case inr.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I (M₁.cl ∅)
e : α
heI : e ∈ I
hel : M₂.Loop e
⊢ ¬M₂.Indep (I \ M₁✶.cl ∅)
Tactic:
rw [hc]
Proof state after:
case inr.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I (M₁.cl ∅)
e : α
heI : e ∈ I
hel : M₂.Loop e
⊢ ¬M₂.Indep (I \ M₂✶.cl ∅)
Theorem: Matroid.eq_of_indep_iff_indep_forall_disjoint_loops_coloops
Proof state before:
case inr.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e✝ f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hndj : ¬Disjoint I (M₁.cl ∅)
e : α
heI : e ∈ I
hel : M₂.Loop e
⊢ ¬M₂.Indep (I \ M₂✶.cl ∅)
Tactic:
exact hel.not_indep_of_mem ⟨heI, hel.not_coloop⟩
Proof state after:
no goals
Theorem: Matroid.eq_of_indep_iff_indep_forall_disjoint_loops_coloops
Proof state before:
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I (M₁.cl ∅)
⊢ M₁.Indep (I \ M₁✶.cl ∅) ↔ M₂.Indep (I \ M₁✶.cl ∅)
Tactic:
rw [h _ (diff_subset.trans hI)]
Proof state after:
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I (M₁.cl ∅)
⊢ Disjoint (I \ M₁✶.cl ∅) (M₁.cl ∅ ∪ M₁✶.cl ∅)
Theorem: Matroid.eq_of_indep_iff_indep_forall_disjoint_loops_coloops
Proof state before:
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I (M₁.cl ∅)
⊢ Disjoint (I \ M₁✶.cl ∅) (M₁.cl ∅ ∪ M₁✶.cl ∅)
Tactic:
rw [disjoint_union_right]
Proof state after:
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I (M₁.cl ∅)
⊢ Disjoint (I \ M₁✶.cl ∅) (M₁.cl ∅) ∧ Disjoint (I \ M₁✶.cl ∅) (M₁✶.cl ∅)
Theorem: Matroid.eq_of_indep_iff_indep_forall_disjoint_loops_coloops
Proof state before:
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K : Set α
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hl : M₁.cl ∅ = M₂.cl ∅
hc : M₁✶.cl ∅ = M₂✶.cl ∅
h : ∀ I ⊆ M₁.E, Disjoint I (M₁.cl ∅ ∪ M₁✶.cl ∅) → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
hdj : Disjoint I (M₁.cl ∅)
⊢ Disjoint (I \ M₁✶.cl ∅) (M₁.cl ∅) ∧ Disjoint (I \ M₁✶.cl ∅) (M₁✶.cl ∅)
Tactic:
exact ⟨disjoint_of_subset_left diff_subset hdj, disjoint_sdiff_left⟩
Proof state after:
no goals
Theorem: Matroid.eq_uniqueBaseOn_of_loops_union_coloops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
⊢ M = uniqueBaseOn (M✶.cl ∅) M.E
Tactic:
refine eq_of_base_iff_base_forall rfl (fun B hBE ↦ ?_)
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B ⊆ M.E
⊢ M.Base B ↔ (uniqueBaseOn (M✶.cl ∅) M.E).Base B
Theorem: Matroid.eq_uniqueBaseOn_of_loops_union_coloops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B ⊆ M.E
⊢ M.Base B ↔ (uniqueBaseOn (M✶.cl ∅) M.E).Base B
Tactic:
rw [uniqueBaseOn_base_iff (show M✶.cl ∅ ⊆ M.E from M✶.cl_subset_ground _)]
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B ⊆ M.E
⊢ M.Base B ↔ B = M✶.cl ∅
Theorem: Matroid.eq_uniqueBaseOn_of_loops_union_coloops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B ⊆ M.E
⊢ M.Base B ↔ B = M✶.cl ∅
Tactic:
rw [hE, ← diff_subset_iff] at hBE
Proof state after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B \ M.cl ∅ ⊆ M✶.cl ∅
⊢ M.Base B ↔ B = M✶.cl ∅
Theorem: Matroid.eq_uniqueBaseOn_of_loops_union_coloops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B \ M.cl ∅ ⊆ M✶.cl ∅
⊢ M.Base B ↔ B = M✶.cl ∅
Tactic:
use fun h ↦ h.coloops_subset.antisymm' (by rwa [sdiff_eq_left.mpr h.indep.disjoint_loops] at hBE)
Proof state after:
case mpr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B \ M.cl ∅ ⊆ M✶.cl ∅
⊢ B = M✶.cl ∅ → M.Base B
Theorem: Matroid.eq_uniqueBaseOn_of_loops_union_coloops
Proof state before:
case mpr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B \ M.cl ∅ ⊆ M✶.cl ∅
⊢ B = M✶.cl ∅ → M.Base B
Tactic:
rintro rfl
Proof state after:
case mpr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
hBE : M✶.cl ∅ \ M.cl ∅ ⊆ M✶.cl ∅
⊢ M.Base (M✶.cl ∅)
Theorem: Matroid.eq_uniqueBaseOn_of_loops_union_coloops
Proof state before:
case mpr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
hBE : M✶.cl ∅ \ M.cl ∅ ⊆ M✶.cl ∅
⊢ M.Base (M✶.cl ∅)
Tactic:
obtain ⟨B, hB⟩ := M.exists_base
Proof state after:
case mpr.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
hBE : M✶.cl ∅ \ M.cl ∅ ⊆ M✶.cl ∅
B : Set α
hB : M.Base B
⊢ M.Base (M✶.cl ∅)
Theorem: Matroid.eq_uniqueBaseOn_of_loops_union_coloops
Proof state before:
case mpr.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
hBE : M✶.cl ∅ \ M.cl ∅ ⊆ M✶.cl ∅
B : Set α
hB : M.Base B
⊢ M.Base (M✶.cl ∅)
Tactic:
rwa [hB.coloops_subset.antisymm ]
Proof state after:
case mpr.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
hBE : M✶.cl ∅ \ M.cl ∅ ⊆ M✶.cl ∅
B : Set α
hB : M.Base B
⊢ B ⊆ M✶.cl ∅
Theorem: Matroid.eq_uniqueBaseOn_of_loops_union_coloops
Proof state before:
case mpr.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
hBE : M✶.cl ∅ \ M.cl ∅ ⊆ M✶.cl ∅
B : Set α
hB : M.Base B
⊢ B ⊆ M✶.cl ∅
Tactic:
refine subset_trans ?_ (diff_subset_iff.2 hE.subset)
Proof state after:
case mpr.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
hBE : M✶.cl ∅ \ M.cl ∅ ⊆ M✶.cl ∅
B : Set α
hB : M.Base B
⊢ B ⊆ M.E \ M.cl ∅
Theorem: Matroid.eq_uniqueBaseOn_of_loops_union_coloops
Proof state before:
case mpr.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
hBE : M✶.cl ∅ \ M.cl ∅ ⊆ M✶.cl ∅
B : Set α
hB : M.Base B
⊢ B ⊆ M.E \ M.cl ∅
Tactic:
rw [subset_diff, and_iff_right hB.subset_ground]
Proof state after:
case mpr.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
hBE : M✶.cl ∅ \ M.cl ∅ ⊆ M✶.cl ∅
B : Set α
hB : M.Base B
⊢ Disjoint B (M.cl ∅)
Theorem: Matroid.eq_uniqueBaseOn_of_loops_union_coloops
Proof state before:
case mpr.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
hBE : M✶.cl ∅ \ M.cl ∅ ⊆ M✶.cl ∅
B : Set α
hB : M.Base B
⊢ Disjoint B (M.cl ∅)
Tactic:
exact hB.indep.disjoint_loops
Proof state after:
no goals
Theorem: Matroid.eq_uniqueBaseOn_of_loops_union_coloops
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
hE : M.E = M.cl ∅ ∪ M✶.cl ∅
B : Set α
hBE : B \ M.cl ∅ ⊆ M✶.cl ∅
h : M.Base B
⊢ B ⊆ M✶.cl ∅
Tactic:
rwa [sdiff_eq_left.mpr h.indep.disjoint_loops] at hBE
Proof state after:
no goals
Theorem: Matroid.uniqueBaseOn_loops_eq
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K I E : Set α
⊢ (uniqueBaseOn I E).cl ∅ = E \ I
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.uniqueBaseOn_coloops_eq'
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K I E : Set α
⊢ (uniqueBaseOn I E)✶.cl ∅ = I ∩ E
Tactic:
simp [inter_comm I]
Proof state after:
no goals
Theorem: Matroid.uniqueBaseOn_coloops_eq
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X Y Z F C K I E : Set α
h : I ⊆ E
⊢ (uniqueBaseOn I E)✶.cl ∅ = I
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Matroid.truncateTo_top
Proof state before:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k : ℕ∞
M : Matroid α
⊢ ∀ I ⊆ (M.truncateTo ⊤).E, (M.truncateTo ⊤).Indep I ↔ M.Indep I
Tactic:
simp [truncateTo]
Proof state after:
no goals
Theorem: Matroid.truncateTo_zero
Proof state before:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k : ℕ∞
M : Matroid α
⊢ M.truncateTo 0 = loopyOn M.E
Tactic:
refine eq_of_indep_iff_indep_forall rfl ?_
Proof state after:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k : ℕ∞
M : Matroid α
⊢ ∀ I ⊆ (M.truncateTo 0).E, (M.truncateTo 0).Indep I ↔ (loopyOn M.E).Indep I
Theorem: Matroid.truncateTo_zero
Proof state before:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k : ℕ∞
M : Matroid α
⊢ ∀ I ⊆ (M.truncateTo 0).E, (M.truncateTo 0).Indep I ↔ (loopyOn M.E).Indep I
Tactic:
suffices ∀ I ⊆ M.E, I = ∅ → M.Indep I by simpa
Proof state after:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k : ℕ∞
M : Matroid α
⊢ ∀ I ⊆ M.E, I = ∅ → M.Indep I
Theorem: Matroid.truncateTo_zero
Proof state before:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k : ℕ∞
M : Matroid α
⊢ ∀ I ⊆ M.E, I = ∅ → M.Indep I
Tactic:
rintro I - rfl
Proof state after:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k : ℕ∞
M : Matroid α
⊢ M.Indep ∅
Theorem: Matroid.truncateTo_zero
Proof state before:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k : ℕ∞
M : Matroid α
⊢ M.Indep ∅
Tactic:
exact M.empty_indep
Proof state after:
no goals
Theorem: Matroid.truncateTo_zero
Proof state before:
α : Type u_1
M✝ : Matroid α
E I B : Set α
k : ℕ∞
M : Matroid α
this : ∀ I ⊆ M.E, I = ∅ → M.Indep I
⊢ ∀ I ⊆ (M.truncateTo 0).E, (M.truncateTo 0).Indep I ↔ (loopyOn M.E).Indep I
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.truncateTo_emptyOn
Proof state before:
α✝ : Type u_1
M : Matroid α✝
E I B : Set α✝
k✝ : ℕ∞
α : Type u_2
k : ℕ∞
⊢ (emptyOn α).truncateTo k = emptyOn α
Tactic:
rw [← ground_eq_empty_iff, truncateTo_ground_eq, emptyOn_ground]
Proof state after:
no goals
Theorem: Matroid.truncate_loopyOn
Proof state before:
α : Type u_1
M : Matroid α
E✝ I B : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ (loopyOn E).truncateTo k = loopyOn E
Tactic:
apply eq_of_indep_iff_indep_forall (by simp)
Proof state after:
α : Type u_1
M : Matroid α
E✝ I B : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ ∀ I ⊆ ((loopyOn E).truncateTo k).E, ((loopyOn E).truncateTo k).Indep I ↔ (loopyOn E).Indep I
Theorem: Matroid.truncate_loopyOn
Proof state before:
α : Type u_1
M : Matroid α
E✝ I B : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ ∀ I ⊆ ((loopyOn E).truncateTo k).E, ((loopyOn E).truncateTo k).Indep I ↔ (loopyOn E).Indep I
Tactic:
suffices ∀ I ⊆ E, I = ∅ → encard I ≤ k by simpa
Proof state after:
α : Type u_1
M : Matroid α
E✝ I B : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ ∀ I ⊆ E, I = ∅ → I.encard ≤ k
Theorem: Matroid.truncate_loopyOn
Proof state before:
α : Type u_1
M : Matroid α
E✝ I B : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ ∀ I ⊆ E, I = ∅ → I.encard ≤ k
Tactic:
rintro _ - rfl
Proof state after:
α : Type u_1
M : Matroid α
E✝ I B : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ ∅.encard ≤ k
Theorem: Matroid.truncate_loopyOn
Proof state before:
α : Type u_1
M : Matroid α
E✝ I B : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ ∅.encard ≤ k
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.truncate_loopyOn
Proof state before:
α : Type u_1
M : Matroid α
E✝ I B : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
⊢ ((loopyOn E).truncateTo k).E = (loopyOn E).E
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.truncate_loopyOn
Proof state before:
α : Type u_1
M : Matroid α
E✝ I B : Set α
k✝ : ℕ∞
E : Set α
k : ℕ∞
this : ∀ I ⊆ E, I = ∅ → I.encard ≤ k
⊢ ∀ I ⊆ ((loopyOn E).truncateTo k).E, ((loopyOn E).truncateTo k).Indep I ↔ (loopyOn E).Indep I
Tactic:
simpa
Proof state after:
no goals