Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ lam]
public meta def
_aux_Mathlib_Analysis_Fourier_RiemannLebesgueLemma___delab_app__private_Mathlib_Analysis_Fourier_RiemannLebesgueLemma_0_termI_1 :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
getExpr✝ >>= fun e✝ =>
(matchLambda✝ (matchFVar✝ `V (matchExpr✝ isType'✝))
(fun n✝ =>
matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝¹ (Expr.isConstOf✝ · `HSMul.hSMul))
(matchExpr✝¹ (Expr.isConstOf✝ · `Real)))
(matchFVar✝¹ `V (matchExpr✝¹ isType'✝¹)))
(matchFVar✝¹ `V (matchExpr✝¹ isType'✝¹)))
pure✝)
(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✝ · `OfNat.ofNat))
(matchExpr✝¹ (Expr.isConstOf✝ · `Real)))
(natLitMatcher✝ 1))
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✝ · `OfNat.ofNat))
(matchExpr✝¹ (Expr.isConstOf✝ · `Real)))
(natLitMatcher✝ 2))
pure✝))
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝¹ (Expr.isConstOf✝ · `HPow.hPow))
(matchExpr✝¹ (Expr.isConstOf✝ · `Real)))
(matchExpr✝¹ (Expr.isConstOf✝ · `Nat)))
(matchExpr✝¹ (Expr.isConstOf✝ · `Real)))
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝¹ (Expr.isConstOf✝ · `Norm.norm))
(matchFVar✝¹ `V (matchExpr✝¹ isType'✝¹)))
pure✝)
(matchExpr✝¹ (· == n✝))))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝¹ (Expr.isConstOf✝ · `OfNat.ofNat))
(matchExpr✝¹ (Expr.isConstOf✝ · `Nat)))
(natLitMatcher✝ 2))
pure✝)))))
(matchExpr✝¹ (· == n✝))) >=>
pure✝¹)
MatchState.empty✝ >>=
fun s✝ => withHeadRefIfTagAppFns✝ `(i)
