-- 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_2.intro.intro.mp
α : Type u_1
inst✝ : BEq α
i acc p s x✝² x✝¹ : List α
a : α
t : List α
x✝ : Option (List α)
s' p' : List α
h : a :: t = p' ++ s'
w : (p' == i) = true
⊢ 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

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case h_2.h_2.intro.intro.mp.intro
α : Type u_1
inst✝ : BEq α
i acc x✝² x✝¹ : List α
a : α
t : List α
x✝ : Option (List α)
s' p' : List α
h : a :: t = p' ++ s'
w : (p' == i) = true
⊢ ∃ p',
    acc.reverse = 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_2.h_2.intro.intro.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : BEq α
i acc s x✝² x✝¹ : List α
a : α
t : List α
x✝ : Option (List α)
s' p' : List α
h : a :: t = p' ++ s'
w : (p' == i) = true
p'' i' : List α
h₁ : a :: t = p'' ++ (i' ++ s)
h₂ : (i' == i) = true
w' : p''.length ≤ [].length
⊢ acc.reverse = acc.reverse ++ p'' ∧ s' = s

Tactic:
simp at w'

Result:
case h_2.h_2.intro.intro.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : BEq α
i acc s x✝² x✝¹ : List α
a : α
t : List α
x✝ : Option (List α)
s' p' : List α
h : a :: t = p' ++ s'
w : (p' == i) = true
p'' i' : List α
h₁ : a :: t = p'' ++ (i' ++ s)
h₂ : (i' == i) = true
w' : p'' = []
⊢ acc.reverse = acc.reverse ++ p'' ∧ s' = s

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

Tactic:
have := dropPrefix?_append_of_beq s h₂

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

Proof state:
case h_2.h_2.intro.intro.mpr
α : Type u_1
inst✝ : BEq α
i acc p s x✝² x✝¹ : List α
a : α
t : List α
x✝ : Option (List α)
s' p' : List α
h : a :: t = p' ++ s'
w : (p' == i) = true
⊢ (∃ 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) →
    acc.reverse = p ∧ s' = s

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

Result:
case h_2.h_2.intro.intro.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : BEq α
i acc s x✝² x✝¹ : List α
a : α
t : List α
x✝ : Option (List α)
s' p' : List α
h : a :: t = p' ++ s'
w : (p' == i) = true
p'' : List α
w' : ∀ (p''_1 i'' s'' : List α), a :: t = p''_1 ++ (i'' ++ s'') → (i'' == i) = true → p''.length ≤ p''_1.length
i' : List α
h₁ : a :: t = p'' ++ (i' ++ s)
h₂ : (i' == i) = true
⊢ acc.reverse = acc.reverse ++ p'' ∧ s' = s

Proof state:
case h_2.h_2.intro.intro.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : BEq α
i acc s x✝² x✝¹ : List α
a : α
t : List α
x✝ : Option (List α)
s' p' : List α
h : a :: t = p' ++ s'
w : (p' == i) = true
p'' : List α
w' : ∀ (p''_1 i'' s'' : List α), a :: t = p''_1 ++ (i'' ++ s'') → (i'' == i) = true → p''.length ≤ p''_1.length
i' : List α
h₁ : a :: t = p'' ++ (i' ++ s)
h₂ : (i' == i) = true
⊢ acc.reverse = acc.reverse ++ p'' ∧ s' = s

Tactic:
specialize w' [] p' s' (by simpa using h) w

Result:
case h_2.h_2.intro.intro.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : BEq α
i acc s x✝² x✝¹ : List α
a : α
t : List α
x✝ : Option (List α)
s' p' : List α
h : a :: t = p' ++ s'
w : (p' == i) = true
p'' i' : List α
h₁ : a :: t = p'' ++ (i' ++ s)
h₂ : (i' == i) = true
w' : p''.length ≤ [].length
⊢ acc.reverse = acc.reverse ++ p'' ∧ s' = s

Proof state:
case h_2.h_2.intro.intro.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : BEq α
i acc s x✝² x✝¹ : List α
a : α
t : List α
x✝ : Option (List α)
s' p' : List α
h : a :: t = p' ++ s'
w : (p' == i) = true
p'' i' : List α
h₂ : (i' == i) = true
w' : p'' = []
h₁ : p' ++ s' = i' ++ s
⊢ p'.length = i'.length

Tactic:
replace w := length_eq_of_beq w

Result:
case h_2.h_2.intro.intro.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : BEq α
i acc s x✝² x✝¹ : List α
a : α
t : List α
x✝ : Option (List α)
s' p' : List α
h : a :: t = p' ++ s'
p'' i' : List α
h₂ : (i' == i) = true
w' : p'' = []
h₁ : p' ++ s' = i' ++ s
w : p'.length = i.length
⊢ p'.length = i'.length

Proof state:
α : 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' ++ i' ++ s = p'' ++ i'' ++ s''

Tactic:
simpa using h₁

Result:
no goals

Proof state:
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
w : ∀ (p'' i'' s'' : List α), p' ++ i' ++ s = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length
i'' s'' : List α
h : (i'' ++ s'').dropPrefix? i = none
h₂ : (i'' == i) = true
h₁ : i'' ++ s'' = a :: (p' ++ (i' ++ s))
⊢ p'.length + 1 ≤ [].length

Tactic:
have := dropPrefix?_append_of_beq s'' 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
w : ∀ (p'' i'' s'' : List α), p' ++ i' ++ s = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length
i'' s'' : List α
h : (i'' ++ s'').dropPrefix? i = none
h₂ : (i'' == i) = true
h₁ : i'' ++ s'' = a :: (p' ++ (i' ++ s))
this : (i'' ++ s'').dropPrefix? i = some s''
⊢ p'.length + 1 ≤ [].length