internlm/Lean-Github huggingface dataset:
Theorem: Matroid.coloop_iff_diff_nonspanning
Proof state before:
case refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.E ⊆ M.cl (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
⊢ e ∈ X
Tactic:
refine by_contra fun he' ↦ h ?_
Proof state after:
case refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.E ⊆ M.cl (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
he' : e ∉ X
⊢ M.E ⊆ M.cl (M.E \ {e})
Theorem: Matroid.coloop_iff_diff_nonspanning
Proof state before:
case refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.E ⊆ M.cl (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
he' : e ∉ X
⊢ M.E ⊆ M.cl (M.E \ {e})
Tactic:
rw [← union_eq_self_of_subset_left (subset_diff_singleton hX he'), ← cl_union_cl_left_eq,
  ← insert_eq_of_mem he, ← union_singleton, union_assoc, union_diff_self, singleton_union,
  ← cl_ground]
Proof state after:
case refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.E ⊆ M.cl (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
he' : e ∉ X
⊢ M.cl M.E ⊆ M.cl (M.cl X ∪ insert e (M.cl M.E))
Theorem: Matroid.coloop_iff_diff_nonspanning
Proof state before:
case refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.E ⊆ M.cl (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
he' : e ∉ X
⊢ M.cl M.E ⊆ M.cl (M.cl X ∪ insert e (M.cl M.E))
Tactic:
apply M.cl_subset_cl
Proof state after:
case refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.E ⊆ M.cl (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
he' : e ∉ X
⊢ M.E ⊆ M.cl X ∪ insert e (M.cl M.E)
Theorem: Matroid.coloop_iff_diff_nonspanning
Proof state before:
case refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.E ⊆ M.cl (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
he' : e ∉ X
⊢ M.E ⊆ M.cl X ∪ insert e (M.cl M.E)
Tactic:
rw [cl_ground]
Proof state after:
case refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.E ⊆ M.cl (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
he' : e ∉ X
⊢ M.E ⊆ M.cl X ∪ insert e M.E
Theorem: Matroid.coloop_iff_diff_nonspanning
Proof state before:
case refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.E ⊆ M.cl (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
he' : e ∉ X
⊢ M.E ⊆ M.cl X ∪ insert e M.E
Tactic:
exact (subset_insert _ _).trans subset_union_right
Proof state after:
no goals
Theorem: Matroid.coloop_iff_diff_nonspanning
Proof state before:
case refine_3
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.Spanning (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ X
⊢ e ∈ M.cl X
Tactic:
exact M.subset_cl X hX he
Proof state after:
no goals
Theorem: Matroid.coloop_iff_diff_cl
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.Coloop e ↔ M.cl (M.E \ {e}) ≠ M.E
Tactic:
rw [coloop_iff_diff_nonspanning, spanning_iff_cl]
Proof state after:
no goals
Theorem: Matroid.coloop_iff_not_mem_cl_compl
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 : autoParam (e ∈ M.E) _auto✝
⊢ M.Coloop e ↔ e ∉ M.cl (M.E \ {e})
Tactic:
rw [coloop_iff_diff_cl, not_iff_not]
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 : autoParam (e ∈ M.E) _auto✝
⊢ M.cl (M.E \ {e}) = M.E ↔ e ∈ M.cl (M.E \ {e})
Theorem: Matroid.coloop_iff_not_mem_cl_compl
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 : autoParam (e ∈ M.E) _auto✝
⊢ M.cl (M.E \ {e}) = M.E ↔ e ∈ M.cl (M.E \ {e})
Tactic:
refine ⟨fun h ↦ by rwa [h], fun h ↦ (M.cl_subset_ground _).antisymm fun x hx ↦ ?_⟩
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 : autoParam (e ∈ M.E) _auto✝
h : e ∈ M.cl (M.E \ {e})
x : α
hx : x ∈ M.E
⊢ x ∈ M.cl (M.E \ {e})
Theorem: Matroid.coloop_iff_not_mem_cl_compl
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 : autoParam (e ∈ M.E) _auto✝
h : e ∈ M.cl (M.E \ {e})
x : α
hx : x ∈ M.E
⊢ x ∈ M.cl (M.E \ {e})
Tactic:
obtain (rfl | hne) := eq_or_ne x e
Proof state after:
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
f : α
B L L' I X Y Z F C K : Set α
x : α
hx : x ∈ M.E
he : autoParam (x ∈ M.E) _auto✝
h : x ∈ M.cl (M.E \ {x})
⊢ x ∈ M.cl (M.E \ {x})

case inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : autoParam (e ∈ M.E) _auto✝
h : e ∈ M.cl (M.E \ {e})
x : α
hx : x ∈ M.E
hne : x ≠ e
⊢ x ∈ M.cl (M.E \ {e})
Theorem: Matroid.coloop_iff_not_mem_cl_compl
Proof state before:
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
f : α
B L L' I X Y Z F C K : Set α
x : α
hx : x ∈ M.E
he : autoParam (x ∈ M.E) _auto✝
h : x ∈ M.cl (M.E \ {x})
⊢ x ∈ M.cl (M.E \ {x})

case inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : autoParam (e ∈ M.E) _auto✝
h : e ∈ M.cl (M.E \ {e})
x : α
hx : x ∈ M.E
hne : x ≠ e
⊢ x ∈ M.cl (M.E \ {e})
Tactic:
assumption
Proof state after:
case inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : autoParam (e ∈ M.E) _auto✝
h : e ∈ M.cl (M.E \ {e})
x : α
hx : x ∈ M.E
hne : x ≠ e
⊢ x ∈ M.cl (M.E \ {e})
Theorem: Matroid.coloop_iff_not_mem_cl_compl
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 α
he : autoParam (e ∈ M.E) _auto✝
h : e ∈ M.cl (M.E \ {e})
x : α
hx : x ∈ M.E
hne : x ≠ e
⊢ x ∈ M.cl (M.E \ {e})
Tactic:
exact M.subset_cl (M.E \ {e}) diff_subset (show x ∈ M.E \ {e} from ⟨hx, hne⟩)
Proof state after:
no goals
Theorem: Matroid.coloop_iff_not_mem_cl_compl
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 : autoParam (e ∈ M.E) _auto✝
h : M.cl (M.E \ {e}) = M.E
⊢ e ∈ M.cl (M.E \ {e})
Tactic:
rwa [h]
Proof state after:
no goals
Theorem: Matroid.Base.mem_coloop_iff_forall_not_mem_fundCct
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 α
hB : M.Base B
he : e ∈ B
⊢ M.Coloop e ↔ ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
Tactic:
refine ⟨fun h x hx heC ↦ (h.not_mem_circuit <| hB.fundCct_circuit hx) heC, 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 α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
⊢ M.Coloop e
Theorem: Matroid.Base.mem_coloop_iff_forall_not_mem_fundCct
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 α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
h' : M.E \ {e} ⊆ M.cl (B \ {e})
⊢ M.Coloop e
Tactic:
rw [coloop_iff_not_mem_cl_compl (hB.subset_ground he)]
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 α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
h' : M.E \ {e} ⊆ M.cl (B \ {e})
⊢ e ∉ M.cl (M.E \ {e})
Theorem: Matroid.Base.mem_coloop_iff_forall_not_mem_fundCct
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 α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
h' : M.E \ {e} ⊆ M.cl (B \ {e})
⊢ e ∉ M.cl (M.E \ {e})
Tactic:
exact not_mem_subset (M.cl_subset_cl_of_subset_cl h') <| hB.indep.not_mem_cl_diff_of_mem he
Proof state after:
no goals
Theorem: Matroid.Base.mem_coloop_iff_forall_not_mem_fundCct
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 α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
⊢ M.E \ {e} ⊆ M.cl (B \ {e})
Tactic:
rintro x ⟨hxE, hne : x ≠ e⟩
Proof state after:
case intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
⊢ x ∈ M.cl (B \ {e})
Theorem: Matroid.Base.mem_coloop_iff_forall_not_mem_fundCct
Proof state before:
case intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
⊢ x ∈ M.cl (B \ {e})
Tactic:
obtain (hx | hx) := em (x ∈ B)
Proof state after:
case intro.inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∈ B
⊢ x ∈ M.cl (B \ {e})

case intro.inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
⊢ x ∈ M.cl (B \ {e})
Theorem: Matroid.Base.mem_coloop_iff_forall_not_mem_fundCct
Proof state before:
case intro.inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
⊢ x ∈ M.cl (B \ {e})
Tactic:
have h_cct := (hB.fundCct_circuit ⟨hxE, hx⟩).mem_cl_diff_singleton_of_mem
  (M.mem_fundCct x B)
Proof state after:
case intro.inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.cl (M.fundCct x B \ {x})
⊢ x ∈ M.cl (B \ {e})
Theorem: Matroid.Base.mem_coloop_iff_forall_not_mem_fundCct
Proof state before:
case intro.inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.cl (M.fundCct x B \ {x})
⊢ x ∈ M.cl (B \ {e})
Tactic:
refine (M.cl_subset_cl (subset_diff_singleton ?_ ?_)) h_cct
Proof state after:
case intro.inr.refine_1
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.cl (M.fundCct x B \ {x})
⊢ M.fundCct x B \ {x} ⊆ B

case intro.inr.refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.cl (M.fundCct x B \ {x})
⊢ e ∉ M.fundCct x B \ {x}
Theorem: Matroid.Base.mem_coloop_iff_forall_not_mem_fundCct
Proof state before:
case intro.inr.refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.cl (M.fundCct x B \ {x})
⊢ e ∉ M.fundCct x B \ {x}
Tactic:
simp [hne.symm, h x ⟨hxE, hx⟩]
Proof state after:
no goals
Theorem: Matroid.Base.mem_coloop_iff_forall_not_mem_fundCct
Proof state before:
case intro.inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∈ B
⊢ x ∈ M.cl (B \ {e})
Tactic:
exact M.subset_cl (B \ {e}) (diff_subset.trans hB.subset_ground) ⟨hx, hne⟩
Proof state after:
no goals
Theorem: Matroid.Base.mem_coloop_iff_forall_not_mem_fundCct
Proof state before:
case intro.inr.refine_1
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.cl (M.fundCct x B \ {x})
⊢ M.fundCct x B \ {x} ⊆ B
Tactic:
simpa using fundCct_subset_insert _ _
Proof state after:
no goals
Theorem: Matroid.exists_mem_circuit_of_not_coloop
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 α
heE : e ∈ M.E
he : ¬M.Coloop e
⊢ ∃ C, M.Circuit C ∧ e ∈ C
Tactic:
simp only [coloop_iff_forall_mem_base, not_forall, Classical.not_imp, exists_prop] at he
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 α
heE : e ∈ M.E
he : ∃ x, M.Base x ∧ e ∉ x
⊢ ∃ C, M.Circuit C ∧ e ∈ C
Theorem: Matroid.exists_mem_circuit_of_not_coloop
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 α
heE : e ∈ M.E
he : ∃ x, M.Base x ∧ e ∉ x
⊢ ∃ C, M.Circuit C ∧ e ∈ C
Tactic:
obtain ⟨B, hB, heB⟩ := he
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 α
heE : e ∈ M.E
B : Set α
hB : M.Base B
heB : e ∉ B
⊢ ∃ C, M.Circuit C ∧ e ∈ C
Theorem: Matroid.exists_mem_circuit_of_not_coloop
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 α
heE : e ∈ M.E
B : Set α
hB : M.Base B
heB : e ∉ B
⊢ ∃ C, M.Circuit C ∧ e ∈ C
Tactic:
exact ⟨M.fundCct e B, hB.fundCct_circuit ⟨heE,heB⟩, .inl rfl⟩
Proof state after:
no goals
Theorem: Matroid.cl_inter_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 : Set α
M : Matroid α
X : Set α
⊢ M.cl X ∩ M✶.cl ∅ = X ∩ M✶.cl ∅
Tactic:
simp_rw [Set.ext_iff, mem_inter_iff, ← coloop_iff_mem_cl_empty, and_congr_left_iff]
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 α
X : Set α
⊢ ∀ (x : α), M.Coloop x → (x ∈ M.cl X ↔ x ∈ X)
Theorem: Matroid.cl_inter_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 : Set α
M : Matroid α
X : Set α
⊢ ∀ (x : α), M.Coloop x → (x ∈ M.cl X ↔ x ∈ X)
Tactic:
intro e he
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 α
X : Set α
e : α
he : M.Coloop e
⊢ e ∈ M.cl X ↔ e ∈ X
Theorem: Matroid.cl_inter_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 : Set α
M : Matroid α
X : Set α
e : α
he : M.Coloop e
⊢ e ∈ M.cl X ↔ e ∈ X
Tactic:
rw [he.mem_cl_iff_mem]
Proof state after:
no goals
Theorem: Matroid.cl_inter_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 ∅
⊢ M.cl X ∩ K = X ∩ K
Tactic:
have hKE : K ∩ M.E = K := by
  rw [inter_eq_left, ← dual_ground]; exact hK.trans (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 X : Set α
hK : K ⊆ M✶.cl ∅
hKE : K ∩ M.E = K
⊢ M.cl X ∩ K = X ∩ K
Theorem: Matroid.cl_inter_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 ∅
hKE : K ∩ M.E = K
⊢ M.cl X ∩ K = X ∩ K
Tactic:
rw [← hKE, ← inter_assoc X, inter_right_comm, hKE, ← cl_inter_ground,
  subset_antisymm_iff, and_iff_left (inter_subset_inter_left K (M.subset_cl _)),
  ← inter_eq_self_of_subset_right hK, ← inter_assoc, cl_inter_coloops_eq,
  inter_assoc]
Proof state after:
no goals
Theorem: Matroid.cl_inter_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 ∅
⊢ K ∩ M.E = K
Tactic:
rw [inter_eq_left, ← dual_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 X : Set α
hK : K ⊆ M✶.cl ∅
⊢ K ⊆ M✶.E
Theorem: Matroid.cl_inter_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 ∅
⊢ K ⊆ M✶.E
Tactic:
exact hK.trans (cl_subset_ground _ _)
Proof state after:
no goals
Theorem: Matroid.cl_insert_coloop_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 X : Set α
he : M.Coloop e
⊢ M.cl (insert e X) = insert e (M.cl X)
Tactic:
rw [ subset_antisymm_iff, insert_subset_iff, and_iff_left (M.cl_subset_cl (subset_insert _ _)),
  and_iff_left (M.mem_cl_of_mem' (mem_insert _ _)), ← union_singleton (s := M.cl X),
  ← diff_subset_iff, subset_singleton_iff]
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 α
he : M.Coloop e
⊢ ∀ y ∈ M.cl (insert e X) \ M.cl X, y = e
Theorem: Matroid.cl_insert_coloop_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 X : Set α
he : M.Coloop e
⊢ ∀ y ∈ M.cl (insert e X) \ M.cl X, y = e
Tactic:
refine fun f hf ↦ (he.mem_of_mem_cl (cl_exchange hf).1).elim Eq.symm (fun heX ↦ False.elim ?_)
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 α
he : M.Coloop e
f : α
hf : f ∈ M.cl (insert e X) \ M.cl X
heX : e ∈ X
⊢ False
Theorem: Matroid.cl_insert_coloop_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 X : Set α
he : M.Coloop e
f : α
hf : f ∈ M.cl (insert e X) \ M.cl X
heX : e ∈ X
⊢ False
Tactic:
simp [insert_eq_of_mem heX] at hf
Proof state after:
no goals
Theorem: Matroid.cl_union_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 ∅
⊢ M.cl (X ∪ K) = M.cl X ∪ K
Tactic:
rw [← cl_union_cl_left_eq]
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 ∅
⊢ M.cl (M.cl X ∪ K) = M.cl X ∪ K
Theorem: Matroid.cl_union_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 ∅
⊢ M.cl (M.cl X ∪ K) = M.cl X ∪ K
Tactic:
refine' (M.subset_cl _).antisymm' fun e he ↦ _
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 : α
he : e ∈ M.cl (M.cl X ∪ K)
⊢ e ∈ M.cl X ∪ K
Theorem: Matroid.cl_union_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 : α
he : e ∈ M.cl (M.cl X ∪ K)
⊢ e ∈ M.cl X ∪ K
Tactic:
obtain he' | ⟨C, hC, heC, hCss⟩ := (mem_cl_iff_mem_or_exists_circuit
  (union_subset (M.cl_subset_ground _) (hK.trans (M✶.cl_subset_ground _)))).1 he
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 X : Set α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
he' : e ∈ M.cl X ∪ K
⊢ e ∈ M.cl X ∪ K

case inr.intro.intro.intro
α : 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 : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
⊢ e ∈ M.cl X ∪ K
Theorem: Matroid.cl_union_eq_of_subset_coloops
Proof state before:
case inr.intro.intro.intro
α : 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 : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
hCX : C \ {e} ⊆ M.cl X
⊢ e ∈ M.cl X ∪ K
Tactic:
exact Or.inl (M.cl_subset_cl_of_subset_cl hCX (hC.mem_cl_diff_singleton_of_mem heC))
Proof state after:
no goals
Theorem: Matroid.cl_union_eq_of_subset_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 X : Set α
hK : K ⊆ M✶.cl ∅
e : α
he : e ∈ M.cl (M.cl X ∪ K)
he' : e ∈ M.cl X ∪ K
⊢ e ∈ M.cl X ∪ K
Tactic:
exact he'
Proof state after:
no goals
Theorem: Matroid.cl_union_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 : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
⊢ C \ {e} ⊆ M.cl X
Tactic:
rw [diff_subset_iff, singleton_union]
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 : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
⊢ C ⊆ insert e (M.cl X)
Theorem: Matroid.cl_union_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 : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
⊢ C ⊆ insert e (M.cl X)
Tactic:
refine (subset_inter hCss Subset.rfl).trans ?_
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 : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
⊢ insert e (M.cl X ∪ K) ∩ C ⊆ insert e (M.cl X)
Theorem: Matroid.cl_union_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 : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
⊢ insert e (M.cl X ∪ K) ∩ C ⊆ insert e (M.cl X)
Tactic:
rintro f ⟨rfl | h1 | h2, h⟩
Proof state after:
case intro.inl
α : 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 ∅
C : Set α
hC : M.Circuit C
f : α
h : f ∈ C
he : f ∈ M.cl (M.cl X ∪ K)
heC : f ∈ C
hCss : C ⊆ insert f (M.cl X ∪ K)
⊢ f ∈ insert f (M.cl X)

case intro.inr.inl
α : 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 : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
f : α
h : f ∈ C
h1 : f ∈ M.cl X
⊢ f ∈ insert e (M.cl X)

case intro.inr.inr
α : 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 : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
f : α
h : f ∈ C
h2 : f ∈ K
⊢ f ∈ insert e (M.cl X)
Theorem: Matroid.cl_union_eq_of_subset_coloops
Proof state before:
case intro.inr.inr
α : 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 : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
f : α
h : f ∈ C
h2 : f ∈ K
⊢ f ∈ insert e (M.cl X)
Tactic:
exact (hC.not_coloop_of_mem h (hK h2)).elim
Proof state after:
no goals
Theorem: Matroid.cl_union_eq_of_subset_coloops
Proof state before:
case intro.inl
α : 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 ∅
C : Set α
hC : M.Circuit C
f : α
h : f ∈ C
he : f ∈ M.cl (M.cl X ∪ K)
heC : f ∈ C
hCss : C ⊆ insert f (M.cl X ∪ K)
⊢ f ∈ insert f (M.cl X)
Tactic:
apply mem_insert
Proof state after:
no goals
Theorem: Matroid.cl_union_eq_of_subset_coloops
Proof state before:
case intro.inr.inl
α : 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 : α
he : e ∈ M.cl (M.cl X ∪ K)
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCss : C ⊆ insert e (M.cl X ∪ K)
f : α
h : f ∈ C
h1 : f ∈ M.cl X
⊢ f ∈ insert e (M.cl X)
Tactic:
exact Or.inr h1
Proof state after:
no goals
Theorem: Matroid.cl_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 : Set α
hK : K ⊆ M✶.cl ∅
⊢ M.cl K = K ∪ M.cl ∅
Tactic:
rw [← empty_union K, cl_union_eq_of_subset_coloops _ hK, empty_union, union_comm]
Proof state after:
no goals
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 ∅
⊢ M.cl (X \ K) = M.cl X \ K
Tactic:
nth_rw 2 [← inter_union_diff X K]
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 ∅
⊢ M.cl (X \ K) = M.cl (X ∩ K ∪ X \ K) \ K
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 ∅
⊢ M.cl (X \ K) = M.cl (X ∩ K ∪ X \ K) \ K
Tactic:
rw [union_comm, cl_union_eq_of_subset_coloops _ (inter_subset_right.trans hK),
  union_diff_distrib, diff_eq_empty.mpr inter_subset_right, union_empty, eq_comm,
  sdiff_eq_self_iff_disjoint, disjoint_iff_forall_ne]
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 ∅
⊢ ∀ ⦃a : α⦄, a ∈ K → ∀ ⦃b : α⦄, b ∈ M.cl (X \ K) → a ≠ b