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

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

Tactic:
rw [← reverse_prefix, isPrefix_iff]

Result:
α✝ : Type u_1
l₁ l₂ : List α✝
le : l₁.length ≤ l₂.length
⊢ (∀ (i : Nat) (h : i < l₁.reverse.length), l₂.reverse[i]? = some l₁.reverse[i]) ↔
    ∀ (i : Nat) (h : i < l₁.length), l₂[i + l₂.length - l₁.length]? = some l₁[i]

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

Tactic:
exact (this.mpr h).2

Result:
no goals

Proof state:
case mp
α✝ : Type u_1
l₁ l₂ : List α✝
le : l₁.length ≤ l₂.length
i : Nat
h : i < l₁.length
w : l₂.reverse[l₁.length - 1 - i]? = some l₁.reverse[l₁.length - 1 - i]
⊢ l₂[i + l₂.length - l₁.length]? = some l₁[i]

Tactic:
rw [getElem?_reverse (by omega)] at w

Result:
case mp
α✝ : Type u_1
l₁ l₂ : List α✝
le : l₁.length ≤ l₂.length
i : Nat
h : i < l₁.length
w : l₂[l₂.length - 1 - (l₁.length - 1 - i)]? = some l₁.reverse[l₁.length - 1 - i]
⊢ l₂[i + l₂.length - l₁.length]? = some l₁[i]

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

Tactic:
specialize w (l₁.length - 1 - i) (by omega)

Result:
case mp
α✝ : Type u_1
l₁ l₂ : List α✝
le : l₁.length ≤ l₂.length
i : Nat
h : i < l₁.length
w : l₂.reverse[l₁.length - 1 - i]? = some l₁.reverse[l₁.length - 1 - i]
⊢ l₂[i + l₂.length - l₁.length]? = some l₁[i]

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

Tactic:
rw [getElem?_reverse]

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

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

Proof state:
case mpr
α✝ : Type u_1
l₁ l₂ : List α✝
le : l₁.length ≤ l₂.length
i : Nat
h : i < l₁.length
w : l₂[l₁.length - 1 - i + l₂.length - l₁.length]? = some l₁[l₁.length - 1 - i]
⊢ l₂[l₂.length - 1 - i]? = some l₁.reverse[i]

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

Tactic:
have p : l₁.length - 1 - i + l₂.length - l₁.length = l₂.length - 1 - i := by omega

Result:
case mpr
α✝ : Type u_1
l₁ l₂ : List α✝
le : l₁.length ≤ l₂.length
i : Nat
h : i < l₁.length
w : l₂[l₁.length - 1 - i + l₂.length - l₁.length]? = some l₁[l₁.length - 1 - i]
p : l₁.length - 1 - i + l₂.length - l₁.length = l₂.length - 1 - i
⊢ l₂[l₂.length - 1 - i]? = some l₁.reverse[i]

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

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
le : l₁.length ≤ l₂.length
i : Nat
h : i < l₁.length
w : l₂.reverse[l₁.length - 1 - i]? = some l₁.reverse[l₁.length - 1 - i]
⊢ l₁.length - 1 - i < l₂.length

Tactic:
omega

Result:
no goals

Proof state:
case mp.e_val.e_i
α✝ : Type u_1
l₁ l₂ : List α✝
le : l₁.length ≤ l₂.length
i : Nat
h : i < l₁.length
w : l₂[i + l₂.length - l₁.length]? = some l₁.reverse[l₁.length - 1 - i]
p : l₂.length - 1 - (l₁.length - 1 - i) = i + l₂.length - l₁.length
⊢ l₁.length - 1 - (l₁.length - 1 - i) = i

Tactic:
omega

Result:
no goals

Proof state:
case mp
α✝ : Type u_1
l₁ l₂ : List α✝
le : l₁.length ≤ l₂.length
i : Nat
h : i < l₁.length
w : l₂[l₂.length - 1 - (l₁.length - 1 - i)]? = some l₁.reverse[l₁.length - 1 - i]
⊢ l₂[i + l₂.length - l₁.length]? = some l₁[i]

Tactic:
have p : l₂.length - 1 - (l₁.length - 1 - i) = i + l₂.length - l₁.length := by omega

Result:
case mp
α✝ : Type u_1
l₁ l₂ : List α✝
le : l₁.length ≤ l₂.length
i : Nat
h : i < l₁.length
w : l₂[l₂.length - 1 - (l₁.length - 1 - i)]? = some l₁.reverse[l₁.length - 1 - i]
p : l₂.length - 1 - (l₁.length - 1 - i) = i + l₂.length - l₁.length
⊢ l₂[i + l₂.length - l₁.length]? = some l₁[i]

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
le : l₁.length ≤ l₂.length
i : Nat
h : i < l₁.length
w : l₂[l₁.length - 1 - i + l₂.length - l₁.length]? = some l₁[l₁.length - 1 - i]
⊢ l₁.length - 1 - i + l₂.length - l₁.length = l₂.length - 1 - i

Tactic:
omega

Result:
no goals

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

Tactic:
simp only [length_reverse]

Result:
α✝ : Type u_1
l₁ l₂ : List α✝
le : l₁.length ≤ l₂.length
⊢ (∀ (i : Nat) (h : i < l₁.length), l₂.reverse[i]? = some l₁.reverse[i]) ↔
    ∀ (i : Nat) (h : i < l₁.length), l₂[i + l₂.length - l₁.length]? = some l₁[i]

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

Tactic:
intro h

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

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

Tactic:
intro w i h

Result:
case mp
α✝ : Type u_1
l₁ l₂ : List α✝
le : l₁.length ≤ l₂.length
w : ∀ (i : Nat) (h : i < l₁.length), l₂.reverse[i]? = some l₁.reverse[i]
i : Nat
h : i < l₁.length
⊢ l₂[i + l₂.length - l₁.length]? = some l₁[i]

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

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

Tactic:
specialize w (l₁.length - 1 - i) (by omega)

Result:
case mpr
α✝ : Type u_1
l₁ l₂ : List α✝
le : l₁.length ≤ l₂.length
i : Nat
h : i < l₁.length
w : l₂[l₁.length - 1 - i + l₂.length - l₁.length]? = some l₁[l₁.length - 1 - i]
⊢ l₂[l₂.length - 1 - i]? = some l₁.reverse[i]

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

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
le : l₁.length ≤ l₂.length
i : Nat
h : i < l₁.length
w : l₂[l₂.length - 1 - (l₁.length - 1 - i)]? = some l₁.reverse[l₁.length - 1 - i]
⊢ l₂.length - 1 - (l₁.length - 1 - i) = i + l₂.length - l₁.length

Tactic:
omega

Result:
no goals