diff --git a/algebra/graded.hlean b/algebra/graded.hlean
index df16627..1369b5c 100644
--- a/algebra/graded.hlean
+++ b/algebra/graded.hlean
@@ -4,7 +4,41 @@
 
 import .left_module .direct_sum .submodule --..heq
 
-open algebra eq left_module pointed function equiv is_equiv is_trunc prod group sigma
+open is_trunc algebra eq left_module pointed function equiv is_equiv prod group sigma nat
+
+-- move
+  lemma le_sub_of_add_le {n m k : ℕ} (h : n + m ≤ k) : n ≤ k - m :=
+  begin
+    induction h with k h IH,
+    { exact le_of_eq !nat.add_sub_cancel⁻¹ },
+    { exact le.trans IH (nat.sub_le_sub_right !self_le_succ _) }
+  end
+
+  lemma iterate_sub {A : Type} (f : A ≃ A) {n m : ℕ} (h : n ≥ m) (a : A) :
+    iterate f (n - m) a = iterate f n (iterate f⁻¹ m a) :=
+  begin
+    revert n h, induction m with m p: intro n h,
+    { reflexivity },
+    { cases n with n, exfalso, apply not_succ_le_zero _ h,
+      rewrite [succ_sub_succ], refine p n (le_of_succ_le_succ h) ⬝ _,
+      refine ap (_^[n]) _ ⬝ !iterate_succ⁻¹, exact !to_right_inv⁻¹ }
+  end
+
+  definition iterate_commute {A : Type} {f g : A → A} (n : ℕ) (h : f ∘ g ~ g ∘ f) :
+    iterate f n ∘ g ~ g ∘ iterate f n :=
+  by induction n with n IH; reflexivity; exact λx, ap f (IH x) ⬝ !h
+
+  definition iterate_equiv {A : Type} (f : A ≃ A) (n : ℕ) : A ≃ A :=
+  equiv.mk (iterate f n)
+           (by induction n with n IH; apply is_equiv_id; exact is_equiv_compose f (iterate f n))
+
+  definition iterate_inv {A : Type} (f : A ≃ A) (n : ℕ) :
+    (iterate_equiv f n)⁻¹ ~ iterate f⁻¹ n :=
+  begin
+    induction n with n p: intro a,
+      reflexivity,
+      exact p (f⁻¹ a) ⬝ !iterate_succ⁻¹
+  end
 
 namespace left_module
 
@@ -60,15 +94,15 @@ f ↘ (to_right_inv (deg f) i)
 
 infix ` ← `:101 := graded_hom_fn_out -- todo: change notation
 
-definition graded_hom.mk [constructor] {M₁ M₂ : graded_module R I} (d : I ≃ I)
+definition graded_hom.mk [constructor] (d : I ≃ I)
   (fn : Πi, M₁ i →lm M₂ (d i)) : M₁ →gm M₂ :=
 graded_hom.mk' d (λi j p, homomorphism_of_eq (ap M₂ p) ∘lm fn i)
 
-definition graded_hom.mk_out [constructor] {M₁ M₂ : graded_module R I} (d : I ≃ I)
+definition graded_hom.mk_out [constructor] (d : I ≃ I)
   (fn : Πi, M₁ (d⁻¹ i) →lm M₂ i) : M₁ →gm M₂ :=
 graded_hom.mk' d (λi j p, fn j ∘lm homomorphism_of_eq (ap M₁ (eq_inv_of_eq p)))
 
-definition graded_hom.mk_out_in [constructor] {M₁ M₂ : graded_module R I} (d₁ : I ≃ I) (d₂ : I ≃ I)
+definition graded_hom.mk_out_in [constructor] (d₁ : I ≃ I) (d₂ : I ≃ I)
   (fn : Πi, M₁ (d₁ i) →lm M₂ (d₂ i)) : M₁ →gm M₂ :=
 graded_hom.mk' (d₁⁻¹ᵉ ⬝e d₂) (λi j p, homomorphism_of_eq (ap M₂ p) ∘lm fn (d₁⁻¹ᵉ i) ∘lm
   homomorphism_of_eq (ap M₁ (to_right_inv d₁ i)⁻¹))
@@ -77,6 +111,10 @@ definition graded_hom_eq_transport (f : M₁ →gm M₂) {i j : I} (p : deg f i
   f ↘ p m = transport M₂ p (f i m) :=
 by induction p; reflexivity
 
+definition graded_hom_mk_refl (d : I ≃ I)
+  (fn : Πi, M₁ i →lm M₂ (d i)) {i : I} (m : M₁ i) : graded_hom.mk d fn i m = fn i m :=
+by reflexivity
+
 definition graded_hom_eq_zero {f : M₁ →gm M₂} {i j k : I} {q : deg f i = j} {p : deg f i = k}
   (m : M₁ i) (r : f ↘ q m = 0) : f ↘ p m = 0 :=
 have f ↘ p m = transport M₂ (q⁻¹ ⬝ p) (f ↘ q m), begin induction p, induction q, reflexivity end,
@@ -102,6 +140,16 @@ abbreviation gmid [constructor] := graded_hom_id M
 definition gm_constant [constructor] (M₁ M₂ : graded_module R I) (d : I ≃ I) : M₁ →gm M₂ :=
 graded_hom.mk' d (gmd_constant d M₁ M₂)
 
+definition is_surjective_graded_hom_compose ⦃x z⦄
+  (f' : M₂ →gm M₃) (f : M₁ →gm M₂) (p : deg f' (deg f x) = z)
+  (H' : Π⦃y⦄ (q : deg f' y = z), is_surjective (f' ↘ q))
+  (H : Π⦃y⦄ (q : deg f x = y), is_surjective (f ↘ q)) : is_surjective ((f' ∘gm f) ↘ p) :=
+begin
+  induction p,
+  apply is_surjective_compose (f' (deg f x)) (f x),
+  apply H', apply H
+end
+
 structure graded_iso (M₁ M₂ : graded_module R I) : Type :=
 mk' :: (to_hom : M₁ →gm M₂)
        (is_equiv_to_hom : Π⦃i j⦄ (p : deg to_hom i = j), is_equiv (to_hom ↘ p))
@@ -183,8 +231,8 @@ infixl ` ⬝epgm `:75 := graded_iso.eq_trans
 definition graded_hom_of_eq [constructor] {M₁ M₂ : graded_module R I} (p : M₁ ~ M₂) : M₁ →gm M₂ :=
 proof graded_iso_of_eq p qed
 
-definition foo {I : Set} (P : I → Type) {i j : I} (M : P i) (N : P j) := unit
-notation M ` ==[`:50 P:0 `] `:0 N:50 := foo P M N
+definition fooff {I : Set} (P : I → Type) {i j : I} (M : P i) (N : P j) := unit
+notation M ` ==[`:50 P:0 `] `:0 N:50 := fooff P M N
 
 definition graded_homotopy (f g : M₁ →gm M₂) : Type :=
 Π⦃i j k⦄ (p : deg f i = j) (q : deg g i = k) (m : M₁ i), f ↘ p m ==[λi, M₂ i] g ↘ q m
@@ -344,6 +392,12 @@ begin
   exact graded_hom_eq_zero m p
 end
 
+definition is_surjective_graded_image_lift ⦃x y⦄ (f : M₁ →gm M₂)
+  (p : deg f x = y) : is_surjective (graded_image_lift f ↘ p) :=
+begin
+  exact sorry
+end
+
 definition graded_image' (f : M₁ →gm M₂) : graded_module R I :=
 λi, image_module (f i)
 
@@ -493,7 +547,18 @@ namespace left_module
   graded_image_lift i ∘gm graded_submodule_incl _
   -- degree i + 0
 
-  theorem j_lemma1 ⦃x : I⦄ (m : D x) : d ((deg j) x) (j x m) = 0 :=
+  lemma is_surjective_i' {x y : I} (p : deg i' x = y)
+    (H : Π⦃z⦄ (q : deg i z = x), is_surjective (i ↘ q)) : is_surjective (i' ↘ p) :=
+  begin
+    apply is_surjective_graded_hom_compose,
+    { intro y q, apply is_surjective_graded_image_lift },
+    { intro y q, apply is_surjective_of_is_equiv,
+      induction q,
+      exact to_is_equiv (equiv_of_isomorphism (image_module_isomorphism (i ← x) (H _)))
+      }
+  end
+
+  lemma j_lemma1 ⦃x : I⦄ (m : D x) : d ((deg j) x) (j x m) = 0 :=
   begin
     rewrite [graded_hom_compose_fn,↑d,graded_hom_compose_fn],
     refine ap (graded_hom_fn j (deg k (deg j x))) _ ⬝
@@ -501,7 +566,7 @@ namespace left_module
     exact compose_constant.elim (gmod_im_in_ker (jk)) x m
   end
 
-  theorem j_lemma2 : Π⦃x : I⦄ ⦃m : D x⦄ (p : i x m = 0),
+  lemma j_lemma2 : Π⦃x : I⦄ ⦃m : D x⦄ (p : i x m = 0),
     (graded_quotient_map _ ∘gm graded_hom_lift j j_lemma1) x m = 0 :> E' _ :=
   begin
     have Π⦃x y : I⦄ (q : deg k x = y) (r : deg d x = deg j y)
@@ -594,12 +659,19 @@ namespace left_module
   ⦃exact_couple, D := D' X, E := E' X, i := i' X, j := j' X, k := k' X,
     ij := i'j' X, jk := j'k' X, ki := k'i' X⦄
 
-  parameters {R : Ring} {I : Set} (X : exact_couple R I) (B : I → ℕ)
-    (Dub : Π⦃x y⦄ ⦃s : ℕ⦄, B x ≤ s → (deg (k X))⁻¹ (iterate (deg (i X)) s ((deg (j X))⁻¹ x)) = y → is_contr (D X y))
-    (Eub : Π⦃x y⦄ ⦃s : ℕ⦄, B x ≤ s → (deg (k X))⁻¹ (iterate (deg (i X)) s ((deg (j X))⁻¹ x)) = y → is_contr (E X y))
-    (Dlb : Π⦃x y⦄ ⦃s : ℕ⦄, B x ≤ s → deg (j X) (iterate (deg (i X))⁻¹ s (deg (k X) x)) = y → is_contr (D X y))
-    (Elb : Π⦃x y⦄ ⦃s : ℕ⦄, B x ≤ s → deg (j X) (iterate (deg (i X))⁻¹ s (deg (k X) x)) = y → is_contr (E X y))
--- also need a single deg j and/or deg k here
+  parameters {R : Ring} {I : Set} (X : exact_couple R I) (B B' : I → ℕ)
+    (Dub : Π⦃x y⦄ ⦃s : ℕ⦄, (deg (i X))^[s] x = y → B x ≤ s → is_contr (D X y))
+    (Eub : Π⦃x y⦄ ⦃s : ℕ⦄, (deg (k X))⁻¹ (iterate (deg (i X)) s ((deg (j X))⁻¹ x)) = y →
+           B x ≤ s → is_contr (E X y))
+    (Dlb : Π⦃x y z⦄ ⦃s : ℕ⦄ (p : deg (i X) x = y),
+    iterate (deg (i X)) s y = z → B' z ≤ s → is_surjective (i X ↘ p))
+    (Elb : Π⦃x y⦄ ⦃s : ℕ⦄, deg (j X) (iterate (deg (i X))⁻¹ᵉ s (deg (k X) x)) = y → B x ≤ s →
+           is_contr (E X y))
+    (deg_ik_commute : deg (i X) ∘ deg (k X) ~ deg (k X) ∘ deg (i X))
+
+  definition deg_iterate_ik_commute (n : ℕ) (x : I) :
+    (deg (i X))^[n] (deg (k X) x) = deg (k X) ((deg (i X))^[n] x) :=
+  iterate_commute _ deg_ik_commute x
 
   -- we start counting pages at 0, not at 2.
   definition page (r : ℕ) : exact_couple R I :=
@@ -638,55 +710,126 @@ namespace left_module
       apply hwhisker_left, symmetry, apply iterate_succ }
   end
 
+  definition deg_j_inv (r : ℕ) :
+    (deg (j (page r)))⁻¹ ~ iterate (deg (i X)) r ∘ (deg (j X))⁻¹ :=
+  have H : deg (j (page r)) ~ iterate_equiv (deg (i X))⁻¹ᵉ r ⬝e deg (j X), from deg_j r,
+  λx, to_inv_homotopy_to_inv H x ⬝ iterate_inv (deg (i X))⁻¹ᵉ r ((deg (j X))⁻¹ x)
+
   definition deg_d (r : ℕ) :
     deg (d (page r)) ~ deg (j X) ∘ iterate (deg (i X))⁻¹ r ∘ deg (k X) :=
   compose2 (deg_j r) (deg_k r)
 
   definition deg_d_inv (r : ℕ) :
     (deg (d (page r)))⁻¹ ~ (deg (k X))⁻¹ ∘ iterate (deg (i X)) r ∘ (deg (j X))⁻¹ :=
-  sorry --inv_homotopy_inv (deg_d r) ⬝hty _  --compose2 (deg_j r) (deg_k r)
+  compose2 (to_inv_homotopy_to_inv (deg_k r)) (deg_j_inv r)
 
   include Elb Eub
-  definition Eub' (x : I) (r : ℕ) (h : B x ≤ r) :
-    is_contr (E (page r) (deg (d (page r)) x)) :=
-  is_contr_E _ _ (Elb h (deg_d r x)⁻¹)
-
-  definition Elb' (x : I) (r : ℕ) (h : B x ≤ r) :
-    is_contr (E (page r) ((deg (d (page r)))⁻¹ x)) :=
-  is_contr_E _ _ (Eub h (deg_d_inv r x)⁻¹)
-
-  -- definition Dub' (x : I) (r : ℕ) (h : B x ≤ r) :
-  --   is_contr (D (page r) (deg (d (page r)) x)) :=
-  -- is_contr_D _ _ (Dlb h (deg_d r x)⁻¹)
-
-  -- definition Dlb' (x : I) (r : ℕ) (h : B x ≤ r) :
-  --   is_contr (D (page r) ((deg (d (page r)))⁻¹ x)) :=
-  -- is_contr_D _ _ (Dub h (deg_d_inv r x)⁻¹)
-
   definition Estable {x : I} {r : ℕ} (H : B x ≤ r) :
     E (page (r + 1)) x ≃lm E (page r) x :=
   begin
     change homology (d (page r) x) (d (page r) ← x) ≃lm E (page r) x,
-    apply homology_isomorphism,
-    exact Elb' _ _ H, exact Eub' _ _ H
+    apply homology_isomorphism: apply is_contr_E,
+    exact Eub (deg_d_inv r x)⁻¹ H, exact Elb (deg_d r x)⁻¹ H
   end
 
-  definition is_equiv_i {x y : I} {r : ℕ} (H : B y ≤ r) (p : deg (i (page r)) x = y) :
-    is_equiv (i (page r) ↘ p) :=
+  include Dlb
+  definition is_surjective_i {x y z : I} {r s : ℕ} (H : B' z ≤ s + r)
+    (p : deg (i (page r)) x = y) (q : iterate (deg (i X)) s y = z) :
+    is_surjective (i (page r) ↘ p) :=
   begin
-    induction p,
-    exact sorry
+    revert x y z s H p q, induction r with r IH: intro x y z s H p q,
+    { exact Dlb p q H  },
+    { change is_surjective (i' (page r) ↘ p),
+      apply is_surjective_i', intro z' q',
+      refine IH _ _ _ _ (le.trans H (le_of_eq (succ_add s r)⁻¹)) _ _,
+      refine !iterate_succ ⬝ ap ((deg (i X))^[s]) _ ⬝ q,
+      exact !deg_i⁻¹ ⬝ p }
   end
 
-  definition Dstable {x : I} {r : ℕ} (H : B x ≤ r) :
+  definition Dstable {x : I} {r : ℕ} (H : B' x ≤ r) :
     D (page (r + 1)) x ≃lm D (page r) x :=
   begin
     change image_module (i (page r) ← x) ≃lm D (page r) x,
-    exact image_module_isomorphism (isomorphism.mk (i (page r) ← x) (is_equiv_i H _))
+    refine image_module_isomorphism (i (page r) ← x)
+      (is_surjective_i (le.trans H (le_of_eq !zero_add⁻¹)) _ _),
+    reflexivity
   end
 
-  definition inf_page : graded_module R I :=
-  λx, E (page (B (deg (k X) x))) x
+  definition Einf : graded_module R I :=
+  λx, E (page (B x)) x
+
+  definition Dinf : graded_module R I :=
+  λx, D (page (B' x)) x
+
+  definition Einfstable {x y : I} {r : ℕ} (Hr : B y ≤ r) (p : x = y) :
+    Einf y ≃lm E (page r) x :=
+  by symmetry; induction p; induction Hr with r Hr IH; reflexivity; exact Estable Hr ⬝lm IH
+
+  definition Dinfstable {x y : I} {r : ℕ} (Hr : B' y ≤ r) (p : x = y) :
+    Dinf y ≃lm D (page r) x :=
+  by symmetry; induction p; induction Hr with r Hr IH; reflexivity; exact Dstable Hr ⬝lm IH
+
+  parameters {x : I}
+
+  definition r (n : ℕ) : ℕ :=
+  max (max (B x + n + 1) (B ((deg (i X))^[n] x)))
+      (max (B' (deg (k X) ((deg (i X))^[n] x)))
+           (max (B' (deg (k X) ((deg (i X))^[n+1] x))) (B ((deg (j X))⁻¹ ((deg (i X))^[n] x)))))
+
+  lemma rb0 (n : ℕ) : r n ≥ n + 1 :=
+  ge.trans !le_max_left (ge.trans !le_max_left !le_add_left)
+  lemma rb1 (n : ℕ) : B x ≤ r n - (n + 1) :=
+  le_sub_of_add_le (le.trans !le_max_left !le_max_left)
+  lemma rb2 (n : ℕ) : B ((deg (i X))^[n] x) ≤ r n :=
+  le.trans !le_max_right !le_max_left
+  lemma rb3 (n : ℕ) : B' (deg (k X) ((deg (i X))^[n] x)) ≤ r n :=
+  le.trans !le_max_left !le_max_right
+  lemma rb4 (n : ℕ) : B' (deg (k X) ((deg (i X))^[n+1] x)) ≤ r n :=
+  le.trans (le.trans !le_max_left !le_max_right) !le_max_right
+  lemma rb5 (n : ℕ) : B ((deg (j X))⁻¹ ((deg (i X))^[n] x)) ≤ r n :=
+  le.trans (le.trans !le_max_right !le_max_right) !le_max_right
+
+  definition Einfdiag : graded_module R ℕ :=
+  λn, Einf ((deg (i X))^[n] x)
+
+  definition Dinfdiag : graded_module R ℕ :=
+  λn, Dinf (deg (k X) ((deg (i X))^[n] x))
+
+  include deg_ik_commute Dub
+  definition short_exact_mod_page_r (n : ℕ) : short_exact_mod
+    (E (page (r n)) ((deg (i X))^[n] x))
+    (D (page (r n)) (deg (k (page (r n))) ((deg (i X))^[n] x)))
+    (D (page (r n)) (deg (i (page (r n))) (deg (k (page (r n))) ((deg (i X))^[n] x)))) :=
+  begin
+    fapply short_exact_mod_of_is_exact,
+    { exact j (page (r n)) ← ((deg (i X))^[n] x) },
+    { exact k (page (r n)) ((deg (i X))^[n] x) },
+    { exact i (page (r n)) (deg (k (page (r n))) ((deg (i X))^[n] x)) },
+    { exact j (page (r n)) _ },
+    { apply is_contr_D, refine Dub !deg_j_inv⁻¹ (rb5 n) },
+    { apply is_contr_E, refine Elb _ (rb1 n),
+      refine ap (deg (j X)) _ ⬝ !deg_j⁻¹,
+      refine iterate_sub _ !rb0 _ ⬝ _, apply ap (_^[r n]),
+      exact ap (deg (i X)) (!deg_iterate_ik_commute ⬝ !deg_k⁻¹) ⬝ !deg_i⁻¹ },
+    { apply jk (page (r n)) },
+    { apply ki (page (r n)) },
+    { apply ij (page (r n)) }
+  end
+
+  definition short_exact_mod_infpage (n : ℕ) :
+    short_exact_mod (Einfdiag n) (Dinfdiag n) (Dinfdiag (n+1)) :=
+  begin
+    refine short_exact_mod_isomorphism _ _ _ (short_exact_mod_page_r n),
+    { exact Einfstable !rb2 idp },
+    { exact Dinfstable !rb3 !deg_k },
+    { exact Dinfstable !rb4 (!deg_i ⬝ ap (deg (i X)) !deg_k ⬝ !deg_ik_commute) }
+  end
+
+  definition Dinfdiag0 (bound_zero : B' (deg (k X) x) = 0) : Dinfdiag 0 ≃lm D X (deg (k X) x) :=
+  Dinfstable (le_of_eq bound_zero) idp
+
+  definition Dinfdiag_stable {s : ℕ} (h : B (deg (k X) x) ≤ s) : is_contr (Dinfdiag s) :=
+  is_contr_D _ _ (Dub !deg_iterate_ik_commute h)
 
   end
 
diff --git a/algebra/is_short_exact.hlean b/algebra/is_short_exact.hlean
index 3f94ced..d0e7b7e 100644
--- a/algebra/is_short_exact.hlean
+++ b/algebra/is_short_exact.hlean
@@ -20,3 +20,16 @@ structure is_short_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C)
   (im_in_ker : Π(a:A), g (f a) = pt)
   (ker_in_im : Π(b:B), (g b = pt) → fiber f b)
   (is_surj   : is_split_surjective g)
+
+definition is_short_exact_of_is_exact {X A B C Y : Type*}
+  (k : X → A) (f : A → B) (g : B → C) (l : C → Y)
+  (hX : is_contr X) (hY : is_contr Y)
+  (kf : is_exact k f) (fg : is_exact f g) (gl : is_exact g l) : is_short_exact f g :=
+sorry
+
+definition is_short_exact_equiv {A B A' B' : Type} {C C' : Type*}
+  {f' : A' → B'} {g' : B' → C'} (f : A → B) (g : B → C)
+  (eA : A ≃ A') (eB : B ≃ B') (eC : C ≃* C')
+  (h : hsquare f f' eA eB) (h : hsquare g g' eB eC)
+  (H : is_short_exact f' g') : is_short_exact f g :=
+sorry
diff --git a/algebra/left_module.hlean b/algebra/left_module.hlean
index 1918447..53fe63c 100644
--- a/algebra/left_module.hlean
+++ b/algebra/left_module.hlean
@@ -7,7 +7,7 @@ Modules prod vector spaces over a ring.
 
 (We use "left_module," which is more precise, because "module" is a keyword.)
 -/
-import algebra.field ..move_to_lib
+import algebra.field ..move_to_lib .is_short_exact
 open is_trunc pointed function sigma eq algebra prod is_equiv equiv group
 
 structure has_scalar [class] (F V : Type) :=
@@ -394,6 +394,28 @@ end
   local attribute pSet_of_LeftModule [coercion]
   definition is_exact_mod (f : M₁ →lm M₂) (f' : M₂ →lm M₃) : Type :=
   @is_exact M₁ M₂ M₃ (homomorphism_fn f) (homomorphism_fn f')
+
+  structure short_exact_mod (A B C : LeftModule R) :=
+    (f : A →lm B)
+    (g : B →lm C)
+    (h : @is_short_exact _ _ (pType.mk _ 0) f g)
+
+  definition short_exact_mod_of_is_exact {X A B C Y : LeftModule R}
+    (k : X →lm A) (f : A →lm B) (g : B →lm C) (l : C →lm Y)
+    (hX : is_contr X) (hY : is_contr Y)
+    (kf : is_exact_mod k f) (fg : is_exact_mod f g) (gl : is_exact_mod g l) :
+    short_exact_mod A B C :=
+  short_exact_mod.mk f g (is_short_exact_of_is_exact k f g l hX hY kf fg gl)
+
+  definition short_exact_mod_isomorphism {A B A' B' C C' : LeftModule R}
+    (eA : A ≃lm A') (eB : B ≃lm B') (eC : C ≃lm C')
+    (H : short_exact_mod A' B' C') : short_exact_mod A B C :=
+  short_exact_mod.mk (eB⁻¹ˡᵐ ∘lm short_exact_mod.f H ∘lm eA) (eC⁻¹ˡᵐ ∘lm short_exact_mod.g H ∘lm eB)
+    (is_short_exact_equiv _ _
+      (equiv_of_isomorphism eA) (equiv_of_isomorphism eB) (pequiv_of_isomorphism eC)
+      (λa, to_right_inv (equiv_of_isomorphism eB) _) (λb, to_right_inv (equiv_of_isomorphism eC) _)
+      (short_exact_mod.h H))
+
   end
 
   end
diff --git a/algebra/submodule.hlean b/algebra/submodule.hlean
index 4ad5375..43cd7aa 100644
--- a/algebra/submodule.hlean
+++ b/algebra/submodule.hlean
@@ -260,6 +260,11 @@ definition image_module [constructor] (φ : M₁ →lm M₂) : LeftModule R := s
 definition image_lift [constructor] (φ : M₁ →lm M₂) : M₁ →lm image_module φ :=
 hom_lift φ (λm, image.mk m idp)
 
+definition is_surjective_image_lift (φ : M₁ →lm M₂) : is_surjective (image_lift φ) :=
+begin
+  refine total_image.rec _, intro m, exact image.mk m (subtype_eq idp)
+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₃ :=
@@ -293,8 +298,9 @@ is_contr.mk 0
     exact (to_respect_zero φ)⁻¹
   end
 
-definition image_module_isomorphism [constructor] (φ : M₁ ≃lm M₂) : image_module φ ≃lm M₂ :=
-submodule_isomorphism _ (λm, image.mk (φ⁻¹ˡᵐ m) proof to_right_inv (equiv_of_isomorphism φ) m qed)
+definition image_module_isomorphism [constructor] (φ : M₁ →lm M₂)
+  (H : is_surjective φ) : image_module φ ≃lm M₂ :=
+submodule_isomorphism _ H
 
 definition has_scalar_kernel (φ : M₁ →lm M₂) ⦃m : M₁⦄ (r : R)
   (p : φ m = 0) : φ (r • m) = 0 :=