Skip to content

feat(Data/Int): port data.int.basic from the lean3 prelude#23

Merged
avigad merged 8 commits intoleanprover-community:masterfrom
denayd:int
Jul 9, 2021
Merged

feat(Data/Int): port data.int.basic from the lean3 prelude#23
avigad merged 8 commits intoleanprover-community:masterfrom
denayd:int

Conversation

@denayd
Copy link
Copy Markdown
Contributor

@denayd denayd commented Jun 30, 2021

I needed some facts about the integers and Lean4 core just defines them and leaves it at that. This file proves the ring properties, provides some lemmas about the Nat to Int coercion, and defines a couple extra functions like sign and gcd.
It has to slightly modify Algebra.Group.Defs because that also defines the ℤ notation

Next up: my port of Data.Int.Order which depends on #18

kbuzzard
kbuzzard reviewed Jul 3, 2021
View reviewed changes
Copy link
Copy Markdown
Member

@kbuzzard kbuzzard left a comment

Choose a reason for hiding this comment

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

I am not sure that the naming convention is the Lean 4 one, but I am not very good at Lean 4 naming conventions yet.

@denayd
Copy link
Copy Markdown
Contributor Author

denayd commented Jul 5, 2021

I am not sure that the naming convention is the Lean 4 one, but I am not very good at Lean 4 naming conventions yet.

Honestly I'm clueless as to what the Lean 4 naming convention is, or if there even is one. I just made snake_case aliases for things because that's what Nat.Basic does and left everything else the same as lean3. Do you know if there's some kind of document or zulip thread I can read that will clarify it a little?

@digama0
Copy link
Copy Markdown
Member

digama0 commented Jul 5, 2021

The main zulip thread on the topic is https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/rfc.3A.20theorem.20names . I was pretty happy with the proposal here and it seemed to be gaining traction until Leo vetoed it in the final hour, and the discussion hasn't progressed since then.

Lean 4 core has a mashup of naming conventions, because the convention changed over time and the old stuff (especially proofs) was not updated. Those snake_case aliases are my attempt to bring some order to the madness with the naming convention called "proposal 3" in the thread: PascalCase namespaces, modules, and types, javaCase functions, and snake_case theorems. The proposal variation of uncertain outcome is whether to javaCase propositions as well.

@avigad
Copy link
Copy Markdown
Contributor

avigad commented Jul 9, 2021

I'll add that I also like Mario's proposal.

@bryangingechen bryangingechen changed the title feat (Data/Int): port data.int.basic from the lean3 prelude feat(Data/Int): port data.int.basic from the lean3 prelude Jul 9, 2021
@avigad
Copy link
Copy Markdown
Contributor

avigad commented Jul 9, 2021

@denayd Git reports a conflict when I try to rebase and merge. Could you rebase and fix it, and then I'll merge?

@avigad avigad merged commit 9a4a3ba into leanprover-community:master Jul 9, 2021
@avigad
Copy link
Copy Markdown
Contributor

avigad commented Jul 9, 2021

@denayd Oh, I could squash-and-merge -- never mind. Sorry for the noise.

@denayd denayd deleted the int branch July 30, 2021 21:40
@github-actions github-actions bot mentioned this pull request Dec 19, 2022
Closed
mattrobball added a commit that referenced this pull request Feb 25, 2023
@mattrobball
# This is a combination of 126 commits.
8fcb216 
# This is the 1st commit message:

automated fixes

Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean

# The commit message #2 will be skipped:

# feat: port CategoryTheory.Limits.IsLimit

# The commit message #3 will be skipped:

# Initial file copy from mathport

# The commit message #4 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #5 will be skipped:

# feat: port CategoryTheory.Limits.Cones

# The commit message #6 will be skipped:

# Initial file copy from mathport

# The commit message #7 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #8 will be skipped:

# feat: port CategoryTheory.Yoneda

# The commit message #9 will be skipped:

# Initial file copy from mathport

# The commit message #10 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #11 will be skipped:

# feat: port CategoryTheory.Functor.Currying

# The commit message #12 will be skipped:

# Initial file copy from mathport

# The commit message #13 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #14 will be skipped:

# fix all but one decl

# The commit message #15 will be skipped:

# fix last errors

# The commit message #16 will be skipped:

# feat: port CategoryTheory.Functor.Hom

# The commit message #17 will be skipped:

# Initial file copy from mathport

# The commit message #18 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #19 will be skipped:

# feat: port CategoryTheory.Types

# The commit message #20 will be skipped:

# Initial file copy from mathport

# The commit message #21 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #22 will be skipped:

# feat: port CategoryTheory.EpiMono

# The commit message #23 will be skipped:

# Initial file copy from mathport

# The commit message #24 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #25 will be skipped:

# feat: port CategoryTheory.Groupoid

# The commit message #26 will be skipped:

# Initial file copy from mathport

# The commit message #27 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #28 will be skipped:

# feat: port CategoryTheory.Pi.Basic

# The commit message #29 will be skipped:

# Initial file copy from mathport

# The commit message #30 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #31 will be skipped:

# fix some errors

# The commit message #32 will be skipped:

# some more fixes

# The commit message #33 will be skipped:

# more fixes

# The commit message #34 will be skipped:

# finally fixed

# The commit message #35 will be skipped:

# lint

# The commit message #36 will be skipped:

# add porting note for scary warning

# The commit message #37 will be skipped:

# add porting note about proliferation of match

# The commit message #38 will be skipped:

# initial pass

# The commit message #39 will be skipped:

# fix errors

# The commit message #40 will be skipped:

# lint

# The commit message #41 will be skipped:

# fix errors; lint; add porting notes

# The commit message #42 will be skipped:

# fix errors; lint; add porting note

# The commit message #43 will be skipped:

# fix error

# The commit message #44 will be skipped:

# fix some errors

# The commit message #45 will be skipped:

# minor fixes

# The commit message #46 will be skipped:

# fix all but four

# The commit message #47 will be skipped:

# fix last errors; lint

# The commit message #48 will be skipped:

# feat: port CategoryTheory.DiscreteCategory

# The commit message #49 will be skipped:

# Initial file copy from mathport

# The commit message #50 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #51 will be skipped:

# get file to build

# The commit message #52 will be skipped:

# lint

# The commit message #53 will be skipped:

# lint some more

# The commit message #54 will be skipped:

# feat: port CategoryTheory.Functor.ReflectsIsomorphisms

# The commit message #55 will be skipped:

# Initial file copy from mathport

# The commit message #56 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #57 will be skipped:

# feat: port CategoryTheory.Functor.EpiMono

# The commit message #58 will be skipped:

# Initial file copy from mathport

# The commit message #59 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #60 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Adjunction

# The commit message #61 will be skipped:

# Initial file copy from mathport

# The commit message #62 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #63 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Basic

# The commit message #64 will be skipped:

# Initial file copy from mathport

# The commit message #65 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #66 will be skipped:

# feat: port CategoryTheory.CommSq

# The commit message #67 will be skipped:

# Initial file copy from mathport

# The commit message #68 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #69 will be skipped:

# first pass

# The commit message #70 will be skipped:

# names and removing restate_axiom

# The commit message #71 will be skipped:

# fix lint

# The commit message #72 will be skipped:

# remove spurious edit

# The commit message #73 will be skipped:

# fix errors; lint

# The commit message #74 will be skipped:

# feat: port CategoryTheory.Adjunction.Basic

# The commit message #75 will be skipped:

# Initial file copy from mathport

# The commit message #76 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #77 will be skipped:

# Initial file copy from mathport

# The commit message #78 will be skipped:

# Mathbin -> Mathlib; add import to Mathlib.lean

# The commit message #79 will be skipped:

# push it as far as possible

# The commit message #80 will be skipped:

# minor changes

# The commit message #81 will be skipped:

# seems to work

# The commit message #82 will be skipped:

# add example and equivalence file for testing

# The commit message #83 will be skipped:

# test: create `slice.lean` test file

# The commit message #84 will be skipped:

# remove equivalence.lean

# The commit message #85 will be skipped:

# remove rewriteTarget'; change MonadExceptOf to MonadExcept

# The commit message #86 will be skipped:

# add documentation and clean up

# The commit message #87 will be skipped:

# move iteration tactics to core

# The commit message #88 will be skipped:

# modify documentation lines

# The commit message #89 will be skipped:

# add module documentation(?)

# The commit message #90 will be skipped:

# fix module docs

# The commit message #91 will be skipped:

# fix test/slice.lean

# The commit message #92 will be skipped:

# fix all but refl error

# The commit message #93 will be skipped:

# fix refl error and lint errors

# The commit message #94 will be skipped:

# fix final long line

# The commit message #95 will be skipped:

# use `Mathport` syntax
# * use existing docs
# * fix docs typos

# The commit message #96 will be skipped:

# test: add simple `rhs`/`lhs` tests

# The commit message #97 will be skipped:

# minor changes to `Tactic.Core`
# * use `m` instead of `TacticM` now that we use `MonadExcept`
# * simplify code for `iterateRange`
# * minor docs tweaks

# The commit message #98 will be skipped:

# update slice naming

# The commit message #99 will be skipped:

# some progress

# The commit message #100 will be skipped:

# only one error left

# The commit message #101 will be skipped:

# filled in last sorry

# The commit message #102 will be skipped:

# break long lines

# The commit message #103 will be skipped:

# delete linter command

# The commit message #104 will be skipped:

# fix comments

# The commit message #105 will be skipped:

# fix two simpNF lints

# The commit message #106 will be skipped:

# fill in some docstrings

# The commit message #107 will be skipped:

# fix most linter issues

# The commit message #108 will be skipped:

# add missing aligns for fields; lint

# The commit message #109 will be skipped:

# restore lost import line

# The commit message #110 will be skipped:

# fix errors; lint

# The commit message #111 will be skipped:

# feat: port CategoryTheory.Limits.Shapes.StrongEpi

# The commit message #112 will be skipped:

# Initial file copy from mathport

# The commit message #113 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #114 will be skipped:

# fix errors; lint

# The commit message #115 will be skipped:

# Update Mathlib.lean

# The commit message #116 will be skipped:

# fix errors; lint

# The commit message #117 will be skipped:

# fix errors; lint; shorten filename

# The commit message #118 will be skipped:

# fix some errors

# The commit message #119 will be skipped:

# fix some more

# The commit message #120 will be skipped:

# fix errors

# The commit message #121 will be skipped:

# lint

# The commit message #122 will be skipped:

# fix errors

# The commit message #123 will be skipped:

# lint

# The commit message #124 will be skipped:

# feat: port CategoryTheory.Category.Ulift

# The commit message #125 will be skipped:

# Initial file copy from mathport

# The commit message #126 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean
mattrobball added a commit that referenced this pull request Feb 25, 2023
@mattrobball
# This is a combination of 90 commits.
20f5a8f 
# This is the 1st commit message:

automated fixes

Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean

# The commit message #2 will be skipped:

# feat: port CategoryTheory.Limits.Cones

# The commit message #3 will be skipped:

# Initial file copy from mathport

# The commit message #4 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #5 will be skipped:

# feat: port CategoryTheory.Yoneda

# The commit message #6 will be skipped:

# Initial file copy from mathport

# The commit message #7 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #8 will be skipped:

# feat: port CategoryTheory.Functor.Currying

# The commit message #9 will be skipped:

# Initial file copy from mathport

# The commit message #10 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #11 will be skipped:

# fix all but one decl

# The commit message #12 will be skipped:

# fix last errors

# The commit message #13 will be skipped:

# feat: port CategoryTheory.Functor.Hom

# The commit message #14 will be skipped:

# Initial file copy from mathport

# The commit message #15 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #16 will be skipped:

# feat: port CategoryTheory.Types

# The commit message #17 will be skipped:

# Initial file copy from mathport

# The commit message #18 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #19 will be skipped:

# feat: port CategoryTheory.EpiMono

# The commit message #20 will be skipped:

# Initial file copy from mathport

# The commit message #21 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #22 will be skipped:

# feat: port CategoryTheory.Groupoid

# The commit message #23 will be skipped:

# Initial file copy from mathport

# The commit message #24 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #25 will be skipped:

# feat: port CategoryTheory.Pi.Basic

# The commit message #26 will be skipped:

# Initial file copy from mathport

# The commit message #27 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #28 will be skipped:

# fix some errors

# The commit message #29 will be skipped:

# some more fixes

# The commit message #30 will be skipped:

# more fixes

# The commit message #31 will be skipped:

# finally fixed

# The commit message #32 will be skipped:

# lint

# The commit message #33 will be skipped:

# add porting note for scary warning

# The commit message #34 will be skipped:

# add porting note about proliferation of match

# The commit message #35 will be skipped:

# initial pass

# The commit message #36 will be skipped:

# fix errors

# The commit message #37 will be skipped:

# lint

# The commit message #38 will be skipped:

# fix errors; lint; add porting notes

# The commit message #39 will be skipped:

# fix errors; lint; add porting note

# The commit message #40 will be skipped:

# fix error

# The commit message #41 will be skipped:

# fix some errors

# The commit message #42 will be skipped:

# minor fixes

# The commit message #43 will be skipped:

# fix all but four

# The commit message #44 will be skipped:

# Delete start_port-macos.sh

# The commit message #45 will be skipped:

# fix last errors; lint

# The commit message #46 will be skipped:

# feat: port CategoryTheory.DiscreteCategory

# The commit message #47 will be skipped:

# Initial file copy from mathport

# The commit message #48 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #49 will be skipped:

# get file to build

# The commit message #50 will be skipped:

# lint

# The commit message #51 will be skipped:

# lint some more

# The commit message #52 will be skipped:

# feat: port CategoryTheory.Functor.ReflectsIsomorphisms

# The commit message #53 will be skipped:

# Initial file copy from mathport

# The commit message #54 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #55 will be skipped:

# feat: port CategoryTheory.Functor.EpiMono

# The commit message #56 will be skipped:

# Initial file copy from mathport

# The commit message #57 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #58 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Adjunction

# The commit message #59 will be skipped:

# Initial file copy from mathport

# The commit message #60 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #61 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Basic

# The commit message #62 will be skipped:

# Initial file copy from mathport

# The commit message #63 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #64 will be skipped:

# feat: port CategoryTheory.CommSq

# The commit message #65 will be skipped:

# Initial file copy from mathport

# The commit message #66 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #67 will be skipped:

# first pass

# The commit message #68 will be skipped:

# names and removing restate_axiom

# The commit message #69 will be skipped:

# fix lint

# The commit message #70 will be skipped:

# remove spurious edit

# The commit message #71 will be skipped:

# fix errors; lint

# The commit message #72 will be skipped:

# feat: port CategoryTheory.Adjunction.Basic

# The commit message #73 will be skipped:

# Initial file copy from mathport

# The commit message #74 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #75 will be skipped:

# Initial file copy from mathport

# The commit message #76 will be skipped:

# Mathbin -> Mathlib; add import to Mathlib.lean

# The commit message #77 will be skipped:

# push it as far as possible

# The commit message #78 will be skipped:

# minor changes

# The commit message #79 will be skipped:

# seems to work

# The commit message #80 will be skipped:

# add example and equivalence file for testing

# The commit message #81 will be skipped:

# test: create `slice.lean` test file

# The commit message #82 will be skipped:

# remove equivalence.lean

# The commit message #83 will be skipped:

# remove rewriteTarget'; change MonadExceptOf to MonadExcept

# The commit message #84 will be skipped:

# add documentation and clean up

# The commit message #85 will be skipped:

# move iteration tactics to core

# The commit message #86 will be skipped:

# add slice to global import file

# The commit message #87 will be skipped:

# modify documentation lines

# The commit message #88 will be skipped:

# add module documentation(?)

# The commit message #89 will be skipped:

# fix module docs

# The commit message #90 will be skipped:

# fix test/slice.lean
mattrobball added a commit that referenced this pull request Mar 1, 2023
@mattrobball
Squashed commit of the following:
2807219 
commit 6a44854
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Feb 28 06:29:46 2023 -0500

    add missing aligns to cones.lean

commit 84ea4c6
Author: Matthew Ballard <matt@mrb.email>
Date:   Mon Feb 27 14:55:26 2023 -0500

    lint for changes and clean up

commit 3ef0e8b
Author: Matthew Ballard <matt@mrb.email>
Date:   Mon Feb 27 14:12:15 2023 -0500

    golf (co)yoneda proofs

commit 16bd36d
Author: Matthew Ballard <matt@mrb.email>
Date:   Mon Feb 27 12:53:09 2023 -0500

    remove extra instances

commit 21f6296
Merge: 1985f48 5107462
Author: Matthew Ballard <matt@mrb.email>
Date:   Mon Feb 27 06:47:34 2023 -0500

    Merge branch 'master' into port/CategoryTheory.Limits.HasLimits

commit 1985f48
Author: Matthew Ballard <matt@mrb.email>
Date:   Mon Feb 27 06:46:53 2023 -0500

    add updated dependencies

commit d862b81
Author: Matthew Ballard <matt@mrb.email>
Date:   Fri Feb 24 21:42:30 2023 -0500

    fix long line

commit 51660c6
Author: Matthew Ballard <matt@mrb.email>
Date:   Fri Feb 24 21:39:24 2023 -0500

    change X to pt

commit e708679
Author: Matthew Ballard <matt@mrb.email>
Date:   Fri Feb 24 21:30:52 2023 -0500

    revert one more

commit 69b5d00
Author: Matthew Ballard <matt@mrb.email>
Date:   Fri Feb 24 21:30:10 2023 -0500

    fix rebase

commit 5f289c1
Author: Matthew Ballard <matt@mrb.email>
Date:   Fri Feb 24 20:52:34 2023 -0500

    fix import file

commit d3d56ee
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Feb 21 23:16:12 2023 -0500

    move names to new convention

commit 9dfd1d9
Author: Matthew Ballard <matt@mrb.email>
Date:   Tue Feb 21 23:02:58 2023 -0500

    add updated files

commit 90d60fc
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Feb 19 19:19:52 2023 -0500

    fix case error

commit 6979193
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Feb 19 00:02:32 2023 -0500

    fix import line typo

commit 843cf69
Author: Matthew Ballard <matt@mrb.email>
Date:   Sat Feb 18 23:52:06 2023 -0500

    fix import file

commit 4534cda
Author: Matthew Ballard <matt@mrb.email>
Date:   Sat Feb 18 23:51:22 2023 -0500

    align names in comments

commit 4dfea81
Author: Matthew Ballard <matt@mrb.email>
Date:   Sat Feb 18 23:38:31 2023 -0500

    lint for CI

commit 6373462
Author: Matthew Ballard <matt@mrb.email>
Date:   Sat Feb 18 23:28:31 2023 -0500

    try fix-comments.py

    only fixed a single issue for the second time now

commit a45d823
Author: Matthew Ballard <matt@mrb.email>
Date:   Sat Feb 18 23:26:14 2023 -0500

    fix final error

commit f7dcf96
Author: Matthew Ballard <matt@mrb.email>
Date:   Sat Feb 18 23:22:54 2023 -0500

    fix all but one decl

commit 2f25984
Author: Matthew Ballard <matt@mrb.email>
Date:   Fri Feb 24 20:50:11 2023 -0500

    automated fixes

    Mathbin -> Mathlib

    fix certain import statements

    move "by" to end of line

    add import to Mathlib.lean

commit f1c2148
Author: Matthew Ballard <matt@mrb.email>
Date:   Fri Feb 24 20:49:48 2023 -0500

    automated fixes

    Mathbin -> Mathlib

    fix certain import statements

    move "by" to end of line

    add import to Mathlib.lean

commit 8fcb216
Author: Matthew Ballard <matt@mrb.email>
Date:   Sat Feb 18 21:19:06 2023 -0500

    # This is a combination of 126 commits.
    # This is the 1st commit message:

    automated fixes

    Mathbin -> Mathlib

    fix certain import statements

    move "by" to end of line

    add import to Mathlib.lean

    # The commit message #2 will be skipped:

    # feat: port CategoryTheory.Limits.IsLimit

    # The commit message #3 will be skipped:

    # Initial file copy from mathport

    # The commit message #4 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #5 will be skipped:

    # feat: port CategoryTheory.Limits.Cones

    # The commit message #6 will be skipped:

    # Initial file copy from mathport

    # The commit message #7 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #8 will be skipped:

    # feat: port CategoryTheory.Yoneda

    # The commit message #9 will be skipped:

    # Initial file copy from mathport

    # The commit message #10 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #11 will be skipped:

    # feat: port CategoryTheory.Functor.Currying

    # The commit message #12 will be skipped:

    # Initial file copy from mathport

    # The commit message #13 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #14 will be skipped:

    # fix all but one decl

    # The commit message #15 will be skipped:

    # fix last errors

    # The commit message #16 will be skipped:

    # feat: port CategoryTheory.Functor.Hom

    # The commit message #17 will be skipped:

    # Initial file copy from mathport

    # The commit message #18 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #19 will be skipped:

    # feat: port CategoryTheory.Types

    # The commit message #20 will be skipped:

    # Initial file copy from mathport

    # The commit message #21 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #22 will be skipped:

    # feat: port CategoryTheory.EpiMono

    # The commit message #23 will be skipped:

    # Initial file copy from mathport

    # The commit message #24 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #25 will be skipped:

    # feat: port CategoryTheory.Groupoid

    # The commit message #26 will be skipped:

    # Initial file copy from mathport

    # The commit message #27 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #28 will be skipped:

    # feat: port CategoryTheory.Pi.Basic

    # The commit message #29 will be skipped:

    # Initial file copy from mathport

    # The commit message #30 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #31 will be skipped:

    # fix some errors

    # The commit message #32 will be skipped:

    # some more fixes

    # The commit message #33 will be skipped:

    # more fixes

    # The commit message #34 will be skipped:

    # finally fixed

    # The commit message #35 will be skipped:

    # lint

    # The commit message #36 will be skipped:

    # add porting note for scary warning

    # The commit message #37 will be skipped:

    # add porting note about proliferation of match

    # The commit message #38 will be skipped:

    # initial pass

    # The commit message #39 will be skipped:

    # fix errors

    # The commit message #40 will be skipped:

    # lint

    # The commit message #41 will be skipped:

    # fix errors; lint; add porting notes

    # The commit message #42 will be skipped:

    # fix errors; lint; add porting note

    # The commit message #43 will be skipped:

    # fix error

    # The commit message #44 will be skipped:

    # fix some errors

    # The commit message #45 will be skipped:

    # minor fixes

    # The commit message #46 will be skipped:

    # fix all but four

    # The commit message #47 will be skipped:

    # fix last errors; lint

    # The commit message #48 will be skipped:

    # feat: port CategoryTheory.DiscreteCategory

    # The commit message #49 will be skipped:

    # Initial file copy from mathport

    # The commit message #50 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #51 will be skipped:

    # get file to build

    # The commit message #52 will be skipped:

    # lint

    # The commit message #53 will be skipped:

    # lint some more

    # The commit message #54 will be skipped:

    # feat: port CategoryTheory.Functor.ReflectsIsomorphisms

    # The commit message #55 will be skipped:

    # Initial file copy from mathport

    # The commit message #56 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #57 will be skipped:

    # feat: port CategoryTheory.Functor.EpiMono

    # The commit message #58 will be skipped:

    # Initial file copy from mathport

    # The commit message #59 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #60 will be skipped:

    # feat: port CategoryTheory.LiftingProperties.Adjunction

    # The commit message #61 will be skipped:

    # Initial file copy from mathport

    # The commit message #62 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #63 will be skipped:

    # feat: port CategoryTheory.LiftingProperties.Basic

    # The commit message #64 will be skipped:

    # Initial file copy from mathport

    # The commit message #65 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #66 will be skipped:

    # feat: port CategoryTheory.CommSq

    # The commit message #67 will be skipped:

    # Initial file copy from mathport

    # The commit message #68 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #69 will be skipped:

    # first pass

    # The commit message #70 will be skipped:

    # names and removing restate_axiom

    # The commit message #71 will be skipped:

    # fix lint

    # The commit message #72 will be skipped:

    # remove spurious edit

    # The commit message #73 will be skipped:

    # fix errors; lint

    # The commit message #74 will be skipped:

    # feat: port CategoryTheory.Adjunction.Basic

    # The commit message #75 will be skipped:

    # Initial file copy from mathport

    # The commit message #76 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #77 will be skipped:

    # Initial file copy from mathport

    # The commit message #78 will be skipped:

    # Mathbin -> Mathlib; add import to Mathlib.lean

    # The commit message #79 will be skipped:

    # push it as far as possible

    # The commit message #80 will be skipped:

    # minor changes

    # The commit message #81 will be skipped:

    # seems to work

    # The commit message #82 will be skipped:

    # add example and equivalence file for testing

    # The commit message #83 will be skipped:

    # test: create `slice.lean` test file

    # The commit message #84 will be skipped:

    # remove equivalence.lean

    # The commit message #85 will be skipped:

    # remove rewriteTarget'; change MonadExceptOf to MonadExcept

    # The commit message #86 will be skipped:

    # add documentation and clean up

    # The commit message #87 will be skipped:

    # move iteration tactics to core

    # The commit message #88 will be skipped:

    # modify documentation lines

    # The commit message #89 will be skipped:

    # add module documentation(?)

    # The commit message #90 will be skipped:

    # fix module docs

    # The commit message #91 will be skipped:

    # fix test/slice.lean

    # The commit message #92 will be skipped:

    # fix all but refl error

    # The commit message #93 will be skipped:

    # fix refl error and lint errors

    # The commit message #94 will be skipped:

    # fix final long line

    # The commit message #95 will be skipped:

    # use `Mathport` syntax
    # * use existing docs
    # * fix docs typos

    # The commit message #96 will be skipped:

    # test: add simple `rhs`/`lhs` tests

    # The commit message #97 will be skipped:

    # minor changes to `Tactic.Core`
    # * use `m` instead of `TacticM` now that we use `MonadExcept`
    # * simplify code for `iterateRange`
    # * minor docs tweaks

    # The commit message #98 will be skipped:

    # update slice naming

    # The commit message #99 will be skipped:

    # some progress

    # The commit message #100 will be skipped:

    # only one error left

    # The commit message #101 will be skipped:

    # filled in last sorry

    # The commit message #102 will be skipped:

    # break long lines

    # The commit message #103 will be skipped:

    # delete linter command

    # The commit message #104 will be skipped:

    # fix comments

    # The commit message #105 will be skipped:

    # fix two simpNF lints

    # The commit message #106 will be skipped:

    # fill in some docstrings

    # The commit message #107 will be skipped:

    # fix most linter issues

    # The commit message #108 will be skipped:

    # add missing aligns for fields; lint

    # The commit message #109 will be skipped:

    # restore lost import line

    # The commit message #110 will be skipped:

    # fix errors; lint

    # The commit message #111 will be skipped:

    # feat: port CategoryTheory.Limits.Shapes.StrongEpi

    # The commit message #112 will be skipped:

    # Initial file copy from mathport

    # The commit message #113 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

    # The commit message #114 will be skipped:

    # fix errors; lint

    # The commit message #115 will be skipped:

    # Update Mathlib.lean

    # The commit message #116 will be skipped:

    # fix errors; lint

    # The commit message #117 will be skipped:

    # fix errors; lint; shorten filename

    # The commit message #118 will be skipped:

    # fix some errors

    # The commit message #119 will be skipped:

    # fix some more

    # The commit message #120 will be skipped:

    # fix errors

    # The commit message #121 will be skipped:

    # lint

    # The commit message #122 will be skipped:

    # fix errors

    # The commit message #123 will be skipped:

    # lint

    # The commit message #124 will be skipped:

    # feat: port CategoryTheory.Category.Ulift

    # The commit message #125 will be skipped:

    # Initial file copy from mathport

    # The commit message #126 will be skipped:

    # automated fixes
    #
    # Mathbin -> Mathlib
    #
    # fix certain import statements
    #
    # move "by" to end of line
    #
    # add import to Mathlib.lean

commit e22a9d9
Author: Matthew Ballard <matt@mrb.email>
Date:   Sat Feb 18 21:19:06 2023 -0500

    Initial file copy from mathport

commit f875c67
Author: Matthew Ballard <matt@mrb.email>
Date:   Sat Feb 18 21:19:06 2023 -0500

    feat: port CategoryTheory.Limits.HasLimits
mattrobball added a commit that referenced this pull request Mar 1, 2023
@mattrobball
# This is a combination of 87 commits.
5b01e46 
# This is the 1st commit message:

automated fixes

Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean

# The commit message #2 will be skipped:

# feat: port CategoryTheory.Limits.HasLimits

# The commit message #3 will be skipped:

# Initial file copy from mathport

# The commit message #4 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #5 will be skipped:

# feat: port CategoryTheory.Limits.IsLimit

# The commit message #6 will be skipped:

# Initial file copy from mathport

# The commit message #7 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #8 will be skipped:

# feat: port CategoryTheory.Limits.Cones

# The commit message #9 will be skipped:

# Initial file copy from mathport

# The commit message #10 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #11 will be skipped:

# feat: port CategoryTheory.Yoneda

# The commit message #12 will be skipped:

# Initial file copy from mathport

# The commit message #13 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #14 will be skipped:

# feat: port CategoryTheory.Functor.Currying

# The commit message #15 will be skipped:

# Initial file copy from mathport

# The commit message #16 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #17 will be skipped:

# fix all but one decl

# The commit message #18 will be skipped:

# fix last errors

# The commit message #19 will be skipped:

# feat: port CategoryTheory.Functor.Hom

# The commit message #20 will be skipped:

# Initial file copy from mathport

# The commit message #21 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #22 will be skipped:

# feat: port CategoryTheory.Types

# The commit message #23 will be skipped:

# Initial file copy from mathport

# The commit message #24 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #25 will be skipped:

# feat: port CategoryTheory.EpiMono

# The commit message #26 will be skipped:

# Initial file copy from mathport

# The commit message #27 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #28 will be skipped:

# feat: port CategoryTheory.Groupoid

# The commit message #29 will be skipped:

# Initial file copy from mathport

# The commit message #30 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #31 will be skipped:

# feat: port CategoryTheory.Pi.Basic

# The commit message #32 will be skipped:

# Initial file copy from mathport

# The commit message #33 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #34 will be skipped:

# fix some errors

# The commit message #35 will be skipped:

# some more fixes

# The commit message #36 will be skipped:

# more fixes

# The commit message #37 will be skipped:

# finally fixed

# The commit message #38 will be skipped:

# lint

# The commit message #39 will be skipped:

# add porting note for scary warning

# The commit message #40 will be skipped:

# add porting note about proliferation of match

# The commit message #41 will be skipped:

# initial pass

# The commit message #42 will be skipped:

# fix errors

# The commit message #43 will be skipped:

# lint

# The commit message #44 will be skipped:

# fix errors; lint; add porting notes

# The commit message #45 will be skipped:

# fix errors; lint; add porting note

# The commit message #46 will be skipped:

# fix error

# The commit message #47 will be skipped:

# fix some errors

# The commit message #48 will be skipped:

# minor fixes

# The commit message #49 will be skipped:

# fix all but four

# The commit message #50 will be skipped:

# Delete start_port-macos.sh

# The commit message #51 will be skipped:

# fix last errors; lint

# The commit message #52 will be skipped:

# feat: port CategoryTheory.DiscreteCategory

# The commit message #53 will be skipped:

# Initial file copy from mathport

# The commit message #54 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #55 will be skipped:

# get file to build

# The commit message #56 will be skipped:

# lint

# The commit message #57 will be skipped:

# lint some more

# The commit message #58 will be skipped:

# feat: port CategoryTheory.Functor.ReflectsIsomorphisms

# The commit message #59 will be skipped:

# Initial file copy from mathport

# The commit message #60 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #61 will be skipped:

# feat: port CategoryTheory.Functor.EpiMono

# The commit message #62 will be skipped:

# Initial file copy from mathport

# The commit message #63 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #64 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Adjunction

# The commit message #65 will be skipped:

# Initial file copy from mathport

# The commit message #66 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #67 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Basic

# The commit message #68 will be skipped:

# Initial file copy from mathport

# The commit message #69 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #70 will be skipped:

# feat: port CategoryTheory.CommSq

# The commit message #71 will be skipped:

# Initial file copy from mathport

# The commit message #72 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #73 will be skipped:

# first pass

# The commit message #74 will be skipped:

# names and removing restate_axiom

# The commit message #75 will be skipped:

# fix lint

# The commit message #76 will be skipped:

# remove spurious edit

# The commit message #77 will be skipped:

# fix errors; lint

# The commit message #78 will be skipped:

# feat: port CategoryTheory.Adjunction.Basic

# The commit message #79 will be skipped:

# Initial file copy from mathport

# The commit message #80 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #81 will be skipped:

# Initial file copy from mathport

# The commit message #82 will be skipped:

# Mathbin -> Mathlib; add import to Mathlib.lean

# The commit message #83 will be skipped:

# push it as far as possible

# The commit message #84 will be skipped:

# minor changes

# The commit message #85 will be skipped:

# seems to work

# The commit message #86 will be skipped:

# add example and equivalence file for testing

# The commit message #87 will be skipped:

# test: create `slice.lean` test file
Vierkantor added a commit to Vierkantor/mathlib4 that referenced this pull request Aug 4, 2025
@leanprover-community-bot-assistant @jrr6
@Rob23oba @jcommelin @kmill @kim-em @Vierkantor @kebekus @YaelDillies @bryangingechen @tydeu
chore: adaptations for nightly-2025-07-29 (leanprover-community#23)
3740955 
* Update lean-toolchain for testing leanprover/lean4#9084

* Update lean-toolchain for leanprover/lean4#9084

* Update lean-toolchain for testing leanprover/lean4#9423

* Update lean-toolchain for testing leanprover/lean4#9424

* chore: update 'unknown identifier' test ouputs

* chore: update 'tactic failed' test outputs

* fix(scripts/create-adaptation-pr): improve find_remote (leanprover-community#26974)

The old one was a syntax error and would've found a `mathlib4-nightly-testing` remote as a `mathlib4` remote (due to substring); this one is a bit more strict and works at least on my machine :-)

* Merge master into nightly-testing

* Update lean-toolchain for leanprover/lean4#9423

* Update lean-toolchain for leanprover/lean4#9424

* chore: update tactic error test outputs

* Update lean-toolchain for leanprover/lean4#9423

* Merge master into nightly-testing

* Merge master into nightly-testing

* Update lean-toolchain for testing leanprover/lean4#9443

* fixes

* fixes

* Merge master into nightly-testing

* Merge master into nightly-testing

* fix

* chore: bump to nightly-2025-07-22

* Merge master into nightly-testing

* adaptation notes for breakages in batteries

* update Cache

* fix

* lake update

* Merge master into nightly-testing

* deprecation

* fixes for Shake

* shake

* shake --update

* fix noisy build detection

* Merge master into nightly-testing

* chore: bump to nightly-2025-07-23

* Merge master into nightly-testing

* Merge master into nightly-testing

* fix

* revert commenting out

* fix noisy test

* Merge master into nightly-testing

* Merge master into nightly-testing

* chore: bump to nightly-2025-07-24

* Merge master into nightly-testing

* Merge master into nightly-testing

* Merge master into nightly-testing

* fixes for changes to Lean.Grind.NatModule

* oops

* Merge master into nightly-testing

* chore: bump to nightly-2025-07-25

* fix

* fix(scripts/create-adaption-pr.sh): fetch `master` if necessary (leanprover-community#27293)

Makes sure that `master` is available, in particular when the remote has been automatically added.

* chore: make create-adapation-pr.sh robust to running on nightly-testing fork (leanprover-community#27411)

cf recent failures at [#nightly-testing > Mathlib bump branch reminders @ 💬](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Mathlib.20bump.20branch.20reminders/near/530460702)

* fix da script

* `lake exe mk_all`

* hmm let's see what breaks

* not these

* hmm..?

* hmm this one as well

* more changes that turn out to be necessary

* Restore files from testing/nightly-testing

* Restore files from testing/nightly-testing

* Restore files from testing/nightly-testing

* Revert accidentals

* `mk_all`

* fix `@[to_additive]`

* Restore files from testing/nightly-testing

* re-add changes

* restore some more stuff carefully

* these

* try fix things

* chore: bump to nightly-2025-07-26

* fix by restoring mathlib change

* restore master versions of mis-merged files

* restore master versions of mis-merged files

* fix merge

* comment out with adaptation note

* huh?

* lake update

* lake update

* fix import

* shaking

* shaking

* shaking

* chore: bump to nightly-2025-07-27

* lake update

* mk_all

* fix merges

* more missed changes (leanprover-community#18)

* Merge master into nightly-testing

* feat: establish examples of harmonic functions (leanprover-community#26844)

If `f : ℂ → F` is complex-differentiable, then show that `f` is harmonic. If `F = ℂ`, then so is its real part, imaginary part, and complex conjugate. If `f` has no zero, then `log ‖f‖` is harmonic.

This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. It is one of the ingredients in the proof of Jensen's Formula in complex analysis.

* chore: replace `Monoid.IsTorsionFree` with `IsMulTorsionFree` (leanprover-community#24311)

From Toric

* fix tests

---------

Co-authored-by: Stefan Kebekus <kebekus@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

* fix test (leanprover-community#19)

* last fix I swear

* unnecessary duplicate imports

* these are actual unused imports (because of core changes?)

* test fix

* chore: adaptations for nightly-2025-07-27

* chore: bump to nightly-2025-07-28

* grind lemma

* more

* chore(Cache): enable FRO cache (leanprover-community#17)

* chore: revert "enable FRO cache (leanprover-community#17)"

This reverts commit 1da13d9.

* Restore regression

* chore: adaptations for nightly-2025-07-28

* chore: adaptations for nightly-2025-07-28

* chore: adaptations for nightly-2025-07-28

* chore: adaptations for nightly-2025-07-28

* adaptation notes

* chore: bump to nightly-2025-07-29

* chore: adaptations for nightly-2025-07-29

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Co-authored-by: Stefan Kebekus <kebekus@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
mathlib-bors bot pushed a commit that referenced this pull request Nov 19, 2025
@bryangingechen
Bgc fix title check (#23)
6ff1da1 
* testing

* leanprover-community

* more testing

* fix

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

Reviewers

@kbuzzard kbuzzard kbuzzard left review comments

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@denayd @digama0 @avigad @kbuzzard