α : Type u
β : Type v
f : ℕ → α → β
l : List α
⊢ ∀ (arr : Array β), length (mapIdx.go f l arr) = length l + Array.size arr
α : Type u
β : Type v
⊢ ∀ (f : ℕ → α → β) (l : List α) (arr : Array β), length (mapIdx.go f l arr) = length l + Array.size arr
intro f l
case nil
α : Type u
β : Type v
f : ℕ → α → β
⊢ ∀ (arr : Array β), length (mapIdx.go f [] arr) = length [] + Array.size arr

case cons
α : Type u
β : Type v
f : ℕ → α → β
head : α
tail : List α
ih : ∀ (arr : Array β), length (mapIdx.go f tail arr) = length tail + Array.size arr
⊢ ∀ (arr : Array β), length (mapIdx.go f (head :: tail) arr) = length (head :: tail) + Array.size arr
α : Type u
β : Type v
f : ℕ → α → β
l : List α
⊢ ∀ (arr : Array β), length (mapIdx.go f l arr) = length l + Array.size arr
induction' l with head tail ih
case nil
α : Type u
β : Type v
f : ℕ → α → β
arr✝ : Array β
⊢ length (mapIdx.go f [] arr✝) = length [] + Array.size arr✝
case nil
α : Type u
β : Type v
f : ℕ → α → β
⊢ ∀ (arr : Array β), length (mapIdx.go f [] arr) = length [] + Array.size arr
intro
no goals
case nil
α : Type u
β : Type v
f : ℕ → α → β
arr✝ : Array β
⊢ length (mapIdx.go f [] arr✝) = length [] + Array.size arr✝
simp only [mapIdx.go, Array.toList_eq, length_nil, zero_add]
case cons
α : Type u
β : Type v
f : ℕ → α → β
head : α
tail : List α
ih : ∀ (arr : Array β), length (mapIdx.go f tail arr) = length tail + Array.size arr
arr✝ : Array β
⊢ length (mapIdx.go f (head :: tail) arr✝) = length (head :: tail) + Array.size arr✝
case cons
α : Type u
β : Type v
f : ℕ → α → β
head : α
tail : List α
ih : ∀ (arr : Array β), length (mapIdx.go f tail arr) = length tail + Array.size arr
⊢ ∀ (arr : Array β), length (mapIdx.go f (head :: tail) arr) = length (head :: tail) + Array.size arr
intro
case cons
α : Type u
β : Type v
f : ℕ → α → β
head : α
tail : List α
ih : ∀ (arr : Array β), length (mapIdx.go f tail arr) = length tail + Array.size arr
arr✝ : Array β
⊢ length (mapIdx.go f tail (Array.push arr✝ (f (Array.size arr✝) head))) = length (head :: tail) + Array.size arr✝
case cons
α : Type u
β : Type v
f : ℕ → α → β
head : α
tail : List α
ih : ∀ (arr : Array β), length (mapIdx.go f tail arr) = length tail + Array.size arr
arr✝ : Array β
⊢ length (mapIdx.go f (head :: tail) arr✝) = length (head :: tail) + Array.size arr✝
simp only [mapIdx.go]
case cons
α : Type u
β : Type v
f : ℕ → α → β
head : α
tail : List α
ih : ∀ (arr : Array β), length (mapIdx.go f tail arr) = length tail + Array.size arr
arr✝ : Array β
⊢ length tail + Array.size (Array.push arr✝ (f (Array.size arr✝) head)) = length (head :: tail) + Array.size arr✝
case cons
α : Type u
β : Type v
f : ℕ → α → β
head : α
tail : List α
ih : ∀ (arr : Array β), length (mapIdx.go f tail arr) = length tail + Array.size arr
arr✝ : Array β
⊢ length (mapIdx.go f tail (Array.push arr✝ (f (Array.size arr✝) head))) = length (head :: tail) + Array.size arr✝
rw [ih]
case cons
α : Type u
β : Type v
f : ℕ → α → β
head : α
tail : List α
ih : ∀ (arr : Array β), length (mapIdx.go f tail arr) = length tail + Array.size arr
arr✝ : Array β
⊢ length tail + (Array.size arr✝ + 1) = Nat.succ (length tail) + Array.size arr✝
case cons
α : Type u
β : Type v
f : ℕ → α → β
head : α
tail : List α
ih : ∀ (arr : Array β), length (mapIdx.go f tail arr) = length tail + Array.size arr
arr✝ : Array β
⊢ length tail + Array.size (Array.push arr✝ (f (Array.size arr✝) head)) = length (head :: tail) + Array.size arr✝
simp only [Array.size_push, length_cons]
no goals
case cons
α : Type u
β : Type v
f : ℕ → α → β
head : α
tail : List α
ih : ∀ (arr : Array β), length (mapIdx.go f tail arr) = length tail + Array.size arr
arr✝ : Array β
⊢ length tail + (Array.size arr✝ + 1) = Nat.succ (length tail) + Array.size arr✝
simp only [Nat.add_succ, add_zero, Nat.add_comm]