diff --git a/library/theories/group_theory/action.lean b/library/theories/group_theory/action.lean
index 2a3631f0a..6a0810b89 100644
--- a/library/theories/group_theory/action.lean
+++ b/library/theories/group_theory/action.lean
@@ -431,7 +431,7 @@ subset_of_forall take g, begin
   apply finsubg_has_inv,
   apply mem_sep_of_mem !mem_univ,
   intro h Ph,
-  have Phg : fin_lcoset (fin_lcoset H g) h = fin_lcoset H g, exact PH Ph,
+  have Phg : fin_lcoset (fin_lcoset H g) h = fin_lcoset H g, from PH Ph,
   revert Phg,
   rewrite [↑conj_by, inv_inv, mul.assoc, fin_lcoset_compose, -fin_lcoset_same, ↑fin_lcoset, mem_image_iff, ↑lmul_by],
   intro Pex, cases Pex with k Pand, cases Pand with Pkin Pk,
@@ -494,9 +494,8 @@ lemma lift_lower_eq : ∀ {p : perm (fin (succ n))} (P : p maxi = maxi),
 | (perm.mk pf Pinj) := assume Pmax, begin
   rewrite [↑lift_perm], congruence,
   apply funext, intro i,
-  have Pfmax : pf maxi = maxi, apply Pmax,
-  have Pd : decidable (i = maxi),
-    exact _,
+  have Pfmax : pf maxi = maxi, by apply Pmax,
+  have Pd : decidable (i = maxi), from _,
     cases Pd with Pe Pne,
       rewrite [Pe, Pfmax], apply lift_fun_max,
       rewrite [lift_fun_of_ne_max Pne, ↑lower_perm, ↑lift_succ],
diff --git a/library/theories/group_theory/cyclic.lean b/library/theories/group_theory/cyclic.lean
index d0bb37a80..d1ee1a693 100644
--- a/library/theories/group_theory/cyclic.lean
+++ b/library/theories/group_theory/cyclic.lean
@@ -194,9 +194,11 @@ lemma order_of_min_pow {a : A} {n : nat}
 or.elim (eq_or_lt_of_le (order_le Pone)) (λ P, P)
   (λ P : order a < succ n, begin
   have Pn : a^(order a) ≠ 1,
+  begin
     rewrite [-(succ_pred_of_pos (order_pos a))],
     apply Pmin, apply nat.lt_of_succ_lt_succ,
-    rewrite [succ_pred_of_pos !order_pos], assumption,
+    rewrite [succ_pred_of_pos !order_pos], assumption
+  end,
   exact absurd (pow_order a) Pn end)
 
 lemma order_dvd_of_pow_eq_one {a : A} {n : nat} (Pone : a^n = 1) : order a ∣ n :=
@@ -243,7 +245,7 @@ local attribute group_of_add_group [instance]
 lemma pow_eq_mul {n : nat} {i : fin (succ n)} : ∀ {k : nat}, i^k = mk_mod n (i*k)
 | 0        := by rewrite [pow_zero]
 | (succ k) := begin
-  have Psucc : i^(succ k) = madd (i^k) i, apply pow_succ',
+  have Psucc : i^(succ k) = madd (i^k) i, by apply pow_succ',
   rewrite [Psucc, pow_eq_mul],
   apply eq_of_veq,
   rewrite [mul_succ, val_madd, ↑mk_mod, mod_add_mod]