Theorem: Stream'.corec_succ (ListPowersProblem/StreamLemmas.lean)

State before:
α : Type ?u.5702
σ : Stream' α
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
g : α✝¹ → α✝¹
x : α✝¹
i : ℕ
⊢ corec f g x (i + 1) = corec f g (g x) i
Tactic:
simp only [corec, map, nth, iterate_eq_Nat_iterate, Function.iterate_succ, Function.comp_apply]
State after:
no goals