case h
f g : CircleDeg1Lift
n : ℕ
x : ℝ
⊢ ↑(f ^ (n + 1)) x = (↑f^[n + 1]) x
f g : CircleDeg1Lift
n : ℕ
⊢ ↑(f ^ (n + 1)) = ↑f^[n + 1]
ext x
no goals
case h
f g : CircleDeg1Lift
n : ℕ
x : ℝ
⊢ ↑(f ^ (n + 1)) x = (↑f^[n + 1]) x
simp [coe_pow n, pow_succ']