α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
⊢ mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
α : Type u
β : Type v
⊢ ∀ (f : ℕ → α → β) (l₁ l₂ : List α) (arr : Array β),
    mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
intros f l₁ l₂ arr
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
len : ℕ
e : length (l₁ ++ l₂) = len
⊢ mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
⊢ mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
generalize e : (l₁ ++ l₂).length = len
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
⊢ ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
len : ℕ
e : length (l₁ ++ l₂) = len
⊢ mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
revert l₁ l₂ arr
case zero
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
h : length (l₁ ++ l₂) = Nat.zero
⊢ mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))

case succ
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
l₁ l₂ : List α
arr : Array β
h : length (l₁ ++ l₂) = Nat.succ len
⊢ mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
⊢ ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
induction' len with len ih <;> intros l₁ l₂ arr h
case zero
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
⊢ mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
case zero
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
h : length (l₁ ++ l₂) = Nat.zero
⊢ mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
have l₁_nil : l₁ = [] := by cases l₁; rfl; contradiction
case zero
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
l₂_nil : l₂ = []
⊢ mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
case zero
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
⊢ mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
have l₂_nil : l₂ = [] := by cases l₂; rfl; rw [List.length_append] at h; contradiction
case zero
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
l₂_nil : l₂ = []
⊢ mapIdx.go f ([] ++ []) arr = mapIdx.go f [] (toArray (mapIdx.go f [] arr))
case zero
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
l₂_nil : l₂ = []
⊢ mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
rw [l₁_nil, l₂_nil]
no goals
case zero
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
l₂_nil : l₂ = []
⊢ mapIdx.go f ([] ++ []) arr = mapIdx.go f [] (toArray (mapIdx.go f [] arr))
simp only [mapIdx.go, Array.toList_eq, Array.toArray_data]
case nil
α : Type u
β : Type v
f : ℕ → α → β
l₂ : List α
arr : Array β
h : length ([] ++ l₂) = Nat.zero
⊢ [] = []

case cons
α : Type u
β : Type v
f : ℕ → α → β
l₂ : List α
arr : Array β
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝ ++ l₂) = Nat.zero
⊢ head✝ :: tail✝ = []
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
h : length (l₁ ++ l₂) = Nat.zero
⊢ l₁ = []
cases l₁
case cons
α : Type u
β : Type v
f : ℕ → α → β
l₂ : List α
arr : Array β
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝ ++ l₂) = Nat.zero
⊢ head✝ :: tail✝ = []
case nil
α : Type u
β : Type v
f : ℕ → α → β
l₂ : List α
arr : Array β
h : length ([] ++ l₂) = Nat.zero
⊢ [] = []

case cons
α : Type u
β : Type v
f : ℕ → α → β
l₂ : List α
arr : Array β
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝ ++ l₂) = Nat.zero
⊢ head✝ :: tail✝ = []
rfl
no goals
case cons
α : Type u
β : Type v
f : ℕ → α → β
l₂ : List α
arr : Array β
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝ ++ l₂) = Nat.zero
⊢ head✝ :: tail✝ = []
contradiction
case nil
α : Type u
β : Type v
f : ℕ → α → β
l₁ : List α
arr : Array β
l₁_nil : l₁ = []
h : length (l₁ ++ []) = Nat.zero
⊢ [] = []

case cons
α : Type u
β : Type v
f : ℕ → α → β
l₁ : List α
arr : Array β
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : length (l₁ ++ head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
⊢ l₂ = []
cases l₂
case cons
α : Type u
β : Type v
f : ℕ → α → β
l₁ : List α
arr : Array β
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : length (l₁ ++ head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
case nil
α : Type u
β : Type v
f : ℕ → α → β
l₁ : List α
arr : Array β
l₁_nil : l₁ = []
h : length (l₁ ++ []) = Nat.zero
⊢ [] = []

case cons
α : Type u
β : Type v
f : ℕ → α → β
l₁ : List α
arr : Array β
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : length (l₁ ++ head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
rfl
case cons
α : Type u
β : Type v
f : ℕ → α → β
l₁ : List α
arr : Array β
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : length l₁ + length (head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
case cons
α : Type u
β : Type v
f : ℕ → α → β
l₁ : List α
arr : Array β
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : length (l₁ ++ head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
rw [List.length_append] at h
no goals
case cons
α : Type u
β : Type v
f : ℕ → α → β
l₁ : List α
arr : Array β
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : length l₁ + length (head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
contradiction
case succ.nil
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
l₂ : List α
arr : Array β
h : length ([] ++ l₂) = Nat.succ len
⊢ mapIdx.go f ([] ++ l₂) arr = mapIdx.go f l₂ (toArray (Array.toList arr))

case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
l₂ : List α
arr : Array β
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ mapIdx.go f (List.append tail l₂) (Array.push arr (f (Array.size arr) head)) =
    mapIdx.go f l₂ (toArray (mapIdx.go f tail (Array.push arr (f (Array.size arr) head))))
case succ
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
l₁ l₂ : List α
arr : Array β
h : length (l₁ ++ l₂) = Nat.succ len
⊢ mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
cases' l₁ with head tail <;> simp only [mapIdx.go]
no goals
case succ.nil
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
l₂ : List α
arr : Array β
h : length ([] ++ l₂) = Nat.succ len
⊢ mapIdx.go f ([] ++ l₂) arr = mapIdx.go f l₂ (toArray (Array.toList arr))
simp only [nil_append, Array.toList_eq, Array.toArray_data]
case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
l₂ : List α
arr : Array β
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ mapIdx.go f (tail ++ l₂) (Array.push arr (f (Array.size arr) head)) =
    mapIdx.go f l₂ (toArray (mapIdx.go f tail (Array.push arr (f (Array.size arr) head))))
case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
l₂ : List α
arr : Array β
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ mapIdx.go f (List.append tail l₂) (Array.push arr (f (Array.size arr) head)) =
    mapIdx.go f l₂ (toArray (mapIdx.go f tail (Array.push arr (f (Array.size arr) head))))
simp only [List.append_eq]
case succ.cons.e
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
l₂ : List α
arr : Array β
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ length (tail ++ l₂) = len
case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
l₂ : List α
arr : Array β
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ mapIdx.go f (tail ++ l₂) (Array.push arr (f (Array.size arr) head)) =
    mapIdx.go f l₂ (toArray (mapIdx.go f tail (Array.push arr (f (Array.size arr) head))))
rw [ih]
case succ.cons.e
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
l₂ : List α
arr : Array β
head : α
tail : List α
h : length tail + length l₂ = len
⊢ length (tail ++ l₂) = len
case succ.cons.e
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
l₂ : List α
arr : Array β
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ length (tail ++ l₂) = len
simp only [cons_append, length_cons, length_append, Nat.succ.injEq] at h
no goals
case succ.cons.e
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
l₂ : List α
arr : Array β
head : α
tail : List α
h : length tail + length l₂ = len
⊢ length (tail ++ l₂) = len
simp only [length_append, h]