chore(*): fix errors in library and sanity_check

src/algebra/big_operators.lean

@@ -332,7 +332,7 @@ finset.strong_induction_on s
         prod_insert (not_mem_erase _ _), ih', mul_one, h₁ x hx])
 
 @[to_additive]
-lemma prod_eq_one [comm_monoid β] {f : α → β} {s : finset α} (h : ∀x∈s, f x = 1) : s.prod f = 1 :=
+lemma prod_eq_one {f : α → β} {s : finset α} (h : ∀x∈s, f x = 1) : s.prod f = 1 :=
 calc s.prod f = s.prod (λx, 1) : finset.prod_congr rfl h
   ... = 1 : finset.prod_const_one
 
@@ -540,12 +540,13 @@ by rwa sum_singleton at this
 end ordered_comm_monoid
 
 section canonically_ordered_monoid
-variables [decidable_eq α] [canonically_ordered_monoid β] [@decidable_rel β (≤)]
+variables [decidable_eq α] [canonically_ordered_monoid β]
 
 lemma sum_le_sum_of_subset (h : s₁ ⊆ s₂) : s₁.sum f ≤ s₂.sum f :=
 sum_le_sum_of_subset_of_nonneg h $ assume x h₁ h₂, zero_le _
 
-lemma sum_le_sum_of_ne_zero (h : ∀x∈s₁, f x ≠ 0 → x ∈ s₂) : s₁.sum f ≤ s₂.sum f :=
+lemma sum_le_sum_of_ne_zero [@decidable_rel β (≤)] (h : ∀x∈s₁, f x ≠ 0 → x ∈ s₂) :
+  s₁.sum f ≤ s₂.sum f :=
 calc s₁.sum f = (s₁.filter (λx, f x = 0)).sum f + (s₁.filter (λx, f x ≠ 0)).sum f :
     by rw [←sum_union, filter_union_filter_neg_eq];
        exact disjoint_filter (assume _ h n_h, n_h h)

src/algebra/order_functions.lean

@@ -187,7 +187,7 @@ variables [decidable_linear_ordered_comm_group α] {a b c : α}
 
 attribute [simp] abs_zero abs_neg
 
-def abs_add := @abs_add_le_abs_add_abs
+lemma abs_add (a b : α) : abs (a + b) ≤ abs a + abs b := abs_add_le_abs_add_abs a b
 
 theorem abs_le : abs a ≤ b ↔ - b ≤ a ∧ a ≤ b :=
 ⟨assume h, ⟨neg_le_of_neg_le $ le_trans (neg_le_abs_self _) h, le_trans (le_abs_self _) h⟩,
@@ -203,7 +203,7 @@ by rw [abs_le, neg_le_sub_iff_le_add, @sub_le_iff_le_add' _ _ b, and_comm]
 lemma abs_sub_lt_iff : abs (a - b) < c ↔ a - b < c ∧ b - a < c :=
 by rw [abs_lt, neg_lt_sub_iff_lt_add, @sub_lt_iff_lt_add' _ _ b, and_comm]
 
-def sub_abs_le_abs_sub := @abs_sub_abs_le_abs_sub
+lemma sub_abs_le_abs_sub (a b : α) : abs a - abs b ≤ abs (a - b) := abs_sub_abs_le_abs_sub a b
 
 lemma abs_abs_sub_le_abs_sub (a b : α) : abs (abs a - abs b) ≤ abs (a - b) :=
 abs_sub_le_iff.2 ⟨sub_abs_le_abs_sub _ _, by rw abs_sub; apply sub_abs_le_abs_sub⟩

src/analysis/complex/exponential.lean

@@ -590,12 +590,12 @@ begin
   norm_num, norm_num, apply pow_pos h
 end
 
-namespace angle
-
 /-- The type of angles -/
 def angle : Type :=
 quotient_add_group.quotient (gmultiples (2 * π))
 
+namespace angle
+
 instance angle.add_comm_group : add_comm_group angle :=
 quotient_add_group.add_comm_group _
 

src/category/functor.lean

@@ -5,7 +5,7 @@ Author: Simon Hudon
 
 Standard identity and composition functors
 -/
-import tactic.ext tactic.cache category.basic
+import tactic.ext tactic.sanity_check category.basic
 
 universe variables u v w
 
@@ -42,7 +42,7 @@ def id.mk {α : Sort u} : α → id α := id
 
 namespace functor
 
-def const (α : Type*) (β : Type*) := α
+@[sanity_skip] def const (α : Type*) (β : Type*) := α
 
 @[pattern] def const.mk {α β} (x : α) : const α β := x
 
@@ -54,7 +54,7 @@ namespace const
 
 protected lemma ext {α β} {x y : const α β} (h : x.run = y.run) : x = y := h
 
-protected def map {γ α β} (f : α → β) (x : const γ β) : const γ α := x
+@[sanity_skip] protected def map {γ α β} (f : α → β) (x : const γ β) : const γ α := x
 
 instance {γ} : functor (const γ) :=
 { map := @const.map γ }
@@ -106,6 +106,9 @@ instance : functor (comp F G) := { map := @comp.map F G _ _ }
 @[functor_norm] lemma map_mk {α β} (h : α → β) (x : F (G α)) :
   h <$> comp.mk x = comp.mk ((<$>) h <$> x) := rfl
 
+@[simp] protected lemma run_map {α β} (h : α → β) (x : comp F G α) :
+  (h <$> x).run = (<$>) h <$> x.run := rfl
+
 variables [is_lawful_functor F] [is_lawful_functor G]
 variables {α β γ : Type v}
 
@@ -116,9 +119,6 @@ protected lemma comp_map (g' : α → β) (h : β → γ) : ∀ (x : comp F G α
            comp.map (h ∘ g') x = comp.map h (comp.map g' x)
 | (comp.mk x) := by simp [comp.map, functor.map_comp_map g' h] with functor_norm
 
-@[simp] protected lemma run_map (h : α → β) (x : comp F G α) :
-  (h <$> x).run = (<$>) h <$> x.run := rfl
-
 instance : is_lawful_functor (comp F G) :=
 { id_map := @comp.id_map F G _ _ _ _,
   comp_map := @comp.comp_map F G _ _ _ _ }

src/category_theory/isomorphism.lean

@@ -197,7 +197,7 @@ is_iso.of_iso $ (as_iso f) ≪≫ (as_iso h)
 
 @[simp] lemma inv_id : inv (𝟙 X) = 𝟙 X := rfl
 @[simp] lemma inv_comp [is_iso f] [is_iso h] : inv (f ≫ h) = inv h ≫ inv f := rfl
-@[simp] lemma is_iso.inv_inv [is_iso f] : inv (inv f) = f := rfl
+@[simp] lemma inv_inv [is_iso f] : inv (inv f) = f := rfl
 @[simp] lemma iso.inv_inv (f : X ≅ Y) : inv (f.inv) = f.hom := rfl
 @[simp] lemma iso.inv_hom (f : X ≅ Y) : inv (f.hom) = f.inv := rfl
 

src/category_theory/limits/preserves.lean

@@ -84,6 +84,7 @@ by { split, intros, cases a, cases b, congr, funext J 𝒥, resetI, apply subsin
 instance preserves_colimits_subsingleton (F : C ⥤ D) : subsingleton (preserves_colimits F) :=
 by { split, intros, cases a, cases b, congr, funext J 𝒥, resetI, apply subsingleton.elim }
 
+omit 𝒟
 instance id_preserves_limits : preserves_limits (𝟭 C) :=
 { preserves_limits_of_shape := λ J 𝒥,
   { preserves_limit := λ K, by exactI ⟨λ c h,
@@ -97,6 +98,7 @@ instance id_preserves_colimits : preserves_colimits (𝟭 C) :=
   ⟨λ s, h.desc ⟨s.X, λ j, s.ι.app j, λ j j' f, s.ι.naturality f⟩,
    by cases K; rcases c with ⟨_, _, _⟩; intros s j; cases s; exact h.fac _ j,
    by cases K; rcases c with ⟨_, _, _⟩; intros s m w; rcases s with ⟨_, _, _⟩; exact h.uniq _ m w⟩⟩ } }
+include 𝒟
 
 section
 variables {E : Type u₃} [ℰ : category.{v} E]
@@ -179,6 +181,7 @@ instance reflects_colimits_of_shape_of_reflects_colimits (F : C ⥤ D)
   [H : reflects_colimits F] : reflects_colimits_of_shape J F :=
 reflects_colimits.reflects_colimits_of_shape F
 
+omit 𝒟
 instance id_reflects_limits : reflects_limits (𝟭 C) :=
 { reflects_limits_of_shape := λ J 𝒥,
   { reflects_limit := λ K, by exactI ⟨λ c h,
@@ -192,6 +195,7 @@ instance id_reflects_colimits : reflects_colimits (𝟭 C) :=
   ⟨λ s, h.desc ⟨s.X, λ j, s.ι.app j, λ j j' f, s.ι.naturality f⟩,
    by cases K; rcases c with ⟨_, _, _⟩; intros s j; cases s; exact h.fac _ j,
    by cases K; rcases c with ⟨_, _, _⟩; intros s m w; rcases s with ⟨_, _, _⟩; exact h.uniq _ m w⟩⟩ } }
+include 𝒟
 
 section
 variables {E : Type u₃} [ℰ : category.{v} E]

src/computability/turing_machine.lean

@@ -1359,7 +1359,7 @@ def st_write {k : K} (v : σ) (l : list (Γ k)) : st_act k → list (Γ k)
 | (pop ff f) := l
 | (pop tt f) := l.tail
 
-@[elab_as_eliminator] theorem {l} stmt_st_rec
+@[elab_as_eliminator] def {l} stmt_st_rec
   {C : stmt₂ → Sort l}
   (H₁ : Π k (s : st_act k) q (IH : C q), C (st_run s q))
   (H₂ : Π a q (IH : C q), C (TM2.stmt.load a q))

src/data/finset.lean

@@ -215,7 +215,7 @@ ne_empty_of_mem (mem_insert_self a s)
 theorem insert_subset {a : α} {s t : finset α} : insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t :=
 by simp only [subset_iff, mem_insert, forall_eq, or_imp_distrib, forall_and_distrib]
 
-theorem subset_insert [h : decidable_eq α] (a : α) (s : finset α) : s ⊆ insert a s :=
+theorem subset_insert (a : α) (s : finset α) : s ⊆ insert a s :=
 λ b, mem_insert_of_mem
 
 theorem insert_subset_insert (a : α) {s t : finset α} (h : s ⊆ t) : insert a s ⊆ insert a t :=
@@ -606,6 +606,9 @@ subset_empty.1 $ filter_subset _
 lemma filter_subset_filter {s t : finset α} (h : s ⊆ t) : s.filter p ⊆ t.filter p :=
 assume a ha, mem_filter.2 ⟨h (mem_filter.1 ha).1, (mem_filter.1 ha).2⟩
 
+@[simp] lemma coe_filter (s : finset α) : ↑(s.filter p) = ({x ∈ ↑s | p x} : set α) :=
+set.ext $ λ _, mem_filter
+
 variable [decidable_eq α]
 theorem filter_union (s₁ s₂ : finset α) :
   (s₁ ∪ s₂).filter p = s₁.filter p ∪ s₂.filter p :=
@@ -647,9 +650,6 @@ by simp only [filter_not, union_sdiff_of_subset (filter_subset s)]
 theorem filter_inter_filter_neg_eq (s : finset α) : s.filter p ∩ s.filter (λa, ¬ p a) = ∅ :=
 by simp only [filter_not, inter_sdiff_self]
 
-@[simp] lemma coe_filter (s : finset α) : ↑(s.filter p) = ({x ∈ ↑s | p x} : set α) :=
-set.ext $ λ _, mem_filter
-
 lemma subset_union_elim {s : finset α} {t₁ t₂ : set α} [decidable_pred (∈ t₁)] (h : ↑s ⊆ t₁ ∪ t₂) :
   ∃s₁ s₂ : finset α, s₁ ∪ s₂ = s ∧ ↑s₁ ⊆ t₁ ∧ ↑s₂ ⊆ t₂ \ t₁ :=
 begin
@@ -847,7 +847,7 @@ def map (f : α ↪ β) (s : finset α) : finset β :=
 
 @[simp] theorem map_val (f : α ↪ β) (s : finset α) : (map f s).1 = s.1.map f := rfl
 
-@[simp] theorem map_empty (f : α ↪ β) (s : finset α) : (∅ : finset α).map f = ∅ := rfl
+@[simp] theorem map_empty (f : α ↪ β) : (∅ : finset α).map f = ∅ := rfl
 
 variables {f : α ↪ β} {s : finset α}
 
@@ -968,7 +968,7 @@ ext.2 $ by simp only [mem_image, exists_prop, mem_inter]; exact λ b,
 ⟨λ ⟨a, ⟨m₁, m₂⟩, e⟩, ⟨⟨a, m₁, e⟩, ⟨a, m₂, e⟩⟩,
  λ ⟨⟨a, m₁, e₁⟩, ⟨a', m₂, e₂⟩⟩, ⟨a, ⟨m₁, hf _ _ (e₂.trans e₁.symm) ▸ m₂⟩, e₁⟩⟩.
 
-@[simp] theorem image_singleton [decidable_eq α] (f : α → β) (a : α) : (singleton a).image f = singleton (f a) :=
+@[simp] theorem image_singleton (f : α → β) (a : α) : (singleton a).image f = singleton (f a) :=
 ext.2 $ λ x, by simpa only [mem_image, exists_prop, mem_singleton, exists_eq_left] using eq_comm
 
 @[simp] theorem image_insert [decidable_eq α] (f : α → β) (a : α) (s : finset α) :
@@ -993,7 +993,7 @@ ext.2 $ λ ⟨x, hx⟩, ⟨or.cases_on (mem_insert.1 hx)
 theorem map_eq_image (f : α ↪ β) (s : finset α) : s.map f = s.image f :=
 eq_of_veq $ (multiset.erase_dup_eq_self.2 (s.map f).2).symm
 
-lemma image_const [decidable_eq β] {s : finset α} (h : s ≠ ∅) (b : β) : s.image (λa, b) = singleton b :=
+lemma image_const {s : finset α} (h : s ≠ ∅) (b : β) : s.image (λa, b) = singleton b :=
 ext.2 $ assume b', by simp only [mem_image, exists_prop, exists_and_distrib_right,
   exists_mem_of_ne_empty h, true_and, mem_singleton, eq_comm]
 
@@ -1005,7 +1005,7 @@ protected def subtype {α} (p : α → Prop) [decidable_pred p] (s : finset α)
   ∀{a : subtype p}, a ∈ s.subtype p ↔ a.val ∈ s
 | ⟨a, ha⟩ := by simp [finset.subtype, ha]
 
-lemma subset_image_iff [decidable_eq α] [decidable_eq β] {f : α → β}
+lemma subset_image_iff [decidable_eq α] {f : α → β}
   {s : finset β} {t : set α} : ↑s ⊆ f '' t ↔ ∃s' : finset α, ↑s' ⊆ t ∧ s'.image f = s :=
 begin
   split, swap,
@@ -1106,10 +1106,10 @@ multiset.card_le_of_le ∘ val_le_iff.mpr
 theorem eq_of_subset_of_card_le {s t : finset α} (h : s ⊆ t) (h₂ : card t ≤ card s) : s = t :=
 eq_of_veq $ multiset.eq_of_le_of_card_le (val_le_iff.mpr h) h₂
 
-lemma card_lt_card [decidable_eq α] {s t : finset α} (h : s ⊂ t) : s.card < t.card :=
+lemma card_lt_card {s t : finset α} (h : s ⊂ t) : s.card < t.card :=
 card_lt_of_lt (val_lt_iff.2 h)
 
-lemma card_le_card_of_inj_on [decidable_eq α] [decidable_eq β] {s : finset α} {t : finset β}
+lemma card_le_card_of_inj_on [decidable_eq β] {s : finset α} {t : finset β}
   (f : α → β) (hf : ∀a∈s, f a ∈ t) (f_inj : ∀a₁∈s, ∀a₂∈s, f a₁ = f a₂ → a₁ = a₂) :
   card s ≤ card t :=
 calc card s = card (s.image f) : by rw [card_image_of_inj_on f_inj]
@@ -1293,7 +1293,7 @@ def pi (s : finset α) (t : Πa, finset (δ a)) : finset (Πa∈s, δ a) :=
   f ∈ s.pi t ↔ (∀a (h : a ∈ s), f a h ∈ t a) :=
 mem_pi _ _ _
 
-def pi.empty (β : α → Sort*) [decidable_eq α] (a : α) (h : a ∈ (∅ : finset α)) : β a :=
+def pi.empty (β : α → Sort*) (a : α) (h : a ∈ (∅ : finset α)) : β a :=
 multiset.pi.empty β a h
 
 def pi.cons (s : finset α) (a : α) (b : δ a) (f : Πa, a ∈ s → δ a) (a' : α) (h : a' ∈ insert a s) : δ a' :=
@@ -1404,7 +1404,7 @@ by unfold fold; rw [insert_val, ndinsert_of_not_mem h, map_cons, fold_cons_left]
 
 @[simp] theorem fold_singleton : (singleton a).fold op b f = f a * b := rfl
 
-@[simp] theorem fold_map [decidable_eq α] {g : γ ↪ α} {s : finset γ} :
+@[simp] theorem fold_map {g : γ ↪ α} {s : finset γ} :
   (s.map g).fold op b f = s.fold op b (f ∘ g) :=
 by simp only [fold, map, multiset.map_map]
 

src/data/finsupp.lean

@@ -959,7 +959,7 @@ variables [add_monoid β] {v v' : α' →₀ β}
   (v + v').subtype_domain p = v.subtype_domain p + v'.subtype_domain p :=
 ext $ λ _, rfl
 
-instance subtype_domain.is_add_monoid_hom [add_monoid β] :
+instance subtype_domain.is_add_monoid_hom :
   is_add_monoid_hom (subtype_domain p : (α →₀ β) → subtype p →₀ β) :=
 { map_add := λ _ _, subtype_domain_add, map_zero := subtype_domain_zero }
 

src/data/fintype.lean

@@ -65,7 +65,7 @@ instance decidable_eq_equiv_fintype [fintype α] [decidable_eq β] :
 instance decidable_injective_fintype [fintype α] [decidable_eq α] [decidable_eq β] :
   decidable_pred (injective : (α → β) → Prop) := λ x, by unfold injective; apply_instance
 
-instance decidable_surjective_fintype [fintype α] [decidable_eq α] [fintype β] [decidable_eq β] :
+instance decidable_surjective_fintype [fintype α] [fintype β] [decidable_eq β] :
   decidable_pred (surjective : (α → β) → Prop) := λ x, by unfold surjective; apply_instance
 
 instance decidable_bijective_fintype [fintype α] [decidable_eq α] [fintype β] [decidable_eq β] :

src/data/list/basic.lean

@@ -5055,7 +5055,7 @@ by {apply get_pointwise, apply sub_zero}
 @length_pointwise α α α ⟨0⟩ ⟨0⟩ _ _ _
 
 @[simp] lemma nil_sub {α : Type} [add_group α]
-  (as : list α) : sub [] as = @neg α ⟨0⟩ _ as :=
+  (as : list α) : sub [] as = neg as :=
 begin
   rw [sub, nil_pointwise],
   congr, ext,

src/data/list/defs.lean

@@ -487,6 +487,8 @@ namespace func
 /- Definitions for using lists as finite
    representations of functions with domain ℕ. -/
 
+def neg [has_neg α] (as : list α) := as.map (λ a, -a)
+
 variables [inhabited α] [inhabited β]
 
 @[simp] def set (a : α) : list α → ℕ → list α
@@ -503,8 +505,6 @@ variables [inhabited α] [inhabited β]
 def equiv (as1 as2 : list α) : Prop :=
 ∀ (m : nat), get m as1 = get m as2
 
-def neg [has_neg α] (as : list α) := as.map (λ a, -a)
-
 @[simp] def pointwise (f : α → β → γ) : list α → list β → list γ
 | []      []      := []
 | []      (b::bs) := map (f $ default α) (b::bs)

src/data/opposite.lean

@@ -7,7 +7,6 @@ Opposites.
 -/
 import data.list.defs
 
-namespace opposite
 universes v u -- declare the `v` first; see `category_theory.category` for an explanation
 variable (α : Sort u)
 
@@ -39,8 +38,9 @@ def opposite : Sort u := α
 -- `presheaf Cᵒᵖ` parses as `presheaf (Cᵒᵖ)` and not `(presheaf C)ᵒᵖ`.
 notation α `ᵒᵖ`:std.prec.max_plus := opposite α
 
-variables {α}
+namespace opposite
 
+variables {α}
 def op : α → αᵒᵖ := id
 def unop : αᵒᵖ → α := id
 

src/data/rat/order.lean

@@ -125,18 +125,16 @@ instance : linear_order ℚ            := by apply_instance
 instance : partial_order ℚ           := by apply_instance
 instance : preorder ℚ                := by apply_instance
 
-protected lemma le_def' {p q : ℚ} (p_pos : 0 < p) (q_pos : 0 < q) :
-  p ≤ q ↔ p.num * q.denom ≤ q.num * p.denom :=
+protected lemma le_def' {p q : ℚ} : p ≤ q ↔ p.num * q.denom ≤ q.num * p.denom :=
 begin
   rw [←(@num_denom q), ←(@num_denom p)],
   conv_rhs { simp only [num_denom] },
   exact rat.le_def (by exact_mod_cast p.pos) (by exact_mod_cast q.pos)
 end
 
-protected lemma lt_def {p q : ℚ} (p_pos : 0 < p) (q_pos : 0 < q) :
-  p < q ↔ p.num * q.denom < q.num * p.denom :=
+protected lemma lt_def {p q : ℚ} : p < q ↔ p.num * q.denom < q.num * p.denom :=
 begin
-  rw [lt_iff_le_and_ne, (rat.le_def' p_pos q_pos)],
+  rw [lt_iff_le_and_ne, rat.le_def'],
   suffices : p ≠ q ↔ p.num * q.denom ≠ q.num * p.denom, by {
     split; intro h,
     { exact lt_iff_le_and_ne.elim_right ⟨h.left, (this.elim_left h.right)⟩ },
@@ -200,7 +198,7 @@ end
 lemma lt_one_iff_num_lt_denom {q : ℚ} : q < 1 ↔ q.num < q.denom :=
 begin
   cases decidable.em (0 < q) with q_pos q_nonpos,
-  { simp [(rat.lt_def q_pos zero_lt_one)] },
+  { simp [rat.lt_def] },
   { replace q_nonpos : q ≤ 0, from not_lt.elim_left q_nonpos,
     have : q.num < q.denom, by
     { have : ¬0 < q.num ↔ ¬0 < q, from not_iff_not.elim_right num_pos_iff_pos,

src/data/seq/computation.lean

@@ -167,7 +167,7 @@ def rmap (f : β → γ) : α ⊕ β → α ⊕ γ
 | (sum.inr b) := sum.inr (f b)
 attribute [simp] lmap rmap
 
-@[simp] def corec_eq (f : β → α ⊕ β) (b : β) :
+@[simp] lemma corec_eq (f : β → α ⊕ β) (b : β) :
   destruct (corec f b) = rmap (corec f) (f b) :=
 begin
   dsimp [corec, destruct],
@@ -903,7 +903,7 @@ def lift_rel_aux (R : α → β → Prop)
 | (sum.inr ca) (sum.inr cb) := C ca cb
 attribute [simp] lift_rel_aux
 
-@[simp] def lift_rel_aux.ret_left (R : α → β → Prop)
+@[simp] lemma lift_rel_aux.ret_left (R : α → β → Prop)
   (C : computation α → computation β → Prop) (a cb) :
   lift_rel_aux R C (sum.inl a) (destruct cb) ↔ ∃ {b}, b ∈ cb ∧ R a b :=
 begin
@@ -919,7 +919,7 @@ theorem lift_rel_aux.swap (R : α → β → Prop) (C) (a b) :
   lift_rel_aux (function.swap R) (function.swap C) b a = lift_rel_aux R C a b :=
 by cases a with a ca; cases b with b cb; simp only [lift_rel_aux]
 
-@[simp] def lift_rel_aux.ret_right (R : α → β → Prop)
+@[simp] lemma lift_rel_aux.ret_right (R : α → β → Prop)
   (C : computation α → computation β → Prop) (b ca) :
   lift_rel_aux R C (destruct ca) (sum.inl b) ↔ ∃ {a}, a ∈ ca ∧ R a b :=
 by rw [←lift_rel_aux.swap, lift_rel_aux.ret_left]

src/data/set/finite.lean

@@ -213,7 +213,7 @@ instance fintype_map {α β} [decidable_eq β] :
 theorem finite_map {α β} {s : set α} :
   ∀ (f : α → β), finite s → finite (f <$> s) := finite_image
 
-def fintype_of_fintype_image [decidable_eq β] (s : set α)
+def fintype_of_fintype_image (s : set α)
   {f : α → β} {g} (I : is_partial_inv f g) [fintype (f '' s)] : fintype s :=
 fintype_of_finset ⟨_, @multiset.nodup_filter_map β α g _
   (@injective_of_partial_inv_right _ _ f g I) (f '' s).to_finset.2⟩ $ λ a,
@@ -352,7 +352,7 @@ 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' [decidable_eq α] (s : set α) [fintype s] : (↑s.to_finset : set α) = s :=
+@[simp] lemma coe_to_finset' (s : set α) [fintype s] : (↑s.to_finset : set α) = s :=
 by ext; simp
 
 end finset

src/data/set/function.lean

@@ -243,7 +243,7 @@ calc
 @[reducible] def right_inv_on (g : β → α) (f : α → β) (b : set β) : Prop :=
 left_inv_on f g b
 
-theorem right_inv_on_of_eq_on_left {g1 g2 : β → α} {f : α → β} {a : set α} {b : set β}
+theorem right_inv_on_of_eq_on_left {g1 g2 : β → α} {f : α → β} {b : set β}
   (h₁ : eq_on g1 g2 b) (h₂ : right_inv_on g1 f b) : right_inv_on g2 f b :=
 left_inv_on_of_eq_on_right h₁ h₂