-- 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
⊢ (mapFinIdx.go as f (head✝ :: tail✝) acc h)[i] =
    if w' : i < acc.size then acc[i] else f i (head✝ :: tail✝)[i - acc.size] ⋯

Tactic:
simp [mapFinIdx.go]

Result:
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
⊢ (mapFinIdx.go as f tail✝ (acc.push (f acc.size head✝ ⋯)) ⋯)[i] =
    if w' : i < acc.size then acc[i] else f i (head✝ :: tail✝)[i - acc.size] ⋯

Proof state:
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
h₃ : i - acc.size = i - (acc.size + 1) + 1
⊢ f i tail✝[i - (acc.size + 1)] ⋯ = f i (head✝ :: tail✝)[i - acc.size] ⋯

Tactic:
simp [h₃]

Result:
no goals

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 w' : i < (acc.push (f acc.size head✝ ⋯)).size then (acc.push (f acc.size head✝ ⋯))[i]
    else f i tail✝[i - (acc.push (f acc.size head✝ ⋯)).size] ⋯) =
    if w' : i < acc.size then acc[i] else f i (head✝ :: tail✝)[i - acc.size] ⋯

Tactic:
simp

Result:
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] ⋯

Proof state:
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] ⋯

Tactic:
have h₃ : i = acc.size := by omega

Result:
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
h₃ : i = acc.size
⊢ (acc.push (f acc.size head✝ ⋯))[i] = f i (head✝ :: tail✝)[i - acc.size] ⋯

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
⊢ (mapFinIdx.go as f [] acc h)[i] = if w' : i < acc.size then acc[i] else f i [][i - acc.size] ⋯

Tactic:
simp only [length_mapFinIdx_go, length_nil, Nat.zero_add] at w h

Result:
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
⊢ (mapFinIdx.go as f [] acc h✝)[i] = if w' : i < acc.size then acc[i] else f i [][i - acc.size] ⋯

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 < acc.size
w : i < as.length
⊢ i < as.length

Tactic:
omega

Result:
no goals

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
⊢ (mapFinIdx.go as f tail✝ (acc.push (f acc.size head✝ ⋯)) ⋯)[i] =
    if w' : i < acc.size then acc[i] else f i (head✝ :: tail✝)[i - acc.size] ⋯

Tactic:
rw [ih]

Result:
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 w' : i < (acc.push (f acc.size head✝ ⋯)).size then (acc.push (f acc.size head✝ ⋯))[i]
    else f i tail✝[i - (acc.push (f acc.size head✝ ⋯)).size] ⋯) =
    if w' : i < acc.size then acc[i] else f i (head✝ :: tail✝)[i - acc.size] ⋯

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 < as.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 < as.length