From da1ed0278a5fed432588cd4da870288f9b9becc7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Sat, 8 Apr 2023 19:06:09 -0600 Subject: [PATCH 1/6] is_well_founded_of_strict_order --- src/data/fintype/card.lean | 24 ++++++++---------------- 1 file changed, 8 insertions(+), 16 deletions(-) diff --git a/src/data/fintype/card.lean b/src/data/fintype/card.lean index 43d7bf3b7f0f5..a0953ddf82bf9 100644 --- a/src/data/fintype/card.lean +++ b/src/data/fintype/card.lean @@ -716,27 +716,19 @@ end namespace finite variables [finite α] -lemma well_founded_of_trans_of_irrefl (r : α → α → Prop) [is_trans α r] [is_irrefl α r] : - well_founded r := -by classical; casesI nonempty_fintype α; exact +instance is_well_founded_of_strict_order (r : α → α → Prop) [is_strict_order α r] : + is_well_founded α r := +⟨by classical; casesI nonempty_fintype α; exact have ∀ x y, r x y → (univ.filter (λ z, r z x)).card < (univ.filter (λ z, r z y)).card, from λ x y hxy, finset.card_lt_card $ by simp only [finset.lt_iff_ssubset.symm, lt_iff_le_not_le, finset.le_iff_subset, finset.subset_iff, mem_filter, true_and, mem_univ, hxy]; exact ⟨λ z hzx, trans hzx hxy, not_forall_of_exists_not ⟨x, not_imp.2 ⟨hxy, irrefl x⟩⟩⟩, -subrelation.wf this (measure_wf _) +subrelation.wf this (measure_wf _)⟩ -lemma preorder.well_founded_lt [preorder α] : well_founded ((<) : α → α → Prop) := -well_founded_of_trans_of_irrefl _ +@[priority 10] instance linear_order.is_well_order_lt [linear_order α] : is_well_order α (<) := { } -lemma preorder.well_founded_gt [preorder α] : well_founded ((>) : α → α → Prop) := -well_founded_of_trans_of_irrefl _ - -@[priority 10] instance linear_order.is_well_order_lt [linear_order α] : is_well_order α (<) := -{ wf := preorder.well_founded_lt } - -@[priority 10] instance linear_order.is_well_order_gt [linear_order α] : is_well_order α (>) := -{ wf := preorder.well_founded_gt } +@[priority 10] instance linear_order.is_well_order_gt [linear_order α] : is_well_order α (>) := { } end finite @@ -767,8 +759,8 @@ lemma finset.exists_minimal {α : Type*} [preorder α] (s : finset α) (h : s.no ∃ m ∈ s, ∀ x ∈ s, ¬ (x < m) := begin obtain ⟨c, hcs : c ∈ s⟩ := h, - have : well_founded (@has_lt.lt {x // x ∈ s} _) := finite.well_founded_of_trans_of_irrefl _, - obtain ⟨⟨m, hms : m ∈ s⟩, -, H⟩ := this.has_min set.univ ⟨⟨c, hcs⟩, trivial⟩, + have : is_well_founded _ (@has_lt.lt {x // x ∈ s} _) := by apply_instance, + obtain ⟨⟨m, hms : m ∈ s⟩, -, H⟩ := this.wf.has_min set.univ ⟨⟨c, hcs⟩, trivial⟩, exact ⟨m, hms, λ x hx hxm, H ⟨x, hx⟩ trivial hxm⟩, end From 746416b24be8df114ce8206877ee9f9b4a2d9711 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Sat, 8 Apr 2023 19:07:52 -0600 Subject: [PATCH 2/6] golf --- src/data/fintype/card.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/data/fintype/card.lean b/src/data/fintype/card.lean index a0953ddf82bf9..865c15bef8383 100644 --- a/src/data/fintype/card.lean +++ b/src/data/fintype/card.lean @@ -759,7 +759,7 @@ lemma finset.exists_minimal {α : Type*} [preorder α] (s : finset α) (h : s.no ∃ m ∈ s, ∀ x ∈ s, ¬ (x < m) := begin obtain ⟨c, hcs : c ∈ s⟩ := h, - have : is_well_founded _ (@has_lt.lt {x // x ∈ s} _) := by apply_instance, + have : well_founded_lt {x // x ∈ s} := by apply_instance, obtain ⟨⟨m, hms : m ∈ s⟩, -, H⟩ := this.wf.has_min set.univ ⟨⟨c, hcs⟩, trivial⟩, exact ⟨m, hms, λ x hx hxm, H ⟨x, hx⟩ trivial hxm⟩, end From 00a41841f845d82cd02851d5afa07655cd68be6e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Sat, 8 Apr 2023 19:26:21 -0600 Subject: [PATCH 3/6] fix --- src/data/fin/tuple/bubble_sort_induction.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/data/fin/tuple/bubble_sort_induction.lean b/src/data/fin/tuple/bubble_sort_induction.lean index 8b496b9e8de09..dd2cbdf9768a2 100644 --- a/src/data/fin/tuple/bubble_sort_induction.lean +++ b/src/data/fin/tuple/bubble_sort_induction.lean @@ -40,7 +40,7 @@ lemma bubble_sort_induction' {n : ℕ} {α : Type*} [linear_order α] {f : fin n begin letI := @preorder.lift _ (lex (fin n → α)) _ (λ σ : equiv.perm (fin n), to_lex (f ∘ σ)), refine @well_founded.induction_bot' _ _ _ - (@finite.preorder.well_founded_lt (equiv.perm (fin n)) _ _) + (@finite.is_well_founded_of_strict_order (equiv.perm (fin n)) _ (<) _).wf (equiv.refl _) (sort f) P (λ σ, f ∘ σ) (λ σ hσ hfσ, _) hf, obtain ⟨i, j, hij₁, hij₂⟩ := antitone_pair_of_not_sorted' hσ, exact ⟨σ * equiv.swap i j, pi.lex_desc hij₁ hij₂, h σ i j hij₁ hij₂ hfσ⟩, From 80117a28f1ffbda38de2da99edf3901d4019a3be Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Sat, 8 Apr 2023 19:26:35 -0600 Subject: [PATCH 4/6] golf --- src/data/fin/tuple/bubble_sort_induction.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/data/fin/tuple/bubble_sort_induction.lean b/src/data/fin/tuple/bubble_sort_induction.lean index dd2cbdf9768a2..085dc9b7635b5 100644 --- a/src/data/fin/tuple/bubble_sort_induction.lean +++ b/src/data/fin/tuple/bubble_sort_induction.lean @@ -40,7 +40,7 @@ lemma bubble_sort_induction' {n : ℕ} {α : Type*} [linear_order α] {f : fin n begin letI := @preorder.lift _ (lex (fin n → α)) _ (λ σ : equiv.perm (fin n), to_lex (f ∘ σ)), refine @well_founded.induction_bot' _ _ _ - (@finite.is_well_founded_of_strict_order (equiv.perm (fin n)) _ (<) _).wf + (@finite.is_well_founded_of_strict_order _ _ (<) _).wf (equiv.refl _) (sort f) P (λ σ, f ∘ σ) (λ σ hσ hfσ, _) hf, obtain ⟨i, j, hij₁, hij₂⟩ := antitone_pair_of_not_sorted' hσ, exact ⟨σ * equiv.swap i j, pi.lex_desc hij₁ hij₂, h σ i j hij₁ hij₂ hfσ⟩, From e9773aba5eff6e76f754adc796bad6177b3f2c4d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Sat, 8 Apr 2023 19:38:48 -0600 Subject: [PATCH 5/6] fix --- src/data/dfinsupp/well_founded.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/data/dfinsupp/well_founded.lean b/src/data/dfinsupp/well_founded.lean index a51551fba65f5..75ca8ac548d62 100644 --- a/src/data/dfinsupp/well_founded.lean +++ b/src/data/dfinsupp/well_founded.lean @@ -171,9 +171,9 @@ begin obtain h | ⟨⟨x⟩⟩ := is_empty_or_nonempty (Π i, α i), { convert empty_wf, ext1 x, exact (h.1 x).elim }, letI : Π i, has_zero (α i) := λ i, ⟨(hs i).min ⊤ ⟨x i, trivial⟩⟩, - haveI := is_trans.swap r, haveI := is_irrefl.swap r, haveI := fintype.of_finite ι, + haveI := is_strict_order.swap r, haveI := fintype.of_finite ι, refine inv_image.wf equiv_fun_on_fintype.symm (lex.well_founded' (λ i a, _) hs _), - exacts [(hs i).not_lt_min ⊤ _ trivial, finite.well_founded_of_trans_of_irrefl r.swap], + exacts [(hs i).not_lt_min ⊤ _ trivial, (finite.is_well_founded_of_strict_order r.swap).wf], end instance pi.lex.well_founded_lt [linear_order ι] [finite ι] [Π i, has_lt (α i)] From eba678adf8fbf09d78cfc981429f9a3cf66387dd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Sat, 8 Apr 2023 19:51:16 -0600 Subject: [PATCH 6/6] golf --- src/topology/noetherian_space.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/topology/noetherian_space.lean b/src/topology/noetherian_space.lean index 18d85a615a0f1..9bb0c461f46a5 100644 --- a/src/topology/noetherian_space.lean +++ b/src/topology/noetherian_space.lean @@ -174,7 +174,7 @@ end @[priority 100] instance finite.to_noetherian_space [finite α] : noetherian_space α := -⟨finite.well_founded_of_trans_of_irrefl _⟩ +⟨is_well_founded.wf⟩ lemma noetherian_space.exists_finset_irreducible [noetherian_space α] (s : closeds α) : ∃ S : finset (closeds α), (∀ k : S, is_irreducible (k : set α)) ∧ s = S.sup id :=