Theorem: Matroid.singleton_circuit (Matroid/Loop.lean)

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.Circuit {e} ↔ M.Loop e
Tactic:
simp_rw [← singleton_dep, circuit_def, mem_minimals_setOf_iff, and_iff_left_iff_imp,
  subset_singleton_iff_eq]
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.Dep {e} → ∀ ⦃y : Set α⦄, M.Dep y → y = ∅ ∨ y = {e} → {e} = y

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.Dep {e} → ∀ ⦃y : Set α⦄, M.Dep y → y = ∅ ∨ y = {e} → {e} = y
Tactic:
rintro _ _ hY (rfl | rfl)
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 α
a✝ : M.Dep {e}
hY : M.Dep ∅
⊢ {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 α
a✝ hY : M.Dep {e}
⊢ {e} = {e}

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 α
a✝ hY : M.Dep {e}
⊢ {e} = {e}
Tactic:
rfl
State after:
no goals

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 α
a✝ : M.Dep {e}
hY : M.Dep ∅
⊢ {e} = ∅
Tactic:
simpa using hY.nonempty
State after:
no goals