-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem zipIdx_eq_cons_iff {l : List α} {k : Nat} :
    zipIdx l k = x :: l' ↔ ∃ a as, l = a :: as ∧ x = (a, k) ∧ l' = zipIdx as (k + 1)

Proof state:
α : Type u_1
x : α × Nat
l₁ : List α
⊢ x.fst :: l₁ = x.fst :: l₁ ∧
    x = (x.fst, x.snd) ∧ l₁.zip (range' (x.snd + 1) ((x.fst :: l₁).length - 1)) = l₁.zipIdx (x.snd + 1)

Tactic:
simp [zipIdx_eq_zip_range']

Result:
no goals

Proof state:
α : Type u_1
x : α × Nat
l' : List (α × Nat)
l : List α
k : Nat
⊢ (∃ l₁' l₂', l = x.fst :: l₁' ∧ range' k l.length = x.snd :: l₂' ∧ l' = l₁'.zip l₂') ↔
    ∃ a as, l = a :: as ∧ x = (a, k) ∧ l' = as.zipIdx (k + 1)

Tactic:
constructor

Result:
case mp
α : Type u_1
x : α × Nat
l' : List (α × Nat)
l : List α
k : Nat
⊢ (∃ l₁' l₂', l = x.fst :: l₁' ∧ range' k l.length = x.snd :: l₂' ∧ l' = l₁'.zip l₂') →
    ∃ a as, l = a :: as ∧ x = (a, k) ∧ l' = as.zipIdx (k + 1)

case mpr
α : Type u_1
x : α × Nat
l' : List (α × Nat)
l : List α
k : Nat
⊢ (∃ a as, l = a :: as ∧ x = (a, k) ∧ l' = as.zipIdx (k + 1)) →
    ∃ l₁' l₂', l = x.fst :: l₁' ∧ range' k l.length = x.snd :: l₂' ∧ l' = l₁'.zip l₂'

Proof state:
case mp
α : Type u_1
x : α × Nat
l' : List (α × Nat)
l : List α
k : Nat
⊢ (∃ l₁' l₂', l = x.fst :: l₁' ∧ range' k l.length = x.snd :: l₂' ∧ l' = l₁'.zip l₂') →
    ∃ a as, l = a :: as ∧ x = (a, k) ∧ l' = as.zipIdx (k + 1)

Tactic:
rintro ⟨l₁, l₂, rfl, h, rfl⟩

Result:
case mp.intro.intro.intro.intro
α : Type u_1
x : α × Nat
k : Nat
l₁ : List α
l₂ : List Nat
h : range' k (x.fst :: l₁).length = x.snd :: l₂
⊢ ∃ a as, x.fst :: l₁ = a :: as ∧ x = (a, k) ∧ l₁.zip l₂ = as.zipIdx (k + 1)

Proof state:
case mp.intro.intro.intro.intro.intro.intro
α : Type u_1
x : α × Nat
l₁ : List α
⊢ ∃ a as,
    x.fst :: l₁ = a :: as ∧
      x = (a, x.snd) ∧ l₁.zip (range' (x.snd + 1) ((x.fst :: l₁).length - 1)) = as.zipIdx (x.snd + 1)

Tactic:
exact ⟨x.1, l₁, by simp [zipIdx_eq_zip_range']⟩

Result:
no goals

Proof state:
case mpr
α : Type u_1
x : α × Nat
l' : List (α × Nat)
l : List α
k : Nat
⊢ (∃ a as, l = a :: as ∧ x = (a, k) ∧ l' = as.zipIdx (k + 1)) →
    ∃ l₁' l₂', l = x.fst :: l₁' ∧ range' k l.length = x.snd :: l₂' ∧ l' = l₁'.zip l₂'

Tactic:
rintro ⟨a, as, rfl, rfl, rfl⟩

Result:
case mpr.intro.intro.intro.intro
α : Type u_1
k : Nat
a : α
as : List α
⊢ ∃ l₁' l₂',
    a :: as = (a, k).fst :: l₁' ∧ range' k (a :: as).length = (a, k).snd :: l₂' ∧ as.zipIdx (k + 1) = l₁'.zip l₂'

Proof state:
case mp.intro.intro.intro.intro
α : Type u_1
x : α × Nat
k : Nat
l₁ : List α
l₂ : List Nat
h : range' k (x.fst :: l₁).length = x.snd :: l₂
⊢ ∃ a as, x.fst :: l₁ = a :: as ∧ x = (a, k) ∧ l₁.zip l₂ = as.zipIdx (k + 1)

Tactic:
rw [range'_eq_cons_iff] at h

Result:
case mp.intro.intro.intro.intro
α : Type u_1
x : α × Nat
k : Nat
l₁ : List α
l₂ : List Nat
h : k = x.snd ∧ 0 < (x.fst :: l₁).length ∧ l₂ = range' (x.snd + 1) ((x.fst :: l₁).length - 1)
⊢ ∃ a as, x.fst :: l₁ = a :: as ∧ x = (a, k) ∧ l₁.zip l₂ = as.zipIdx (k + 1)

Proof state:
case mp.intro.intro.intro.intro
α : Type u_1
x : α × Nat
k : Nat
l₁ : List α
l₂ : List Nat
h : k = x.snd ∧ 0 < (x.fst :: l₁).length ∧ l₂ = range' (x.snd + 1) ((x.fst :: l₁).length - 1)
⊢ ∃ a as, x.fst :: l₁ = a :: as ∧ x = (a, k) ∧ l₁.zip l₂ = as.zipIdx (k + 1)

Tactic:
obtain ⟨rfl, -, rfl⟩ := h

Result:
case mp.intro.intro.intro.intro.intro.intro
α : Type u_1
x : α × Nat
l₁ : List α
⊢ ∃ a as,
    x.fst :: l₁ = a :: as ∧
      x = (a, x.snd) ∧ l₁.zip (range' (x.snd + 1) ((x.fst :: l₁).length - 1)) = as.zipIdx (x.snd + 1)

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_1
k : Nat
a : α
as : List α
⊢ a :: as = (a, k).fst :: as ∧
    range' k (a :: as).length = (a, k).snd :: range' (k + 1) as.length ∧
      as.zipIdx (k + 1) = as.zip (range' (k + 1) as.length)

Tactic:
simp [zipIdx_eq_zip_range', range'_succ]

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_1
k : Nat
a : α
as : List α
⊢ ∃ l₁' l₂',
    a :: as = (a, k).fst :: l₁' ∧ range' k (a :: as).length = (a, k).snd :: l₂' ∧ as.zipIdx (k + 1) = l₁'.zip l₂'

Tactic:
refine ⟨as, range' (k+1) as.length, ?_⟩

Result:
case mpr.intro.intro.intro.intro
α : Type u_1
k : Nat
a : α
as : List α
⊢ a :: as = (a, k).fst :: as ∧
    range' k (a :: as).length = (a, k).snd :: range' (k + 1) as.length ∧
      as.zipIdx (k + 1) = as.zip (range' (k + 1) as.length)

Proof state:
α : Type u_1
x : α × Nat
l' : List (α × Nat)
l : List α
k : Nat
⊢ l.zipIdx k = x :: l' ↔ ∃ a as, l = a :: as ∧ x = (a, k) ∧ l' = as.zipIdx (k + 1)

Tactic:
rw [zipIdx_eq_zip_range', zip_eq_cons_iff]

Result:
α : Type u_1
x : α × Nat
l' : List (α × Nat)
l : List α
k : Nat
⊢ (∃ l₁' l₂', l = x.fst :: l₁' ∧ range' k l.length = x.snd :: l₂' ∧ l' = l₁'.zip l₂') ↔
    ∃ a as, l = a :: as ∧ x = (a, k) ∧ l' = as.zipIdx (k + 1)