chore(*): make sure definitions don't generate s x, s : set _ (#3591

)

Fix the following definitions: `subtype.fintype`, `pfun.dom`, `pfun.as_subtype`, `pfun.equiv_subtype`.

src/data/fintype/basic.lean

@@ -546,8 +546,11 @@ instance Prop.fintype : fintype Prop :=
 ⟨⟨true::false::0, by simp [true_ne_false]⟩,
  classical.cases (by simp) (by simp)⟩
 
+instance subtype.fintype (p : α → Prop) [decidable_pred p] [fintype α] : fintype {x // p x} :=
+fintype.subtype (univ.filter p) (by simp)
+
 def set_fintype {α} [fintype α] (s : set α) [decidable_pred s] : fintype s :=
-fintype.subtype (univ.filter (∈ s)) (by simp)
+subtype.fintype (λ x, x ∈ s)
 
 namespace function.embedding
 
@@ -637,9 +640,6 @@ instance finset.fintype [fintype α] : fintype (finset α) :=
   fintype.card (finset α) = 2 ^ (fintype.card α) :=
 finset.card_powerset finset.univ
 
-instance subtype.fintype (p : α → Prop) [decidable_pred p] [fintype α] : fintype {x // p x} :=
-set_fintype _
-
 @[simp] lemma set.to_finset_univ [fintype α] :
   (set.univ : set α).to_finset = finset.univ :=
 by { ext, simp only [set.mem_univ, mem_univ, set.mem_to_finset] }
@@ -655,7 +655,7 @@ by rw fintype.subtype_card; exact card_le_of_subset (subset_univ _)
 theorem fintype.card_subtype_lt [fintype α] {p : α → Prop} [decidable_pred p]
   {x : α} (hx : ¬ p x) : fintype.card {x // p x} < fintype.card α :=
 by rw [fintype.subtype_card]; exact finset.card_lt_card
-  ⟨subset_univ _, classical.not_forall.2 ⟨x, by simp [*, set.mem_def]⟩⟩
+  ⟨subset_univ _, classical.not_forall.2 ⟨x, by simp [hx]⟩⟩
 
 instance psigma.fintype {α : Type*} {β : α → Type*} [fintype α] [∀ a, fintype (β a)] :
   fintype (Σ' a, β a) :=

src/data/pfun.lean

@@ -317,10 +317,10 @@ variables {α : Type*} {β : Type*} {γ : Type*}
 instance : inhabited (α →. β) := ⟨λ a, roption.none⟩
 
 /-- The domain of a partial function -/
-def dom (f : α →. β) : set α := λ a, (f a).dom
+def dom (f : α →. β) : set α := {a | (f a).dom}
 
 theorem mem_dom (f : α →. β) (x : α) : x ∈ dom f ↔ ∃ y, y ∈ f x :=
-by simp [dom, set.mem_def, roption.dom_iff_mem]
+by simp [dom, roption.dom_iff_mem]
 
 theorem dom_eq (f : α →. β) : dom f = {x | ∃ y, y ∈ f x} :=
 set.ext (mem_dom f)
@@ -342,11 +342,13 @@ theorem ext {f g : α →. β} (H : ∀ a b, b ∈ f a ↔ b ∈ g a) : f = g :=
 funext $ λ a, roption.ext (H a)
 
 /-- Turn a partial function into a function out of a subtype -/
-def as_subtype (f : α →. β) (s : {x // f.dom x}) : β := f.fn s.1 s.2
+def as_subtype (f : α →. β) (s : f.dom) : β := f.fn s s.2
 
+/-- The set of partial functions `α →. β` is equivalent to
+the set of pairs `(p : α → Prop, f : subtype p → β)`. -/
 def equiv_subtype : (α →. β) ≃ (Σ p : α → Prop, subtype p → β) :=
-⟨λ f, ⟨f.dom, as_subtype f⟩,
- λ ⟨p, f⟩ x, ⟨p x, λ h, f ⟨x, h⟩⟩,
+⟨λ f, ⟨λ a, (f a).dom, as_subtype f⟩,
+ λ f x, ⟨f.1 x, λ h, f.2 ⟨x, h⟩⟩,
  λ f, funext $ λ a, roption.eta _,
  λ ⟨p, f⟩, by dsimp; congr; funext a; cases a; refl⟩
 

src/data/set/basic.lean

@@ -1645,11 +1645,14 @@ range_coe
   range (coe : subtype p → α) = {x | p x} :=
 range_coe
 
+@[simp] lemma coe_preimage_self (s : set α) : (coe : s → α) ⁻¹' s = univ :=
+by rw [← preimage_range (coe : s → α), range_coe]
+
 lemma range_val_subtype {p : α → Prop} :
   range (subtype.val : subtype p → α) = {x | p x} :=
 range_coe
 
-theorem coe_image_subset (s : set α) (t : set s) : t.image coe ⊆ s :=
+theorem coe_image_subset (s : set α) (t : set s) : coe '' t ⊆ s :=
 λ x ⟨y, yt, yvaleq⟩, by rw ←yvaleq; exact y.property
 
 theorem coe_image_univ (s : set α) : (coe : s → α) '' set.univ = s :=

src/data/set/countable.lean

@@ -83,15 +83,13 @@ lemma countable_encodable [encodable α] (s : set α) : countable s :=
 lemma countable.exists_surjective {s : set α} (hc : countable s) (hs : s.nonempty) :
   ∃f:ℕ → α, s = range f :=
 begin
-  rcases hs with ⟨x, hx⟩,
   letI : encodable s := countable.to_encodable hc,
-  letI : inhabited s := ⟨⟨x, hx⟩⟩,
+  letI : nonempty s := hs.to_subtype,
   have : countable (univ : set s) := countable_encodable _,
   rcases countable_iff_exists_surjective.1 this with ⟨g, hg⟩,
   have : range g = univ := univ_subset_iff.1 hg,
   use coe ∘ g,
-  rw [range_comp, this],
-  simp only [image_univ, subtype.range_coe, mem_def]
+  simp only [range_comp, this, image_univ, subtype.range_coe]
 end
 
 @[simp] lemma countable_empty : countable (∅ : set α) :=

src/data/set/lattice.lean

@@ -527,10 +527,10 @@ lemma sInter_eq_bInter {s : set (set α)} : (⋂₀ s) = (⋂ (i : set α) (h :
 by rw [← sInter_image, image_id']
 
 lemma sUnion_eq_Union {s : set (set α)} : (⋃₀ s) = (⋃ (i : s), i) :=
-by simp only [←sUnion_range, subtype.range_coe, mem_def]
+by simp only [←sUnion_range, subtype.range_coe]
 
 lemma sInter_eq_Inter {s : set (set α)} : (⋂₀ s) = (⋂ (i : s), i) :=
-by simp only [←sInter_range, subtype.range_coe, mem_def]
+by simp only [←sInter_range, subtype.range_coe]
 
 lemma union_eq_Union {s₁ s₂ : set α} : s₁ ∪ s₂ = ⋃ b : bool, cond b s₁ s₂ :=
 set.ext $ λ x, by simp [bool.exists_bool, or_comm]

src/linear_algebra/basic.lean

@@ -768,7 +768,7 @@ mem_sup.trans $ by simp only [submodule.exists, coe_mk]
 
 end
 
-lemma mem_span_singleton_self (x : M) : x ∈ span R ({x} : set M) := subset_span (mem_def.mpr rfl)
+lemma mem_span_singleton_self (x : M) : x ∈ span R ({x} : set M) := subset_span rfl
 
 lemma mem_span_singleton {y : M} : x ∈ span R ({y} : set M) ↔ ∃ a:R, a • y = x :=
 ⟨λ h, begin