fun_prop use assumptions

Stream: mathlib4

[Alex Meiburg]

I have a goal like

T : ℝ
f : ℝ → ℝ
hi : f (1 / T) ≠ 0
⊢ DifferentiableAt ℝ (fun T => Real.log (f (1 / T))) T

and I try fun_prop, it says that it gets stuck at

Failed to prove necessary assumption `f (1 / T) ≠ 0` when applying theorem `Real.differentiableAt_log`.

Does it not check for local assumptions that would make it work? I thought that was kind of the whole point -- to reduce the conclusion to other terms systematically

[Michael Rothgang]

Quick reply, not at the docs: I think you can use the discharger (or was it disch? please check!) option. Does that help? (I agree that this is non-ideal user experience.)

[Alex Meiburg]

Hmm, yes something like that works. That leaves with the slightly ugly form of things then like

have := hi.2
have := DifferentiableAt_Z_if_ZIntegrable hi
have : T ≠ 0 := left_ne_zero_of_mul_eq_one hβT
fun_prop (disch := assumption)

so where I'm making these several side goals needed and then discharging them by assumption. But, it works!

It looks like there is some fun_prop [foo, bar] syntax that exists, at least it parses and I thought it would be like nlinarith [foo, bar] where I can pass in other facts. But that doesn't seem to be that, and there's little docs on how fun_prop should be used sadly