case nil
ι : Type ?u.450424
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n : ℕ
f : α → β
⊢ enumFrom n (map f []) = map (Prod.map id f) (enumFrom n [])

case cons
ι : Type ?u.450424
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n : ℕ
f : α → β
hd : α
tl : List α
IH : enumFrom n (map f tl) = map (Prod.map id f) (enumFrom n tl)
⊢ enumFrom n (map f (hd :: tl)) = map (Prod.map id f) (enumFrom n (hd :: tl))
ι : Type ?u.450424
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n : ℕ
l : List α
f : α → β
⊢ enumFrom n (map f l) = map (Prod.map id f) (enumFrom n l)
induction' l with hd tl IH
no goals
case nil
ι : Type ?u.450424
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n : ℕ
f : α → β
⊢ enumFrom n (map f []) = map (Prod.map id f) (enumFrom n [])
rfl
case cons
ι : Type ?u.450424
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n : ℕ
f : α → β
hd : α
tl : List α
IH : enumFrom n (map f tl) = map (Prod.map id f) (enumFrom n tl)
⊢ (n, f hd) :: map (Prod.map succ id ∘ Prod.map id f) (enumFrom n tl) =
    Prod.map id f (n, hd) :: map (Prod.map id f ∘ Prod.map succ id) (enumFrom n tl)
case cons
ι : Type ?u.450424
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n : ℕ
f : α → β
hd : α
tl : List α
IH : enumFrom n (map f tl) = map (Prod.map id f) (enumFrom n tl)
⊢ enumFrom n (map f (hd :: tl)) = map (Prod.map id f) (enumFrom n (hd :: tl))
rw [map_cons, enumFrom_cons', enumFrom_cons', map_cons, map_map, IH, map_map]
no goals
case cons
ι : Type ?u.450424
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n : ℕ
f : α → β
hd : α
tl : List α
IH : enumFrom n (map f tl) = map (Prod.map id f) (enumFrom n tl)
⊢ (n, f hd) :: map (Prod.map succ id ∘ Prod.map id f) (enumFrom n tl) =
    Prod.map id f (n, hd) :: map (Prod.map id f ∘ Prod.map succ id) (enumFrom n tl)
rfl