【Lean4】change

change

現在の目標を、定義上等しい別の目標へ変更する

Plaintext

example :
    myFrobeniusFun K p 1 = 1 := by
  change 1 ^ p = 1
  exact one_pow p

example :
    myFrobeniusFun K p 1 = 1 := by
  change 1 ^ p = 1
  exact one_pow p