chore(data/finset): drop to_set, use has_lift instead (#2629)

Also cleanup `coe_to_finset` lemmas. Now we have `set.finite.coe_to_finset` and `set.coe_to_finset`.

Co-authored-by: Johan Commelin <johan@commelin.net>

src/algebra/direct_sum.lean

@@ -64,7 +64,7 @@ theorem mk_inj (s : finset ι) : function.injective (mk β s) :=
 dfinsupp.mk_inj s
 
 theorem of_inj (i : ι) : function.injective (of β i) :=
-λ x y H, congr_fun (mk_inj _ H) ⟨i, by simp [finset.to_set]⟩
+λ x y H, congr_fun (mk_inj _ H) ⟨i, by simp⟩
 
 @[elab_as_eliminator]
 protected theorem induction_on {C : direct_sum ι β → Prop}

src/data/finset.lean

@@ -47,9 +47,7 @@ multiset.decidable_mem _ _
 /-! ### set coercion -/
 
 /-- Convert a finset to a set in the natural way. -/
-def to_set (s : finset α) : set α := {x | x ∈ s}
-
-instance : has_lift (finset α) (set α) := ⟨to_set⟩
+instance : has_lift (finset α) (set α) := ⟨λ s, {x | x ∈ s}⟩
 
 @[simp] lemma mem_coe {a : α} {s : finset α} : a ∈ (↑s : set α) ↔ a ∈ s := iff.rfl
 
@@ -69,7 +67,7 @@ ext.2
 @[simp] theorem coe_inj {s₁ s₂ : finset α} : (↑s₁ : set α) = ↑s₂ ↔ s₁ = s₂ :=
 set.ext_iff.trans ext.symm
 
-lemma to_set_injective {α} : function.injective (finset.to_set : finset α → set α) :=
+lemma coe_injective {α} : function.injective (coe : finset α → set α) :=
 λ s t, coe_inj.1
 
 /-! ### subset -/
@@ -650,9 +648,6 @@ sdiff_subset_sdiff (subset.refl _) (empty_subset _)
 @[simp] lemma coe_sdiff (s₁ s₂ : finset α) : ↑(s₁ \ s₂) = (↑s₁ \ ↑s₂ : set α) :=
 set.ext $ λ _, mem_sdiff
 
-@[simp] lemma to_set_sdiff (s t : finset α) : (s \ t).to_set = s.to_set \ t.to_set :=
-by apply finset.coe_sdiff
-
 @[simp] theorem union_sdiff_self_eq_union {s t : finset α} : s ∪ (t \ s) = s ∪ t :=
 ext.2 $ λ a, by simp only [mem_union, mem_sdiff, or_iff_not_imp_left,
   imp_and_distrib, and_iff_left id]

src/data/finsupp.lean

@@ -915,7 +915,7 @@ section comap_domain
 the preimage of `l.support`, `comap_domain f l hf` is the finitely supported function
 from `α₁` to `γ` given by composing `l` with `f`. -/
 def comap_domain {α₁ α₂ γ : Type*} [has_zero γ]
-  (f : α₁ → α₂) (l : α₂ →₀ γ) (hf : set.inj_on f (f ⁻¹' l.support.to_set)) : α₁ →₀ γ :=
+  (f : α₁ → α₂) (l : α₂ →₀ γ) (hf : set.inj_on f (f ⁻¹' ↑l.support)) : α₁ →₀ γ :=
 { support := l.support.preimage hf,
   to_fun := (λ a, l (f a)),
   mem_support_to_fun :=
@@ -927,21 +927,21 @@ def comap_domain {α₁ α₂ γ : Type*} [has_zero γ]
 
 @[simp]
 lemma comap_domain_apply {α₁ α₂ γ : Type*} [has_zero γ]
-  (f : α₁ → α₂) (l : α₂ →₀ γ) (hf : set.inj_on f (f ⁻¹' l.support.to_set)) (a : α₁) :
+  (f : α₁ → α₂) (l : α₂ →₀ γ) (hf : set.inj_on f (f ⁻¹' ↑l.support)) (a : α₁) :
   comap_domain f l hf a = l (f a) :=
 rfl
 
 lemma sum_comap_domain {α₁ α₂ β γ : Type*} [has_zero β] [add_comm_monoid γ]
   (f : α₁ → α₂) (l : α₂ →₀ β) (g : α₂ → β → γ)
-  (hf : set.bij_on f (f ⁻¹' l.support.to_set) l.support.to_set) :
+  (hf : set.bij_on f (f ⁻¹' ↑l.support) ↑l.support) :
   (comap_domain f l hf.inj_on).sum (g ∘ f) = l.sum g :=
 begin
   simp [sum],
   simp [comap_domain, finset.sum_preimage f _ _ (λ (x : α₂), g x (l x))]
 end
 
 lemma eq_zero_of_comap_domain_eq_zero {α₁ α₂ γ : Type*} [add_comm_monoid γ]
-  (f : α₁ → α₂) (l : α₂ →₀ γ) (hf : set.bij_on f (f ⁻¹' l.support.to_set) l.support.to_set) :
+  (f : α₁ → α₂) (l : α₂ →₀ γ) (hf : set.bij_on f (f ⁻¹' ↑l.support) ↑l.support) :
    comap_domain f l hf.inj_on = 0 → l = 0 :=
 begin
   rw [← support_eq_empty, ← support_eq_empty, comap_domain],

src/data/fintype/basic.lean

@@ -231,6 +231,9 @@ by simp [to_finset]
 @[simp] theorem mem_to_finset_val {s : set α} [fintype s] {a : α} : a ∈ s.to_finset.1 ↔ a ∈ s :=
 mem_to_finset
 
+@[simp] theorem coe_to_finset (s : set α) [fintype s] : (↑s.to_finset : set α) = s :=
+set.ext $ λ _, mem_to_finset
+
 end set
 
 lemma finset.card_univ [fintype α] : (finset.univ : finset α).card = fintype.card α :=

src/data/set/finite.lean

@@ -2,12 +2,17 @@
 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
-
-Finite sets.
 -/
 import data.fintype.basic
 import algebra.big_operators
 
+/-!
+# Finite sets
+
+This file defines predicates `finite : set α → Prop` and `infinite : set α → Prop` and proves some
+basic facts about finite sets.
+-/
+
 open set function
 
 universes u v w x
@@ -30,13 +35,13 @@ classical.choice h
 
 /-- Get a finset from a finite set -/
 noncomputable def finite.to_finset {s : set α} (h : finite s) : finset α :=
-@set.to_finset _ _ (finite.fintype h)
+@set.to_finset _ _ h.fintype
 
 @[simp] theorem finite.mem_to_finset {s : set α} {h : finite s} {a : α} : a ∈ h.to_finset ↔ a ∈ s :=
-@mem_to_finset _ _ (finite.fintype h) _
+@mem_to_finset _ _ h.fintype _
 
-lemma finite.coe_to_finset {α} {s : set α} (h : finite s) : ↑h.to_finset = s :=
-by { ext, apply mem_to_finset }
+@[simp] lemma finite.coe_to_finset {α} {s : set α} (h : finite s) : ↑h.to_finset = s :=
+@set.coe_to_finset _ s h.fintype
 
 theorem finite.exists_finset {s : set α} : finite s →
   ∃ s' : finset α, ∀ a : α, a ∈ s' ↔ a ∈ s
@@ -76,6 +81,7 @@ eq.trans (by congr) empty_card
 
 @[simp] theorem finite_empty : @finite α ∅ := ⟨set.fintype_empty⟩
 
+/-- A `fintype` structure on `insert a s`. -/
 def fintype_insert' {a : α} (s : set α) [fintype s] (h : a ∉ s) : fintype (insert a s : set α) :=
 fintype.of_finset ⟨a :: s.to_finset.1,
   multiset.nodup_cons_of_nodup (by simp [h]) s.to_finset.2⟩ $ by simp
@@ -324,21 +330,11 @@ lemma finite_subsets_of_finite {α : Type u} {a : set α} (h : finite a) : finit
 begin
   -- we just need to translate the result, already known for finsets,
   -- to the language of finite sets
-  let s := coe '' ((finset.powerset (finite.to_finset h)).to_set),
+  let s : set (set α) := coe '' (↑(finset.powerset (finite.to_finset h)) : set (finset α)),
   have : finite s := finite_image _ (finite_mem_finset _),
-  have : {b | b ⊆ a} ⊆ s :=
-  begin
-    assume b hb,
-    rw [set.mem_image],
-    rw [set.mem_set_of_eq] at hb,
-    let b' : finset α := finite.to_finset (finite_subset h hb),
-    have : b' ∈ (finset.powerset (finite.to_finset h)).to_set :=
-      show b' ∈ (finset.powerset (finite.to_finset h)),
-        by simp [b', finset.subset_iff]; exact hb,
-    have : coe b' = b := by ext; simp,
-    exact ⟨b', by assumption, by assumption⟩
-  end,
-  exact finite_subset ‹finite s› this
+  apply finite_subset this,
+  refine λ b hb, ⟨(finite_subset h hb).to_finset, _, finite.coe_to_finset _⟩,
+  simpa [finset.subset_iff]
 end
 
 lemma exists_min_image [linear_order β] (s : set α) (f : α → β) (h1 : finite s) :
@@ -355,20 +351,14 @@ end set
 
 namespace finset
 variables [decidable_eq β]
-variables {s t u : finset α} {f : α → β} {a : α}
+variables {s : finset α}
 
 lemma finite_to_set (s : finset α) : set.finite (↑s : set α) :=
 set.finite_mem_finset s
 
 @[simp] lemma coe_bind {f : α → finset β} : ↑(s.bind f) = (⋃x ∈ (↑s : set α), ↑(f x) : set β) :=
 by simp [set.ext_iff]
 
-@[simp] lemma coe_to_finset {s : set α} {hs : set.finite s} : ↑(hs.to_finset) = s :=
-by simp [set.ext_iff]
-
-@[simp] lemma coe_to_finset' (s : set α) [fintype s] : (↑s.to_finset : set α) = s :=
-by ext; simp
-
 end finset
 
 namespace set
@@ -420,8 +410,7 @@ finite_subset (finset.finite_to_set $ finset.range (b + 1)) range_find_greatest_
 lemma card_lt_card {s t : set α} [fintype s] [fintype t] (h : s ⊂ t) :
   fintype.card s < fintype.card t :=
 begin
-  haveI := classical.prop_decidable,
-  rw [← finset.coe_to_finset' s, ← finset.coe_to_finset' t, finset.coe_ssubset] at h,
+  rw [← s.coe_to_finset, ← t.coe_to_finset, finset.coe_ssubset] at h,
   rw [fintype.card_of_finset' _ (λ x, mem_to_finset),
       fintype.card_of_finset' _ (λ x, mem_to_finset)],
   exact finset.card_lt_card h,
@@ -516,24 +505,25 @@ namespace finset
 
 section preimage
 
+/-- Preimage of `s : finset β` under a map `f` injective of `f ⁻¹' s` as a `finset`.  -/
 noncomputable def preimage {f : α → β} (s : finset β)
   (hf : set.inj_on f (f ⁻¹' ↑s)) : finset α :=
-set.finite.to_finset (set.finite_preimage hf (set.finite_mem_finset s))
+(set.finite_preimage hf (set.finite_mem_finset s)).to_finset
 
 @[simp] lemma mem_preimage {f : α → β} {s : finset β} {hf : set.inj_on f (f ⁻¹' ↑s)} {x : α} :
   x ∈ preimage s hf ↔ f x ∈ s :=
-by simp [preimage]
+set.finite.mem_to_finset
 
-@[simp] lemma coe_preimage {f : α → β} (s : finset β)
+@[simp, norm_cast] lemma coe_preimage {f : α → β} (s : finset β)
   (hf : set.inj_on f (f ⁻¹' ↑s)) : (↑(preimage s hf) : set α) = f ⁻¹' ↑s :=
-by simp [set.ext_iff]
+set.finite.coe_to_finset _
 
 lemma image_preimage [decidable_eq β] (f : α → β) (s : finset β)
-  (hf : set.bij_on f (f ⁻¹' s.to_set) s.to_set) :
+  (hf : set.bij_on f (f ⁻¹' ↑s) ↑s) :
   image f (preimage s hf.inj_on) = s :=
 finset.coe_inj.1 $
 suffices f '' (f ⁻¹' ↑s) = ↑s, by simpa,
-(set.subset.antisymm (image_preimage_subset _ _) hf.2.2)
+(set.subset.antisymm (image_preimage_subset _ _) hf.surj_on)
 
 end preimage
 

src/linear_algebra/basic.lean

@@ -1909,9 +1909,9 @@ lemma supr_range_std_basis_eq_infi_ker_proj {I J : set ι}
   (⨆i∈I, range (std_basis R φ i)) = (⨅i∈J, ker (proj i)) :=
 begin
   refine le_antisymm (supr_range_std_basis_le_infi_ker_proj _ _ _ _ hd) _,
-  have : set.univ ⊆ ↑hI.to_finset ∪ J, { rwa [finset.coe_to_finset] },
+  have : set.univ ⊆ ↑hI.to_finset ∪ J, { rwa [hI.coe_to_finset] },
   refine le_trans (infi_ker_proj_le_supr_range_std_basis R φ this) (supr_le_supr $ assume i, _),
-  rw [← finset.mem_coe, finset.coe_to_finset],
+  rw [set.finite.mem_to_finset],
   exact le_refl _
 end
 

src/linear_algebra/basis.lean

@@ -179,7 +179,7 @@ begin
   simp only [linear_map.comp_apply],
   split,
   { intros h l hl₁ hl₂,
-    have h_bij : bij_on subtype.val (subtype.val ⁻¹' l.support.to_set : set s) l.support.to_set,
+    have h_bij : bij_on subtype.val (subtype.val ⁻¹' ↑l.support : set s) ↑l.support,
     { apply bij_on.mk,
       { unfold maps_to },
       { apply subtype.val_injective.inj_on },
@@ -237,7 +237,7 @@ begin
   { apply linear_independent_of_zero_eq_one zero_eq_one },
   rw linear_independent_subtype,
   intros l hl₁ hl₂,
-  have h_bij : bij_on v (v ⁻¹' finset.to_set (l.support)) (finset.to_set (l.support)),
+  have h_bij : bij_on v (v ⁻¹' ↑l.support) ↑l.support,
   { apply bij_on.mk,
     { unfold maps_to },
     { apply (linear_independent.injective zero_eq_one hv).inj_on },
@@ -397,7 +397,7 @@ begin
     { simp only [(span_Union _).symm],
       refine span_mono (@supr_le_supr2 (set M) _ _ _ _ _ _),
       rintros ⟨i⟩, exact ⟨i, le_refl _⟩ },
-    { change finite (plift.up ⁻¹' s.to_set),
+    { change finite (plift.up ⁻¹' ↑s),
       exact finite_preimage (assume i j _ _, plift.up.inj) s.finite_to_set } }
 end
 

src/linear_algebra/dimension.lean

@@ -53,7 +53,7 @@ theorem is_basis.le_span (zero_ne_one : (0 : K) ≠ 1) {v : ι → V} {J : set V
 begin
   cases le_or_lt cardinal.omega (cardinal.mk J) with oJ oJ,
   { have := cardinal.mk_range_eq_of_inj  (linear_independent.injective zero_ne_one hv.1),
-    let S : J → set ι := λ j, (is_basis.repr hv j).support.to_set,
+    let S : J → set ι := λ j, ↑(is_basis.repr hv j).support,
     let S' : J → set V := λ j, v '' S j,
     have hs : range v ⊆ ⋃ j, S' j,
     { intros b hb,
@@ -79,8 +79,8 @@ begin
     { rwa [cardinal.sum_const, cardinal.mul_eq_max oJ (le_refl _), max_eq_left oJ] } },
   { rcases exists_finite_card_le_of_finite_of_linear_independent_of_span
       (cardinal.lt_omega_iff_finite.1 oJ) hv.1.to_subtype_range _ with ⟨fI, hi⟩,
-    { rwa [← cardinal.nat_cast_le, cardinal.finset_card, finset.coe_to_finset,
-        cardinal.finset_card, finset.coe_to_finset] at hi, },
+    { rwa [← cardinal.nat_cast_le, cardinal.finset_card, set.finite.coe_to_finset,
+        cardinal.finset_card, set.finite.coe_to_finset] at hi, },
     { rw hJ, apply set.subset_univ } },
 end
 end

src/linear_algebra/finsupp.lean

@@ -393,7 +393,7 @@ begin
 end
 
 lemma total_comap_domain
- (f : α → α') (l : α' →₀ R) (hf : set.inj_on f (f ⁻¹' l.support.to_set)) :
+ (f : α → α') (l : α' →₀ R) (hf : set.inj_on f (f ⁻¹' ↑l.support)) :
  finsupp.total α M R v (finsupp.comap_domain f l hf) = (l.support.preimage hf).sum (λ i, (l (f i)) • (v i)) :=
 by rw finsupp.total_apply; refl
 

src/ring_theory/adjoin.lean

@@ -154,12 +154,14 @@ namespace subalgebra
 variables {R : Type u} {A : Type v}
 variables [comm_ring R] [comm_ring A] [algebra R A]
 
+/-- A subalgebra `S` is finitely generated if there exists `t : finset A` such that
+`algebra.adjoin R t = S`. -/
 def fg (S : subalgebra R A) : Prop :=
 ∃ t : finset A, algebra.adjoin R ↑t = S
 
 theorem fg_def {S : subalgebra R A} : S.fg ↔ ∃ t : set A, set.finite t ∧ algebra.adjoin R t = S :=
 ⟨λ ⟨t, ht⟩, ⟨↑t, set.finite_mem_finset t, ht⟩,
-λ ⟨t, ht1, ht2⟩, ⟨ht1.to_finset, by rwa finset.coe_to_finset⟩⟩
+λ ⟨t, ht1, ht2⟩, ⟨ht1.to_finset, by rwa set.finite.coe_to_finset⟩⟩
 
 theorem fg_bot : (⊥ : subalgebra R A).fg :=
 ⟨∅, algebra.adjoin_empty R A⟩

src/ring_theory/free_comm_ring.lean

@@ -211,7 +211,7 @@ free_comm_ring.induction_on x
     (is_supported_upwards hxt $ set.subset_union_right s t)⟩)
 
 theorem exists_finset_support (x : free_comm_ring α) : ∃ s : finset α, is_supported x ↑s :=
-let ⟨s, hfs, hxs⟩ := exists_finite_support x in ⟨hfs.to_finset, by rwa finset.coe_to_finset⟩
+let ⟨s, hfs, hxs⟩ := exists_finite_support x in ⟨hfs.to_finset, by rwa set.finite.coe_to_finset⟩
 
 end free_comm_ring
 

src/ring_theory/noetherian.lean

@@ -369,7 +369,7 @@ instance is_noetherian_ring.to_is_noetherian {R : Type*} [ring R] :
 instance ring.is_noetherian_of_fintype (R M) [fintype M] [ring R] [add_comm_group M] [module R M] :
   is_noetherian R M :=
 by letI := classical.dec; exact
-⟨assume s, ⟨to_finset s, by rw [finset.coe_to_finset', submodule.span_eq]⟩⟩
+⟨assume s, ⟨to_finset s, by rw [set.coe_to_finset, submodule.span_eq]⟩⟩
 
 theorem ring.is_noetherian_of_zero_eq_one {R} [ring R] (h01 : (0 : R) = 1) : is_noetherian_ring R :=
 by haveI := subsingleton_of_zero_eq_one R h01;

src/set_theory/ordinal.lean

@@ -3168,7 +3168,7 @@ lemma mk_compl_of_omega_le {α : Type*} (s : set α) (h : omega ≤ #α) (h2 : #
 by { refine eq_of_add_eq_of_omega_le _ h2 h, exact mk_sum_compl s }
 
 lemma mk_compl_finset_of_omega_le {α : Type*} (s : finset α) (h : omega ≤ #α) :
-  #(-s.to_set : set α) = #α :=
+  #(-↑s : set α) = #α :=
 by { apply mk_compl_of_omega_le _ h, exact lt_of_lt_of_le (finset_card_lt_omega s) h }
 
 lemma mk_compl_eq_mk_compl_infinite {α : Type*} {s t : set α} (h : omega ≤ #α) (hs : #s < #α)