[GOAL]
α : Type u
β : Type v
l : List α
f : ℕ → α → β
n : ℕ
⊢ List.oldMapIdxCore f n l = List.oldMapIdx (fun i a => f (i + n) a) l
[PROOFSTEP]
induction' l with hd tl hl generalizing f n
[GOAL]
case nil
α : Type u
β : Type v
f✝ : ℕ → α → β
n✝ : ℕ
f : ℕ → α → β
n : ℕ
⊢ List.oldMapIdxCore f n [] = List.oldMapIdx (fun i a => f (i + n) a) []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
f✝ : ℕ → α → β
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (f : ℕ → α → β) (n : ℕ), List.oldMapIdxCore f n tl = List.oldMapIdx (fun i a => f (i + n) a) tl
f : ℕ → α → β
n : ℕ
⊢ List.oldMapIdxCore f n (hd :: tl) = List.oldMapIdx (fun i a => f (i + n) a) (hd :: tl)
[PROOFSTEP]
rw [List.oldMapIdx]
[GOAL]
case cons
α : Type u
β : Type v
f✝ : ℕ → α → β
n✝ : ℕ
hd : α
tl : List α
hl : ∀ (f : ℕ → α → β) (n : ℕ), List.oldMapIdxCore f n tl = List.oldMapIdx (fun i a => f (i + n) a) tl
f : ℕ → α → β
n : ℕ
⊢ List.oldMapIdxCore f n (hd :: tl) = List.oldMapIdxCore (fun i a => f (i + n) a) 0 (hd :: tl)
[PROOFSTEP]
simp only [List.oldMapIdxCore, hl, add_left_comm, add_comm, add_zero, zero_add]
[GOAL]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
⊢ ∀ (l : List α), p l
[PROOFSTEP]
let q := fun l ↦ p (reverse l)
[GOAL]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
⊢ ∀ (l : List α), p l
[PROOFSTEP]
have pq : ∀ l, p (reverse l) → q l := by simp only [reverse_reverse]; intro; exact id
[GOAL]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
⊢ ∀ (l : List α), p (reverse l) → q l
[PROOFSTEP]
simp only [reverse_reverse]
[GOAL]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
⊢ ∀ (l : List α), p (reverse l) → p (reverse l)
[PROOFSTEP]
intro
[GOAL]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
l✝ : List α
⊢ p (reverse l✝) → p (reverse l✝)
[PROOFSTEP]
exact id
[GOAL]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
⊢ ∀ (l : List α), p l
[PROOFSTEP]
have qp : ∀ l, q (reverse l) → p l := by simp only [reverse_reverse]; intro; exact id
[GOAL]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
⊢ ∀ (l : List α), q (reverse l) → p l
[PROOFSTEP]
simp only [reverse_reverse]
[GOAL]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
⊢ ∀ (l : List α), p l → p l
[PROOFSTEP]
intro
[GOAL]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
l✝ : List α
⊢ p l✝ → p l✝
[PROOFSTEP]
exact id
[GOAL]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
⊢ ∀ (l : List α), p l
[PROOFSTEP]
intro l
[GOAL]
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
⊢ p l
[PROOFSTEP]
apply qp
[GOAL]
case a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
⊢ q (reverse l)
[PROOFSTEP]
generalize (reverse l) = l
[GOAL]
case a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l✝ l : List α
⊢ q l
[PROOFSTEP]
induction' l with head tail ih
[GOAL]
case a.nil
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
⊢ q []
[PROOFSTEP]
apply pq
[GOAL]
case a.nil.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
⊢ p (reverse [])
[PROOFSTEP]
simp only [reverse_nil, base]
[GOAL]
case a.cons
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ q (head :: tail)
[PROOFSTEP]
apply pq
[GOAL]
case a.cons.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ p (reverse (head :: tail))
[PROOFSTEP]
simp only [reverse_cons]
[GOAL]
case a.cons.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ p (reverse tail ++ [head])
[PROOFSTEP]
apply ind
[GOAL]
case a.cons.a.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ p (reverse tail)
[PROOFSTEP]
apply qp
[GOAL]
case a.cons.a.a.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ q (reverse (reverse tail))
[PROOFSTEP]
rw [reverse_reverse]
[GOAL]
case a.cons.a.a.a
α : Type u
β : Type v
p : List α → Prop
base : p []
ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])
q : List α → Prop := fun l => p (reverse l)
pq : ∀ (l : List α), p (reverse l) → q l
qp : ∀ (l : List α), q (reverse l) → p l
l : List α
head : α
tail : List α
ih : q tail
⊢ q tail
[PROOFSTEP]
exact ih
[GOAL]
α : Type u
β : Type v
⊢ ∀ (f : ℕ → α → β) (n : ℕ) (l₁ l₂ : List α),
    List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
[PROOFSTEP]
intros f n l₁ l₂
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
[PROOFSTEP]
generalize e : (l₁ ++ l₂).length = len
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
len : ℕ
e : length (l₁ ++ l₂) = len
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
[PROOFSTEP]
revert n l₁ l₂
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
⊢ ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
[PROOFSTEP]
induction' len with len ih
[GOAL]
case zero
α : Type u
β : Type v
f : ℕ → α → β
⊢ ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = Nat.zero →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
[PROOFSTEP]
intros n l₁ l₂ h
[GOAL]
case succ
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
⊢ ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = Nat.succ len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
[PROOFSTEP]
intros n l₁ l₂ h
[GOAL]
case zero
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.zero
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
[PROOFSTEP]
have l₁_nil : l₁ = [] := by cases l₁; rfl; contradiction
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.zero
⊢ l₁ = []
[PROOFSTEP]
cases l₁
[GOAL]
case nil
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₂ : List α
h : length ([] ++ l₂) = Nat.zero
⊢ [] = []
case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₂ : List α
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝ ++ l₂) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₂ : List α
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝ ++ l₂) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
contradiction
[GOAL]
case zero
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
[PROOFSTEP]
have l₂_nil : l₂ = [] := by cases l₂; rfl; rw [List.length_append] at h ; contradiction
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
⊢ l₂ = []
[PROOFSTEP]
cases l₂
[GOAL]
case nil
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ : List α
l₁_nil : l₁ = []
h : length (l₁ ++ []) = Nat.zero
⊢ [] = []
case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ : List α
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : length (l₁ ++ head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ : List α
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : length (l₁ ++ head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
rw [List.length_append] at h 
[GOAL]
case cons
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ : List α
l₁_nil : l₁ = []
head✝ : α
tail✝ : List α
h : length l₁ + length (head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
contradiction
[GOAL]
case zero
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
l₂_nil : l₂ = []
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
[PROOFSTEP]
simp only [l₁_nil, l₂_nil]
[GOAL]
case zero
α : Type u
β : Type v
f : ℕ → α → β
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
l₂_nil : l₂ = []
⊢ List.oldMapIdxCore f n ([] ++ []) = List.oldMapIdxCore f n [] ++ List.oldMapIdxCore f (n + length []) []
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₁ l₂ : List α
h : length (l₁ ++ l₂) = Nat.succ len
⊢ List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
[PROOFSTEP]
cases' l₁ with head tail
[GOAL]
case succ.nil
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
h : length ([] ++ l₂) = Nat.succ len
⊢ List.oldMapIdxCore f n ([] ++ l₂) = List.oldMapIdxCore f n [] ++ List.oldMapIdxCore f (n + length []) l₂
[PROOFSTEP]
rfl
[GOAL]
case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ List.oldMapIdxCore f n (head :: tail ++ l₂) =
    List.oldMapIdxCore f n (head :: tail) ++ List.oldMapIdxCore f (n + length (head :: tail)) l₂
[PROOFSTEP]
simp only [List.oldMapIdxCore, List.append_eq, length_cons, cons_append, cons.injEq, true_and]
[GOAL]
case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ List.oldMapIdxCore f (n + 1) (tail ++ l₂) =
    List.oldMapIdxCore f (n + 1) tail ++ List.oldMapIdxCore f (n + Nat.succ (length tail)) l₂
[PROOFSTEP]
suffices : n + Nat.succ (length tail) = n + 1 + tail.length
[GOAL]
case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
this : n + Nat.succ (length tail) = n + 1 + length tail
⊢ List.oldMapIdxCore f (n + 1) (tail ++ l₂) =
    List.oldMapIdxCore f (n + 1) tail ++ List.oldMapIdxCore f (n + Nat.succ (length tail)) l₂
case this
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ n + Nat.succ (length tail) = n + 1 + length tail
[PROOFSTEP]
{ rw [this]
  apply ih (n + 1) _ _ _
  simp only [cons_append, length_cons, length_append, Nat.succ.injEq] at h 
  simp only [length_append, h]
}
[GOAL]
case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
this : n + Nat.succ (length tail) = n + 1 + length tail
⊢ List.oldMapIdxCore f (n + 1) (tail ++ l₂) =
    List.oldMapIdxCore f (n + 1) tail ++ List.oldMapIdxCore f (n + Nat.succ (length tail)) l₂
[PROOFSTEP]
rw [this]
[GOAL]
case succ.cons
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
this : n + Nat.succ (length tail) = n + 1 + length tail
⊢ List.oldMapIdxCore f (n + 1) (tail ++ l₂) =
    List.oldMapIdxCore f (n + 1) tail ++ List.oldMapIdxCore f (n + 1 + length tail) l₂
[PROOFSTEP]
apply ih (n + 1) _ _ _
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
this : n + Nat.succ (length tail) = n + 1 + length tail
⊢ length (tail ++ l₂) = len
[PROOFSTEP]
simp only [cons_append, length_cons, length_append, Nat.succ.injEq] at h 
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
this : n + Nat.succ (length tail) = n + 1 + length tail
h : length tail + length l₂ = len
⊢ length (tail ++ l₂) = len
[PROOFSTEP]
simp only [length_append, h]
[GOAL]
case this
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ n + Nat.succ (length tail) = n + 1 + length tail
[PROOFSTEP]
{rw [Nat.add_assoc]; simp only [Nat.add_comm]
}
-- Porting note: new theorem.
[GOAL]
case this
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ n + Nat.succ (length tail) = n + 1 + length tail
[PROOFSTEP]
rw [Nat.add_assoc]
[GOAL]
case this
α : Type u
β : Type v
f : ℕ → α → β
len : ℕ
ih :
  ∀ (n : ℕ) (l₁ l₂ : List α),
    length (l₁ ++ l₂) = len →
      List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + length l₁) l₂
n : ℕ
l₂ : List α
head : α
tail : List α
h : length (head :: tail ++ l₂) = Nat.succ len
⊢ n + Nat.succ (length tail) = n + (1 + length tail)
[PROOFSTEP]
simp only [Nat.add_comm]
[GOAL]
α : Type u
β : Type v
⊢ ∀ (f : ℕ → α → β) (l : List α) (e : α), List.oldMapIdx f (l ++ [e]) = List.oldMapIdx f l ++ [f (length l) e]
[PROOFSTEP]
intros f l e
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdx f (l ++ [e]) = List.oldMapIdx f l ++ [f (length l) e]
[PROOFSTEP]
unfold List.oldMapIdx
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdxCore f 0 (l ++ [e]) = List.oldMapIdxCore f 0 l ++ [f (length l) e]
[PROOFSTEP]
rw [List.oldMapIdxCore_append f 0 l [e]]
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdxCore f 0 l ++ List.oldMapIdxCore f (0 + length l) [e] = List.oldMapIdxCore f 0 l ++ [f (length l) e]
[PROOFSTEP]
simp only [zero_add, append_cancel_left_eq]
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdxCore f (length l) [e] = [f (length l) e]
[PROOFSTEP]
rfl
  -- Porting note: new theorem.
[GOAL]
α : 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))
[PROOFSTEP]
intros f l₁ l₂ arr
[GOAL]
α : 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))
[PROOFSTEP]
generalize e : (l₁ ++ l₂).length = len
[GOAL]
α : 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))
[PROOFSTEP]
revert l₁ l₂ arr
[GOAL]
α : 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))
[PROOFSTEP]
induction' len with len ih
[GOAL]
case zero
α : Type u
β : Type v
f : ℕ → α → β
⊢ ∀ (l₁ l₂ : List α) (arr : Array β),
    length (l₁ ++ l₂) = Nat.zero → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
[PROOFSTEP]
intros l₁ l₂ arr h
[GOAL]
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 β),
    length (l₁ ++ l₂) = Nat.succ len → mapIdx.go f (l₁ ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f l₁ arr))
[PROOFSTEP]
intros l₁ l₂ arr h
[GOAL]
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))
[PROOFSTEP]
have l₁_nil : l₁ = [] := by cases l₁; rfl; contradiction
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
h : length (l₁ ++ l₂) = Nat.zero
⊢ l₁ = []
[PROOFSTEP]
cases l₁
[GOAL]
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✝ = []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
f : ℕ → α → β
l₂ : List α
arr : Array β
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝ ++ l₂) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
contradiction
[GOAL]
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))
[PROOFSTEP]
have l₂_nil : l₂ = [] := by cases l₂; rfl; rw [List.length_append] at h ; contradiction
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
l₁ l₂ : List α
arr : Array β
h : length (l₁ ++ l₂) = Nat.zero
l₁_nil : l₁ = []
⊢ l₂ = []
[PROOFSTEP]
cases l₂
[GOAL]
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✝ = []
[PROOFSTEP]
rfl
[GOAL]
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✝ = []
[PROOFSTEP]
rw [List.length_append] at h 
[GOAL]
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✝ = []
[PROOFSTEP]
contradiction
[GOAL]
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))
[PROOFSTEP]
rw [l₁_nil, l₂_nil]
[GOAL]
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))
[PROOFSTEP]
simp only [mapIdx.go, Array.toList_eq, Array.toArray_data]
[GOAL]
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))
[PROOFSTEP]
cases' l₁ with head tail
[GOAL]
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 (mapIdx.go f [] arr))
[PROOFSTEP]
simp only [mapIdx.go]
[GOAL]
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 (head :: tail ++ l₂) arr = mapIdx.go f l₂ (toArray (mapIdx.go f (head :: tail) arr))
[PROOFSTEP]
simp only [mapIdx.go]
[GOAL]
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))
[PROOFSTEP]
simp only [nil_append, Array.toList_eq, Array.toArray_data]
[GOAL]
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))))
[PROOFSTEP]
simp only [List.append_eq]
[GOAL]
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))))
[PROOFSTEP]
rw [ih]
[GOAL]
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
[PROOFSTEP]
simp only [cons_append, length_cons, length_append, Nat.succ.injEq] at h 
[GOAL]
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
[PROOFSTEP]
simp only [length_append, h]
  -- Porting note: new theorem.
[GOAL]
α : Type u
β : Type v
⊢ ∀ (f : ℕ → α → β) (l : List α) (arr : Array β), length (mapIdx.go f l arr) = length l + Array.size arr
[PROOFSTEP]
intro f l
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
l : List α
⊢ ∀ (arr : Array β), length (mapIdx.go f l arr) = length l + Array.size arr
[PROOFSTEP]
induction' l with head tail ih
[GOAL]
case nil
α : Type u
β : Type v
f : ℕ → α → β
⊢ ∀ (arr : Array β), length (mapIdx.go f [] arr) = length [] + Array.size arr
[PROOFSTEP]
intro
[GOAL]
case nil
α : Type u
β : Type v
f : ℕ → α → β
arr✝ : Array β
⊢ length (mapIdx.go f [] arr✝) = length [] + Array.size arr✝
[PROOFSTEP]
simp only [mapIdx.go, Array.toList_eq, length_nil, zero_add]
[GOAL]
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
[PROOFSTEP]
intro
[GOAL]
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✝
[PROOFSTEP]
simp only [mapIdx.go]
[GOAL]
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✝
[PROOFSTEP]
rw [ih]
[GOAL]
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✝
[PROOFSTEP]
simp only [Array.size_push, length_cons]
[GOAL]
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✝
[PROOFSTEP]
simp only [Nat.add_succ, add_zero, Nat.add_comm]
  -- Porting note: new theorem.
[GOAL]
α : Type u
β : Type v
⊢ ∀ (f : ℕ → α → β) (l : List α) (e : α), mapIdx f (l ++ [e]) = mapIdx f l ++ [f (length l) e]
[PROOFSTEP]
intros f l e
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ mapIdx f (l ++ [e]) = mapIdx f l ++ [f (length l) e]
[PROOFSTEP]
unfold mapIdx
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ mapIdx.go f (l ++ [e]) #[] = mapIdx.go f l #[] ++ [f (length l) e]
[PROOFSTEP]
rw [mapIdxGo_append f l [e]]
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ mapIdx.go f [e] (toArray (mapIdx.go f l #[])) = mapIdx.go f l #[] ++ [f (length l) e]
[PROOFSTEP]
simp only [mapIdx.go, Array.size_toArray, mapIdxGo_length, length_nil, add_zero, Array.toList_eq, Array.push_data,
  Array.data_toArray]
  -- Porting note: new theorem.
[GOAL]
α : Type u
β : Type v
⊢ ∀ (f : ℕ → α → β) (l : List α), mapIdx f l = List.oldMapIdx f l
[PROOFSTEP]
intro f
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β
⊢ ∀ (l : List α), mapIdx f l = List.oldMapIdx f l
[PROOFSTEP]
apply list_reverse_induction
[GOAL]
case base
α : Type u
β : Type v
f : ℕ → α → β
⊢ mapIdx f [] = List.oldMapIdx f []
[PROOFSTEP]
rfl
[GOAL]
case ind
α : Type u
β : Type v
f : ℕ → α → β
⊢ ∀ (l : List α) (e : α), mapIdx f l = List.oldMapIdx f l → mapIdx f (l ++ [e]) = List.oldMapIdx f (l ++ [e])
[PROOFSTEP]
intro l e h
[GOAL]
case ind
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
h : mapIdx f l = List.oldMapIdx f l
⊢ mapIdx f (l ++ [e]) = List.oldMapIdx f (l ++ [e])
[PROOFSTEP]
rw [List.oldMapIdx_append, mapIdx_append_one, h]
[GOAL]
α : Type u
β : Type v
⊢ ∀ (l : List α) (n : ℕ) (f : ℕ → α → β),
    map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range (length l)) l
[PROOFSTEP]
intro l
[GOAL]
α : Type u
β : Type v
l : List α
⊢ ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range (length l)) l
[PROOFSTEP]
generalize e : l.length = len
[GOAL]
α : Type u
β : Type v
l : List α
len : ℕ
e : length l = len
⊢ ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
[PROOFSTEP]
revert l
[GOAL]
α : Type u
β : Type v
len : ℕ
⊢ ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
[PROOFSTEP]
induction' len with len ih
[GOAL]
case zero
α : Type u
β : Type v
⊢ ∀ (l : List α),
    length l = Nat.zero →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range Nat.zero) l
[PROOFSTEP]
intros l e n f
[GOAL]
case succ
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
⊢ ∀ (l : List α),
    length l = Nat.succ len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range (Nat.succ len)) l
[PROOFSTEP]
intros l e n f
[GOAL]
case zero
α : Type u
β : Type v
l : List α
e : length l = Nat.zero
n : ℕ
f : ℕ → α → β
⊢ map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range Nat.zero) l
[PROOFSTEP]
have : l = [] := by cases l; rfl; contradiction
[GOAL]
α : Type u
β : Type v
l : List α
e : length l = Nat.zero
n : ℕ
f : ℕ → α → β
⊢ l = []
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u
β : Type v
n : ℕ
f : ℕ → α → β
e : length [] = Nat.zero
⊢ [] = []
case cons
α : Type u
β : Type v
n : ℕ
f : ℕ → α → β
head✝ : α
tail✝ : List α
e : length (head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
n : ℕ
f : ℕ → α → β
head✝ : α
tail✝ : List α
e : length (head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
contradiction
[GOAL]
case zero
α : Type u
β : Type v
l : List α
e : length l = Nat.zero
n : ℕ
f : ℕ → α → β
this : l = []
⊢ map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range Nat.zero) l
[PROOFSTEP]
rw [this]
[GOAL]
case zero
α : Type u
β : Type v
l : List α
e : length l = Nat.zero
n : ℕ
f : ℕ → α → β
this : l = []
⊢ map (uncurry f) (enumFrom n []) = zipWith (fun i => f (i + n)) (range Nat.zero) []
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
l : List α
e : length l = Nat.succ len
n : ℕ
f : ℕ → α → β
⊢ map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range (Nat.succ len)) l
[PROOFSTEP]
cases' l with head tail
[GOAL]
case succ.nil
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
e : length [] = Nat.succ len
⊢ map (uncurry f) (enumFrom n []) = zipWith (fun i => f (i + n)) (range (Nat.succ len)) []
[PROOFSTEP]
contradiction
[GOAL]
case succ.cons
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
⊢ map (uncurry f) (enumFrom n (head :: tail)) = zipWith (fun i => f (i + n)) (range (Nat.succ len)) (head :: tail)
[PROOFSTEP]
simp only [map, uncurry_apply_pair, range_succ_eq_map, zipWith, zero_add, zipWith_map_left]
[GOAL]
case succ.cons
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
⊢ f n head :: map (uncurry f) (enumFrom (n + 1) tail) =
    f n head :: zipWith ((fun i => f (i + n)) ∘ Nat.succ) (range len) tail
[PROOFSTEP]
rw [ih]
[GOAL]
case succ.cons
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
⊢ f n head :: zipWith (fun i => f (i + (n + 1))) (range len) tail =
    f n head :: zipWith ((fun i => f (i + n)) ∘ Nat.succ) (range len) tail
case succ.cons.e
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
⊢ length tail = len
[PROOFSTEP]
suffices : (fun i ↦ f (i + (n + 1))) = ((fun i ↦ f (i + n)) ∘ Nat.succ)
[GOAL]
case succ.cons
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
this : (fun i => f (i + (n + 1))) = (fun i => f (i + n)) ∘ Nat.succ
⊢ f n head :: zipWith (fun i => f (i + (n + 1))) (range len) tail =
    f n head :: zipWith ((fun i => f (i + n)) ∘ Nat.succ) (range len) tail
case this
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
⊢ (fun i => f (i + (n + 1))) = (fun i => f (i + n)) ∘ Nat.succ
case succ.cons.e
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
⊢ length tail = len
[PROOFSTEP]
rw [this]
[GOAL]
case this
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
⊢ (fun i => f (i + (n + 1))) = (fun i => f (i + n)) ∘ Nat.succ
case succ.cons.e
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
⊢ length tail = len
[PROOFSTEP]
funext n' a
[GOAL]
case this.h.h
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
n' : ℕ
a : α
⊢ f (n' + (n + 1)) a = ((fun i => f (i + n)) ∘ Nat.succ) n' a
case succ.cons.e
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
⊢ length tail = len
[PROOFSTEP]
simp only [comp, Nat.add_assoc, Nat.add_comm, Nat.add_succ]
[GOAL]
case succ.cons.e
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length (head :: tail) = Nat.succ len
⊢ length tail = len
[PROOFSTEP]
simp only [length_cons, Nat.succ.injEq] at e 
[GOAL]
case succ.cons.e
α : Type u
β : Type v
len : ℕ
ih :
  ∀ (l : List α),
    length l = len →
      ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range len) l
n : ℕ
f : ℕ → α → β
head : α
tail : List α
e : length tail = len
⊢ length tail = len
[PROOFSTEP]
exact e
[GOAL]
α : Type u
β : Type v
l : List α
f : ℕ → α → β
⊢ mapIdx f l = map (uncurry f) (enum l)
[PROOFSTEP]
rw [List.new_def_eq_old_def]
[GOAL]
α : Type u
β : Type v
l : List α
f : ℕ → α → β
⊢ List.oldMapIdx f l = map (uncurry f) (enum l)
[PROOFSTEP]
induction' l with hd tl hl generalizing f
[GOAL]
case nil
α : Type u
β : Type v
f✝ f : ℕ → α → β
⊢ List.oldMapIdx f [] = map (uncurry f) (enum [])
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
f✝ : ℕ → α → β
hd : α
tl : List α
hl : ∀ (f : ℕ → α → β), List.oldMapIdx f tl = map (uncurry f) (enum tl)
f : ℕ → α → β
⊢ List.oldMapIdx f (hd :: tl) = map (uncurry f) (enum (hd :: tl))
[PROOFSTEP]
rw [List.oldMapIdx, List.oldMapIdxCore, List.oldMapIdxCore_eq, hl]
[GOAL]
case cons
α : Type u
β : Type v
f✝ : ℕ → α → β
hd : α
tl : List α
hl : ∀ (f : ℕ → α → β), List.oldMapIdx f tl = map (uncurry f) (enum tl)
f : ℕ → α → β
⊢ f 0 hd :: map (uncurry fun i a => f (i + (0 + 1)) a) (enum tl) = map (uncurry f) (enum (hd :: tl))
[PROOFSTEP]
simp [enum_eq_zip_range, map_uncurry_zip_eq_zipWith]
[GOAL]
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
l : List α
f : ℕ → α → β
a : α
⊢ mapIdx f (a :: l) = f 0 a :: mapIdx (fun i => f (i + 1)) l
[PROOFSTEP]
simp [mapIdx_eq_enum_map, enum_eq_zip_range, map_uncurry_zip_eq_zipWith, range_succ_eq_map, zipWith_map_left]
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
K L : List α
f : ℕ → α → β
⊢ mapIdx f (K ++ L) = mapIdx f K ++ mapIdx (fun i a => f (i + length K) a) L
[PROOFSTEP]
induction' K with a J IH generalizing f
[GOAL]
case nil
α✝ : Type u
β : Type v
α : Type u_1
L : List α
f✝ f : ℕ → α → β
⊢ mapIdx f ([] ++ L) = mapIdx f [] ++ mapIdx (fun i a => f (i + length []) a) L
[PROOFSTEP]
rfl
[GOAL]
case cons
α✝ : Type u
β : Type v
α : Type u_1
L : List α
f✝ : ℕ → α → β
a : α
J : List α
IH : ∀ (f : ℕ → α → β), mapIdx f (J ++ L) = mapIdx f J ++ mapIdx (fun i a => f (i + length J) a) L
f : ℕ → α → β
⊢ mapIdx f (a :: J ++ L) = mapIdx f (a :: J) ++ mapIdx (fun i a_1 => f (i + length (a :: J)) a_1) L
[PROOFSTEP]
simp [IH fun i ↦ f (i + 1), add_assoc]
[GOAL]
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
l : List α
f : ℕ → α → β
⊢ length (mapIdx f l) = length l
[PROOFSTEP]
induction' l with hd tl IH generalizing f
[GOAL]
case nil
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
f✝ f : ℕ → α → β
⊢ length (mapIdx f []) = length []
[PROOFSTEP]
rfl
[GOAL]
case cons
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
f✝ : ℕ → α → β
hd : α
tl : List α
IH : ∀ (f : ℕ → α → β), length (mapIdx f tl) = length tl
f : ℕ → α → β
⊢ length (mapIdx f (hd :: tl)) = length (hd :: tl)
[PROOFSTEP]
simp [IH]
[GOAL]
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
l : List α
f : ℕ → α → β
i : ℕ
h : i < length l
h' : optParam (i < length (mapIdx f l)) (_ : i < length (mapIdx f l))
⊢ nthLe (mapIdx f l) i h' = f i (nthLe l i h)
[PROOFSTEP]
simp [mapIdx_eq_enum_map, enum_eq_zip_range]
[GOAL]
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
l : List α
f : ℕ → α → β
⊢ mapIdx f l = ofFn fun i => f (↑i) (get l i)
[PROOFSTEP]
induction' l with hd tl IH generalizing f
[GOAL]
case nil
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
f✝ f : ℕ → α → β
⊢ mapIdx f [] = ofFn fun i => f (↑i) (get [] i)
[PROOFSTEP]
rfl
[GOAL]
case cons
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
f✝ : ℕ → α → β
hd : α
tl : List α
IH : ∀ (f : ℕ → α → β), mapIdx f tl = ofFn fun i => f (↑i) (get tl i)
f : ℕ → α → β
⊢ mapIdx f (hd :: tl) = ofFn fun i => f (↑i) (get (hd :: tl) i)
[PROOFSTEP]
simp [IH]
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β → β
b : β
as : List α
start : ℕ
⊢ foldrIdx f b as start = foldrIdxSpec f b as start
[PROOFSTEP]
induction as generalizing start
[GOAL]
case nil
α : Type u
β : Type v
f : ℕ → α → β → β
b : β
start : ℕ
⊢ foldrIdx f b [] start = foldrIdxSpec f b [] start
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
f : ℕ → α → β → β
b : β
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (start : ℕ), foldrIdx f b tail✝ start = foldrIdxSpec f b tail✝ start
start : ℕ
⊢ foldrIdx f b (head✝ :: tail✝) start = foldrIdxSpec f b (head✝ :: tail✝) start
[PROOFSTEP]
simp only [foldrIdx, foldrIdxSpec_cons, *]
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β → β
b : β
as : List α
⊢ foldrIdx f b as = foldr (uncurry f) b (enum as)
[PROOFSTEP]
simp only [foldrIdx, foldrIdxSpec, foldrIdx_eq_foldrIdxSpec, enum]
[GOAL]
α : Type u
β : Type v
p : α → Prop
inst✝ : DecidablePred p
as : List α
⊢ indexesValues (fun b => decide (p b)) as = filter ((fun b => decide (p b)) ∘ Prod.snd) (enum as)
[PROOFSTEP]
simp [indexesValues, foldrIdx_eq_foldr_enum, uncurry, filter_eq_foldr]
[GOAL]
α : Type u
β : Type v
p : α → Prop
inst✝ : DecidablePred p
as : List α
⊢ findIdxs (fun b => decide (p b)) as = map Prod.fst (indexesValues (fun b => decide (p b)) as)
[PROOFSTEP]
simp only [indexesValues_eq_filter_enum, map_filter_eq_foldr, findIdxs, uncurry, foldrIdx_eq_foldr_enum,
  decide_eq_true_eq, comp_apply, Bool.cond_decide]
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β → α
a : α
bs : List β
start : ℕ
⊢ foldlIdx f a bs start = foldlIdxSpec f a bs start
[PROOFSTEP]
induction bs generalizing start a
[GOAL]
case nil
α : Type u
β : Type v
f : ℕ → α → β → α
a : α
start : ℕ
⊢ foldlIdx f a [] start = foldlIdxSpec f a [] start
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
f : ℕ → α → β → α
head✝ : β
tail✝ : List β
tail_ih✝ : ∀ (a : α) (start : ℕ), foldlIdx f a tail✝ start = foldlIdxSpec f a tail✝ start
a : α
start : ℕ
⊢ foldlIdx f a (head✝ :: tail✝) start = foldlIdxSpec f a (head✝ :: tail✝) start
[PROOFSTEP]
simp [foldlIdxSpec, *]
[GOAL]
α : Type u
β : Type v
f : ℕ → α → β → α
a : α
bs : List β
⊢ foldlIdx f a bs = foldl (fun a p => f p.fst a p.snd) a (enum bs)
[PROOFSTEP]
simp only [foldlIdx, foldlIdxSpec, foldlIdx_eq_foldlIdxSpec, enum]
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β : Type u
f : ℕ → α → β → m β
b : β
as : List α
inst✝ : LawfulMonad m
⊢ foldrIdxM f b as = foldrM (uncurry f) b (enum as)
[PROOFSTEP]
simp only [foldrIdxM, foldrM_eq_foldr, foldrIdx_eq_foldr_enum, uncurry]
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → β → α → m β
b : β
as : List α
⊢ foldlIdxM f b as = List.foldlM (fun b p => f p.fst b p.snd) b (enum as)
[PROOFSTEP]
rw [foldlIdxM, foldlM_eq_foldl, foldlIdx_eq_foldl_enum]
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
⊢ mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
[PROOFSTEP]
generalize e : as.length = len
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
len : ℕ
e : length as = len
⊢ mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
[PROOFSTEP]
revert as arr
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
⊢ ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
[PROOFSTEP]
induction' len with len ih
[GOAL]
case zero
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
⊢ ∀ (arr : Array β) (as : List α),
    length as = Nat.zero →
      mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
[PROOFSTEP]
intro arr as h
[GOAL]
case succ
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
⊢ ∀ (arr : Array β) (as : List α),
    length as = Nat.succ len →
      mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
[PROOFSTEP]
intro arr as h
[GOAL]
case zero
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
h : length as = Nat.zero
⊢ mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
[PROOFSTEP]
have : as = [] := by cases as; rfl; contradiction
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
h : length as = Nat.zero
⊢ as = []
[PROOFSTEP]
cases as
[GOAL]
case nil
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
h : length [] = Nat.zero
⊢ [] = []
case cons
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
rfl
[GOAL]
case cons
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
head✝ : α
tail✝ : List α
h : length (head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
[PROOFSTEP]
contradiction
[GOAL]
case zero
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
arr : Array β
as : List α
h : length as = Nat.zero
this : as = []
⊢ mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
[PROOFSTEP]
simp only [this, mapIdxM.go, mapIdxMAuxSpec, List.traverse, map_pure, append_nil]
[GOAL]
case succ
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
h : length as = Nat.succ len
⊢ mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
[PROOFSTEP]
match as with
| nil => contradiction
| cons head tail =>
  simp only [length_cons, Nat.succ.injEq] at h 
  simp only [mapIdxM.go, mapIdxMAuxSpec_cons, map_eq_pure_bind, seq_eq_bind_map, LawfulMonad.bind_assoc, pure_bind]
  congr
  conv => {lhs; intro x; rw [ih _ _ h]; }
  funext x
  simp only [Array.toList_eq, Array.push_data, append_assoc, singleton_append, Array.size_push, map_eq_pure_bind]
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
h : length [] = Nat.succ len
⊢ mapIdxM.go f [] arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) []
[PROOFSTEP]
contradiction
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length (head :: tail) = Nat.succ len
⊢ mapIdxM.go f (head :: tail) arr =
    (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) (head :: tail)
[PROOFSTEP]
simp only [length_cons, Nat.succ.injEq] at h 
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
⊢ mapIdxM.go f (head :: tail) arr =
    (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) (head :: tail)
[PROOFSTEP]
simp only [mapIdxM.go, mapIdxMAuxSpec_cons, map_eq_pure_bind, seq_eq_bind_map, LawfulMonad.bind_assoc, pure_bind]
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
⊢ (do
      let __do_lift ← f (Array.size arr) head
      mapIdxM.go f tail (Array.push arr __do_lift)) =
    do
    let x ← f (Array.size arr) head
    let x_1 ← mapIdxMAuxSpec f (Array.size arr + 1) tail
    pure (Array.toList arr ++ x :: x_1)
[PROOFSTEP]
congr
[GOAL]
case e_a
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
⊢ (fun __do_lift => mapIdxM.go f tail (Array.push arr __do_lift)) = fun x => do
    let x_1 ← mapIdxMAuxSpec f (Array.size arr + 1) tail
    pure (Array.toList arr ++ x :: x_1)
[PROOFSTEP]
conv => {lhs; intro x; rw [ih _ _ h]; }
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
| (fun __do_lift => mapIdxM.go f tail (Array.push arr __do_lift)) = fun x => do
    let x_1 ← mapIdxMAuxSpec f (Array.size arr + 1) tail
    pure (Array.toList arr ++ x :: x_1)
[PROOFSTEP]
{lhs; intro x; rw [ih _ _ h]; }
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
| (fun __do_lift => mapIdxM.go f tail (Array.push arr __do_lift)) = fun x => do
    let x_1 ← mapIdxMAuxSpec f (Array.size arr + 1) tail
    pure (Array.toList arr ++ x :: x_1)
[PROOFSTEP]
{lhs; intro x; rw [ih _ _ h]; }
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
| (fun __do_lift => mapIdxM.go f tail (Array.push arr __do_lift)) = fun x => do
    let x_1 ← mapIdxMAuxSpec f (Array.size arr + 1) tail
    pure (Array.toList arr ++ x :: x_1)
[PROOFSTEP]
lhs
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
| fun __do_lift => mapIdxM.go f tail (Array.push arr __do_lift)
[PROOFSTEP]
intro x
[GOAL]
case h
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
x : β
| mapIdxM.go f tail (Array.push arr x)
[PROOFSTEP]
rw [ih _ _ h]
[GOAL]
case e_a
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
⊢ (fun x =>
      (fun x_1 => Array.toList (Array.push arr x) ++ x_1) <$> mapIdxMAuxSpec f (Array.size (Array.push arr x)) tail) =
    fun x => do
    let x_1 ← mapIdxMAuxSpec f (Array.size arr + 1) tail
    pure (Array.toList arr ++ x :: x_1)
[PROOFSTEP]
funext x
[GOAL]
case e_a.h
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
len : ℕ
ih :
  ∀ (arr : Array β) (as : List α),
    length as = len → mapIdxM.go f as arr = (fun x => Array.toList arr ++ x) <$> mapIdxMAuxSpec f (Array.size arr) as
arr : Array β
as : List α
head : α
tail : List α
h : length tail = len
x : β
⊢ (fun x_1 => Array.toList (Array.push arr x) ++ x_1) <$> mapIdxMAuxSpec f (Array.size (Array.push arr x)) tail = do
    let x_1 ← mapIdxMAuxSpec f (Array.size arr + 1) tail
    pure (Array.toList arr ++ x :: x_1)
[PROOFSTEP]
simp only [Array.toList_eq, Array.push_data, append_assoc, singleton_append, Array.size_push, map_eq_pure_bind]
[GOAL]
α✝ : Type u
β✝ : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : ℕ → α → m β
as : List α
⊢ mapIdxM as f = List.traverse (uncurry f) (enum as)
[PROOFSTEP]
simp only [mapIdxM, mapIdxMGo_eq_mapIdxMAuxSpec, Array.toList_eq, Array.data_toArray, nil_append, mapIdxMAuxSpec,
  Array.size_toArray, length_nil, id_map', enum]
[GOAL]
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
as : List α
arr : Array PUnit
⊢ mapIdxMAux' f (Array.size arr) as = SeqRight.seqRight (mapIdxM.go f as arr) fun x => pure PUnit.unit
[PROOFSTEP]
revert arr
[GOAL]
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
as : List α
⊢ ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) as = SeqRight.seqRight (mapIdxM.go f as arr) fun x => pure PUnit.unit
[PROOFSTEP]
induction' as with head tail ih
[GOAL]
case nil
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
⊢ ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) [] = SeqRight.seqRight (mapIdxM.go f [] arr) fun x => pure PUnit.unit
[PROOFSTEP]
intro arr
[GOAL]
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
⊢ ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) (head :: tail) =
      SeqRight.seqRight (mapIdxM.go f (head :: tail) arr) fun x => pure PUnit.unit
[PROOFSTEP]
intro arr
[GOAL]
case nil
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
arr : Array PUnit
⊢ mapIdxMAux' f (Array.size arr) [] = SeqRight.seqRight (mapIdxM.go f [] arr) fun x => pure PUnit.unit
[PROOFSTEP]
simp only [mapIdxMAux', mapIdxM.go, seqRight_eq, map_pure, seq_pure]
[GOAL]
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
⊢ mapIdxMAux' f (Array.size arr) (head :: tail) =
    SeqRight.seqRight (mapIdxM.go f (head :: tail) arr) fun x => pure PUnit.unit
[PROOFSTEP]
simp only [mapIdxMAux', seqRight_eq, map_eq_pure_bind, seq_eq_bind, bind_pure_unit, LawfulMonad.bind_assoc, pure_bind,
  mapIdxM.go, seq_pure]
[GOAL]
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
⊢ (do
      f (Array.size arr) head
      mapIdxMAux' f (Array.size arr + 1) tail) =
    do
    let x ← f (Array.size arr) head
    let x ← mapIdxM.go f tail (Array.push arr x)
    pure (const (List PUnit) id x PUnit.unit)
[PROOFSTEP]
generalize (f (Array.size arr) head) = head
[GOAL]
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
head : m PUnit
⊢ (do
      head
      mapIdxMAux' f (Array.size arr + 1) tail) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (Array.push arr x)
    pure (const (List PUnit) id x PUnit.unit)
[PROOFSTEP]
let arr_1 := arr.push ⟨⟩
[GOAL]
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
head : m PUnit
arr_1 : Array PUnit := Array.push arr PUnit.unit
⊢ (do
      head
      mapIdxMAux' f (Array.size arr + 1) tail) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (Array.push arr x)
    pure (const (List PUnit) id x PUnit.unit)
[PROOFSTEP]
have : arr_1.size = arr.size + 1 := Array.size_push arr ⟨⟩
[GOAL]
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
head : m PUnit
arr_1 : Array PUnit := Array.push arr PUnit.unit
this : Array.size arr_1 = Array.size arr + 1
⊢ (do
      head
      mapIdxMAux' f (Array.size arr + 1) tail) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (Array.push arr x)
    pure (const (List PUnit) id x PUnit.unit)
[PROOFSTEP]
rw [← this, ih arr_1]
[GOAL]
case cons
α✝ : Type u
β : Type v
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head✝ : α
tail : List α
ih :
  ∀ (arr : Array PUnit),
    mapIdxMAux' f (Array.size arr) tail = SeqRight.seqRight (mapIdxM.go f tail arr) fun x => pure PUnit.unit
arr : Array PUnit
head : m PUnit
arr_1 : Array PUnit := Array.push arr PUnit.unit
this : Array.size arr_1 = Array.size arr + 1
⊢ (do
      head
      SeqRight.seqRight (mapIdxM.go f tail arr_1) fun x => pure PUnit.unit) =
    do
    let x ← head
    let x ← mapIdxM.go f tail (Array.push arr x)
    pure (const (List PUnit) id x PUnit.unit)
[PROOFSTEP]
simp only [seqRight_eq, map_eq_pure_bind, seq_pure, LawfulMonad.bind_assoc, pure_bind]
