diff --git a/algebra/graded.hlean b/algebra/graded.hlean
index ee6c7bd..42f9361 100644
--- a/algebra/graded.hlean
+++ b/algebra/graded.hlean
@@ -414,10 +414,10 @@ end
 
 definition dirsum : LeftModule R :=
 LeftModule_of_AddAbGroup (dirsum' N) (λr n, dirsum_smul r n)
-  (λr, homomorphism.addstruct (dirsum_smul r))
-  dirsum_smul_right_distrib
-  dirsum_mul_smul
-  dirsum_one_smul
+  proof (λr, homomorphism.addstruct (dirsum_smul r)) qed
+  proof dirsum_smul_right_distrib qed
+  proof dirsum_mul_smul qed
+  proof dirsum_one_smul qed
 
 /- graded variants of left-module constructions -/
 
diff --git a/algebra/seq_colim.hlean b/algebra/seq_colim.hlean
index b184bda..2de1070 100644
--- a/algebra/seq_colim.hlean
+++ b/algebra/seq_colim.hlean
@@ -47,16 +47,15 @@ namespace group
       end
 
     definition seq_colim_glue {i : @trunctype.mk 0 ℕ _} {a : A i} : seq_colim_incl i a = seq_colim_incl (succ i) (f i a) :=
-   begin
-     refine !homomorphism_comp_compute ⬝ _,
-     refine gqg_eq_of_rel _ _ ⬝ (!homomorphism_comp_compute)⁻¹,
-     exact tr (seq_colim_rel.rmk _ _)
-   end
+    begin
+      refine gqg_eq_of_rel _ _,
+      exact tr (seq_colim_rel.rmk _ _)
+    end
 
     section
       local abbreviation h (m : seq_colim →g A') : Πi, A i →g A' := λi, m ∘g (seq_colim_incl i)
       local abbreviation k (m : seq_colim →g A') : Πi a, h m i a = h m (succ i) (f i a) :=
-        λ i a, !homomorphism_comp_compute ⬝ ap m (@seq_colim_glue i a) ⬝ !homomorphism_comp_compute⁻¹
+      λ i a, ap m (@seq_colim_glue i a)
 
       definition seq_colim_unique (m : seq_colim →g A') :
         Πv, seq_colim_elim (h m) (k m) v = m v :=
@@ -77,7 +76,6 @@ namespace group
   seq_colim_elim (λi, seq_colim_incl i ∘g h i)
     begin
       intro i a,
-      refine !homomorphism_comp_compute ⬝ _ ⬝ !homomorphism_comp_compute⁻¹,
       refine _ ⬝ ap (seq_colim_incl (succ i)) (p i a)⁻¹,
       apply seq_colim_glue
     end
diff --git a/algebra/submodule.hlean b/algebra/submodule.hlean
index 301c1e1..67e6ad3 100644
--- a/algebra/submodule.hlean
+++ b/algebra/submodule.hlean
@@ -277,12 +277,13 @@ begin
 end
 
 variables {ψ : M₂ →lm M₃} {φ : M₁ →lm M₂} {θ : M₁ →lm M₃}
+
 definition image_elim [constructor] (θ : M₁ →lm M₃) (h : Π⦃g⦄, φ g = 0 → θ g = 0) :
   image_module φ →lm M₃ :=
 begin
   refine homomorphism.mk (image_elim (group_homomorphism_of_lm_homomorphism θ) h) _,
   split,
-  { apply homomorphism.addstruct },
+  { exact homomorphism.struct (image_elim (group_homomorphism_of_lm_homomorphism θ) _) },
   { intro r, refine @total_image.rec _ _ _ _ (λx, !is_trunc_eq) _, intro g,
     apply to_respect_smul }
 end