case nil
ι : Type ?u.449078
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n✝ k✝ n k : ℕ
⊢ map (Prod.map (fun x => x + n) id) (enumFrom k []) = enumFrom (n + k) []

case cons
ι : Type ?u.449078
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n✝ k✝ : ℕ
hd : α
tl : List α
IH : ∀ (n k : ℕ), map (Prod.map (fun x => x + n) id) (enumFrom k tl) = enumFrom (n + k) tl
n k : ℕ
⊢ map (Prod.map (fun x => x + n) id) (enumFrom k (hd :: tl)) = enumFrom (n + k) (hd :: tl)
ι : Type ?u.449078
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ l : List α
n k : ℕ
⊢ map (Prod.map (fun x => x + n) id) (enumFrom k l) = enumFrom (n + k) l
induction' l with hd tl IH generalizing n k
no goals
case nil
ι : Type ?u.449078
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n✝ k✝ n k : ℕ
⊢ map (Prod.map (fun x => x + n) id) (enumFrom k []) = enumFrom (n + k) []
simp [enumFrom]
case cons
ι : Type ?u.449078
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n✝ k✝ : ℕ
hd : α
tl : List α
IH : ∀ (n k : ℕ), map (Prod.map (fun x => x + n) id) (enumFrom k tl) = enumFrom (n + k) tl
n k : ℕ
⊢ (k + n, hd) :: map (Prod.map (fun x => x + n) id) (enumFrom (k + 1) tl) = (n + k, hd) :: enumFrom (n + k + 1) tl
case cons
ι : Type ?u.449078
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n✝ k✝ : ℕ
hd : α
tl : List α
IH : ∀ (n k : ℕ), map (Prod.map (fun x => x + n) id) (enumFrom k tl) = enumFrom (n + k) tl
n k : ℕ
⊢ map (Prod.map (fun x => x + n) id) (enumFrom k (hd :: tl)) = enumFrom (n + k) (hd :: tl)
simp only [enumFrom, map, zero_add, Prod.map_mk, id.def, eq_self_iff_true, true_and_iff]
no goals
case cons
ι : Type ?u.449078
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n✝ k✝ : ℕ
hd : α
tl : List α
IH : ∀ (n k : ℕ), map (Prod.map (fun x => x + n) id) (enumFrom k tl) = enumFrom (n + k) tl
n k : ℕ
⊢ (k + n, hd) :: map (Prod.map (fun x => x + n) id) (enumFrom (k + 1) tl) = (n + k, hd) :: enumFrom (n + k + 1) tl
simp [IH, add_comm n k, add_assoc, add_left_comm]