∀ {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} (f : F) [inst : FunLike F UpperHalfPlane ℂ] {k : ℤ}
  [SlashInvariantFormClass F 𝒢 k] (τ : UpperHalfPlane) (h h' : ↥ℋ),
  h ≈ h' → (fun g => SlashAction.map k (↑g)⁻¹ (⇑f) τ) h = (fun g => SlashAction.map k (↑g)⁻¹ (⇑f) τ) h'