no goals
f g : CircleDeg1Lift
⊢ τ (f ^ 0) = ↑0 * τ f
simp
no goals
f g : CircleDeg1Lift
n : ℕ
⊢ τ (f ^ (n + 1)) = ↑(n + 1) * τ f
rw [pow_succ', translationNumber_mul_of_commute (Commute.pow_self f n),
  translationNumber_pow n, Nat.cast_add_one, add_mul, one_mul]