Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.DFunLike.coe]
public meta def
«_aux_Mathlib_AlgebraicGeometry_Gluing___delab_app__private_Mathlib_AlgebraicGeometry_Gluing_0_AlgebraicGeometry_Scheme_IsLocallyDirected_term↓__1» :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 6
(getExpr✝ >>= fun e✝ =>
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `DFunLike.coe))
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Equiv))
(matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Shrink)) pure✝) pure✝))
pure✝))
(matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Shrink)) pure✝) pure✝))
(matchLambda✝ (matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Shrink)) pure✝) pure✝)
(fun n✝ => pure✝¹)))
pure✝)
(matchApp✝
(matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Equiv.symm)) pure✝)
(matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Shrink)) pure✝) pure✝))
(matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `equivShrink)) pure✝) pure✝)))
(matchVar✝ `j) >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ => MatchState.delabVar✝ s✝ `j (some✝ e✝) >>= fun j => withHeadRefIfTagAppFns✝ `(↓$j))
