How to "open a definition" of a function

Stream: new members

[Michael Novak]

Let's say I defined some function f using def and then I want to prove some theorem which is a property of f and I managed to prove this property for the definition of this function, but in the goal statement the name f appears and not the definition. How can I reach the goal? I tried using dsimp [f], but it doesn't work. As a silly example (not the actual thing I'm working on):

def f : ℝ → ℝ := fun x ↦ 3*x

theorem test (h : Continuous (fun (x : ℝ) ↦  3*x)) : Continuous f := sorry

How would you usually deal with this?

[Rémy Degenne]

unfold f

[Michael Novak]

Thank you very much! The funny thing is that I also forgot this natural English word - to unfold a definition, that's why I wrote "open" a definition in the title.

[Jakub Nowak]

dsimp will only unfold the definition when it has its argument applied:

def f : Nat → Nat := fun x ↦ x + 1

example : f = sorry := by
  dsimp [f]
  -- ⊢ f = sorry

example : f y = sorry := by
  dsimp [f]
  -- ⊢ y + 1 = sorry

[Ruben Van de Velde]

def f : Nat → Nat := fun x ↦ x + 1

example : f = sorry := by
  dsimp +unfoldPartialApp [f]
  -- ⊢ (fun x => x + 1) = sorry