Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.Finset.Icc]
public meta def
_aux_Mathlib_NumberTheory_SiegelsLemma___delab_app__private_Mathlib_NumberTheory_SiegelsLemma_0_Int_Matrix_termT_1 :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 5
(getExpr✝ >>= fun e✝ =>
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finset.Icc))
(matchForall✝ (matchFVar✝ `β (matchExpr✝ isType'✝))
(fun n✝ => matchExpr✝¹ (Expr.isConstOf✝¹ · `Int))))
pure✝)
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
(matchForall✝¹ (matchFVar✝ `β (matchExpr✝ isType'✝))
(fun n✝¹ => matchExpr✝² (Expr.isConstOf✝² · `Int))))
(natLitMatcher✝ 0))
pure✝))
(matchLambda✝ (matchFVar✝ `β (matchExpr✝ isType'✝))
(fun n✝² =>
matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝³ (Expr.isConstOf✝³ · `Nat.cast))
(matchExpr✝³ (Expr.isConstOf✝³ · `Int)))
pure✝¹)
(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✝ `(T))
