Try this: simp only [↓f_eq]