[Merged by Bors] - chore: uncdot various files#12422
Conversation
|
And I should also say: thank you for your continuous effort on developing linters. I would be really happy for the multi-goal linter to land. Just yesterday I was commenting on this with a new contributor's PR. |
grunweg
left a comment
There was a problem hiding this comment.
Now reviewed up to and including LinearAlgebra.
| simp_rw [← div_pow] | ||
| rw [geom_sum_eq, div_le_iff_of_neg] | ||
| · trans (-1 : ℝ) | ||
| · linarith |
There was a problem hiding this comment.
Just highlighting: this is really just un-indenting; git's diff is confusing here.
grunweg
left a comment
There was a problem hiding this comment.
Now reviewed up to and including Probability. That's it from me for today.
Most comments are flagging things for reviewers; two blocks I'd have to review more closely as github's diff is not so clear.
| · rw [Pi.add_apply, Set.indicator_of_mem, Set.indicator_of_not_mem, add_zero] <;> simpa | ||
| · rw [Pi.add_apply, Set.indicator_of_not_mem, Set.indicator_of_mem, zero_add] <;> | ||
| simpa using hx | ||
| · split_ifs with h |
There was a problem hiding this comment.
This is adding two dots (which I don't object to; I trust your linter).
| rw [Measure.restrict_apply] at hs | ||
| apply h𝓕.measure_zero_of_invariant _ _ hs | ||
| · intro γ | ||
| · apply h𝓕.measure_zero_of_invariant _ _ hs |
There was a problem hiding this comment.
Nice find! (This is a mix of cdot-ing and un-cdot-ing, so arguably fits here.)
| exact Continuous.continuousOn (Continuous.comp' (continuous_mul_left (-1)) this) | ||
| · simp only [neg_mul, one_mul] | ||
| exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp | ||
| · have : ∫ a in uIoc 0 x, r * rexp (-(r * a)) = ∫ a in (0)..x, r * rexp (-(r * a)) := by |
There was a problem hiding this comment.
This is mostly cdot-ing; arguably, this belongs into another PR.
There was a problem hiding this comment.
To be more precise: this file is cdot-ing here and on line 148, but un-cdot-ing on line 150. IOW, this could be included here.
grunweg
left a comment
There was a problem hiding this comment.
Now reviewed the remainder of this PR (and the merge commits): I think this is good to go.
| cases' lt_or_le c (g y) with hc hc | ||
| · rcases em (a ∈ range f) with (⟨x, rfl⟩ | _) | ||
| · refine' ⟨x, xu, _, hyxu.le⟩ | ||
| have hyb : (g - dg) y < b := by |
There was a problem hiding this comment.
This block has to be manually checked.
There was a problem hiding this comment.
Did so: it's just github's diff being confused. Reviewing with whitespace hidden shows this is just un-cdoting.
A portion of #12422 containing all the changes in `Mathlib/[A-C]` up to and including `CategoryTheory`.
|
bors d+ I am not going to kick this on the queue yet, for fear of merge conflicts... |
|
✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
These `·` are scoping when there is a single active goal. These were found using a modification of the linter at #12339.
|
Pull request successfully merged into master. Build succeeded: |
A portion of #12422 containing all the changes in `Mathlib/[A-C]` up to and including `CategoryTheory`.
These `·` are scoping when there is a single active goal. These were found using a modification of the linter at #12339.
A portion of #12422 containing all the changes in `Mathlib/[A-C]` up to and including `CategoryTheory`.
These `·` are scoping when there is a single active goal. These were found using a modification of the linter at #12339.
A portion of #12422 containing all the changes in `Mathlib/[A-C]` up to and including `CategoryTheory`.
These `·` are scoping when there is a single active goal. These were found using a modification of the linter at #12339.
These
·are scoping when there is a single active goal.These were found using a modification of the linter at #12339.