From b20cc0be5d6c077566db91acb84c732d97f21dc7 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Mon, 8 Jul 2024 11:13:33 +0200 Subject: [PATCH 1/2] chore(Imo/Imo1998Q2): remove porting note --- Archive/Imo/Imo1998Q2.lean | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/Archive/Imo/Imo1998Q2.lean b/Archive/Imo/Imo1998Q2.lean index 3e4180353dd8cd..3d665a102adef8 100644 --- a/Archive/Imo/Imo1998Q2.lean +++ b/Archive/Imo/Imo1998Q2.lean @@ -130,8 +130,9 @@ 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`. + 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) : @@ -139,10 +140,7 @@ theorem A_fibre_over_judgePair {p : JudgePair J} (h : p.Distinct) : 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) : From 5f8f603d6bf2218c6fa24fa3dba46fd51cd6d1b7 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Mon, 8 Jul 2024 17:07:17 +0200 Subject: [PATCH 2/2] Update Archive/Imo/Imo1998Q2.lean --- Archive/Imo/Imo1998Q2.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Archive/Imo/Imo1998Q2.lean b/Archive/Imo/Imo1998Q2.lean index 3d665a102adef8..8f0e4d140b7605 100644 --- a/Archive/Imo/Imo1998Q2.lean +++ b/Archive/Imo/Imo1998Q2.lean @@ -130,7 +130,6 @@ 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`. unfold Set.InjOn aesop #align imo1998_q2.A_fibre_over_contestant_card Imo1998Q2.A_fibre_over_contestant_card