From 6b936a9d2daba3bf60f963c8dad157c741813c5b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Sun, 29 May 2022 09:04:36 +0000 Subject: [PATCH] =?UTF-8?q?feat(data/set/basic):=20simp-normal=20form=20fo?= =?UTF-8?q?r=20`=E2=86=A5{x=20|=20p=20x}`=20(#14441)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We make `{x // p x}` the simp-normal form for `↥{x | p x}`. We also rewrite some lemmas to use the former instead of the latter. --- archive/imo/imo1987_q1.lean | 11 ++++++----- src/algebra/algebraic_card.lean | 16 ++++++++-------- src/data/set/basic.lean | 5 +++-- src/set_theory/cardinal/basic.lean | 3 +++ src/set_theory/cardinal/cofinality.lean | 2 +- src/set_theory/cardinal/ordinal.lean | 2 +- src/tactic/subtype_instance.lean | 2 +- 7 files changed, 23 insertions(+), 18 deletions(-) diff --git a/archive/imo/imo1987_q1.lean b/archive/imo/imo1987_q1.lean index 5e7a5e4396f57..9dd606ffe31bb 100644 --- a/archive/imo/imo1987_q1.lean +++ b/archive/imo/imo1987_q1.lean @@ -30,15 +30,16 @@ namespace imo_1987_q1 /-- The set of pairs `(x : α, σ : perm α)` such that `σ x = x` is equivalent to the set of pairs `(x : α, σ : perm {x}ᶜ)`. -/ def fixed_points_equiv : - {σx : α × perm α | σx.2 σx.1 = σx.1} ≃ Σ x : α, perm ({x}ᶜ : set α) := -calc {σx : α × perm α | σx.2 σx.1 = σx.1} ≃ Σ x : α, {σ : perm α | σ x = x} : set_prod_equiv_sigma _ -... ≃ Σ x : α, {σ : perm α | ∀ y : ({x} : set α), σ y = equiv.refl ↥({x} : set α) y} : + {σx : α × perm α // σx.2 σx.1 = σx.1} ≃ Σ x : α, perm ({x}ᶜ : set α) := +calc {σx : α × perm α // σx.2 σx.1 = σx.1} ≃ Σ x : α, {σ : perm α // σ x = x} : + set_prod_equiv_sigma _ +... ≃ Σ x : α, {σ : perm α // ∀ y : ({x} : set α), σ y = equiv.refl ↥({x} : set α) y} : sigma_congr_right (λ x, equiv.set.of_eq $ by { simp only [set_coe.forall], dsimp, simp }) ... ≃ Σ x : α, perm ({x}ᶜ : set α) : sigma_congr_right (λ x, by apply equiv.set.compl) theorem card_fixed_points : - card {σx : α × perm α | σx.2 σx.1 = σx.1} = card α * (card α - 1)! := + card {σx : α × perm α // σx.2 σx.1 = σx.1} = card α * (card α - 1)! := by simp [card_congr (fixed_points_equiv α), card_perm, finset.filter_not, finset.card_sdiff, finset.filter_eq', finset.card_univ] @@ -60,7 +61,7 @@ It is easy to see that the cardinality of the LHS is given by `∑ k : fin (card α + 1), k * p α k`. -/ def fixed_points_equiv' : (Σ (k : fin (card α + 1)) (σ : fiber α k), fixed_points σ.1) ≃ - {σx : α × perm α | σx.2 σx.1 = σx.1} := + {σx : α × perm α // σx.2 σx.1 = σx.1} := { to_fun := λ p, ⟨⟨p.2.2, p.2.1⟩, p.2.2.2⟩, inv_fun := λ p, ⟨⟨card (fixed_points p.1.2), (card_subtype_le _).trans_lt (nat.lt_succ_self _)⟩, diff --git a/src/algebra/algebraic_card.lean b/src/algebra/algebraic_card.lean index cf43779263e5d..c0b4bbc4cbb90 100644 --- a/src/algebra/algebraic_card.lean +++ b/src/algebra/algebraic_card.lean @@ -25,7 +25,7 @@ open_locale cardinal namespace algebraic theorem omega_le_cardinal_mk_of_char_zero (R A : Type*) [comm_ring R] [is_domain R] - [ring A] [algebra R A] [char_zero A] : ω ≤ #{x : A | is_algebraic R x} := + [ring A] [algebra R A] [char_zero A] : ω ≤ #{x : A // is_algebraic R x} := @mk_le_of_injective (ulift ℕ) {x : A | is_algebraic R x} (λ n, ⟨_, is_algebraic_nat n.down⟩) (λ m n hmn, by simpa using hmn) @@ -35,7 +35,7 @@ variables (R : Type u) (A : Type v) [comm_ring R] [comm_ring A] [is_domain A] [a [no_zero_smul_divisors R A] theorem cardinal_mk_lift_le_mul : - cardinal.lift.{u v} (#{x : A | is_algebraic R x}) ≤ cardinal.lift.{v u} (#(polynomial R)) * ω := + cardinal.lift.{u v} (#{x : A // is_algebraic R x}) ≤ cardinal.lift.{v u} (#(polynomial R)) * ω := begin rw [←mk_ulift, ←mk_ulift], let g : ulift.{u} {x : A | is_algebraic R x} → ulift.{v} (polynomial R) := @@ -61,12 +61,12 @@ begin end theorem cardinal_mk_lift_le_max : - cardinal.lift.{u v} (#{x : A | is_algebraic R x}) ≤ max (cardinal.lift.{v u} (#R)) ω := + cardinal.lift.{u v} (#{x : A // is_algebraic R x}) ≤ max (cardinal.lift.{v u} (#R)) ω := (cardinal_mk_lift_le_mul R A).trans $ (mul_le_mul_right' (lift_le.2 cardinal_mk_le_max) _).trans $ by simp [le_total] theorem cardinal_mk_lift_le_of_infinite [infinite R] : - cardinal.lift.{u v} (#{x : A | is_algebraic R x}) ≤ cardinal.lift.{v u} (#R) := + cardinal.lift.{u v} (#{x : A // is_algebraic R x}) ≤ cardinal.lift.{v u} (#R) := (cardinal_mk_lift_le_max R A).trans $ by simp variable [encodable R] @@ -79,7 +79,7 @@ begin end @[simp] theorem cardinal_mk_of_encodable_of_char_zero [char_zero A] [is_domain R] : - #{x : A | is_algebraic R x} = ω := + #{x : A // is_algebraic R x} = ω := le_antisymm (by simp) (omega_le_cardinal_mk_of_char_zero R A) end lift @@ -89,13 +89,13 @@ section non_lift variables (R A : Type u) [comm_ring R] [comm_ring A] [is_domain A] [algebra R A] [no_zero_smul_divisors R A] -theorem cardinal_mk_le_mul : #{x : A | is_algebraic R x} ≤ #(polynomial R) * ω := +theorem cardinal_mk_le_mul : #{x : A // is_algebraic R x} ≤ #(polynomial R) * ω := by { rw [←lift_id (#_), ←lift_id (#(polynomial R))], exact cardinal_mk_lift_le_mul R A } -theorem cardinal_mk_le_max : #{x : A | is_algebraic R x} ≤ max (#R) ω := +theorem cardinal_mk_le_max : #{x : A // is_algebraic R x} ≤ max (#R) ω := by { rw [←lift_id (#_), ←lift_id (#R)], exact cardinal_mk_lift_le_max R A } -theorem cardinal_mk_le_of_infinite [infinite R] : #{x : A | is_algebraic R x} ≤ #R := +theorem cardinal_mk_le_of_infinite [infinite R] : #{x : A // is_algebraic R x} ≤ #R := (cardinal_mk_le_max R A).trans $ by simp end non_lift diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean index 13112795f24dd..036dab8064e28 100644 --- a/src/data/set/basic.lean +++ b/src/data/set/basic.lean @@ -126,8 +126,9 @@ section set_coe variables {α : Type u} -theorem set.set_coe_eq_subtype (s : set α) : - coe_sort.{(u+1) (u+2)} s = {x // x ∈ s} := rfl +theorem set.coe_eq_subtype (s : set α) : ↥s = {x // x ∈ s} := rfl + +@[simp] theorem set.coe_set_of (p : α → Prop) : ↥{x | p x} = {x // p x} := rfl @[simp] theorem set_coe.forall {s : set α} {p : s → Prop} : (∀ x : s, p x) ↔ (∀ x (h : x ∈ s), p ⟨x, h⟩) := diff --git a/src/set_theory/cardinal/basic.lean b/src/set_theory/cardinal/basic.lean index ee0f58c9dca64..68b634cdbbfc6 100644 --- a/src/set_theory/cardinal/basic.lean +++ b/src/set_theory/cardinal/basic.lean @@ -1030,6 +1030,9 @@ begin { rintro ⟨f, hf⟩, exact ⟨embedding.trans ⟨f, hf⟩ equiv.ulift.symm.to_embedding⟩ } end +@[simp] lemma mk_subtype_le_omega (p : α → Prop) : #{x // p x} ≤ ω ↔ countable {x | p x} := +mk_set_le_omega _ + @[simp] lemma omega_add_omega : ω + ω = ω := mk_denumerable _ lemma omega_mul_omega : ω * ω = ω := mk_denumerable _ diff --git a/src/set_theory/cardinal/cofinality.lean b/src/set_theory/cardinal/cofinality.lean index ed60c6137771b..95f56d6b35761 100644 --- a/src/set_theory/cardinal/cofinality.lean +++ b/src/set_theory/cardinal/cofinality.lean @@ -687,7 +687,7 @@ begin { rintro x ⟨hx, hx'⟩, exact hx }, { refine le_trans ha _, apply ge_of_eq, apply quotient.sound, constructor, refine equiv.trans _ (equiv.subtype_subtype_equiv_subtype_exists _ _).symm, - simp only [set_coe_eq_subtype, mem_singleton_iff, mem_preimage, mem_set_of_eq] }, + simp only [coe_eq_subtype, mem_singleton_iff, mem_preimage, mem_set_of_eq] }, rintro x ⟨hx, hx'⟩, exact hx' end diff --git a/src/set_theory/cardinal/ordinal.lean b/src/set_theory/cardinal/ordinal.lean index f800402dae50f..75591ffb3e522 100644 --- a/src/set_theory/cardinal/ordinal.lean +++ b/src/set_theory/cardinal/ordinal.lean @@ -697,7 +697,7 @@ calc #(finset α) ≤ #(list α) : mk_le_of_surjective list.to_finset_surjective ... = #α : mk_list_eq_mk α lemma mk_bounded_set_le_of_infinite (α : Type u) [infinite α] (c : cardinal) : - #{t : set α // mk t ≤ c} ≤ #α ^ c := + #{t : set α // #t ≤ c} ≤ #α ^ c := begin refine le_trans _ (by rw [←add_one_eq (omega_le_mk α)]), induction c using cardinal.induction_on with β, diff --git a/src/tactic/subtype_instance.lean b/src/tactic/subtype_instance.lean index e8209db65bb77..5160037818792 100644 --- a/src/tactic/subtype_instance.lean +++ b/src/tactic/subtype_instance.lean @@ -24,7 +24,7 @@ do field ← get_current_field, b ← target >>= is_prop, if b then do - `[simp [subtype.ext_iff_val], dsimp [set.set_coe_eq_subtype]], + `[simp [subtype.ext_iff_val], dsimp [set.coe_eq_subtype]], intros, applyc field; assumption else do