[Merged by Bors] - chore: adapt to multiple goal linter 1 #12338
Conversation
There was a problem hiding this comment.
You didn't mark this ready for review yet. I still decided to leave a few comments; hope they helpful.
To my eye, most of these look like clear improvements that should be uncontroversial. I commented on other that might require more thought or where follow-up golfing is possible.
| @@ -355,7 +355,7 @@ def gluedCover : Scheme.GlueData.{u} where | |||
| This is an isomorphism, as witnessed by an `IsIso` instance. -/ | |||
| def fromGlued : 𝒰.gluedCover.glued ⟶ X := by | |||
| fapply Multicoequalizer.desc | |||
| exact fun x => 𝒰.map x | |||
| · exact fun x => 𝒰.map x | |||
There was a problem hiding this comment.
Can you move this into the fapply? If possible, I'd find this even nicer.
| exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.2⟩ | ||
| repeat' erw [WithBot.coe_eq_coe] | ||
| exact add_eq_zero_iff' (zero_le _) (zero_le _) | ||
| repeat (· exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.1⟩) |
There was a problem hiding this comment.
I'm on the fence if the any_goals => repeat change is better.
| rw [List.eq_replicate.2 ⟨_, h⟩, prod_replicate, one_pow] | ||
| · exact (length l) | ||
| · rfl⟩ |
There was a problem hiding this comment.
| rw [List.eq_replicate.2 ⟨_, h⟩, prod_replicate, one_pow] | |
| · exact (length l) | |
| · rfl⟩ | |
| rw [List.eq_replicate.mpr ⟨rfl, h⟩, prod_replicate, one_pow]⟩ |
| @@ -129,7 +129,7 @@ theorem hasFDerivAt_integral_of_dominated_loc_of_lip' {F' : α → H →L[𝕜] | |||
| exact ((hF_meas _ x_in).sub (hF_meas _ x₀_in)).sub (hF'_meas.apply_continuousLinearMap _) | |||
| · refine mem_of_superset h_ball fun x hx ↦ ?_ | |||
| apply (h_diff.and h_lipsch).mono | |||
| rintro a ⟨-, ha_bound⟩ | |||
| on_goal 1 => rintro a ⟨-, ha_bound⟩ | |||
There was a problem hiding this comment.
I get why this was linted this way, but it seems unnecessary. The 2nd goal is just a bounding function waiting to get described by the next line.
There was a problem hiding this comment.
I have been using on_goal sometimes as a place-holder for something where maybe the linter should be manually silenced. I'll leave this comment visible, in case someone else wants to chime in.
| on_goal 1 => let b : Finset ℂ := ?_ | ||
| on_goal 1 => let c : Finset ℂ := ?_ |
There was a problem hiding this comment.
Perhaps the linter shouldn't add on_goal when the additional goals are terms of Type and not Prop.
There was a problem hiding this comment.
This is probably a good heuristic, though I would limit the use of this heuristic to theorems. Again, I'll leave this up for further comments.
| @@ -649,15 +649,15 @@ theorem cont_eval_fix {f k v} (fok : Code.Ok f) : | |||
| obtain ⟨v'', h₁, h₂⟩ := this | |||
| rw [reaches_eval] at h₂ | |||
| swap | |||
| exact ReflTransGen.single rfl | |||
| · exact ReflTransGen.single rfl | |||
There was a problem hiding this comment.
Could be on_goal 2 => exact ReflTransGen.single rfl removing the previous swap.
There was a problem hiding this comment.
I tried to recycle as much as possible the original syntax. I would prefer this change to be a separate PR.
|
!bench |
|
Here are the benchmark results for commit 68a02d1. |
adomani
changed the title
Co-authored-by: Ruben Van de Velde <[email protected]>
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
added
merge-conflict
leanprover-community-mathlib4-bot
removed
the
merge-conflict
|
bors d+ |
|
✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
This PR was reduced by approximately half of its original size: the other half of this PR is now the content of #12560. This PR was reduced by approximately half of its halved size: the other half of the halved PR is now the content of #12834. A PR analogous to the merged PRs #12338, #12361 and #12372: reformatting proofs following the multiple goals linter of #12339. This should be the last of the adaptations.
This PR was reduced by approximately half of its original size: the other half of this PR is now the content of #12560. This PR was reduced by approximately half of its halved size: the other half of the halved PR is now the content of #12834. A PR analogous to the merged PRs #12338, #12361 and #12372: reformatting proofs following the multiple goals linter of #12339. This should be the last of the adaptations.
This PR was reduced by approximately half of its original size: the other half of this PR is now the content of #12560. This PR was reduced by approximately half of its halved size: the other half of the halved PR is now the content of #12834. A PR analogous to the merged PRs #12338, #12361 and #12372: reformatting proofs following the multiple goals linter of #12339. This should be the last of the adaptations.
A linter that makes sure that, when multiple goals are present, they are enclosed in `·`s. Adaptations (the order is chronological, there should be no dependency among them): * #12338, * #12361, * #12372, * #12560, * #12834, * #12381, * #12908, * #14939, plus many many more that this comment is too small to contain. Co-authored-by: Michael Rothgang <[email protected]>
A PR accompanying #12339.
Zulip discussion