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

Tactic:
rw [w, 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
⊢ i < l₂.length

Proof state:
case mp
α✝ : 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₂[i + l₂.length - l₁.length]? = some l₁[i]

Tactic:
rw [w, getElem_reverse]

Result:
case mp
α✝ : 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
⊢ some l₁[l₁.length - 1 - (l₁.length - 1 - i)] = some l₁[i]

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
⊢ 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]

Tactic:
simp only [and_congr_right_iff]

Result:
α✝ : Type u_1
l₁ l₂ : List α✝
⊢ l₁.length ≤ l₂.length → (l₁ <:+ l₂ ↔ ∀ (i : Nat) (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
w : ∀ (i : Nat) (h : i < l₁.length), l₂.reverse[i]? = some l₁.reverse[i]
i : Nat
h : i < l₁.length
⊢ l₁.length - 1 - i < l₁.length

Tactic:
omega

Result:
no goals

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

Tactic:
constructor

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

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₂

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

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

case mpr
α✝ : Type u_1
l₁ l₂ : List α✝
le : l₁.length ≤ l₂.length
⊢ (∀ (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]

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

Tactic:
rw [p] at w

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

Tactic:
intro h

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

Proof state:
case mp
α✝ : 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
⊢ some l₁[l₁.length - 1 - (l₁.length - 1 - i)] = some l₁[i]

Tactic:
congr

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

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]
p : l₂.length - 1 - (l₁.length - 1 - i) = i + l₂.length - l₁.length
⊢ l₂[i + l₂.length - l₁.length]? = some l₁[i]

Tactic:
rw [p] at w

Result:
case mp
α✝ : 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₂[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
⊢ i < l₂.length

Tactic:
exact Nat.lt_of_lt_of_le h le

Result:
no goals

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

Tactic:
intro le

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

Proof state:
case mpr
α✝ : Type u_1
l₁ l₂ : List α✝
le : l₁.length ≤ l₂.length
⊢ (∀ (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:
intro w i h

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₂.reverse[i]? = some l₁.reverse[i]