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

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
n : Nat
y z : List α
⊢ (range' (n + y.length) (y.length + z.length - y.length)).zip z = (range' (n + y.length) z.length).zip z

Tactic:
congr

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.e_a.e_len
α : Type u_1
n : Nat
y z : List α
⊢ y.length + z.length - y.length = z.length

Proof state:
case mpr
α : Type u_1
l₁ l₂ : List (Nat × α)
l : List α
n : Nat
⊢ (∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = enumFrom n l₁' ∧ l₂ = enumFrom (n + l₁'.length) l₂') →
    ∃ w x y z, w.length = y.length ∧ range' n l.length = w ++ x ∧ l = 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
n : Nat
l₁' l₂' : List α
⊢ ∃ w x y z,
    w.length = y.length ∧
      range' n (l₁' ++ l₂').length = w ++ x ∧
        l₁' ++ l₂' = y ++ z ∧ enumFrom n l₁' = w.zip y ∧ enumFrom (n + l₁'.length) l₂' = x.zip z

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

Tactic:
constructor

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

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

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

Tactic:
rw [range'_eq_append_iff] at h'

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

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

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
n : Nat
y z : List α
⊢ ∃ l₁' l₂',
    y ++ z = l₁' ++ l₂' ∧
      (range' n y.length).zip y = enumFrom n l₁' ∧
        (range' (n + y.length) ((y ++ z).length - y.length)).zip z = enumFrom (n + l₁'.length) l₂'

Tactic:
refine ⟨y, z, rfl, ?_⟩

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
n : Nat
y z : List α
⊢ (range' n y.length).zip y = enumFrom n y ∧
    (range' (n + y.length) ((y ++ z).length - y.length)).zip z = enumFrom (n + y.length) z

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

Tactic:
rw [enumFrom_eq_zip_range', zip_eq_append_iff]

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

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

Tactic:
obtain rfl := h

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
n : Nat
y z : List α
⊢ ∃ l₁' l₂',
    y ++ z = l₁' ++ l₂' ∧
      (range' n y.length).zip y = enumFrom n l₁' ∧
        (range' (n + y.length) ((y ++ z).length - y.length)).zip z = enumFrom (n + l₁'.length) l₂'

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

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

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

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

Tactic:
simp only [length_range'] at h

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

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

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

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

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
n : Nat
y z : List α
⊢ (range' n y.length).zip y = enumFrom n y ∧
    (range' (n + y.length) ((y ++ z).length - y.length)).zip z = enumFrom (n + y.length) z

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

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
n : Nat
y z : List α
⊢ (range' (n + y.length) (y.length + z.length - y.length)).zip z = (range' (n + y.length) z.length).zip z