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

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

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

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

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

Tactic:
rcases l₁ with ⟨l₁⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
l₂ : Array β
l : List α
f : (i : Nat) → α → i < { toList := l }.size → β
l₁ : List β
⊢ { toList := l }.mapFinIdx f = { toList := l₁ } ++ l₂ ↔
    ∃ l₁' l₂' w,
      (l₁'.mapFinIdx fun i a h => f i a ⋯) = { toList := l₁ } ∧ (l₂'.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₂ : List α
f : (i : Nat) → α → i < { toList := l₁ ++ l₂ }.size → β
⊢ ∃ l₁' l₂' h,
    (l₁'.mapFinIdx fun i a h_1 => f i a ⋯) = { toList := l₁.mapFinIdx fun i a h => f i a ⋯ } ∧
      (l₂'.mapFinIdx fun i a h_1 => f (i + l₁'.size) a ⋯) =
        { toList := l₂.mapFinIdx fun i a h => f (i + l₁.length) a ⋯ }

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

Result:
no goals

Proof state:
α : Type ?u.78996
β : Type ?u.79017
l : Array α
f : (i : Nat) → α → i < l.size → β
l₁ l₂ : Array β
l₁' l₂' : Array α
w : l = l₁' ++ l₂'
i : Nat
a : α
h : i < l₁'.size
⊢ i < l₁'.size + l₂'.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.78996
β : Type ?u.79017
l : Array α
f : (i : Nat) → α → i < l.size → β
l₁ l₂ : Array β
l₁' l₂' : Array α
w : l = l₁' ++ l₂'
i : Nat
a : α
h : i < l₂'.size
⊢ i + l₁'.size < l₁'.size + l₂'.size

Tactic:
omega

Result:
no goals

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

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
l₁ l₂ : Array β
l : List α
f : (i : Nat) → α → i < { toList := l }.size → β
⊢ { toList := l }.mapFinIdx f = l₁ ++ l₂ ↔
    ∃ l₁' l₂' w, (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.mpr.intro.mk.intro.mk.intro.intro
α : Type u_1
β : Type u_2
l₁ l₂ : List α
f : (i : Nat) → α → i < { toList := { toList := l₁ }.toList ++ { toList := l₂ }.toList }.size → β
⊢ ∃ l₁' l₂' w,
    ((l₁'.mapFinIdx fun i a h => f i a ⋯) = l₁.mapFinIdx fun i a h => f i a ⋯) ∧
      (l₂'.mapFinIdx fun i a h => f (i + l₁'.length) a ⋯) = l₂.mapFinIdx fun i a h => f (i + l₁.length) a ⋯

Tactic:
refine ⟨l₁, l₂, 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₂✝ : List β
l₁ l₂ : List α
f : (i : Nat) → α → i < { toList := { toList := l₁ }.toList ++ { toList := l₂ }.toList }.size → β
h₁ : ({ toList := l₁ }.mapFinIdx fun i a h => f i a ⋯) = { toList := l₁✝ }
h₂ : ({ toList := l₂ }.mapFinIdx fun i a h => f (i + { toList := l₁ }.size) a ⋯) = { toList := l₂✝ }
⊢ ∃ l₁' l₂' w, (l₁'.mapFinIdx fun i a h => f i a ⋯) = l₁✝ ∧ (l₂'.mapFinIdx fun i a h => f (i + l₁'.length) a ⋯) = l₂✝

Tactic:
simp [← toList_inj] at h₁ h₂

Result:
case mk.mk.mk.mpr.intro.mk.intro.mk.intro.intro
α : Type u_1
β : Type u_2
l₁✝ l₂✝ : List β
l₁ l₂ : List α
f : (i : Nat) → α → i < { toList := { toList := l₁ }.toList ++ { toList := l₂ }.toList }.size → β
h₁ : (l₁.mapFinIdx fun i a h => f i a ⋯) = l₁✝
h₂ : (l₂.mapFinIdx fun i a h => f (i + l₁.length) a ⋯) = l₂✝
⊢ ∃ l₁' l₂' w, (l₁'.mapFinIdx fun i a h => f i a ⋯) = l₁✝ ∧ (l₂'.mapFinIdx fun i a h => f (i + l₁'.length) a ⋯) = l₂✝