-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem getElem_mapFinIdx_go {as : List α} {f : (i : Nat) → α → (h : i < as.length) → β} {i : Nat} {h} {w} :
    (mapFinIdx.go as f bs acc h)[i] =
      if w' : i < acc.size then
        acc[i]
      else
        f i (bs[i - acc.size]'(by simp at w; omega)) (by simp at w; omega)

Proof state:
case cons
α : Type u_1
β : Type u_2
as : List α
f : (i : Nat) → α → i < as.length → β
i : Nat
head✝ : α
tail✝ : List α
ih :
  ∀ {acc : Array β} {h : tail✝.length + acc.size = as.length} {w : i < (mapFinIdx.go as f tail✝ acc h).length},
    (mapFinIdx.go as f tail✝ acc h)[i] = if w' : i < acc.size then acc[i] else f i tail✝[i - acc.size] ⋯
acc : Array β
h : (head✝ :: tail✝).length + acc.size = as.length
w : i < (mapFinIdx.go as f (head✝ :: tail✝) acc h).length
⊢ (if h_1 : i < acc.size + 1 then (acc.push (f acc.size head✝ ⋯))[i] else f i tail✝[i - (acc.size + 1)] ⋯) =
    if w' : i < acc.size then acc[i] else f i (head✝ :: tail✝)[i - acc.size] ⋯

Tactic:
split <;> rename_i h₁ <;> split <;> rename_i h₂

Result:
case cons.isTrue.isTrue
α : Type u_1
β : Type u_2
as : List α
f : (i : Nat) → α → i < as.length → β
i : Nat
head✝ : α
tail✝ : List α
ih :
  ∀ {acc : Array β} {h : tail✝.length + acc.size = as.length} {w : i < (mapFinIdx.go as f tail✝ acc h).length},
    (mapFinIdx.go as f tail✝ acc h)[i] = if w' : i < acc.size then acc[i] else f i tail✝[i - acc.size] ⋯
acc : Array β
h : (head✝ :: tail✝).length + acc.size = as.length
w : i < (mapFinIdx.go as f (head✝ :: tail✝) acc h).length
h₁ : i < acc.size + 1
h₂ : i < acc.size
⊢ (acc.push (f acc.size head✝ ⋯))[i] = acc[i]

case cons.isTrue.isFalse
α : Type u_1
β : Type u_2
as : List α
f : (i : Nat) → α → i < as.length → β
i : Nat
head✝ : α
tail✝ : List α
ih :
  ∀ {acc : Array β} {h : tail✝.length + acc.size = as.length} {w : i < (mapFinIdx.go as f tail✝ acc h).length},
    (mapFinIdx.go as f tail✝ acc h)[i] = if w' : i < acc.size then acc[i] else f i tail✝[i - acc.size] ⋯
acc : Array β
h : (head✝ :: tail✝).length + acc.size = as.length
w : i < (mapFinIdx.go as f (head✝ :: tail✝) acc h).length
h₁ : i < acc.size + 1
h₂ : ¬i < acc.size
⊢ (acc.push (f acc.size head✝ ⋯))[i] = f i (head✝ :: tail✝)[i - acc.size] ⋯

case cons.isFalse.isTrue
α : Type u_1
β : Type u_2
as : List α
f : (i : Nat) → α → i < as.length → β
i : Nat
head✝ : α
tail✝ : List α
ih :
  ∀ {acc : Array β} {h : tail✝.length + acc.size = as.length} {w : i < (mapFinIdx.go as f tail✝ acc h).length},
    (mapFinIdx.go as f tail✝ acc h)[i] = if w' : i < acc.size then acc[i] else f i tail✝[i - acc.size] ⋯
acc : Array β
h : (head✝ :: tail✝).length + acc.size = as.length
w : i < (mapFinIdx.go as f (head✝ :: tail✝) acc h).length
h₁ : ¬i < acc.size + 1
h₂ : i < acc.size
⊢ f i tail✝[i - (acc.size + 1)] ⋯ = acc[i]

case cons.isFalse.isFalse
α : Type u_1
β : Type u_2
as : List α
f : (i : Nat) → α → i < as.length → β
i : Nat
head✝ : α
tail✝ : List α
ih :
  ∀ {acc : Array β} {h : tail✝.length + acc.size = as.length} {w : i < (mapFinIdx.go as f tail✝ acc h).length},
    (mapFinIdx.go as f tail✝ acc h)[i] = if w' : i < acc.size then acc[i] else f i tail✝[i - acc.size] ⋯
acc : Array β
h : (head✝ :: tail✝).length + acc.size = as.length
w : i < (mapFinIdx.go as f (head✝ :: tail✝) acc h).length
h₁ : ¬i < acc.size + 1
h₂ : ¬i < acc.size
⊢ f i tail✝[i - (acc.size + 1)] ⋯ = f i (head✝ :: tail✝)[i - acc.size] ⋯

Proof state:
α : Type u_1
β : Type u_2
as : List α
f : (i : Nat) → α → i < as.length → β
i : Nat
head✝ : α
tail✝ : List α
ih :
  ∀ {acc : Array β} {h : tail✝.length + acc.size = as.length} {w : i < (mapFinIdx.go as f tail✝ acc h).length},
    (mapFinIdx.go as f tail✝ acc h)[i] = if w' : i < acc.size then acc[i] else f i tail✝[i - acc.size] ⋯
acc : Array β
h : (head✝ :: tail✝).length + acc.size = as.length
w : i < (mapFinIdx.go as f (head✝ :: tail✝) acc h).length
h₁ : ¬i < acc.size + 1
h₂ : ¬i < acc.size
⊢ i - acc.size = i - (acc.size + 1) + 1

Tactic:
omega

Result:
no goals

Proof state:
case cons.isTrue.isTrue
α : Type u_1
β : Type u_2
as : List α
f : (i : Nat) → α → i < as.length → β
i : Nat
head✝ : α
tail✝ : List α
ih :
  ∀ {acc : Array β} {h : tail✝.length + acc.size = as.length} {w : i < (mapFinIdx.go as f tail✝ acc h).length},
    (mapFinIdx.go as f tail✝ acc h)[i] = if w' : i < acc.size then acc[i] else f i tail✝[i - acc.size] ⋯
acc : Array β
h : (head✝ :: tail✝).length + acc.size = as.length
w : i < (mapFinIdx.go as f (head✝ :: tail✝) acc h).length
h₁ : i < acc.size + 1
h₂ : i < acc.size
⊢ (acc.push (f acc.size head✝ ⋯))[i] = acc[i]

Tactic:
rw [Array.getElem_push_lt]

Result:
no goals

Proof state:
case cons.isFalse.isTrue
α : Type u_1
β : Type u_2
as : List α
f : (i : Nat) → α → i < as.length → β
i : Nat
head✝ : α
tail✝ : List α
ih :
  ∀ {acc : Array β} {h : tail✝.length + acc.size = as.length} {w : i < (mapFinIdx.go as f tail✝ acc h).length},
    (mapFinIdx.go as f tail✝ acc h)[i] = if w' : i < acc.size then acc[i] else f i tail✝[i - acc.size] ⋯
acc : Array β
h : (head✝ :: tail✝).length + acc.size = as.length
w : i < (mapFinIdx.go as f (head✝ :: tail✝) acc h).length
h₁ : ¬i < acc.size + 1
h₂ : i < acc.size
⊢ f i tail✝[i - (acc.size + 1)] ⋯ = acc[i]

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.8161
β : Type ?u.8200
bs : List α
acc : Array β
as : List α
f : (i : Nat) → α → i < as.length → β
i : Nat
h : bs.length + acc.size = as.length
w : i < (mapFinIdx.go as f bs acc h).length
w' : ¬i < acc.size
⊢ i - acc.size < bs.length

Tactic:
simp at w

Result:
α : Type ?u.8161
β : Type ?u.8200
bs : List α
acc : Array β
as : List α
f : (i : Nat) → α → i < as.length → β
i : Nat
h : bs.length + acc.size = as.length
w' : ¬i < acc.size
w : i < as.length
⊢ i - acc.size < bs.length

Proof state:
case nil
α : Type u_1
β : Type u_2
as : List α
f : (i : Nat) → α → i < as.length → β
i : Nat
acc : Array β
h✝ : [].length + acc.size = as.length
w✝ : i < (mapFinIdx.go as f [] acc h✝).length
w : i < as.length
h : acc.size = as.length
⊢ acc[i] = if w' : i < acc.size then acc[i] else f i [][i - acc.size] ⋯

Tactic:
rw [dif_pos]

Result:
no goals