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

Tactic:
intro h

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

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

Tactic:
simp_all

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

Tactic:
simp_all

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

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

Tactic:
obtain ⟨p', p⟩ := p

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

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

Tactic:
rw [p, w _ (by omega), getElem?_eq_getElem]

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

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
⊢ i - k + k - min k l₂.length < l₁.length

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 < 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
⊢ (if i < k then l₂[i]? else none) = l₂[i]?

Tactic:
simp_all

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 < min k l₂.length + l₁.length
h✝ : i < min k l₂.length
⊢ k ≤ i → 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
⊢ i - k + k - min k l₂.length < l₁.length

Tactic:
omega

Result:
no goals

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

Tactic:
have := s.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
this : t.length ≤ l₂.length
⊢ l₁.length + (t.length - l₁.length) ≤ l₂.length

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

Tactic:
rintro ⟨k, le, w⟩

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]
⊢ l₁ <:+: l₂