Skip to content

[Merged by Bors] - feat(Tactic/workOnGoal): port workOnGoal from mathlib#93

Closed
kim-em wants to merge 1 commit intomasterfrom
workOnGoal
Closed

[Merged by Bors] - feat(Tactic/workOnGoal): port workOnGoal from mathlib#93
kim-em wants to merge 1 commit intomasterfrom
workOnGoal

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

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

No description provided.

@gebner
Copy link
Copy Markdown
Member

gebner commented Nov 15, 2021

bors r+

bors bot pushed a commit that referenced this pull request Nov 15, 2021
@kim-em
feat(Tactic/workOnGoal): port workOnGoal from mathlib (#93)
74efc4a 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Nov 15, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(Tactic/workOnGoal): port workOnGoal from mathlib [Merged by Bors] - feat(Tactic/workOnGoal): port workOnGoal from mathlib Nov 15, 2021
@bors bors bot closed this Nov 15, 2021
@bors bors bot deleted the workOnGoal branch November 15, 2021 09:13
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 May 10, 2025
@kbuzzard
feat: add Polynomial.div_C and C_div (#24751)
1096f8b 
Zulip thread: [#maths > How can I get 1/2&#42;2=1 in Q&#91;X?&#93; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/How.20can.20I.20get.201.2F2*2.3D1.20in.20Q.5BX.3F.5D/near/517280660)

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
tannerduve pushed a commit that referenced this pull request May 13, 2025
@kbuzzard @tannerduve
feat: add Polynomial.div_C and C_div (#24751)
da78c11 
Zulip thread: [#maths > How can I get 1/2&#42;2=1 in Q&#91;X?&#93; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/How.20can.20I.20get.201.2F2*2.3D1.20in.20Q.5BX.3F.5D/near/517280660)

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
bwehlin pushed a commit to bwehlin/mathlib4 that referenced this pull request May 31, 2025
@kbuzzard
feat: add Polynomial.div_C and C_div (leanprover-community#24751)
77e9040 
Zulip thread: [#maths > How can I get 1/2&leanprover-community#42;2=1 in Q&leanprover-community#91;X?&leanprover-community#93; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/How.20can.20I.20get.201.2F2*2.3D1.20in.20Q.5BX.3F.5D/near/517280660)

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
mathlib-bors bot pushed a commit that referenced this pull request Sep 5, 2025
@Nebula691 @Whysoserioushah
@kckennylau @eric-wieser @hongjiayang1
feat(Algebra/QuadraticAlgebra): custom structure for quadratic algebr…
62eeacf 
…as (#27511)

Discussed in [#Is there code for X? > Z&#91;(1+sqrt(1+4k))/2&#93; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Z.5B.281.2Bsqrt.281.2B4k.29.29.2F2.5D/near/520523635)

Co-authored-by: Edison Xie <yx3021@ic.ac.uk>
Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
Co-authored-by: Whysoserioushah <yx3021@ic.ac.uk>
Co-authored-by: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: hongjiayang1 <jh1321@ic.ac.uk>
CBirkbeck pushed a commit to CBirkbeck/mathlib4 that referenced this pull request Sep 8, 2025
@Nebula691 @Whysoserioushah
@kckennylau @eric-wieser @hongjiayang1 @CBirkbeck
feat(Algebra/QuadraticAlgebra): custom structure for quadratic algebr…
6a03e10 
…as (leanprover-community#27511)

Discussed in [#Is there code for X? > Z&leanprover-community#91;(1+sqrt(1+4k))/2&leanprover-community#93; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Z.5B.281.2Bsqrt.281.2B4k.29.29.2F2.5D/near/520523635)

Co-authored-by: Edison Xie <yx3021@ic.ac.uk>
Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
Co-authored-by: Whysoserioushah <yx3021@ic.ac.uk>
Co-authored-by: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: hongjiayang1 <jh1321@ic.ac.uk>
yuanyi-350 pushed a commit to yuanyi-350/yuanyi_mathlib4 that referenced this pull request Sep 10, 2025
@Nebula691 @Whysoserioushah
@kckennylau @eric-wieser @hongjiayang1 @yuanyi-350
feat(Algebra/QuadraticAlgebra): custom structure for quadratic algebr…
a23b948 
…as (leanprover-community#27511)

Discussed in [#Is there code for X? > Z&leanprover-community#91;(1+sqrt(1+4k))/2&leanprover-community#93; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Z.5B.281.2Bsqrt.281.2B4k.29.29.2F2.5D/near/520523635)

Co-authored-by: Edison Xie <yx3021@ic.ac.uk>
Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
Co-authored-by: Whysoserioushah <yx3021@ic.ac.uk>
Co-authored-by: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: hongjiayang1 <jh1321@ic.ac.uk>
mathlib-bors bot pushed a commit that referenced this pull request Sep 11, 2025
@vasnesterov
feat(Data/Real): representation of reals from [0, 1] in positional …
e5d0dd6 
…system (#26021)

* Introduce `ofDigits {b : ℕ} (digits : ℕ → Fin b) : ℝ`, representing a real number of the form `0.d₀d₁d₂...` (where `dᵢ = digits i`) as an infinite sum.
* Prove that this sum converges to a number in the interval `[0, 1]`.
* Prove `ofDigits_close_of_common_prefix`: if the first `n` digits of two numbers are equal, then their difference is bounded by `b⁻ⁿ`.
* Introduce `Real.digits`, which converts a real number into its sequence of digits.
* Prove that `ofDigits (toDigits x b) = x`.

Zulip threads: 
- [Zulip thread where this was proposed](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Base.20n.20expansion.20of.20real.20numbers.3F/near/502937293) 
- [#PR reviews > representation of reals in &#91;0, 1&#93; in positional system](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/representation.20of.20reals.20in.20.5B0.2C.201.5D.20in.20positional.20system/with/537704930)
robertmaxton42 pushed a commit to robertmaxton42/mathlib4 that referenced this pull request Sep 11, 2025
@Nebula691 @Whysoserioushah
@kckennylau @eric-wieser @hongjiayang1 @robertmaxton42
feat(Algebra/QuadraticAlgebra): custom structure for quadratic algebr…
0d2eab7 
…as (leanprover-community#27511)

Discussed in [#Is there code for X? > Z&leanprover-community#91;(1+sqrt(1+4k))/2&leanprover-community#93; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Z.5B.281.2Bsqrt.281.2B4k.29.29.2F2.5D/near/520523635)

Co-authored-by: Edison Xie <yx3021@ic.ac.uk>
Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
Co-authored-by: Whysoserioushah <yx3021@ic.ac.uk>
Co-authored-by: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: hongjiayang1 <jh1321@ic.ac.uk>
joelriou pushed a commit to joelriou/mathlib4 that referenced this pull request Oct 2, 2025
@Nebula691 @Whysoserioushah
@kckennylau @eric-wieser @hongjiayang1 @joelriou
feat(Algebra/QuadraticAlgebra): custom structure for quadratic algebr…
1ea91d3 
…as (leanprover-community#27511)

Discussed in [#Is there code for X? > Z&leanprover-community#91;(1+sqrt(1+4k))/2&leanprover-community#93; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Z.5B.281.2Bsqrt.281.2B4k.29.29.2F2.5D/near/520523635)

Co-authored-by: Edison Xie <yx3021@ic.ac.uk>
Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk>
Co-authored-by: Whysoserioushah <yx3021@ic.ac.uk>
Co-authored-by: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: hongjiayang1 <jh1321@ic.ac.uk>
joelriou pushed a commit to joelriou/mathlib4 that referenced this pull request Oct 2, 2025
@vasnesterov @joelriou
feat(Data/Real): representation of reals from [0, 1] in positional …
1f64342 
…system (leanprover-community#26021)

* Introduce `ofDigits {b : ℕ} (digits : ℕ → Fin b) : ℝ`, representing a real number of the form `0.d₀d₁d₂...` (where `dᵢ = digits i`) as an infinite sum.
* Prove that this sum converges to a number in the interval `[0, 1]`.
* Prove `ofDigits_close_of_common_prefix`: if the first `n` digits of two numbers are equal, then their difference is bounded by `b⁻ⁿ`.
* Introduce `Real.digits`, which converts a real number into its sequence of digits.
* Prove that `ofDigits (toDigits x b) = x`.

Zulip threads: 
- [Zulip thread where this was proposed](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Base.20n.20expansion.20of.20real.20numbers.3F/near/502937293) 
- [#PR reviews > representation of reals in &leanprover-community#91;0, 1&leanprover-community#93; in positional system](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/representation.20of.20reals.20in.20.5B0.2C.201.5D.20in.20positional.20system/with/537704930)
zhuyizheng pushed a commit to zhuyizheng/mathlib4 that referenced this pull request Oct 2, 2025
@vasnesterov @zhuyizheng
feat(Data/Real): representation of reals from [0, 1] in positional …
926d886 
…system (leanprover-community#26021)

* Introduce `ofDigits {b : ℕ} (digits : ℕ → Fin b) : ℝ`, representing a real number of the form `0.d₀d₁d₂...` (where `dᵢ = digits i`) as an infinite sum.
* Prove that this sum converges to a number in the interval `[0, 1]`.
* Prove `ofDigits_close_of_common_prefix`: if the first `n` digits of two numbers are equal, then their difference is bounded by `b⁻ⁿ`.
* Introduce `Real.digits`, which converts a real number into its sequence of digits.
* Prove that `ofDigits (toDigits x b) = x`.

Zulip threads: 
- [Zulip thread where this was proposed](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Base.20n.20expansion.20of.20real.20numbers.3F/near/502937293) 
- [#PR reviews > representation of reals in &leanprover-community#91;0, 1&leanprover-community#93; in positional system](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/representation.20of.20reals.20in.20.5B0.2C.201.5D.20in.20positional.20system/with/537704930)
Kha pushed a commit to Kha/mathlib4 that referenced this pull request Oct 23, 2025
@kim-em
chore: adaptations for nightly-2025-10-20 (leanprover-community#93)
6377881
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@kim-em @gebner