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

Proof state:
case h_3.mpr.intro.intro.inr.intro.intro
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a b : α
bs a' : List α
w : (a :: a' == b :: bs) = true
⊢ (a == b) = true ∧ ∃ p', a' ++ s = p' ++ s ∧ (p' == bs) = true

Tactic:
simp only [cons_beq_cons, Bool.and_eq_true] at w

Result:
case h_3.mpr.intro.intro.inr.intro.intro
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a b : α
bs a' : List α
w : (a == b) = true ∧ (a' == bs) = true
⊢ (a == b) = true ∧ ∃ p', a' ++ s = p' ++ s ∧ (p' == bs) = true

Proof state:
α : Type u_1
inst✝ : BEq α
l p s : List α
⊢ (match l, p with
      | list, [] => some list
      | [], head :: tail => none
      | a :: as, b :: bs => if (a == b) = true then as.dropPrefix? bs else none) =
      some s ↔
    ∃ p', l = p' ++ s ∧ (p' == p) = true

Tactic:
split

Result:
case h_1
α : Type u_1
inst✝ : BEq α
l s x✝¹ x✝ : List α
⊢ some l = some s ↔ ∃ p', l = p' ++ s ∧ (p' == []) = true

case h_2
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
head✝ : α
tail✝ : List α
⊢ none = some s ↔ ∃ p', [] = p' ++ s ∧ (p' == head✝ :: tail✝) = true

case h_3
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a✝ : α
as✝ : List α
b✝ : α
bs✝ : List α
⊢ (if (a✝ == b✝) = true then as✝.dropPrefix? bs✝ else none) = some s ↔
    ∃ p', a✝ :: as✝ = p' ++ s ∧ (p' == b✝ :: bs✝) = true

Proof state:
case h_3.mp.intro.intro.intro
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a b : α
bs : List α
w : (a == b) = true
p' : List α
h : (p' == bs) = true
⊢ ∃ p'_1, a :: (p' ++ s) = p'_1 ++ s ∧ (p'_1 == b :: bs) = true

Tactic:
refine ⟨a :: p', by simp_all⟩

Result:
no goals

Proof state:
case h_3
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a : α
as : List α
b : α
bs : List α
⊢ (a == b) = true ∧ as.dropPrefix? bs = some s ↔ ∃ p', a :: as = p' ++ s ∧ (p' == b :: bs) = true

Tactic:
constructor

Result:
case h_3.mp
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a : α
as : List α
b : α
bs : List α
⊢ (a == b) = true ∧ as.dropPrefix? bs = some s → ∃ p', a :: as = p' ++ s ∧ (p' == b :: bs) = true

case h_3.mpr
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a : α
as : List α
b : α
bs : List α
⊢ (∃ p', a :: as = p' ++ s ∧ (p' == b :: bs) = true) → (a == b) = true ∧ as.dropPrefix? bs = some s

Proof state:
case h_3.mpr.intro.intro.inr.intro.intro
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a b : α
bs a' : List α
w : (a == b) = true ∧ (a' == bs) = true
⊢ (a == b) = true ∧ ∃ p', a' ++ s = p' ++ s ∧ (p' == bs) = true

Tactic:
refine ⟨w.1, a', rfl, w.2⟩

Result:
no goals

Proof state:
case h_2
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
head✝ : α
tail✝ : List α
⊢ none = some s ↔ ∃ p', [] = p' ++ s ∧ (p' == head✝ :: tail✝) = true

Tactic:
simp

Result:
no goals

Proof state:
case h_3.mp
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a : α
as : List α
b : α
bs : List α
⊢ ((a == b) = true ∧ ∃ p', as = p' ++ s ∧ (p' == bs) = true) → ∃ p', a :: as = p' ++ s ∧ (p' == b :: bs) = true

Tactic:
rintro ⟨w, p', rfl, h⟩

Result:
case h_3.mp.intro.intro.intro
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a b : α
bs : List α
w : (a == b) = true
p' : List α
h : (p' == bs) = true
⊢ ∃ p'_1, a :: (p' ++ s) = p'_1 ++ s ∧ (p'_1 == b :: bs) = true

Proof state:
case h_3.mpr.intro.intro.inl.intro
α : Type u_1
inst✝ : BEq α
x✝¹ x✝ : List α
a : α
as : List α
b : α
bs : List α
w : ([] == b :: bs) = true
⊢ (a == b) = true ∧ ∃ p', as = p' ++ a :: as ∧ (p' == bs) = true

Tactic:
simp at w

Result:
no goals

Proof state:
case h_3.mpr
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a : α
as : List α
b : α
bs : List α
⊢ (∃ p', a :: as = p' ++ s ∧ (p' == b :: bs) = true) → (a == b) = true ∧ ∃ p', as = p' ++ s ∧ (p' == bs) = true

Tactic:
rintro ⟨p, h, w⟩

Result:
case h_3.mpr.intro.intro
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a : α
as : List α
b : α
bs p : List α
h : a :: as = p ++ s
w : (p == b :: bs) = true
⊢ (a == b) = true ∧ ∃ p', as = p' ++ s ∧ (p' == bs) = true

Proof state:
case h_3
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a : α
as : List α
b : α
bs : List α
⊢ (if (a == b) = true then as.dropPrefix? bs else none) = some s ↔ ∃ p', a :: as = p' ++ s ∧ (p' == b :: bs) = true

Tactic:
simp only [ite_none_right_eq_some]

Result:
case h_3
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a : α
as : List α
b : α
bs : List α
⊢ (a == b) = true ∧ as.dropPrefix? bs = some s ↔ ∃ p', a :: as = p' ++ s ∧ (p' == b :: bs) = true

Proof state:
case h_3.mpr.intro.intro
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a : α
as : List α
b : α
bs p : List α
h : p = [] ∧ s = a :: as ∨ ∃ a', p = a :: a' ∧ as = a' ++ s
w : (p == b :: bs) = true
⊢ (a == b) = true ∧ ∃ p', as = p' ++ s ∧ (p' == bs) = true

Tactic:
obtain (⟨rfl, rfl⟩ | ⟨a', rfl, rfl⟩) := h

Result:
case h_3.mpr.intro.intro.inl.intro
α : Type u_1
inst✝ : BEq α
x✝¹ x✝ : List α
a : α
as : List α
b : α
bs : List α
w : ([] == b :: bs) = true
⊢ (a == b) = true ∧ ∃ p', as = p' ++ a :: as ∧ (p' == bs) = true

case h_3.mpr.intro.intro.inr.intro.intro
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a b : α
bs a' : List α
w : (a :: a' == b :: bs) = true
⊢ (a == b) = true ∧ ∃ p', a' ++ s = p' ++ s ∧ (p' == bs) = true

Proof state:
case h_3.mp
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a : α
as : List α
b : α
bs : List α
⊢ (a == b) = true ∧ as.dropPrefix? bs = some s → ∃ p', a :: as = p' ++ s ∧ (p' == b :: bs) = true

Tactic:
rw [dropPrefix?_eq_some_iff]

Result:
case h_3.mp
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a : α
as : List α
b : α
bs : List α
⊢ ((a == b) = true ∧ ∃ p', as = p' ++ s ∧ (p' == bs) = true) → ∃ p', a :: as = p' ++ s ∧ (p' == b :: bs) = true

Proof state:
case h_3
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a✝ : α
as✝ : List α
b✝ : α
bs✝ : List α
⊢ (if (a✝ == b✝) = true then as✝.dropPrefix? bs✝ else none) = some s ↔
    ∃ p', a✝ :: as✝ = p' ++ s ∧ (p' == b✝ :: bs✝) = true

Tactic:
rename_i a as b bs

Result:
case h_3
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a : α
as : List α
b : α
bs : List α
⊢ (if (a == b) = true then as.dropPrefix? bs else none) = some s ↔ ∃ p', a :: as = p' ++ s ∧ (p' == b :: bs) = true

Proof state:
case h_1
α : Type u_1
inst✝ : BEq α
l s x✝¹ x✝ : List α
⊢ some l = some s ↔ ∃ p', l = p' ++ s ∧ (p' == []) = true

Tactic:
simp

Result:
no goals

Proof state:
case h_3.mpr
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a : α
as : List α
b : α
bs : List α
⊢ (∃ p', a :: as = p' ++ s ∧ (p' == b :: bs) = true) → (a == b) = true ∧ as.dropPrefix? bs = some s

Tactic:
rw [dropPrefix?_eq_some_iff]

Result:
case h_3.mpr
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a : α
as : List α
b : α
bs : List α
⊢ (∃ p', a :: as = p' ++ s ∧ (p' == b :: bs) = true) → (a == b) = true ∧ ∃ p', as = p' ++ s ∧ (p' == bs) = true

Proof state:
case h_3.mpr.intro.intro
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a : α
as : List α
b : α
bs p : List α
h : a :: as = p ++ s
w : (p == b :: bs) = true
⊢ (a == b) = true ∧ ∃ p', as = p' ++ s ∧ (p' == bs) = true

Tactic:
rw [cons_eq_append_iff] at h

Result:
case h_3.mpr.intro.intro
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a : α
as : List α
b : α
bs p : List α
h : p = [] ∧ s = a :: as ∨ ∃ a', p = a :: a' ∧ as = a' ++ s
w : (p == b :: bs) = true
⊢ (a == b) = true ∧ ∃ p', as = p' ++ s ∧ (p' == bs) = true

Proof state:
α : Type u_1
inst✝ : BEq α
s x✝¹ x✝ : List α
a b : α
bs : List α
w : (a == b) = true
p' : List α
h : (p' == bs) = true
⊢ a :: (p' ++ s) = a :: p' ++ s ∧ (a :: p' == b :: bs) = true

Tactic:
simp_all

Result:
no goals

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

Tactic:
unfold dropPrefix?

Result:
α : Type u_1
inst✝ : BEq α
l p s : List α
⊢ (match l, p with
      | list, [] => some list
      | [], head :: tail => none
      | a :: as, b :: bs => if (a == b) = true then as.dropPrefix? bs else none) =
      some s ↔
    ∃ p', l = p' ++ s ∧ (p' == p) = true