case nil
ι : Type ?u.448212
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ ys✝ : List α
n✝ : ℕ
ys : List α
n : ℕ
⊢ enumFrom n ([] ++ ys) = enumFrom n [] ++ enumFrom (n + length []) ys

case cons
ι : Type ?u.448212
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ ys✝ : List α
n✝ : ℕ
x : α
xs : List α
IH : ∀ (ys : List α) (n : ℕ), enumFrom n (xs ++ ys) = enumFrom n xs ++ enumFrom (n + length xs) ys
ys : List α
n : ℕ
⊢ enumFrom n (x :: xs ++ ys) = enumFrom n (x :: xs) ++ enumFrom (n + length (x :: xs)) ys
ι : Type ?u.448212
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ xs ys : List α
n : ℕ
⊢ enumFrom n (xs ++ ys) = enumFrom n xs ++ enumFrom (n + length xs) ys
induction' xs with x xs IH generalizing ys n
no goals
case nil
ι : Type ?u.448212
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ ys✝ : List α
n✝ : ℕ
ys : List α
n : ℕ
⊢ enumFrom n ([] ++ ys) = enumFrom n [] ++ enumFrom (n + length []) ys
simp
no goals
case cons
ι : Type ?u.448212
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ ys✝ : List α
n✝ : ℕ
x : α
xs : List α
IH : ∀ (ys : List α) (n : ℕ), enumFrom n (xs ++ ys) = enumFrom n xs ++ enumFrom (n + length xs) ys
ys : List α
n : ℕ
⊢ enumFrom n (x :: xs ++ ys) = enumFrom n (x :: xs) ++ enumFrom (n + length (x :: xs)) ys
rw [cons_append, enumFrom_cons, IH, ← cons_append, ← enumFrom_cons, length, add_right_comm,
  add_assoc]