Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.Nat.floor]
public meta def
_aux_Mathlib_NumberTheory_SiegelsLemma___delab_app__private_Mathlib_NumberTheory_SiegelsLemma_0_Int_Matrix_termB_1 :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 5
(getExpr✝ >>= fun e✝ =>
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Nat.floor)) (matchExpr✝ (Expr.isConstOf✝ · `Real)))
pure✝)
pure✝)
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `HPow.hPow))
(matchExpr✝ (Expr.isConstOf✝ · `Real)))
(matchExpr✝ (Expr.isConstOf✝ · `Real)))
(matchExpr✝ (Expr.isConstOf✝ · `Real)))
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `HMul.hMul))
(matchExpr✝ (Expr.isConstOf✝ · `Real)))
(matchExpr✝ (Expr.isConstOf✝ · `Real)))
(matchExpr✝ (Expr.isConstOf✝ · `Real)))
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Nat.cast))
(matchExpr✝ (Expr.isConstOf✝ · `Real)))
pure✝)
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Fintype.card))
(matchFVar✝ `β (matchExpr✝ isType'✝)))
pure✝)))
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Max.max))
(matchExpr✝ (Expr.isConstOf✝ · `Real)))
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
(matchExpr✝ (Expr.isConstOf✝ · `Real)))
(natLitMatcher✝ 1))
pure✝))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Norm.norm))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Matrix))
(matchFVar✝ `α (matchExpr✝ isType'✝)))
(matchFVar✝ `β (matchExpr✝ isType'✝)))
(matchExpr✝ (Expr.isConstOf✝ · `Int))))
pure✝)
(matchFVar✝ `A
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Matrix))
(matchFVar✝ `α (matchExpr✝ isType'✝)))
(matchFVar✝ `β (matchExpr✝ isType'✝)))
(matchExpr✝ (Expr.isConstOf✝ · `Int))))))))
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `HDiv.hDiv))
(matchExpr✝ (Expr.isConstOf✝ · `Real)))
(matchExpr✝ (Expr.isConstOf✝ · `Real)))
(matchExpr✝ (Expr.isConstOf✝ · `Real)))
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Nat.cast))
(matchExpr✝ (Expr.isConstOf✝ · `Real)))
pure✝)
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Fintype.card))
(matchFVar✝ `α (matchExpr✝ isType'✝)))
pure✝)))
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `HSub.hSub))
(matchExpr✝ (Expr.isConstOf✝ · `Real)))
(matchExpr✝ (Expr.isConstOf✝ · `Real)))
(matchExpr✝ (Expr.isConstOf✝ · `Real)))
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Nat.cast))
(matchExpr✝ (Expr.isConstOf✝ · `Real)))
pure✝)
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Fintype.card))
(matchFVar✝ `β (matchExpr✝ isType'✝)))
pure✝)))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Nat.cast))
(matchExpr✝ (Expr.isConstOf✝ · `Real)))
pure✝)
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Fintype.card))
(matchFVar✝ `α (matchExpr✝ isType'✝)))
pure✝))))) >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ => withHeadRefIfTagAppFns✝ `(B))
