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

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

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

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

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

Tactic:
exact ⟨x.2, l₂, by simp [enumFrom_eq_zip_range']⟩

Result:
no goals

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

Tactic:
constructor

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

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

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

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

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

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

Tactic:
rw [range'_eq_cons_iff] at h

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

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

Tactic:
rw [enumFrom_eq_zip_range', zip_eq_cons_iff]

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

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

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

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

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

Tactic:
simp [enumFrom_eq_zip_range', range'_succ]

Result:
no goals

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

Tactic:
simp [enumFrom_eq_zip_range']

Result:
no goals

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

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

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