Skip to content

feat(Data/Subtype): port data/subtype.lean from mathlib3#29

Merged
gebner merged 1 commit intoleanprover-community:masterfrom
dwrensha:subtype
Aug 3, 2021
Merged

feat(Data/Subtype): port data/subtype.lean from mathlib3#29
gebner merged 1 commit intoleanprover-community:masterfrom
dwrensha:subtype

Conversation

@dwrensha
Copy link
Copy Markdown
Member

@dwrensha dwrensha commented Aug 1, 2021

Ports all of the items from mathlib3's data/subtype.lean and adds theorem heq_iff_eq in Data/Logic/Basic.lean.

@gebner
Copy link
Copy Markdown
Member

gebner commented Aug 3, 2021

Thanks! BTW, I'm not sure if you saw Mario's talk at FMM. But we're most likely replacing all of the manually ported files here by automatically ported ones later this year (using a tool like https://github.com/dselsam/mathport/).

If you're doing it just for fun or to learn Lean 4 or because you need the files for another project, then please by all means continue. But please be aware that we're probably going to delete everything here (except for the tactics).

@gebner gebner merged commit 191c247 into leanprover-community:master Aug 3, 2021
@dwrensha
Copy link
Copy Markdown
Member Author

dwrensha commented Aug 3, 2021 •
edited
Loading

Yes, I am aware that the plan is to use automation to port everything. I'm still motivated to work on manually porting things because:

  1. it's fun and educational,
  2. I'm impatient to start building mathlib-dependent things in Lean 4, and
  3. I'm not 100% confident that the automated porting effort will fully succeed, so it seems prudent to not put all of our eggs in that basket.

@dwrensha dwrensha deleted the subtype branch August 3, 2021 11:53
@digama0
Copy link
Copy Markdown
Member

digama0 commented Aug 3, 2021

@dwrensha By the way, I'll say what I said in that talk as well: If you are doing manual porting, I want you to pay particular attention to things that can't be done as easily in lean 4 or need a workaround, and post them as issues on the https://github.com/dselsam/mathport/ repo. This is one of the most important things we need to learn at this stage in order to make sure porting goes smoothly.

@dwrensha
Copy link
Copy Markdown
Member Author

dwrensha commented Aug 3, 2021

I've been leaving notes in the ported code where things are not completely straightforward, e.g.

mathlib4/Mathlib/Data/Subtype.lean

Line 138 in 7822926

Port note: we need explicit universes here because in Lean 3 we have

I don't think I have a good enough understanding of mathport to be able to translate these notes into issues to open there.

@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
kim-em added a commit that referenced this pull request Aug 15, 2025
@leanprover-community-bot-assistant @fgdorais
@jrr6 @Rob23oba @jcommelin @kmill @kim-em @Vierkantor @kebekus @YaelDillies @bryangingechen @tydeu @Kha @nomeata
chore: adaptations for nightly-2025-08-06 (#29)
3940fd5 
* Update lean-toolchain for leanprover/lean4#9084

* Update Batteries branch for testing leanprover-community/batteries#1306

* chore: adaptation to batteries#1306

* 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 (#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 (#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 (#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 (#18)

* Merge master into nightly-testing

* feat: establish examples of harmonic functions (#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` (#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 (#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

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

* grind lemma

* more

* chore(Cache): enable FRO cache (#17)

* chore: revert "enable FRO cache (#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

* fix; bad merge?

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

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

* deprecation

* Update lean-toolchain for leanprover/lean4#9633

* chore: update test error message outputs

* adaptation note about Xor'

* shake --update

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

* fix

* fix test output

* fix test output

* fix test output

* chore: bump to nightly-2025-08-01

* fix

* Update lean-toolchain for leanprover/lean4#9587

* chore: bump to nightly-2025-08-02

* Bump batteries

* Fix warning

* chore: bump to nightly-2025-08-03

* update test

* fix test

* fix merge?

* chore: bump to nightly-2025-08-04

* fix

* chore: bump to nightly-2025-08-05

* deprecations

* shake --fix

* fix imports

* remove Shake again?

* chore: bump to nightly-2025-08-06

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: F. G. Dorais <fgdorais@gmail.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>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Rob23oba added a commit to Rob23oba/mathlib4 that referenced this pull request Aug 24, 2025
@leanprover-community-bot-assistant @kim-em
@Kha @nomeata @fgdorais @jrr6 @Rob23oba @jcommelin @kmill @Vierkantor @kebekus @YaelDillies @bryangingechen @tydeu @datokrat
chore: adaptations for nightly-2025-08-17 (leanprover-community#37)
919bac0 
* fix test output

* fix test output

* fix test output

* chore: bump to nightly-2025-08-01

* fix

* Update lean-toolchain for leanprover/lean4#9587

* chore: bump to nightly-2025-08-02

* Bump batteries

* Fix warning

* chore: bump to nightly-2025-08-03

* update test

* fix test

* fix merge?

* chore: bump to nightly-2025-08-04

* fix

* chore: bump to nightly-2025-08-05

* deprecations

* shake --fix

* fix imports

* remove Shake again?

* chore: adaptations for nightly-2025-08-04 (leanprover-community#26)

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

* Update lean-toolchain for leanprover/lean4#9084

* Update Batteries branch for testing leanprover-community/batteries#1306

* chore: adaptation to batteries#1306

* 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

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

* 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

* fix; bad merge?

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

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

* deprecation

* Update lean-toolchain for leanprover/lean4#9633

* chore: update test error message outputs

* adaptation note about Xor'

* shake --update

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

* fix

* fix test output

* fix test output

* fix test output

* chore: bump to nightly-2025-08-01

* fix

* Update lean-toolchain for leanprover/lean4#9587

* chore: bump to nightly-2025-08-02

* Bump batteries

* Fix warning

* chore: bump to nightly-2025-08-03

* update test

* fix test

* fix merge?

* chore: bump to nightly-2025-08-04

* fix

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: F. G. Dorais <fgdorais@gmail.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>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

* remove Shake

* chore: adaptations for nightly-2025-08-05 (leanprover-community#27)

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

* Update lean-toolchain for leanprover/lean4#9084

* Update Batteries branch for testing leanprover-community/batteries#1306

* chore: adaptation to batteries#1306

* 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

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

* 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

* fix; bad merge?

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

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

* deprecation

* Update lean-toolchain for leanprover/lean4#9633

* chore: update test error message outputs

* adaptation note about Xor'

* shake --update

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

* fix

* fix test output

* fix test output

* fix test output

* chore: bump to nightly-2025-08-01

* fix

* Update lean-toolchain for leanprover/lean4#9587

* chore: bump to nightly-2025-08-02

* Bump batteries

* Fix warning

* chore: bump to nightly-2025-08-03

* update test

* fix test

* fix merge?

* chore: bump to nightly-2025-08-04

* fix

* chore: bump to nightly-2025-08-05

* deprecations

* shake --fix

* fix imports

* remove Shake again?

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: F. G. Dorais <fgdorais@gmail.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>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

* chore: bump to nightly-2025-08-06

* fix

* chore: adaptations for nightly-2025-08-06 (leanprover-community#29)

* Update lean-toolchain for leanprover/lean4#9084

* Update Batteries branch for testing leanprover-community/batteries#1306

* chore: adaptation to batteries#1306

* 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

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

* 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

* fix; bad merge?

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

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

* deprecation

* Update lean-toolchain for leanprover/lean4#9633

* chore: update test error message outputs

* adaptation note about Xor'

* shake --update

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

* fix

* fix test output

* fix test output

* fix test output

* chore: bump to nightly-2025-08-01

* fix

* Update lean-toolchain for leanprover/lean4#9587

* chore: bump to nightly-2025-08-02

* Bump batteries

* Fix warning

* chore: bump to nightly-2025-08-03

* update test

* fix test

* fix merge?

* chore: bump to nightly-2025-08-04

* fix

* chore: bump to nightly-2025-08-05

* deprecations

* shake --fix

* fix imports

* remove Shake again?

* chore: bump to nightly-2025-08-06

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: F. G. Dorais <fgdorais@gmail.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>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

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

* lake update aesop

* lake update aesop

* deprecations

* chore: bump to nightly-2025-08-08

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

* Update lean-toolchain for leanprover/lean4#9800

* Update lean-toolchain for leanprover/lean4#9800

* Update lean-toolchain for leanprover/lean4#9800

* addressing some cases of mathlib4#380

* fix tests

* Update lean-toolchain for leanprover/lean4#9800

* Update lean-toolchain for leanprover/lean4#9800

* chore: bump to nightly-2025-08-10

* fix (all?) `protected` regressions

* Update lean-toolchain for leanprover/lean4#9800

* fix

* adaptation note?

* noncomputable

* revert grind proof

* remove upstreamed

* fixes

* feat: better statement of flip_map_app

* sad adaptation note

* update adaptation note

* fix merge

* chore: bump to nightly-2025-08-11

* chore: adaptations for nightly-2025-08-11

* chore: adaptations for nightly-2025-08-11

* fixes

* fix

* fix toolchain?

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

* use legacy lemma for now

* revert bad changes

* upstream LE/LT (Subtype p) instances

* chore(Cache): use FRO cache (v2) (leanprover-community#30)

* chore(Cache): enable FRO cache

* feat: only print "packing" when actually packing

* feat: always prefix with repo in FRO cache

* fix

* chore: bump to nightly-2025-08-12

* chore: trigger rebuild to test cache

* chore: use `cache put!` in CI to debug

* shake --update

* chore: adaptations for nightly-2025-08-12

* empty

* chore: bump to nightly-2025-08-13

* Revert "chore: use `cache put!` in CI to debug"

This reverts commit 7c6202b.

* redundant grind warnings

* revert leanprover-community#28272: add back grind proofs

* fix test

* chore: adaptations for nightly-2025-08-13

* fixes

* restore test

* chore: bump to nightly-2025-08-14

* adaptation note about grind regression

* fix tests

* update test output

* chore: bump to nightly-2025-08-16

* bump proofwidgets

* bump proofwidgets

* chore: bump to nightly-2025-08-17

* chore: adaptations for nightly-2025-08-17

* Apply suggestions from code review

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: F. G. Dorais <fgdorais@gmail.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: 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: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
kim-em added a commit to kim-em/mathlib4 that referenced this pull request Aug 31, 2025
@leanprover-community-bot-assistant @kim-em
@fgdorais @jrr6 @Rob23oba @jcommelin @kmill @Vierkantor @kebekus @YaelDillies @bryangingechen @tydeu @Kha @nomeata @datokrat
chore: adaptations for nightly-2025-08-19 (leanprover-community#39)
ac321b0 
* chore: bump to nightly-2025-08-05

* deprecations

* shake --fix

* fix imports

* remove Shake again?

* chore: adaptations for nightly-2025-08-04 (leanprover-community#26)

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

* Update lean-toolchain for leanprover/lean4#9084

* Update Batteries branch for testing leanprover-community/batteries#1306

* chore: adaptation to batteries#1306

* 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

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

* 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

* fix; bad merge?

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

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

* deprecation

* Update lean-toolchain for leanprover/lean4#9633

* chore: update test error message outputs

* adaptation note about Xor'

* shake --update

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

* fix

* fix test output

* fix test output

* fix test output

* chore: bump to nightly-2025-08-01

* fix

* Update lean-toolchain for leanprover/lean4#9587

* chore: bump to nightly-2025-08-02

* Bump batteries

* Fix warning

* chore: bump to nightly-2025-08-03

* update test

* fix test

* fix merge?

* chore: bump to nightly-2025-08-04

* fix

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: F. G. Dorais <fgdorais@gmail.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>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

* remove Shake

* chore: adaptations for nightly-2025-08-05 (leanprover-community#27)

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

* Update lean-toolchain for leanprover/lean4#9084

* Update Batteries branch for testing leanprover-community/batteries#1306

* chore: adaptation to batteries#1306

* 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

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

* 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

* fix; bad merge?

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

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

* deprecation

* Update lean-toolchain for leanprover/lean4#9633

* chore: update test error message outputs

* adaptation note about Xor'

* shake --update

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

* fix

* fix test output

* fix test output

* fix test output

* chore: bump to nightly-2025-08-01

* fix

* Update lean-toolchain for leanprover/lean4#9587

* chore: bump to nightly-2025-08-02

* Bump batteries

* Fix warning

* chore: bump to nightly-2025-08-03

* update test

* fix test

* fix merge?

* chore: bump to nightly-2025-08-04

* fix

* chore: bump to nightly-2025-08-05

* deprecations

* shake --fix

* fix imports

* remove Shake again?

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: F. G. Dorais <fgdorais@gmail.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>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

* chore: bump to nightly-2025-08-06

* fix

* chore: adaptations for nightly-2025-08-06 (leanprover-community#29)

* Update lean-toolchain for leanprover/lean4#9084

* Update Batteries branch for testing leanprover-community/batteries#1306

* chore: adaptation to batteries#1306

* 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

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

* 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

* fix; bad merge?

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

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

* deprecation

* Update lean-toolchain for leanprover/lean4#9633

* chore: update test error message outputs

* adaptation note about Xor'

* shake --update

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

* fix

* fix test output

* fix test output

* fix test output

* chore: bump to nightly-2025-08-01

* fix

* Update lean-toolchain for leanprover/lean4#9587

* chore: bump to nightly-2025-08-02

* Bump batteries

* Fix warning

* chore: bump to nightly-2025-08-03

* update test

* fix test

* fix merge?

* chore: bump to nightly-2025-08-04

* fix

* chore: bump to nightly-2025-08-05

* deprecations

* shake --fix

* fix imports

* remove Shake again?

* chore: bump to nightly-2025-08-06

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: F. G. Dorais <fgdorais@gmail.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>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

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

* lake update aesop

* lake update aesop

* deprecations

* chore: bump to nightly-2025-08-08

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

* Update lean-toolchain for leanprover/lean4#9800

* Update lean-toolchain for leanprover/lean4#9800

* Update lean-toolchain for leanprover/lean4#9800

* addressing some cases of mathlib4#380

* fix tests

* Update lean-toolchain for leanprover/lean4#9800

* Update lean-toolchain for leanprover/lean4#9800

* chore: bump to nightly-2025-08-10

* fix (all?) `protected` regressions

* Update lean-toolchain for leanprover/lean4#9800

* fix

* adaptation note?

* noncomputable

* revert grind proof

* remove upstreamed

* fixes

* feat: better statement of flip_map_app

* sad adaptation note

* update adaptation note

* fix merge

* chore: bump to nightly-2025-08-11

* chore: adaptations for nightly-2025-08-11

* chore: adaptations for nightly-2025-08-11

* fixes

* fix

* fix toolchain?

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

* use legacy lemma for now

* revert bad changes

* upstream LE/LT (Subtype p) instances

* chore(Cache): use FRO cache (v2) (leanprover-community#30)

* chore(Cache): enable FRO cache

* feat: only print "packing" when actually packing

* feat: always prefix with repo in FRO cache

* fix

* chore: bump to nightly-2025-08-12

* chore: trigger rebuild to test cache

* chore: use `cache put!` in CI to debug

* shake --update

* chore: adaptations for nightly-2025-08-12

* empty

* chore: bump to nightly-2025-08-13

* Revert "chore: use `cache put!` in CI to debug"

This reverts commit 7c6202b.

* redundant grind warnings

* revert leanprover-community#28272: add back grind proofs

* fix test

* chore: adaptations for nightly-2025-08-13

* fixes

* restore test

* chore: bump to nightly-2025-08-14

* adaptation note about grind regression

* fix tests

* update test output

* feat: workflow for reporting `grind` regressions

This PR contains a (untested!) workflow that is supposed to build Mathlib with a few tactic analysis flags. It reports the results of these build steps to Zulip for the FRO (and in particular Kim).

* chore: bump to nightly-2025-08-16

* bump proofwidgets

* bump proofwidgets

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

* chore: bump to nightly-2025-08-17

* chore: adaptations for nightly-2025-08-17

* Update lean-toolchain for leanprover/lean4#9942

* Update lean-toolchain for leanprover/lean4#9942

* make `filter_upwards` more robust to side goals

* Update lean-toolchain for leanprover/lean4#9674

* simpler change to filter_upwards

* chore: bump to nightly-2025-08-18

* Apply suggestions from code review

* Use JS to generate uuid instead of uuidgen which appears not to be installed

* GH Problem Matcher wrapper doesn't like multiline arguments; wrap multiple steps instead.

* Hmm, maybe uuidgen exists and it was gh-problem-matcher that was the issue?

* Can we just `apt install` dependencies?

* Apparently Linux exposes uuids from the kernel. Nifty!

* Then we don't need to install uuidgen

* Try also implementing a docgen step for nightly testing

* Cut off the output after 9k bytes, otherwise Zulip complains

* Fixes

* chore: bump to nightly-2025-08-19

* Filter out the build progress lines.

* Switch `doc-gen4` version to "main", otherwise it complains there is no nightly-testing release.

* lake update

* cleanup imports

* Fix `git remote` complaining that `nightly-testing` already exists.

* Fix error message.

* fix tests

* shake --fix

* satisfy actionlint

* shellcheck

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: F. G. Dorais <fgdorais@gmail.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: 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: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@dwrensha @gebner @digama0