no goals
α : Type u
β : Type v
γ : Type w
n : Nat
r : List Nat
⊢ iotaTR.go n r = reverse r ++ iota n
induction n generalizing r with
| zero => simp [iota, iotaTR.go]
| succ n ih => simp [iota, iotaTR.go, ih, append_assoc]
no goals
case zero
α : Type u
β : Type v
γ : Type w
r : List Nat
⊢ iotaTR.go Nat.zero r = reverse r ++ iota Nat.zero
simp [iota, iotaTR.go]
no goals
case succ
α : Type u
β : Type v
γ : Type w
n : Nat
ih : ∀ (r : List Nat), iotaTR.go n r = reverse r ++ iota n
r : List Nat
⊢ iotaTR.go (Nat.succ n) r = reverse r ++ iota (Nat.succ n)
simp [iota, iotaTR.go, ih, append_assoc]
no goals
α : Type u
β : Type v
γ : Type w
aux : ∀ (n : Nat) (r : List Nat), iotaTR.go n r = reverse r ++ iota n
n : Nat
⊢ iota n = iotaTR n
simp [iotaTR, aux]