-- 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.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] ⋯

Tactic:
subst h₃

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

Tactic:
omega

Result:
no goals

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

Tactic:
simp only [mapFinIdx.go, Array.getElem_toList]

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
⊢ acc[i] = if w' : i < acc.size then acc[i] else f i [][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

Tactic:
omega

Result:
no goals

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

Tactic:
have h₃ : i - acc.size = (i - (acc.size + 1)) + 1 := by omega

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

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

Tactic:
simp

Result:
no goals