Skip to content

feat(Set): port Lean 3 init.data.set#8

Merged
gebner merged 5 commits intoleanprover-community:masterfrom
kbuzzard:set
May 25, 2021
Merged

feat(Set): port Lean 3 init.data.set#8
gebner merged 5 commits intoleanprover-community:masterfrom
kbuzzard:set

Conversation

@kbuzzard
Copy link
Copy Markdown
Member

@kbuzzard kbuzzard commented May 23, 2021

I define the Mem notation typeclass and then port the core Lean 3 set file
lib/lean/library/init/data/set.lean.

gebner
gebner reviewed May 25, 2021
View reviewed changes
kbuzzard
kbuzzard commented May 25, 2021
View reviewed changes
@gebner gebner merged commit 50610c3 into leanprover-community:master May 25, 2021
@shingtaklam1324 shingtaklam1324 mentioned this pull request May 26, 2021
Merged
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 Jun 30, 2025
@kim-em @jcommelin
@sgouezel @kmill @Kha @Rob23oba @chrisflav @kckennylau @fbarroero @zwarich @tydeu @Vierkantor @nomeata @jrr6
chore: adaptations for nightly-2025-06-30 (#8)
df47d57 
* cleanup grind tests

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

* merge lean-pr-testing-8419

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

* merge lean-pr-testing-8653

* adaptation note

* oops

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

* remove nolint simpNF

* remove spurious file

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

* fix

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

* Merge master into nightly-testing

* fix

* remove upstreamed

* drop no-op `show`

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

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

* intentionally left blank

* fix tests

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

* fix upstream

* fix

* fix

* fixes

* chore: adaptations for nightly-2025-06-16

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

* fixes

* more fixes

* fixes!

* more fixes!

* hmm

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

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

* chore: lint `show` (adaptation for leanprover/lean4#7395) (#25749)

Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`.
Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633

Co-authored-by: Christian Merten <christian@merten.dev>
Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>

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

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

* chore: adaptations for nightly-2025-06-18

* Merge master into nightly-testing

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

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

* bump Qq and batteries

* meta adaptations

* bump aesop

* fix

* fix (adaptation note)

* Update lean-toolchain for leanprover/lean4#8699

* shake

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

* fix

* Update lean-toolchain for leanprover/lean4#8699

* fix: correct memoFix's use of unsafe code

* fix: adjust noncomputable annotations for new compiler

* fix: replace use of `open private _ in` with `open private _ from`

The implementation of `open private _ from` relies on specific
internals of the old compiler and will no longer work.

* remove mul_hmul

* chore: adjust one maxHeartbeats for the new compiler

* linter

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

* chore: adaptations for nightly-2025-06-20

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

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

* fix

* fixes

* fixes

* fixes

* updated lake manifest

* comment out tests

* chore: fix for nightly-testing (#26246)

* fix

* fix

* fix grind typeclasses

* chore: adaptations for nightly-2025-06-20

* lake update

* Update lean-toolchain for leanprover/lean4#8914

* fix grind instance

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

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

* chore: rm unused `Lean.Util.Paths` import & use updated batteries

* Ensure we checkout mathlib4 master, not nightly-testing master (which does not exist)

* merge lean-pr-testing-8804

* Bump dependencies and silence linter.

* Fixes

(Now `elabSimpArgs` already handles `*`, so we can delete the associated code.)

* lake update; disable unusedSimpArgs in Batteries

* lkae update aesop

* disable unusedSimpArgs in MathlibTest

* fix grind instance priorities

* comment out MathlibTest/zmod with adaptation note

* touch for CI

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

* Kick CI

* Bump batteries

* Guessing adaption for leanprover/lean4#8929

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

* fix: workflow merging master into nightly-testing

* fix

* chore: cache get uses tracking remote

* touch for new CI

* restart CI

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

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

* Teach Mathlib about `mrefine`

* Merge master into nightly-testing

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

* chore: update linter warning test outputs

* chore: remove excess line break in deprecation lint now that notes add their own line breaks

* chore: more test cleanup

* .

* cleanup adaptation notes

* fix

* fix

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

* Merge master into nightly-testing

* Merge master into nightly-testing

* re-enable unusedSimpArgs

* re-enable unusedSimpArgs

* re-enable unusedSimpArgs

* re-enable unusedSimpArgs

* re-enable unusedSimpArgs

* fix tests

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

* Merge master into nightly-testing

* lintining

* Merge master into nightly-testing

* unused simp args

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

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

* Merge master into nightly-testing

* chore: robustify `open Mathlib` benchmark

* deprecations

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

* Merge master into nightly-testing

* fixes

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

* lake update

* lake update

* lake update

* lake update

* lake update

* .

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Rob23oba <101damnations@github.com>
Co-authored-by: Christian Merten <christian@merten.dev>
Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com>
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Co-authored-by: Cameron Zwarich <cameron@lean-fro.org>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
kim-em added a commit that referenced this pull request Mar 3, 2026
@kim-em @claude
style(Tactic/InferInstanceAsPercent): fix docstring indentation
d2a35d3 
Remove extra leading spaces on continuation lines of docstrings
to match mathlib convention (#8).

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
kim-em added a commit that referenced this pull request Mar 3, 2026
@kim-em @claude
style(Tactic/InferInstanceAsPercent): fix docstring indentation
299e855 
Remove extra leading spaces on continuation lines of docstrings
to match mathlib convention (#8).

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
kim-em added a commit that referenced this pull request Mar 12, 2026
@kim-em @claude
style(Tactic/InferInstanceAsPercent): fix docstring indentation
65471da 
Remove extra leading spaces on continuation lines of docstrings
to match mathlib convention (#8).

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@gebner gebner gebner left review comments

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@kbuzzard @gebner