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

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

Tactic:
rw [← reverse_prefix, reverse_concat, prefix_cons_iff]

Result:
α : Type u_1
l₁ l₂ : List α
a : α
⊢ (l₁.reverse = [] ∨ ∃ t, l₁.reverse = a :: t ∧ t <+: l₂.reverse) ↔ l₁ = [] ∨ ∃ t, l₁ = t ++ [a] ∧ t <:+ l₂

Proof state:
α : Type u_1
l₁ l₂ : List α
a : α
t : List α
w : l₁.reverse = a :: t
h : t <+: l₂.reverse
⊢ t.reverse <:+ l₂

Tactic:
simpa using h.reverse

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
a : α
t : List α
w : l₁.reverse = a :: t
h : t <+: l₂.reverse
⊢ l₁ = t.reverse ++ [a]

Tactic:
simpa using congrArg reverse w

Result:
no goals

Proof state:
case h
α : Type u_1
l₁ l₂ : List α
a : α
⊢ (∃ t, l₁.reverse = a :: t ∧ t <+: l₂.reverse) ↔ ∃ t, l₁ = t ++ [a] ∧ t <:+ l₂

Tactic:
constructor

Result:
case h.mp
α : Type u_1
l₁ l₂ : List α
a : α
⊢ (∃ t, l₁.reverse = a :: t ∧ t <+: l₂.reverse) → ∃ t, l₁ = t ++ [a] ∧ t <:+ l₂

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

Proof state:
case h.mp
α : Type u_1
l₁ l₂ : List α
a : α
⊢ (∃ t, l₁.reverse = a :: t ∧ t <+: l₂.reverse) → ∃ t, l₁ = t ++ [a] ∧ t <:+ l₂

Tactic:
rintro ⟨t, w, h⟩

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

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

Tactic:
exact ⟨t.reverse, by simpa using congrArg reverse w, by simpa using h.reverse⟩

Result:
no goals

Proof state:
α : Type u_1
l₂ : List α
a : α
t : List α
h : t <:+ l₂
⊢ t.reverse <+: l₂.reverse

Tactic:
simpa using h.reverse

Result:
no goals

Proof state:
case h.mpr.intro.intro
α : Type u_1
l₂ : List α
a : α
t : List α
h : t <:+ l₂
⊢ ∃ t_1, (t ++ [a]).reverse = a :: t_1 ∧ t_1 <+: l₂.reverse

Tactic:
exact ⟨t.reverse, by simp, by simpa using h.reverse⟩

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
a : α
⊢ (l₁ = [] ∨ ∃ t, l₁.reverse = a :: t ∧ t <+: l₂.reverse) ↔ l₁ = [] ∨ ∃ t, l₁ = t ++ [a] ∧ t <:+ l₂

Tactic:
apply or_congr_right

Result:
case h
α : Type u_1
l₁ l₂ : List α
a : α
⊢ (∃ t, l₁.reverse = a :: t ∧ t <+: l₂.reverse) ↔ ∃ t, l₁ = t ++ [a] ∧ t <:+ l₂

Proof state:
α : Type u_1
l₁ l₂ : List α
a : α
⊢ (l₁.reverse = [] ∨ ∃ t, l₁.reverse = a :: t ∧ t <+: l₂.reverse) ↔ l₁ = [] ∨ ∃ t, l₁ = t ++ [a] ∧ t <:+ l₂

Tactic:
simp only [reverse_eq_nil_iff]

Result:
α : Type u_1
l₁ l₂ : List α
a : α
⊢ (l₁ = [] ∨ ∃ t, l₁.reverse = a :: t ∧ t <+: l₂.reverse) ↔ l₁ = [] ∨ ∃ t, l₁ = t ++ [a] ∧ t <:+ l₂

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

Tactic:
rintro ⟨t, rfl, h⟩

Result:
case h.mpr.intro.intro
α : Type u_1
l₂ : List α
a : α
t : List α
h : t <:+ l₂
⊢ ∃ t_1, (t ++ [a]).reverse = a :: t_1 ∧ t_1 <+: l₂.reverse

Proof state:
α : Type u_1
l₂ : List α
a : α
t : List α
h : t <:+ l₂
⊢ (t ++ [a]).reverse = a :: t.reverse

Tactic:
simp

Result:
no goals