Skip to content

[Merged by Bors] - feat: port Order.Synonym#562

Closed
pechersky wants to merge 61 commits intomasterfrom
pechersky/port-order-synonym
Closed

[Merged by Bors] - feat: port Order.Synonym#562
pechersky wants to merge 61 commits intomasterfrom
pechersky/port-order-synonym

Conversation

@pechersky
Copy link
Copy Markdown
Contributor

@pechersky pechersky commented Nov 9, 2022 •
edited
Loading

mathlib3 hash: fd47bdf09e90f553519c712378e651975fe8c829

checked against mathlib3port using:

leanf=Order/Synonym.lean; diff Mathlib/$leanf <(rg -v "^#print" ../mathlib3port/Mathbin/$leanf) -d -y --suppress-common-lines | rg -w "(inductive|structure|class|lemma|theorem|def)"

kim-em and others added 23 commits November 6, 2022 20:20
@kim-em
port of data.funlike.*
6631370
@kim-em
long line
7700ecf
@kim-em
docBlame
df8ac7f
@kim-em
import
4f074d3
@kim-em
copy and paste mathport output
6170aab
@kim-em
restore lemmas
76bc3e2
@kim-em
Merge branch 'fun_like' into equiv_defs
9bac811
@kim-em
starting
f240c63
@kim-em
rename
246a5c8
@pechersky
feat: port Order.Basic
17df209 
TODO: decide on min/max alignment with mathlib3
Used the mathport3 output, with sparse proof copying
from previous version
@pechersky
Remove leftover port prec comment
ca1443d
@pechersky
docs and lints
97c9ffb
@Vierkantor
Fix: Function.Surjective.unique was inferring α : Prop when it ca…
b21f8e8 
…n be any `Sort`
@pechersky
Merge branch 'master' into pechersky/port-order-basic
5c11d31
@Vierkantor
Builds until the Quot section
d88f4d8
@Vierkantor
Move to appropriate file
aa3e0d1
@Vierkantor
Revert wrong implicitness
465c82b
@Vierkantor
to_fun_as_coe is useless
487f8b6
@pechersky
Switch ext to intros tactic
c2cfbe8
@pechersky
clean up min/max via toMin/toMax
875554c
@pechersky
Merge remote-tracking branch 'origin/equiv_defs' into pechersky/port-…
5cc3f99 
…order-synonym
@pechersky
Merge remote-tracking branch 'origin/equiv_defs' into pechersky/port-…
b9e3ce3 
…order-synonym
@pechersky
feat: port Order.Synonym
7b89140
@pechersky pechersky added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) awaiting-review labels Nov 9, 2022
This was referenced Nov 11, 2022
Closed
Closed
@kim-em kim-em removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 18, 2022
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Nov 18, 2022

bors merge

@bors
Copy link
Copy Markdown

bors bot commented Nov 18, 2022

Merge conflict.

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Nov 18, 2022

bors merge

bors bot pushed a commit that referenced this pull request Nov 18, 2022
@kim-em @pechersky
@Vierkantor @dwarn
feat: port Order.Synonym (#562)
63095f3 
mathlib3 hash: fd47bdf09e90f553519c712378e651975fe8c829

- [x] depends on: #556 
- [x] depends on: #550 



Co-authored-by: Yakov Pechersky <ypechersky@treeline.bio>
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: David Wärn <codwarn@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Nov 18, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Order.Synonym [Merged by Bors] - feat: port Order.Synonym Nov 18, 2022
@bors bors bot closed this Nov 18, 2022
@bors bors bot deleted the pechersky/port-order-synonym branch November 18, 2022 03:56
bors bot pushed a commit that referenced this pull request Nov 18, 2022
@kim-em @pechersky @Vierkantor
feat: port Order.Max (#567)
e07097c 
mathlib3 hash: fd47bdf09e90f553519c712378e651975fe8c829

- [x] depends on: #566 
- [x] depends on: #562 



Co-authored-by: Yakov Pechersky <ypechersky@treeline.bio>
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
bors bot pushed a commit that referenced this pull request Nov 18, 2022
@kim-em @pechersky @Vierkantor
feat: port Order.Compare (#569)
454d62c 
mathlib3 hash: fd47bdf09e90f553519c712378e651975fe8c829

- [x] depends on: #568 
- [x] depends on: #562 



Co-authored-by: Yakov Pechersky <ypechersky@treeline.bio>
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em kim-em left review comments

Assignees

No one assigned

Labels

mathlib-port This is a port of a theory file from mathlib.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

8 participants

@pechersky @kim-em @digama0 @j-loreaux @Vierkantor @dwarn @Ruben-VandeVelde @77Tigers