Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ lam]
public meta def
_aux_Mathlib_NumberTheory_SiegelsLemma___delab_app__private_Mathlib_NumberTheory_SiegelsLemma_0_Int_Matrix_termN_1_1 :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
getExpr✝ >>= fun e✝ =>
(matchLambda✝ (matchFVar✝ `α (matchExpr✝ isType'✝))
(fun n✝ =>
matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝¹ (Expr.isConstOf✝ · `Finset.sum))
(matchFVar✝¹ `β (matchExpr✝¹ isType'✝¹)))
(matchExpr✝¹ (Expr.isConstOf✝ · `Int)))
pure✝)
(matchApp✝
(matchApp✝ (matchExpr✝¹ (Expr.isConstOf✝ · `Finset.univ))
(matchFVar✝¹ `β (matchExpr✝¹ isType'✝¹)))
pure✝))
(matchLambda✝¹ (matchFVar✝¹ `β (matchExpr✝¹ isType'✝¹))
(fun n✝¹ =>
matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝² (Expr.isConstOf✝¹ · `HMul.hMul))
(matchExpr✝² (Expr.isConstOf✝¹ · `Int)))
(matchExpr✝² (Expr.isConstOf✝¹ · `Int)))
(matchExpr✝² (Expr.isConstOf✝¹ · `Int)))
pure✝¹)
(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✝¹))))))))
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝² (Expr.isConstOf✝¹ · `Neg.neg))
(matchExpr✝² (Expr.isConstOf✝¹ · `Int)))
pure✝¹)
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝² (Expr.isConstOf✝¹ · `NegPart.negPart))
(matchExpr✝² (Expr.isConstOf✝¹ · `Int)))
pure✝¹)
(matchApp✝¹
(matchApp✝¹
(matchFVar✝² `A
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝² (Expr.isConstOf✝¹ · `Matrix))
(matchFVar✝² `α (matchExpr✝² isType'✝²)))
(matchFVar✝² `β (matchExpr✝² isType'✝²)))
(matchExpr✝² (Expr.isConstOf✝¹ · `Int))))
(matchExpr✝² (· == n✝)))
(matchExpr✝² (· == n✝¹)))))))) >=>
pure✝²)
MatchState.empty✝ >>=
fun s✝ => withHeadRefIfTagAppFns✝ `(N)
