Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.HSub.hSub]
public meta def
«_aux_Mathlib_NumberTheory_Cyclotomic_Three___delab_app__private_Mathlib_NumberTheory_Cyclotomic_Three_0_IsCyclotomicExtension_Rat_Three_termλ_1» :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 6
(getExpr✝ >>= fun e✝ =>
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `HSub.hSub))
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `NumberField.RingOfIntegers))
(matchFVar✝ `K (matchExpr✝ isType'✝)))
pure✝))
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `NumberField.RingOfIntegers))
(matchFVar✝ `K (matchExpr✝ isType'✝)))
pure✝))
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `NumberField.RingOfIntegers))
(matchFVar✝ `K (matchExpr✝ isType'✝)))
pure✝))
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `IsPrimitiveRoot.toInteger))
(matchFVar✝ `K (matchExpr✝ isType'✝)))
pure✝)
(matchFVar✝ `ζ (matchFVar✝ `K (matchExpr✝ isType'✝))))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(natLitMatcher✝ 3))
pure✝))
pure✝)
(matchFVar✝ `hζ
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `IsPrimitiveRoot))
(matchFVar✝ `K (matchExpr✝ isType'✝)))
pure✝)
(matchFVar✝ `ζ (matchFVar✝ `K (matchExpr✝ isType'✝))))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(natLitMatcher✝ 3))
pure✝)))))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `NumberField.RingOfIntegers))
(matchFVar✝ `K (matchExpr✝ isType'✝)))
pure✝))
(natLitMatcher✝ 1))
pure✝) >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ => withHeadRefIfTagAppFns✝ `(λ))
