Making an issue to record a comment raised by @j-loreaux during the reviewing of my PR #36895 (about the SL2R action on the upper half-plane).

It seems fun_prop doesn't work as well as one might like on goals about continuity of matrix-valued functions. It would be nice if goals like

∀ (g : SL(2, ℝ)) (τ : ℍ), ContinuousAt 
  (fun ⟨h, z⟩ ↦ (h 0 0 * (z : ℂ) + h 0 1) / (h 1 0 * z + h 1 1)) (g, τ)

could be handled automatically by the tactic.