internlm/Lean-Github huggingface dataset:
Theorem: Matroid.not_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 α
he : autoParam (e ∈ M.E) _auto✝
⊢ ¬M.Nonloop e ↔ M.Loop e
Tactic:
rw [← not_loop_iff, not_not]
Proof state after:
no goals
Theorem: Matroid.nonloop_iff_mem_compl_loops
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.Nonloop e ↔ e ∈ M.E \ M.cl ∅
Tactic:
rw [Nonloop, Loop, and_comm, mem_diff]
Proof state after:
no goals
Theorem: Matroid.not_nonloop_iff_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.Nonloop e ↔ M.cl {e} = M.cl ∅
Tactic:
by_cases he : e ∈ M.E
Proof state after:
case pos
α : 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
⊢ ¬M.Nonloop e ↔ M.cl {e} = M.cl ∅

case neg
α : 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
⊢ ¬M.Nonloop e ↔ M.cl {e} = M.cl ∅
Theorem: Matroid.not_nonloop_iff_cl
Proof state before:
case neg
α : 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
⊢ ¬M.Nonloop e ↔ M.cl {e} = M.cl ∅
Tactic:
simp [← cl_inter_ground, singleton_inter_eq_empty.2 he,
  (show ¬ M.Nonloop e from fun h ↦ he h.mem_ground)]
Proof state after:
no goals
Theorem: Matroid.not_nonloop_iff_cl
Proof state before:
case pos
α : 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
⊢ ¬M.Nonloop e ↔ M.cl {e} = M.cl ∅
Tactic:
simp [Nonloop, and_comm, not_and, not_not, loop_iff_cl_eq_cl_empty', he]
Proof state after:
no goals
Theorem: Matroid.loop_or_nonloop
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 α
e : α
he : autoParam (e ∈ M.E) _auto✝
⊢ M.Loop e ∨ M.Nonloop e
Tactic:
rw [Nonloop, and_iff_left 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 α
e : α
he : autoParam (e ∈ M.E) _auto✝
⊢ M.Loop e ∨ ¬M.Loop e
Theorem: Matroid.loop_or_nonloop
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 α
e : α
he : autoParam (e ∈ M.E) _auto✝
⊢ M.Loop e ∨ ¬M.Loop e
Tactic:
apply em
Proof state after:
no goals
Theorem: Matroid.indep_singleton
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.Indep {e} ↔ M.Nonloop e
Tactic:
rw [Nonloop, ← singleton_dep, dep_iff, not_and, not_imp_not, singleton_subset_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.Indep {e} ↔ (e ∈ M.E → M.Indep {e}) ∧ e ∈ M.E
Theorem: Matroid.indep_singleton
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.Indep {e} ↔ (e ∈ M.E → M.Indep {e}) ∧ e ∈ M.E
Tactic:
exact ⟨fun h ↦ ⟨fun _ ↦ h, singleton_subset_iff.mp h.subset_ground⟩, fun h ↦ h.1 h.2⟩
Proof state after:
no goals
Theorem: Matroid.Indep.nonloop_of_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 α
hI : M.Indep I
h : e ∈ I
⊢ M.Nonloop e
Tactic:
rw [← not_loop_iff (hI.subset_ground 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 α
hI : M.Indep I
h : e ∈ I
⊢ ¬M.Loop e
Theorem: Matroid.Indep.nonloop_of_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 α
hI : M.Indep I
h : e ∈ I
⊢ ¬M.Loop e
Tactic:
exact fun he ↦ (he.not_mem_of_indep hI) h
Proof state after:
no goals
Theorem: Matroid.Nonloop.exists_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 α
he : M.Nonloop e
⊢ ∃ B, M.Base B ∧ e ∈ B
Tactic:
simpa using (indep_singleton.2 he).exists_base_superset
Proof state after:
no goals
Theorem: Matroid.Cocircuit.nonloop_of_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 α
hK : M.Cocircuit K
he : e ∈ K
⊢ M.Nonloop e
Tactic:
rw [← not_loop_iff (hK.subset_ground he), ← singleton_circuit]
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 : M.Cocircuit K
he : e ∈ K
⊢ ¬M.Circuit {e}
Theorem: Matroid.Cocircuit.nonloop_of_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 α
hK : M.Cocircuit K
he : e ∈ K
⊢ ¬M.Circuit {e}
Tactic:
intro 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 α
hK : M.Cocircuit K
he : e ∈ K
he' : M.Circuit {e}
⊢ False
Theorem: Matroid.Cocircuit.nonloop_of_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 α
hK : M.Cocircuit K
he : e ∈ K
he' : M.Circuit {e}
⊢ False
Tactic:
obtain ⟨f, ⟨rfl, -⟩, hfe⟩ := (he'.cocircuit_inter_nontrivial hK ⟨e, by simp [he]⟩).exists_ne e
Proof state after:
case intro.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
f✝ : α
B L L' I X Y Z F C K : Set α
hK : M.Cocircuit K
f : α
he : f ∈ K
he' : M.Circuit {f}
hfe : f ≠ f
⊢ False
Theorem: Matroid.Cocircuit.nonloop_of_mem
Proof state before:
case intro.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
f✝ : α
B L L' I X Y Z F C K : Set α
hK : M.Cocircuit K
f : α
he : f ∈ K
he' : M.Circuit {f}
hfe : f ≠ f
⊢ False
Tactic:
exact hfe rfl
Proof state after:
no goals
Theorem: Matroid.Cocircuit.nonloop_of_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 α
hK : M.Cocircuit K
he : e ∈ K
he' : M.Circuit {e}
⊢ e ∈ {e} ∩ K
Tactic:
simp [he]
Proof state after:
no goals
Theorem: Matroid.Circuit.nonloop_of_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 α
hC : M.Circuit C
hC' : C.Nontrivial
he : e ∈ C
hL : M.Loop e
⊢ False
Tactic:
simp [hL.eq_of_circuit_mem hC he] at hC'
Proof state after:
no goals
Theorem: Matroid.Circuit.nonloop_of_mem_of_one_lt_card
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 α
hC : M.Circuit C
h : 1 < C.encard
he : e ∈ C
⊢ M.Nonloop e
Tactic:
refine nonloop_of_not_loop (hC.subset_ground he) (fun hlp ↦ ?_)
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 α
hC : M.Circuit C
h : 1 < C.encard
he : e ∈ C
hlp : M.Loop e
⊢ False
Theorem: Matroid.Circuit.nonloop_of_mem_of_one_lt_card
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 α
hC : M.Circuit C
h : 1 < C.encard
he : e ∈ C
hlp : M.Loop e
⊢ False
Tactic:
rw [hlp.eq_of_circuit_mem hC he, encard_singleton] 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 α
hC : M.Circuit C
h : 1 < 1
he : e ∈ C
hlp : M.Loop e
⊢ False
Theorem: Matroid.Circuit.nonloop_of_mem_of_one_lt_card
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 α
hC : M.Circuit C
h : 1 < 1
he : e ∈ C
hlp : M.Loop e
⊢ False
Tactic:
exact h.ne rfl
Proof state after:
no goals
Theorem: Matroid.nonloop_iff_not_mem_cl_empty
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.Nonloop e ↔ e ∉ M.cl ∅
Tactic:
rw [Nonloop, loop_iff_mem_cl_empty, and_iff_left he]
Proof state after:
no goals
Theorem: Matroid.Nonloop.mem_cl_singleton
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
hef : e ∈ M.cl {f}
⊢ f ∈ M.cl {e}
Tactic:
rw [← union_empty {_}, singleton_union] at *
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.Nonloop e
hef : e ∈ M.cl (insert f ∅)
⊢ f ∈ M.cl (insert e ∅)
Theorem: Matroid.Nonloop.mem_cl_singleton
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
hef : e ∈ M.cl (insert f ∅)
⊢ f ∈ M.cl (insert e ∅)
Tactic:
exact (M.cl_exchange (X := ∅) ⟨hef, (nonloop_iff_not_mem_cl_empty he.mem_ground).1 he⟩).1
Proof state after:
no goals
Theorem: Matroid.Nonloop.nonloop_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.Nonloop e
hef : e ∈ M.cl {f}
⊢ M.Nonloop f
Tactic:
rw [Nonloop, and_comm]
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.Nonloop e
hef : e ∈ M.cl {f}
⊢ f ∈ M.E ∧ ¬M.Loop f
Theorem: Matroid.Nonloop.nonloop_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.Nonloop e
hef : e ∈ M.cl {f}
⊢ f ∈ M.E ∧ ¬M.Loop f
Tactic:
by_contra! 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.Nonloop e
hef : e ∈ M.cl {f}
h : f ∈ M.E → M.Loop f
⊢ False
Theorem: Matroid.Nonloop.nonloop_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.Nonloop e
hef : e ∈ M.cl {f}
h : f ∈ M.E → M.Loop f
⊢ False
Tactic:
apply he.not_loop
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.Nonloop e
hef : e ∈ M.cl {f}
h : f ∈ M.E → M.Loop f
⊢ M.Loop e
Theorem: Matroid.Nonloop.nonloop_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.Nonloop e
hef : e ∈ M.cl {f}
h : f ∈ M.E → M.Loop f
⊢ M.Loop e
Tactic:
rw [loop_iff_mem_cl_empty] at *
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.Nonloop e
hef : e ∈ M.cl {f}
h : f ∈ M.E → f ∈ M.cl ∅
⊢ e ∈ M.cl ∅
Theorem: Matroid.Nonloop.nonloop_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.Nonloop e
hef : e ∈ M.cl {f}
h : f ∈ M.E → f ∈ M.cl ∅
⊢ e ∈ M.cl ∅
Tactic:
convert hef using 1
Proof state after:
case h.e'_5
α : 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
hef : e ∈ M.cl {f}
h : f ∈ M.E → f ∈ M.cl ∅
⊢ M.cl ∅ = M.cl {f}
Theorem: Matroid.Nonloop.nonloop_of_mem_cl
Proof state before:
case h.e'_5
α : 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
hef : e ∈ M.cl {f}
h : f ∈ M.E → f ∈ M.cl ∅
⊢ M.cl ∅ = M.cl {f}
Tactic:
obtain (hf | hf) := em (f ∈ M.E)
Proof state after:
case h.e'_5.inl
α : 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
hef : e ∈ M.cl {f}
h : f ∈ M.E → f ∈ M.cl ∅
hf : f ∈ M.E
⊢ M.cl ∅ = M.cl {f}

case h.e'_5.inr
α : 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
hef : e ∈ M.cl {f}
h : f ∈ M.E → f ∈ M.cl ∅
hf : f ∉ M.E
⊢ M.cl ∅ = M.cl {f}
Theorem: Matroid.Nonloop.nonloop_of_mem_cl
Proof state before:
case h.e'_5.inr
α : 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
hef : e ∈ M.cl {f}
h : f ∈ M.E → f ∈ M.cl ∅
hf : f ∉ M.E
⊢ M.cl ∅ = M.cl {f}
Tactic:
rw [eq_comm, ← cl_inter_ground, inter_comm, inter_singleton_eq_empty.mpr hf]
Proof state after:
no goals
Theorem: Matroid.Nonloop.nonloop_of_mem_cl
Proof state before:
case h.e'_5.inl
α : 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
hef : e ∈ M.cl {f}
h : f ∈ M.E → f ∈ M.cl ∅
hf : f ∈ M.E
⊢ M.cl ∅ = M.cl {f}
Tactic:
rw [← cl_cl _ ∅, ← insert_eq_of_mem (h hf), cl_insert_cl_eq_cl_insert, insert_emptyc_eq]
Proof state after:
no goals
Theorem: Matroid.Nonloop.cl_eq_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.Nonloop e
hef : e ∈ M.cl {f}
⊢ M.cl {e} = M.cl {f}
Tactic:
rw [← cl_cl _ {f}, ← insert_eq_of_mem hef, cl_insert_cl_eq_cl_insert,
  ← cl_cl _ {e}, ← insert_eq_of_mem (he.mem_cl_singleton hef), cl_insert_cl_eq_cl_insert,
  pair_comm]
Proof state after:
no goals
Theorem: Matroid.Nonloop.cl_eq_cl_iff_circuit_of_ne
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
hef : e ≠ f
⊢ M.cl {e} = M.cl {f} ↔ M.Circuit {e, f}
Tactic:
refine' ⟨fun h ↦ _, fun 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 α
he : M.Nonloop e
hef : e ≠ f
h : M.cl {e} = M.cl {f}
⊢ M.Circuit {e, f}

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 α
he : M.Nonloop e
hef : e ≠ f
h : M.Circuit {e, f}
⊢ M.cl {e} = M.cl {f}
Theorem: Matroid.Nonloop.cl_eq_cl_iff_circuit_of_ne
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 α
he : M.Nonloop e
hef : e ≠ f
h : M.Circuit {e, f}
⊢ M.cl {e} = M.cl {f}
Tactic:
have hcl := (h.cl_diff_singleton_eq_cl e).trans (h.cl_diff_singleton_eq_cl f).symm
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 α
he : M.Nonloop e
hef : e ≠ f
h : M.Circuit {e, f}
hcl : M.cl ({e, f} \ {e}) = M.cl ({e, f} \ {f})
⊢ M.cl {e} = M.cl {f}
Theorem: Matroid.Nonloop.cl_eq_cl_iff_circuit_of_ne
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 α
he : M.Nonloop e
hef : e ≠ f
h : M.Circuit {e, f}
hcl : M.cl ({e, f} \ {e}) = M.cl ({e, f} \ {f})
⊢ M.cl {e} = M.cl {f}
Tactic:
rwa [pair_diff_left hef, pair_diff_right hef, eq_comm] at hcl
Proof state after:
no goals
Theorem: Matroid.Nonloop.cl_eq_cl_iff_circuit_of_ne
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 α
he : M.Nonloop e
hef : e ≠ f
h : M.cl {e} = M.cl {f}
⊢ M.Circuit {e, f}
Tactic:
have hf := he.nonloop_of_mem_cl (by rw [← h]; exact M.mem_cl_self e)
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 α
he : M.Nonloop e
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
⊢ M.Circuit {e, f}
Theorem: Matroid.Nonloop.cl_eq_cl_iff_circuit_of_ne
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 α
he : M.Nonloop e
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
⊢ M.Circuit {e, f}
Tactic:
rw [circuit_iff_dep_forall_diff_singleton_indep, dep_iff, insert_subset_iff,
  and_iff_right he.mem_ground, singleton_subset_iff, and_iff_left hf.mem_ground]
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 α
he : M.Nonloop e
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
⊢ ¬M.Indep {e, f} ∧ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})
Theorem: Matroid.Nonloop.cl_eq_cl_iff_circuit_of_ne
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 α
he : M.Nonloop e
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
⊢ ¬M.Indep {e, f} ∧ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})
Tactic:
refine' ⟨fun hi ↦ _, _⟩
Proof state after:
case refine'_1.refine'_1
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
hi : M.Indep {e, f}
⊢ False

case refine'_1.refine'_2
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
⊢ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})
Theorem: Matroid.Nonloop.cl_eq_cl_iff_circuit_of_ne
Proof state before:
case refine'_1.refine'_2
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
⊢ ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})
Tactic:
rintro x (rfl | rfl)
Proof state after:
case refine'_1.refine'_2.inl
α : Type u_1
β : Type u_2
M N : Matroid α
f : α
B L L' I X Y Z F C K : Set α
hf : M.Nonloop f
x : α
he : M.Nonloop x
hef : x ≠ f
h : M.cl {x} = M.cl {f}
⊢ M.Indep ({x, f} \ {x})

case refine'_1.refine'_2.inr
α : Type u_1
β : Type u_2
M N : Matroid α
e : α
B L L' I X Y Z F C K : Set α
he : M.Nonloop e
x : α
hef : e ≠ x
h : M.cl {e} = M.cl {x}
hf : M.Nonloop x
⊢ M.Indep ({e, x} \ {x})
Theorem: Matroid.Nonloop.cl_eq_cl_iff_circuit_of_ne
Proof state before:
case refine'_1.refine'_2.inr
α : Type u_1
β : Type u_2
M N : Matroid α
e : α
B L L' I X Y Z F C K : Set α
he : M.Nonloop e
x : α
hef : e ≠ x
h : M.cl {e} = M.cl {x}
hf : M.Nonloop x
⊢ M.Indep ({e, x} \ {x})
Tactic:
rwa [pair_diff_right hef, indep_singleton]
Proof state after:
no goals
Theorem: Matroid.Nonloop.cl_eq_cl_iff_circuit_of_ne
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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
⊢ e ∈ M.cl {?m.31393}
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 α
he : M.Nonloop e
hef : e ≠ f
h : M.cl {e} = M.cl {f}
⊢ e ∈ M.cl {e}
Theorem: Matroid.Nonloop.cl_eq_cl_iff_circuit_of_ne
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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
⊢ e ∈ M.cl {e}
Tactic:
exact M.mem_cl_self e
Proof state after:
no goals
Theorem: Matroid.Nonloop.cl_eq_cl_iff_circuit_of_ne
Proof state before:
case refine'_1.refine'_1
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
hi : M.Indep {e, f}
⊢ False
Tactic:
apply hi.not_mem_cl_diff_of_mem (mem_insert _ _)
Proof state after:
case refine'_1.refine'_1
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
hi : M.Indep {e, f}
⊢ e ∈ M.cl ({e, f} \ {e})
Theorem: Matroid.Nonloop.cl_eq_cl_iff_circuit_of_ne
Proof state before:
case refine'_1.refine'_1
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
hi : M.Indep {e, f}
⊢ e ∈ M.cl ({e, f} \ {e})
Tactic:
rw [insert_diff_of_mem _ (by exact rfl : e ∈ {e}), diff_singleton_eq_self (by simpa), ← h]
Proof state after:
case refine'_1.refine'_1
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
hi : M.Indep {e, f}
⊢ e ∈ M.cl {e}
Theorem: Matroid.Nonloop.cl_eq_cl_iff_circuit_of_ne
Proof state before:
case refine'_1.refine'_1
α : 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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
hi : M.Indep {e, f}
⊢ e ∈ M.cl {e}
Tactic:
exact mem_cl_self _ _ he.mem_ground
Proof state after:
no goals
Theorem: Matroid.Nonloop.cl_eq_cl_iff_circuit_of_ne
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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
hi : M.Indep {e, f}
⊢ e ∈ {e}
Tactic:
exact rfl
Proof state after:
no goals
Theorem: Matroid.Nonloop.cl_eq_cl_iff_circuit_of_ne
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
hef : e ≠ f
h : M.cl {e} = M.cl {f}
hf : M.Nonloop f
hi : M.Indep {e, f}
⊢ e ∉ {f}
Tactic:
simpa
Proof state after:
no goals
Theorem: Matroid.Nonloop.cl_eq_cl_iff_circuit_of_ne
Proof state before:
case refine'_1.refine'_2.inl
α : Type u_1
β : Type u_2
M N : Matroid α
f : α
B L L' I X Y Z F C K : Set α
hf : M.Nonloop f
x : α
he : M.Nonloop x
hef : x ≠ f
h : M.cl {x} = M.cl {f}
⊢ M.Indep ({x, f} \ {x})
Tactic:
rwa [pair_diff_left hef, indep_singleton]
Proof state after:
no goals
Theorem: Matroid.Nonloop.cl_eq_cl_iff_eq_or_dep
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
hf : M.Nonloop f
⊢ M.cl {e} = M.cl {f} ↔ e = f ∨ ¬M.Indep {e, f}
Tactic:
obtain (rfl | hne) := eq_or_ne e f
Proof state after:
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
e : α
B L L' I X Y Z F C K : Set α
he hf : M.Nonloop e
⊢ M.cl {e} = M.cl {e} ↔ e = e ∨ ¬M.Indep {e, e}

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 : M.Nonloop e
hf : M.Nonloop f
hne : e ≠ f
⊢ M.cl {e} = M.cl {f} ↔ e = f ∨ ¬M.Indep {e, f}
Theorem: Matroid.Nonloop.cl_eq_cl_iff_eq_or_dep
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 : M.Nonloop e
hf : M.Nonloop f
hne : e ≠ f
⊢ M.cl {e} = M.cl {f} ↔ e = f ∨ ¬M.Indep {e, f}
Tactic:
simp_rw [he.cl_eq_cl_iff_circuit_of_ne hne, or_iff_right hne,
  circuit_iff_dep_forall_diff_singleton_indep, dep_iff, insert_subset_iff, singleton_subset_iff,
  and_iff_left hf.mem_ground, and_iff_left he.mem_ground, and_iff_left_iff_imp]
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 : M.Nonloop e
hf : M.Nonloop f
hne : e ≠ f
⊢ ¬M.Indep {e, f} → ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})
Theorem: Matroid.Nonloop.cl_eq_cl_iff_eq_or_dep
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 : M.Nonloop e
hf : M.Nonloop f
hne : e ≠ f
⊢ ¬M.Indep {e, f} → ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})
Tactic:
rintro hi x (rfl | rfl)
Proof state after:
case inr.inl
α : Type u_1
β : Type u_2
M N : Matroid α
f : α
B L L' I X Y Z F C K : Set α
hf : M.Nonloop f
x : α
he : M.Nonloop x
hne : x ≠ f
hi : ¬M.Indep {x, f}
⊢ M.Indep ({x, f} \ {x})

case inr.inr
α : Type u_1
β : Type u_2
M N : Matroid α
e : α
B L L' I X Y Z F C K : Set α
he : M.Nonloop e
x : α
hf : M.Nonloop x
hne : e ≠ x
hi : ¬M.Indep {e, x}
⊢ M.Indep ({e, x} \ {x})
Theorem: Matroid.Nonloop.cl_eq_cl_iff_eq_or_dep
Proof state before:
case inr.inr
α : Type u_1
β : Type u_2
M N : Matroid α
e : α
B L L' I X Y Z F C K : Set α
he : M.Nonloop e
x : α
hf : M.Nonloop x
hne : e ≠ x
hi : ¬M.Indep {e, x}
⊢ M.Indep ({e, x} \ {x})
Tactic:
rwa [pair_diff_right hne, indep_singleton]
Proof state after:
no goals
Theorem: Matroid.Nonloop.cl_eq_cl_iff_eq_or_dep
Proof state before:
case inl
α : Type u_1
β : Type u_2
M N : Matroid α
e : α
B L L' I X Y Z F C K : Set α
he hf : M.Nonloop e
⊢ M.cl {e} = M.cl {e} ↔ e = e ∨ ¬M.Indep {e, e}
Tactic:
exact iff_of_true rfl (Or.inl rfl)
Proof state after:
no goals
Theorem: Matroid.Nonloop.cl_eq_cl_iff_eq_or_dep
Proof state before:
case inr.inl
α : Type u_1
β : Type u_2
M N : Matroid α
f : α
B L L' I X Y Z F C K : Set α
hf : M.Nonloop f
x : α
he : M.Nonloop x
hne : x ≠ f
hi : ¬M.Indep {x, f}
⊢ M.Indep ({x, f} \ {x})
Tactic:
rwa [pair_diff_left hne, indep_singleton]
Proof state after:
no goals
Theorem: Matroid.restrict_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 R : Set α
⊢ (M ↾ R).Nonloop e ↔ M.Nonloop e ∧ e ∈ R
Tactic:
rw [← indep_singleton, restrict_indep_iff, singleton_subset_iff, indep_singleton]
Proof state after:
no goals
Theorem: Matroid.Nonloop.of_restriction
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 : N.Nonloop e
hNM : N ≤r M
⊢ M.Nonloop e
Tactic:
obtain ⟨R, -, rfl⟩ := hNM
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
e f : α
B L L' I X Y Z F C K R : Set α
h : (M ↾ R).Nonloop e
⊢ M.Nonloop e
Theorem: Matroid.Nonloop.of_restriction
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
e f : α
B L L' I X Y Z F C K R : Set α
h : (M ↾ R).Nonloop e
⊢ M.Nonloop e
Tactic:
exact h.of_restrict
Proof state after:
no goals
Theorem: Matroid.comap_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 : Matroid β
f : α → β
⊢ (M.comap f).Nonloop e ↔ M.Nonloop (f e)
Tactic:
rw [← indep_singleton, comap_indep_iff, image_singleton, indep_singleton,
  and_iff_left (injOn_singleton _ _)]
Proof state after:
no goals
Theorem: Matroid.freeOn_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 E : Set α
⊢ (freeOn E).Nonloop e ↔ e ∈ E
Tactic:
rw [← indep_singleton, freeOn_indep_iff, singleton_subset_iff]
Proof state after:
no goals