-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem prefix_cons_iff : l₁ <+: a :: l₂ ↔ l₁ = [] ∨ ∃ t, l₁ = a :: t ∧ t <+: l₂

Proof state:
α✝ : Type u_1
a : α✝
l₂ : List α✝
a' : α✝
l₁ t : List α✝
w : a' :: l₁ = a :: t
s : List α✝
h' : t ++ s = l₂
⊢ a :: t ++ s = a :: l₂

Tactic:
simp [h']

Result:
no goals

Proof state:
case cons
α✝ : Type u_1
a : α✝
l₂ : List α✝
a' : α✝
l₁ : List α✝
⊢ a' :: l₁ <+: a :: l₂ ↔ a' :: l₁ = [] ∨ ∃ t, a' :: l₁ = a :: t ∧ t <+: l₂

Tactic:
constructor

Result:
case cons.mp
α✝ : Type u_1
a : α✝
l₂ : List α✝
a' : α✝
l₁ : List α✝
⊢ a' :: l₁ <+: a :: l₂ → a' :: l₁ = [] ∨ ∃ t, a' :: l₁ = a :: t ∧ t <+: l₂

case cons.mpr
α✝ : Type u_1
a : α✝
l₂ : List α✝
a' : α✝
l₁ : List α✝
⊢ (a' :: l₁ = [] ∨ ∃ t, a' :: l₁ = a :: t ∧ t <+: l₂) → a' :: l₁ <+: a :: l₂

Proof state:
case cons.mpr.inr.intro.intro.intro
α✝ : Type u_1
a : α✝
l₂ : List α✝
a' : α✝
l₁ t : List α✝
w : a' :: l₁ = a :: t
s : List α✝
h' : t ++ s = l₂
⊢ a :: t <+: a :: l₂

Tactic:
refine ⟨s, by simp [h']⟩

Result:
no goals

Proof state:
case cons.mp.intro
α✝ : Type u_1
a : α✝
l₂ : List α✝
a' : α✝
l₁ t : List α✝
h : a' :: l₁ ++ t = a :: l₂
⊢ a' :: l₁ = [] ∨ ∃ t, a' :: l₁ = a :: t ∧ t <+: l₂

Tactic:
simp at h

Result:
case cons.mp.intro
α✝ : Type u_1
a : α✝
l₂ : List α✝
a' : α✝
l₁ t : List α✝
h : a' = a ∧ l₁ ++ t = l₂
⊢ a' :: l₁ = [] ∨ ∃ t, a' :: l₁ = a :: t ∧ t <+: l₂

Proof state:
case cons.mpr
α✝ : Type u_1
a : α✝
l₂ : List α✝
a' : α✝
l₁ : List α✝
⊢ (a' :: l₁ = [] ∨ ∃ t, a' :: l₁ = a :: t ∧ t <+: l₂) → a' :: l₁ <+: a :: l₂

Tactic:
rintro (h | ⟨t, w, ⟨s, h'⟩⟩)

Result:
case cons.mpr.inl
α✝ : Type u_1
a : α✝
l₂ : List α✝
a' : α✝
l₁ : List α✝
h : a' :: l₁ = []
⊢ a' :: l₁ <+: a :: l₂

case cons.mpr.inr.intro.intro.intro
α✝ : Type u_1
a : α✝
l₂ : List α✝
a' : α✝
l₁ t : List α✝
w : a' :: l₁ = a :: t
s : List α✝
h' : t ++ s = l₂
⊢ a' :: l₁ <+: a :: l₂

Proof state:
case cons.mpr.inl
α✝ : Type u_1
a : α✝
l₂ : List α✝
a' : α✝
l₁ : List α✝
h : a' :: l₁ = []
⊢ a' :: l₁ <+: a :: l₂

Tactic:
simp [h]

Result:
no goals

Proof state:
case cons.mp
α✝ : Type u_1
a : α✝
l₂ : List α✝
a' : α✝
l₁ : List α✝
⊢ a' :: l₁ <+: a :: l₂ → a' :: l₁ = [] ∨ ∃ t, a' :: l₁ = a :: t ∧ t <+: l₂

Tactic:
rintro ⟨t, h⟩

Result:
case cons.mp.intro
α✝ : Type u_1
a : α✝
l₂ : List α✝
a' : α✝
l₁ t : List α✝
h : a' :: l₁ ++ t = a :: l₂
⊢ a' :: l₁ = [] ∨ ∃ t, a' :: l₁ = a :: t ∧ t <+: l₂

Proof state:
case cons.mp.intro
α✝ : Type u_1
a : α✝
l₂ : List α✝
a' : α✝
l₁ t : List α✝
h : a' = a ∧ l₁ ++ t = l₂
⊢ a' :: l₁ = [] ∨ ∃ t, a' :: l₁ = a :: t ∧ t <+: l₂

Tactic:
obtain ⟨rfl, rfl⟩ := h

Result:
case cons.mp.intro.intro
α✝ : Type u_1
a' : α✝
l₁ t : List α✝
⊢ a' :: l₁ = [] ∨ ∃ t_1, a' :: l₁ = a' :: t_1 ∧ t_1 <+: l₁ ++ t

Proof state:
case cons.mp.intro.intro
α✝ : Type u_1
a' : α✝
l₁ t : List α✝
⊢ a' :: l₁ = [] ∨ ∃ t_1, a' :: l₁ = a' :: t_1 ∧ t_1 <+: l₁ ++ t

Tactic:
exact Or.inr ⟨l₁, rfl, prefix_append l₁ t⟩

Result:
no goals

Proof state:
case cons.mpr.inr.intro.intro.intro
α✝ : Type u_1
a : α✝
l₂ : List α✝
a' : α✝
l₁ t : List α✝
w : a' :: l₁ = a :: t
s : List α✝
h' : t ++ s = l₂
⊢ a' :: l₁ <+: a :: l₂

Tactic:
simp only [w]

Result:
case cons.mpr.inr.intro.intro.intro
α✝ : Type u_1
a : α✝
l₂ : List α✝
a' : α✝
l₁ t : List α✝
w : a' :: l₁ = a :: t
s : List α✝
h' : t ++ s = l₂
⊢ a :: t <+: a :: l₂

Proof state:
case nil
α✝ : Type u_1
a : α✝
l₂ : List α✝
⊢ [] <+: a :: l₂ ↔ [] = [] ∨ ∃ t, [] = a :: t ∧ t <+: l₂

Tactic:
simp

Result:
no goals