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.

Sign up for GitHub

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(Imo/Imo1998Q2): remove resolved porting notes #14505

Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - chore(Imo/Imo1998Q2): remove resolved porting notes #14505

Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
b20cc0b
chore(Imo/Imo1998Q2): remove porting note
mo271 Jul 8, 2024
5f8f603
Update Archive/Imo/Imo1998Q2.lean
mo271 Jul 8, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 4 additions & 6 deletions Archive/Imo/Imo1998Q2.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -130,19 +130,17 @@ theorem A_fibre_over_contestant_card (c : C) :
((A r).filter fun a : AgreedTriple C J => a.contestant = c).card := by
rw [A_fibre_over_contestant r]
apply Finset.card_image_of_injOn
-- Porting note (#10936): used to be `tidy`. TODO: remove `ext` after `extCore` to `aesop`.
unfold Set.InjOn; intros; ext; all_goals aesop
-- Porting note (#10936): used to be `tidy`.
Copy link
Collaborator

Choose a reason for hiding this comment

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

I guess this porting note is no longer actionable (the tidy tactic was not ported; aesop is meant to replace it), so tend towards removing it. I'll let a maintainer comment.

Copy link
Member

Choose a reason for hiding this comment

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

Yes, please remove it.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

done

unfold Set.InjOn
aesop
#align imo1998_q2.A_fibre_over_contestant_card Imo1998Q2.A_fibre_over_contestant_card

theorem A_fibre_over_judgePair {p : JudgePair J} (h : p.Distinct) :
agreedContestants r p = ((A r).filter fun a : AgreedTriple C J => a.judgePair = p).image
AgreedTriple.contestant := by
dsimp only [A, agreedContestants]; ext c; constructor <;> intro h
· rw [Finset.mem_image]; refine ⟨⟨c, p⟩, ?_⟩; aesop
-- Porting note: this used to be `finish`
· simp only [Finset.mem_filter, Finset.mem_image, Prod.exists] at h
rcases h with ⟨_, ⟨_, ⟨_, ⟨h, _⟩⟩⟩⟩
cases h; aesop
· aesop
#align imo1998_q2.A_fibre_over_judge_pair Imo1998Q2.A_fibre_over_judgePair

theorem A_fibre_over_judgePair_card {p : JudgePair J} (h : p.Distinct) :
Expand Down
Loading