_aux_Mathlib_Topology_Defs_Filter___delab_app_Topology_nhdsGE_1

Lean4

/-- Pretty printer defined by `notation3` command. -/
@[scoped delab✝ app.nhdsWithin]
public meta def _aux_Mathlib_Topology_Defs_Filter___delab_app_Topology_nhdsGE_1 : Delab✝ :=
  whenPPOption✝ getPPNotation✝ <|
    whenNotPPOption✝ getPPExplicit✝ <|
      withOverApp✝ 4
        (getExpr✝ >>= fun e✝ =>
          (matchApp✝
                  (matchApp✝ (matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `nhdsWithin)) pure✝) pure✝)
                    (matchVar✝ `x))
                  (matchApp✝ (matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Set.Ici)) pure✝) pure✝)
                    (matchVar✝ `x)) >=>
                pure✝)
              MatchState.empty✝ >>=
            fun s✝ => MatchState.delabVar✝ s✝ `x (some✝ e✝) >>= fun x => withHeadRefIfTagAppFns✝ `(𝓝[≥] $x))

Похожие утверждения