Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.HDiv.hDiv]
public meta def
_aux_Mathlib_NumberTheory_SiegelsLemma___delab_app__private_Mathlib_NumberTheory_SiegelsLemma_0_Int_Matrix_termE_1 :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 6
(getExpr✝ >>= fun e✝ =>
(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✝ `(e))
