unfold definition in goal?

Stream: new members

[Chris M]

I have the following goal state:

1 goal
fg: ℝ → ℝ
ab: ℝ
hfa: fn_lb f a
hgb: fn_lb g b
⊢ fn_lb (λ (x : ℝ), f x + g x) (a + b)

Is there a tactic for unfolding the definition offn_lb in this goal state?

[Chris M]

Neither simp nor dsimp work.

[Jalex Stark]

unfold or dunfold or delta?

[Chris M]

None of those do anything

[Jalex Stark]

can you post a #mwe?

[Chris M]

import data.real.basic
import tactic

example (hfa : fn_lb f a) (hgb : fn_lb g b) :
  fn_lb (λ x, f x + g x) (a + b) :=
begin
  dunfold,
end

[Jalex Stark]

dunfold fn_lb

[Jalex Stark]

you wouldn't want a tactic that says "unfold every definition you see and then show me the result"

[Chris M]

right

[Chris M]

So this unfolds the definition in the conclusion, but not in the assumptions. how do I unfold the assumptinos?

[Jalex Stark]

dunfold fn_lb at hfa or dunfold fn_lb at *

[Chris M]

great :)

[Jalex Stark]

all of this should be in the docs, see e.g. tactic#unfold

[Chris M]

Ok thanks, I'll look there next time