case nil
ι : Type ?u.1166
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
h✝ : a ∈ l
h : a ∈ []
⊢ ∃ s t, [] = s ++ a :: t

case cons
ι : Type ?u.1166
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l✝ : List α
h✝ : a ∈ l✝
b : α
l : List α
ih : a ∈ l → ∃ s t, l = s ++ a :: t
h : a ∈ b :: l
⊢ ∃ s t, b :: l = s ++ a :: t
ι : Type ?u.1166
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
h : a ∈ l
⊢ ∃ s t, l = s ++ a :: t
induction' l with b l ih
case cons
ι : Type ?u.1166
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l✝ : List α
h✝ : a ∈ l✝
b : α
l : List α
ih : a ∈ l → ∃ s t, l = s ++ a :: t
h : a ∈ b :: l
⊢ ∃ s t, b :: l = s ++ a :: t
case nil
ι : Type ?u.1166
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
h✝ : a ∈ l
h : a ∈ []
⊢ ∃ s t, [] = s ++ a :: t

case cons
ι : Type ?u.1166
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l✝ : List α
h✝ : a ∈ l✝
b : α
l : List α
ih : a ∈ l → ∃ s t, l = s ++ a :: t
h : a ∈ b :: l
⊢ ∃ s t, b :: l = s ++ a :: t
{cases h}
case cons.head
ι : Type ?u.1166
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l✝ : List α
h : a ∈ l✝
l : List α
ih : a ∈ l → ∃ s t, l = s ++ a :: t
⊢ ∃ s t, a :: l = s ++ a :: t

case cons.tail
ι : Type ?u.1166
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l✝ : List α
h✝ : a ∈ l✝
b : α
l : List α
ih : a ∈ l → ∃ s t, l = s ++ a :: t
h : Mem a l
⊢ ∃ s t, b :: l = s ++ a :: t
case cons
ι : Type ?u.1166
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l✝ : List α
h✝ : a ∈ l✝
b : α
l : List α
ih : a ∈ l → ∃ s t, l = s ++ a :: t
h : a ∈ b :: l
⊢ ∃ s t, b :: l = s ++ a :: t
rcases h with (_ | ⟨_, h⟩)
no goals
case cons.head
ι : Type ?u.1166
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l✝ : List α
h : a ∈ l✝
l : List α
ih : a ∈ l → ∃ s t, l = s ++ a :: t
⊢ ∃ s t, a :: l = s ++ a :: t
exact ⟨[], l, rfl⟩
case cons.tail.intro.intro
ι : Type ?u.1166
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
h✝ : a ∈ l
b : α
s t : List α
ih : a ∈ s ++ a :: t → ∃ s_1 t_1, s ++ a :: t = s_1 ++ a :: t_1
h : Mem a (s ++ a :: t)
⊢ ∃ s_1 t_1, b :: (s ++ a :: t) = s_1 ++ a :: t_1
case cons.tail
ι : Type ?u.1166
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l✝ : List α
h✝ : a ∈ l✝
b : α
l : List α
ih : a ∈ l → ∃ s t, l = s ++ a :: t
h : Mem a l
⊢ ∃ s t, b :: l = s ++ a :: t
rcases ih h with ⟨s, t, rfl⟩
no goals
case cons.tail.intro.intro
ι : Type ?u.1166
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
l : List α
h✝ : a ∈ l
b : α
s t : List α
ih : a ∈ s ++ a :: t → ∃ s_1 t_1, s ++ a :: t = s_1 ++ a :: t_1
h : Mem a (s ++ a :: t)
⊢ ∃ s_1 t_1, b :: (s ++ a :: t) = s_1 ++ a :: t_1
exact ⟨b :: s, t, rfl⟩