-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapFinIdx_eq_append_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
    l.mapFinIdx f = l₁ ++ l₂ ↔
      ∃ (l₁' : List α) (l₂' : List α) (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₁'.length) a (by simp [w]; omega)) = l₂

Proof state:
case mpr
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ (∃ 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₂) →
    ∃ h, ∀ (i : Nat) (h_1 : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h_1

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

Result:
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
l₁' l₂' : List α
f : (i : Nat) → α → i < (l₁' ++ l₂').length → β
⊢ ∃ h,
    ∀ (i : Nat) (h_1 : i < (l₁' ++ l₂').length),
      ((l₁'.mapFinIdx fun i a h => f i a ⋯) ++ l₂'.mapFinIdx fun i a h => f (i + l₁'.length) a ⋯)[i] =
        f i (l₁' ++ l₂')[i] h_1

Proof state:
case mpr.intro.intro.intro.intro.isFalse
α : Type u_1
β : Type u_2
l₁' l₂' : List α
f : (i : Nat) → α → i < (l₁' ++ l₂').length → β
i : Nat
h : i < (l₁' ++ l₂').length
h'✝ : ¬i < (l₁'.mapFinIdx fun i a h => f i a ⋯).length
h' : l₁'.length ≤ i
⊢ (l₂'.mapFinIdx fun i a h => f (i + l₁'.length) a ⋯)[i - (l₁'.mapFinIdx fun i a h => f i a ⋯).length] =
    f i (l₁' ++ l₂')[i] h

Tactic:
have : i - l₁'.length + l₁'.length = i := by omega

Result:
case mpr.intro.intro.intro.intro.isFalse
α : Type u_1
β : Type u_2
l₁' l₂' : List α
f : (i : Nat) → α → i < (l₁' ++ l₂').length → β
i : Nat
h : i < (l₁' ++ l₂').length
h'✝ : ¬i < (l₁'.mapFinIdx fun i a h => f i a ⋯).length
h' : l₁'.length ≤ i
this : i - l₁'.length + l₁'.length = i
⊢ (l₂'.mapFinIdx fun i a h => f (i + l₁'.length) a ⋯)[i - (l₁'.mapFinIdx fun i a h => f i a ⋯).length] =
    f i (l₁' ++ l₂')[i] h

Proof state:
case mp.left.h
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
⊢ ∀ (i : Nat) (h₁ : i < ((take l₁.length l).mapFinIdx fun i a h => f i a ⋯).length) (h₂ : i < l₁.length),
    ((take l₁.length l).mapFinIdx fun i a h => f i a ⋯)[i] = l₁[i]

Tactic:
intro i hi₁ hi₂

Result:
case mp.left.h
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
i : Nat
hi₁ : i < ((take l₁.length l).mapFinIdx fun i a h => f i a ⋯).length
hi₂ : i < l₁.length
⊢ ((take l₁.length l).mapFinIdx fun i a h => f i a ⋯)[i] = l₁[i]

Proof state:
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ 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₁'.length) a ⋯) = l₂

Tactic:
rw [mapFinIdx_eq_iff]

Result:
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ (∃ h, ∀ (i : Nat) (h_1 : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h_1) ↔
    ∃ 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₂

Proof state:
case mp.left.h
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
i : Nat
hi₁ : i < ((take l₁.length l).mapFinIdx fun i a h => f i a ⋯).length
hi₂ : i < l₁.length
⊢ f i l[i] ⋯ = l₁[i]

Tactic:
specialize w i (by omega)

Result:
case mp.left.h
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
h : l₁.length + l₂.length = l.length
i : Nat
hi₁ : i < ((take l₁.length l).mapFinIdx fun i a h => f i a ⋯).length
hi₂ : i < l₁.length
w : (l₁ ++ l₂)[i] = f i l[i] ⋯
⊢ f i l[i] ⋯ = l₁[i]

Proof state:
case mp.left.h
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
i : Nat
hi₁ : i < ((take l₁.length l).mapFinIdx fun i a h => f i a ⋯).length
hi₂ : i < l₁.length
⊢ ((take l₁.length l).mapFinIdx fun i a h => f i a ⋯)[i] = l₁[i]

Tactic:
simp only [getElem_mapFinIdx, getElem_take]

Result:
case mp.left.h
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
i : Nat
hi₁ : i < ((take l₁.length l).mapFinIdx fun i a h => f i a ⋯).length
hi₂ : i < l₁.length
⊢ f i l[i] ⋯ = l₁[i]

Proof state:
case mp.right.h
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
i : Nat
hi₁ : i < ((drop l₁.length l).mapFinIdx fun i a h => f (i + (take l₁.length l).length) a ⋯).length
hi₂ : i < l₂.length
⊢ f (i + min l₁.length l.length) l[l₁.length + i] ⋯ = l₂[i]

Tactic:
have : l₁.length ≤ l.length := by omega

Result:
case mp.right.h
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
i : Nat
hi₁ : i < ((drop l₁.length l).mapFinIdx fun i a h => f (i + (take l₁.length l).length) a ⋯).length
hi₂ : i < l₂.length
this : l₁.length ≤ l.length
⊢ f (i + min l₁.length l.length) l[l₁.length + i] ⋯ = l₂[i]

Proof state:
case mp.right.h
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
i : Nat
hi₁ : i < ((drop l₁.length l).mapFinIdx fun i a h => f (i + (take l₁.length l).length) a ⋯).length
hi₂ : i < l₂.length
⊢ f (i + (take l₁.length l).length) (drop l₁.length l)[i] ⋯ = l₂[i]

Tactic:
simp only [length_take, getElem_drop]

Result:
case mp.right.h
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
i : Nat
hi₁ : i < ((drop l₁.length l).mapFinIdx fun i a h => f (i + (take l₁.length l).length) a ⋯).length
hi₂ : i < l₂.length
⊢ f (i + min l₁.length l.length) l[l₁.length + i] ⋯ = l₂[i]

Proof state:
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h✝ : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h
h : l₁.length + l₂.length = l.length
i : Nat
hi₁ : i < ((drop l₁.length l).mapFinIdx fun i a h => f (i + (take l₁.length l).length) a ⋯).length
hi₂ : i < l₂.length
⊢ l₁.length ≤ l.length

Tactic:
omega

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
⊢ (∃ h, ∀ (i : Nat) (h_1 : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h_1) →
    ∃ 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:
intro ⟨h, w⟩

Result:
case mp
α : Type u_1
β : Type u_2
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
h : (l₁ ++ l₂).length = l.length
w : ∀ (i : Nat) (h_1 : i < l.length), (l₁ ++ l₂)[i] = f i l[i] h_1
⊢ ∃ 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₂