-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapFinIdx_eq_append_iff {l : Vector α (n + m)} {f : (i : Nat) → α → (h : i < n + m) → β}
    {l₁ : Vector β n} {l₂ : Vector β m} :
    l.mapFinIdx f = l₁ ++ l₂ ↔
      ∃ (l₁' : Vector α n) (l₂' : Vector α m), l = l₁' ++ l₂' ∧
        l₁'.mapFinIdx (fun i a h => f i a (by omega)) = l₁ ∧
        l₂'.mapFinIdx (fun i a h => f (i + n) a (by omega)) = l₂

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

Tactic:
rcases l with ⟨l, h⟩

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

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

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

Result:
case mk.mk
α : Type u_1
m : Nat
β : Type u_2
l₂ : Vector β m
l : Array α
l₁ : Array β
f : (i : Nat) → α → i < l₁.size + m → β
h : l.size = l₁.size + m
⊢ { toArray := l, size_toArray := h }.mapFinIdx f = { toArray := l₁, size_toArray := ⋯ } ++ l₂ ↔
    ∃ 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 ⋯) = l₂

Proof state:
case mk.mk.mk
α : Type u_1
β : Type u_2
l : Array α
l₁ l₂ : Array β
f : (i : Nat) → α → i < l₁.size + l₂.size → β
h : l.size = l₁.size + l₂.size
⊢ { toArray := l, size_toArray := h }.mapFinIdx f =
      { toArray := l₁, size_toArray := ⋯ } ++ { toArray := l₂, size_toArray := ⋯ } ↔
    ∃ 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 := ⋯ }

Tactic:
simp only [mapFinIdx_mk, mk_append_mk, eq_mk, Array.mapFinIdx_eq_append_iff, toArray_mapFinIdx,
  mk_eq, toArray_append, exists_and_left, exists_prop]

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

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

Tactic:
constructor

Result:
case mk.mk.mk.mp
α : Type u_1
β : Type u_2
l : Array α
l₁ l₂ : Array β
f : (i : Nat) → α → i < l₁.size + l₂.size → β
h : l.size = l₁.size + l₂.size
⊢ (∃ l₁' l₂' w,
      (l₁'.mapFinIdx fun i a h_1 => f i a ⋯) = l₁ ∧ (l₂'.mapFinIdx fun i a h_1 => f (i + l₁'.size) a ⋯) = l₂) →
    ∃ l₁' l₂',
      l = l₁'.toArray ++ l₂'.toArray ∧
        (l₁'.mapFinIdx fun i a h => f i a ⋯) = l₁ ∧ (l₂'.mapFinIdx fun i a h => f (i + l₁.size) a ⋯) = l₂

case mk.mk.mk.mpr
α : Type u_1
β : Type u_2
l : Array α
l₁ l₂ : Array β
f : (i : Nat) → α → i < l₁.size + l₂.size → β
h : l.size = l₁.size + l₂.size
⊢ (∃ l₁' l₂',
      l = l₁'.toArray ++ l₂'.toArray ∧
        (l₁'.mapFinIdx fun i a h => f i a ⋯) = l₁ ∧ (l₂'.mapFinIdx fun i a h => f (i + l₁.size) a ⋯) = l₂) →
    ∃ l₁' l₂' w, (l₁'.mapFinIdx fun i a h_1 => f i a ⋯) = l₁ ∧ (l₂'.mapFinIdx fun i a h_1 => f (i + l₁'.size) a ⋯) = l₂

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

Tactic:
simp_all

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
m : Nat
β : Type u_2
l₂ : Vector β m
l : Array α
l₁ : Array β
f : (i : Nat) → α → i < l₁.size + m → β
h : l.size = l₁.size + m
⊢ { toArray := l, size_toArray := h }.mapFinIdx f = { toArray := l₁, size_toArray := ⋯ } ++ l₂ ↔
    ∃ 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 ⋯) = l₂

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

Result:
case mk.mk.mk
α : Type u_1
β : Type u_2
l : Array α
l₁ l₂ : Array β
f : (i : Nat) → α → i < l₁.size + l₂.size → β
h : l.size = l₁.size + l₂.size
⊢ { toArray := l, size_toArray := h }.mapFinIdx f =
      { toArray := l₁, size_toArray := ⋯ } ++ { toArray := l₂, size_toArray := ⋯ } ↔
    ∃ 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 := ⋯ }

Proof state:
case mk.mk.mk.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
l₁ l₂ : Array β
f : (i : Nat) → α → i < l₁.size + l₂.size → β
l₁' l₂' : Array α
h : (l₁' ++ l₂').size = l₁.size + l₂.size
h₁ : (l₁'.mapFinIdx fun i a h_1 => f i a ⋯) = l₁
h₂ : (l₂'.mapFinIdx fun i a h_1 => f (i + l₁'.size) a ⋯) = l₂
h₁' : l₁'.size = l₁.size
h₂' : l₂'.size = l₂.size
⊢ ∃ l₁'_1 l₂'_1,
    l₁' ++ l₂' = l₁'_1.toArray ++ l₂'_1.toArray ∧
      (l₁'_1.mapFinIdx fun i a h => f i a ⋯) = l₁ ∧ (l₂'_1.mapFinIdx fun i a h => f (i + l₁.size) a ⋯) = l₂

Tactic:
exact ⟨⟨l₁', h₁'⟩, ⟨l₂', h₂'⟩, by simp_all⟩

Result:
no goals

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

Tactic:
refine ⟨l₁, l₂, by simp_all⟩

Result:
no goals