[Merged by Bors] - chore: adaptations for the multi-goal linter#14939
[Merged by Bors] - chore: adaptations for the multi-goal linter#14939
Conversation
PR summary fec7d8aedaImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit> |
| refine (norm_sum_le _ _).trans <| (sum_le_sum this).trans ?_ | ||
| rw [← sum_mul] | ||
| trans μ.toBoxAdditive I * ε₁; swap; linarith | ||
| trans μ.toBoxAdditive I * ε₁; swap |
There was a problem hiding this comment.
This "swap and handle side goal idiom" could also be replaced by "pick_goal 2 => linarith" or similar. Just tell me your favourite bikeshed colour :-)
| (ψ : b ⟶ c) [p.IsHomLift f φ] [p.IsHomLift g ψ] : p.IsHomLift (f ≫ g) (φ ≫ ψ) := by | ||
| apply of_commSq | ||
| rw [p.map_comp] | ||
| on_goal 1 => rw [p.map_comp] |
There was a problem hiding this comment.
The line below applies to both goals; this rw just massages the first into the suitable form.
There was a problem hiding this comment.
I think this is obscure enough that it warrants a comment in the code. I would never have guessed that behaviour if I had to fix this proof because it broke for unrelated reasons.
There was a problem hiding this comment.
Sure, I've added a comment to this instance and the four other places with similar logic.
| positivity | ||
| have := noAccidental hA | ||
| rw [Nat.floor_lt' (by positivity), inv_pos_lt_iff_one_lt_mul'] at hG | ||
| swap |
There was a problem hiding this comment.
This is a positivity side goal: it feels clearer to me to solve that first.
|
✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
|
If anybody feels like tweaking the comments from the last commit, feel free to propose a follow-up; I'll be happy to review it. |
|
Pull request successfully merged into master. Build succeeded: |
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 <rothgami@math.hu-berlin.de>
I really don't care which colour we paint this bikeshed in - if you prefer fixing this in a different style, I'm all ears!