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

Proof state:
case mk.mk.mk.mp.intro.intro.intro.intro
α : Type u_1
k : Nat
l₁' l₂' : Array α
h : (l₁' ++ l₂').size = (l₁'.zipIdx k).size + (l₂'.zipIdx (k + l₁'.size)).size
⊢ ∃ l₁'_1 l₂'_1,
    l₁' ++ l₂' = l₁'_1.toArray ++ l₂'_1.toArray ∧
      l₁'.zipIdx k = l₁'_1.zipIdx k ∧ l₂'.zipIdx (k + l₁'.size) = l₂'_1.zipIdx (k + (l₁'.zipIdx k).size)

Tactic:
exact ⟨⟨l₁', by simp⟩, ⟨l₂', by simp⟩, by simp⟩

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
m : Nat
l₂ : Vector (α × Nat) m
k : Nat
l : Array α
l₁ : Array (α × Nat)
h : l.size = l₁.size + m
⊢ { toArray := l, size_toArray := h }.zipIdx k = { toArray := l₁, size_toArray := ⋯ } ++ l₂ ↔
    ∃ l₁' l₂',
      { toArray := l, size_toArray := h } = l₁' ++ l₂' ∧
        { toArray := l₁, size_toArray := ⋯ } = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁.size)

Tactic:
rcases l₂ with ⟨l₂, rfl⟩

Result:
case mk.mk.mk
α : Type u_1
k : Nat
l : Array α
l₁ l₂ : Array (α × Nat)
h : l.size = l₁.size + l₂.size
⊢ { toArray := l, size_toArray := h }.zipIdx k =
      { toArray := l₁, size_toArray := ⋯ } ++ { toArray := l₂, size_toArray := ⋯ } ↔
    ∃ l₁' l₂',
      { toArray := l, size_toArray := h } = l₁' ++ l₂' ∧
        { toArray := l₁, size_toArray := ⋯ } = l₁'.zipIdx k ∧
          { toArray := l₂, size_toArray := ⋯ } = l₂'.zipIdx (k + l₁.size)

Proof state:
case mk.mk.mk.mpr.intro.mk.intro.mk.intro.intro
α : Type u_1
k : Nat
l₁ l₂ : Array (α × Nat)
l₁' : Array α
h₁ : l₁'.size = l₁.size
l₂' : Array α
h₂ : l₂'.size = l₂.size
h :
  ({ toArray := l₁', size_toArray := h₁ }.toArray ++ { toArray := l₂', size_toArray := h₂ }.toArray).size =
    l₁.size + l₂.size
w₁ : l₁ = { toArray := l₁', size_toArray := h₁ }.zipIdx k
w₂ : l₂ = { toArray := l₂', size_toArray := h₂ }.zipIdx (k + l₁.size)
⊢ ∃ l₁'_1 l₂'_1,
    { toArray := l₁', size_toArray := h₁ }.toArray ++ { toArray := l₂', size_toArray := h₂ }.toArray = l₁'_1 ++ l₂'_1 ∧
      l₁ = l₁'_1.zipIdx k ∧ l₂ = l₂'_1.zipIdx (k + l₁'_1.size)

Tactic:
exact ⟨l₁', l₂', by simp, w₁, by simp [h₁, w₂]⟩

Result:
no goals

Proof state:
case mk.mk.mk.mp
α : Type u_1
k : Nat
l : Array α
l₁ l₂ : Array (α × Nat)
h : l.size = l₁.size + l₂.size
⊢ (∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁'.size)) →
    ∃ l₁' l₂', l = l₁'.toArray ++ l₂'.toArray ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁.size)

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

Result:
case mk.mk.mk.mp.intro.intro.intro.intro
α : Type u_1
k : Nat
l₁' l₂' : Array α
h : (l₁' ++ l₂').size = (l₁'.zipIdx k).size + (l₂'.zipIdx (k + l₁'.size)).size
⊢ ∃ l₁'_1 l₂'_1,
    l₁' ++ l₂' = l₁'_1.toArray ++ l₂'_1.toArray ∧
      l₁'.zipIdx k = l₁'_1.zipIdx k ∧ l₂'.zipIdx (k + l₁'.size) = l₂'_1.zipIdx (k + (l₁'.zipIdx k).size)

Proof state:
case mk.mk.mk
α : Type u_1
k : Nat
l : Array α
l₁ l₂ : Array (α × Nat)
h : l.size = l₁.size + l₂.size
⊢ (∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁'.size)) ↔
    ∃ l₁' l₂', l = l₁'.toArray ++ l₂'.toArray ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁.size)

Tactic:
constructor

Result:
case mk.mk.mk.mp
α : Type u_1
k : Nat
l : Array α
l₁ l₂ : Array (α × Nat)
h : l.size = l₁.size + l₂.size
⊢ (∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁'.size)) →
    ∃ l₁' l₂', l = l₁'.toArray ++ l₂'.toArray ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁.size)

case mk.mk.mk.mpr
α : Type u_1
k : Nat
l : Array α
l₁ l₂ : Array (α × Nat)
h : l.size = l₁.size + l₂.size
⊢ (∃ l₁' l₂', l = l₁'.toArray ++ l₂'.toArray ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁.size)) →
    ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁'.size)

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

Tactic:
rcases l with ⟨l, h⟩

Result:
case mk
α : Type u_1
n m : Nat
l₁ : Vector (α × Nat) n
l₂ : Vector (α × Nat) m
k : Nat
l : Array α
h : l.size = n + m
⊢ { toArray := l, size_toArray := h }.zipIdx k = l₁ ++ l₂ ↔
    ∃ l₁' l₂', { toArray := l, size_toArray := h } = l₁' ++ l₂' ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + n)

Proof state:
case mk
α : Type u_1
n m : Nat
l₁ : Vector (α × Nat) n
l₂ : Vector (α × Nat) m
k : Nat
l : Array α
h : l.size = n + m
⊢ { toArray := l, size_toArray := h }.zipIdx k = l₁ ++ l₂ ↔
    ∃ l₁' l₂', { toArray := l, size_toArray := h } = l₁' ++ l₂' ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + n)

Tactic:
rcases l₁ with ⟨l₁, rfl⟩

Result:
case mk.mk
α : Type u_1
m : Nat
l₂ : Vector (α × Nat) m
k : Nat
l : Array α
l₁ : Array (α × Nat)
h : l.size = l₁.size + m
⊢ { toArray := l, size_toArray := h }.zipIdx k = { toArray := l₁, size_toArray := ⋯ } ++ l₂ ↔
    ∃ l₁' l₂',
      { toArray := l, size_toArray := h } = l₁' ++ l₂' ∧
        { toArray := l₁, size_toArray := ⋯ } = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁.size)

Proof state:
α : Type u_1
k : Nat
l₁ l₂ : Array (α × Nat)
l₁' : Array α
h₁ : l₁'.size = l₁.size
l₂' : Array α
h₂ : l₂'.size = l₂.size
h :
  ({ toArray := l₁', size_toArray := h₁ }.toArray ++ { toArray := l₂', size_toArray := h₂ }.toArray).size =
    l₁.size + l₂.size
w₁ : l₁ = { toArray := l₁', size_toArray := h₁ }.zipIdx k
w₂ : l₂ = { toArray := l₂', size_toArray := h₂ }.zipIdx (k + l₁.size)
⊢ l₂ = l₂'.zipIdx (k + l₁'.size)

Tactic:
simp [h₁, w₂]

Result:
no goals

Proof state:
α : Type u_1
k : Nat
l₁' l₂' : Array α
h : (l₁' ++ l₂').size = (l₁'.zipIdx k).size + (l₂'.zipIdx (k + l₁'.size)).size
⊢ l₂'.size = (l₂'.zipIdx (k + l₁'.size)).size

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
k : Nat
l₁ l₂ : Array (α × Nat)
l₁' : Array α
h₁ : l₁'.size = l₁.size
l₂' : Array α
h₂ : l₂'.size = l₂.size
h :
  ({ toArray := l₁', size_toArray := h₁ }.toArray ++ { toArray := l₂', size_toArray := h₂ }.toArray).size =
    l₁.size + l₂.size
w₁ : l₁ = { toArray := l₁', size_toArray := h₁ }.zipIdx k
w₂ : l₂ = { toArray := l₂', size_toArray := h₂ }.zipIdx (k + l₁.size)
⊢ { toArray := l₁', size_toArray := h₁ }.toArray ++ { toArray := l₂', size_toArray := h₂ }.toArray = l₁' ++ l₂'

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
k : Nat
l₁' l₂' : Array α
h : (l₁' ++ l₂').size = (l₁'.zipIdx k).size + (l₂'.zipIdx (k + l₁'.size)).size
⊢ l₁'.size = (l₁'.zipIdx k).size

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk.mk.mpr
α : Type u_1
k : Nat
l : Array α
l₁ l₂ : Array (α × Nat)
h : l.size = l₁.size + l₂.size
⊢ (∃ l₁' l₂', l = l₁'.toArray ++ l₂'.toArray ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁.size)) →
    ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁'.size)

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

Result:
case mk.mk.mk.mpr.intro.mk.intro.mk.intro.intro
α : Type u_1
k : Nat
l₁ l₂ : Array (α × Nat)
l₁' : Array α
h₁ : l₁'.size = l₁.size
l₂' : Array α
h₂ : l₂'.size = l₂.size
h :
  ({ toArray := l₁', size_toArray := h₁ }.toArray ++ { toArray := l₂', size_toArray := h₂ }.toArray).size =
    l₁.size + l₂.size
w₁ : l₁ = { toArray := l₁', size_toArray := h₁ }.zipIdx k
w₂ : l₂ = { toArray := l₂', size_toArray := h₂ }.zipIdx (k + l₁.size)
⊢ ∃ l₁'_1 l₂'_1,
    { toArray := l₁', size_toArray := h₁ }.toArray ++ { toArray := l₂', size_toArray := h₂ }.toArray = l₁'_1 ++ l₂'_1 ∧
      l₁ = l₁'_1.zipIdx k ∧ l₂ = l₂'_1.zipIdx (k + l₁'_1.size)