-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem cons_sublist_iff {a : α} {l l'} :
    a :: l <+ l' ↔ ∃ r₁ r₂, l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂

Proof state:
α : Type u_1
a : α
l : List α
a' : α
r₁ r₂ : List α
ih : a :: l <+ r₁ ++ r₂ ↔ ∃ r₁_1 r₂_1, r₁ ++ r₂ = r₁_1 ++ r₂_1 ∧ a ∈ r₁_1 ∧ l <+ r₂_1
w : a :: l <+ r₁ ++ r₂
h₁ : a ∈ r₁
h₂ : l <+ r₂
⊢ a' :: (r₁ ++ r₂) = a' :: r₁ ++ r₂

Tactic:
simp

Result:
no goals

Proof state:
case cons.mp
α : Type u_1
a : α
l : List α
a' : α
l' : List α
ih : a :: l <+ l' ↔ ∃ r₁ r₂, l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂
w : a :: l <+ a' :: l'
⊢ ∃ r₁ r₂, a' :: l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂

Tactic:
cases w with
| cons _ w =>
  obtain ⟨r₁, r₂, rfl, h₁, h₂⟩ := ih.1 w
  exact ⟨a' :: r₁, r₂, by simp, mem_cons_of_mem a' h₁, h₂⟩
| cons₂ _ w =>
  exact ⟨[a], l', by simp, mem_singleton_self _, w⟩

Result:
no goals

Proof state:
case cons
α : Type u_1
a : α
l : List α
a' : α
l' : List α
ih : a :: l <+ l' ↔ ∃ r₁ r₂, l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂
⊢ a :: l <+ a' :: l' ↔ ∃ r₁ r₂, a' :: l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂

Tactic:
constructor

Result:
case cons.mp
α : Type u_1
a : α
l : List α
a' : α
l' : List α
ih : a :: l <+ l' ↔ ∃ r₁ r₂, l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂
⊢ a :: l <+ a' :: l' → ∃ r₁ r₂, a' :: l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂

case cons.mpr
α : Type u_1
a : α
l : List α
a' : α
l' : List α
ih : a :: l <+ l' ↔ ∃ r₁ r₂, l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂
⊢ (∃ r₁ r₂, a' :: l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂) → a :: l <+ a' :: l'

Proof state:
case nil
α : Type u_1
a : α
l : List α
⊢ a :: l <+ [] ↔ ∃ r₁ r₂, [] = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂

Tactic:
simp

Result:
no goals

Proof state:
case cons.mpr.intro.intro.intro.intro
α : Type u_1
a : α
l : List α
a' : α
l' : List α
ih : a :: l <+ l' ↔ ∃ r₁ r₂, l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂
r₁ r₂ : List α
w : a' :: l' = r₁ ++ r₂
h₁ : a ∈ r₁
h₂ : l <+ r₂
⊢ a :: l <+ a' :: l'

Tactic:
rw [w, ← singleton_append]

Result:
case cons.mpr.intro.intro.intro.intro
α : Type u_1
a : α
l : List α
a' : α
l' : List α
ih : a :: l <+ l' ↔ ∃ r₁ r₂, l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂
r₁ r₂ : List α
w : a' :: l' = r₁ ++ r₂
h₁ : a ∈ r₁
h₂ : l <+ r₂
⊢ [a] ++ l <+ r₁ ++ r₂

Proof state:
α : Type u_1
a : α
l : List α
a' : α
l' : List α
ih : a :: l <+ l' ↔ ∃ r₁ r₂, l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂
r₁ r₂ : List α
w : a' :: l' = r₁ ++ r₂
h₁ : a ∈ r₁
h₂ : l <+ r₂
⊢ [a] <+ r₁

Tactic:
simpa

Result:
no goals

Proof state:
case cons.mp.cons
α : Type u_1
a : α
l : List α
a' : α
l' : List α
ih : a :: l <+ l' ↔ ∃ r₁ r₂, l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂
w : a :: l <+ l'
⊢ ∃ r₁ r₂, a' :: l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂

Tactic:
obtain ⟨r₁, r₂, rfl, h₁, h₂⟩ := ih.1 w

Result:
case cons.mp.cons.intro.intro.intro.intro
α : Type u_1
a : α
l : List α
a' : α
r₁ r₂ : List α
ih : a :: l <+ r₁ ++ r₂ ↔ ∃ r₁_1 r₂_1, r₁ ++ r₂ = r₁_1 ++ r₂_1 ∧ a ∈ r₁_1 ∧ l <+ r₂_1
w : a :: l <+ r₁ ++ r₂
h₁ : a ∈ r₁
h₂ : l <+ r₂
⊢ ∃ r₁_1 r₂_1, a' :: (r₁ ++ r₂) = r₁_1 ++ r₂_1 ∧ a ∈ r₁_1 ∧ l <+ r₂_1

Proof state:
case cons.mp.cons.intro.intro.intro.intro
α : Type u_1
a : α
l : List α
a' : α
r₁ r₂ : List α
ih : a :: l <+ r₁ ++ r₂ ↔ ∃ r₁_1 r₂_1, r₁ ++ r₂ = r₁_1 ++ r₂_1 ∧ a ∈ r₁_1 ∧ l <+ r₂_1
w : a :: l <+ r₁ ++ r₂
h₁ : a ∈ r₁
h₂ : l <+ r₂
⊢ ∃ r₁_1 r₂_1, a' :: (r₁ ++ r₂) = r₁_1 ++ r₂_1 ∧ a ∈ r₁_1 ∧ l <+ r₂_1

Tactic:
exact ⟨a' :: r₁, r₂, by simp, mem_cons_of_mem a' h₁, h₂⟩

Result:
no goals

Proof state:
case cons.mpr.intro.intro.intro.intro
α : Type u_1
a : α
l : List α
a' : α
l' : List α
ih : a :: l <+ l' ↔ ∃ r₁ r₂, l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂
r₁ r₂ : List α
w : a' :: l' = r₁ ++ r₂
h₁ : a ∈ r₁
h₂ : l <+ r₂
⊢ [a] ++ l <+ r₁ ++ r₂

Tactic:
exact Sublist.append (by simpa) h₂

Result:
no goals

Proof state:
case cons.mp
α : Type u_1
a : α
l : List α
a' : α
l' : List α
ih : a :: l <+ l' ↔ ∃ r₁ r₂, l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂
⊢ a :: l <+ a' :: l' → ∃ r₁ r₂, a' :: l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂

Tactic:
intro w

Result:
case cons.mp
α : Type u_1
a : α
l : List α
a' : α
l' : List α
ih : a :: l <+ l' ↔ ∃ r₁ r₂, l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂
w : a :: l <+ a' :: l'
⊢ ∃ r₁ r₂, a' :: l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂

Proof state:
α : Type u_1
a : α
l l' : List α
ih : a :: l <+ l' ↔ ∃ r₁ r₂, l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂
w : l <+ l'
⊢ a :: l' = [a] ++ l'

Tactic:
simp

Result:
no goals

Proof state:
case cons.mp.cons₂
α : Type u_1
a : α
l l' : List α
ih : a :: l <+ l' ↔ ∃ r₁ r₂, l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂
w : l <+ l'
⊢ ∃ r₁ r₂, a :: l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂

Tactic:
exact ⟨[a], l', by simp, mem_singleton_self _, w⟩

Result:
no goals

Proof state:
case cons.mpr
α : Type u_1
a : α
l : List α
a' : α
l' : List α
ih : a :: l <+ l' ↔ ∃ r₁ r₂, l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂
⊢ (∃ r₁ r₂, a' :: l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂) → a :: l <+ a' :: l'

Tactic:
rintro ⟨r₁, r₂, w, h₁, h₂⟩

Result:
case cons.mpr.intro.intro.intro.intro
α : Type u_1
a : α
l : List α
a' : α
l' : List α
ih : a :: l <+ l' ↔ ∃ r₁ r₂, l' = r₁ ++ r₂ ∧ a ∈ r₁ ∧ l <+ r₂
r₁ r₂ : List α
w : a' :: l' = r₁ ++ r₂
h₁ : a ∈ r₁
h₂ : l <+ r₂
⊢ a :: l <+ a' :: l'