-- 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:
α : 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
⊢ l = take l₁.length l ++ drop l₁.length l

Tactic:
simp

Result:
no goals

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
this : l₁.length ≤ l.length
⊢ f (i + min l₁.length l.length) l[l₁.length + i] ⋯ = l₂[i]

Tactic:
simp only [Nat.min_eq_left this, Nat.add_comm]

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 + l₁.length) l[i + l₁.length] ⋯ = 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
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]

Tactic:
rw [getElem_append_left hi₂] at w

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₁[i] = f i l[i] ⋯
⊢ f i l[i] ⋯ = l₁[i]

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
l₁' l₂' : List α
f : (i : Nat) → α → i < (l₁' ++ l₂').length → β
i : Nat
h : i < (l₁' ++ l₂').length
⊢ (if h' : i < (l₁'.mapFinIdx fun i a h => f i a ⋯).length then (l₁'.mapFinIdx fun i a h => f i a ⋯)[i]
    else (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:
split <;> rename_i h'

Result:
case mpr.intro.intro.intro.intro.isTrue
α : 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
⊢ (l₁'.mapFinIdx fun i a h => f i a ⋯)[i] = f i (l₁' ++ l₂')[i] h

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
⊢ (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:
α : 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 < ((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
w : (l₁ ++ l₂)[i + l₁.length] = f (i + l₁.length) l[i + l₁.length] ⋯
⊢ l₁.length ≤ i + l₁.length

Tactic:
omega

Result:
no goals

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
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
w : (l₁ ++ l₂)[i + l₁.length] = f (i + l₁.length) l[i + l₁.length] ⋯
⊢ f (i + l₁.length) l[i + l₁.length] ⋯ = l₂[i]

Tactic:
rw [getElem_append_right (by omega)] at w

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
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
w : l₂[i + l₁.length - l₁.length] = f (i + l₁.length) l[i + l₁.length] ⋯
⊢ f (i + l₁.length) l[i + l₁.length] ⋯ = l₂[i]

Proof state:
α : Type ?u.50384
β : Type ?u.50406
l₁ l₂ : List β
l : List α
f : (i : Nat) → α → i < l.length → β
l₁' l₂' : List α
w : l = l₁' ++ l₂'
i : Nat
a : α
h : i < l₂'.length
⊢ 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✝ : (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
⊢ ((take l₁.length l).mapFinIdx fun i a h => f i a ⋯) = l₁ ∧
    ((drop l₁.length l).mapFinIdx fun i a h => f (i + (take l₁.length l).length) a ⋯) = l₂

Tactic:
constructor

Result:
case mp.left
α : 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
⊢ ((take l₁.length l).mapFinIdx fun i a h => f i a ⋯) = l₁

case mp.right
α : 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
⊢ ((drop l₁.length l).mapFinIdx fun i a h => f (i + (take l₁.length l).length) a ⋯) = l₂

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
this : l₁.length ≤ l.length
⊢ f (i + l₁.length) l[i + l₁.length] ⋯ = l₂[i]

Tactic:
specialize w (i + 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
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
w : (l₁ ++ l₂)[i + l₁.length] = f (i + l₁.length) l[i + l₁.length] ⋯
⊢ f (i + l₁.length) l[i + l₁.length] ⋯ = l₂[i]