Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore: simplify by rfl #7039

Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - chore: simplify by rfl #7039

wants to merge 2 commits into from

Conversation

mo271
Copy link
Collaborator

@mo271 mo271 commented Sep 8, 2023

Open in Gitpod

@mo271 @eric-wieser
Update Archive/Imo/Imo1962Q4.lean
bf3d8b2 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
eric-wieser
eric-wieser approved these changes Sep 8, 2023
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

bors merge

Thanks!

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Sep 8, 2023
bors bot pushed a commit that referenced this pull request Sep 8, 2023
@mo271
chore: simplify by rfl (#7039)
8908a0a 
Co-authored-by: Moritz Firsching <firsching@google.com>
@bors
Copy link

bors bot commented Sep 8, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title chore: simplify by rfl [Merged by Bors] - chore: simplify by rfl Sep 8, 2023
@bors bors bot closed this Sep 8, 2023
@bors bors bot deleted the mo271/by_rfl branch September 8, 2023 22:16
@kmill
Copy link
Contributor

kmill commented Sep 10, 2023

!bench

I'm just curious if this had any impact on performance -- it turns out rfl can sometimes be slower than by rfl because of elaboration order (though I believe it can also be faster sometimes, so who knows).

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit bf3d8b2.
There were significant changes against commit f0c7f6d:

  Benchmark                                              Metric         Change
  ============================================================================
- ~Mathlib.NumberTheory.ModularForms.JacobiTheta.Basic   instructions     5.5%

@mo271
Copy link
Collaborator Author

mo271 commented Sep 10, 2023 •
edited
Loading

@kmill
Does this mean we should roll back the Mathlib/NumberTheory/ModularForms/JacobiTheta/Basic.lean?

@kmill
Copy link
Contributor

kmill commented Sep 10, 2023

@mo271 I think it's safe leaving it as-is, but if you're really motivated you could investigate if an individual rfl got much slower than the rest. That's only if you're really motivated though!

Julian added a commit that referenced this pull request Sep 11, 2023
@Julian
Merge branch 'fix-lint' into alexjbest/auto-suggest
4eadc5d 
* fix-lint: (463 commits)
  chore: lint-style.py was calling str.replace incorrectly
  chore: module doc for #find_home, #minimize_imports, import early (#7095)
  chore: reduce imports to Data.Rat.Cast.CharZero (#7091)
  chore: cleanup imports of Data/Rat/Cast/Defs (#7092)
  chore: linarith only needs ring1 (#7090)
  refactor(Data/Int/Bitwise): use `<<<` and `>>>` notation (#6789)
  chore: delete redundant commented-out positivity test (#7085)
  chore: fix docstrings, names and aligns about paracompacity of emetric spaces (#7064)
  feat(Data/Finsupp): add notation (#6367)
  refactor: re-home some meta code (#6921)
  fix: don't use `False` as a bool, use `false` (#7059)
  chore: fix reference to `compactCovering` in docstring (#7065)
  fix: fix link in docstring of IsWellFounded (#7063)
  chore: tidy various files (#7041)
  feat: roots in an algebra (#6740)
  chore: revert ProofWidgets bump in #7044 and #7056 (#7069)
  feat: super factorial (#6768)
  feat(LinearAlgebra/Matrix/Trace): add Matrix.trace_diagonal (#7061)
  chore: complete ProofWidgets bump (#7056)
  feat: More `Finset.sup'` lemmas (#7021)
  feat: self_lt_pow (#7058)
  chore: move some files to `MeasureTheory/MeasurableSpace/` (#7045)
  chore(RingTheory/Nilpotent): untwine two universes (#7057)
  feat: von Neumann Mean Ergodic Theorem (#6053)
  feat: (sSup, Iic) and (Ici, sInf) are Galois connections (#6951)
  feat: derivative along a vector (#7038)
  feat: check for some common git problems in CI (#7043)
  chore: bump ProofWidgets (#7044)
  feat(Topology/Algebra): add `DiscreteTopology Mˣ` (#7028)
  chore: simplify `by rfl` (#7039)
  chore: tidy various files (#7035)
  refactor(LinearAlgebra/CliffordAlgebra/Conjugation): expose implementation details of 'reverse' (#6783)
  feat: add `DiscreteTopology.of_continuous_injective` (#7029)
  feat: restore the module docstring code snippet (#7030)
  feat: flesh out the API for `realPart` and `imaginaryPart` (#7023)
  chore: missing simps lemmas for `Multiplicative` defs (#7016)
  feat: characterize isLittleO on principal filters (#7008)
  doc: cleanup documentation on Basis.constr (#7007)
  feat: cleanup API around differentiable functions (#7004)
  feat: add Nat.digits_append_digits (#6999)
  feat: definition of the homology of a short complex (#6994)
  chore: implement porting notes about Polish spaces (#6991)
  feat(Algebra/Category/ModuleCat): composition of restriction of scalar functors (#6915)
  feat: compute the integral of sqrt (1 - x ^ 2) (#6905)
  chore(*/TensorProduct): missing functorial lemmas (#6781)
  feat: a functor from a small category to a filtered category factors through a small filtered category (#6212)
  feat: expand API on locally integrable functions (#7006)
  chore: split Tactic.NormNum.Basic (#7002)
  feat: a few lemmas on continuous functions (#7005)
  feat: ZMod.castHom_self (#7013)
  ...
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
@mo271 @kodyvajjha
chore: simplify by rfl (#7039)
0d35048 
Co-authored-by: Moritz Firsching <firsching@google.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser approved these changes

Assignees
No one assigned
Labels
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.
5 participants
@mo271 @kmill @leanprover-bot @eric-wieser @leanprover-community-mathlib4-bot