diff --git a/leanpkg.toml b/leanpkg.toml
index 59bd47d3f11b3..00d583fee9084 100644
--- a/leanpkg.toml
+++ b/leanpkg.toml
@@ -1,7 +1,7 @@
 [package]
 name = "mathlib"
 version = "0.1"
-lean_version = "leanprover-community/lean:3.26.0"
+lean_version = "leanprover-community/lean:3.27.0"
 path = "src"
 
 [dependencies]
diff --git a/src/algebraic_geometry/presheafed_space.lean b/src/algebraic_geometry/presheafed_space.lean
index 3a776364d959e..0e8e4cf2996db 100644
--- a/src/algebraic_geometry/presheafed_space.lean
+++ b/src/algebraic_geometry/presheafed_space.lean
@@ -225,9 +225,8 @@ def restrict_top_iso (X : PresheafedSpace C) :
     dsimp only [nat_trans.comp_app, comp_c_app, of_restrict, to_restrict_top,
         whisker_right_app, comp_base, nat_trans.op_app, opens.map_iso_inv_app],
     erw [← X.presheaf.map_comp, ← X.presheaf.map_comp, ← X.presheaf.map_comp, id_c_app],
-    convert eq_to_hom_map X.presheaf _, swap,
-    { erw [op_obj, id_base, opens.map_id_obj], refl },
-    { refine has_hom.hom.unop_inj _, exact subsingleton.elim _ _ } } }
+    convert eq_to_hom_map X.presheaf _,
+    erw [op_obj, id_base, opens.map_id_obj], refl } }
 
 /--
 The global sections, notated Gamma.
diff --git a/src/category_theory/opposites.lean b/src/category_theory/opposites.lean
index 4ea5634cb0da5..9fc088e1d9fed 100644
--- a/src/category_theory/opposites.lean
+++ b/src/category_theory/opposites.lean
@@ -406,6 +406,12 @@ rfl
 lemma op_equiv_symm_apply (A B : Cᵒᵖ) (f : B.unop ⟶ A.unop) : (op_equiv _ _).symm f = f.op :=
 rfl
 
+instance subsingleton_of_unop (A B : Cᵒᵖ) [subsingleton (unop B ⟶ unop A)] : subsingleton (A ⟶ B) :=
+(op_equiv A B).subsingleton
+
+instance decidable_eq_of_unop (A B : Cᵒᵖ) [decidable_eq (unop B ⟶ unop A)] : decidable_eq (A ⟶ B) :=
+(op_equiv A B).decidable_eq
+
 universes v
 variables {α : Type v} [preorder α]
 
diff --git a/src/computability/language.lean b/src/computability/language.lean
index 7ca703ebd66f6..0357b29e888ea 100644
--- a/src/computability/language.lean
+++ b/src/computability/language.lean
@@ -204,11 +204,11 @@ begin
     { use 0,
       tauto },
     { specialize ih _,
+      { exact λ y hy, hS _ (list.mem_cons_of_mem _ hy) },
       { cases ih with i ih,
         use i.succ,
         rw [pow_succ, mem_mul],
-        exact ⟨ x, S.join, hS x (list.mem_cons_self _ _), ih, rfl ⟩ },
-      { exact λ y hy, hS _ (list.mem_cons_of_mem _ hy) } } },
+        exact ⟨ x, S.join, hS x (list.mem_cons_self _ _), ih, rfl ⟩ } } },
   { rintro ⟨ i, hx ⟩,
     induction i with i ih generalizing x,
     { rw [pow_zero, mem_one] at hx,
diff --git a/src/computability/regular_expressions.lean b/src/computability/regular_expressions.lean
index 4daaf5c340c56..6ab513e54ec3e 100644
--- a/src/computability/regular_expressions.lean
+++ b/src/computability/regular_expressions.lean
@@ -228,9 +228,9 @@ begin
         { finish },
         refine ⟨ t, U.join, by finish, _, _ ⟩,
         { specialize helem (b :: t) _,
+          { finish },
           rw rmatch at helem,
           convert helem.2,
-          finish,
           finish },
         { have hwf : U.join.length < (list.cons a x).length,
           { rw hsum,
diff --git a/src/computability/tm_computable.lean b/src/computability/tm_computable.lean
index a499db7266238..4154e47fe9d9d 100644
--- a/src/computability/tm_computable.lean
+++ b/src/computability/tm_computable.lean
@@ -74,7 +74,7 @@ end fin_tm2
 def init_list (tm : fin_tm2) (s : list (tm.Γ tm.k₀)) : tm.cfg :=
 { l := option.some tm.main,
   var := tm.initial_state,
-  stk := λ k, @dite (k = tm.k₀) (tm.K_decidable_eq k tm.k₀) (list (tm.Γ k))
+  stk := λ k, @dite (list (tm.Γ k)) (k = tm.k₀) (tm.K_decidable_eq k tm.k₀)
                 (λ h, begin rw h, exact s, end)
                 (λ _,[]) }
 
@@ -82,7 +82,7 @@ def init_list (tm : fin_tm2) (s : list (tm.Γ tm.k₀)) : tm.cfg :=
 def halt_list (tm : fin_tm2) (s : list (tm.Γ tm.k₁)) : tm.cfg :=
 { l := option.none,
   var := tm.initial_state,
-  stk := λ k, @dite (k = tm.k₁) (tm.K_decidable_eq k tm.k₁) (list (tm.Γ k))
+  stk := λ k, @dite (list (tm.Γ k)) (k = tm.k₁) (tm.K_decidable_eq k tm.k₁)
                 (λ h, begin rw h, exact s, end)
                 (λ _,[]) }
 
diff --git a/src/data/polynomial/degree/definitions.lean b/src/data/polynomial/degree/definitions.lean
index 09ff129a61efc..c515c4029814e 100644
--- a/src/data/polynomial/degree/definitions.lean
+++ b/src/data/polynomial/degree/definitions.lean
@@ -215,7 +215,7 @@ coeff_eq_zero_of_nat_degree_lt (lt_add_one _)
 
 -- We need the explicit `decidable` argument here because an exotic one shows up in a moment!
 lemma ite_le_nat_degree_coeff (p : polynomial R) (n : ℕ) (I : decidable (n < 1 + nat_degree p)) :
-  @ite (n < 1 + nat_degree p) I _ (coeff p n) 0 = coeff p n :=
+  @ite _ (n < 1 + nat_degree p) I (coeff p n) 0 = coeff p n :=
 begin
   split_ifs,
   { refl },
diff --git a/src/linear_algebra/dual.lean b/src/linear_algebra/dual.lean
index 54f2503b534e4..4480ef4ae5912 100644
--- a/src/linear_algebra/dual.lean
+++ b/src/linear_algebra/dual.lean
@@ -234,7 +234,7 @@ h.to_dual_apply_right i v
   (h.dual_basis_is_basis.to_dual _).comp (h.to_dual B) = eval K V :=
 begin
   refine h.ext (λ i, h.dual_basis_is_basis.ext (λ j, _)),
-  suffices : @ite _ (classical.prop_decidable _) K 1 0 = @ite _ (de j i) K 1 0,
+  suffices : @ite K _ (classical.prop_decidable _) 1 0 = @ite K _ (de j i) 1 0,
     by simpa [h.dual_basis_is_basis.to_dual_apply_left, h.dual_basis_repr, h.to_dual_apply_right],
   split_ifs; refl
 end
diff --git a/src/tactic/split_ifs.lean b/src/tactic/split_ifs.lean
index 4fd9a0addecdc..97efa1f8f06d4 100644
--- a/src/tactic/split_ifs.lean
+++ b/src/tactic/split_ifs.lean
@@ -15,8 +15,8 @@ open interactive
 meta def find_if_cond : expr → option expr | e :=
 e.fold none $ λ e _ acc, acc <|> do
 c ← match e with
-| `(@ite %%c %%_ _ _ _) := some c
-| `(@dite %%c %%_ _ _ _) := some c
+| `(@ite _ %%c %%_ _ _) := some c
+| `(@dite _ %%c %%_ _ _) := some c
 | _ := none
 end,
 guard ¬c.has_var,
diff --git a/src/tactic/unfold_cases.lean b/src/tactic/unfold_cases.lean
index 25e34d3ccebd4..4693a943bada6 100644
--- a/src/tactic/unfold_cases.lean
+++ b/src/tactic/unfold_cases.lean
@@ -95,7 +95,7 @@ namespace unfold_cases
   (e.g. `whnf` or `dsimp`).
 -/
 meta def find_splitting_expr : expr → tactic expr
-| `(@ite %%cond %%dec_inst _ _ _ = _) := pure `(@decidable.em %%cond %%dec_inst)
+| `(@ite _ %%cond %%dec_inst _ _ = _) := pure `(@decidable.em %%cond %%dec_inst)
 | `(%%(app x y) = _) := pure y
 | e := fail!"expected an expression of the form: f x = y. Got:\n{e}"
 
diff --git a/src/topology/locally_constant/basic.lean b/src/topology/locally_constant/basic.lean
index 73effc734a241..fecf679e4c45b 100644
--- a/src/topology/locally_constant/basic.lean
+++ b/src/topology/locally_constant/basic.lean
@@ -127,8 +127,8 @@ begin
   suffices : x ∉ Uᶜ, from not_not.1 this,
   intro hxV,
   specialize hs U Uᶜ (hf {f y}) (hf {f y}ᶜ) _ ⟨y, ⟨hy, rfl⟩⟩ ⟨x, ⟨hx, hxV⟩⟩,
-  { simpa only [inter_empty, not_nonempty_empty, inter_compl_self] using hs },
-  { simp only [union_compl_self, subset_univ] }
+  { simp only [union_compl_self, subset_univ] },
+  { simpa only [inter_empty, not_nonempty_empty, inter_compl_self] using hs }
 end
 
 lemma iff_is_const [preconnected_space X] {f : X → Y} :
diff --git a/src/topology/omega_complete_partial_order.lean b/src/topology/omega_complete_partial_order.lean
index 971b4e486f92a..459c12e0598f3 100644
--- a/src/topology/omega_complete_partial_order.lean
+++ b/src/topology/omega_complete_partial_order.lean
@@ -68,10 +68,10 @@ begin
   dsimp [is_open] at *,
   apply complete_lattice.Sup_continuous' _,
   introv ht, specialize h₀ { x | t x } _,
-  { simpa using h₀ },
   { simp only [flip, set.mem_image] at *,
     rcases ht with ⟨x,h₀,h₁⟩, subst h₁,
-    simpa, }
+    simpa, },
+  { simpa using h₀ }
 end
 
 end Scott
diff --git a/test/qpf.lean b/test/qpf.lean
index 3a5e5ff42bd16..b015723e205d6 100644
--- a/test/qpf.lean
+++ b/test/qpf.lean
@@ -175,14 +175,15 @@ end
 lemma supp_mk_tt' {α} (x : α) : qpf.supp' (foo.mk tt x) = {x} :=
 begin
   dsimp [qpf.supp'], ext, simp, dsimp [qpf.box], split; intro h,
-  { specialize h {x} _, { simp at h, assumption },
-    clear h, introv hfg, simp, rw hfg, simp },
+  { specialize h {x} _,
+    { clear h, introv hfg, simp, rw hfg, simp },
+    { simp at h, assumption }, },
   { introv hfg, subst x_1, classical,
     let f : α → α ⊕ bool := λ x, if x ∈ i then sum.inl x else sum.inr tt,
     let g : α → α ⊕ bool := λ x, if x ∈ i then sum.inl x else sum.inr ff,
     specialize hfg _ f g _,
+    { intros, simp [*,f,g,if_pos] },
     { simp [f,g] at hfg, split_ifs at hfg,
-      assumption, cases hfg },
-    { intros, simp [*,f,g,if_pos] } }
+      assumption, cases hfg } }
 end
 end ex