Label PR based on Comment

[Merged by Bors] - feat(Mathlib/Order/SuccPred/Limit): more `WithTop` lemmas about `IsMin`/`CovBy`/`IsSuccLimit` #217295

Sign in to view logs

Triggered via pull request August 21, 2026 22:45

SnirBroshi

created #38841

Status Success

Total duration 4s

Artifacts –

labels_from_comment.yml

on: pull_request_review_comment