wip

src/algebra/big_operators/basic.lean

@@ -530,7 +530,7 @@ prod_attach
 lemma prod_subtype {p : α → Prop} {F : fintype (subtype p)} (s : finset α)
   (h : ∀ x, x ∈ s ↔ p x) (f : α → β) :
   ∏ a in s, f a = ∏ a : subtype p, f a :=
-have (∈ s) = p, from set.ext h, by { substI p, rw [←prod_finset_coe], congr }
+have (∈ s) = p, by { ext, rw h }, by { substI p, rw [←prod_finset_coe], congr }
 
 @[to_additive]
 lemma prod_eq_one {f : α → β} {s : finset α} (h : ∀x∈s, f x = 1) : (∏ x in s, f x) = 1 :=
@@ -1428,4 +1428,3 @@ begin
     simp only [his, finset.sum_insert, not_false_iff],
     exact (int.nat_abs_add_le _ _).trans (add_le_add le_rfl IH) }
 end
-

src/algebra/pointwise.lean

@@ -333,7 +333,7 @@ image_prod _
 
 theorem range_smul_range [has_scalar α β] {ι κ : Type*} (b : ι → α) (c : κ → β) :
   range b • range c = range (λ p : ι × κ, b p.1 • c p.2) :=
-ext $ λ x, ⟨λ hx, let ⟨p, q, ⟨i, hi⟩, ⟨j, hj⟩, hpq⟩ := set.mem_smul.1 hx in
+set.ext $ λ x, ⟨λ hx, let ⟨p, q, ⟨i, hi⟩, ⟨j, hj⟩, hpq⟩ := set.mem_smul.1 hx in
   ⟨(i, j), hpq ▸ hi ▸ hj ▸ rfl⟩,
 λ ⟨⟨i, j⟩, h⟩, set.mem_smul.2 ⟨b i, c j, ⟨i, rfl⟩, ⟨j, rfl⟩, h⟩⟩
 
@@ -498,7 +498,7 @@ begin
     simpa only [true_and, true_or, eq_self_iff_true, finset.mem_insert], },
   { suffices g : (s : set M) ⊆ insert x T * insert y T', { norm_cast at g, assumption, },
     transitivity ↑(T * T'),
-    apply h,
+    exact coe_subset.2 h,
     rw finset.coe_mul,
     apply set.mul_subset_mul (set.subset_insert x T) (set.subset_insert y T'), },
 end

src/category_theory/essential_image.lean

@@ -35,13 +35,13 @@ isomorphic to an object in the image of the function `F.obj`. In other words, th
 under isomorphism of the function `F.obj`.
 This is the "non-evil" way of describing the image of a functor.
 -/
-def ess_image (F : C ⥤ D) : set D := λ Y, ∃ (X : C), nonempty (F.obj X ≅ Y)
+def ess_image (F : C ⥤ D) : set D := { Y | ∃ (X : C), nonempty (F.obj X ≅ Y) }
 
 /-- Get the witnessing object that `Y` is in the subcategory given by `F`. -/
 def ess_image.witness {Y : D} (h : Y ∈ F.ess_image) : C := h.some
 
 /-- Extract the isomorphism between `F.obj h.witness` and `Y` itself. -/
-def ess_image.get_iso {Y : D} (h : Y ∈ F.ess_image) : F.obj h.witness ≅ Y :=
+def ess_image.get_iso {Y : D} (h : Y ∈ F.ess_image) : F.obj (ess_image.witness h) ≅ Y :=
 classical.choice h.some_spec
 
 /-- Being in the essential image is a "hygenic" property: it is preserved under isomorphism. -/
@@ -102,17 +102,19 @@ class ess_surj (F : C ⥤ D) : Prop :=
 (mem_ess_image [] (Y : D) : Y ∈ F.ess_image)
 
 instance : ess_surj F.to_ess_image :=
-{ mem_ess_image := λ ⟨Y, hY⟩, ⟨_, ⟨⟨_, _, hY.get_iso.hom_inv_id, hY.get_iso.inv_hom_id⟩⟩⟩ }
+{ mem_ess_image := λ ⟨Y, hY⟩,
+  ⟨_, ⟨⟨_, _, (functor.ess_image.get_iso hY).hom_inv_id,
+    (functor.ess_image.get_iso hY).inv_hom_id⟩⟩⟩ }
 
 variables (F) [ess_surj F]
 
 /-- Given an essentially surjective functor, we can find a preimage for every object `Y` in the
     codomain. Applying the functor to this preimage will yield an object isomorphic to `Y`, see
     `obj_obj_preimage_iso`. -/
-def functor.obj_preimage (Y : D) : C := (ess_surj.mem_ess_image F Y).witness
+def functor.obj_preimage (Y : D) : C := functor.ess_image.witness (ess_surj.mem_ess_image F Y)
 /-- Applying an essentially surjective functor to a preimage of `Y` yields an object that is
     isomorphic to `Y`. -/
 def functor.obj_obj_preimage_iso (Y : D) : F.obj (F.obj_preimage Y) ≅ Y :=
-(ess_surj.mem_ess_image F Y).get_iso
+functor.ess_image.get_iso (ess_surj.mem_ess_image F Y)
 
 end category_theory

src/combinatorics/hall.lean

@@ -211,8 +211,9 @@ begin
   { apply nat.le_of_lt_succ,
     rw ←hn,
     convert (card_compl_lt_iff_nonempty _).mpr hs,
-    convert fintype.card_coe (sᶜ),
-    exact (finset.coe_compl s).symm },
+    rw ← fintype.card_coe sᶜ,
+    congr' 1,
+    show subtype _ = subtype _, simp },
   rcases ih t'' card_ι''_le (hall_cond_of_compl hus ht) with ⟨f'', hf'', hsf''⟩,
   /- Put them together -/
   have f'_mem_bUnion : ∀ {x'} (hx' : x' ∈ s), f' ⟨x', hx'⟩ ∈ s.bUnion t,

src/combinatorics/quiver.lean

@@ -155,7 +155,7 @@ def wide_subquiver_equiv_set_total {V} [quiver V] :
   wide_subquiver V ≃ set (total V) :=
 { to_fun := λ H, { e | e.hom ∈ H e.left e.right },
   inv_fun := λ S a b, { e | total.mk a b e ∈ S },
-  left_inv := λ H, rfl,
+  left_inv := by { intro, ext, refl },
   right_inv := by { intro S, ext, cases x, refl } }
 
 /-- `G.path a b` is the type of paths from `a` to `b` through the arrows of `G`. -/

src/combinatorics/simple_graph/basic.lean

@@ -101,10 +101,10 @@ namespace simple_graph
 variables {V : Type u} (G : simple_graph V)
 
 /-- `G.neighbor_set v` is the set of vertices adjacent to `v` in `G`. -/
-def neighbor_set (v : V) : set V := set_of (G.adj v)
+def neighbor_set (v : V) : set V := { w | G.adj v w }
 
 instance neighbor_set.mem_decidable (v : V) [decidable_rel G.adj] :
-  decidable_pred (G.neighbor_set v) := by { unfold neighbor_set, apply_instance }
+  decidable_pred (∈ G.neighbor_set v) := by { unfold neighbor_set, apply_instance }
 
 lemma ne_of_adj {a b : V} (hab : G.adj a b) : a ≠ b :=
 by { rintro rfl, exact G.loopless a hab }
@@ -152,13 +152,13 @@ begin
 end
 
 instance edge_set_decidable_pred [decidable_rel G.adj] :
-  decidable_pred G.edge_set := sym2.from_rel.decidable_pred _
+  decidable_pred (∈ G.edge_set) := sym2.from_rel.decidable_pred _
 
 instance edges_fintype [decidable_eq V] [fintype V] [decidable_rel G.adj] :
   fintype G.edge_set := subtype.fintype _
 
 instance incidence_set_decidable_pred [decidable_eq V] [decidable_rel G.adj] (v : V) :
-  decidable_pred (G.incidence_set v) := λ e, and.decidable
+  decidable_pred (∈ G.incidence_set v) := λ e, and.decidable
 
 /--
 The `edge_set` of the graph as a `finset`.
@@ -224,7 +224,8 @@ lemma not_mem_common_neighbors_right (v w : V) : w ∉ G.common_neighbors v w :=
 lemma common_neighbors_subset_neighbor_set (v w : V) : G.common_neighbors v w ⊆ G.neighbor_set v :=
 by simp [common_neighbors]
 
-instance [decidable_rel G.adj] (v w : V) : decidable_pred (G.common_neighbors v w) :=
+instance common_neighbors.decidable [decidable_rel G.adj] (v w : V) :
+  decidable_pred (∈ G.common_neighbors v w) :=
 λ a, and.decidable
 
 section incidence

src/computability/DFA.lean

@@ -42,7 +42,7 @@ def eval := M.eval_from M.start
 
 /-- `M.accepts` is the language of `x` such that `M.eval x` is an accept state. -/
 def accepts : language α :=
-λ x, M.eval x ∈ M.accept
+{ x | M.eval x ∈ M.accept }
 
 lemma mem_accepts (x : list α) : x ∈ M.accepts ↔ M.eval_from M.start x ∈ M.accept := by refl
 

src/computability/NFA.lean

@@ -53,7 +53,7 @@ def eval := M.eval_from M.start
 
 /-- `M.accepts` is the language of `x` such that there is an accept state in `M.eval x`. -/
 def accepts : language α :=
-λ x, ∃ S ∈ M.accept, S ∈ M.eval x
+{ x | ∃ S ∈ M.accept, S ∈ M.eval x }
 
 /-- `M.to_DFA` is an `DFA` constructed from a `NFA` `M` using the subset construction. The
   states is the type of `set`s of `M.state` and the step function is `M.step_set`. -/

src/computability/epsilon_NFA.lean

@@ -35,11 +35,20 @@ namespace ε_NFA
 
 instance : inhabited (ε_NFA α σ) := ⟨ ε_NFA.mk (λ _ _, ∅) ∅ ∅ ⟩
 
+/-- Use `ε_closure` instead. -/
+inductive ε_closure_pred : set σ → σ → Prop
+| base : ∀ S (s ∈ S), ε_closure_pred S s
+| step : ∀ S s (t ∈ M.step s none), ε_closure_pred S s → ε_closure_pred S t
+
 /-- The `ε_closure` of a set is the set of states which can be reached by taking a finite string of
   ε-transitions from an element of the the set -/
-inductive ε_closure : set σ → set σ
-| base : ∀ S (s ∈ S), ε_closure S s
-| step : ∀ S s (t ∈ M.step s none), ε_closure S s → ε_closure S t
+def ε_closure (S : set σ) : set σ := { s | ε_closure_pred M S s }
+
+lemma ε_closure.base {S} (s ∈ S) : s ∈ ε_closure M S :=
+ε_closure_pred.base _ _ H
+
+lemma ε_closure.step {S s} (t ∈ M.step s none) : s ∈ ε_closure M S → t ∈ ε_closure M S :=
+ε_closure_pred.step _ _ _ H
 
 /-- `M.step_set S a` is the union of the ε-closure of `M.step s a` for all `s ∈ S`. -/
 def step_set : set σ → α → set σ :=
@@ -56,7 +65,7 @@ def eval := M.eval_from M.start
 
 /-- `M.accepts` is the language of `x` such that there is an accept state in `M.eval x`. -/
 def accepts : language α :=
-λ x, ∃ S ∈ M.accept, S ∈ M.eval x
+{ x | ∃ S ∈ M.accept, S ∈ M.eval x }
 
 /-- `M.to_NFA` is an `NFA` constructed from an `ε_NFA` `M`. -/
 def to_NFA : NFA α σ :=

src/computability/language.lean

@@ -36,7 +36,7 @@ instance : has_one (language α) := ⟨{[]}⟩
 instance : inhabited (language α) := ⟨0⟩
 
 /-- The sum of two languages is the union of  -/
-instance : has_add (language α) := ⟨set.union⟩
+instance : has_add (language α) := ⟨(∪)⟩
 instance : has_mul (language α) := ⟨set.image2 (++)⟩
 
 lemma zero_def : (0 : language α) = (∅ : set _) := rfl

src/computability/reduce.lean

@@ -112,7 +112,7 @@ theorem computable_of_many_one_reducible
   (h₁ : p ≤₀ q) (h₂ : computable_pred q) : computable_pred p :=
 begin
   rcases h₁ with ⟨f, c, hf⟩,
-  rw [show p = λ a, q (f a), from set.ext hf],
+  rw [show p = λ a, q (f a), by ext; rw hf],
   rcases computable_iff.1 h₂ with ⟨g, hg, rfl⟩,
   exact ⟨by apply_instance, by simpa using hg.comp c⟩
 end
@@ -271,37 +271,37 @@ variables {γ : Type w} [primcodable γ] [inhabited γ]
 /--
 Computable and injective mapping of predicates to sets of natural numbers.
 -/
-def to_nat (p : set α) : set ℕ :=
-{ n | p ((encodable.decode α n).get_or_else (default α)) }
+def to_nat (p : α → Prop) : ℕ → Prop :=
+λ n, p ((encodable.decode α n).get_or_else (default α))
 
 @[simp]
-lemma to_nat_many_one_reducible {p : set α} : to_nat p ≤₀ p :=
+lemma to_nat_many_one_reducible {p : α → Prop} : to_nat p ≤₀ p :=
 ⟨λ n, (encodable.decode α n).get_or_else (default α),
  computable.option_get_or_else computable.decode (computable.const _),
  λ _, iff.rfl⟩
 
 @[simp]
-lemma many_one_reducible_to_nat {p : set α} : p ≤₀ to_nat p :=
-⟨encodable.encode, computable.encode, by simp [to_nat, set_of]⟩
+lemma many_one_reducible_to_nat {p : α → Prop} : p ≤₀ to_nat p :=
+⟨encodable.encode, computable.encode, by simp [to_nat]⟩
 
 @[simp]
-lemma many_one_reducible_to_nat_to_nat {p : set α} {q : set β} :
+lemma many_one_reducible_to_nat_to_nat {p : α → Prop} {q : β → Prop} :
   to_nat p ≤₀ to_nat q ↔ p ≤₀ q :=
 ⟨λ h, many_one_reducible_to_nat.trans (h.trans to_nat_many_one_reducible),
  λ h, to_nat_many_one_reducible.trans (h.trans many_one_reducible_to_nat)⟩
 
 @[simp]
-lemma to_nat_many_one_equiv {p : set α} : many_one_equiv (to_nat p) p :=
+lemma to_nat_many_one_equiv {p : α → Prop} : many_one_equiv (to_nat p) p :=
 by simp [many_one_equiv]
 
 @[simp]
-lemma many_one_equiv_to_nat (p : set α) (q : set β) :
+lemma many_one_equiv_to_nat (p : α → Prop) (q : β → Prop) :
   many_one_equiv (to_nat p) (to_nat q) ↔ many_one_equiv p q :=
 by simp [many_one_equiv]
 
 /-- A many-one degree is an equivalence class of sets up to many-one equivalence. -/
 def many_one_degree : Type :=
-quotient (⟨many_one_equiv, equivalence_of_many_one_equiv⟩ : setoid (set ℕ))
+quotient (⟨many_one_equiv, equivalence_of_many_one_equiv⟩ : setoid (ℕ → Prop))
 
 namespace many_one_degree
 
@@ -311,19 +311,19 @@ quotient.mk' (to_nat p)
 
 @[elab_as_eliminator]
 protected lemma ind_on {C : many_one_degree → Prop} (d : many_one_degree)
-  (h : ∀ p : set ℕ, C (of p)) : C d :=
+  (h : ∀ p : ℕ → Prop, C (of p)) : C d :=
 quotient.induction_on' d h
 
 /--
 Lifts a function on sets of natural numbers to many-one degrees.
 -/
 @[elab_as_eliminator, reducible]
-protected def lift_on {φ} (d : many_one_degree) (f : set ℕ → φ)
+protected def lift_on {φ} (d : many_one_degree) (f : (ℕ → Prop) → φ)
   (h : ∀ p q, many_one_equiv p q → f p = f q) : φ :=
 quotient.lift_on' d f h
 
 @[simp]
-protected lemma lift_on_eq {φ} (p : set ℕ) (f : set ℕ → φ)
+protected lemma lift_on_eq {φ} (p : ℕ → Prop) (f : (ℕ → Prop) → φ)
     (h : ∀ p q, many_one_equiv p q → f p = f q) :
   (of p).lift_on f h = f p :=
 rfl
@@ -332,7 +332,7 @@ rfl
 Lifts a binary function on sets of natural numbers to many-one degrees.
 -/
 @[elab_as_eliminator, reducible, simp]
-protected def lift_on₂ {φ} (d₁ d₂ : many_one_degree) (f : set ℕ → set ℕ → φ)
+protected def lift_on₂ {φ} (d₁ d₂ : many_one_degree) (f : (ℕ → Prop) → (ℕ → Prop) → φ)
     (h : ∀ p₁ p₂ q₁ q₂, many_one_equiv p₁ p₂ → many_one_equiv q₁ q₂ → f p₁ q₁ = f p₂ q₂) :
   φ :=
 d₁.lift_on (λ p, d₂.lift_on (f p) (λ q₁ q₂ hq, h _ _ _ _ (by refl) hq))
@@ -345,15 +345,15 @@ begin
 end
 
 @[simp]
-protected lemma lift_on₂_eq {φ} (p q : set ℕ) (f : set ℕ → set ℕ → φ)
+protected lemma lift_on₂_eq {φ} (p q : ℕ → Prop) (f : (ℕ → Prop) → (ℕ → Prop) → φ)
     (h : ∀ p₁ p₂ q₁ q₂, many_one_equiv p₁ p₂ → many_one_equiv q₁ q₂ → f p₁ q₁ = f p₂ q₂) :
   (of p).lift_on₂ (of q) f h = f p q :=
 rfl
 
 @[simp] lemma of_eq_of {p : α → Prop} {q : β → Prop} : of p = of q ↔ many_one_equiv p q :=
 by simp [of, quotient.eq']
 
-instance : inhabited many_one_degree := ⟨of (∅ : set ℕ)⟩
+instance : inhabited many_one_degree := ⟨of (λ n : ℕ, false)⟩
 
 /--
 For many-one degrees `d₁` and `d₂`, `d₁ ≤ d₂` if the sets in `d₁` are many-one reducible to the
@@ -406,7 +406,7 @@ instance : has_add many_one_degree :=
         (hr₂.trans one_one_reducible.disjoin_right.to_many_one)⟩
   end⟩
 
-@[simp] lemma add_of (p : set α) (q : set β) : of (p ⊕' q) = of p + of q :=
+@[simp] lemma add_of (p : α → Prop) (q : β → Prop) : of (p ⊕' q) = of p + of q :=
 of_eq_of.mpr
   ⟨disjoin_many_one_reducible
     (many_one_reducible_to_nat.trans one_one_reducible.disjoin_left.to_many_one)

src/computability/regular_expressions.lean

@@ -295,7 +295,7 @@ begin
       tauto } }
 end
 
-instance (P : regular_expression α) : decidable_pred P.matches :=
+instance matches.decidable_pred (P : regular_expression α) : decidable_pred (∈ P.matches) :=
 begin
   intro x,
   change decidable (x ∈ P.matches),

src/control/traversable/instances.lean

@@ -111,7 +111,7 @@ lemma mem_traverse {f : α' → set β'} :
 | []      (b::bs) := by simp
 | (a::as) (b::bs) :=
   suffices (b :: bs : list β') ∈ traverse f (a :: as) ↔ b ∈ f a ∧ bs ∈ traverse f as,
-    by simp [mem_traverse as bs],
+    by simp [mem_traverse as bs, (<*>)],
   iff.intro
     (assume ⟨_, ⟨b, hb, rfl⟩, _, hl, rfl⟩, ⟨hb, hl⟩)
     (assume ⟨hb, hl⟩, ⟨_, ⟨b, hb, rfl⟩, _, hl, rfl⟩)

src/data/equiv/basic.lean

@@ -1315,7 +1315,7 @@ subtype_equiv (equiv.refl α) (assume a, h ▸ iff.rfl)
 /-- The subtypes corresponding to equal sets are equivalent. -/
 @[simps apply]
 def set_congr {α : Type*} {s t : set α} (h : s = t) : s ≃ t :=
-subtype_equiv_prop h
+subtype_equiv (equiv.refl α) (by simp [h])
 
 /-- A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates. This
 version allows the “inner” predicate to depend on `h : p a`. -/
@@ -1697,7 +1697,7 @@ protected def compl {α : Type u} {β : Type v} {s : set α} {t : set β} [decid
 /-- The set product of two sets is equivalent to the type product of their coercions to types. -/
 protected def prod {α β} (s : set α) (t : set β) :
   s.prod t ≃ s × t :=
-@subtype_prod_equiv_prod α β s t
+@subtype_prod_equiv_prod α β (∈ s) (∈ t)
 
 /-- If a function `f` is injective on a set `s`, then `s` is equivalent to `f '' s`. -/
 protected noncomputable def image_of_inj_on {α β} (f : α → β) (s : set α) (H : inj_on f s) :
@@ -1729,7 +1729,7 @@ protected def congr {α β : Type*} (e : α ≃ β) : set α ≃ set β :=
 /-- The set `{x ∈ s | t x}` is equivalent to the set of `x : s` such that `t x`. -/
 protected def sep {α : Type u} (s : set α) (t : α → Prop) :
   ({ x ∈ s | t x } : set α) ≃ { x : s | t x } :=
-(equiv.subtype_subtype_equiv_subtype_inter s t).symm
+(equiv.subtype_subtype_equiv_subtype_inter _ _).symm
 
 /-- The set `𝒫 S := {x | x ⊆ S}` is equivalent to the type `set S`. -/
 protected def powerset {α} (S : set α) : 𝒫 S ≃ set S :=

src/data/equiv/encodable/basic.lean

@@ -142,7 +142,7 @@ theorem encodek₂ [encodable α] (a : α) : decode₂ α (encode a) = some a :=
 mem_decode₂.2 rfl
 
 /-- The encoding function has decidable range. -/
-def decidable_range_encode (α : Type*) [encodable α] : decidable_pred (set.range (@encode α _)) :=
+def decidable_range_encode (α : Type*) [encodable α] : decidable_pred (∈ set.range (@encode α _)) :=
 λ x, decidable_of_iff (option.is_some (decode₂ α x))
   ⟨λ h, ⟨option.get h, by rw [← decode₂_is_partial_inv (option.get h), option.some_get]⟩,
   λ ⟨n, hn⟩, by rw [← hn, encodek₂]; exact rfl⟩

src/data/equiv/local_equiv.lean

@@ -370,7 +370,7 @@ set.ext $ λ x, and.congr_right_iff.2 $ λ hx, by simp only [mem_preimage, e.lef
 
 lemma source_inter_preimage_target_inter (s : set β) :
   e.source ∩ (e ⁻¹' (e.target ∩ s)) = e.source ∩ (e ⁻¹' s) :=
-ext $ λ x, ⟨λ hx, ⟨hx.1, hx.2.2⟩, λ hx, ⟨hx.1, e.map_source hx.1, hx.2⟩⟩
+set.ext $ λ x, ⟨λ hx, ⟨hx.1, hx.2.2⟩, λ hx, ⟨hx.1, e.map_source hx.1, hx.2⟩⟩
 
 lemma target_inter_inv_preimage_preimage (s : set β) :
   e.target ∩ e.symm ⁻¹' (e ⁻¹' s) = e.target ∩ s :=