-- 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
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
⊢ ∃ k, l₁.length + k ≤ l₂.length ∧ ∀ (i : Nat) (h : i < l₁.length), l₂[i + k]? = some l₁[i]

Tactic:
obtain ⟨t, p, s⟩ := infix_iff_suffix_prefix.mp h

Result:
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]

Proof state:
α✝ : 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
⊢ i + (t.length - l₁.length) < t.length

Tactic:
omega

Result:
no goals

Proof state:
case mpr.intro.intro.h.isTrue.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 < min k l₂.length + l₁.length
h✝ : i < min k l₂.length
⊢ k ≤ i → l₂.length ≤ i

Tactic:
omega

Result:
no goals

Proof state:
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]?

Tactic:
rw [getElem?_append]

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
⊢ (if i < (take k l₂).length then (take k l₂)[i]? else l₁[i - (take k l₂).length]?) = 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
⊢ i = i - k + k

Tactic:
omega

Result:
no goals

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
t : List α✝
p : l₁ <:+ t
s : t <+: l₂
⊢ l₁.length + (t.length - l₁.length) ≤ l₂.length

Tactic:
have := p.length_le

Result:
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
t : List α✝
p : l₁ <:+ t
s : t <+: l₂
this : l₁.length ≤ t.length
⊢ l₁.length + (t.length - l₁.length) ≤ l₂.length

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:
rw [s _ (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
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]

Proof state:
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

Tactic:
omega

Result:
no goals

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
⊢ l₁[i - min k l₂.length]? = l₂[i]?

Tactic:
have p : i = (i - k) + k := by omega

Result:
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
⊢ l₁[i - min k l₂.length]? = l₂[i]?

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
t : List α✝
p : l₁ <:+ t
s : t <+: l₂
this✝ : l₁.length ≤ t.length
this : t.length ≤ l₂.length
⊢ l₁.length + (t.length - l₁.length) ≤ l₂.length

Tactic:
omega

Result:
no goals

Proof state:
case mpr.intro.intro.h.isTrue.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
h✝ : i < (take k l₂).length
⊢ (take k l₂)[i]? = l₂[i]?

Tactic:
rw [getElem?_take]

Result:
case mpr.intro.intro.h.isTrue.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
h✝ : i < (take k l₂).length
⊢ (if i < k then l₂[i]? else none) = 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₂
⊢ ∀ (i : Nat) (h : i < l₁.length), l₂[i + (t.length - l₁.length)]? = some l₁[i]

Tactic:
rw [isSuffix_iff] at p

Result:
case mp.intro.intro
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
t : List α✝
p : l₁.length ≤ t.length ∧ ∀ (i : Nat) (h : i < l₁.length), t[i + t.length - l₁.length]? = some l₁[i]
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
α✝ : 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]?

Tactic:
rw [getElem?_drop]

Result:
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]?

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]
⊢ take k l₂ ++ l₁ ++ drop (k + l₁.length) l₂ = l₂

Tactic:
ext1 i

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
⊢ (take k l₂ ++ l₁ ++ drop (k + l₁.length) l₂)[i]? = l₂[i]?

Proof state:
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
⊢ (if i < (take k l₂).length then (take k l₂)[i]? else l₁[i - (take k l₂).length]?) = l₂[i]?

Tactic:
split

Result:
case mpr.intro.intro.h.isTrue.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
h✝ : i < (take k l₂).length
⊢ (take k l₂)[i]? = l₂[i]?

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 < (take k l₂ ++ l₁).length
h✝ : ¬i < (take k l₂).length
⊢ l₁[i - (take k l₂).length]? = l₂[i]?

Proof state:
α✝ : 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]
⊢ l₁.length ≤ t.length

Tactic:
omega

Result:
no goals