Skip to content

feat(Data/List/Basic): start porting from mathlib#22

Merged
avigad merged 4 commits intomasterfrom
list_stuff
Jul 9, 2021
Merged

feat(Data/List/Basic): start porting from mathlib#22
avigad merged 4 commits intomasterfrom
list_stuff

Conversation

@avigad
Copy link
Copy Markdown
Contributor

@avigad avigad commented Jun 26, 2021

For a couple of projects I am working on, I would like to do some basic combinatorial reasoning in Lean 4. In particular, I am aiming towards some approximation to finset. My plan is to:

  • port some more logic
  • port some more stuff about lists
  • port some basic function stuff (injectivity, function images)
  • use lists without duplicates as a proxy for finite sets.

The main thing I need are some properties of cardinality, including the fact that if there is a bijection between nodup lists, they have the same cardinality.

I am still learning how to use Lean 4, so the proofs are messy. I will go back and improve them one day. I am hoping the community will let me get away with some quick-and-dirty triage in the meanwhile just to get things going.

I can vouch for the fact that porting mathlib files is a good way to learn the new syntax, in case others want to join in.

@digama0 I usually got error messages when I tried to use the block tactics, so I resorted to focus instead. If/when this is merged, if you want, I'll post some examples where the block versions don't seem to work.

@avigad avigad requested a review from digama0 June 26, 2021 18:52
gebner
gebner reviewed Jun 28, 2021
View reviewed changes
Mathlib/Data/List/Basic.lean Outdated
@[simp] lemma mem_cons_iff (a y : α) (l : List α) : a ∈ y :: l ↔ (a = y ∨ a ∈ l) :=
Iff.rfl

-- used to be @[rsimp]
Copy link
Copy Markdown
Member

@gebner gebner Jun 28, 2021

Choose a reason for hiding this comment

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

I think it's now officially time to forget about rsimp.

Mathlib/Data/List/Basic.lean Outdated
Comment on lines +206 to +210
instance DecidableMem [DecidableEq α] (a : α) : ∀ (l : List α), Decidable (a ∈ l)
| [] => isFalse notFalse
| b :: l =>
if h₁ : a = b then isTrue (Or.inl h₁)
else match DecidableMem a l with
| isTrue h₂ => isTrue (Or.inr h₂)
| isFalse h₂ => isFalse (not_or_intro h₁ h₂)
Copy link
Copy Markdown
Member

@gebner gebner Jun 28, 2021

Choose a reason for hiding this comment

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

Suggested change
instance DecidableMem [DecidableEq α] (a : α) : ∀ (l : List α), Decidable (a ∈ l)
| [] => isFalse notFalse
| b :: l =>
if h₁ : a = b then isTrue (Or.inl h₁)
else match DecidableMem a l with
| isTrue h₂ => isTrue (Or.inr h₂)
| isFalse h₂ => isFalse (not_or_intro h₁ h₂)
instance decidableMem [DecidableEq α] (a : α) : ∀ (l : List α), Decidable (a ∈ l)
| [] => isFalse notFalse
| b :: l =>
if h₁ : a = b then isTrue (Or.inl h₁)
else match decidableMem a l with
| isTrue h₂ => isTrue (Or.inr h₂)
| isFalse h₂ => isFalse (not_or_intro h₁ h₂)

Mathlib/SetNotation.lean Outdated
Comment on lines +33 to +34
syntax "∀" binderterm "," term : term
syntax "∃" binderterm "," term : term
Copy link
Copy Markdown
Member

@gebner gebner Jun 28, 2021

Choose a reason for hiding this comment

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

Suggested change
syntax "∀" binderterm "," term : term
syntax "∃" binderterm "," term : term
syntax "∀ " binderterm ", " term : term
syntax "∃ " binderterm ", " term : term

Mathlib/SetNotation.lean Outdated

declare_syntax_cat binderterm -- notation for `a` or `a : A` or `a ∈ S`
syntax ident : binderterm
syntax ident " : " term : binderterm
Copy link
Copy Markdown
Member

@gebner gebner Jun 28, 2021

Choose a reason for hiding this comment

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

Suggested change
syntax ident " : " term : binderterm

If you add syntax for ∀ x : α, ..., then you should add a macro/elaborator for it as well. The only reason this works at the moment is pure coincidence: the built-in parser for forall is built in the same way, and therefore the built-in expander for forall also happens to apply to our newly defined syntax.

This overlap also produces really ugly error messages:

#check ∀ x : Foo, x = x
/-
▶ 42:8-42:24: error:
overloaded, errors 
  elaboration function for '«term∀_,_»' has not been implemented
    ∀x : Foo,x = x
  
  42:13 unknown identifier 'Foo'
-/

Copy link
Copy Markdown
Contributor Author

@avigad avigad Jul 2, 2021

Choose a reason for hiding this comment

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

I only moved this declaration from Set.lean. It looks like @kbuzzard put it there. Why do we need it, if the built-in expander for forall already handles it? Should I simply delete it and add syntax only for the bounded versions?

Also: I experimented with a delaborator for bounded quantifiers. It seems that, at least for forall, we need to introduce a definition like forallb to register it. Should I do that, or just let the pretty-printer print the expanded version?

Copy link
Copy Markdown
Member

@gebner gebner Jul 3, 2021

Choose a reason for hiding this comment

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

Yes, I think the ident ":" term : binderterm syntax should just be removed (at least for now).

I experimented with a delaborator for bounded quantifiers. It seems that, at least for forall, we need to introduce a definition like forallb to register it.

We might want forallb for other reasons (e.g. to ensure that simp doesn't simplify a bounded quantifier ∀ x < max a b, p x to a non-bounded quantifier like ∀ x, x < a ∨ x < b → p x). But it's easy enough to register a delaborator for forall expressions:

import Lean

open Lean PrettyPrinter.Delaborator

@[delab forallE]
def delabForallBounded : Delab :=
  -- use `guard` here to restrict to bounded quantifiers
  `(here goes your beautiful output)

#check ∀ x, true -- here✝ goes✝ your✝ beautiful✝ output✝ : Prop

Copy link
Copy Markdown
Contributor Author

@avigad avigad Jul 9, 2021

Choose a reason for hiding this comment

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

Thanks, it's good to know that we can match against forallE. I didn't add the delaborator, but I just made all the other corrections.

Copy link
Copy Markdown
Member

@kbuzzard kbuzzard Jul 9, 2021

Choose a reason for hiding this comment

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

I might have PR'ed that binder stuff but I strongly suspect some kids on the discord wrote it, and I don't claim that either I or they knew what they were doing :-) The file Set.lean was stuff ported from core Lean 3 which was not in core Lean 4 (so I didn't really know where to put it in this repo). I did the same thing with Function.lean . I didn't know if we were adopting a "please keep all Lean 4 mathlib files as a proper subset of the corresponding Lean 3 mathlib files" attitude or not.

@avigad avigad merged commit 5212f0c into master Jul 9, 2021
@dwrensha dwrensha mentioned this pull request Aug 19, 2022
Closed
bors bot pushed a commit that referenced this pull request Aug 22, 2022
@dwrensha
chore: uncomment cons_injective and cons_inj in Data/List/Basic.lean (#…
d211150 
…372)

Uncomment two theorems that were added in commented form in #22.

You may compare to the mathlib3 versions here: https://github.com/leanprover-community/mathlib/blob/aaf7dc2c34831dbd92a21b9e37c1f63017d35f45/src/data/list/basic.lean#L50-L54
mattrobball added a commit that referenced this pull request Feb 25, 2023
@mattrobball
# This is a combination of 126 commits.
8fcb216 
# This is the 1st commit message:

automated fixes

Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean

# The commit message #2 will be skipped:

# feat: port CategoryTheory.Limits.IsLimit

# The commit message #3 will be skipped:

# Initial file copy from mathport

# The commit message #4 will be skipped:

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

# The commit message #5 will be skipped:

# feat: port CategoryTheory.Limits.Cones

# The commit message #6 will be skipped:

# Initial file copy from mathport

# The commit message #7 will be skipped:

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

# The commit message #8 will be skipped:

# feat: port CategoryTheory.Yoneda

# The commit message #9 will be skipped:

# Initial file copy from mathport

# The commit message #10 will be skipped:

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

# The commit message #11 will be skipped:

# feat: port CategoryTheory.Functor.Currying

# The commit message #12 will be skipped:

# Initial file copy from mathport

# The commit message #13 will be skipped:

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

# The commit message #14 will be skipped:

# fix all but one decl

# The commit message #15 will be skipped:

# fix last errors

# The commit message #16 will be skipped:

# feat: port CategoryTheory.Functor.Hom

# The commit message #17 will be skipped:

# Initial file copy from mathport

# The commit message #18 will be skipped:

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

# The commit message #19 will be skipped:

# feat: port CategoryTheory.Types

# The commit message #20 will be skipped:

# Initial file copy from mathport

# The commit message #21 will be skipped:

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

# The commit message #22 will be skipped:

# feat: port CategoryTheory.EpiMono

# The commit message #23 will be skipped:

# Initial file copy from mathport

# The commit message #24 will be skipped:

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

# The commit message #25 will be skipped:

# feat: port CategoryTheory.Groupoid

# The commit message #26 will be skipped:

# Initial file copy from mathport

# The commit message #27 will be skipped:

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

# The commit message #28 will be skipped:

# feat: port CategoryTheory.Pi.Basic

# The commit message #29 will be skipped:

# Initial file copy from mathport

# The commit message #30 will be skipped:

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

# The commit message #31 will be skipped:

# fix some errors

# The commit message #32 will be skipped:

# some more fixes

# The commit message #33 will be skipped:

# more fixes

# The commit message #34 will be skipped:

# finally fixed

# The commit message #35 will be skipped:

# lint

# The commit message #36 will be skipped:

# add porting note for scary warning

# The commit message #37 will be skipped:

# add porting note about proliferation of match

# The commit message #38 will be skipped:

# initial pass

# The commit message #39 will be skipped:

# fix errors

# The commit message #40 will be skipped:

# lint

# The commit message #41 will be skipped:

# fix errors; lint; add porting notes

# The commit message #42 will be skipped:

# fix errors; lint; add porting note

# The commit message #43 will be skipped:

# fix error

# The commit message #44 will be skipped:

# fix some errors

# The commit message #45 will be skipped:

# minor fixes

# The commit message #46 will be skipped:

# fix all but four

# The commit message #47 will be skipped:

# fix last errors; lint

# The commit message #48 will be skipped:

# feat: port CategoryTheory.DiscreteCategory

# The commit message #49 will be skipped:

# Initial file copy from mathport

# The commit message #50 will be skipped:

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

# The commit message #51 will be skipped:

# get file to build

# The commit message #52 will be skipped:

# lint

# The commit message #53 will be skipped:

# lint some more

# The commit message #54 will be skipped:

# feat: port CategoryTheory.Functor.ReflectsIsomorphisms

# The commit message #55 will be skipped:

# Initial file copy from mathport

# The commit message #56 will be skipped:

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

# The commit message #57 will be skipped:

# feat: port CategoryTheory.Functor.EpiMono

# The commit message #58 will be skipped:

# Initial file copy from mathport

# The commit message #59 will be skipped:

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

# The commit message #60 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Adjunction

# The commit message #61 will be skipped:

# Initial file copy from mathport

# The commit message #62 will be skipped:

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

# The commit message #63 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Basic

# The commit message #64 will be skipped:

# Initial file copy from mathport

# The commit message #65 will be skipped:

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

# The commit message #66 will be skipped:

# feat: port CategoryTheory.CommSq

# The commit message #67 will be skipped:

# Initial file copy from mathport

# The commit message #68 will be skipped:

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

# The commit message #69 will be skipped:

# first pass

# The commit message #70 will be skipped:

# names and removing restate_axiom

# The commit message #71 will be skipped:

# fix lint

# The commit message #72 will be skipped:

# remove spurious edit

# The commit message #73 will be skipped:

# fix errors; lint

# The commit message #74 will be skipped:

# feat: port CategoryTheory.Adjunction.Basic

# The commit message #75 will be skipped:

# Initial file copy from mathport

# The commit message #76 will be skipped:

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

# The commit message #77 will be skipped:

# Initial file copy from mathport

# The commit message #78 will be skipped:

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

# The commit message #79 will be skipped:

# push it as far as possible

# The commit message #80 will be skipped:

# minor changes

# The commit message #81 will be skipped:

# seems to work

# The commit message #82 will be skipped:

# add example and equivalence file for testing

# The commit message #83 will be skipped:

# test: create `slice.lean` test file

# The commit message #84 will be skipped:

# remove equivalence.lean

# The commit message #85 will be skipped:

# remove rewriteTarget'; change MonadExceptOf to MonadExcept

# The commit message #86 will be skipped:

# add documentation and clean up

# The commit message #87 will be skipped:

# move iteration tactics to core

# The commit message #88 will be skipped:

# modify documentation lines

# The commit message #89 will be skipped:

# add module documentation(?)

# The commit message #90 will be skipped:

# fix module docs

# The commit message #91 will be skipped:

# fix test/slice.lean

# The commit message #92 will be skipped:

# fix all but refl error

# The commit message #93 will be skipped:

# fix refl error and lint errors

# The commit message #94 will be skipped:

# fix final long line

# The commit message #95 will be skipped:

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

# The commit message #96 will be skipped:

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

# The commit message #97 will be skipped:

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

# The commit message #98 will be skipped:

# update slice naming

# The commit message #99 will be skipped:

# some progress

# The commit message #100 will be skipped:

# only one error left

# The commit message #101 will be skipped:

# filled in last sorry

# The commit message #102 will be skipped:

# break long lines

# The commit message #103 will be skipped:

# delete linter command

# The commit message #104 will be skipped:

# fix comments

# The commit message #105 will be skipped:

# fix two simpNF lints

# The commit message #106 will be skipped:

# fill in some docstrings

# The commit message #107 will be skipped:

# fix most linter issues

# The commit message #108 will be skipped:

# add missing aligns for fields; lint

# The commit message #109 will be skipped:

# restore lost import line

# The commit message #110 will be skipped:

# fix errors; lint

# The commit message #111 will be skipped:

# feat: port CategoryTheory.Limits.Shapes.StrongEpi

# The commit message #112 will be skipped:

# Initial file copy from mathport

# The commit message #113 will be skipped:

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

# The commit message #114 will be skipped:

# fix errors; lint

# The commit message #115 will be skipped:

# Update Mathlib.lean

# The commit message #116 will be skipped:

# fix errors; lint

# The commit message #117 will be skipped:

# fix errors; lint; shorten filename

# The commit message #118 will be skipped:

# fix some errors

# The commit message #119 will be skipped:

# fix some more

# The commit message #120 will be skipped:

# fix errors

# The commit message #121 will be skipped:

# lint

# The commit message #122 will be skipped:

# fix errors

# The commit message #123 will be skipped:

# lint

# The commit message #124 will be skipped:

# feat: port CategoryTheory.Category.Ulift

# The commit message #125 will be skipped:

# Initial file copy from mathport

# The commit message #126 will be skipped:

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

automated fixes

Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean

# The commit message #2 will be skipped:

# feat: port CategoryTheory.Limits.Cones

# The commit message #3 will be skipped:

# Initial file copy from mathport

# The commit message #4 will be skipped:

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

# The commit message #5 will be skipped:

# feat: port CategoryTheory.Yoneda

# The commit message #6 will be skipped:

# Initial file copy from mathport

# The commit message #7 will be skipped:

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

# The commit message #8 will be skipped:

# feat: port CategoryTheory.Functor.Currying

# The commit message #9 will be skipped:

# Initial file copy from mathport

# The commit message #10 will be skipped:

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

# The commit message #11 will be skipped:

# fix all but one decl

# The commit message #12 will be skipped:

# fix last errors

# The commit message #13 will be skipped:

# feat: port CategoryTheory.Functor.Hom

# The commit message #14 will be skipped:

# Initial file copy from mathport

# The commit message #15 will be skipped:

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

# The commit message #16 will be skipped:

# feat: port CategoryTheory.Types

# The commit message #17 will be skipped:

# Initial file copy from mathport

# The commit message #18 will be skipped:

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

# The commit message #19 will be skipped:

# feat: port CategoryTheory.EpiMono

# The commit message #20 will be skipped:

# Initial file copy from mathport

# The commit message #21 will be skipped:

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

# The commit message #22 will be skipped:

# feat: port CategoryTheory.Groupoid

# The commit message #23 will be skipped:

# Initial file copy from mathport

# The commit message #24 will be skipped:

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

# The commit message #25 will be skipped:

# feat: port CategoryTheory.Pi.Basic

# The commit message #26 will be skipped:

# Initial file copy from mathport

# The commit message #27 will be skipped:

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

# The commit message #28 will be skipped:

# fix some errors

# The commit message #29 will be skipped:

# some more fixes

# The commit message #30 will be skipped:

# more fixes

# The commit message #31 will be skipped:

# finally fixed

# The commit message #32 will be skipped:

# lint

# The commit message #33 will be skipped:

# add porting note for scary warning

# The commit message #34 will be skipped:

# add porting note about proliferation of match

# The commit message #35 will be skipped:

# initial pass

# The commit message #36 will be skipped:

# fix errors

# The commit message #37 will be skipped:

# lint

# The commit message #38 will be skipped:

# fix errors; lint; add porting notes

# The commit message #39 will be skipped:

# fix errors; lint; add porting note

# The commit message #40 will be skipped:

# fix error

# The commit message #41 will be skipped:

# fix some errors

# The commit message #42 will be skipped:

# minor fixes

# The commit message #43 will be skipped:

# fix all but four

# The commit message #44 will be skipped:

# Delete start_port-macos.sh

# The commit message #45 will be skipped:

# fix last errors; lint

# The commit message #46 will be skipped:

# feat: port CategoryTheory.DiscreteCategory

# The commit message #47 will be skipped:

# Initial file copy from mathport

# The commit message #48 will be skipped:

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

# The commit message #49 will be skipped:

# get file to build

# The commit message #50 will be skipped:

# lint

# The commit message #51 will be skipped:

# lint some more

# The commit message #52 will be skipped:

# feat: port CategoryTheory.Functor.ReflectsIsomorphisms

# The commit message #53 will be skipped:

# Initial file copy from mathport

# The commit message #54 will be skipped:

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

# The commit message #55 will be skipped:

# feat: port CategoryTheory.Functor.EpiMono

# The commit message #56 will be skipped:

# Initial file copy from mathport

# The commit message #57 will be skipped:

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

# The commit message #58 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Adjunction

# The commit message #59 will be skipped:

# Initial file copy from mathport

# The commit message #60 will be skipped:

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

# The commit message #61 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Basic

# The commit message #62 will be skipped:

# Initial file copy from mathport

# The commit message #63 will be skipped:

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

# The commit message #64 will be skipped:

# feat: port CategoryTheory.CommSq

# The commit message #65 will be skipped:

# Initial file copy from mathport

# The commit message #66 will be skipped:

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

# The commit message #67 will be skipped:

# first pass

# The commit message #68 will be skipped:

# names and removing restate_axiom

# The commit message #69 will be skipped:

# fix lint

# The commit message #70 will be skipped:

# remove spurious edit

# The commit message #71 will be skipped:

# fix errors; lint

# The commit message #72 will be skipped:

# feat: port CategoryTheory.Adjunction.Basic

# The commit message #73 will be skipped:

# Initial file copy from mathport

# The commit message #74 will be skipped:

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

# The commit message #75 will be skipped:

# Initial file copy from mathport

# The commit message #76 will be skipped:

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

# The commit message #77 will be skipped:

# push it as far as possible

# The commit message #78 will be skipped:

# minor changes

# The commit message #79 will be skipped:

# seems to work

# The commit message #80 will be skipped:

# add example and equivalence file for testing

# The commit message #81 will be skipped:

# test: create `slice.lean` test file

# The commit message #82 will be skipped:

# remove equivalence.lean

# The commit message #83 will be skipped:

# remove rewriteTarget'; change MonadExceptOf to MonadExcept

# The commit message #84 will be skipped:

# add documentation and clean up

# The commit message #85 will be skipped:

# move iteration tactics to core

# The commit message #86 will be skipped:

# add slice to global import file

# The commit message #87 will be skipped:

# modify documentation lines

# The commit message #88 will be skipped:

# add module documentation(?)

# The commit message #89 will be skipped:

# fix module docs

# The commit message #90 will be skipped:

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

    add missing aligns to cones.lean

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

    lint for changes and clean up

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

    golf (co)yoneda proofs

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

    remove extra instances

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

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

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

    add updated dependencies

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

    fix long line

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

    change X to pt

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

    revert one more

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

    fix rebase

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

    fix import file

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

    move names to new convention

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

    add updated files

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

    fix case error

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

    fix import line typo

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

    fix import file

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

    align names in comments

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

    lint for CI

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

    try fix-comments.py

    only fixed a single issue for the second time now

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

    fix final error

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

    fix all but one decl

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

    automated fixes

    Mathbin -> Mathlib

    fix certain import statements

    move "by" to end of line

    add import to Mathlib.lean

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

    automated fixes

    Mathbin -> Mathlib

    fix certain import statements

    move "by" to end of line

    add import to Mathlib.lean

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

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

    automated fixes

    Mathbin -> Mathlib

    fix certain import statements

    move "by" to end of line

    add import to Mathlib.lean

    # The commit message #2 will be skipped:

    # feat: port CategoryTheory.Limits.IsLimit

    # The commit message #3 will be skipped:

    # Initial file copy from mathport

    # The commit message #4 will be skipped:

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

    # The commit message #5 will be skipped:

    # feat: port CategoryTheory.Limits.Cones

    # The commit message #6 will be skipped:

    # Initial file copy from mathport

    # The commit message #7 will be skipped:

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

    # The commit message #8 will be skipped:

    # feat: port CategoryTheory.Yoneda

    # The commit message #9 will be skipped:

    # Initial file copy from mathport

    # The commit message #10 will be skipped:

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

    # The commit message #11 will be skipped:

    # feat: port CategoryTheory.Functor.Currying

    # The commit message #12 will be skipped:

    # Initial file copy from mathport

    # The commit message #13 will be skipped:

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

    # The commit message #14 will be skipped:

    # fix all but one decl

    # The commit message #15 will be skipped:

    # fix last errors

    # The commit message #16 will be skipped:

    # feat: port CategoryTheory.Functor.Hom

    # The commit message #17 will be skipped:

    # Initial file copy from mathport

    # The commit message #18 will be skipped:

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

    # The commit message #19 will be skipped:

    # feat: port CategoryTheory.Types

    # The commit message #20 will be skipped:

    # Initial file copy from mathport

    # The commit message #21 will be skipped:

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

    # The commit message #22 will be skipped:

    # feat: port CategoryTheory.EpiMono

    # The commit message #23 will be skipped:

    # Initial file copy from mathport

    # The commit message #24 will be skipped:

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

    # The commit message #25 will be skipped:

    # feat: port CategoryTheory.Groupoid

    # The commit message #26 will be skipped:

    # Initial file copy from mathport

    # The commit message #27 will be skipped:

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

    # The commit message #28 will be skipped:

    # feat: port CategoryTheory.Pi.Basic

    # The commit message #29 will be skipped:

    # Initial file copy from mathport

    # The commit message #30 will be skipped:

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

    # The commit message #31 will be skipped:

    # fix some errors

    # The commit message #32 will be skipped:

    # some more fixes

    # The commit message #33 will be skipped:

    # more fixes

    # The commit message #34 will be skipped:

    # finally fixed

    # The commit message #35 will be skipped:

    # lint

    # The commit message #36 will be skipped:

    # add porting note for scary warning

    # The commit message #37 will be skipped:

    # add porting note about proliferation of match

    # The commit message #38 will be skipped:

    # initial pass

    # The commit message #39 will be skipped:

    # fix errors

    # The commit message #40 will be skipped:

    # lint

    # The commit message #41 will be skipped:

    # fix errors; lint; add porting notes

    # The commit message #42 will be skipped:

    # fix errors; lint; add porting note

    # The commit message #43 will be skipped:

    # fix error

    # The commit message #44 will be skipped:

    # fix some errors

    # The commit message #45 will be skipped:

    # minor fixes

    # The commit message #46 will be skipped:

    # fix all but four

    # The commit message #47 will be skipped:

    # fix last errors; lint

    # The commit message #48 will be skipped:

    # feat: port CategoryTheory.DiscreteCategory

    # The commit message #49 will be skipped:

    # Initial file copy from mathport

    # The commit message #50 will be skipped:

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

    # The commit message #51 will be skipped:

    # get file to build

    # The commit message #52 will be skipped:

    # lint

    # The commit message #53 will be skipped:

    # lint some more

    # The commit message #54 will be skipped:

    # feat: port CategoryTheory.Functor.ReflectsIsomorphisms

    # The commit message #55 will be skipped:

    # Initial file copy from mathport

    # The commit message #56 will be skipped:

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

    # The commit message #57 will be skipped:

    # feat: port CategoryTheory.Functor.EpiMono

    # The commit message #58 will be skipped:

    # Initial file copy from mathport

    # The commit message #59 will be skipped:

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

    # The commit message #60 will be skipped:

    # feat: port CategoryTheory.LiftingProperties.Adjunction

    # The commit message #61 will be skipped:

    # Initial file copy from mathport

    # The commit message #62 will be skipped:

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

    # The commit message #63 will be skipped:

    # feat: port CategoryTheory.LiftingProperties.Basic

    # The commit message #64 will be skipped:

    # Initial file copy from mathport

    # The commit message #65 will be skipped:

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

    # The commit message #66 will be skipped:

    # feat: port CategoryTheory.CommSq

    # The commit message #67 will be skipped:

    # Initial file copy from mathport

    # The commit message #68 will be skipped:

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

    # The commit message #69 will be skipped:

    # first pass

    # The commit message #70 will be skipped:

    # names and removing restate_axiom

    # The commit message #71 will be skipped:

    # fix lint

    # The commit message #72 will be skipped:

    # remove spurious edit

    # The commit message #73 will be skipped:

    # fix errors; lint

    # The commit message #74 will be skipped:

    # feat: port CategoryTheory.Adjunction.Basic

    # The commit message #75 will be skipped:

    # Initial file copy from mathport

    # The commit message #76 will be skipped:

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

    # The commit message #77 will be skipped:

    # Initial file copy from mathport

    # The commit message #78 will be skipped:

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

    # The commit message #79 will be skipped:

    # push it as far as possible

    # The commit message #80 will be skipped:

    # minor changes

    # The commit message #81 will be skipped:

    # seems to work

    # The commit message #82 will be skipped:

    # add example and equivalence file for testing

    # The commit message #83 will be skipped:

    # test: create `slice.lean` test file

    # The commit message #84 will be skipped:

    # remove equivalence.lean

    # The commit message #85 will be skipped:

    # remove rewriteTarget'; change MonadExceptOf to MonadExcept

    # The commit message #86 will be skipped:

    # add documentation and clean up

    # The commit message #87 will be skipped:

    # move iteration tactics to core

    # The commit message #88 will be skipped:

    # modify documentation lines

    # The commit message #89 will be skipped:

    # add module documentation(?)

    # The commit message #90 will be skipped:

    # fix module docs

    # The commit message #91 will be skipped:

    # fix test/slice.lean

    # The commit message #92 will be skipped:

    # fix all but refl error

    # The commit message #93 will be skipped:

    # fix refl error and lint errors

    # The commit message #94 will be skipped:

    # fix final long line

    # The commit message #95 will be skipped:

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

    # The commit message #96 will be skipped:

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

    # The commit message #97 will be skipped:

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

    # The commit message #98 will be skipped:

    # update slice naming

    # The commit message #99 will be skipped:

    # some progress

    # The commit message #100 will be skipped:

    # only one error left

    # The commit message #101 will be skipped:

    # filled in last sorry

    # The commit message #102 will be skipped:

    # break long lines

    # The commit message #103 will be skipped:

    # delete linter command

    # The commit message #104 will be skipped:

    # fix comments

    # The commit message #105 will be skipped:

    # fix two simpNF lints

    # The commit message #106 will be skipped:

    # fill in some docstrings

    # The commit message #107 will be skipped:

    # fix most linter issues

    # The commit message #108 will be skipped:

    # add missing aligns for fields; lint

    # The commit message #109 will be skipped:

    # restore lost import line

    # The commit message #110 will be skipped:

    # fix errors; lint

    # The commit message #111 will be skipped:

    # feat: port CategoryTheory.Limits.Shapes.StrongEpi

    # The commit message #112 will be skipped:

    # Initial file copy from mathport

    # The commit message #113 will be skipped:

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

    # The commit message #114 will be skipped:

    # fix errors; lint

    # The commit message #115 will be skipped:

    # Update Mathlib.lean

    # The commit message #116 will be skipped:

    # fix errors; lint

    # The commit message #117 will be skipped:

    # fix errors; lint; shorten filename

    # The commit message #118 will be skipped:

    # fix some errors

    # The commit message #119 will be skipped:

    # fix some more

    # The commit message #120 will be skipped:

    # fix errors

    # The commit message #121 will be skipped:

    # lint

    # The commit message #122 will be skipped:

    # fix errors

    # The commit message #123 will be skipped:

    # lint

    # The commit message #124 will be skipped:

    # feat: port CategoryTheory.Category.Ulift

    # The commit message #125 will be skipped:

    # Initial file copy from mathport

    # The commit message #126 will be skipped:

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

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

    Initial file copy from mathport

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

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

automated fixes

Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean

# The commit message #2 will be skipped:

# feat: port CategoryTheory.Limits.HasLimits

# The commit message #3 will be skipped:

# Initial file copy from mathport

# The commit message #4 will be skipped:

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

# The commit message #5 will be skipped:

# feat: port CategoryTheory.Limits.IsLimit

# The commit message #6 will be skipped:

# Initial file copy from mathport

# The commit message #7 will be skipped:

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

# The commit message #8 will be skipped:

# feat: port CategoryTheory.Limits.Cones

# The commit message #9 will be skipped:

# Initial file copy from mathport

# The commit message #10 will be skipped:

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

# The commit message #11 will be skipped:

# feat: port CategoryTheory.Yoneda

# The commit message #12 will be skipped:

# Initial file copy from mathport

# The commit message #13 will be skipped:

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

# The commit message #14 will be skipped:

# feat: port CategoryTheory.Functor.Currying

# The commit message #15 will be skipped:

# Initial file copy from mathport

# The commit message #16 will be skipped:

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

# The commit message #17 will be skipped:

# fix all but one decl

# The commit message #18 will be skipped:

# fix last errors

# The commit message #19 will be skipped:

# feat: port CategoryTheory.Functor.Hom

# The commit message #20 will be skipped:

# Initial file copy from mathport

# The commit message #21 will be skipped:

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

# The commit message #22 will be skipped:

# feat: port CategoryTheory.Types

# The commit message #23 will be skipped:

# Initial file copy from mathport

# The commit message #24 will be skipped:

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

# The commit message #25 will be skipped:

# feat: port CategoryTheory.EpiMono

# The commit message #26 will be skipped:

# Initial file copy from mathport

# The commit message #27 will be skipped:

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

# The commit message #28 will be skipped:

# feat: port CategoryTheory.Groupoid

# The commit message #29 will be skipped:

# Initial file copy from mathport

# The commit message #30 will be skipped:

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

# The commit message #31 will be skipped:

# feat: port CategoryTheory.Pi.Basic

# The commit message #32 will be skipped:

# Initial file copy from mathport

# The commit message #33 will be skipped:

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

# The commit message #34 will be skipped:

# fix some errors

# The commit message #35 will be skipped:

# some more fixes

# The commit message #36 will be skipped:

# more fixes

# The commit message #37 will be skipped:

# finally fixed

# The commit message #38 will be skipped:

# lint

# The commit message #39 will be skipped:

# add porting note for scary warning

# The commit message #40 will be skipped:

# add porting note about proliferation of match

# The commit message #41 will be skipped:

# initial pass

# The commit message #42 will be skipped:

# fix errors

# The commit message #43 will be skipped:

# lint

# The commit message #44 will be skipped:

# fix errors; lint; add porting notes

# The commit message #45 will be skipped:

# fix errors; lint; add porting note

# The commit message #46 will be skipped:

# fix error

# The commit message #47 will be skipped:

# fix some errors

# The commit message #48 will be skipped:

# minor fixes

# The commit message #49 will be skipped:

# fix all but four

# The commit message #50 will be skipped:

# Delete start_port-macos.sh

# The commit message #51 will be skipped:

# fix last errors; lint

# The commit message #52 will be skipped:

# feat: port CategoryTheory.DiscreteCategory

# The commit message #53 will be skipped:

# Initial file copy from mathport

# The commit message #54 will be skipped:

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

# The commit message #55 will be skipped:

# get file to build

# The commit message #56 will be skipped:

# lint

# The commit message #57 will be skipped:

# lint some more

# The commit message #58 will be skipped:

# feat: port CategoryTheory.Functor.ReflectsIsomorphisms

# The commit message #59 will be skipped:

# Initial file copy from mathport

# The commit message #60 will be skipped:

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

# The commit message #61 will be skipped:

# feat: port CategoryTheory.Functor.EpiMono

# The commit message #62 will be skipped:

# Initial file copy from mathport

# The commit message #63 will be skipped:

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

# The commit message #64 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Adjunction

# The commit message #65 will be skipped:

# Initial file copy from mathport

# The commit message #66 will be skipped:

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

# The commit message #67 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Basic

# The commit message #68 will be skipped:

# Initial file copy from mathport

# The commit message #69 will be skipped:

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

# The commit message #70 will be skipped:

# feat: port CategoryTheory.CommSq

# The commit message #71 will be skipped:

# Initial file copy from mathport

# The commit message #72 will be skipped:

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

# The commit message #73 will be skipped:

# first pass

# The commit message #74 will be skipped:

# names and removing restate_axiom

# The commit message #75 will be skipped:

# fix lint

# The commit message #76 will be skipped:

# remove spurious edit

# The commit message #77 will be skipped:

# fix errors; lint

# The commit message #78 will be skipped:

# feat: port CategoryTheory.Adjunction.Basic

# The commit message #79 will be skipped:

# Initial file copy from mathport

# The commit message #80 will be skipped:

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

# The commit message #81 will be skipped:

# Initial file copy from mathport

# The commit message #82 will be skipped:

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

# The commit message #83 will be skipped:

# push it as far as possible

# The commit message #84 will be skipped:

# minor changes

# The commit message #85 will be skipped:

# seems to work

# The commit message #86 will be skipped:

# add example and equivalence file for testing

# The commit message #87 will be skipped:

# test: create `slice.lean` test file
mathlib-bors bot pushed a commit that referenced this pull request Nov 19, 2025
@bryangingechen
Bgc fix title check (#22)
8a5a1ca 
* testing

* leanprover-community

* more testing

* fix
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

@kbuzzard kbuzzard kbuzzard left review comments

@digama0 digama0 Awaiting requested review from digama0

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

@avigad @gebner @kbuzzard