Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.Set.range]
public meta def
_aux_Mathlib_Algebra_Category_Grp_EpiMono___delab_app__private_Mathlib_Algebra_Category_Grp_EpiMono_0_GrpCat_SurjectiveOfEpiAuxs_termX_1 :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 3
(getExpr✝ >>= fun e✝ =>
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Set.range))
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Set))
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `GrpCat.carrier))
(matchFVar✝ `B (matchExpr✝ (Expr.isConstOf✝ · `GrpCat))))))
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `GrpCat.carrier))
(matchFVar✝ `B (matchExpr✝ (Expr.isConstOf✝ · `GrpCat)))))
(matchLambda✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `GrpCat.carrier))
(matchFVar✝ `B (matchExpr✝ (Expr.isConstOf✝ · `GrpCat))))
(fun n✝ =>
matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `HSMul.hSMul))
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `GrpCat.carrier))
(matchFVar✝¹ `B (matchExpr✝¹ (Expr.isConstOf✝¹ · `GrpCat)))))
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `Set))
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `GrpCat.carrier))
(matchFVar✝¹ `B (matchExpr✝¹ (Expr.isConstOf✝¹ · `GrpCat))))))
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `Set))
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `GrpCat.carrier))
(matchFVar✝¹ `B (matchExpr✝¹ (Expr.isConstOf✝¹ · `GrpCat))))))
pure✝)
(matchExpr✝¹ (· == n✝)))
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `SetLike.coe))
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `Subgroup))
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `GrpCat.carrier))
(matchFVar✝¹ `B (matchExpr✝¹ (Expr.isConstOf✝¹ · `GrpCat)))))
pure✝))
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `GrpCat.carrier))
(matchFVar✝¹ `B (matchExpr✝¹ (Expr.isConstOf✝¹ · `GrpCat)))))
pure✝)
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `MonoidHom.range))
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `GrpCat.carrier))
(matchFVar✝¹ `A (matchExpr✝¹ (Expr.isConstOf✝¹ · `GrpCat)))))
pure✝)
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `GrpCat.carrier))
(matchFVar✝¹ `B (matchExpr✝¹ (Expr.isConstOf✝¹ · `GrpCat)))))
pure✝)
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `GrpCat.Hom.hom))
(matchFVar✝¹ `A (matchExpr✝¹ (Expr.isConstOf✝¹ · `GrpCat))))
(matchFVar✝¹ `B (matchExpr✝¹ (Expr.isConstOf✝¹ · `GrpCat))))
(matchFVar✝¹ `f
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `Quiver.Hom))
(matchExpr✝¹ (Expr.isConstOf✝¹ · `GrpCat)))
pure✝)
(matchFVar✝¹ `A (matchExpr✝¹ (Expr.isConstOf✝¹ · `GrpCat))))
(matchFVar✝¹ `B (matchExpr✝¹ (Expr.isConstOf✝¹ · `GrpCat)))))))))) >=>
pure✝¹)
MatchState.empty✝ >>=
fun s✝ => withHeadRefIfTagAppFns✝ `(X))
