feat(data/set/basic): simp-normal form for ↥{x | p x} (#14441)

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

@@ -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 _)⟩,

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

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⟩) :=

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 _

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
 

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 β,

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