_aux_Mathlib_Topology_Defs_Filter___delab_app_Topology_nhdsNE_1

Lean4
/-- Pretty printer defined by `notation3` command. -/
@[scoped delab✝ app.nhdsWithin]
public meta def _aux_Mathlib_Topology_Defs_Filter___delab_app_Topology_nhdsNE_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✝ · `HasCompl.compl))
                        (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Set)) pure✝))
                      pure✝)
                    (matchApp✝
                      (matchApp✝
                        (matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Singleton.singleton)) pure✝)
                          (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Set)) pure✝))
                        pure✝)
                      (matchVar✝ `x))) >=>
                pure✝)
              MatchState.empty✝ >>=
            fun s✝ => MatchState.delabVar✝ s✝ `x (some✝ e✝) >>= fun x => withHeadRefIfTagAppFns✝ `(𝓝[≠] $x))
Похожие утверждения