[Merged by Bors] - doc: fix recurring instances of "this files" #30719

harahu · 2025-10-20T10:31:25Z

I noticed that there were a lot of instances of the typo "this files" in the repo. I fixed these while doing some drive-by typo fixes in the files I touched while I was at it.

The drive-by fixes are due to Codex and consist of:

Minor textual tweaks to improve flow of sentences.
Punctuation, like adding commas and full stops where appropriate in sentences.
Trimming superfluous white space and adding missing white space.
Swapping a ∪-operator for a ∩, where the latter was intended.
Swapping 𝒱(α, β, 𝔖 uβ) for 𝒱(α, β, 𝔖, uβ) where the latter was intended.

github-actions · 2025-10-20T10:32:34Z

PR summary 0d837987e5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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).

Mathlib/Topology/Algebra/Group/ClosedSubgroup.lean

grunweg

Thanks! LGTM with the changes below fixed.

Mathlib/LinearAlgebra/SesquilinearForm/Basic.lean

Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean

Mathlib/Topology/Algebra/OpenSubgroup.lean

grunweg · 2025-10-20T20:41:34Z

Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

  `β` is T₂ and `𝔖` covers `α`
 * `UniformOnFun.tendsto_iff_tendstoUniformlyOn`:
-  `𝒱(α, β, 𝔖 uβ)` is indeed the uniform structure of `𝔖`-convergence
+  `𝒱(α, β, 𝔖, uβ)` is indeed the uniform structure of `𝔖`-convergence


I'd need domain expertise to verify this. Are you absolutely sure this is correct? Otherwise, please split this into a separate PR.

I am pretty sure. The original, 𝒱(α, β, 𝔖 uβ) never actually shows up elsewhere in this file, whereas 𝒱(α, β, 𝔖, uβ) shows up 5 times in different docstrings in this file. I can't imagine anything else than this being the intended meaning.

See e.g. the definition of this structure on lines 40-42

If you're still unconvinced I can revert it.

This looks correct to me, but really shouldn't go in this PR. I'm happy to let you off this one time, but mixing a tricky change in with 30 boring changes means a person reviewing the boring stuff will give up at the tricky stuff and leave before finishing, and the person looking for tricky stuff will skip your review because it looks boring.

Just wanted to say that I'm grateful, not for you letting me off the hook, @eric-wieser, but for you so clearly explaining why this mixing is a bad idea. This psychological point is something that makes perfect sense when you point it out, but that I hadn't thought properly about. I guess part of the problem is that I don't have a well-developed sense of what is and isn't trivial. But I'll keep this in mind.

eric-wieser · 2025-10-20T21:17:07Z

I fixed these while doing some drive-by fixes in the files I touched while I was at it.

Please try to resist the urge to do this, as it makes review slower; or if you do, use git add -p to split them out into a separate PR.

Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

grunweg · 2025-10-20T21:49:26Z

I fixed these while doing some drive-by fixes in the files I touched while I was at it.

Please try to resist the urge to do this, as it makes review slower; or if you do, use git add -p to split them out into a separate PR.

Strongly agree! You like fast reviews (as do I), and having a PR do only one thing makes it much faster.

harahu · 2025-10-20T22:21:47Z

Good point. I had just been working with a bunch of typo PRs, and those tend to end up quite heterogeneous in content anyway, so I didn't connect that the "this files"-related changes could be (very) quickly merged on their own. Oh well.

harahu · 2025-10-20T22:40:00Z

-awaiting-author

Mathlib/Data/List/Lattice.lean

eric-wieser

This looks ok to me now. Please summarize explicitly in the description any change that isn't "this files". @grunweg, are you happy?

grunweg · 2025-10-21T08:22:27Z

Can you update the PR description as requested and ping me again once you've done this, please? I strongly presume I'll be happy then and just merge it. Thanks!

harahu · 2025-10-21T09:31:07Z

@grunweg: PR description is now updated with a summary of the drive-by changes.

-awaiting-author

grunweg · 2025-10-21T09:34:25Z

I'm happy now!
bors merge

I noticed that there were a lot of instances of the typo "this files" in the repo. I fixed these while doing some drive-by typo fixes in the files I touched while I was at it. The drive-by fixes are due to Codex and consist of: - Minor textual tweaks to improve flow of sentences. - Punctuation, like adding commas and full stops where appropriate in sentences. - Trimming superfluous white space and adding missing white space. - Swapping a `∪`-operator for a `∩`, where the latter was intended. - Swapping `𝒱(α, β, 𝔖 uβ)` for `𝒱(α, β, 𝔖, uβ)` where the latter was intended.

mathlib-bors · 2025-10-21T10:04:22Z

Build failed (retrying...):

Post-Build Step

I noticed that there were a lot of instances of the typo "this files" in the repo. I fixed these while doing some drive-by typo fixes in the files I touched while I was at it. The drive-by fixes are due to Codex and consist of: - Minor textual tweaks to improve flow of sentences. - Punctuation, like adding commas and full stops where appropriate in sentences. - Trimming superfluous white space and adding missing white space. - Swapping a `∪`-operator for a `∩`, where the latter was intended. - Swapping `𝒱(α, β, 𝔖 uβ)` for `𝒱(α, β, 𝔖, uβ)` where the latter was intended.

mathlib-bors · 2025-10-21T10:16:56Z

Build failed:

Post-Build Step

bryangingechen · 2025-10-21T12:02:15Z

bors r+

I noticed that there were a lot of instances of the typo "this files" in the repo. I fixed these while doing some drive-by typo fixes in the files I touched while I was at it. The drive-by fixes are due to Codex and consist of: - Minor textual tweaks to improve flow of sentences. - Punctuation, like adding commas and full stops where appropriate in sentences. - Trimming superfluous white space and adding missing white space. - Swapping a `∪`-operator for a `∩`, where the latter was intended. - Swapping `𝒱(α, β, 𝔖 uβ)` for `𝒱(α, β, 𝔖, uβ)` where the latter was intended.

mathlib-bors · 2025-10-21T13:18:49Z

Pull request successfully merged into master.

Build succeeded:

harahu added 2 commits October 20, 2025 12:25

Fix typos

907a449

Some more cases

686e5f3

harahu marked this pull request as ready for review October 20, 2025 10:41

eric-wieser reviewed Oct 20, 2025

View reviewed changes

Mathlib/Topology/Algebra/Group/ClosedSubgroup.lean Show resolved Hide resolved

Revert a change

60f0e8a

grunweg reviewed Oct 20, 2025

View reviewed changes

grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 20, 2025

Update Mathlib/LinearAlgebra/SesquilinearForm/Basic.lean

452f942

Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

PR feedback

ea7ca22

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 20, 2025

eric-wieser reviewed Oct 20, 2025

View reviewed changes

Mathlib/Data/List/Lattice.lean Show resolved Hide resolved

eric-wieser approved these changes Oct 20, 2025

View reviewed changes

grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 21, 2025

Trim a space that I introduced

301d485

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 21, 2025

leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Oct 21, 2025

mathlib-bors bot changed the title ~~doc: fix recurring instances of "this files"~~ [Merged by Bors] - doc: fix recurring instances of "this files" Oct 21, 2025

mathlib-bors bot closed this Oct 21, 2025

harahu deleted the doc/this-files branch October 21, 2025 13:31

[Merged by Bors] - doc: fix recurring instances of "this files" #30719

[Merged by Bors] - doc: fix recurring instances of "this files" #30719

Conversation

harahu commented Oct 20, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Oct 20, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 0d837987e5

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg Oct 20, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

harahu Oct 20, 2025

Choose a reason for hiding this comment

Uh oh!

harahu Oct 20, 2025

Choose a reason for hiding this comment

Uh oh!

harahu Oct 20, 2025

Choose a reason for hiding this comment

Uh oh!

eric-wieser Oct 20, 2025

Choose a reason for hiding this comment

Uh oh!

harahu Oct 21, 2025

Choose a reason for hiding this comment

Uh oh!

eric-wieser commented Oct 20, 2025

Uh oh!

grunweg commented Oct 20, 2025

Uh oh!

harahu commented Oct 20, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

harahu commented Oct 20, 2025

Uh oh!

Uh oh!

eric-wieser left a comment

Choose a reason for hiding this comment

Uh oh!

grunweg commented Oct 21, 2025

Uh oh!

harahu commented Oct 21, 2025

Uh oh!

grunweg commented Oct 21, 2025

Uh oh!

mathlib-bors bot commented Oct 21, 2025

Uh oh!

mathlib-bors bot commented Oct 21, 2025

Uh oh!

bryangingechen commented Oct 21, 2025

Uh oh!

mathlib-bors bot commented Oct 21, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

harahu commented Oct 20, 2025 •

edited

Loading

github-actions bot commented Oct 20, 2025 •

edited

Loading

grunweg Oct 20, 2025 •

edited

Loading

harahu commented Oct 20, 2025 •

edited

Loading