-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem isSuffixOf?_eq_some_iff_append_eq [BEq α] [LawfulBEq α] {xs ys zs : List α} :
    xs.isSuffixOf? ys = some zs ↔ zs ++ xs = ys

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs ys zs : List α
x✝ : ∃ a, xs.reverse ++ a = ys.reverse ∧ a.reverse = zs
w✝ : List α
h : xs.reverse ++ zs.reverse = ys.reverse
heq : w✝ = zs.reverse
⊢ zs ++ xs = ys

Tactic:
rw [← reverse_inj, reverse_append, h]

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs ys zs : List α
⊢ zs ++ xs = ys → ∃ a, xs.reverse ++ a = ys.reverse ∧ a.reverse = zs

Tactic:
intro h

Result:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs ys zs : List α
h : zs ++ xs = ys
⊢ ∃ a, xs.reverse ++ a = ys.reverse ∧ a.reverse = zs

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs ys zs : List α
⊢ (∃ a, xs.reverse ++ a = ys.reverse ∧ a.reverse = zs) ↔ zs ++ xs = ys

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs ys zs : List α
⊢ (∃ a, xs.reverse ++ a = ys.reverse ∧ a.reverse = zs) → zs ++ xs = ys

case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs ys zs : List α
⊢ zs ++ xs = ys → ∃ a, xs.reverse ++ a = ys.reverse ∧ a.reverse = zs

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs ys zs : List α
x✝ : ∃ a, xs.reverse ++ a = ys.reverse ∧ a.reverse = zs
w✝ : List α
h : xs.reverse ++ w✝ = ys.reverse
heq : w✝.reverse = zs
⊢ zs ++ xs = ys

Tactic:
rw [List.reverse_eq_iff] at heq

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs ys zs : List α
x✝ : ∃ a, xs.reverse ++ a = ys.reverse ∧ a.reverse = zs
w✝ : List α
h : xs.reverse ++ w✝ = ys.reverse
heq : w✝ = zs.reverse
⊢ zs ++ xs = ys

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs ys zs : List α
⊢ xs.isSuffixOf? ys = some zs ↔ zs ++ xs = ys

Tactic:
simp only [isSuffixOf?, map_eq_some', isPrefixOf?_eq_some_iff_append_eq]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs ys zs : List α
⊢ (∃ a, xs.reverse ++ a = ys.reverse ∧ a.reverse = zs) ↔ zs ++ xs = ys

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs ys zs : List α
x✝ : ∃ a, xs.reverse ++ a = ys.reverse ∧ a.reverse = zs
w✝ : List α
h : xs.reverse ++ w✝ = ys.reverse
heq : w✝ = zs.reverse
⊢ zs ++ xs = ys

Tactic:
rw [heq] at h

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs ys zs : List α
x✝ : ∃ a, xs.reverse ++ a = ys.reverse ∧ a.reverse = zs
w✝ : List α
h : xs.reverse ++ zs.reverse = ys.reverse
heq : w✝ = zs.reverse
⊢ zs ++ xs = ys

Proof state:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs ys zs : List α
h : zs ++ xs = ys
⊢ xs.reverse ++ zs.reverse = ys.reverse ∧ zs.reverse.reverse = zs

Tactic:
simp [← h]

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs ys zs : List α
h : zs ++ xs = ys
⊢ ∃ a, xs.reverse ++ a = ys.reverse ∧ a.reverse = zs

Tactic:
exists zs.reverse

Result:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs ys zs : List α
h : zs ++ xs = ys
⊢ xs.reverse ++ zs.reverse = ys.reverse ∧ zs.reverse.reverse = zs

Proof state:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs ys zs : List α
⊢ (∃ a, xs.reverse ++ a = ys.reverse ∧ a.reverse = zs) → zs ++ xs = ys

Tactic:
intro
| ⟨_, h, heq⟩ =>
  rw [List.reverse_eq_iff] at heq
  rw [heq] at h
  rw [← reverse_inj, reverse_append, h]

Result:
no goals