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_termS_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✝)
(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✝²))))))))))
(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✝⁵ · `PosPart.posPart))
(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✝ `(S))
