昨日の関数合成はなんか違ったかも……．でもよくわかってない．

import Mathlib.Tactic
open Nat

@[simp]
def fun_pow {α : Type u} (f : α → α) : (n : Nat) → (α → α)
  | 0 => id
  | succ n => (fun_pow f n) ∘ f

instance {α : Type u} : HPow (α → α) (Nat) (α → α) where
  hPow := fun_pow

def f : (Fin 2) → (Fin 2)
  | 0 => 1
  | 1 => 0

theorem a {α : Type u} (g : α → α) : g^(0) = id := by rfl
theorem aa : f^(0) = id := by
  rfl

最後のrflが通らない．simpすると1 = idとかに簡略化されてしまっているらしい．何だろう．うーむ．最初のimportがないと動くような．