internlm/Lean-Github huggingface dataset:
Theorem: Matroid.uniqueBaseOn_nonloop_iff
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).Nonloop e ↔ e ∈ I ∩ E
Tactic:
rw [← indep_singleton, uniqueBaseOn_indep_iff', singleton_subset_iff]
Proof state after:
no goals
Theorem: Matroid.Nonloop.exists_mem_cocircuit
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.Nonloop e
⊢ ∃ K, M.Cocircuit K ∧ e ∈ K
Tactic:
obtain ⟨B, hB, heB⟩ := he.exists_mem_base
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 α
he : M.Nonloop e
B : Set α
hB : M.Base B
heB : e ∈ B
⊢ ∃ K, M.Cocircuit K ∧ e ∈ K
Theorem: Matroid.Nonloop.exists_mem_cocircuit
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 α
he : M.Nonloop e
B : Set α
hB : M.Base B
heB : e ∈ B
⊢ ∃ K, M.Cocircuit K ∧ e ∈ K
Tactic:
exact ⟨_, fundCocct_cocircuit heB hB, mem_fundCocct M e B⟩
Proof state after:
no goals
Theorem: Matroid.toNonloop
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 α
inst✝ : M.Loopless
he : autoParam (e ∈ M.E) _auto✝
⊢ M.Nonloop e
Tactic:
rw [← not_loop_iff, loop_iff_mem_cl_empty, cl_empty_eq_empty]
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 α
inst✝ : M.Loopless
he : autoParam (e ∈ M.E) _auto✝
⊢ e ∉ ∅
Theorem: Matroid.toNonloop
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 α
inst✝ : M.Loopless
he : autoParam (e ∈ M.E) _auto✝
⊢ e ∉ ∅
Tactic:
exact not_mem_empty _
Proof state after:
no goals
Theorem: Matroid.loopless_iff_forall_circuit
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.Loopless ↔ ∀ (C : Set α), M.Circuit C → 1 < C.encard
Tactic:
simp_rw [lt_iff_not_le, encard_le_one_iff_eq, not_or, not_exists, ← nonempty_iff_ne_empty]
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.Loopless ↔ ∀ (C : Set α), M.Circuit C → C.Nonempty ∧ ∀ (x : α), ¬C = {x}
Theorem: Matroid.loopless_iff_forall_circuit
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.Loopless ↔ ∀ (C : Set α), M.Circuit C → C.Nonempty ∧ ∀ (x : α), ¬C = {x}
Tactic:
refine ⟨fun h C hC ↦ ⟨hC.nonempty, fun e ↦ ?_⟩,
  fun h ↦ loopless_iff_forall_nonloop.2 fun e he ↦ (not_loop_iff he).1 fun hel ↦
    (h _ (singleton_circuit.2 hel)).2 e 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 : Set α
h : M.Loopless
C : Set α
hC : M.Circuit C
e : α
⊢ ¬C = {e}
Theorem: Matroid.loopless_iff_forall_circuit
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 α
h : M.Loopless
C : Set α
hC : M.Circuit C
e : α
⊢ ¬C = {e}
Tactic:
rintro 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 : Set α
h : M.Loopless
e : α
hC : M.Circuit {e}
⊢ False
Theorem: Matroid.loopless_iff_forall_circuit
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 α
h : M.Loopless
e : α
hC : M.Circuit {e}
⊢ False
Tactic:
rw [singleton_circuit] at 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 α
h : M.Loopless
e : α
hC : M.Loop e
⊢ False
Theorem: Matroid.loopless_iff_forall_circuit
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 α
h : M.Loopless
e : α
hC : M.Loop e
⊢ False
Tactic:
exact M.not_loop e hC
Proof state after:
no goals
Theorem: Matroid.loopyOn_loopless_iff
Proof state before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K E : Set α
⊢ (loopyOn E).Loopless ↔ E = ∅
Tactic:
simp [loopless_iff_forall_not_loop, eq_empty_iff_forall_not_mem]
Proof state after:
no goals
Theorem: Matroid.removeLoops_eq_self
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 α
inst✝ : M.Loopless
⊢ M.removeLoops = M
Tactic:
rw [removeLoops, ← Loopless.ground_eq, restrict_ground_eq_self]
Proof state after:
no goals
Theorem: Matroid.removeLoops_eq_self_iff
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.removeLoops = M ↔ M.Loopless
Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ M.removeLoops_eq_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 α
h : M.removeLoops = M
⊢ M.Loopless
Theorem: Matroid.removeLoops_eq_self_iff
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 α
h : M.removeLoops = M
⊢ M.Loopless
Tactic:
rw [← 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 α
h : M.removeLoops = M
⊢ M.removeLoops.Loopless
Theorem: Matroid.removeLoops_eq_self_iff
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 α
h : M.removeLoops = M
⊢ M.removeLoops.Loopless
Tactic:
infer_instance
Proof state after:
no goals
Theorem: Matroid.eq_restrict_removeLoops
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 = M.removeLoops ↾ M.E
Tactic:
rw [removeLoops, eq_iff_indep_iff_indep_forall]
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.E = (M ↾ {e | M.Nonloop e} ↾ M.E).E ∧ ∀ I ⊆ M.E, M.Indep I ↔ (M ↾ {e | M.Nonloop e} ↾ M.E).Indep I
Theorem: Matroid.eq_restrict_removeLoops
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.E = (M ↾ {e | M.Nonloop e} ↾ M.E).E ∧ ∀ I ⊆ M.E, M.Indep I ↔ (M ↾ {e | M.Nonloop e} ↾ M.E).Indep I
Tactic:
simp only [restrict_ground_eq, restrict_indep_iff, true_and]
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 α
⊢ ∀ I ⊆ M.E, M.Indep I ↔ (M.Indep I ∧ I ⊆ {e | M.Nonloop e}) ∧ I ⊆ M.E
Theorem: Matroid.eq_restrict_removeLoops
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 α
⊢ ∀ I ⊆ M.E, M.Indep I ↔ (M.Indep I ∧ I ⊆ {e | M.Nonloop e}) ∧ I ⊆ M.E
Tactic:
exact fun I hIE ↦ ⟨fun hI ↦ ⟨⟨hI,fun e heI ↦ hI.nonloop_of_mem heI⟩, hIE⟩, fun hI ↦ hI.1.1⟩
Proof state after:
no goals
Theorem: Matroid.removeLoops_nonloop_iff
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.removeLoops.Nonloop e ↔ M.Nonloop e
Tactic:
rw [removeLoops_eq_restr, restrict_nonloop_iff, mem_setOf, and_self]
Proof state after:
no goals
Theorem: Matroid.removeLoops_idem
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.removeLoops.removeLoops = M.removeLoops
Tactic:
simp [removeLoops_eq_restr]
Proof state after:
no goals
Theorem: Matroid.removeLoops_restr_eq_restr
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 α
hX : X ⊆ {e | M.Nonloop e}
⊢ M.removeLoops ↾ X = M ↾ X
Tactic:
rwa [removeLoops_eq_restr, restrict_restrict_eq]
Proof state after:
no goals
Theorem: Matroid.Loop.dual_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 α
he : M.Loop e
⊢ M✶.Coloop e
Tactic:
rwa [Coloop, dual_dual]
Proof state after:
no goals
Theorem: Matroid.dual_coloop_iff_loop
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 α
h : M✶.Coloop e
⊢ M.Loop e
Tactic:
rw [← dual_dual M]
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 α
h : M✶.Coloop e
⊢ M✶✶.Loop e
Theorem: Matroid.dual_coloop_iff_loop
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 α
h : M✶.Coloop e
⊢ M✶✶.Loop e
Tactic:
exact h.dual_loop
Proof state after:
no goals
Theorem: Matroid.dual_loop_iff_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 α
h : M✶.Loop e
⊢ M.Coloop e
Tactic:
rw [← dual_dual M]
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 α
h : M✶.Loop e
⊢ M✶✶.Coloop e
Theorem: Matroid.dual_loop_iff_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 α
h : M✶.Loop e
⊢ M✶✶.Coloop e
Tactic:
exact h.dual_coloop
Proof state after:
no goals
Theorem: Matroid.coloop_iff_forall_mem_base
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 ↔ ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
Tactic:
simp_rw [← dual_loop_iff_coloop, loop_iff_forall_mem_compl_base, dual_base_iff',
  dual_ground, mem_diff]
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 α
⊢ (∀ (B : Set α), M.Base (M.E \ B) ∧ B ⊆ M.E → e ∈ M.E ∧ e ∉ B) ↔ ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
Theorem: Matroid.coloop_iff_forall_mem_base
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 α
⊢ (∀ (B : Set α), M.Base (M.E \ B) ∧ B ⊆ M.E → e ∈ M.E ∧ e ∉ B) ↔ ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
Tactic:
refine' ⟨fun h B hB ↦ _, fun h B ⟨hB, _⟩ ↦ ⟨hB.subset_ground (h hB), (h hB).2⟩⟩
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 α
h : ∀ (B : Set α), M.Base (M.E \ B) ∧ B ⊆ M.E → e ∈ M.E ∧ e ∉ B
B : Set α
hB : M.Base B
⊢ e ∈ B
Theorem: Matroid.coloop_iff_forall_mem_base
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 α
h : ∀ (B : Set α), M.Base (M.E \ B) ∧ B ⊆ M.E → e ∈ M.E ∧ e ∉ B
B : Set α
hB : M.Base B
⊢ e ∈ B
Tactic:
rw [← diff_diff_cancel_left hB.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 α
h : ∀ (B : Set α), M.Base (M.E \ B) ∧ B ⊆ M.E → e ∈ M.E ∧ e ∉ B
B : Set α
hB : M.Base B
⊢ e ∈ M.E \ (M.E \ B)
Theorem: Matroid.coloop_iff_forall_mem_base
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 α
h : ∀ (B : Set α), M.Base (M.E \ B) ∧ B ⊆ M.E → e ∈ M.E ∧ e ∉ B
B : Set α
hB : M.Base B
⊢ e ∈ M.E \ (M.E \ B)
Tactic:
exact h (M.E \ B) ⟨(by rwa [diff_diff_cancel_left hB.subset_ground]), diff_subset⟩
Proof state after:
no goals
Theorem: Matroid.coloop_iff_forall_mem_base
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 α
h : ∀ (B : Set α), M.Base (M.E \ B) ∧ B ⊆ M.E → e ∈ M.E ∧ e ∉ B
B : Set α
hB : M.Base B
⊢ M.Base (M.E \ (M.E \ B))
Tactic:
rwa [diff_diff_cancel_left hB.subset_ground]
Proof state after:
no goals
Theorem: Matroid.Loop.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 α
h : M.Loop e
⊢ ¬M.Coloop e
Tactic:
rw [← dual_loop_iff_coloop]
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 α
h : M.Loop e
⊢ ¬M✶.Loop e
Theorem: Matroid.Loop.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 α
h : M.Loop e
⊢ ¬M✶.Loop e
Tactic:
rw [← dual_dual M, dual_loop_iff_coloop] at 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 α
h : M✶.Coloop e
⊢ ¬M✶.Loop e
Theorem: Matroid.Loop.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 α
h : M✶.Coloop e
⊢ ¬M✶.Loop e
Tactic:
exact h.nonloop.not_loop
Proof state after:
no goals
Theorem: Matroid.coloop_iff_forall_mem_compl_circuit
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 α
inst✝ : M✶.RkPos
⊢ M.Coloop e ↔ ∀ (C : Set α), M.Circuit C → e ∈ M.E \ C
Tactic:
refine ⟨fun h C hC ↦ ⟨h.mem_ground, h.not_mem_circuit hC⟩, 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 α
inst✝ : M✶.RkPos
h : ∀ (C : Set α), M.Circuit C → e ∈ M.E \ C
⊢ M.Coloop e
Theorem: Matroid.coloop_iff_forall_mem_compl_circuit
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 α
inst✝ : M✶.RkPos
h : ∀ (C : Set α), M.Circuit C → e ∈ M.E \ C
⊢ M.Coloop e
Tactic:
rw [coloop_iff_forall_mem_base]
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 α
inst✝ : M✶.RkPos
h : ∀ (C : Set α), M.Circuit C → e ∈ M.E \ C
⊢ ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
Theorem: Matroid.coloop_iff_forall_mem_compl_circuit
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 α
inst✝ : M✶.RkPos
h : ∀ (C : Set α), M.Circuit C → e ∈ M.E \ C
⊢ ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
Tactic:
refine fun B hB ↦ by_contra fun heB ↦ ?_
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 α
inst✝ : M✶.RkPos
h : ∀ (C : Set α), M.Circuit C → e ∈ M.E \ C
B : Set α
hB : M.Base B
heB : e ∉ B
⊢ False
Theorem: Matroid.coloop_iff_forall_mem_compl_circuit
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 α
inst✝ : M✶.RkPos
h : ∀ (C : Set α), M.Circuit C → e ∈ M.E \ C
B : Set α
hB : M.Base B
heB : e ∉ B
⊢ False
Tactic:
have heE : e ∈ M.E := Exists.elim M.exists_circuit (fun C hC ↦ (h C hC).1)
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 α
inst✝ : M✶.RkPos
h : ∀ (C : Set α), M.Circuit C → e ∈ M.E \ C
B : Set α
hB : M.Base B
heB : e ∉ B
heE : e ∈ M.E
⊢ False
Theorem: Matroid.coloop_iff_forall_mem_compl_circuit
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 α
inst✝ : M✶.RkPos
h : ∀ (C : Set α), M.Circuit C → e ∈ M.E \ C
B : Set α
hB : M.Base B
heB : e ∉ B
heE : e ∈ M.E
⊢ False
Tactic:
rw [← hB.cl_eq] at heE
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 α
inst✝ : M✶.RkPos
h : ∀ (C : Set α), M.Circuit C → e ∈ M.E \ C
B : Set α
hB : M.Base B
heB : e ∉ B
heE : e ∈ M.cl B
⊢ False
Theorem: Matroid.coloop_iff_forall_mem_compl_circuit
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 α
inst✝ : M✶.RkPos
h : ∀ (C : Set α), M.Circuit C → e ∈ M.E \ C
B : Set α
hB : M.Base B
heB : e ∉ B
heE : e ∈ M.cl B
⊢ False
Tactic:
exact (h _ (hB.indep.fundCct_circuit ⟨heE, heB⟩)).2 (mem_fundCct _ _ _)
Proof state after:
no goals
Theorem: Matroid.coloop_iff_forall_mem_cl_iff_mem
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 ↔ (∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E
Tactic:
rw [coloop_iff_forall_mem_base]
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 α
⊢ (∀ ⦃B : Set α⦄, M.Base B → e ∈ B) ↔ (∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E
Theorem: Matroid.coloop_iff_forall_mem_cl_iff_mem
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 α
⊢ (∀ ⦃B : Set α⦄, M.Base B → e ∈ B) ↔ (∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E
Tactic:
refine' ⟨fun h ↦ _, fun h B hB ↦ _⟩
Proof state after:
case refine'_1
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
⊢ (∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E

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 : (∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E
B : Set α
hB : M.Base B
⊢ e ∈ B
Theorem: Matroid.coloop_iff_forall_mem_cl_iff_mem
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 : (∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E
B : Set α
hB : M.Base B
⊢ e ∈ B
Tactic:
rw [← h.1, hB.cl_eq]
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 : (∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E
B : Set α
hB : M.Base B
⊢ e ∈ M.E
Theorem: Matroid.coloop_iff_forall_mem_cl_iff_mem
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 : (∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E
B : Set α
hB : M.Base B
⊢ e ∈ M.E
Tactic:
exact h.2
Proof state after:
no goals
Theorem: Matroid.coloop_iff_forall_mem_cl_iff_mem
Proof state before:
case refine'_1
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
⊢ (∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E
Tactic:
have heE := M.exists_base.elim (fun _ hB ↦ hB.subset_ground (h hB))
Proof state after:
case refine'_1
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
heE : e ∈ M.E
⊢ (∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E
Theorem: Matroid.coloop_iff_forall_mem_cl_iff_mem
Proof state before:
case refine'_1
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
heE : e ∈ M.E
⊢ (∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E
Tactic:
refine' ⟨fun X ↦ ⟨fun heX ↦ _, fun heX ↦ M.mem_cl_of_mem' heX⟩, heE⟩
Proof state after:
case refine'_1
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
heE : e ∈ M.E
X : Set α
heX : e ∈ M.cl X
⊢ e ∈ X
Theorem: Matroid.coloop_iff_forall_mem_cl_iff_mem
Proof state before:
case refine'_1
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
heE : e ∈ M.E
X : Set α
heX : e ∈ M.cl X
⊢ e ∈ X
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis (X ∩ M.E)
Proof state after:
case refine'_1.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X✝ Y Z F C K : Set α
h : ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
heE : e ∈ M.E
X : Set α
heX : e ∈ M.cl X
I : Set α
hI : M.Basis I (X ∩ M.E)
⊢ e ∈ X
Theorem: Matroid.coloop_iff_forall_mem_cl_iff_mem
Proof state before:
case refine'_1.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I✝ X✝ Y Z F C K : Set α
h : ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
heE : e ∈ M.E
X : Set α
heX : e ∈ M.cl X
I : Set α
hI : M.Basis I (X ∩ M.E)
⊢ e ∈ X
Tactic:
obtain ⟨B, hB, hIB⟩ := hI.indep.exists_base_superset
Proof state after:
case refine'_1.intro.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I✝ X✝ Y Z F C K : Set α
h : ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
heE : e ∈ M.E
X : Set α
heX : e ∈ M.cl X
I : Set α
hI : M.Basis I (X ∩ M.E)
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ e ∈ X
Theorem: Matroid.coloop_iff_forall_mem_cl_iff_mem
Proof state before:
case refine'_1.intro.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I✝ X✝ Y Z F C K : Set α
h : ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
heE : e ∈ M.E
X : Set α
heX : e ∈ M.cl X
I : Set α
hI : M.Basis I (X ∩ M.E)
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ e ∈ X
Tactic:
rw [← cl_inter_ground, ← hI.cl_eq_cl] at heX
Proof state after:
case refine'_1.intro.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I✝ X✝ Y Z F C K : Set α
h : ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
heE : e ∈ M.E
X I : Set α
heX : e ∈ M.cl I
hI : M.Basis I (X ∩ M.E)
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ e ∈ X
Theorem: Matroid.coloop_iff_forall_mem_cl_iff_mem
Proof state before:
case refine'_1.intro.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I✝ X✝ Y Z F C K : Set α
h : ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
heE : e ∈ M.E
X I : Set α
heX : e ∈ M.cl I
hI : M.Basis I (X ∩ M.E)
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ e ∈ X
Tactic:
exact (hI.subset ((hB.indep.cl_inter_eq_self_of_subset hIB).subset ⟨heX, h hB⟩)).1
Proof state after:
no goals
Theorem: Matroid.coloop_iff_forall_mem_cl_iff_mem'
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 ↔ (∀ X ⊆ M.E, e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E
Tactic:
rw [coloop_iff_forall_mem_cl_iff_mem, 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 α
⊢ e ∈ M.E → ((∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ↔ ∀ X ⊆ M.E, e ∈ M.cl X ↔ e ∈ X)
Theorem: Matroid.coloop_iff_forall_mem_cl_iff_mem'
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 α
⊢ e ∈ M.E → ((∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ↔ ∀ X ⊆ M.E, e ∈ M.cl X ↔ e ∈ X)
Tactic:
refine fun he ↦ ⟨fun h X _ ↦ h X, fun h X ↦ ?_⟩
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 : e ∈ M.E
h : ∀ X ⊆ M.E, e ∈ M.cl X ↔ e ∈ X
X : Set α
⊢ e ∈ M.cl X ↔ e ∈ X
Theorem: Matroid.coloop_iff_forall_mem_cl_iff_mem'
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 : e ∈ M.E
h : ∀ X ⊆ M.E, e ∈ M.cl X ↔ e ∈ X
X : Set α
⊢ e ∈ M.cl X ↔ e ∈ X
Tactic:
rw [← cl_inter_ground, h (X ∩ M.E) inter_subset_right, mem_inter_iff, and_iff_left he]
Proof state after:
no goals
Theorem: Matroid.Coloop.mem_of_mem_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 α
he : M.Coloop e
hX : e ∈ M.cl X
⊢ e ∈ X
Tactic:
rwa [← he.mem_cl_iff_mem]
Proof state after:
no goals
Theorem: Matroid.coloop_iff_diff_nonspanning
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.Spanning (M.E \ {e})
Tactic:
rw [coloop_iff_forall_mem_cl_iff_mem']
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 α
⊢ (∀ X ⊆ M.E, e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E ↔ ¬M.Spanning (M.E \ {e})
Theorem: Matroid.coloop_iff_diff_nonspanning
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 α
⊢ (∀ X ⊆ M.E, e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E ↔ ¬M.Spanning (M.E \ {e})
Tactic:
refine ⟨fun h hsp ↦ ?_, fun h ↦ ⟨fun X hX ↦ ⟨fun he ↦ ?_, fun he ↦ ?_⟩, by_contra fun h' ↦ h ?_⟩⟩
Proof state after:
case refine_1
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : (∀ X ⊆ M.E, e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E
hsp : M.Spanning (M.E \ {e})
⊢ False

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.Spanning (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
⊢ e ∈ X

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

case refine_4
α : 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})
h' : e ∉ M.E
⊢ M.Spanning (M.E \ {e})
Theorem: Matroid.coloop_iff_diff_nonspanning
Proof state before:
case refine_4
α : 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})
h' : e ∉ M.E
⊢ M.Spanning (M.E \ {e})
Tactic:
rw [spanning_iff_cl, diff_singleton_eq_self h', cl_ground]
Proof state after:
no goals
Theorem: Matroid.coloop_iff_diff_nonspanning
Proof state before:
case refine_1
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : (∀ X ⊆ M.E, e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E
hsp : M.Spanning (M.E \ {e})
⊢ False
Tactic:
simpa [hsp.cl_eq.symm ▸ h.2] using h.1 (M.E \ {e})
Proof state after:
no goals
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.Spanning (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
⊢ e ∈ X
Tactic:
rw [spanning_iff_ground_subset_cl] at 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
⊢ e ∈ X