-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapFinIdx_append {K L : List α} {f : (i : Nat) → α → (h : i < (K ++ L).length) → β} :
    (K ++ L).mapFinIdx f =
      K.mapFinIdx (fun i a h => f i a (by simp; omega)) ++
        L.mapFinIdx (fun i a h => f (i + K.length) a (by simp; omega))

Proof state:
case h
α : Type u_1
β : Type u_2
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
i : Nat
h₁ : i < ((K ++ L).mapFinIdx f).length
h₂ : i < ((K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.length) a ⋯).length
⊢ f i (K ++ L)[i] ⋯ = if h : i < K.length then f i K[i] ⋯ else f (i - K.length + K.length) L[i - K.length] ⋯

Tactic:
split <;> rename_i h

Result:
case h.isTrue
α : Type u_1
β : Type u_2
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
i : Nat
h₁ : i < ((K ++ L).mapFinIdx f).length
h₂ : i < ((K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.length) a ⋯).length
h : i < K.length
⊢ f i (K ++ L)[i] ⋯ = f i K[i] ⋯

case h.isFalse
α : Type u_1
β : Type u_2
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
i : Nat
h₁ : i < ((K ++ L).mapFinIdx f).length
h₂ : i < ((K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.length) a ⋯).length
h : ¬i < K.length
⊢ f i (K ++ L)[i] ⋯ = f (i - K.length + K.length) L[i - K.length] ⋯

Proof state:
case h
α : Type u_1
β : Type u_2
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
i : Nat
h₁ : i < ((K ++ L).mapFinIdx f).length
h₂ : i < ((K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.length) a ⋯).length
⊢ ((K ++ L).mapFinIdx f)[i] = ((K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.length) a ⋯)[i]

Tactic:
rw [getElem_append]

Result:
case h
α : Type u_1
β : Type u_2
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
i : Nat
h₁ : i < ((K ++ L).mapFinIdx f).length
h₂ : i < ((K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.length) a ⋯).length
⊢ ((K ++ L).mapFinIdx f)[i] =
    if h' : i < (K.mapFinIdx fun i a h => f i a ⋯).length then (K.mapFinIdx fun i a h => f i a ⋯)[i]
    else (L.mapFinIdx fun i a h => f (i + K.length) a ⋯)[i - (K.mapFinIdx fun i a h => f i a ⋯).length]

Proof state:
α : Type ?u.22784
β : Type ?u.22874
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
i : Nat
a : α
h : i < K.length
⊢ i < (K ++ L).length

Tactic:
simp

Result:
α : Type ?u.22784
β : Type ?u.22874
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
i : Nat
a : α
h : i < K.length
⊢ i < K.length + L.length

Proof state:
case hl
α : Type u_1
β : Type u_2
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
⊢ ((K ++ L).mapFinIdx f).length =
    ((K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.length) a ⋯).length

Tactic:
simp

Result:
no goals

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

Tactic:
congr

Result:
case h.isFalse.e_i
α : Type u_1
β : Type u_2
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
i : Nat
h₁ : i < ((K ++ L).mapFinIdx f).length
h₂ : i < ((K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.length) a ⋯).length
h✝ : ¬i < K.length
h : K.length ≤ i
⊢ i = i - K.length + K.length

Proof state:
α : Type u_1
β : Type u_2
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
⊢ (K ++ L).mapFinIdx f = (K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.length) a ⋯

Tactic:
apply ext_getElem

Result:
case hl
α : Type u_1
β : Type u_2
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
⊢ ((K ++ L).mapFinIdx f).length =
    ((K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.length) a ⋯).length

case h
α : Type u_1
β : Type u_2
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
⊢ ∀ (i : Nat) (h₁ : i < ((K ++ L).mapFinIdx f).length)
    (h₂ : i < ((K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.length) a ⋯).length),
    ((K ++ L).mapFinIdx f)[i] = ((K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.length) a ⋯)[i]

Proof state:
α : Type ?u.22784
β : Type ?u.22874
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
i : Nat
a : α
h : i < L.length
⊢ i + K.length < (K ++ L).length

Tactic:
simp

Result:
α : Type ?u.22784
β : Type ?u.22874
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
i : Nat
a : α
h : i < L.length
⊢ i + K.length < K.length + L.length

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

Tactic:
simp only [Nat.not_lt] at h

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

Proof state:
case h.isFalse.e_i
α : Type u_1
β : Type u_2
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
i : Nat
h₁ : i < ((K ++ L).mapFinIdx f).length
h₂ : i < ((K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.length) a ⋯).length
h✝ : ¬i < K.length
h : K.length ≤ i
⊢ i = i - K.length + K.length

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.22784
β : Type ?u.22874
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
i : Nat
a : α
h : i < K.length
⊢ i < K.length + L.length

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.22784
β : Type ?u.22874
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
i : Nat
a : α
h : i < L.length
⊢ i + K.length < K.length + L.length

Tactic:
omega

Result:
no goals

Proof state:
case h.isTrue
α : Type u_1
β : Type u_2
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
i : Nat
h₁ : i < ((K ++ L).mapFinIdx f).length
h₂ : i < ((K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.length) a ⋯).length
h : i < K.length
⊢ f i (K ++ L)[i] ⋯ = f i K[i] ⋯

Tactic:
rw [getElem_append_left]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
i : Nat
h₁ : i < ((K ++ L).mapFinIdx f).length
h₂ : i < ((K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.length) a ⋯).length
⊢ ((K ++ L).mapFinIdx f)[i] =
    if h' : i < (K.mapFinIdx fun i a h => f i a ⋯).length then (K.mapFinIdx fun i a h => f i a ⋯)[i]
    else (L.mapFinIdx fun i a h => f (i + K.length) a ⋯)[i - (K.mapFinIdx fun i a h => f i a ⋯).length]

Tactic:
simp only [getElem_mapFinIdx, length_mapFinIdx]

Result:
case h
α : Type u_1
β : Type u_2
K L : List α
f : (i : Nat) → α → i < (K ++ L).length → β
i : Nat
h₁ : i < ((K ++ L).mapFinIdx f).length
h₂ : i < ((K.mapFinIdx fun i a h => f i a ⋯) ++ L.mapFinIdx fun i a h => f (i + K.length) a ⋯).length
⊢ f i (K ++ L)[i] ⋯ = if h : i < K.length then f i K[i] ⋯ else f (i - K.length + K.length) L[i - K.length] ⋯