-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Sublist.lean
theorem isInfix_iff : l₁ <:+: l₂ ↔
    ∃ k, l₁.length + k ≤ l₂.length ∧ ∀ i (h : i < l₁.length), l₂[i + k]? = some l₁[i]

Proof state:
case mp.intro.intro.intro
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
t : List α✝
s : ∀ (i : Nat) (h : i < t.length), l₂[i]? = some t[i]
p' : l₁.length ≤ t.length
p : ∀ (i : Nat) (h : i < l₁.length), t[i + t.length - l₁.length]? = some l₁[i]
⊢ ∀ (i : Nat) (h : i < l₁.length), l₂[i + (t.length - l₁.length)]? = some l₁[i]

Tactic:
intro i h

Result:
case mp.intro.intro.intro
α✝ : Type u_1
l₁ l₂ : List α✝
h✝ : l₁ <:+: l₂
t : List α✝
s : ∀ (i : Nat) (h : i < t.length), l₂[i]? = some t[i]
p' : l₁.length ≤ t.length
p : ∀ (i : Nat) (h : i < l₁.length), t[i + t.length - l₁.length]? = some l₁[i]
i : Nat
h : i < l₁.length
⊢ l₂[i + (t.length - l₁.length)]? = some l₁[i]

Proof state:
case mp.intro.intro
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
t : List α✝
p : l₁ <:+ t
s : t <+: l₂
⊢ ∃ k, l₁.length + k ≤ l₂.length ∧ ∀ (i : Nat) (h : i < l₁.length), l₂[i + k]? = some l₁[i]

Tactic:
refine ⟨t.length - l₁.length, by have := p.length_le; have := s.length_le; omega, ?_⟩

Result:
case mp.intro.intro
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
t : List α✝
p : l₁ <:+ t
s : t <+: l₂
⊢ ∀ (i : Nat) (h : i < l₁.length), l₂[i + (t.length - l₁.length)]? = some l₁[i]

Proof state:
case mpr.intro.intro.h.isFalse.e_a
α✝ : Type u_1
l₁ l₂ : List α✝
k : Nat
le : l₁.length + k ≤ l₂.length
w : ∀ (i : Nat) (h : i < l₁.length), l₂[i + k]? = some l₁[i]
i : Nat
h✝ : min k l₂.length + l₁.length ≤ i
⊢ k + l₁.length + (i - (min k l₂.length + l₁.length)) = i

Tactic:
omega

Result:
no goals

Proof state:
case mpr.intro.intro
α✝ : Type u_1
l₁ l₂ : List α✝
k : Nat
le : l₁.length + k ≤ l₂.length
w : ∀ (i : Nat) (h : i < l₁.length), l₂[i + k]? = some l₁[i]
⊢ l₁ <:+: l₂

Tactic:
refine ⟨l₂.take k, l₂.drop (k + l₁.length), ?_⟩

Result:
case mpr.intro.intro
α✝ : Type u_1
l₁ l₂ : List α✝
k : Nat
le : l₁.length + k ≤ l₂.length
w : ∀ (i : Nat) (h : i < l₁.length), l₂[i + k]? = some l₁[i]
⊢ take k l₂ ++ l₁ ++ drop (k + l₁.length) l₂ = l₂

Proof state:
case mp.intro.intro.intro
α✝ : Type u_1
l₁ l₂ : List α✝
h✝ : l₁ <:+: l₂
t : List α✝
s : ∀ (i : Nat) (h : i < t.length), l₂[i]? = some t[i]
p' : l₁.length ≤ t.length
i : Nat
h : i < l₁.length
p : t[i + (t.length - l₁.length)]? = some l₁[i]
⊢ some t[i + (t.length - l₁.length)] = some l₁[i]

Tactic:
rw [← getElem?_eq_getElem, p]

Result:
no goals

Proof state:
case mp.intro.intro.intro
α✝ : Type u_1
l₁ l₂ : List α✝
h✝ : l₁ <:+: l₂
t : List α✝
s : ∀ (i : Nat) (h : i < t.length), l₂[i]? = some t[i]
p' : l₁.length ≤ t.length
i : Nat
h : i < l₁.length
p : t[i + t.length - l₁.length]? = some l₁[i]
⊢ some t[i + (t.length - l₁.length)] = some l₁[i]

Tactic:
rw [Nat.add_sub_assoc (by omega)] at p

Result:
case mp.intro.intro.intro
α✝ : Type u_1
l₁ l₂ : List α✝
h✝ : l₁ <:+: l₂
t : List α✝
s : ∀ (i : Nat) (h : i < t.length), l₂[i]? = some t[i]
p' : l₁.length ≤ t.length
i : Nat
h : i < l₁.length
p : t[i + (t.length - l₁.length)]? = some l₁[i]
⊢ some t[i + (t.length - l₁.length)] = some l₁[i]

Proof state:
case mpr.intro.intro.h.isFalse
α✝ : Type u_1
l₁ l₂ : List α✝
k : Nat
le : l₁.length + k ≤ l₂.length
w : ∀ (i : Nat) (h : i < l₁.length), l₂[i + k]? = some l₁[i]
i : Nat
h✝ : ¬i < (take k l₂ ++ l₁).length
⊢ l₂[k + l₁.length + (i - (take k l₂ ++ l₁).length)]? = l₂[i]?

Tactic:
congr

Result:
case mpr.intro.intro.h.isFalse.e_a
α✝ : Type u_1
l₁ l₂ : List α✝
k : Nat
le : l₁.length + k ≤ l₂.length
w : ∀ (i : Nat) (h : i < l₁.length), l₂[i + k]? = some l₁[i]
i : Nat
h✝ : ¬i < (take k l₂ ++ l₁).length
⊢ k + l₁.length + (i - (take k l₂ ++ l₁).length) = i

Proof state:
case mpr.intro.intro.h.isTrue.isFalse
α✝ : Type u_1
l₁ l₂ : List α✝
k : Nat
le : l₁.length + k ≤ l₂.length
w : ∀ (i : Nat) (h : i < l₁.length), l₂[i + k]? = some l₁[i]
i : Nat
h✝¹ : i < min k l₂.length + l₁.length
h✝ : min k l₂.length ≤ i
p : i = i - k + k
⊢ some l₁[i - k + k - min k l₂.length] = some l₁[i - k]

Tactic:
congr 2

Result:
case mpr.intro.intro.h.isTrue.isFalse.e_val.e_i
α✝ : Type u_1
l₁ l₂ : List α✝
k : Nat
le : l₁.length + k ≤ l₂.length
w : ∀ (i : Nat) (h : i < l₁.length), l₂[i + k]? = some l₁[i]
i : Nat
h✝¹ : i < min k l₂.length + l₁.length
h✝ : min k l₂.length ≤ i
p : i = i - k + k
⊢ i - k + k - min k l₂.length = i - k

Proof state:
case mp.intro.intro.intro
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
t : List α✝
s : t <+: l₂
p' : l₁.length ≤ t.length
p : ∀ (i : Nat) (h : i < l₁.length), t[i + t.length - l₁.length]? = some l₁[i]
⊢ ∀ (i : Nat) (h : i < l₁.length), l₂[i + (t.length - l₁.length)]? = some l₁[i]

Tactic:
rw [isPrefix_iff] at s

Result:
case mp.intro.intro.intro
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
t : List α✝
s : ∀ (i : Nat) (h : i < t.length), l₂[i]? = some t[i]
p' : l₁.length ≤ t.length
p : ∀ (i : Nat) (h : i < l₁.length), t[i + t.length - l₁.length]? = some l₁[i]
⊢ ∀ (i : Nat) (h : i < l₁.length), l₂[i + (t.length - l₁.length)]? = some l₁[i]

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
k : Nat
le : l₁.length + k ≤ l₂.length
w : ∀ (i : Nat) (h : i < l₁.length), l₂[i + k]? = some l₁[i]
i : Nat
h✝¹ : i < min k l₂.length + l₁.length
h✝ : min k l₂.length ≤ i
p : i = i - k + k
⊢ i - k < l₁.length

Tactic:
omega

Result:
no goals

Proof state:
case mpr.intro.intro.h
α✝ : Type u_1
l₁ l₂ : List α✝
k : Nat
le : l₁.length + k ≤ l₂.length
w : ∀ (i : Nat) (h : i < l₁.length), l₂[i + k]? = some l₁[i]
i : Nat
⊢ (if i < (take k l₂ ++ l₁).length then (take k l₂ ++ l₁)[i]?
    else (drop (k + l₁.length) l₂)[i - (take k l₂ ++ l₁).length]?) =
    l₂[i]?

Tactic:
split

Result:
case mpr.intro.intro.h.isTrue
α✝ : Type u_1
l₁ l₂ : List α✝
k : Nat
le : l₁.length + k ≤ l₂.length
w : ∀ (i : Nat) (h : i < l₁.length), l₂[i + k]? = some l₁[i]
i : Nat
h✝ : i < (take k l₂ ++ l₁).length
⊢ (take k l₂ ++ l₁)[i]? = l₂[i]?

case mpr.intro.intro.h.isFalse
α✝ : Type u_1
l₁ l₂ : List α✝
k : Nat
le : l₁.length + k ≤ l₂.length
w : ∀ (i : Nat) (h : i < l₁.length), l₂[i + k]? = some l₁[i]
i : Nat
h✝ : ¬i < (take k l₂ ++ l₁).length
⊢ (drop (k + l₁.length) l₂)[i - (take k l₂ ++ l₁).length]? = l₂[i]?

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
⊢ l₁ <:+: l₂ ↔ ∃ k, l₁.length + k ≤ l₂.length ∧ ∀ (i : Nat) (h : i < l₁.length), l₂[i + k]? = some l₁[i]

Tactic:
constructor

Result:
case mp
α✝ : Type u_1
l₁ l₂ : List α✝
⊢ l₁ <:+: l₂ → ∃ k, l₁.length + k ≤ l₂.length ∧ ∀ (i : Nat) (h : i < l₁.length), l₂[i + k]? = some l₁[i]

case mpr
α✝ : Type u_1
l₁ l₂ : List α✝
⊢ (∃ k, l₁.length + k ≤ l₂.length ∧ ∀ (i : Nat) (h : i < l₁.length), l₂[i + k]? = some l₁[i]) → l₁ <:+: l₂

Proof state:
case mpr.intro.intro.h
α✝ : Type u_1
l₁ l₂ : List α✝
k : Nat
le : l₁.length + k ≤ l₂.length
w : ∀ (i : Nat) (h : i < l₁.length), l₂[i + k]? = some l₁[i]
i : Nat
⊢ (take k l₂ ++ l₁ ++ drop (k + l₁.length) l₂)[i]? = l₂[i]?

Tactic:
rw [getElem?_append]

Result:
case mpr.intro.intro.h
α✝ : Type u_1
l₁ l₂ : List α✝
k : Nat
le : l₁.length + k ≤ l₂.length
w : ∀ (i : Nat) (h : i < l₁.length), l₂[i + k]? = some l₁[i]
i : Nat
⊢ (if i < (take k l₂ ++ l₁).length then (take k l₂ ++ l₁)[i]?
    else (drop (k + l₁.length) l₂)[i - (take k l₂ ++ l₁).length]?) =
    l₂[i]?

Proof state:
case mp.intro.intro.intro
α✝ : Type u_1
l₁ l₂ : List α✝
h✝ : l₁ <:+: l₂
t : List α✝
s : ∀ (i : Nat) (h : i < t.length), l₂[i]? = some t[i]
p' : l₁.length ≤ t.length
p : ∀ (i : Nat) (h : i < l₁.length), t[i + t.length - l₁.length]? = some l₁[i]
i : Nat
h : i < l₁.length
⊢ some t[i + (t.length - l₁.length)] = some l₁[i]

Tactic:
specialize p i (by omega)

Result:
case mp.intro.intro.intro
α✝ : Type u_1
l₁ l₂ : List α✝
h✝ : l₁ <:+: l₂
t : List α✝
s : ∀ (i : Nat) (h : i < t.length), l₂[i]? = some t[i]
p' : l₁.length ≤ t.length
i : Nat
h : i < l₁.length
p : t[i + t.length - l₁.length]? = some l₁[i]
⊢ some t[i + (t.length - l₁.length)] = some l₁[i]