diff --git a/src/category_theory/preadditive/projective.lean b/src/category_theory/preadditive/projective.lean
index 89e532ada0046..4745c47d719a1 100644
--- a/src/category_theory/preadditive/projective.lean
+++ b/src/category_theory/preadditive/projective.lean
@@ -96,7 +96,7 @@ instance (X : Type u) : projective X :=
   ⟨λ x, ((epi_iff_surjective _).mp epi (f x)).some,
   by { ext x, exact ((epi_iff_surjective _).mp epi (f x)).some_spec, }⟩ }
 
-instance Type_enough_projectives : enough_projectives (Type u) :=
+instance Type.enough_projectives : enough_projectives (Type u) :=
 { presentation := λ X, ⟨{ P := X, f := 𝟙 X, }⟩, }
 
 instance {P Q : C} [has_binary_coproduct P Q] [projective P] [projective Q] :
diff --git a/src/order/boolean_algebra.lean b/src/order/boolean_algebra.lean
index b114b4e5f7bb3..b112479c29f03 100644
--- a/src/order/boolean_algebra.lean
+++ b/src/order/boolean_algebra.lean
@@ -32,7 +32,7 @@ intervals.)
 * `boolean_algebra`: the main type class for Boolean algebras; it extends both
   `generalized_boolean_algebra` and `boolean_algebra.core`. An instance of `boolean_algebra` can be
   obtained from one of `boolean_algebra.core` using `boolean_algebra.of_core`.
-* `boolean_algebra_Prop`: the Boolean algebra instance on `Prop`
+* `Prop.boolean_algebra`: the Boolean algebra instance on `Prop`
 
 ## Implementation notes
 
@@ -679,12 +679,12 @@ theorem top_sdiff : ⊤ \ x = xᶜ := by rw [sdiff_eq, top_inf_eq]
 
 end boolean_algebra
 
-instance boolean_algebra_Prop : boolean_algebra Prop :=
+instance Prop.boolean_algebra : boolean_algebra Prop :=
 boolean_algebra.of_core
 { compl := not,
   inf_compl_le_bot := λ p ⟨Hp, Hpc⟩, Hpc Hp,
   top_le_sup_compl := λ p H, classical.em p,
-  .. bounded_distrib_lattice_Prop }
+  .. Prop.bounded_distrib_lattice }
 
 instance pi.boolean_algebra {ι : Type u} {α : ι → Type v} [∀ i, boolean_algebra (α i)] :
   boolean_algebra (Π i, α i) :=
diff --git a/src/order/bounded_lattice.lean b/src/order/bounded_lattice.lean
index f09571caab4a0..7c943f3308059 100644
--- a/src/order/bounded_lattice.lean
+++ b/src/order/bounded_lattice.lean
@@ -295,7 +295,7 @@ lemma inf_eq_bot_iff_le_compl {α : Type u} [bounded_distrib_lattice α] {a b c
       ... = ⊥ : h₂⟩
 
 /-- Propositions form a bounded distributive lattice. -/
-instance bounded_distrib_lattice_Prop : bounded_distrib_lattice Prop :=
+instance Prop.bounded_distrib_lattice : bounded_distrib_lattice Prop :=
 { le           := λ a b, a → b,
   le_refl      := λ _, id,
   le_trans     := λ a b c f g, g ∘ f,
diff --git a/src/order/complete_boolean_algebra.lean b/src/order/complete_boolean_algebra.lean
index ee0945a23edc8..f57bcd8473ed8 100644
--- a/src/order/complete_boolean_algebra.lean
+++ b/src/order/complete_boolean_algebra.lean
@@ -110,12 +110,12 @@ instance pi.complete_boolean_algebra {ι : Type*} {π : ι → Type*}
   [∀ i, complete_boolean_algebra (π i)] : complete_boolean_algebra (Π i, π i) :=
 { .. pi.boolean_algebra, .. pi.complete_distrib_lattice }
 
-instance : complete_boolean_algebra Prop :=
+instance Prop.complete_boolean_algebra : complete_boolean_algebra Prop :=
 { infi_sup_le_sup_Inf := λ p s, iff.mp $
     by simp only [forall_or_distrib_left, complete_lattice.Inf, infi_Prop_eq, sup_Prop_eq],
   inf_Sup_le_supr_inf := λ p s, iff.mp $
     by simp only [complete_lattice.Sup, exists_and_distrib_left, inf_Prop_eq, supr_Prop_eq],
-  .. boolean_algebra_Prop, .. complete_lattice_Prop }
+  .. Prop.boolean_algebra, .. Prop.complete_lattice }
 
 section complete_boolean_algebra
 variables [complete_boolean_algebra α] {a b : α} {s : set α} {f : ι → α}
diff --git a/src/order/complete_lattice.lean b/src/order/complete_lattice.lean
index 97aeb7ec0a527..c3c8c685bdfc6 100644
--- a/src/order/complete_lattice.lean
+++ b/src/order/complete_lattice.lean
@@ -1077,14 +1077,14 @@ end complete_linear_order
 ### Instances
 -/
 
-instance complete_lattice_Prop : complete_lattice Prop :=
+instance Prop.complete_lattice : complete_lattice Prop :=
 { Sup    := λs, ∃a∈s, a,
   le_Sup := assume s a h p, ⟨a, h, p⟩,
   Sup_le := assume s a h ⟨b, h', p⟩, h b h' p,
   Inf    := λs, ∀a:Prop, a∈s → a,
   Inf_le := assume s a h p, p a h,
   le_Inf := assume s a h p b hb, h b hb p,
-  .. bounded_distrib_lattice_Prop }
+  .. Prop.bounded_distrib_lattice }
 
 @[simp] lemma Inf_Prop_eq {s : set Prop} : Inf s = (∀p ∈ s, p) := rfl
 
diff --git a/src/tactic/has_variable_names.lean b/src/tactic/has_variable_names.lean
index 19ada9a64fd9a..6506401847408 100644
--- a/src/tactic/has_variable_names.lean
+++ b/src/tactic/has_variable_names.lean
@@ -109,7 +109,7 @@ make_listlike_instance α
 instance : has_variable_names ℕ :=
 ⟨[`n, `m, `o]⟩
 
-instance : has_variable_names Prop :=
+instance Prop.has_variable_names : has_variable_names Prop :=
 ⟨[`P, `Q, `R]⟩
 
 instance {α} [has_variable_names α] : has_variable_names (thunk α) :=
diff --git a/src/testing/slim_check/sampleable.lean b/src/testing/slim_check/sampleable.lean
index eafc046d9f077..37820c1ee84a8 100644
--- a/src/testing/slim_check/sampleable.lean
+++ b/src/testing/slim_check/sampleable.lean
@@ -514,7 +514,7 @@ instance list.sampleable : sampleable_functor list.{u} :=
   shrink := λ α Iα shr_α, @list.shrink_with _ Iα shr_α,
   p_repr := @list.has_repr }
 
-instance prop.sampleable_ext : sampleable_ext Prop :=
+instance Prop.sampleable_ext : sampleable_ext Prop :=
 { proxy_repr := bool,
   interp := coe,
   sample := choose_any bool,