-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore(set_theory/ordinal/arithmetic): clean up is_normal.sup
and related
#15162
Conversation
@@ -1933,6 +1928,7 @@ begin | |||
{ intros c l IH, | |||
refine eq_of_forall_ge_iff (λ d, (((opow_is_normal a1).trans | |||
(add_is_normal b)).limit_le l).trans _), | |||
dsimp, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I have no idea why this was needed all of a sudden.
@@ -234,7 +234,7 @@ begin | |||
{ let g : ι → ordinal.{u} := λ i, (enum_ord_order_iso hs).symm ⟨_, hf i⟩, | |||
suffices : enum_ord s (sup.{u u} g) = sup.{u u} f, | |||
{ rw ←this, exact enum_ord_mem hs _ }, | |||
rw is_normal.sup.{u u u} h g hι, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I feel like you should be using a resetI
instead of this @
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Adding resetI,
before this rw
still doesn't work if I don't use @
. Not sure why.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
(I pushed a small change to squeeze the dsimp
s)
✌️ vihdzp can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…lated (#15162) We golf various theorems and tweak their arguments. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded: |
is_normal.sup
and relatedis_normal.sup
and related
We golf various theorems and tweak their arguments.