α : Type u
β : Type v
l : List α
⊢ ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range (length l)) l
α : Type u
β : Type v
⊢ ∀ (l : List α) (n : ℕ) (f : ℕ → α → β),
    map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range (length l)) l
intro l
α : 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
α : Type u
β : Type v
l : List α
⊢ ∀ (n : ℕ) (f : ℕ → α → β), map (uncurry f) (enumFrom n l) = zipWith (fun i => f (i + n)) (range (length l)) l
generalize e : l.length = len
α : 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
α : 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
revert l
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

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
α : 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
induction' len with len ih <;> intros l e n f
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
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
have : l = [] := by cases l; rfl; contradiction
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) []
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
rw [this]
no goals
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) []
rfl
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✝ = []
α : Type u
β : Type v
l : List α
e : length l = Nat.zero
n : ℕ
f : ℕ → α → β
⊢ l = []
cases l
case cons
α : Type u
β : Type v
n : ℕ
f : ℕ → α → β
head✝ : α
tail✝ : List α
e : length (head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
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✝ = []
rfl
no goals
case cons
α : Type u
β : Type v
n : ℕ
f : ℕ → α → β
head✝ : α
tail✝ : List α
e : length (head✝ :: tail✝) = Nat.zero
⊢ head✝ :: tail✝ = []
contradiction
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)) []

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)
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
cases' l with head tail
no goals
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)) []
contradiction
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
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)
simp only [map, uncurry_apply_pair, range_succ_eq_map, zipWith, zero_add, zipWith_map_left]
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
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
rw [ih]
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
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
suffices : (fun i ↦ f (i + (n + 1))) = ((fun i ↦ f (i + n)) ∘ Nat.succ)
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
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
rw [this]
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
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
funext 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
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
simp only [comp, Nat.add_assoc, Nat.add_comm, Nat.add_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 tail = len
⊢ length tail = len
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
simp only [length_cons, Nat.succ.injEq] at e
no goals
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
exact e