case intro
α : Type u_1
f : α → α
hf : Involutive f
m : ℕ
⊢ f^[m + m] = id
α : Type u_1
f : α → α
n : ℕ
hf : Involutive f
hn : Even n
⊢ f^[n] = id
rcases hn with ⟨m, rfl⟩
no goals
case intro
α : Type u_1
f : α → α
hf : Involutive f
m : ℕ
⊢ f^[m + m] = id
rw [← two_mul, hf.iterate_two_mul]