Skip to content
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: adapt to multiple goal linter 2 #12361

Closed
wants to merge 10 commits into from

Conversation

adomani
Copy link
Collaborator

@adomani adomani commented Apr 23, 2024

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


Open in Gitpod

@adomani adomani changed the title chore: more cdots chore: adapt to multiple goal linter 2 Apr 23, 2024
@@ -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]
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Indeed: see also this thread!

Comment on lines 176 to +179
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]⟩
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does this really deserve to be indented?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator Author

@adomani adomani Apr 25, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Comment on lines 277 to 278
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,
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(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
    ...

?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Contributor

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM otherwise. Thanks for this huge cleanup!

@Vierkantor Vierkantor added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Apr 25, 2024
@adomani
Copy link
Collaborator Author

adomani commented Apr 25, 2024

Anne, thank you very much for your review!

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

bors d+

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Apr 30, 2024

✌️ 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.

@leanprover-community-mathlib4-bot 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
@leanprover-community-mathlib4-bot 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
A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339.
@adomani
Copy link
Collaborator Author

adomani commented Apr 30, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Apr 30, 2024
A PR analogous to #12338: reformatting proofs following the multiple goals linter of #12339.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Apr 30, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors 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 mathlib-bors bot closed this Apr 30, 2024
@mathlib-bors 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
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
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
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 May 13, 2024
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.
callesonne pushed a commit that referenced this pull request May 16, 2024
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
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
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.
grunweg pushed a commit that referenced this pull request May 17, 2024
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.
mathlib-bors bot pushed a commit that referenced this pull request Oct 21, 2024
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]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants