Skip to content

[Merged by Bors] - feat(Tactic): finish implementation of iterate#96

Closed
kim-em wants to merge 5 commits intomasterfrom
semorrison/iterate
Closed

[Merged by Bors] - feat(Tactic): finish implementation of iterate#96
kim-em wants to merge 5 commits intomasterfrom
semorrison/iterate

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Nov 16, 2021 •
edited by bors bot
Loading

No description provided.

gebner
gebner reviewed Nov 16, 2021
View reviewed changes
kim-em
kim-em commented Nov 18, 2021
View reviewed changes
kim-em
kim-em commented Nov 18, 2021
View reviewed changes
Mathlib/Tactic/Basic.lean Outdated
Comment on lines +226 to +230
/--
`iterate n { ... }` runs the tactic block exactly `n` times.
`iterate { ... }` runs the tactic block repeatedly until failure.
-/
syntax (name := iterate) "iterate" (num)? ppSpace tacticSeq : tactic
Copy link
Copy Markdown
Contributor Author

@kim-em kim-em Nov 18, 2021

Choose a reason for hiding this comment

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

When using separate syntax and elab_rules or macro_rules, where should the tactic doc-string go?

@gebner
Copy link
Copy Markdown
Member

gebner commented Nov 23, 2021

bors r+

bors bot pushed a commit that referenced this pull request Nov 23, 2021
@kim-em
feat(Tactic): finish implementation of iterate (#96)
7b28b02 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Nov 23, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(Tactic): finish implementation of iterate [Merged by Bors] - feat(Tactic): finish implementation of iterate Nov 23, 2021
@bors bors bot closed this Nov 23, 2021
@bors bors bot deleted the semorrison/iterate branch November 23, 2021 08:59
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 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
mathlib-bors bot pushed a commit that referenced this pull request Mar 23, 2025
@eric-wieser @qawbecrdtey
feat: sumPiLpEquivProdLpPiLp (#22973)
ece3cec 
Zulip threads
* [#Is there code for X? > Product of Euclidean spaces @ 💬](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Product.20of.20Euclidean.20spaces/near/500124944)
* [#mathlib4 > Create &#96;LinearIsometryEquiv&#96; with &#96;WithLp 2 (α × β)&#96; and.. @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Create.20.60LinearIsometryEquiv.60.20with.20.60WithLp.202.20.28.CE.B1.20.C3.97.20.CE.B2.29.60.20and.2E.2E/near/505938119)



Co-authored-by: qawbecrdtey <qawbecrdtey@kaist.ac.kr>
mathlib-bors bot pushed a commit that referenced this pull request Mar 26, 2025
@eric-wieser
fix(Tactic/Use): do not allow unprotected cdot (#23257)
d825991 
Zulip thread: [#mathlib4 > &#96;use ·&#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60use.20.C2.B7.60/near/448279748)
mathlib-bors bot pushed a commit that referenced this pull request Mar 26, 2025
@eric-wieser
fix(Tactic/Use): do not allow unprotected cdot (#23257)
8623dd1 
Zulip thread: [#mathlib4 > &#96;use ·&#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60use.20.C2.B7.60/near/448279748)



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Paul-Lez pushed a commit that referenced this pull request Mar 27, 2025
@eric-wieser @Paul-Lez
fix(Tactic/Use): do not allow unprotected cdot (#23257)
f859726 
Zulip thread: [#mathlib4 > &#96;use ·&#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60use.20.C2.B7.60/near/448279748)



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
mathlib-bors bot pushed a commit that referenced this pull request Mar 31, 2025
@vasnesterov
fix(Tactic/Lift): replace simp at h h with simp at h (#23437)
4be83ef 
The `lift` tactic previously called `simp only [h_eq] at h h` instead of `simp only [h_eq] at h` when rewriting a local hypothesis `h` with `h_eq : old_value = ↑lifted_value`. This caused hypothesis duplication in some cases:  
[#mathlib4 > Bug in &#96;lift&#96; tactic? @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Bug.20in.20.60lift.60.20tactic.3F/near/508521400)  

This PR removes the second `h` in the `simp` call.
mathlib-bors bot pushed a commit that referenced this pull request Apr 14, 2025
@adomani
fix(deprecated module): automatically disable the header linter (#24027)
7e89760 
This PR makes the `header` linter silent if the first non-import command of a file is `deprecated_module`.

[Zulip#mathlib4 > &#96;Deprecated&#96; folder @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60Deprecated.60.20folder/near/511986519)
mathlib-bors bot pushed a commit that referenced this pull request Apr 15, 2025
@plp127 @eric-wieser
chore: rename fields of LinearOrder (#23976)
593c38c 
Renames `LinearOrder.decidable**` -> `LinearOrder.toDecidable**`, and same for `ConditionallyCompleteLinearOrder` and `CompleteLinearOrder`

See zulip message [#mathlib4 > extending &#96;RCLike&#96; and &#96;LinearOrder&#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/extending.20.60RCLike.60.20and.20.60LinearOrder.60/near/511047785)

Also fixes lots of potential diamonds caused by not specifying the `decidableEq` or `decidableLT` fields when creating an instance.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
mathlib-bors bot pushed a commit that referenced this pull request May 11, 2025
@wwylele
fix(Order): remove leftover OrderDual from `Set.isWF_iff_no_descend…
8be5607 
…ing_seq` (#24776)

From [#mathlib4 > Why does &#96;Set.isWF_iff_no_descending_seq&#96; takes order d...](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Why.20does.20.60Set.2EisWF_iff_no_descending_seq.60.20takes.20order.20d.2E.2E.2E/with/517314153)
mathlib-bors bot pushed a commit that referenced this pull request May 11, 2025
@wwylele
fix(Order): remove leftover OrderDual from `Set.isWF_iff_no_descend…
eee7898 
…ing_seq` (#24776)

From [#mathlib4 > Why does &#96;Set.isWF_iff_no_descending_seq&#96; takes order d...](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Why.20does.20.60Set.2EisWF_iff_no_descending_seq.60.20takes.20order.20d.2E.2E.2E/with/517314153)
mathlib-bors bot pushed a commit that referenced this pull request May 12, 2025
@eric-wieser
feat: Equiv.functionSwap (#24821)
2d404f1 
[#Is there code for X? > Equiv version of &#96;function.swap&#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Equiv.20version.20of.20.60function.2Eswap.60/near/285460783)
tannerduve pushed a commit that referenced this pull request May 13, 2025
@adomani @tannerduve
fix(deprecated module): automatically disable the header linter (#24027)
d242f81 
This PR makes the `header` linter silent if the first non-import command of a file is `deprecated_module`.

[Zulip#mathlib4 > &#96;Deprecated&#96; folder @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60Deprecated.60.20folder/near/511986519)
tannerduve pushed a commit that referenced this pull request May 13, 2025
@plp127 @eric-wieser @tannerduve
chore: rename fields of LinearOrder (#23976)
800ba20 
Renames `LinearOrder.decidable**` -> `LinearOrder.toDecidable**`, and same for `ConditionallyCompleteLinearOrder` and `CompleteLinearOrder`

See zulip message [#mathlib4 > extending &#96;RCLike&#96; and &#96;LinearOrder&#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/extending.20.60RCLike.60.20and.20.60LinearOrder.60/near/511047785)

Also fixes lots of potential diamonds caused by not specifying the `decidableEq` or `decidableLT` fields when creating an instance.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
tannerduve pushed a commit that referenced this pull request May 13, 2025
@wwylele @tannerduve
fix(Order): remove leftover OrderDual from `Set.isWF_iff_no_descend…
7643ebd 
…ing_seq` (#24776)

From [#mathlib4 > Why does &#96;Set.isWF_iff_no_descending_seq&#96; takes order d...](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Why.20does.20.60Set.2EisWF_iff_no_descending_seq.60.20takes.20order.20d.2E.2E.2E/with/517314153)
mathlib-bors bot pushed a commit that referenced this pull request Jul 15, 2025
@alreadydone
fix(Topology/Covering): switch to standard definition (#24983)
3d1fc47 
As discussed in [#mathlib4 > edge cases not covered by &#96;IsCoveringMap&#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/edge.20cases.20not.20covered.20by.20.60IsCoveringMap.60/near/518413081), the previous definition doesn't include examples like the inclusion of a one-point space into a two-point discrete space.
BeibeiX0 pushed a commit to BeibeiX0/mathlib4 that referenced this pull request Jul 16, 2025
@eric-wieser @BeibeiX0
chore: remove space after ⅟ (leanprover-community#26997)
e10972e 
This will change how the docs and infoview render, and the rules for the upcoming whitespace linter.

Zulip thread: [#mathlib4 > Space after &leanprover-community#96;⅟ &leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Space.20after.20.60.E2.85.9F.20.60/near/528309060)



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
BeibeiX0 pushed a commit to BeibeiX0/mathlib4 that referenced this pull request Jul 16, 2025
@alreadydone @BeibeiX0
fix(Topology/Covering): switch to standard definition (leanprover-com…
d95f033 
…munity#24983)

As discussed in [#mathlib4 > edge cases not covered by &leanprover-community#96;IsCoveringMap&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/edge.20cases.20not.20covered.20by.20.60IsCoveringMap.60/near/518413081), the previous definition doesn't include examples like the inclusion of a one-point space into a two-point discrete space.
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
@grunweg @callesonne
feat: EuclideanSpace.finAddEquivProd (leanprover-community#26086)
6ef05ea 
I need this for leanprover-community#25505 (to show that R^n is a submanifold of R^m for n \leq m) and for my bordism theory branch.

Previous zulip discussions:
- [#Is there code for X? > Product of Euclidean spaces @ 💬](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Product.20of.20Euclidean.20spaces/near/500124944)
- [#mathlib4 > Create &leanprover-community#96;LinearIsometryEquiv&leanprover-community#96; with &leanprover-community#96;WithLp 2 (α × β)&leanprover-community#96; and.. @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Create.20.60LinearIsometryEquiv.60.20with.20.60WithLp.202.20.28.CE.B1.20.C3.97.20.CE.B2.29.60.20and.2E.2E/near/505938119)
- [#mathlib4 > Manifold structure on Moebius strip @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Manifold.20structure.20on.20Moebius.20strip/near/522156122)

Co-authored-by: @peabrainiac
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
@eric-wieser @YaelDillies @callesonne
chore: split WithLp.equiv into a new pair WithLp.toLp/`WithLp.ofL…
f2df34f 
…p` (leanprover-community#26459)

`(WithLp.equiv p _).symm v` is very inconvenient as a normal form when working with `WithLp`.

This introduces `WithLp.toLp p v` as the simp-normal spelling of this operation, and `v'.ofLp` as the simp-normal spelling of `WithLp.equiv p _ v'`. It then deprecates almost all the lemmas about `WithLp.equiv`, as these are no longer stated in simp-normal form.

The motivation for making `toLp` and `ofLp` as plain functions, as opposed to `Equiv`s, is to permit them to be later adapted into a constructor and projection of a one-field structure. Almost nothing in mathlib needs them to be equivs anyway.

Zulip thread: [#mathlib4 > defeq abuse in &leanprover-community#96;WithLp&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/defeq.20abuse.20in.20.60WithLp.60/near/516241777)

Co-authored-by: Yael Dillies <yael.dillies@gmail.com>
Co-authored-by: Paul Lezeau <paul.lezeau@gmail.com>



Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
@eric-wieser @callesonne
chore: remove space after ⅟ (leanprover-community#26997)
2049769 
This will change how the docs and infoview render, and the rules for the upcoming whitespace linter.

Zulip thread: [#mathlib4 > Space after &leanprover-community#96;⅟ &leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Space.20after.20.60.E2.85.9F.20.60/near/528309060)



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
@alreadydone @callesonne
fix(Topology/Covering): switch to standard definition (leanprover-com…
43d26ab 
…munity#24983)

As discussed in [#mathlib4 > edge cases not covered by &leanprover-community#96;IsCoveringMap&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/edge.20cases.20not.20covered.20by.20.60IsCoveringMap.60/near/518413081), the previous definition doesn't include examples like the inclusion of a one-point space into a two-point discrete space.
hrmacbeth pushed a commit to szqzs/mathlib4 that referenced this pull request Jul 28, 2025
@eric-wieser @YaelDillies @hrmacbeth
chore: split WithLp.equiv into a new pair WithLp.toLp/`WithLp.ofL…
5a261b0 
…p` (leanprover-community#26459)

`(WithLp.equiv p _).symm v` is very inconvenient as a normal form when working with `WithLp`.

This introduces `WithLp.toLp p v` as the simp-normal spelling of this operation, and `v'.ofLp` as the simp-normal spelling of `WithLp.equiv p _ v'`. It then deprecates almost all the lemmas about `WithLp.equiv`, as these are no longer stated in simp-normal form.

The motivation for making `toLp` and `ofLp` as plain functions, as opposed to `Equiv`s, is to permit them to be later adapted into a constructor and projection of a one-field structure. Almost nothing in mathlib needs them to be equivs anyway.

Zulip thread: [#mathlib4 > defeq abuse in &leanprover-community#96;WithLp&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/defeq.20abuse.20in.20.60WithLp.60/near/516241777)

Co-authored-by: Yael Dillies <yael.dillies@gmail.com>
Co-authored-by: Paul Lezeau <paul.lezeau@gmail.com>



Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
hrmacbeth pushed a commit to szqzs/mathlib4 that referenced this pull request Jul 28, 2025
@eric-wieser @hrmacbeth
chore: remove space after ⅟ (leanprover-community#26997)
b4ee20d 
This will change how the docs and infoview render, and the rules for the upcoming whitespace linter.

Zulip thread: [#mathlib4 > Space after &leanprover-community#96;⅟ &leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Space.20after.20.60.E2.85.9F.20.60/near/528309060)



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
hrmacbeth pushed a commit to szqzs/mathlib4 that referenced this pull request Jul 28, 2025
@alreadydone @hrmacbeth
fix(Topology/Covering): switch to standard definition (leanprover-com…
2dd65fe 
…munity#24983)

As discussed in [#mathlib4 > edge cases not covered by &leanprover-community#96;IsCoveringMap&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/edge.20cases.20not.20covered.20by.20.60IsCoveringMap.60/near/518413081), the previous definition doesn't include examples like the inclusion of a one-point space into a two-point discrete space.
mathlib-bors bot pushed a commit that referenced this pull request Aug 13, 2025
@eric-wieser
refactor: rename Rel to SetRel, restore the old Rel (#27447)
59e4fba 
Many users are confused that Rel no longer means what it used to. Since the design is not obvious (and the implementation is explicitly part of the interface thanks to `abbrev`), let's give it a name that makes the choice obvious.

This then restores the old definition of `Rel`, as an abbrev; it's conceivable that many users were just using this as a shorthand, and this stops them being broken by #25587. Such users will of course be broken if they used [the old API](https://github.com/leanprover-community/mathlib4/blob/59bd63c72671849996d64c5d3b5f24a36333483c%5E/Mathlib/Data/Rel.lean).

This way, users bumping from 4.21.0 to 4.22.0 and using `Rel` only as a shorthand will not be broken.

[#mathlib4 > Changing &#96;Rel&#96; to &#96;Set (α × β)&#96;, to help uniform spaces @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Changing.20.60Rel.60.20to.20.60Set.20.28.CE.B1.20.C3.97.20.CE.B2.29.60.2C.20to.20help.20uniform.20spaces/near/528531852)
mathlib-bors bot pushed a commit that referenced this pull request Aug 19, 2025
@JovanGerb
feat(Order/Antisymmetrization): support AntisymmRel in `gcongr_forw…
dc60430 
…ard` (#28514)

This PR adds support for `AntisymmRel` in `gcongr_forward`, so that we can `grw` using the `AntisymmRel (· ≤ ·)` relation.

Requested in [#mathlib4 > Announcement: New &#96;grw&#96; tactic @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Announcement.3A.20New.20.60grw.60.20tactic/near/534752659)
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Aug 20, 2025
@JovanGerb
feat(Order/Antisymmetrization): support AntisymmRel in `gcongr_forw…
5cc616b 
…ard` (leanprover-community#28514)

This PR adds support for `AntisymmRel` in `gcongr_forward`, so that we can `grw` using the `AntisymmRel (· ≤ ·)` relation.

Requested in [#mathlib4 > Announcement: New &leanprover-community#96;grw&leanprover-community#96; tactic @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Announcement.3A.20New.20.60grw.60.20tactic/near/534752659)
mathlib-bors bot pushed a commit that referenced this pull request Aug 22, 2025
@xroblot
chore: remove unnecessary simp call (#28775)
69c685f 
cf. [#mathlib4 > Lint error with &#96;Simp says&#96;](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Lint.20error.20with.20.60Simp.20says.60)
mathlib-bors bot pushed a commit that referenced this pull request Aug 22, 2025
@Sebi-Kumar
feat(Topology/Path): add theorem about casting with rfl (#28185)
c3c2249 
Prove the trivial result `p.cast rfl rfl = p` for a path `p`, which serves as a useful result for the simplifier to know. Suggested by Aaron Liu at the discussion [#Is there code for X? > Dealing with &#96;Path.cast&#96;](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Dealing.20with.20.60Path.2Ecast.60).
Paul-Lez pushed a commit to Paul-Lez/mathlib4 that referenced this pull request Aug 23, 2025
@eric-wieser @Paul-Lez
refactor: rename Rel to SetRel, restore the old Rel (leanprover…
bd8f99d 
…-community#27447)

Many users are confused that Rel no longer means what it used to. Since the design is not obvious (and the implementation is explicitly part of the interface thanks to `abbrev`), let's give it a name that makes the choice obvious.

This then restores the old definition of `Rel`, as an abbrev; it's conceivable that many users were just using this as a shorthand, and this stops them being broken by leanprover-community#25587. Such users will of course be broken if they used [the old API](https://github.com/leanprover-community/mathlib4/blob/59bd63c72671849996d64c5d3b5f24a36333483c%5E/Mathlib/Data/Rel.lean).

This way, users bumping from 4.21.0 to 4.22.0 and using `Rel` only as a shorthand will not be broken.

[#mathlib4 > Changing &leanprover-community#96;Rel&leanprover-community#96; to &leanprover-community#96;Set (α × β)&leanprover-community#96;, to help uniform spaces @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Changing.20.60Rel.60.20to.20.60Set.20.28.CE.B1.20.C3.97.20.CE.B2.29.60.2C.20to.20help.20uniform.20spaces/near/528531852)
Paul-Lez pushed a commit to Paul-Lez/mathlib4 that referenced this pull request Aug 23, 2025
@JovanGerb @Paul-Lez
feat(Order/Antisymmetrization): support AntisymmRel in `gcongr_forw…
5905e70 
…ard` (leanprover-community#28514)

This PR adds support for `AntisymmRel` in `gcongr_forward`, so that we can `grw` using the `AntisymmRel (· ≤ ·)` relation.

Requested in [#mathlib4 > Announcement: New &leanprover-community#96;grw&leanprover-community#96; tactic @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Announcement.3A.20New.20.60grw.60.20tactic/near/534752659)
Paul-Lez pushed a commit to Paul-Lez/mathlib4 that referenced this pull request Aug 23, 2025
@xroblot @Paul-Lez
chore: remove unnecessary simp call (leanprover-community#28775)
14cee9a 
cf. [#mathlib4 > Lint error with &leanprover-community#96;Simp says&leanprover-community#96;](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Lint.20error.20with.20.60Simp.20says.60)
Paul-Lez pushed a commit to Paul-Lez/mathlib4 that referenced this pull request Aug 23, 2025
@Sebi-Kumar @Paul-Lez
feat(Topology/Path): add theorem about casting with rfl (leanprover-c…
b2952ef 
…ommunity#28185)

Prove the trivial result `p.cast rfl rfl = p` for a path `p`, which serves as a useful result for the simplifier to know. Suggested by Aaron Liu at the discussion [#Is there code for X? > Dealing with &leanprover-community#96;Path.cast&leanprover-community#96;](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Dealing.20with.20.60Path.2Ecast.60).
pechersky pushed a commit to pechersky/mathlib4 that referenced this pull request Aug 25, 2025
@JovanGerb @pechersky
feat(Order/Antisymmetrization): support AntisymmRel in `gcongr_forw…
c8b4f59 
…ard` (leanprover-community#28514)

This PR adds support for `AntisymmRel` in `gcongr_forward`, so that we can `grw` using the `AntisymmRel (· ≤ ·)` relation.

Requested in [#mathlib4 > Announcement: New &leanprover-community#96;grw&leanprover-community#96; tactic @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Announcement.3A.20New.20.60grw.60.20tactic/near/534752659)
pechersky pushed a commit to pechersky/mathlib4 that referenced this pull request Aug 25, 2025
@xroblot @pechersky
chore: remove unnecessary simp call (leanprover-community#28775)
2569ff9 
cf. [#mathlib4 > Lint error with &leanprover-community#96;Simp says&leanprover-community#96;](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Lint.20error.20with.20.60Simp.20says.60)
pechersky pushed a commit to pechersky/mathlib4 that referenced this pull request Aug 25, 2025
@Sebi-Kumar @pechersky
feat(Topology/Path): add theorem about casting with rfl (leanprover-c…
033b8d8 
…ommunity#28185)

Prove the trivial result `p.cast rfl rfl = p` for a path `p`, which serves as a useful result for the simplifier to know. Suggested by Aaron Liu at the discussion [#Is there code for X? > Dealing with &leanprover-community#96;Path.cast&leanprover-community#96;](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Dealing.20with.20.60Path.2Ecast.60).
mathlib-bors bot pushed a commit that referenced this pull request Aug 27, 2025
@grunweg
chore: move most of Data/Matrix to LinearAlgebra (#28966)
1cd593f 
These are not related to data structures at all.
This PR is not exhaustive, likely further files in `Data/Matrix` should also be moved.

Zulip discussion: [#mathlib4 > Cleaning up &#96;Data&#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Cleaning.20up.20.60Data.60/near/536224905)

Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
FormulaRabbit81 pushed a commit to YaelDillies/mathlib4 that referenced this pull request Aug 30, 2025
@Sebi-Kumar @FormulaRabbit81
feat(Topology/Path): add theorem about casting with rfl (leanprover-c…
254c601 
…ommunity#28185)

Prove the trivial result `p.cast rfl rfl = p` for a path `p`, which serves as a useful result for the simplifier to know. Suggested by Aaron Liu at the discussion [#Is there code for X? > Dealing with &leanprover-community#96;Path.cast&leanprover-community#96;](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Dealing.20with.20.60Path.2Ecast.60).
FormulaRabbit81 pushed a commit to YaelDillies/mathlib4 that referenced this pull request Aug 30, 2025
@grunweg @FormulaRabbit81
chore: move most of Data/Matrix to LinearAlgebra (leanprover-communit…
9099d46 
…y#28966)

These are not related to data structures at all.
This PR is not exhaustive, likely further files in `Data/Matrix` should also be moved.

Zulip discussion: [#mathlib4 > Cleaning up &leanprover-community#96;Data&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Cleaning.20up.20.60Data.60/near/536224905)

Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
mathlib-bors bot pushed a commit that referenced this pull request Aug 30, 2025
@JovanGerb
style: prefer some/none over .some/.none (#27896)
4594829 
The notation `.some` and `.none` are very useful when working with other inductive types such as `LOption` which have fields names `some` and/or `none`. But for `Option`, we prefer to simply write `some`/`none`.

[#mathlib4 > style: &#96;.some&#96;/&#96;.none&#96; vs &#96;some&#96;/&#96;none&#96;](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/style.3A.20.60.2Esome.60.2F.60.2Enone.60.20vs.20.60some.60.2F.60none.60)

Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
CBirkbeck pushed a commit to CBirkbeck/mathlib4 that referenced this pull request Sep 8, 2025
@JovanGerb @CBirkbeck
style: prefer some/none over .some/.none (leanprover-communit…
92f85d7 
…y#27896)

The notation `.some` and `.none` are very useful when working with other inductive types such as `LOption` which have fields names `some` and/or `none`. But for `Option`, we prefer to simply write `some`/`none`.

[#mathlib4 > style: &leanprover-community#96;.some&leanprover-community#96;/&leanprover-community#96;.none&leanprover-community#96; vs &leanprover-community#96;some&leanprover-community#96;/&leanprover-community#96;none&leanprover-community#96;](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/style.3A.20.60.2Esome.60.2F.60.2Enone.60.20vs.20.60some.60.2F.60none.60)

Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
mathlib-bors bot pushed a commit that referenced this pull request Sep 22, 2025
@JovanGerb
feat: extensible push and pull tactics (#21965)
ccc14f2 
This PR defines the `push` and `pull` tactics, and makes `push_neg` a macro for `push Not`. The tactics are also available in `conv` mode.

For tagging, there is only the `@[push]` attribute, which adds the reverse rewrite for the `pull` tactic when relevant. In the future, we may also need a separate `@[pull X]` attribute for pulling `X`.

Thanks to this change, we will be able to make `push_neg` into a more powerful tactic by tagging more lemmas. It also means that about 60 files now don't need to import `LinearOrder`/`PartialOrder`. This will be especially useful when we get the `@[to_dual]` attribute.

This work originally started in #21769. There is now the follow up PR #29000 which adds `push` tags and tests for them.

The `@[push]` attribute is defined in `Mathlib.Tactic.Push.Attr` and the main implementation of `push` and `pull` is in `Mathlib.Tactic.Push`.

Some proofs need to be fixed because the new simp-based `push_neg` can see through more reducible definitions.

Zulip conversation: [#mathlib4 > I made an extensible &#96;push&#96; tactic generalizing &#96;push_neg&#96;](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/I.20made.20an.20extensible.20.60push.60.20tactic.20generalizing.20.60push_neg.60)

closes #21841
mathlib-bors bot pushed a commit that referenced this pull request Sep 23, 2025
@JovanGerb
feat: extensible push and pull tactics (#21965)
79b52d2 
This PR defines the `push` and `pull` tactics, and makes `push_neg` a macro for `push Not`. The tactics are also available in `conv` mode.

For tagging, there is only the `@[push]` attribute, which adds the reverse rewrite for the `pull` tactic when relevant. In the future, we may also need a separate `@[pull X]` attribute for pulling `X`.

Thanks to this change, we will be able to make `push_neg` into a more powerful tactic by tagging more lemmas. It also means that about 60 files now don't need to import `LinearOrder`/`PartialOrder`. This will be especially useful when we get the `@[to_dual]` attribute.

This work originally started in #21769. There is now the follow up PR #29000 which adds `push` tags and tests for them.

The `@[push]` attribute is defined in `Mathlib.Tactic.Push.Attr` and the main implementation of `push` and `pull` is in `Mathlib.Tactic.Push`.

Some proofs need to be fixed because the new simp-based `push_neg` can see through more reducible definitions.

Zulip conversation: [#mathlib4 > I made an extensible &#96;push&#96; tactic generalizing &#96;push_neg&#96;](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/I.20made.20an.20extensible.20.60push.60.20tactic.20generalizing.20.60push_neg.60)

closes #21841
mathlib-bors bot pushed a commit that referenced this pull request Sep 23, 2025
@JovanGerb
feat(Order/Filter/Basic): gcongr for EventuallyEq (#29747)
a45cce9 
This was originally requested in [#mathlib4 > ✔ &#96;rw&#96; with ae relations](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.E2.9C.94.20.60rw.60.20with.20ae.20relations/with/529301301)
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

@digama0 digama0 digama0 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.

3 participants

@kim-em @gebner @digama0