タクティクひとつならbyも要らない？

def f5 (n : Nat) : Nat := by
  cases n 
  exact 3 -- zero case
  exact 7 -- succ case
#eval f5 0 --> 3
#eval f5 1 --> 7
example : f5 0 = 3 := rfl -- by も要らない！？
example : f5 5 = 7 := rfl
example : f5 2 = 7 := by
  exact Eq.refl 7