fun_prop fails to prove given assumption

Stream: mathlib4

[Bhavik Mehta]

Here's my example:

import Mathlib

example {y : ℝ} (hy₁ : -1 < y) (hy₂ : y < 1) :
    DifferentiableAt ℝ (fun x ↦ (1 + x) / (1 - x)) y := by
  have h : 1 - y ≠ 0 := by grind
  fun_prop

I added h after seeing the error message reported by fun_prop, but it still struggles.
What's going on here? How can I make fun_prop useful in cases like this?

[Michael Rothgang]

Does fun_prop (discharger := assumption) work?

[Bhavik Mehta]

It does!