case intro
α : Type u_1
f : α → α
hf : Involutive f
m : ℕ
⊢ f^[2 * m + 1] = f
α : Type u_1
f : α → α
n : ℕ
hf : Involutive f
hn : Odd n
⊢ f^[n] = f
rcases hn with ⟨m, rfl⟩
no goals
case intro
α : Type u_1
f : α → α
hf : Involutive f
m : ℕ
⊢ f^[2 * m + 1] = f
rw [iterate_add, hf.iterate_two_mul, comp.left_id, iterate_one]