Lean4
/-- Pretty printer defined by `notation3` command. -/
@[scoped delab✝ app.CategoryTheory.Functor.obj]
public meta def «_aux_Mathlib_AlgebraicGeometry_Scheme___delab_app_AlgebraicGeometry_termΓ(_,_)_1» : Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 6
(getExpr✝ >>= fun e✝ =>
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `CategoryTheory.Functor.obj))
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Opposite))
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `TopologicalSpace.Opens))
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `TopCat.carrier))
(matchApp✝
(matchApp✝
(matchApp✝
(matchExpr✝ (Expr.isConstOf✝ · `AlgebraicGeometry.PresheafedSpace.carrier))
(matchExpr✝ (Expr.isConstOf✝ · `CommRingCat)))
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝
(matchExpr✝
(Expr.isConstOf✝ · `AlgebraicGeometry.SheafedSpace.toPresheafedSpace))
(matchExpr✝ (Expr.isConstOf✝ · `CommRingCat)))
pure✝)
(matchApp✝
(matchExpr✝
(Expr.isConstOf✝ · `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace))
(matchApp✝
(matchExpr✝
(Expr.isConstOf✝ · `AlgebraicGeometry.Scheme.toLocallyRingedSpace))
(matchVar✝ `X)))))))
pure✝)))
pure✝)
(matchExpr✝ (Expr.isConstOf✝ · `CommRingCat)))
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `AlgebraicGeometry.PresheafedSpace.presheaf))
(matchExpr✝ (Expr.isConstOf✝ · `CommRingCat)))
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `AlgebraicGeometry.SheafedSpace.toPresheafedSpace))
(matchExpr✝ (Expr.isConstOf✝ · `CommRingCat)))
pure✝)
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace))
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `AlgebraicGeometry.Scheme.toLocallyRingedSpace))
(matchVar✝ `X))))))
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Opposite.op))
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `AlgebraicGeometry.Scheme.Opens)) (matchVar✝ `X)))
(matchVar✝ `U)) >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ =>
MatchState.delabVar✝ s✝ `U (some✝ e✝) >>= fun U =>
MatchState.delabVar✝ s✝ `X (some✝ e✝) >>= fun X => withHeadRefIfTagAppFns✝ `(Γ($X, $U)))
