Theorem: List.singleton_isInfix_iff_mem (One.lean)

State before:
α✝ : Type u_1
e : α✝
l : List α✝
⊢ [e] <:+: l ↔ e ∈ l
Tactic:
apply Iff.intro
State after:
case mp
α✝ : Type u_1
e : α✝
l : List α✝
⊢ [e] <:+: l → e ∈ l

case mpr
α✝ : Type u_1
e : α✝
l : List α✝
⊢ e ∈ l → [e] <:+: l

State before:
case mp
α✝ : Type u_1
e : α✝
l : List α✝
⊢ [e] <:+: l → e ∈ l

case mpr
α✝ : Type u_1
e : α✝
l : List α✝
⊢ e ∈ l → [e] <:+: l
Tactic:
. intro ⟨s,t,h⟩
  simp only [append_assoc, singleton_append, mem_append, find?, mem_cons, true_or, or_true, ← h]
State after:
case mpr
α✝ : Type u_1
e : α✝
l : List α✝
⊢ e ∈ l → [e] <:+: l

State before:
case mpr
α✝ : Type u_1
e : α✝
l : List α✝
⊢ e ∈ l → [e] <:+: l
Tactic:
. intro mem
  have ⟨s,t,h⟩ := List.mem_split mem
  exists s,t
  rw [h, append_assoc, singleton_append]
State after:
no goals