[Merged by Bors] - chore: adapt to multiple goal linter 2 #12361

adomani · 2024-04-23T08:08:13Z

A PR analogous to #12338: reformatting proofs following the multiple goals linter of #12339.

…gain

Mathlib/RingTheory/Polynomial/Selmer.lean

Vierkantor · 2024-04-25T10:09:58Z

Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean

@@ -156,9 +156,9 @@ theorem cyclotomic_mul_prime_pow_eq (R : Type*) {p m : ℕ} [Fact (Nat.Prime p)]
    have hdiv : p ∣ p ^ a.succ * m := ⟨p ^ a * m, by rw [← mul_assoc, pow_succ']⟩
    rw [pow_succ', mul_assoc, mul_comm, cyclotomic_mul_prime_dvd_eq_pow R hdiv,
      cyclotomic_mul_prime_pow_eq _ _ a.succ_pos, ← pow_mul]
-    congr 1
-    simp only [tsub_zero, Nat.succ_sub_succ_eq_sub]
-    rwa [Nat.mul_sub_right_distrib, mul_comm, pow_succ]


Does this mean that rwa used assumption on a different goal than the one it rewrote? :O

Indeed: see also this thread!

Vierkantor · 2024-04-25T10:24:42Z

Mathlib/Analysis/Fourier/PoissonSummation.lean

  refine' (le_of_eq _).trans (ContinuousMap.norm_coe_le_norm _ ⟨-x, _⟩)
-  rw [ContinuousMap.restrict_apply_mk, ContinuousMap.comp_apply, ContinuousMap.coe_mk,
-    ContinuousMap.coe_mk, neg_neg]
-  exact ⟨by linarith [hx.2], by linarith [hx.1]⟩
+  · rw [ContinuousMap.restrict_apply_mk, ContinuousMap.comp_apply, ContinuousMap.coe_mk,
+      ContinuousMap.coe_mk, neg_neg]
+    exact ⟨by linarith [hx.2], by linarith [hx.1]⟩


Does this really deserve to be indented?

At that point, there are two goals, the second being

-x ∈ Icc (-x✝ + -S) (-x✝ + -R)

I do not understand though how Lean solves this one.

Oh, I think that I see now.

The "first goal" becomes identical to the second one after the rw. So, I guess that the final exact solves the current goal and then Lean realizes that it already knows how to solve that goal and closes the second one as well.

Vierkantor · 2024-04-25T10:28:16Z

Mathlib/RingTheory/Norm.lean

  letI : ∀ f : L →ₐ[K] E, Fintype (@AlgHom L F E _ _ _ _ f.toRingHom.toAlgebra) := ?_
-  rw [Fintype.prod_equiv algHomEquivSigma (fun σ : F →ₐ[K] E => _) fun σ => σ.1 pb.gen,
-    ← Finset.univ_sigma_univ, Finset.prod_sigma, ← Finset.prod_pow]
-  refine Finset.prod_congr rfl fun σ _ => ?_
-  · letI : Algebra L E := σ.toRingHom.toAlgebra
-    simp_rw [Finset.prod_const]
-    congr
-    exact AlgHom.card L F E
-  · intro σ
-    simp only [algHomEquivSigma, Equiv.coe_fn_mk, AlgHom.restrictDomain, AlgHom.comp_apply,
-      IsScalarTower.coe_toAlgHom']
+  · rw [Fintype.prod_equiv algHomEquivSigma (fun σ : F →ₐ[K] E => _) fun σ => σ.1 pb.gen,


(Can't add a suggestion here.) Should this be instead something like:

letI : ∀ f : L →ₐ[K] E, Fintype (@AlgHom L F E _ _ _ _ f.toRingHom.toAlgebra) := by ...

?

This was puzzling: the letI created an extra goal, wanting to figure out some function. I could not understand where this was used and removing the letI line simply worked!

Maybe this was an instance of an "unused letI"? Is there an "unused have/let" linter? Does it check for letI?

Vierkantor

LGTM otherwise. Thanks for this huge cleanup!

adomani · 2024-04-25T10:58:16Z

Anne, thank you very much for your review!

jcommelin · 2024-04-30T04:29:35Z

bors d+

mathlib-bors · 2024-04-30T04:29:37Z

✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

…gain

A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339.

adomani · 2024-04-30T09:02:40Z

bors r+

A PR analogous to #12338: reformatting proofs following the multiple goals linter of #12339.

mathlib-bors · 2024-04-30T10:36:00Z

Pull request successfully merged into master.

Build succeeded:

A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339.

A PR analogous to #12338: reformatting proofs following the multiple goals linter of #12339.

A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339.

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 PR analogous to #12338: reformatting proofs following the multiple goals linter of #12339.

A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339.

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]>

adomani added 2 commits April 23, 2024 09:03

chore: more cdots

d820f45

long lines

c17b20d

adomani added the awaiting-review label Apr 23, 2024

adomani mentioned this pull request Apr 23, 2024

[Merged by Bors] - chore: adapt to multiple goal linter 3 #12372

Closed

Merge branch 'master' into adomani/use_cdots_again

a8faf70

This was referenced Apr 23, 2024

[Merged by Bors] - chore: adapt to multiple goal linter 4 #12381

Closed

[Merged by Bors] - feat: the multiGoal linter #12339

Closed

adomani changed the title ~~chore: more cdots~~ chore: adapt to multiple goal linter 2 Apr 23, 2024

adomani added 5 commits April 23, 2024 17:25

a couple of extra additions

8d04735

Merge remote-tracking branch 'origin/master' into adomani/use_cdots_a…

16d0476

…gain

nilpotent

bf2b99e

Merge remote-tracking branch 'origin/master' into adomani/use_cdots_a…

686b10b

…gain

more fixes

ee08db0

Vierkantor reviewed Apr 25, 2024

View reviewed changes

Mathlib/RingTheory/Polynomial/Selmer.lean Outdated Show resolved Hide resolved

Vierkantor reviewed Apr 25, 2024

View reviewed changes

Vierkantor added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Apr 25, 2024

Anne's findings

92c99c6

adomani added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 25, 2024

github-actions bot added delegated and removed awaiting-review labels Apr 30, 2024

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 30, 2024

Merge remote-tracking branch 'origin/master' into adomani/use_cdots_a…

523d9bd

…gain

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 30, 2024

mathlib-bors bot pushed a commit that referenced this pull request Apr 30, 2024

chore: adapt to multiple goal linter 3 (#12372)

ce2e171

A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339.

mathlib-bors bot pushed a commit that referenced this pull request Apr 30, 2024

chore: adapt to multiple goal linter 2 (#12361)

fe96aa4

A PR analogous to #12338: reformatting proofs following the multiple goals linter of #12339.

mathlib-bors bot changed the title ~~chore: adapt to multiple goal linter 2~~ [Merged by Bors] - chore: adapt to multiple goal linter 2 Apr 30, 2024

mathlib-bors bot closed this Apr 30, 2024

mathlib-bors bot deleted the adomani/use_cdots_again branch April 30, 2024 10:36

mathlib-bors bot pushed a commit that referenced this pull request Apr 30, 2024

chore: adapt to multiple goal linter 3 (#12372)

d29b378

A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339.

apnelson1 pushed a commit that referenced this pull request May 12, 2024

chore: adapt to multiple goal linter 2 (#12361)

c38d260

A PR analogous to #12338: reformatting proofs following the multiple goals linter of #12339.

apnelson1 pushed a commit that referenced this pull request May 12, 2024

chore: adapt to multiple goal linter 3 (#12372)

986e06d

A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339.

callesonne pushed a commit that referenced this pull request May 16, 2024

chore: adapt to multiple goal linter 2 (#12361)

de4ab15

A PR analogous to #12338: reformatting proofs following the multiple goals linter of #12339.

callesonne pushed a commit that referenced this pull request May 16, 2024

chore: adapt to multiple goal linter 3 (#12372)

863d5c2

A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore: adapt to multiple goal linter 2 #12361

[Merged by Bors] - chore: adapt to multiple goal linter 2 #12361

adomani commented Apr 23, 2024

Vierkantor Apr 25, 2024

adomani Apr 25, 2024

Vierkantor Apr 25, 2024

adomani Apr 25, 2024

adomani Apr 25, 2024 •

edited

Loading

Vierkantor Apr 25, 2024

adomani Apr 25, 2024

Vierkantor left a comment

adomani commented Apr 25, 2024

jcommelin commented Apr 30, 2024

mathlib-bors bot commented Apr 30, 2024

adomani commented Apr 30, 2024

mathlib-bors bot commented Apr 30, 2024

[Merged by Bors] - chore: adapt to multiple goal linter 2 #12361

[Merged by Bors] - chore: adapt to multiple goal linter 2 #12361

Conversation

adomani commented Apr 23, 2024

Vierkantor Apr 25, 2024

Choose a reason for hiding this comment

adomani Apr 25, 2024

Choose a reason for hiding this comment

Vierkantor Apr 25, 2024

Choose a reason for hiding this comment

adomani Apr 25, 2024

Choose a reason for hiding this comment

adomani Apr 25, 2024 • edited Loading

Choose a reason for hiding this comment

Vierkantor Apr 25, 2024

Choose a reason for hiding this comment

adomani Apr 25, 2024

Choose a reason for hiding this comment

Vierkantor left a comment

Choose a reason for hiding this comment

adomani commented Apr 25, 2024

jcommelin commented Apr 30, 2024

mathlib-bors bot commented Apr 30, 2024

adomani commented Apr 30, 2024

mathlib-bors bot commented Apr 30, 2024

adomani Apr 25, 2024 •

edited

Loading