Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.Module.End.maxGenEigenspace]
public meta def
«_aux_Mathlib_Algebra_Lie_Weights_Basic___delab_app__private_Mathlib_Algebra_Lie_Weights_Basic_0_LieModule_term𝕎(_,_,_)_1» :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 7
(getExpr✝ >>= fun e✝ =>
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Module.End.maxGenEigenspace))
(matchFVar✝ `R (matchExpr✝ isType'✝)))
(matchVar✝ `M))
pure✝)
pure✝)
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `DFunLike.coe))
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `LieHom))
(matchFVar✝ `R (matchExpr✝ isType'✝)))
(matchFVar✝ `L (matchExpr✝ isType'✝)))
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Module.End))
(matchFVar✝ `R (matchExpr✝ isType'✝)))
(matchVar✝ `M))
pure✝)
pure✝)
pure✝))
pure✝)
pure✝)
pure✝)
pure✝)
pure✝))
(matchFVar✝ `L (matchExpr✝ isType'✝)))
(matchLambda✝ (matchFVar✝ `L (matchExpr✝ isType'✝))
(fun n✝ =>
matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `Module.End))
(matchFVar✝¹ `R (matchExpr✝¹ isType'✝¹)))
(matchVar✝¹ `M))
pure✝¹)
pure✝¹)
pure✝¹)))
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `LieModule.toEnd))
(matchFVar✝ `R (matchExpr✝ isType'✝)))
(matchFVar✝ `L (matchExpr✝ isType'✝)))
(matchVar✝ `M))
pure✝)
pure✝)
pure✝)
pure✝)
pure✝)
pure✝)
pure✝))
(matchVar✝ `x)))
(matchVar✝ `χ) >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ =>
MatchState.delabVar✝ s✝ `χ (some✝ e✝) >>= fun χ =>
MatchState.delabVar✝ s✝ `x (some✝ e✝) >>= fun x =>
MatchState.delabVar✝ s✝ `M (some✝ e✝) >>= fun M => withHeadRefIfTagAppFns✝ `(𝕎($M, $χ, $x)))
