-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapIdx_eq_append_iff {l : Vector α (n + m)} {f : Nat → α → β} {l₁ : Vector β n} {l₂ : Vector β m} :
    mapIdx f l = l₁ ++ l₂ ↔
      ∃ (l₁' : Vector α n) (l₂' : Vector α m), l = l₁' ++ l₂' ∧
        l₁'.mapIdx f = l₁ ∧
        l₂'.mapIdx (fun i => f (i + l₁'.size)) = l₂

Proof state:
case mk.mk
α : Type u_1
m : Nat
β : Type u_2
f : Nat → α → β
l₂ : Vector β m
l : Array α
l₁ : Array β
h : l.size = l₁.size + m
⊢ mapIdx f { toArray := l, size_toArray := h } = { toArray := l₁, size_toArray := ⋯ } ++ l₂ ↔
    ∃ l₁' l₂',
      { toArray := l, size_toArray := h } = l₁' ++ l₂' ∧
        mapIdx f l₁' = { toArray := l₁, size_toArray := ⋯ } ∧ mapIdx (fun i => f (i + l₁'.size)) l₂' = l₂

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

Result:
case mk.mk.mk
α : Type u_1
β : Type u_2
f : Nat → α → β
l : Array α
l₁ l₂ : Array β
h : l.size = l₁.size + l₂.size
⊢ mapIdx f { toArray := l, size_toArray := h } =
      { toArray := l₁, size_toArray := ⋯ } ++ { toArray := l₂, size_toArray := ⋯ } ↔
    ∃ l₁' l₂',
      { toArray := l, size_toArray := h } = l₁' ++ l₂' ∧
        mapIdx f l₁' = { toArray := l₁, size_toArray := ⋯ } ∧
          mapIdx (fun i => f (i + l₁'.size)) l₂' = { toArray := l₂, size_toArray := ⋯ }

Proof state:
case mk.mk.mk
α : Type u_1
β : Type u_2
f : Nat → α → β
l : Array α
l₁ l₂ : Array β
h : l.size = l₁.size + l₂.size
⊢ (∃ l₁' l₂',
      { toArray := l, size_toArray := h } = l₁' ++ l₂' ∧
        (l₁'.mapFinIdx fun i a h => f i a) = { toArray := l₁, size_toArray := ⋯ } ∧
          (l₂'.mapFinIdx fun i a h => f (i + l₁.size) a) = { toArray := l₂, size_toArray := ⋯ }) ↔
    ∃ l₁' l₂',
      { toArray := l, size_toArray := h } = l₁' ++ l₂' ∧
        mapIdx f l₁' = { toArray := l₁, size_toArray := ⋯ } ∧
          mapIdx (fun i => f (i + l₁'.size)) l₂' = { toArray := l₂, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk.mk
α : Type u_1
β : Type u_2
f : Nat → α → β
l : Array α
l₁ l₂ : Array β
h : l.size = l₁.size + l₂.size
⊢ mapIdx f { toArray := l, size_toArray := h } =
      { toArray := l₁, size_toArray := ⋯ } ++ { toArray := l₂, size_toArray := ⋯ } ↔
    ∃ l₁' l₂',
      { toArray := l, size_toArray := h } = l₁' ++ l₂' ∧
        mapIdx f l₁' = { toArray := l₁, size_toArray := ⋯ } ∧
          mapIdx (fun i => f (i + l₁'.size)) l₂' = { toArray := l₂, size_toArray := ⋯ }

Tactic:
rw [mapIdx_eq_mapFinIdx, mapFinIdx_eq_append_iff]

Result:
case mk.mk.mk
α : Type u_1
β : Type u_2
f : Nat → α → β
l : Array α
l₁ l₂ : Array β
h : l.size = l₁.size + l₂.size
⊢ (∃ l₁' l₂',
      { toArray := l, size_toArray := h } = l₁' ++ l₂' ∧
        (l₁'.mapFinIdx fun i a h => f i a) = { toArray := l₁, size_toArray := ⋯ } ∧
          (l₂'.mapFinIdx fun i a h => f (i + l₁.size) a) = { toArray := l₂, size_toArray := ⋯ }) ↔
    ∃ l₁' l₂',
      { toArray := l, size_toArray := h } = l₁' ++ l₂' ∧
        mapIdx f l₁' = { toArray := l₁, size_toArray := ⋯ } ∧
          mapIdx (fun i => f (i + l₁'.size)) l₂' = { toArray := l₂, size_toArray := ⋯ }

Proof state:
case mk
α : Type u_1
n m : Nat
β : Type u_2
f : Nat → α → β
l₁ : Vector β n
l₂ : Vector β m
l : Array α
h : l.size = n + m
⊢ mapIdx f { toArray := l, size_toArray := h } = l₁ ++ l₂ ↔
    ∃ l₁' l₂',
      { toArray := l, size_toArray := h } = l₁' ++ l₂' ∧ mapIdx f l₁' = l₁ ∧ mapIdx (fun i => f (i + l₁'.size)) l₂' = l₂

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

Result:
case mk.mk
α : Type u_1
m : Nat
β : Type u_2
f : Nat → α → β
l₂ : Vector β m
l : Array α
l₁ : Array β
h : l.size = l₁.size + m
⊢ mapIdx f { toArray := l, size_toArray := h } = { toArray := l₁, size_toArray := ⋯ } ++ l₂ ↔
    ∃ l₁' l₂',
      { toArray := l, size_toArray := h } = l₁' ++ l₂' ∧
        mapIdx f l₁' = { toArray := l₁, size_toArray := ⋯ } ∧ mapIdx (fun i => f (i + l₁'.size)) l₂' = l₂

Proof state:
α : Type u_1
n m : Nat
β : Type u_2
l : Vector α (n + m)
f : Nat → α → β
l₁ : Vector β n
l₂ : Vector β m
⊢ mapIdx f l = l₁ ++ l₂ ↔ ∃ l₁' l₂', l = l₁' ++ l₂' ∧ mapIdx f l₁' = l₁ ∧ mapIdx (fun i => f (i + l₁'.size)) l₂' = l₂

Tactic:
rcases l with ⟨l, h⟩

Result:
case mk
α : Type u_1
n m : Nat
β : Type u_2
f : Nat → α → β
l₁ : Vector β n
l₂ : Vector β m
l : Array α
h : l.size = n + m
⊢ mapIdx f { toArray := l, size_toArray := h } = l₁ ++ l₂ ↔
    ∃ l₁' l₂',
      { toArray := l, size_toArray := h } = l₁' ++ l₂' ∧ mapIdx f l₁' = l₁ ∧ mapIdx (fun i => f (i + l₁'.size)) l₂' = l₂