-- 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:
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₁'.mapFinIdx fun i a h_1 => f i a ⋯).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:
have h₂' := congrArg Array.size h₂

Result:
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₁'.mapFinIdx fun i a h_1 => f i a ⋯).size = l₁.size
h₂' : (l₂'.mapFinIdx fun i a h_1 => f (i + l₁'.size) a ⋯).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₂

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₂
⊢ ∃ 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:
have h₁' := congrArg Array.size h₁

Result:
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₁'.mapFinIdx fun i a h_1 => f i a ⋯).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₂

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₁'.mapFinIdx fun i a h_1 => f i a ⋯).size = l₁.size
h₂' : (l₂'.mapFinIdx fun i a h_1 => f (i + l₁'.size) a ⋯).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:
simp only [Array.size_mapFinIdx] at h₁' h₂'

Result:
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₂

Proof state:
α : Type ?u.40202
n m : Nat
β : Type ?u.40260
l : Vector α (n + m)
f : (i : Nat) → α → i < n + m → β
l₁ : Vector β n
l₂ : Vector β m
l₁' : Vector α n
l₂' : Vector α m
i : Nat
a : α
h : i < n
⊢ i < n + m

Tactic:
omega

Result:
no goals

Proof state:
α : 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₂✝
⊢ ∃ 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:
simp_all

Result:
no goals

Proof state:
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₂

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

Result:
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₂✝

Proof state:
α : Type ?u.40202
n m : Nat
β : Type ?u.40260
l : Vector α (n + m)
f : (i : Nat) → α → i < n + m → β
l₁ : Vector β n
l₂ : Vector β m
l₁' : Vector α n
l₂' : Vector α m
i : Nat
a : α
h : i < m
⊢ i + n < n + m

Tactic:
omega

Result:
no goals

Proof state:
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₂

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

Result:
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₂
⊢ ∃ 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₂