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

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

Tactic:
rcases l₁ with ⟨l₁⟩

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

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

Tactic:
rcases l with ⟨l⟩

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

Proof state:
case mk.mk.mk.mp.intro.intro.intro.intro
α : Type u_1
k : Nat
l₁' l₂' : List α
⊢ ∃ l₁'_1 l₂'_1,
    l₁' ++ l₂' = l₁'_1.toList ++ l₂'_1.toList ∧
      { toList := l₁'.zipIdx k } = l₁'_1.zipIdx k ∧
        { toList := l₂'.zipIdx (k + l₁'.length) } = l₂'_1.zipIdx (k + l₁'_1.size)

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

Result:
no goals

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

Tactic:
rcases l₂ with ⟨l₂⟩

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

Proof state:
case mk.mk.mk
α : Type u_1
k : Nat
l : List α
l₁ l₂ : List (α × Nat)
⊢ { toList := l }.zipIdx k = { toList := l₁ } ++ { toList := l₂ } ↔
    ∃ l₁' l₂',
      { toList := l } = l₁' ++ l₂' ∧ { toList := l₁ } = l₁'.zipIdx k ∧ { toList := l₂ } = l₂'.zipIdx (k + l₁'.size)

Tactic:
simp only [zipIdx_toArray, List.append_toArray, mk.injEq, List.zipIdx_eq_append_iff,
  toArray_eq_append_iff]

Result:
case mk.mk.mk
α : Type u_1
k : Nat
l : List α
l₁ l₂ : List (α × Nat)
⊢ (∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁'.length)) ↔
    ∃ l₁' l₂',
      l = l₁'.toList ++ l₂'.toList ∧ { toList := l₁ } = l₁'.zipIdx k ∧ { toList := l₂ } = 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₂' : List α
⊢ ∃ l₁'_1 l₂'_1,
    { toList := l₁' }.toList ++ { toList := l₂' }.toList = l₁'_1 ++ l₂'_1 ∧
      l₁'.zipIdx k = l₁'_1.zipIdx k ∧ l₂'.zipIdx (k + l₁'.length) = l₂'_1.zipIdx (k + l₁'_1.length)

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

Result:
no goals

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

Tactic:
simp only [zipIdx_toArray, mk.injEq, size_toArray] at h

Result:
case mk.mk.mk.mpr.intro.mk.intro.mk.intro
α : Type u_1
k : Nat
l₁ l₂ : List (α × Nat)
l₁' l₂' : List α
h : l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁'.length)
⊢ ∃ l₁'_1 l₂'_1,
    { toList := l₁' }.toList ++ { toList := l₂' }.toList = l₁'_1 ++ l₂'_1 ∧
      l₁ = l₁'_1.zipIdx k ∧ l₂ = l₂'_1.zipIdx (k + l₁'_1.length)

Proof state:
case mk.mk.mk.mpr
α : Type u_1
k : Nat
l : List α
l₁ l₂ : List (α × Nat)
⊢ (∃ l₁' l₂',
      l = l₁'.toList ++ l₂'.toList ∧ { toList := l₁ } = l₁'.zipIdx k ∧ { toList := l₂ } = l₂'.zipIdx (k + l₁'.size)) →
    ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁'.length)

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

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

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

Tactic:
constructor

Result:
case mk.mk.mk.mp
α : Type u_1
k : Nat
l : List α
l₁ l₂ : List (α × Nat)
⊢ (∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁'.length)) →
    ∃ l₁' l₂',
      l = l₁'.toList ++ l₂'.toList ∧ { toList := l₁ } = l₁'.zipIdx k ∧ { toList := l₂ } = l₂'.zipIdx (k + l₁'.size)

case mk.mk.mk.mpr
α : Type u_1
k : Nat
l : List α
l₁ l₂ : List (α × Nat)
⊢ (∃ l₁' l₂',
      l = l₁'.toList ++ l₂'.toList ∧ { toList := l₁ } = l₁'.zipIdx k ∧ { toList := l₂ } = l₂'.zipIdx (k + l₁'.size)) →
    ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁'.length)

Proof state:
α : Type u_1
k : Nat
l₁' l₂' : List α
⊢ { toList := l₁' }.toList ++ { toList := l₂' }.toList = l₁' ++ l₂' ∧
    l₁'.zipIdx k = l₁'.zipIdx k ∧ l₂'.zipIdx (k + l₁'.length) = l₂'.zipIdx (k + l₁'.length)

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk.mk.mp
α : Type u_1
k : Nat
l : List α
l₁ l₂ : List (α × Nat)
⊢ (∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁'.length)) →
    ∃ l₁' l₂',
      l = l₁'.toList ++ l₂'.toList ∧ { toList := l₁ } = l₁'.zipIdx k ∧ { toList := 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₂' : List α
⊢ ∃ l₁'_1 l₂'_1,
    l₁' ++ l₂' = l₁'_1.toList ++ l₂'_1.toList ∧
      { toList := l₁'.zipIdx k } = l₁'_1.zipIdx k ∧
        { toList := l₂'.zipIdx (k + l₁'.length) } = l₂'_1.zipIdx (k + l₁'_1.size)

Proof state:
α : Type u_1
k : Nat
l₁' l₂' : List α
⊢ l₁' ++ l₂' = { toList := l₁' }.toList ++ { toList := l₂' }.toList ∧
    { toList := l₁'.zipIdx k } = { toList := l₁' }.zipIdx k ∧
      { toList := l₂'.zipIdx (k + l₁'.length) } = { toList := l₂' }.zipIdx (k + { toList := l₁' }.size)

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk.mk.mpr.intro.mk.intro.mk.intro
α : Type u_1
k : Nat
l₁ l₂ : List (α × Nat)
l₁' l₂' : List α
h : l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁'.length)
⊢ ∃ l₁'_1 l₂'_1,
    { toList := l₁' }.toList ++ { toList := l₂' }.toList = l₁'_1 ++ l₂'_1 ∧
      l₁ = l₁'_1.zipIdx k ∧ l₂ = l₂'_1.zipIdx (k + l₁'_1.length)

Tactic:
obtain ⟨rfl, rfl⟩ := h

Result:
case mk.mk.mk.mpr.intro.mk.intro.mk.intro.intro
α : Type u_1
k : Nat
l₁' l₂' : List α
⊢ ∃ l₁'_1 l₂'_1,
    { toList := l₁' }.toList ++ { toList := l₂' }.toList = l₁'_1 ++ l₂'_1 ∧
      l₁'.zipIdx k = l₁'_1.zipIdx k ∧ l₂'.zipIdx (k + l₁'.length) = l₂'_1.zipIdx (k + l₁'_1.length)