∫ Утверждение Mathlib

_aux_Mathlib_AlgebraicGeometry_EllipticCurve_Projective_Formula___delab_app__private_Mathlib_AlgebraicGeometry_EllipticCurve_Projective_Formula_0_termZ_1

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

URI: https://scilib.ai/kg/mathlib#_aux_Mathlib_AlgebraicGeometry_EllipticCurve_Projective_Formula___delab_app__private_Mathlib_AlgebraicGeometry_EllipticCurve_Projective_Formula_0_termZ_1

← MathLib Explorer

Lean4

/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.OfNat.ofNat]
public meta def
  _aux_Mathlib_AlgebraicGeometry_EllipticCurve_Projective_Formula___delab_app__private_Mathlib_AlgebraicGeometry_EllipticCurve_Projective_Formula_0_termZ_1 :
    Delab✝ :=
  whenPPOption✝ getPPNotation✝ <|
    whenNotPPOption✝ getPPExplicit✝ <|
      withOverApp✝ 3
        (getExpr✝ >>= fun e✝ =>
          (matchApp✝
                  (matchApp✝
                    (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
                      (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Fin))
                        (matchApp✝
                          (matchApp✝
                            (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
                              (matchExpr✝ (Expr.isConstOf✝ · `Nat)))
                            (natLitMatcher✝ 3))
                          pure✝)))
                    (natLitMatcher✝ 2))
                  pure✝ >=>
                pure✝)
              MatchState.empty✝ >>=
            fun s✝ => withHeadRefIfTagAppFns✝ `(z))

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