-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem zipIdx_eq_append_iff {l : List α} {k : Nat} :
    zipIdx l k = l₁ ++ l₂ ↔
      ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = zipIdx l₁' k ∧ l₂ = zipIdx l₂' (k + l₁'.length)

Proof state:
α : Type u_1
l₁ l₂ : List (α × Nat)
l : List α
k : Nat
⊢ l.zipIdx k = l₁ ++ l₂ ↔ ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁'.length)

Tactic:
rw [zipIdx_eq_zip_range', zip_eq_append_iff]

Result:
α : Type u_1
l₁ l₂ : List (α × Nat)
l : List α
k : Nat
⊢ (∃ w x y z, w.length = y.length ∧ l = w ++ x ∧ range' k l.length = y ++ z ∧ l₁ = w.zip y ∧ l₂ = x.zip z) ↔
    ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁'.length)

Proof state:
case mpr
α : Type u_1
l₁ l₂ : List (α × Nat)
l : List α
k : Nat
⊢ (∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁'.length)) →
    ∃ w x y z, w.length = y.length ∧ l = w ++ x ∧ range' k l.length = y ++ z ∧ l₁ = w.zip y ∧ l₂ = x.zip z

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

Result:
case mpr.intro.intro.intro.intro
α : Type u_1
k : Nat
l₁' l₂' : List α
⊢ ∃ w x y z,
    w.length = y.length ∧
      l₁' ++ l₂' = w ++ x ∧
        range' k (l₁' ++ l₂').length = y ++ z ∧ l₁'.zipIdx k = w.zip y ∧ l₂'.zipIdx (k + l₁'.length) = x.zip z

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
k : Nat
w x : List α
⊢ w.zip (range' k w.length) = w.zipIdx k ∧
    x.zip (range' (k + w.length) ((w ++ x).length - w.length)) = x.zipIdx (k + w.length)

Tactic:
simp only [zipIdx_eq_zip_range', length_append, true_and]

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
k : Nat
w x : List α
⊢ x.zip (range' (k + w.length) (w.length + x.length - w.length)) = x.zip (range' (k + w.length) x.length)

Proof state:
α : Type u_1
l₁ l₂ : List (α × Nat)
l : List α
k : Nat
⊢ (∃ w x y z, w.length = y.length ∧ l = w ++ x ∧ range' k l.length = y ++ z ∧ l₁ = w.zip y ∧ l₂ = x.zip z) ↔
    ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁'.length)

Tactic:
constructor

Result:
case mp
α : Type u_1
l₁ l₂ : List (α × Nat)
l : List α
k : Nat
⊢ (∃ w x y z, w.length = y.length ∧ l = w ++ x ∧ range' k l.length = y ++ z ∧ l₁ = w.zip y ∧ l₂ = x.zip z) →
    ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁'.length)

case mpr
α : Type u_1
l₁ l₂ : List (α × Nat)
l : List α
k : Nat
⊢ (∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁'.length)) →
    ∃ w x y z, w.length = y.length ∧ l = w ++ x ∧ range' k l.length = y ++ z ∧ l₁ = w.zip y ∧ l₂ = x.zip z

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.e_a.e_len
α : Type u_1
k : Nat
w x : List α
⊢ w.length + x.length - w.length = x.length

Tactic:
omega

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_1
k : Nat
l₁' l₂' : List α
⊢ l₁'.length = (range' k l₁'.length).length ∧
    l₁' ++ l₂' = l₁' ++ l₂' ∧
      range' k (l₁' ++ l₂').length = range' k l₁'.length ++ range' (k + l₁'.length) l₂'.length ∧
        l₁'.zip (range' k l₁'.length) = l₁'.zip (range' k l₁'.length) ∧
          l₂'.zip (range' (k + l₁'.length) l₂'.length) = l₂'.zip (range' (k + l₁'.length) l₂'.length)

Tactic:
simp [Nat.add_comm]

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
k : Nat
w x : List α
⊢ ∃ l₁' l₂',
    w ++ x = l₁' ++ l₂' ∧
      w.zip (range' k w.length) = l₁'.zipIdx k ∧
        x.zip (range' (k + w.length) ((w ++ x).length - w.length)) = l₂'.zipIdx (k + l₁'.length)

Tactic:
refine ⟨w, x, rfl, ?_⟩

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
k : Nat
w x : List α
⊢ w.zip (range' k w.length) = w.zipIdx k ∧
    x.zip (range' (k + w.length) ((w ++ x).length - w.length)) = x.zipIdx (k + w.length)

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
k✝ : Nat
w x : List α
k : Nat
h : w.length = (range' k✝ k).length
⊢ ∃ l₁' l₂',
    w ++ x = l₁' ++ l₂' ∧
      w.zip (range' k✝ k) = l₁'.zipIdx k✝ ∧ x.zip (range' (k✝ + k) ((w ++ x).length - k)) = l₂'.zipIdx (k✝ + l₁'.length)

Tactic:
simp only [length_range'] at h

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
k✝ : Nat
w x : List α
k : Nat
h : w.length = k
⊢ ∃ l₁' l₂',
    w ++ x = l₁' ++ l₂' ∧
      w.zip (range' k✝ k) = l₁'.zipIdx k✝ ∧ x.zip (range' (k✝ + k) ((w ++ x).length - k)) = l₂'.zipIdx (k✝ + l₁'.length)

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
k✝ : Nat
w x : List α
k : Nat
h : w.length = k
⊢ ∃ l₁' l₂',
    w ++ x = l₁' ++ l₂' ∧
      w.zip (range' k✝ k) = l₁'.zipIdx k✝ ∧ x.zip (range' (k✝ + k) ((w ++ x).length - k)) = l₂'.zipIdx (k✝ + l₁'.length)

Tactic:
obtain rfl := h

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
k : Nat
w x : List α
⊢ ∃ l₁' l₂',
    w ++ x = l₁' ++ l₂' ∧
      w.zip (range' k w.length) = l₁'.zipIdx k ∧
        x.zip (range' (k + w.length) ((w ++ x).length - w.length)) = l₂'.zipIdx (k + l₁'.length)

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_1
k : Nat
l₁' l₂' : List α
⊢ ∃ w x y z,
    w.length = y.length ∧
      l₁' ++ l₂' = w ++ x ∧
        range' k (l₁' ++ l₂').length = y ++ z ∧
          l₁'.zip (range' k l₁'.length) = w.zip y ∧ l₂'.zip (range' (k + l₁'.length) l₂'.length) = x.zip z

Tactic:
refine ⟨l₁', l₂', range' k l₁'.length, range' (k + l₁'.length) l₂'.length, ?_⟩

Result:
case mpr.intro.intro.intro.intro
α : Type u_1
k : Nat
l₁' l₂' : List α
⊢ l₁'.length = (range' k l₁'.length).length ∧
    l₁' ++ l₂' = l₁' ++ l₂' ∧
      range' k (l₁' ++ l₂').length = range' k l₁'.length ++ range' (k + l₁'.length) l₂'.length ∧
        l₁'.zip (range' k l₁'.length) = l₁'.zip (range' k l₁'.length) ∧
          l₂'.zip (range' (k + l₁'.length) l₂'.length) = l₂'.zip (range' (k + l₁'.length) l₂'.length)

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_1
k : Nat
l₁' l₂' : List α
⊢ ∃ w x y z,
    w.length = y.length ∧
      l₁' ++ l₂' = w ++ x ∧
        range' k (l₁' ++ l₂').length = y ++ z ∧ l₁'.zipIdx k = w.zip y ∧ l₂'.zipIdx (k + l₁'.length) = x.zip z

Tactic:
simp only [zipIdx_eq_zip_range']

Result:
case mpr.intro.intro.intro.intro
α : Type u_1
k : Nat
l₁' l₂' : List α
⊢ ∃ w x y z,
    w.length = y.length ∧
      l₁' ++ l₂' = w ++ x ∧
        range' k (l₁' ++ l₂').length = y ++ z ∧
          l₁'.zip (range' k l₁'.length) = w.zip y ∧ l₂'.zip (range' (k + l₁'.length) l₂'.length) = x.zip z

Proof state:
case mp
α : Type u_1
l₁ l₂ : List (α × Nat)
l : List α
k : Nat
⊢ (∃ w x y z, w.length = y.length ∧ l = w ++ x ∧ range' k l.length = y ++ z ∧ l₁ = w.zip y ∧ l₂ = x.zip z) →
    ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁'.length)

Tactic:
rintro ⟨w, x, y, z, h, rfl, h', rfl, rfl⟩

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
k : Nat
w x : List α
y z : List Nat
h : w.length = y.length
h' : range' k (w ++ x).length = y ++ z
⊢ ∃ l₁' l₂', w ++ x = l₁' ++ l₂' ∧ w.zip y = l₁'.zipIdx k ∧ x.zip z = l₂'.zipIdx (k + l₁'.length)

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
k : Nat
w x : List α
y z : List Nat
h : w.length = y.length
h' : range' k (w ++ x).length = y ++ z
⊢ ∃ l₁' l₂', w ++ x = l₁' ++ l₂' ∧ w.zip y = l₁'.zipIdx k ∧ x.zip z = l₂'.zipIdx (k + l₁'.length)

Tactic:
rw [range'_eq_append_iff] at h'

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
k : Nat
w x : List α
y z : List Nat
h : w.length = y.length
h' : ∃ k_1, k_1 ≤ (w ++ x).length ∧ y = range' k k_1 ∧ z = range' (k + k_1) ((w ++ x).length - k_1)
⊢ ∃ l₁' l₂', w ++ x = l₁' ++ l₂' ∧ w.zip y = l₁'.zipIdx k ∧ x.zip z = l₂'.zipIdx (k + l₁'.length)