Skip to content

[Merged by Bors] - feat: port Order.Max#567

Closed
pechersky wants to merge 76 commits intomasterfrom
pechersky/port-order-max
Closed

[Merged by Bors] - feat: port Order.Max#567
pechersky wants to merge 76 commits intomasterfrom
pechersky/port-order-max

Conversation

@pechersky
Copy link
Copy Markdown
Contributor

@pechersky pechersky commented Nov 11, 2022 •
edited by kim-em
Loading

mathlib3 hash: fd47bdf09e90f553519c712378e651975fe8c829

Checked the hash against recent mathlib3port via:

leanf=Order/Max.lean; diff Mathlib/$leanf ../mathlib3port/Mathbin/$leanf -y --suppress-common-lines | rg "(lemma|theorem|def)"

kim-em and others added 30 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
@kim-em
merge master
bef5f97
@pechersky
Merge remote-tracking branch 'origin/master' into pechersky/port-orde…
a154971 
…r-max
@pechersky
chore: fix Data.Bool
cca0b1b 
by calling out to root
There was a clash between PRs
@pechersky
Merge branch 'pechersky/realign-bool-decide' into pechersky/port-orde…
beb0537 
…r-max
@pechersky
One more mention
5f7688e
@pechersky
Merge branch 'pechersky/realign-bool-decide' into pechersky/port-orde…
99c2ae6 
…r-max
@pechersky
feat: port Order.Max
715fee1
Ruben-VandeVelde and others added 16 commits November 17, 2022 14:44
@Ruben-VandeVelde
Merge branch 'master' into equiv_defs
6c79022
@77Tigers
add Trans instance for Equiv
2a6c0a1
@kim-em
Merge remote-tracking branch 'origin/master' into equiv_defs
78c142a
@kim-em
linting
04d962a
@kim-em
merge
2595ce4
@kim-em
lint
c74802b
@kim-em
Merge branch 'equiv_defs' into pechersky/port-order-synonym
40b5d6f
@kim-em
Merge branch 'pechersky/port-order-synonym' into pechersky/port-order…
6556bb2 
…-max
@kim-em
Mathlib.lean
a067a60
@kim-em
Merge branch 'equiv_defs' into pechersky/port-order-synonym
45f67a3
@kim-em
Merge branch 'pechersky/port-order-synonym' into pechersky/port-order…
8758f92 
…-max
@digama0
style
4f566ca
@kim-em
lint
89733b6
@kim-em
Merge remote-tracking branch 'origin/equiv_defs' into pechersky/port-…
4075655 
…order-synonym
@kim-em
Merge remote-tracking branch 'origin/master' into pechersky/port-orde…
4391b19 
…r-synonym
@kim-em
Merge branch 'pechersky/port-order-synonym' into pechersky/port-order…
c551ca5 
…-max
@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

👎 Rejected by label

@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 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
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.Max [Merged by Bors] - feat: port Order.Max Nov 18, 2022
@bors bors bot closed this Nov 18, 2022
@bors bors bot deleted the pechersky/port-order-max branch November 18, 2022 04:23
bors bot pushed a commit that referenced this pull request Nov 18, 2022
@kim-em @pechersky @Vierkantor
feat: port Order.Monotone (#591)
8722e20 
mathlib3 hash: fd47bdf09e90f553519c712378e651975fe8c829

- [x] depends on: #567 
- [x] depends on: #560 
- [x] depends on: #569 



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

No reviews

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