-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem dropInfix?_go_eq_some_iff [BEq α] {i l acc p s : List α} :
    dropInfix?.go i l acc = some (p, s) ↔ ∃ p',
      p = acc.reverse ++ p' ∧
      -- `i` is an infix up to `==`
      (∃ i', l = p' ++ i' ++ s ∧ i' == i) ∧
        -- and there is no shorter prefix for which that is the case
        (∀ p'' i'' s'', l = p'' ++ i'' ++ s'' → i'' == i → p''.length ≥ p'.length)

Proof state:
case h_2.h_1.mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : BEq α
i acc s x✝² x✝¹ : List α
a : α
x✝ : Option (List α)
p' i' : List α
h₂✝ : (i' == i) = true
h : (a :: (p' ++ i' ++ s)).dropPrefix? i = none
w : ∀ (p'' i'' s'' : List α), p' ++ i' ++ s = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length
p'' i'' s'' : List α
h₁ : p'' = [] ∧ i'' ++ s'' = a :: (p' ++ (i' ++ s)) ∨ ∃ a', p'' = a :: a' ∧ p' ++ (i' ++ s) = a' ++ (i'' ++ s'')
h₂ : (i'' == i) = true
⊢ p'.length + 1 ≤ p''.length

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

Result:
case h_2.h_1.mp.intro.intro.intro.intro.intro.inl.intro
α : Type u_1
inst✝ : BEq α
i acc s x✝² x✝¹ : List α
a : α
x✝ : Option (List α)
p' i' : List α
h₂✝ : (i' == i) = true
h : (a :: (p' ++ i' ++ s)).dropPrefix? i = none
w : ∀ (p'' i'' s'' : List α), p' ++ i' ++ s = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length
i'' s'' : List α
h₂ : (i'' == i) = true
h₁ : i'' ++ s'' = a :: (p' ++ (i' ++ s))
⊢ p'.length + 1 ≤ [].length

case h_2.h_1.mp.intro.intro.intro.intro.intro.inr.intro.intro
α : Type u_1
inst✝ : BEq α
i acc s x✝² x✝¹ : List α
a : α
x✝ : Option (List α)
p' i' : List α
h₂✝ : (i' == i) = true
h : (a :: (p' ++ i' ++ s)).dropPrefix? i = none
w : ∀ (p'' i'' s'' : List α), p' ++ i' ++ s = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length
i'' s'' : List α
h₂ : (i'' == i) = true
p'' : List α
h₁ : p' ++ (i' ++ s) = p'' ++ (i'' ++ s'')
⊢ p'.length + 1 ≤ (a :: p'').length

Proof state:
case h_2.h_1.mp
α : Type u_1
inst✝ : BEq α
i acc p s x✝² x✝¹ : List α
a : α
t : List α
x✝ : Option (List α)
h : (a :: t).dropPrefix? i = none
⊢ (∃ p',
      p = (a :: acc).reverse ++ p' ∧
        (∃ i', t = p' ++ i' ++ s ∧ (i' == i) = true) ∧
          ∀ (p'' i'' s'' : List α), t = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length) →
    ∃ p',
      p = acc.reverse ++ p' ∧
        (∃ i', a :: t = p' ++ i' ++ s ∧ (i' == i) = true) ∧
          ∀ (p'' i'' s'' : List α), a :: t = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length

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

Result:
case h_2.h_1.mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : BEq α
i acc s x✝² x✝¹ : List α
a : α
x✝ : Option (List α)
p' i' : List α
h₂ : (i' == i) = true
h : (a :: (p' ++ i' ++ s)).dropPrefix? i = none
w : ∀ (p'' i'' s'' : List α), p' ++ i' ++ s = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length
⊢ ∃ p'_1,
    (a :: acc).reverse ++ p' = acc.reverse ++ p'_1 ∧
      (∃ i'_1, a :: (p' ++ i' ++ s) = p'_1 ++ i'_1 ++ s ∧ (i'_1 == i) = true) ∧
        ∀ (p'' i'' s'' : List α),
          a :: (p' ++ i' ++ s) = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'_1.length

Proof state:
case h_2.h_2
α : Type u_1
inst✝ : BEq α
i acc p s x✝² x✝¹ : List α
a : α
t : List α
x✝ : Option (List α)
s' : List α
h : (a :: t).dropPrefix? i = some s'
⊢ some (acc.reverse, s') = some (p, s) ↔
    ∃ p',
      p = acc.reverse ++ p' ∧
        (∃ i', a :: t = p' ++ i' ++ s ∧ (i' == i) = true) ∧
          ∀ (p'' i'' s'' : List α), a :: t = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length

Tactic:
simp only [some.injEq, Prod.mk.injEq, append_assoc, ge_iff_le]

Result:
case h_2.h_2
α : Type u_1
inst✝ : BEq α
i acc p s x✝² x✝¹ : List α
a : α
t : List α
x✝ : Option (List α)
s' : List α
h : (a :: t).dropPrefix? i = some s'
⊢ acc.reverse = p ∧ s' = s ↔
    ∃ p',
      p = acc.reverse ++ p' ∧
        (∃ i', a :: t = p' ++ (i' ++ s) ∧ (i' == i) = true) ∧
          ∀ (p'' i'' s'' : List α), a :: t = p'' ++ (i'' ++ s'') → (i'' == i) = true → p'.length ≤ p''.length

Proof state:
α : Type u_1
inst✝ : BEq α
i l acc p s : List α
⊢ dropInfix?.go i l acc = some (p, s) ↔
    ∃ p',
      p = acc.reverse ++ p' ∧
        (∃ i', l = p' ++ i' ++ s ∧ (i' == i) = true) ∧
          ∀ (p'' i'' s'' : List α), l = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length

Tactic:
unfold dropInfix?.go

Result:
α : Type u_1
inst✝ : BEq α
i l acc p s : List α
⊢ (match l, acc with
      | [], acc => if i.isEmpty = true then some (acc.reverse, []) else none
      | a :: as, acc =>
        match (a :: as).dropPrefix? i with
        | none => dropInfix?.go i as (a :: acc)
        | some s => some (acc.reverse, s)) =
      some (p, s) ↔
    ∃ p',
      p = acc.reverse ++ p' ∧
        (∃ i', l = p' ++ i' ++ s ∧ (i' == i) = true) ∧
          ∀ (p'' i'' s'' : List α), l = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length

Proof state:
case h_2.h_1.mpr.intro.intro.intro.intro.intro.inl.intro.intro
α : Type u_1
inst✝ : BEq α
i acc x✝² x✝¹ : List α
a : α
t : List α
x✝ : Option (List α)
h : (a :: t).dropPrefix? i = none
w : ∀ (p'' i'' s'' : List α), a :: t = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ [].length
h₂ : i = []
⊢ ∃ p',
    acc.reverse ++ [] = (a :: acc).reverse ++ p' ∧
      (∃ i', t = p' ++ i' ++ a :: t ∧ (i' == i) = true) ∧
        ∀ (p'' i'' s'' : List α), t = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length

Tactic:
simp only [h₂] at h

Result:
case h_2.h_1.mpr.intro.intro.intro.intro.intro.inl.intro.intro
α : Type u_1
inst✝ : BEq α
i acc x✝² x✝¹ : List α
a : α
t : List α
x✝ : Option (List α)
w : ∀ (p'' i'' s'' : List α), a :: t = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ [].length
h₂ : i = []
h : (a :: t).dropPrefix? [] = none
⊢ ∃ p',
    acc.reverse ++ [] = (a :: acc).reverse ++ p' ∧
      (∃ i', t = p' ++ i' ++ a :: t ∧ (i' == i) = true) ∧
        ∀ (p'' i'' s'' : List α), t = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length

Proof state:
case h_2.h_1
α : Type u_1
inst✝ : BEq α
i acc p s x✝² x✝¹ : List α
a : α
t : List α
x✝ : Option (List α)
h : (a :: t).dropPrefix? i = none
⊢ dropInfix?.go i t (a :: acc) = some (p, s) ↔
    ∃ p',
      p = acc.reverse ++ p' ∧
        (∃ i', a :: t = p' ++ i' ++ s ∧ (i' == i) = true) ∧
          ∀ (p'' i'' s'' : List α), a :: t = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length

Tactic:
rw [dropInfix?_go_eq_some_iff]

Result:
case h_2.h_1
α : Type u_1
inst✝ : BEq α
i acc p s x✝² x✝¹ : List α
a : α
t : List α
x✝ : Option (List α)
h : (a :: t).dropPrefix? i = none
⊢ (∃ p',
      p = (a :: acc).reverse ++ p' ∧
        (∃ i', t = p' ++ i' ++ s ∧ (i' == i) = true) ∧
          ∀ (p'' i'' s'' : List α), t = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length) ↔
    ∃ p',
      p = acc.reverse ++ p' ∧
        (∃ i', a :: t = p' ++ i' ++ s ∧ (i' == i) = true) ∧
          ∀ (p'' i'' s'' : List α), a :: t = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length

Proof state:
case h_1.mpr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : BEq α
i acc x✝¹ x✝ : List α
w : ∀ (p'' i'' s'' : List α), p'' = [] → i'' = [] → s'' = [] → (i'' == i) = true → [].length ≤ p''.length
h : ([] == i) = true
⊢ i = [] ∧ acc.reverse = acc.reverse ++ [] ∧ [] = []

Tactic:
simp_all

Result:
no goals