-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem dropSuffix?_eq_some_iff [BEq α] {l p s : List α} :
    dropSuffix? l s = some p ↔ ∃ s', l = p ++ s' ∧ s' == s

Proof state:
case mpr.intro.intro
α : Type u_1
inst✝ : BEq α
p s s' : List α
w : (s' == s) = true
⊢ (drop ((p ++ s').length - s.length) (p ++ s') == s) = true ∧ take ((p ++ s').length - s.length) (p ++ s') = p

Tactic:
simp [length_eq_of_beq w, w]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
l p s : List α
⊢ (drop (l.length - s.length) l == s) = true ∧ take (l.length - s.length) l = p ↔ ∃ s', l = p ++ s' ∧ (s' == s) = true

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝ : BEq α
l p s : List α
⊢ (drop (l.length - s.length) l == s) = true ∧ take (l.length - s.length) l = p → ∃ s', l = p ++ s' ∧ (s' == s) = true

case mpr
α : Type u_1
inst✝ : BEq α
l p s : List α
⊢ (∃ s', l = p ++ s' ∧ (s' == s) = true) → (drop (l.length - s.length) l == s) = true ∧ take (l.length - s.length) l = p

Proof state:
α : Type u_1
inst✝ : BEq α
l p s : List α
⊢ (match splitAt (l.length - s.length) l with
      | (r, s') => if (s' == s) = true then some r else none) =
      some p ↔
    ∃ s', l = p ++ s' ∧ (s' == s) = true

Tactic:
rw [splitAt_eq]

Result:
α : Type u_1
inst✝ : BEq α
l p s : List α
⊢ (match (take (l.length - s.length) l, drop (l.length - s.length) l) with
      | (r, s') => if (s' == s) = true then some r else none) =
      some p ↔
    ∃ s', l = p ++ s' ∧ (s' == s) = true

Proof state:
α : Type u_1
inst✝ : BEq α
l s : List α
w : (drop (l.length - s.length) l == s) = true
⊢ l = take (l.length - s.length) l ++ drop (l.length - s.length) l

Tactic:
simp

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝ : BEq α
l p s : List α
⊢ (drop (l.length - s.length) l == s) = true ∧ take (l.length - s.length) l = p → ∃ s', l = p ++ s' ∧ (s' == s) = true

Tactic:
rintro ⟨w, rfl⟩

Result:
case mp.intro
α : Type u_1
inst✝ : BEq α
l s : List α
w : (drop (l.length - s.length) l == s) = true
⊢ ∃ s', l = take (l.length - s.length) l ++ s' ∧ (s' == s) = true

Proof state:
case mpr
α : Type u_1
inst✝ : BEq α
l p s : List α
⊢ (∃ s', l = p ++ s' ∧ (s' == s) = true) → (drop (l.length - s.length) l == s) = true ∧ take (l.length - s.length) l = p

Tactic:
rintro ⟨s', rfl, w⟩

Result:
case mpr.intro.intro
α : Type u_1
inst✝ : BEq α
p s s' : List α
w : (s' == s) = true
⊢ (drop ((p ++ s').length - s.length) (p ++ s') == s) = true ∧ take ((p ++ s').length - s.length) (p ++ s') = p

Proof state:
α : Type u_1
inst✝ : BEq α
l p s : List α
⊢ (match (take (l.length - s.length) l, drop (l.length - s.length) l) with
      | (r, s') => if (s' == s) = true then some r else none) =
      some p ↔
    ∃ s', l = p ++ s' ∧ (s' == s) = true

Tactic:
simp only [ite_none_right_eq_some, some.injEq]

Result:
α : Type u_1
inst✝ : BEq α
l p s : List α
⊢ (drop (l.length - s.length) l == s) = true ∧ take (l.length - s.length) l = p ↔ ∃ s', l = p ++ s' ∧ (s' == s) = true

Proof state:
case mp.intro
α : Type u_1
inst✝ : BEq α
l s : List α
w : (drop (l.length - s.length) l == s) = true
⊢ ∃ s', l = take (l.length - s.length) l ++ s' ∧ (s' == s) = true

Tactic:
refine ⟨_, by simp, w⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
l p s : List α
⊢ l.dropSuffix? s = some p ↔ ∃ s', l = p ++ s' ∧ (s' == s) = true

Tactic:
unfold dropSuffix?

Result:
α : Type u_1
inst✝ : BEq α
l p s : List α
⊢ (match splitAt (l.length - s.length) l with
      | (r, s') => if (s' == s) = true then some r else none) =
      some p ↔
    ∃ s', l = p ++ s' ∧ (s' == s) = true