-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem getElem?_mapIdx_go : ∀ {l : List α} {arr : Array β} {i : Nat},
    (mapIdx.go f l arr)[i]? =
      if h : i < arr.size then some arr[i] else Option.map (f i) l[i - arr.size]?
  | [], arr, i => by
    simp only [mapIdx.go, Array.toListImpl_eq, getElem?_def, Array.length_toList,
      ← Array.getElem_toList, length_nil, Nat.not_lt_zero, ↓reduceDIte, Option.map_none']
  | a :: l, arr, i => by
    rw [mapIdx.go, getElem?_mapIdx_go]
    simp only [Array.size_push]
    split <;> split
    · simp only [Option.some.injEq]
      rw [← Array.getElem_toList]
      simp only [Array.push_toList]
      rw [getElem_append_left, ← Array.getElem_toList]
    · have : i = arr.size

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
h✝¹ : i < arr.size + 1
h✝ : ¬i < arr.size
⊢ i = arr.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
⊢ (if h : i < (arr.push (f arr.size a)).size then some (arr.push (f arr.size a))[i]
    else Option.map (f i) l[i - (arr.push (f arr.size a)).size]?) =
    if h : i < arr.size then some arr[i] else Option.map (f i) (a :: l)[i - arr.size]?

Tactic:
simp only [Array.size_push]

Result:
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
⊢ (if h : i < arr.size + 1 then some (arr.push (f arr.size a))[i] else Option.map (f i) l[i - (arr.size + 1)]?) =
    if h : i < arr.size then some arr[i] else Option.map (f i) (a :: l)[i - arr.size]?

Proof state:
case isTrue.isTrue
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
h✝¹ : i < arr.size + 1
h✝ : i < arr.size
⊢ (arr.toList ++ [f arr.size a])[i] = arr[i]

Tactic:
rw [getElem_append_left, ← Array.getElem_toList]

Result:
no goals

Proof state:
case isTrue.isTrue
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
h✝¹ : i < arr.size + 1
h✝ : i < arr.size
⊢ (arr.push (f arr.size a)).toList[i] = arr[i]

Tactic:
simp only [Array.push_toList]

Result:
case isTrue.isTrue
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
h✝¹ : i < arr.size + 1
h✝ : i < arr.size
⊢ (arr.toList ++ [f arr.size a])[i] = arr[i]

Proof state:
case isTrue.isTrue
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
h✝¹ : i < arr.size + 1
h✝ : i < arr.size
⊢ (arr.push (f arr.size a))[i] = arr[i]

Tactic:
rw [← Array.getElem_toList]

Result:
case isTrue.isTrue
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
h✝¹ : i < arr.size + 1
h✝ : i < arr.size
⊢ (arr.push (f arr.size a)).toList[i] = arr[i]

Proof state:
case isFalse.isFalse
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
h✝¹ : ¬i < arr.size + 1
h✝ : ¬i < arr.size
⊢ Option.map (f i) l[i - (arr.size + 1)]? = Option.map (f i) (a :: l)[i - arr.size]?

Tactic:
have : i - arr.size = i - (arr.size + 1) + 1 := by omega

Result:
case isFalse.isFalse
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
h✝¹ : ¬i < arr.size + 1
h✝ : ¬i < arr.size
this : i - arr.size = i - (arr.size + 1) + 1
⊢ Option.map (f i) l[i - (arr.size + 1)]? = Option.map (f i) (a :: l)[i - arr.size]?

Proof state:
case isFalse.isFalse
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
h✝¹ : ¬i < arr.size + 1
h✝ : ¬i < arr.size
this : i - arr.size = i - (arr.size + 1) + 1
⊢ Option.map (f i) l[i - (arr.size + 1)]? = Option.map (f i) (a :: l)[i - arr.size]?

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
h✝¹ : ¬i < arr.size + 1
h✝ : ¬i < arr.size
⊢ i - arr.size = i - (arr.size + 1) + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
arr : Array β
i : Nat
⊢ (mapIdx.go f [] arr)[i]? = if h : i < arr.size then some arr[i] else Option.map (f i) [][i - arr.size]?

Tactic:
simp only [mapIdx.go, Array.toListImpl_eq, getElem?_def, Array.length_toList,
  ← Array.getElem_toList, length_nil, Nat.not_lt_zero, ↓reduceDIte, Option.map_none']

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
⊢ (if h : i < arr.size + 1 then some (arr.push (f arr.size a))[i] else Option.map (f i) l[i - (arr.size + 1)]?) =
    if h : i < arr.size then some arr[i] else Option.map (f i) (a :: l)[i - arr.size]?

Tactic:
split <;> split

Result:
case isTrue.isTrue
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
h✝¹ : i < arr.size + 1
h✝ : i < arr.size
⊢ some (arr.push (f arr.size a))[i] = some arr[i]

case isTrue.isFalse
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
h✝¹ : i < arr.size + 1
h✝ : ¬i < arr.size
⊢ some (arr.push (f arr.size a))[i] = Option.map (f i) (a :: l)[i - arr.size]?

case isFalse.isTrue
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
h✝¹ : ¬i < arr.size + 1
h✝ : i < arr.size
⊢ Option.map (f i) l[i - (arr.size + 1)]? = some arr[i]

case isFalse.isFalse
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
h✝¹ : ¬i < arr.size + 1
h✝ : ¬i < arr.size
⊢ Option.map (f i) l[i - (arr.size + 1)]? = Option.map (f i) (a :: l)[i - arr.size]?

Proof state:
case isFalse.isTrue
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
h✝¹ : ¬i < arr.size + 1
h✝ : i < arr.size
⊢ Option.map (f i) l[i - (arr.size + 1)]? = some arr[i]

Tactic:
omega

Result:
no goals

Proof state:
case isTrue.isTrue
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
h✝¹ : i < arr.size + 1
h✝ : i < arr.size
⊢ some (arr.push (f arr.size a))[i] = some arr[i]

Tactic:
simp only [Option.some.injEq]

Result:
case isTrue.isTrue
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
h✝¹ : i < arr.size + 1
h✝ : i < arr.size
⊢ (arr.push (f arr.size a))[i] = arr[i]

Proof state:
case isTrue.isFalse
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
h✝¹ : i < arr.size + 1
h✝ : ¬i < arr.size
⊢ some (arr.push (f arr.size a))[i] = Option.map (f i) (a :: l)[i - arr.size]?

Tactic:
have : i = arr.size := by omega

Result:
case isTrue.isFalse
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
h✝¹ : i < arr.size + 1
h✝ : ¬i < arr.size
this : i = arr.size
⊢ some (arr.push (f arr.size a))[i] = Option.map (f i) (a :: l)[i - arr.size]?

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
⊢ (mapIdx.go f (a :: l) arr)[i]? = if h : i < arr.size then some arr[i] else Option.map (f i) (a :: l)[i - arr.size]?

Tactic:
rw [mapIdx.go, getElem?_mapIdx_go]

Result:
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
⊢ (if h : i < (arr.push (f arr.size a)).size then some (arr.push (f arr.size a))[i]
    else Option.map (f i) l[i - (arr.push (f arr.size a)).size]?) =
    if h : i < arr.size then some arr[i] else Option.map (f i) (a :: l)[i - arr.size]?

Proof state:
case isTrue.isFalse
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
arr : Array β
i : Nat
h✝¹ : i < arr.size + 1
h✝ : ¬i < arr.size
this : i = arr.size
⊢ some (arr.push (f arr.size a))[i] = Option.map (f i) (a :: l)[i - arr.size]?

Tactic:
simp_all

Result:
no goals