Skip to content

[Merged by Bors] - feat(ENat): (∀ a : ℕ, a ≤ m → a ≤ n) ↔ m ≤ n#23101

Closed
YaelDillies wants to merge 7 commits intomasterfrom
enat_nat_cast_le_iff_le
Closed

[Merged by Bors] - feat(ENat): (∀ a : ℕ, a ≤ m → a ≤ n) ↔ m ≤ n#23101
YaelDillies wants to merge 7 commits intomasterfrom
enat_nat_cast_le_iff_le

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Mar 19, 2025

From my PhD (MiscYD)

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 19, 2025 •
edited
Loading

PR summary b8f36bba7b

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ eq_bot_iff_forall_le
+ eq_bot_iff_forall_lt
+ eq_bot_iff_forall_ne
+ eq_none_iff_forall_some_ne
+ forall_coe_le_iff_le
+ forall_le_iff_eq_top
+ forall_lt_iff_eq_top
+ forall_natCast_le_iff_le
++ eq_top_iff_forall_ge
++ eq_top_iff_forall_gt
- eq_top_iff_forall_le
- eq_top_iff_forall_lt
- forall_ge_iff_eq_top
- forall_gt_iff_eq_top
-++ eq_top_iff_forall_ne

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

b-mehta
b-mehta approved these changes Mar 19, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@b-mehta b-mehta left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+

Comment thread Mathlib/Data/ENat/Basic.lean
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 19, 2025

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Mar 19, 2025
@YaelDillies YaelDillies added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Mar 19, 2025
b-mehta
b-mehta reviewed Mar 19, 2025
View reviewed changes
Comment thread Mathlib/Order/WithBot.lean Outdated
b-mehta
b-mehta reviewed Mar 19, 2025
View reviewed changes
Comment thread Mathlib/Order/WithBot.lean
b-mehta
b-mehta reviewed Mar 19, 2025
View reviewed changes
Comment thread Mathlib/Data/ENat/Basic.lean Outdated
@YaelDillies @b-mehta @github-actions
typos
55572e6 
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
b-mehta
b-mehta reviewed Mar 19, 2025
View reviewed changes
Comment thread Mathlib/Order/WithBot.lean
@[simp]
theorem coe_top_lt [OrderTop α] : (⊤ : α) < x ↔ x = ⊤ := by cases x <;> simp

lemma forall_gt_iff_eq_top : (∀ a : α, a < y) ↔ y = ⊤ := by
Copy link
Copy Markdown
Contributor

@b-mehta b-mehta Mar 19, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hold on, why are these getting removed?

Copy link
Copy Markdown
Contributor Author

@YaelDillies YaelDillies Mar 19, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well, in #23101 (comment) you said you wanted y = ⊤ ↔ ∀ a : α, a < y to exist. Since (∀ a : α, a < y) ↔ y = ⊤ already existed then, I assumed you wanted me to replace it, so I have replaced it (and indeed I don't think we should have both).

Copy link
Copy Markdown
Contributor

@b-mehta b-mehta Mar 19, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ehhh, okay

Comment thread Mathlib/Data/ENat/Basic.lean Outdated
@b-mehta b-mehta removed the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Mar 19, 2025
YaelDillies and others added 2 commits March 19, 2025 21:25
@YaelDillies @b-mehta
more typos
4d62325 
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
@YaelDillies
fix
feeb51f
@YaelDillies YaelDillies added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Mar 19, 2025
@ghost
Copy link
Copy Markdown

ghost commented Mar 19, 2025

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Mar 19, 2025
mathlib-bors bot pushed a commit that referenced this pull request Mar 20, 2025
@YaelDillies
feat(ENat): (∀ a : ℕ, a ≤ m → a ≤ n) ↔ m ≤ n (#23101)
6ab5985 
From my PhD (MiscYD)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 20, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(ENat): (∀ a : ℕ, a ≤ m → a ≤ n) ↔ m ≤ n [Merged by Bors] - feat(ENat): (∀ a : ℕ, a ≤ m → a ≤ n) ↔ m ≤ n Mar 20, 2025
@mathlib-bors mathlib-bors bot closed this Mar 20, 2025
@mathlib-bors mathlib-bors bot deleted the enat_nat_cast_le_iff_le branch March 20, 2025 00:57
tukamilano pushed a commit that referenced this pull request Mar 20, 2025
@YaelDillies @tukamilano
feat(ENat): (∀ a : ℕ, a ≤ m → a ≤ n) ↔ m ≤ n (#23101)
458ba7b 
From my PhD (MiscYD)
erdOne
erdOne reviewed Apr 7, 2025
View reviewed changes
Comment thread Mathlib/Order/WithBot.lean
Comment on lines +822 to +823
@[deprecated (since := "2025-03-19")] alias forall_lt_iff_eq_top := eq_top_iff_forall_gt
@[deprecated (since := "2025-03-19")] alias forall_le_iff_eq_top := eq_top_iff_forall_ge
Copy link
Copy Markdown
Member

@erdOne erdOne Apr 7, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These have the wrong name. (Do we care?)

Copy link
Copy Markdown
Contributor Author

@YaelDillies YaelDillies Apr 7, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

#23761

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@b-mehta b-mehta b-mehta approved these changes

@erdOne erdOne erdOne left review comments

Assignees

No one assigned

Labels

auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@YaelDillies @b-mehta @erdOne
⚡