【Lean4】congrArg

congrArg

等しいものに同じ関数を適用しても等しい、という事実を使う

Plaintext

example (a b : α) (h : a = b) (f : α → β) :
    f a = f b := by
  exact congrArg f h

example (a b : α) (h : a = b) (f : α → β) :
    f a = f b := by
  exact congrArg f h