From 179575794a0987f3bb5fde7589a4c710cf72ce86 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Mon, 1 Oct 2018 17:44:49 -0400
Subject: [PATCH] Prove basic properties of spectral sequences

Also separate exact_couple and spectral_sequence in separate files
---
 README.md                         |    2 +-
 algebra/exact_couple.hlean        | 1052 +++++++++++++++++++++-------
 algebra/exact_couple_old.hlean    |  288 ++++++++
 algebra/left_module.hlean         |   57 ++
 algebra/spectral_sequence.hlean   | 1055 +++--------------------------
 algebra/submodule.hlean           |   49 +-
 cohomology/projective_space.hlean |    6 +-
 cohomology/serre.hlean            |   18 +-
 homotopy/three_by_three.hlean     |    2 +-
 9 files changed, 1316 insertions(+), 1213 deletions(-)
 create mode 100644 algebra/exact_couple_old.hlean

diff --git a/README.md b/README.md
index 6ad42bd..98e3937 100644
--- a/README.md
+++ b/README.md
@@ -3,7 +3,7 @@
 Formalization project of the CMU HoTT group to formalize the Serre spectral sequence.
 
 *Update July 16*: The construction of the Serre spectral sequence has been completed. The result is `serre_convergence` in `cohomology.serre`.
-The main algebra part is in `algebra.spectral_sequence`.
+The main algebra part is in `algebra.exact_couple`.
 
 This repository also contains the contents of the MRC group on formalizing homology in Lean.
 
diff --git a/algebra/exact_couple.hlean b/algebra/exact_couple.hlean
index 2d8a1ff..32833e1 100644
--- a/algebra/exact_couple.hlean
+++ b/algebra/exact_couple.hlean
@@ -1,288 +1,882 @@
-/-
-Copyright (c) 2016 Egbert Rijke. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Egbert Rijke, Steve Awodey
+/- Exact couples of graded (left-) R-modules. This file includes:
+  - Constructing exact couples from sequences of maps
+  - Deriving an exact couple
+  - The convergence theorem for exact couples -/
 
-Exact couple, derived couples, and so on
--/
+-- Author: Floris van Doorn
 
-/-
-import algebra.group_theory hit.set_quotient types.sigma types.list types.sum .quotient_group .subgroup .ses
+import .graded ..spectrum.basic .product_group
 
-open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function group trunc
-     equiv is_equiv
+open algebra is_trunc left_module is_equiv equiv eq function nat sigma set_quotient group
+     left_module
 
--- This definition needs to be moved to exactness.hlean. However we had trouble doing so. Please help.
-definition iso_ker_im_of_exact {A B C : AbGroup} (f : A →g B) (g : B →g C) (E : is_exact f g) : ab_Kernel g ≃g ab_image f :=
+/- exact couples -/
+
+namespace exact_couple
+
+  structure exact_couple (R : Ring) (I : AddAbGroup) : Type :=
+    (D E : graded_module R I)
+    (i : D →gm D) (j : D →gm E) (k : E →gm D)
+    (ij : is_exact_gmod i j)
+    (jk : is_exact_gmod j k)
+    (ki : is_exact_gmod k i)
+
+  open exact_couple.exact_couple
+
+  definition exact_couple_reindex [constructor] {R : Ring} {I J : AddAbGroup}
+    (e : AddGroup_of_AddAbGroup J ≃g AddGroup_of_AddAbGroup I)
+    (X : exact_couple R I) : exact_couple R J :=
+  ⦃exact_couple, D := λy, D X (e y), E := λy, E X (e y),
+    i := graded_hom_reindex e (i X),
+    j := graded_hom_reindex e (j X),
+    k := graded_hom_reindex e (k X),
+    ij := is_exact_gmod_reindex e (ij X),
+    jk := is_exact_gmod_reindex e (jk X),
+    ki := is_exact_gmod_reindex e (ki X)⦄
+
+  namespace derived_couple
+  section
+
+  parameters {R : Ring} {I : AddAbGroup} (X : exact_couple R I)
+  local abbreviation D := D X
+  local abbreviation E := E X
+  local abbreviation i := i X
+  local abbreviation j := j X
+  local abbreviation k := k X
+  local abbreviation ij := ij X
+  local abbreviation jk := jk X
+  local abbreviation ki := ki X
+
+  definition d : E →gm E := j ∘gm k
+  definition D' : graded_module R I := graded_image i
+  definition E' : graded_module R I := graded_homology d d
+
+  definition is_contr_E' {x : I} (H : is_contr (E x)) : is_contr (E' x) :=
+  is_contr_homology _ _ _
+
+  definition is_contr_D' {x : I} (H : is_contr (D x)) : is_contr (D' x) :=
+  is_contr_image_module _ _
+
+  definition E'_isomorphism {x : I} (H1 : is_contr (E ((deg d)⁻¹ᵉ x)))
+    (H2 : is_contr (E (deg d x))) : E' x ≃lm E x :=
+  homology_isomorphism _ _ H1 H2
+
+  definition i' : D' →gm D' :=
+  graded_image_lift i ∘gm  graded_submodule_incl (λx, image (i ← x))
+
+  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
-  fapply ab_subgroup_iso,
-  intro a,
-  induction E,
-  exact ker_in_im a,
-  intro a b, induction b with q, induction q with b p, induction p,
-  induction E,
-  exact im_in_ker b,
+    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
 
-definition is_differential {B : AbGroup} (d : B →g B) := Π(b:B), d (d b) = 1
-
-definition image_subgroup_of_diff {B : AbGroup} (d : B →g B) (H : is_differential d) : subgroup_rel (ab_kernel d) :=
-  subgroup_rel_of_subgroup (image_subgroup d) (kernel_subgroup d)
+  lemma j_lemma1 ⦃x : I⦄ (m : D x) : d ((deg j) x) (j x m) = 0 :=
   begin
-    intro g p,
-    induction p with f, induction f with h p,
-    rewrite [p⁻¹],
-    esimp,
-    exact H h
+    rewrite [graded_hom_compose_fn,↑d,graded_hom_compose_fn],
+    refine ap (graded_hom_fn j (deg k (deg j x))) _ ⬝
+      !to_respect_zero,
+    exact compose_constant.elim (gmod_im_in_ker (jk)) x m
   end
 
-definition diff_im_in_ker {B : AbGroup} (d : B →g B) (H : is_differential d) : Π(b : B), image_subgroup d b → kernel_subgroup d b :=
+  lemma j_lemma2 : Π⦃x : I⦄ ⦃m : D x⦄ (p : i x m = 0),
+    (graded_homology_intro _ _ ∘gm graded_hom_lift _ j j_lemma1) x m = 0 :> E' _ :=
   begin
-    intro b p,
-    induction p with q, induction q with b' p, induction p, exact H b'
+    have Π⦃x y : I⦄ (q : deg k x = y) (r : deg d x = deg j y)
+      (s : ap (deg j) q = r) ⦃m : D y⦄ (p : i y m = 0), image (d ↘ r) (j y m),
+    begin
+      intros, induction s, induction q,
+      note m_in_im_k := is_exact.ker_in_im (ki idp _) _ p,
+      induction m_in_im_k with e q,
+      induction q,
+      apply image.mk e idp
+    end,
+    have Π⦃x : I⦄ ⦃m : D x⦄ (p : i x m = 0), image (d ← (deg j x)) (j x m),
+    begin
+      intros,
+      refine this _ _ _ p,
+      exact to_right_inv (deg k) _ ⬝ to_left_inv (deg j) x,
+      apply is_set.elim
+      -- rewrite [ap_con, -adj],
+    end,
+    intros,
+    rewrite [graded_hom_compose_fn],
+    exact @quotient_map_eq_zero _ _ _ _ _ (this p)
   end
 
-definition homology {B : AbGroup} (d : B →g B) (H : is_differential d) : AbGroup :=
-  @quotient_ab_group (ab_kernel d) (image_subgroup_of_diff d H)
+  definition j' : D' →gm E' :=
+  graded_image_elim (graded_homology_intro d d ∘gm graded_hom_lift _ j j_lemma1) j_lemma2
+  -- degree deg j - deg i
 
-definition homology_ugly {B : AbGroup} (d : B →g B) (H : is_differential d) : AbGroup :=
-  @quotient_ab_group (ab_kernel d) (image_subgroup (ab_subgroup_of_subgroup_incl (diff_im_in_ker d H)))
+  lemma k_lemma1 ⦃x : I⦄ (m : E x) (p : d x m = 0) : image (i ← (deg k x)) (k x m) :=
+  gmod_ker_in_im (exact_couple.ij X) (k x m) p
 
+  definition k₂ : graded_kernel d →gm D' := graded_submodule_functor k k_lemma1
 
-definition homology_iso_ugly {B : AbGroup} (d : B →g B) (H : is_differential d) : (homology d H) ≃g (homology_ugly d H) :=
+  lemma k_lemma2 ⦃x : I⦄ (m : E x) (h₁ : lm_kernel (d x) m) (h₂ : image (d ← x) m) :
+    k₂ x ⟨m, h₁⟩ = 0 :=
   begin
-  fapply @iso_of_ab_qg_group (ab_kernel d),
-  intro a,
-  intro p, induction p with f, induction f with b p,
-  fapply tr, fapply fiber.mk, fapply sigma.mk, exact d b, fapply tr, fapply fiber.mk, exact b, reflexivity,
-  induction a with c q, fapply subtype_eq, refine p ⬝ _, reflexivity,
-  intro b p, induction p with f, induction f with c p, induction p,
-  induction c with a q, induction q with f, induction f with a' p, induction p,
-  fapply tr, fapply fiber.mk, exact a', reflexivity
+    assert H₁ : Π⦃x' y z w : I⦄ (p : deg k x' = y) (q : deg j y = z) (r : deg k z = w) (n : E x'),
+      k ↘ r (j ↘ q (k ↘ p n)) = 0,
+    { intros, exact gmod_im_in_ker (exact_couple.jk X) q r (k ↘ p n) },
+    induction h₂ with n p,
+    assert H₂ : k x m = 0,
+    { rewrite [-p], refine ap (k x) (graded_hom_compose_fn_out j k x n) ⬝ _, apply H₁ },
+    exact subtype_eq H₂
   end
 
+  definition k' : E' →gm D' :=
+  @graded_quotient_elim _ _ _ _ _ _ k₂
+                       (by intro x m h; cases m with [m1, m2]; exact k_lemma2 m1 m2 h)
 
-definition SES_iso_C {A B C C' : AbGroup} (ses : SES A B C) (k : C ≃g C') : SES A B C' :=
+  open sigma.ops
+  definition i'_eq ⦃x : I⦄ (m : D x) (h : image (i ← x) m) : (i' x ⟨m, h⟩).1 = i x m :=
+  by reflexivity
+
+  definition k'_eq ⦃x : I⦄ (m : E x) (h : d x m = 0) : (k' x (class_of ⟨m, h⟩)).1 = k x m :=
+  by reflexivity
+
+  lemma j'_eq {x : I} (m : D x) : j' ↘ (ap (deg j) (left_inv (deg i) x)) (graded_image_lift i x m) =
+    class_of (graded_hom_lift _ j proof j_lemma1 qed x m) :=
   begin
-  fapply SES.mk,
-  exact SES.f ses,
-  exact k ∘g SES.g ses,
-  exact SES.Hf ses,
-  fapply @is_surjective_compose _ _ _ k (SES.g ses),
-  exact is_surjective_of_is_equiv k,
-  exact SES.Hg ses,
-  fapply is_exact.mk,
-  intro a,
-  esimp,
-  note h := SES.ex ses,
-  note h2 := is_exact.im_in_ker h a,
-  refine ap k h2 ⬝ _ ,
-  exact to_respect_one k,
-  intro b,
-  intro k3,
-  note h := SES.ex ses,
-  note h3 := is_exact.ker_in_im h b,
-  fapply is_exact.ker_in_im h,
-  refine  _ ⬝ ap k⁻¹ᵍ k3 ⬝ _ ,
-  esimp,
-  exact (to_left_inv (equiv_of_isomorphism k) ((SES.g ses) b))⁻¹,
-  exact to_respect_one k⁻¹ᵍ
+    refine graded_image_elim_destruct _ _ _ idp _ m,
+    apply is_set.elim,
   end
 
+  definition deg_i' : deg i' ~ deg i := by reflexivity
+  definition deg_j' : deg j' ~ deg j ∘ (deg i)⁻¹ := by reflexivity
+  definition deg_k' : deg k' ~ deg k := by reflexivity
 
-definition SES_of_differential_ugly {B : AbGroup} (d : B →g B) (H : is_differential d) : SES (ab_image d) (ab_kernel d) (homology_ugly d H) :=
+  open group
+  set_option pp.coercions true
+  lemma i'j' : is_exact_gmod i' j' :=
   begin
-    exact SES_of_inclusion (ab_subgroup_of_subgroup_incl (diff_im_in_ker d H)) (is_embedding_ab_subgroup_of_subgroup_incl (diff_im_in_ker d H)),
-   end
-
-definition SES_of_differential {B : AbGroup} (d : B →g B) (H : is_differential d) : SES (ab_image d) (ab_kernel d) (homology d H) :=
-  begin
-    fapply SES_iso_C,
-    fapply SES_of_inclusion (ab_subgroup_of_subgroup_incl (diff_im_in_ker d H)) (is_embedding_ab_subgroup_of_subgroup_incl (diff_im_in_ker d H)),
-    exact (homology_iso_ugly d H)⁻¹ᵍ
-   end
-
-structure exact_couple (A B : AbGroup) : Type :=
-  ( i : A →g A) (j : A →g B) (k : B →g A)
-  ( exact_ij : is_exact i j)
-  ( exact_jk : is_exact j k)
-  ( exact_ki : is_exact k i)
-
-definition differential {A B : AbGroup} (EC : exact_couple A B) : B →g B :=
-  (exact_couple.j EC) ∘g (exact_couple.k EC)
-
-definition differential_is_differential {A B : AbGroup} (EC : exact_couple A B) : is_differential (differential EC) :=
-  begin
-    induction EC,
-    induction exact_jk,
-    intro b,
-    exact (ap (group_fun j) (im_in_ker (group_fun k b))) ⬝ (respect_one j)
+    intro x, refine equiv_rect (deg i) _ _,
+    intros y z p q, revert z q x p,
+    refine eq.rec_grading (deg i ⬝e deg j') (deg j) (ap (deg j) (left_inv (deg i) y)) _,
+    intro x, revert y, refine eq.rec_equiv (deg i) _,
+    apply transport (λx, is_exact_mod x _) (idpath (i' x)),
+    apply transport (λx, is_exact_mod _ (j' ↘ (ap (deg j) (left_inv (deg i) x)))) (idpath x),
+    apply is_exact_mod.mk,
+    { revert x, refine equiv_rect (deg i) _ _, intro x,
+      refine graded_image.rec _, intro m,
+      transitivity j' ↘ _ (graded_image_lift i (deg i x) (i x m)),
+        apply ap (λx, j' ↘ _ x), apply subtype_eq, apply i'_eq,
+      refine !j'_eq ⬝ _,
+      apply ap class_of, apply subtype_eq, exact is_exact.im_in_ker (exact_couple.ij X idp idp) m },
+    { revert x, refine equiv_rect (deg k) _ _, intro x,
+      refine graded_image.rec _, intro m p,
+      assert q : graded_homology_intro d d (deg j (deg k x))
+                   (graded_hom_lift _ j j_lemma1 (deg k x) m) = 0,
+      { exact !j'_eq⁻¹ ⬝ p },
+      note q2 := image_of_graded_homology_intro_eq_zero idp (graded_hom_lift _ j _ _ m) q,
+      induction q2 with n r,
+      assert s : j (deg k x) (m - k x n) = 0,
+      { refine respect_sub (j (deg k x)) m (k x n) ⬝ _,
+        refine ap (sub _) r ⬝ _, apply sub_self },
+      assert t : trunctype.carrier (image (i ← (deg k x)) (m - k x n)),
+      { exact is_exact.ker_in_im (exact_couple.ij X _ _) _ s },
+      refine image.mk ⟨m - k x n, t⟩ _,
+      apply subtype_eq, refine !i'_eq ⬝ !to_respect_sub ⬝ _,
+      refine ap (@sub (D (deg i (deg k x))) _ _) _ ⬝ @sub_zero _ _ _,
+      apply is_exact.im_in_ker (exact_couple.ki X _ _) }
   end
 
-section derived_couple
-
-/-
-   A - i -> A
- k ^        |
-   |        v j
-   B ====== B
--/
-
-  parameters {A B : AbGroup} (EC : exact_couple A B)
-  local abbreviation i := exact_couple.i EC
-  local abbreviation j := exact_couple.j EC
-  local abbreviation k := exact_couple.k EC
-  local abbreviation d := differential EC
-  local abbreviation H := differential_is_differential EC
- -- local abbreviation u := exact_couple.i (SES_of_differential d H)
-
-definition derived_couple_A : AbGroup :=
-  ab_subgroup (image_subgroup i)
-
-definition derived_couple_B : AbGroup :=
-  homology (differential EC) (differential_is_differential EC)
-
-definition derived_couple_i : derived_couple_A →g derived_couple_A :=
-  (image_lift (exact_couple.i EC)) ∘g (image_incl (exact_couple.i EC))
-
-definition SES_of_exact_couple_at_i : SES (ab_kernel i) A (ab_image i) :=
+  lemma j'k' : is_exact_gmod j' k' :=
   begin
-  fapply SES_iso_C,
-  fapply SES_of_subgroup (kernel_subgroup i),
-  fapply ab_group_first_iso_thm i,
+    refine equiv_rect (deg i) _ _,
+    intros x y z p, revert y p z,
+    refine eq.rec_grading (deg i ⬝e deg j') (deg j) (ap (deg j) (left_inv (deg i) x)) _,
+    intro z q, induction q,
+    apply is_exact_mod.mk,
+    { refine graded_image.rec _, intro m,
+      refine ap (k' _) (j'_eq m) ⬝ _,
+      apply subtype_eq,
+      refine k'_eq _ _ ⬝ _,
+      exact is_exact.im_in_ker (exact_couple.jk X idp idp) m },
+    { intro m p, induction m using set_quotient.rec_prop with m,
+      induction m with m h, note q := (k'_eq m h)⁻¹ ⬝ ap pr1 p,
+      induction is_exact.ker_in_im (exact_couple.jk X idp idp) m q with n r,
+      apply image.mk (graded_image_lift i x n),
+      refine !j'_eq ⬝ _,
+      apply ap class_of, apply subtype_eq, exact r }
   end
 
-definition kj_zero (a : A) : k (j a) = 1 :=
-is_exact.im_in_ker (exact_couple.exact_jk EC) a
-
-definition j_factor : A →g (ab_kernel d) :=
-begin
-  fapply ab_hom_lift j,
-  intro a,
-  unfold kernel_subgroup,
-  exact calc
-    d (j a) = j (k (j a)) : rfl
-       ...  = j 1 : by exact ap j (kj_zero a)
-       ...  = 1   : to_respect_one,
-end
-
-definition subgroup_iso_exact_at_A : ab_kernel i ≃g ab_image k :=
+  lemma k'i' : is_exact_gmod k' i' :=
   begin
-  fapply ab_subgroup_iso,
-  intro a,
-  induction EC,
-  induction exact_ki,
-  exact ker_in_im a,
-  intro a b, induction b with f, induction f with b p, induction p,
-  induction EC,
-  induction exact_ki,
-  exact im_in_ker b,
+    apply is_exact_gmod.mk,
+    { intro x m, induction m using set_quotient.rec_prop with m,
+      cases m with m p, apply subtype_eq,
+      change i (deg k x) (k x m) = 0,
+      exact is_exact.im_in_ker (exact_couple.ki X idp idp) m },
+    { intro x m, induction m with m h, intro p,
+      have i (deg k x) m = 0, from ap pr1 p,
+      induction is_exact.ker_in_im (exact_couple.ki X idp idp) m this with n q,
+      have j (deg k x) m = 0, from @(is_exact.im_in_ker2 (exact_couple.ij X _ _)) m h,
+      have d x n = 0, from ap (j (deg k x)) q ⬝ this,
+      exact image.mk (class_of ⟨n, this⟩) (subtype_eq q) }
   end
 
-definition subgroup_iso_exact_at_A_triangle : ab_kernel_incl i ~ ab_image_incl k ∘g subgroup_iso_exact_at_A :=
+  end
+  end derived_couple
+
+  open derived_couple
+
+  definition derived_couple [constructor] {R : Ring} {I : AddAbGroup}
+    (X : exact_couple R I) : exact_couple R I :=
+  ⦃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⦄
+
+  /- if an exact couple is bounded, we can prove the convergence theorem for it -/
+  structure is_bounded {R : Ring} {I : AddAbGroup} (X : exact_couple R I) : Type :=
+  mk' :: (B B' : I → ℕ)
+    (Dub : Π⦃x y⦄ ⦃s : ℕ⦄, (deg (i X))^[s] x = y → B x ≤ s → is_contr (D X y))
+    (Dlb : Π⦃x y z⦄ ⦃s : ℕ⦄ (p : deg (i X) x = y), (deg (i X))^[s] y = z → B' z ≤ s →
+      is_surjective (i X ↘ p))
+    (Elb : Π⦃x y⦄ ⦃s : ℕ⦄, (deg (i X))⁻¹ᵉ^[s] x = y → B x ≤ s → is_contr (E X y))
+
+/- Note: Elb proves Dlb for some bound B', but we want tight control over when B' = 0 -/
+  protected definition is_bounded.mk [constructor] {R : Ring} {I : AddAbGroup} {X : exact_couple R I}
+    (B B' B'' : I → ℕ)
+    (Dub : Π⦃x : I⦄ ⦃s : ℕ⦄, B x ≤ s → is_contr (D X ((deg (i X))^[s] x)))
+    (Dlb : Π⦃x : I⦄ ⦃s : ℕ⦄, B' x ≤ s → is_surjective (i X (((deg (i X))⁻¹ᵉ^[s + 1] x))))
+    (Elb : Π⦃x : I⦄ ⦃s : ℕ⦄, B'' x ≤ s → is_contr (E X ((deg (i X))⁻¹ᵉ^[s] x))) : is_bounded X :=
   begin
-    fapply ab_subgroup_iso_triangle,
-    intro a b, induction b with f, induction f with b p, induction p,
-    induction EC, induction exact_ki, exact im_in_ker b,
+    apply is_bounded.mk' (λx, max (B x) (B'' x)) B',
+    { intro x y s p h, induction p, exact Dub (le.trans !le_max_left h) },
+    { exact abstract begin intro x y z s p q h, induction p, induction q,
+      refine transport (λx, is_surjective (i X x)) _ (Dlb h),
+      rewrite [-iterate_succ], apply iterate_left_inv end end },
+    { intro x y s p h, induction p, exact Elb (le.trans !le_max_right h) }
   end
 
-definition subgroup_homom_ker_to_im : ab_kernel i →g ab_image d :=
-  (image_homomorphism k j) ∘g subgroup_iso_exact_at_A
-
-open eq
-
-definition left_square_derived_ses_aux : j_factor ∘g ab_image_incl k ~ (SES.f (SES_of_differential d H)) ∘g (image_homomorphism k j) :=
+  open is_bounded
+  definition is_bounded_reindex [constructor] {R : Ring} {I J : AddAbGroup}
+    (e : AddGroup_of_AddAbGroup J ≃g AddGroup_of_AddAbGroup I)
+    {X : exact_couple R I} (HH : is_bounded X) : is_bounded (exact_couple_reindex e X) :=
   begin
-    intro x,
-    induction x with a p, induction p with f, induction f with b p, induction p,
-    fapply subtype_eq,
-    reflexivity,
+    apply is_bounded.mk' (B HH ∘ e) (B' HH ∘ e),
+    { intros x y s p h, refine Dub HH _ h,
+      refine (iterate_hsquare e _ s x)⁻¹ ⬝ ap e p, intro x,
+      exact to_right_inv (group.equiv_of_isomorphism e) _ },
+    { intros x y z s p q h, refine Dlb HH _ _ h,
+      refine (iterate_hsquare e _ s y)⁻¹ ⬝ ap e q, intro x,
+      exact to_right_inv (group.equiv_of_isomorphism e) _ },
+    { intro x y s p h, refine Elb HH _ h,
+      refine (iterate_hsquare e _ s x)⁻¹ ⬝ ap e p, intro x,
+      exact to_right_inv (group.equiv_of_isomorphism e) _ },
+
   end
 
-definition left_square_derived_ses : j_factor ∘g (ab_kernel_incl i) ~ (SES.f (SES_of_differential d H)) ∘g subgroup_homom_ker_to_im :=
+  namespace convergence_theorem
+  section
+
+  parameters {R : Ring} {I : AddAbGroup} (X : exact_couple R I) (HH : is_bounded X)
+
+  local abbreviation B := B HH
+  local abbreviation B' := B' HH
+  local abbreviation Dub := Dub HH
+  local abbreviation Dlb := Dlb HH
+  local abbreviation Elb := Elb HH
+
+  /- We start counting pages at 0, which corresponds to what is usually called the second page -/
+  definition page (r : ℕ) : exact_couple R I :=
+  iterate derived_couple r X
+
+  definition is_contr_E (r : ℕ) (x : I) (h : is_contr (E X x)) :
+    is_contr (E (page r) x) :=
+  by induction r with r IH; exact h; exact is_contr_E' (page r) IH
+
+  definition is_contr_D (r : ℕ) (x : I) (h : is_contr (D X x)) :
+    is_contr (D (page r) x) :=
+  by induction r with r IH; exact h; exact is_contr_D' (page r) IH
+
+  definition deg_i (r : ℕ) : deg (i (page r)) ~ deg (i X) :=
   begin
-    intro x,
-    exact (ap j_factor (subgroup_iso_exact_at_A_triangle x)) ⬝ (left_square_derived_ses_aux (subgroup_iso_exact_at_A x)),
+    induction r with r IH,
+    { reflexivity },
+    { exact IH }
   end
 
-definition derived_couple_j_unique :
-    is_contr (Σ hC, group_fun (hC ∘g SES.g SES_of_exact_couple_at_i) ~ group_fun
-       (SES.g (SES_of_differential d H) ∘g j_factor)) :=
-quotient_extend_unique_SES (SES_of_exact_couple_at_i) (SES_of_differential d H) (subgroup_homom_ker_to_im) (j_factor) (left_square_derived_ses)
-
-definition derived_couple_j : derived_couple_A →g derived_couple_B :=
-   begin
-     exact pr1 (center' (derived_couple_j_unique)),
-   end
-
-definition derived_couple_j_htpy : group_fun (derived_couple_j ∘g SES.g SES_of_exact_couple_at_i) ~ group_fun
-       (SES.g (SES_of_differential d H) ∘g j_factor) :=
-   begin
-     exact pr2 (center' (derived_couple_j_unique)),
-   end
-
-definition SES_im_i_trivial : SES trivial_ab_group derived_couple_A derived_couple_A :=
+  definition deg_k (r : ℕ) : deg (k (page r)) ~ deg (k X) :=
   begin
-    fapply SES_of_isomorphism_right,
-    fapply isomorphism.refl,
+    induction r with r IH,
+    { reflexivity },
+    { exact IH }
   end
 
-definition subgroup_iso_exact_kerj_imi : ab_kernel j ≃g ab_image i :=
+  definition deg_j (r : ℕ) :
+    deg (j (page r)) ~ deg (j X) ∘ iterate (deg (i X))⁻¹ r :=
   begin
-    fapply iso_ker_im_of_exact,
-    induction EC,
-    exact exact_ij,
+    induction r with r IH,
+    { reflexivity },
+    { refine hwhisker_left (deg (j (page r)))
+        (to_inv_homotopy_inv (deg_i r)) ⬝hty _,
+      refine hwhisker_right _ IH ⬝hty _,
+      apply hwhisker_left, symmetry, apply iterate_succ }
   end
 
-definition k_restrict_aux : ab_kernel d →g ab_kernel j :=
-  begin
-    fapply ab_hom_lift_kernel,
-    exact k ∘g ab_kernel_incl d,
-    intro p, induction p with b p, exact p,
-  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_inv H x ⬝ iterate_inv (deg (i X))⁻¹ᵉ r ((deg (j X))⁻¹ x)
 
-definition k_restrict : ab_kernel d →g derived_couple_A :=
-  subgroup_iso_exact_kerj_imi ∘g k_restrict_aux
+  definition deg_dr (r : ℕ) :
+    deg (d (page r)) ~ deg (j X) ∘ iterate (deg (i X))⁻¹ r ∘ deg (k X) :=
+  compose2 (deg_j r) (deg_k r)
 
-definition k_restrict_square_left : k_restrict ∘g (SES.f (SES_of_differential d H)) ~ λ x, 1 :=
+  definition deg_dr_inv (r : ℕ) :
+    (deg (d (page r)))⁻¹ ~ (deg (k X))⁻¹ ∘ iterate (deg (i X)) r ∘ (deg (j X))⁻¹ :=
+  compose2 (to_inv_homotopy_inv (deg_k r)) (deg_j_inv r)
+
+  -- definition E_isomorphism' {x : I} {r₁ r₂ : ℕ} (H : r₁ ≤ r₂)
+  --   (H1 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E X ((deg (d (page r)))⁻¹ᵉ x)))
+  --   (H2 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E X (deg (d (page r)) x))) :
+  --   E (page r₂) x ≃lm E (page r₁) x :=
+  -- begin
+  --   assert H2 : Π⦃r⦄, r₁ ≤ r → r ≤ r₂ → E (page r) x ≃lm E (page r₁) x,
+  --   { intro r Hr₁ Hr₂,
+  --     induction Hr₁ with r Hr₁ IH, reflexivity,
+  --     let Hr₂' := le_of_succ_le Hr₂,
+  --     exact E'_isomorphism (page r) (is_contr_E r _ (H1 Hr₁ Hr₂)) (is_contr_E r _ (H2 Hr₁ Hr₂))
+  --       ⬝lm IH Hr₂' },
+  --   exact H2 H (le.refl _)
+  -- end
+
+  -- definition E_isomorphism0' {x : I} {r : ℕ}
+  --   (H1 : Πr, is_contr (E X ((deg (d (page r)))⁻¹ᵉ x)))
+  --   (H2 : Πr, is_contr (E X (deg (d (page r)) x))) : E (page r) x ≃lm E X x :=
+  -- E_isomorphism' (zero_le r) _ _
+
+  parameter {X}
+
+  definition deg_iterate_ik_commute (n : ℕ) :
+    hsquare (deg (k X)) (deg (k X)) ((deg (i X))^[n]) ((deg (i X))^[n]) :=
+  iterate_commute n (deg_commute (k X) (i X))
+
+  definition deg_iterate_ij_commute (n : ℕ) :
+    hsquare (deg (j X)) (deg (j X)) ((deg (i X))⁻¹ᵉ^[n]) ((deg (i X))⁻¹ᵉ^[n]) :=
+  iterate_commute n (deg_commute (j X) (i X))⁻¹ʰᵗʸᵛ
+
+  definition B2 (x : I) : ℕ := max (B (deg (k X) x)) (B ((deg (j X))⁻¹ x))
+  definition Eub ⦃x y : I⦄ ⦃s : ℕ⦄ (p : (deg (i X))^[s] x = y) (h : B2 x ≤ s) :
+    is_contr (E X y) :=
   begin
-    intro x,
-    induction x with b' p,
-    induction p with q,
-    induction q with b p,
     induction p,
-    fapply subtype_eq,
-    induction EC,
-    induction exact_jk,
-    fapply im_in_ker,
+    refine @(is_contr_middle_of_is_exact (exact_couple.jk X (right_inv (deg (j X)) _) idp)) _ _ _,
+    exact Dub (iterate_commute s (deg_commute (j X) (i X))⁻¹ʰᵗʸʰ x) (le.trans !le_max_right h),
+    exact Dub (deg_iterate_ik_commute s x) (le.trans !le_max_left h)
   end
 
-definition derived_couple_k_unique :   is_contr
-    (Σ hC, group_fun (hC ∘g SES.g (SES_of_differential d H)) ~ group_fun
-       (SES.g SES_im_i_trivial ∘g k_restrict))
-  :=
-quotient_extend_unique_SES (SES_of_differential d H) (SES_im_i_trivial) (trivial_homomorphism (ab_image d) trivial_ab_group) (k_restrict) (k_restrict_square_left)
+  definition B3 (x : I) : ℕ :=
+  max (B (deg (j X) (deg (k X) x))) (B2 ((deg (k X))⁻¹ ((deg (j X))⁻¹ x)))
 
-definition derived_couple_k : derived_couple_B →g derived_couple_A :=
-   begin
-     exact pr1 (center' (derived_couple_k_unique)),
-   end
-
-definition derived_couple_k_htpy : group_fun (derived_couple_k ∘g SES.g (SES_of_differential d H)) ~ group_fun
-       (SES.g (SES_im_i_trivial) ∘g k_restrict) :=
-   begin
-     exact pr2 (center' (derived_couple_k_unique)),
-   end
-
-definition derived_couple_exact_ij : is_exact_ag derived_couple_i derived_couple_j :=
+  definition Estable {x : I} {r : ℕ} (H : B3 x ≤ r) :
+    E (page (r + 1)) x ≃lm E (page r) x :=
   begin
-    fapply is_exact.mk,
-    intro a,
-    induction a with a' t,
-    induction t with q, induction q with a p, induction p,
-    repeat exact sorry,
+    change homology (d (page r) x) (d (page r) ← x) ≃lm E (page r) x,
+    apply homology_isomorphism: apply is_contr_E,
+    exact Eub (hhinverse (deg_iterate_ik_commute r) _ ⬝ (deg_dr_inv r x)⁻¹)
+              (le.trans !le_max_right H),
+    exact Elb (deg_iterate_ij_commute r _ ⬝ (deg_dr r x)⁻¹)
+              (le.trans !le_max_left H)
   end
 
-end derived_couple
+  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
+    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) :
+    D (page (r + 1)) x ≃lm D (page r) x :=
+  begin
+    change image_module (i (page r) ← x) ≃lm D (page r) x,
+    refine image_module_isomorphism (i (page r) ← x)
+      (is_surjective_i (le.trans H (le_of_eq !zero_add⁻¹)) _ _),
+    reflexivity
+  end
+
+  /- the infinity pages of E and D -/
+  definition Einf : graded_module R I :=
+  λx, E (page (B3 x)) x
+
+  definition Dinf : graded_module R I :=
+  λx, D (page (B' x)) x
+
+  definition Einfstable {x y : I} {r : ℕ} (Hr : B3 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
+
+  -- definition Einf_isomorphism' {x : I} (r₁ : ℕ)
+  --   (H1 : Π⦃r⦄, r₁ ≤ r → is_contr (E X ((deg (d (page r)))⁻¹ᵉ x)))
+  --   (H2 : Π⦃r⦄, r₁ ≤ r → is_contr (E X (deg (d (page r)) x))) :
+  --   Einf x ≃lm E (page r₁) x :=
+  -- begin
+  --   cases le.total r₁ (B3 x) with Hr Hr,
+  --   exact E_isomorphism' Hr (λr Hr₁ Hr₂, H1 Hr₁) (λr Hr₁ Hr₂, H2 Hr₁),
+  --   exact Einfstable Hr idp
+  -- end
+
+  -- definition Einf_isomorphism0' {x : I}
+  --   (H1 : Π⦃r⦄, is_contr (E X ((deg (d (page r)))⁻¹ᵉ x)))
+  --   (H2 : Π⦃r⦄, is_contr (E X (deg (d (page r)) x))) :
+  --   Einf x ≃lm E X x :=
+  -- E_isomorphism0' _ _
+
+  parameters (x : I)
+
+  definition rb (n : ℕ) : ℕ :=
+  max (max (B (deg (j X) (deg (k X) x)) + n + 1) (B3 ((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 : ℕ) : rb n ≥ n + 1 :=
+  ge.trans !le_max_left (ge.trans !le_max_left !le_add_left)
+  lemma rb1 (n : ℕ) : B (deg (j X) (deg (k X) x)) ≤ rb n - (n + 1) :=
+  nat.le_sub_of_add_le (le.trans !le_max_left !le_max_left)
+  lemma rb2 (n : ℕ) : B3 ((deg (i X))^[n] x) ≤ rb n :=
+  le.trans !le_max_right !le_max_left
+  lemma rb3 (n : ℕ) : B' (deg (k X) ((deg (i X))^[n] x)) ≤ rb n :=
+  le.trans !le_max_left !le_max_right
+  lemma rb4 (n : ℕ) : B' (deg (k X) ((deg (i X))^[n+1] x)) ≤ rb 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)) ≤ rb 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))
+
+  definition short_exact_mod_page_r (n : ℕ) : short_exact_mod
+    (E (page (rb n)) ((deg (i X))^[n] x))
+    (D (page (rb n)) (deg (k (page (rb n))) ((deg (i X))^[n] x)))
+    (D (page (rb n)) (deg (i (page (rb n))) (deg (k (page (rb n))) ((deg (i X))^[n] x)))) :=
+  begin
+    fapply short_exact_mod_of_is_exact,
+    { exact j (page (rb n)) ← ((deg (i X))^[n] x) },
+    { exact k (page (rb n)) ((deg (i X))^[n] x) },
+    { exact i (page (rb n)) (deg (k (page (rb n))) ((deg (i X))^[n] x)) },
+    { exact j (page (rb n)) _ },
+    { apply is_contr_D, refine Dub !deg_j_inv⁻¹ (rb5 n) },
+    { apply is_contr_E, refine Elb _ (rb1 n),
+      refine !deg_iterate_ij_commute ⬝ _,
+      refine ap (deg (j X)) _ ⬝ !deg_j⁻¹,
+      refine iterate_sub _ !rb0 _ ⬝ _, apply ap (_^[rb n]),
+      exact ap (deg (i X)) (!deg_iterate_ik_commute ⬝ !deg_k⁻¹) ⬝ !deg_i⁻¹ },
+    { apply jk (page (rb n)) },
+    { apply ki (page (rb n)) },
+    { apply ij (page (rb 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_commute (k X) (i X) _) }
+  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
+
+  lemma Dinfdiag_stable {s : ℕ} (h : B (deg (k X) x) ≤ s) : is_contr (Dinfdiag s) :=
+  is_contr_D _ _ (Dub !deg_iterate_ik_commute h)
+
+  /- some useful immediate properties -/
+
+  definition short_exact_mod_infpage0 (bound_zero : B' (deg (k X) x) = 0) :
+    short_exact_mod (Einfdiag 0) (D X (deg (k X) x)) (Dinfdiag 1) :=
+  begin
+    refine short_exact_mod_isomorphism _ _ _ (short_exact_mod_infpage 0),
+    { reflexivity },
+    { exact (Dinfdiag0 bound_zero)⁻¹ˡᵐ },
+    { reflexivity }
+  end
+
+  /- the convergence theorem is the following result -/
+  definition is_built_from_infpage (bound_zero : B' (deg (k X) x) = 0) :
+    is_built_from (D X (deg (k X) x)) Einfdiag :=
+  is_built_from.mk Dinfdiag short_exact_mod_infpage (Dinfdiag0 bound_zero) (B (deg (k X) x))
+    (λs, Dinfdiag_stable)
+
+  end
+
+  definition deg_dr_reindex {R : Ring} {I J : AddAbGroup}
+    (e : AddGroup_of_AddAbGroup J ≃g AddGroup_of_AddAbGroup I) (X : exact_couple R I)
+    (r : ℕ) : deg (d (page (exact_couple_reindex e X) r)) ~
+    e⁻¹ᵍ ∘ deg (d (page X r)) ∘ e :=
+  begin
+    intro x, refine !deg_dr ⬝ _ ⬝ ap e⁻¹ᵍ !deg_dr⁻¹,
+    apply ap (e⁻¹ᵍ ∘ deg (j X)),
+    note z := @iterate_hsquare _ _ (deg (i (exact_couple_reindex e X)))⁻¹ᵉ (deg (i X))⁻¹ᵉ e
+      (λx, proof to_right_inv (group.equiv_of_isomorphism e) _ qed)⁻¹ʰᵗʸʰ r,
+    refine z _ ⬝ _, apply ap ((deg (i X))⁻¹ᵉ^[r]),
+    exact to_right_inv (group.equiv_of_isomorphism e) _
+  end
+
+  end convergence_theorem
+
+  open int group prod convergence_theorem prod.ops
+
+  definition Z2 [constructor] : AddAbGroup := agℤ ×aa agℤ
+
+  structure convergent_exact_couple.{u v w} {R : Ring} (E' : agℤ → agℤ → LeftModule.{u v} R)
+                                 (Dinf : agℤ → LeftModule.{u w} R) : Type.{max u (v+1) (w+1)} :=
+    (X : exact_couple.{u 0 w v} R Z2)
+    (HH : is_bounded X)
+    (st : agℤ → Z2)
+    (HB : Π(n : agℤ), is_bounded.B' HH (deg (k X) (st n)) = 0)
+    (e : Π(x : Z2), exact_couple.E X x ≃lm E' x.1 x.2)
+    (f : Π(n : agℤ), exact_couple.D X (deg (k X) (st n)) ≃lm Dinf n)
+    (deg_d : ℕ → Z2)
+    (deg_d_eq0 : Π(r : ℕ), deg (d (page X r)) 0 = deg_d r)
+
+  infix ` ⟹ `:25 := convergent_exact_couple -- todo: maybe this should define convergent_spectral_sequence
+
+  definition convergent_exact_couple_g [reducible] (E' : agℤ → agℤ → AbGroup) (Dinf : agℤ → AbGroup) : Type :=
+  (λn s, LeftModule_int_of_AbGroup (E' n s)) ⟹ (λn, LeftModule_int_of_AbGroup (Dinf n))
+
+  infix ` ⟹ᵍ `:25 := convergent_exact_couple_g
+
+  section exact_couple
+  open convergent_exact_couple
+  parameters {R : Ring} {E' : agℤ → agℤ → LeftModule R} {Dinf : agℤ → LeftModule R} (c : E' ⟹ Dinf)
+  local abbreviation X := X c
+  local abbreviation i := i X
+  local abbreviation HH := HH c
+  local abbreviation st := st c
+  local abbreviation Dinfdiag (n : agℤ) (k : ℕ) := Dinfdiag HH (st n) k
+  local abbreviation Einfdiag (n : agℤ) (k : ℕ) := Einfdiag HH (st n) k
+
+  definition deg_d_eq (r : ℕ) (ns : Z2) : (deg (d (page X r))) ns = ns + deg_d c r :=
+  !deg_eq ⬝ ap (λx, _ + x) (deg_d_eq0 c r)
+
+  definition deg_d_inv_eq (r : ℕ) (ns : Z2) :
+    (deg (d (page X r)))⁻¹ᵉ ns = ns - deg_d c r :=
+  inv_eq_of_eq (!deg_d_eq ⬝ proof !neg_add_cancel_right qed)⁻¹
+
+  definition convergent_exact_couple_isomorphism {E'' : agℤ → agℤ → LeftModule R} {Dinf' : graded_module R agℤ}
+    (e' : Πn s, E' n s ≃lm E'' n s) (f' : Πn, Dinf n ≃lm Dinf' n) : E'' ⟹ Dinf' :=
+  convergent_exact_couple.mk X HH st (HB c)
+    begin intro x, induction x with n s, exact e c (n, s) ⬝lm e' n s end
+    (λn, f c n ⬝lm f' n) (deg_d c) (deg_d_eq0 c)
+
+  include c
+  definition convergent_exact_couple_reindex (i : agℤ ×ag agℤ ≃g agℤ ×ag agℤ) :
+    (λp q, E' (i (p, q)).1 (i (p, q)).2) ⟹ Dinf :=
+  begin
+    fapply convergent_exact_couple.mk (exact_couple_reindex i X) (is_bounded_reindex i HH),
+    { exact λn, i⁻¹ᵍ (st n) },
+    { intro n, refine ap (B' HH) _ ⬝ HB c n,
+      refine to_right_inv (group.equiv_of_isomorphism i) _ ⬝ _,
+      apply ap (deg (k X)), exact to_right_inv (group.equiv_of_isomorphism i) _ },
+    { intro x, induction x with p q, exact e c (i (p, q)) },
+    { intro n, refine _ ⬝lm f c n, refine isomorphism_of_eq (ap (D X) _),
+      refine to_right_inv (group.equiv_of_isomorphism i) _ ⬝ _,
+      apply ap (deg (k X)), exact to_right_inv (group.equiv_of_isomorphism i) _ },
+    { exact λn, i⁻¹ᵍ (deg_d c n) },
+    { intro r, esimp, refine !deg_dr_reindex ⬝ ap i⁻¹ᵍ (ap (deg (d _)) (group.to_respect_zero i) ⬝
+        deg_d_eq0 c r) }
+  end
+
+  definition convergent_exact_couple_negate_abutment : E' ⟹ (λn, Dinf (-n)) :=
+  convergent_exact_couple.mk X HH (st ∘ neg) (λn, HB c (-n)) (e c) (λn, f c (-n))
+                             (deg_d c) (deg_d_eq0 c)
+  omit c
+
+  definition is_built_from_of_convergent_exact_couple (n : ℤ) :
+    is_built_from (Dinf n) (Einfdiag n) :=
+  is_built_from_isomorphism_left (f c n) (is_built_from_infpage HH (st n) (HB c n))
+
+  theorem is_contr_convergent_exact_couple_precise (n : agℤ)
+  (H : Π(n : agℤ) (l : ℕ), is_contr (E' ((deg i)^[l] (st n)).1 ((deg i)^[l] (st n)).2)) :
+    is_contr (Dinf n) :=
+  begin
+    assert H2 : Π(l : ℕ), is_contr (Einfdiag n l),
+    { intro l, apply is_contr_E,
+      refine is_trunc_equiv_closed_rev -2 (equiv_of_isomorphism (e c _)) (H n l) },
+    exact is_contr_total (is_built_from_of_convergent_exact_couple n) H2
+  end
+
+  theorem is_contr_convergent_exact_couple (n : agℤ) (H : Π(n s : agℤ), is_contr (E' n s)) :
+    is_contr (Dinf n) :=
+  is_contr_convergent_exact_couple_precise n (λn s, !H)
+
+  -- definition E_isomorphism {r₁ r₂ : ℕ} {n s : agℤ} (H : r₁ ≤ r₂)
+  --   (H1 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E X ((n, s) - deg_d c r)))
+  --   (H2 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E X ((n, s) + deg_d c r))) :
+  --   E (page X r₂) (n, s) ≃lm E (page X r₁) (n, s) :=
+  -- E_isomorphism' X H
+  --   (λr Hr₁ Hr₂, transport (is_contr ∘ E X) (deg_d_inv_eq r (n, s))⁻¹ᵖ (H1 Hr₁ Hr₂))
+  --   (λr Hr₁ Hr₂, transport (is_contr ∘ E X) (deg_d_eq r (n, s))⁻¹ᵖ (H2 Hr₁ Hr₂))
+
+  -- definition E_isomorphism0 {r : ℕ} {n s : agℤ} (H1 : Πr, is_contr (E X ((n, s) - deg_d c r)))
+  --   (H2 : Πr, is_contr (E X ((n, s) + deg_d c r))) : E (page X r) (n, s) ≃lm E' n s :=
+  -- E_isomorphism (zero_le r) _ _ ⬝lm e c (n, s)
+
+  -- definition Einf_isomorphism (r₁ : ℕ) {n s : agℤ}
+  --   (H1 : Π⦃r⦄, r₁ ≤ r → is_contr (E X ((n,s) - deg_d c r)))
+  --   (H2 : Π⦃r⦄, r₁ ≤ r → is_contr (E X ((n,s) + deg_d c r))) :
+  --   Einf HH (n, s) ≃lm E (page X r₁) (n, s) :=
+  -- Einf_isomorphism' HH r₁ (λr Hr₁, transport (is_contr ∘ E X) (deg_d_inv_eq r (n, s))⁻¹ᵖ (H1 Hr₁))
+  --                        (λr Hr₁, transport (is_contr ∘ E X) (deg_d_eq r (n, s))⁻¹ᵖ (H2 Hr₁))
+
+  -- definition Einf_isomorphism0 {n s : agℤ}
+  --   (H1 : Π⦃r⦄, is_contr (E X ((n,s) - deg_d c r)))
+  --   (H2 : Π⦃r⦄, is_contr (E X ((n,s) + deg_d c r))) :
+  --   Einf HH (n, s) ≃lm E' n s :=
+  -- E_isomorphism0 _ _
+
+  end exact_couple
+
+  variables {E' : agℤ → agℤ → AbGroup} {Dinf : agℤ → AbGroup}
+  definition convergent_exact_couple_g_isomorphism {E'' : agℤ → agℤ → AbGroup}
+    {Dinf' : agℤ → AbGroup} (c : E' ⟹ᵍ Dinf)
+    (e' : Πn s, E' n s ≃g E'' n s) (f' : Πn, Dinf n ≃g Dinf' n) : E'' ⟹ᵍ Dinf' :=
+  convergent_exact_couple_isomorphism c (λn s, lm_iso_int.mk (e' n s)) (λn, lm_iso_int.mk (f' n))
+
+end exact_couple
+open exact_couple
+namespace pointed
+
+  open pointed int group is_trunc trunc is_conn
+
+  definition homotopy_group_conn_nat (n : ℕ) (A : Type*[1]) : AbGroup :=
+  AbGroup.mk (π[n] A) (ab_group_homotopy_group_of_is_conn n A)
+
+  definition homotopy_group_conn : Π(n : ℤ) (A : Type*[1]), AbGroup
+  | (of_nat n) A := homotopy_group_conn_nat n A
+  | (-[1+ n])  A := trivial_ab_group_lift
+
+  notation `πc[`:95 n:0 `]`:0 := homotopy_group_conn n
+
+  definition homotopy_group_conn_nat_functor (n : ℕ) {A B : Type*[1]} (f : A →* B) :
+    homotopy_group_conn_nat n A →g homotopy_group_conn_nat n B :=
+  begin
+    cases n with n, { apply trivial_homomorphism },
+    cases n with n, { apply trivial_homomorphism },
+    exact π→g[n+2] f
+  end
+
+  definition homotopy_group_conn_functor :
+    Π(n : ℤ) {A B : Type*[1]} (f : A →* B), πc[n] A →g πc[n] B
+  | (of_nat n) A B f := homotopy_group_conn_nat_functor n f
+  | (-[1+ n])  A B f := trivial_homomorphism _ _
+
+  notation `π→c[`:95 n:0 `]`:0 := homotopy_group_conn_functor n
+
+  section
+  open prod prod.ops fiber
+  parameters {A : ℤ → Type*[1]} (f : Π(n : ℤ), A n →* A (n - 1)) [Hf : Πn, is_conn_fun 1 (f n)]
+  include Hf
+  local abbreviation I [constructor] := Z2
+
+  -- definition D_sequence : graded_module rℤ I :=
+  -- λv, LeftModule_int_of_AbGroup (πc[v.2] (A (v.1)))
+
+  -- definition E_sequence : graded_module rℤ I :=
+  -- λv, LeftModule_int_of_AbGroup (πc[v.2] (pconntype.mk (pfiber (f (v.1))) !Hf pt))
+
+  /- first need LES of these connected homotopy groups -/
+
+  -- definition exact_couple_sequence : exact_couple rℤ I :=
+  -- exact_couple.mk D_sequence E_sequence sorry sorry sorry sorry sorry sorry
+
+  end
+
+
+end pointed
+
+namespace spectrum
+  open pointed int group is_trunc trunc is_conn prod prod.ops group fin chain_complex
+  section
+
+  parameters {A : ℤ → spectrum} (f : Π(s : ℤ), A s →ₛ A (s - 1))
+
+  local abbreviation I [constructor] := Z2
+
+  definition D_sequence : graded_module rℤ I :=
+  λv, LeftModule_int_of_AbGroup (πₛ[v.1] (A (v.2)))
+
+  definition E_sequence : graded_module rℤ I :=
+  λv, LeftModule_int_of_AbGroup (πₛ[v.1] (sfiber (f (v.2))))
+
+  include f
+
+  definition i_sequence : D_sequence →gm D_sequence :=
+  begin
+    fapply graded_hom.mk, exact (prod_equiv_prod erfl (add_right_action (- (1 : ℤ)))),
+    { intro i, exact pair_eq !add_zero⁻¹ idp },
+    intro v,
+    apply lm_hom_int.mk, esimp,
+    rexact πₛ→[v.1] (f v.2)
+  end
+
+  definition deg_j_seq_inv [constructor] : I ≃ I :=
+  prod_equiv_prod (add_right_action (1 : ℤ)) (add_right_action (- (1 : ℤ)))
+
+  definition fn_j_sequence [unfold 3] (x : I) :
+    D_sequence (deg_j_seq_inv x) →lm E_sequence x :=
+  begin
+    induction x with n s,
+    apply lm_hom_int.mk, esimp,
+    rexact shomotopy_groups_fun (f s) (n, 2)
+  end
+
+  definition j_sequence : D_sequence →gm E_sequence :=
+  graded_hom.mk_out deg_j_seq_inv⁻¹ᵉ (λi, idp) fn_j_sequence
+
+  definition k_sequence : E_sequence →gm D_sequence :=
+  begin
+    fapply graded_hom.mk erfl deg_eq_id,
+    intro v, induction v with n s,
+    apply lm_hom_int.mk, esimp,
+    exact πₛ→[n] (spoint (f s))
+  end
+
+  lemma ij_sequence : is_exact_gmod i_sequence j_sequence :=
+  begin
+    intro x y z p q,
+    revert y z q p,
+    refine eq.rec_right_inv (deg j_sequence) _,
+    intro y, induction x with n s, induction y with m t,
+    refine equiv_rect !pair_eq_pair_equiv⁻¹ᵉ _ _,
+    intro pq, esimp at pq, induction pq with p q,
+    revert t q, refine eq.rec_equiv (add_right_action (-(1 : ℤ))) _,
+    induction p using eq.rec_symm,
+    apply is_exact_homotopy homotopy.rfl,
+    { symmetry, exact graded_hom_mk_out_destruct deg_j_seq_inv⁻¹ᵉ (λi, idp) fn_j_sequence },
+    rexact is_exact_of_is_exact_at (is_exact_LES_of_shomotopy_groups (f s) (m, 2)),
+  end
+
+  lemma jk_sequence : is_exact_gmod j_sequence k_sequence :=
+  begin
+    intro x y z p q, induction q,
+    revert x y p, refine eq.rec_right_inv (deg j_sequence) _,
+    intro x, induction x with n s,
+    apply is_exact_homotopy,
+    { symmetry, exact graded_hom_mk_out_destruct deg_j_seq_inv⁻¹ᵉ (λi, idp) fn_j_sequence },
+    { reflexivity },
+    rexact is_exact_of_is_exact_at (is_exact_LES_of_shomotopy_groups (f s) (n, 1)),
+  end
+
+  lemma ki_sequence : is_exact_gmod k_sequence i_sequence :=
+  begin
+    intro x y z p q, induction p, induction q, induction x with n s,
+    rexact is_exact_of_is_exact_at (is_exact_LES_of_shomotopy_groups (f s) (n, 0)),
+  end
+
+  definition exact_couple_sequence [constructor] : exact_couple rℤ I :=
+  exact_couple.mk D_sequence E_sequence i_sequence j_sequence k_sequence
+                  ij_sequence jk_sequence ki_sequence
+
+  open int
+  parameters (ub : ℤ → ℤ) (lb : ℤ → ℤ)
+    (Aub : Π(s n : ℤ), s ≥ ub n + (1 : ℤ) → is_equiv (πₛ→[n] (f s)))
+    (Alb : Π(s n : ℤ), s ≤ lb n → is_contr (πₛ[n] (A s)))
+
+  definition B : I → ℕ
+  | (n, s) := max0 (s - lb n)
+
+  definition B' : I → ℕ
+  | (n, s) := max0 (ub n - s)
+
+  definition B'' : I → ℕ
+  | (n, s) := max0 (max (ub n + (1 : ℤ) - s) (ub (n+(1 : ℤ)) + (1 : ℤ) - s))
+
+  lemma iterate_deg_i (n s : ℤ) (m : ℕ) : (deg i_sequence)^[m] (n, s) = (n, s - m) :=
+  begin
+    induction m with m IH,
+    { exact prod_eq idp !sub_zero⁻¹ },
+    { exact ap (deg i_sequence) IH ⬝ (prod_eq idp !sub_sub) }
+  end
+
+  lemma iterate_deg_i_inv (n s : ℤ) (m : ℕ) : (deg i_sequence)⁻¹ᵉ^[m] (n, s) = (n, s + m) :=
+  begin
+    induction m with m IH,
+    { exact prod_eq idp !add_zero⁻¹ },
+    { exact ap (deg i_sequence)⁻¹ᵉ IH ⬝ (prod_eq idp !add.assoc) }
+  end
+
+  include Aub Alb
+  lemma Dub ⦃x : I⦄ ⦃t : ℕ⦄ (h : B x ≤ t) : is_contr (D_sequence ((deg i_sequence)^[t] x)) :=
+  begin
+    apply Alb, induction x with n s, rewrite [iterate_deg_i],
+    apply sub_le_of_sub_le,
+    exact le_of_max0_le h,
+  end
+
+  lemma Dlb ⦃x : I⦄ ⦃t : ℕ⦄ (h : B' x ≤ t) :
+    is_surjective (i_sequence ((deg i_sequence)⁻¹ᵉ^[t+1] x)) :=
+  begin
+    apply is_surjective_of_is_equiv,
+    apply Aub, induction x with n s,
+    rewrite [iterate_deg_i_inv, ▸*, of_nat_add, -add.assoc],
+    apply add_le_add_right,
+    apply le_add_of_sub_left_le,
+    exact le_of_max0_le h
+  end
+
+  lemma Elb ⦃x : I⦄ ⦃t : ℕ⦄ (h : B'' x ≤ t) : is_contr (E_sequence ((deg i_sequence)⁻¹ᵉ^[t] x)) :=
+  begin
+    induction x with n s,
+    rewrite [iterate_deg_i_inv, ▸*],
+    apply is_contr_shomotopy_group_sfiber_of_is_equiv,
+    apply Aub, apply le_add_of_sub_left_le, apply le_of_max0_le, refine le.trans _ h,
+    apply max0_monotone, apply le_max_left,
+    apply Aub, apply le_add_of_sub_left_le, apply le_of_max0_le, refine le.trans _ h,
+    apply max0_monotone, apply le_max_right
+  end
+
+  definition is_bounded_sequence [constructor] : is_bounded exact_couple_sequence :=
+  is_bounded.mk B B' B'' Dub Dlb Elb
+    -- (by intro x; reflexivity)
+    -- begin
+    --   intro x, induction x with n s, apply pair_eq, esimp, esimp, esimp [j_sequence, i_sequence],
+    --   refine !add.assoc ⬝ ap (add s) !add.comm ⬝ !add.assoc⁻¹,
+    -- end
+
+  definition convergent_exact_couple_sequence : (λn s, πₛ[n] (sfiber (f s))) ⟹ᵍ (λn, πₛ[n] (A (ub n))) :=
+  begin
+    fapply convergent_exact_couple.mk,
+    { exact exact_couple_sequence },
+    { exact is_bounded_sequence },
+    { exact λn, (n, ub n) },
+    { intro n, change max0 (ub n - ub n) = 0, exact ap max0 (sub_self (ub n)) },
+    { intro ns, reflexivity },
+    { intro n, reflexivity },
+    { intro r, exact (-(1 : ℤ), r + (1 : ℤ)) },
+    { intro r, refine !convergence_theorem.deg_dr ⬝ _,
+      refine ap (deg j_sequence) !iterate_deg_i_inv ⬝ _,
+      exact prod_eq idp !zero_add }
+  end
+
+  end
+
+-- Uncomment the next line to see that the proof uses univalence, but that there are no holes
+--('sorry') in the proof:
+
+-- print axioms is_bounded_sequence
+
+-- It depends on univalence in an essential way. The reason is that the long exact sequence
+-- of homotopy groups already depends on univalence. Namely, in that proof we need to show that if f
+-- : A → B and g : B → C are exact at B, then ∥A∥₀ → ∥B∥₀ → ∥C∥₀ is exact at ∥B∥₀. For this we need
+-- that the equality |b|₀ = |b'|₀ is equivalent to ∥b = b'∥₋₁, which requires univalence.
+end spectrum
diff --git a/algebra/exact_couple_old.hlean b/algebra/exact_couple_old.hlean
new file mode 100644
index 0000000..2d8a1ff
--- /dev/null
+++ b/algebra/exact_couple_old.hlean
@@ -0,0 +1,288 @@
+/-
+Copyright (c) 2016 Egbert Rijke. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Egbert Rijke, Steve Awodey
+
+Exact couple, derived couples, and so on
+-/
+
+/-
+import algebra.group_theory hit.set_quotient types.sigma types.list types.sum .quotient_group .subgroup .ses
+
+open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function group trunc
+     equiv is_equiv
+
+-- This definition needs to be moved to exactness.hlean. However we had trouble doing so. Please help.
+definition iso_ker_im_of_exact {A B C : AbGroup} (f : A →g B) (g : B →g C) (E : is_exact f g) : ab_Kernel g ≃g ab_image f :=
+  begin
+  fapply ab_subgroup_iso,
+  intro a,
+  induction E,
+  exact ker_in_im a,
+  intro a b, induction b with q, induction q with b p, induction p,
+  induction E,
+  exact im_in_ker b,
+  end
+
+definition is_differential {B : AbGroup} (d : B →g B) := Π(b:B), d (d b) = 1
+
+definition image_subgroup_of_diff {B : AbGroup} (d : B →g B) (H : is_differential d) : subgroup_rel (ab_kernel d) :=
+  subgroup_rel_of_subgroup (image_subgroup d) (kernel_subgroup d)
+  begin
+    intro g p,
+    induction p with f, induction f with h p,
+    rewrite [p⁻¹],
+    esimp,
+    exact H h
+  end
+
+definition diff_im_in_ker {B : AbGroup} (d : B →g B) (H : is_differential d) : Π(b : B), image_subgroup d b → kernel_subgroup d b :=
+  begin
+    intro b p,
+    induction p with q, induction q with b' p, induction p, exact H b'
+  end
+
+definition homology {B : AbGroup} (d : B →g B) (H : is_differential d) : AbGroup :=
+  @quotient_ab_group (ab_kernel d) (image_subgroup_of_diff d H)
+
+definition homology_ugly {B : AbGroup} (d : B →g B) (H : is_differential d) : AbGroup :=
+  @quotient_ab_group (ab_kernel d) (image_subgroup (ab_subgroup_of_subgroup_incl (diff_im_in_ker d H)))
+
+
+definition homology_iso_ugly {B : AbGroup} (d : B →g B) (H : is_differential d) : (homology d H) ≃g (homology_ugly d H) :=
+  begin
+  fapply @iso_of_ab_qg_group (ab_kernel d),
+  intro a,
+  intro p, induction p with f, induction f with b p,
+  fapply tr, fapply fiber.mk, fapply sigma.mk, exact d b, fapply tr, fapply fiber.mk, exact b, reflexivity,
+  induction a with c q, fapply subtype_eq, refine p ⬝ _, reflexivity,
+  intro b p, induction p with f, induction f with c p, induction p,
+  induction c with a q, induction q with f, induction f with a' p, induction p,
+  fapply tr, fapply fiber.mk, exact a', reflexivity
+  end
+
+
+definition SES_iso_C {A B C C' : AbGroup} (ses : SES A B C) (k : C ≃g C') : SES A B C' :=
+  begin
+  fapply SES.mk,
+  exact SES.f ses,
+  exact k ∘g SES.g ses,
+  exact SES.Hf ses,
+  fapply @is_surjective_compose _ _ _ k (SES.g ses),
+  exact is_surjective_of_is_equiv k,
+  exact SES.Hg ses,
+  fapply is_exact.mk,
+  intro a,
+  esimp,
+  note h := SES.ex ses,
+  note h2 := is_exact.im_in_ker h a,
+  refine ap k h2 ⬝ _ ,
+  exact to_respect_one k,
+  intro b,
+  intro k3,
+  note h := SES.ex ses,
+  note h3 := is_exact.ker_in_im h b,
+  fapply is_exact.ker_in_im h,
+  refine  _ ⬝ ap k⁻¹ᵍ k3 ⬝ _ ,
+  esimp,
+  exact (to_left_inv (equiv_of_isomorphism k) ((SES.g ses) b))⁻¹,
+  exact to_respect_one k⁻¹ᵍ
+  end
+
+
+definition SES_of_differential_ugly {B : AbGroup} (d : B →g B) (H : is_differential d) : SES (ab_image d) (ab_kernel d) (homology_ugly d H) :=
+  begin
+    exact SES_of_inclusion (ab_subgroup_of_subgroup_incl (diff_im_in_ker d H)) (is_embedding_ab_subgroup_of_subgroup_incl (diff_im_in_ker d H)),
+   end
+
+definition SES_of_differential {B : AbGroup} (d : B →g B) (H : is_differential d) : SES (ab_image d) (ab_kernel d) (homology d H) :=
+  begin
+    fapply SES_iso_C,
+    fapply SES_of_inclusion (ab_subgroup_of_subgroup_incl (diff_im_in_ker d H)) (is_embedding_ab_subgroup_of_subgroup_incl (diff_im_in_ker d H)),
+    exact (homology_iso_ugly d H)⁻¹ᵍ
+   end
+
+structure exact_couple (A B : AbGroup) : Type :=
+  ( i : A →g A) (j : A →g B) (k : B →g A)
+  ( exact_ij : is_exact i j)
+  ( exact_jk : is_exact j k)
+  ( exact_ki : is_exact k i)
+
+definition differential {A B : AbGroup} (EC : exact_couple A B) : B →g B :=
+  (exact_couple.j EC) ∘g (exact_couple.k EC)
+
+definition differential_is_differential {A B : AbGroup} (EC : exact_couple A B) : is_differential (differential EC) :=
+  begin
+    induction EC,
+    induction exact_jk,
+    intro b,
+    exact (ap (group_fun j) (im_in_ker (group_fun k b))) ⬝ (respect_one j)
+  end
+
+section derived_couple
+
+/-
+   A - i -> A
+ k ^        |
+   |        v j
+   B ====== B
+-/
+
+  parameters {A B : AbGroup} (EC : exact_couple A B)
+  local abbreviation i := exact_couple.i EC
+  local abbreviation j := exact_couple.j EC
+  local abbreviation k := exact_couple.k EC
+  local abbreviation d := differential EC
+  local abbreviation H := differential_is_differential EC
+ -- local abbreviation u := exact_couple.i (SES_of_differential d H)
+
+definition derived_couple_A : AbGroup :=
+  ab_subgroup (image_subgroup i)
+
+definition derived_couple_B : AbGroup :=
+  homology (differential EC) (differential_is_differential EC)
+
+definition derived_couple_i : derived_couple_A →g derived_couple_A :=
+  (image_lift (exact_couple.i EC)) ∘g (image_incl (exact_couple.i EC))
+
+definition SES_of_exact_couple_at_i : SES (ab_kernel i) A (ab_image i) :=
+  begin
+  fapply SES_iso_C,
+  fapply SES_of_subgroup (kernel_subgroup i),
+  fapply ab_group_first_iso_thm i,
+  end
+
+definition kj_zero (a : A) : k (j a) = 1 :=
+is_exact.im_in_ker (exact_couple.exact_jk EC) a
+
+definition j_factor : A →g (ab_kernel d) :=
+begin
+  fapply ab_hom_lift j,
+  intro a,
+  unfold kernel_subgroup,
+  exact calc
+    d (j a) = j (k (j a)) : rfl
+       ...  = j 1 : by exact ap j (kj_zero a)
+       ...  = 1   : to_respect_one,
+end
+
+definition subgroup_iso_exact_at_A : ab_kernel i ≃g ab_image k :=
+  begin
+  fapply ab_subgroup_iso,
+  intro a,
+  induction EC,
+  induction exact_ki,
+  exact ker_in_im a,
+  intro a b, induction b with f, induction f with b p, induction p,
+  induction EC,
+  induction exact_ki,
+  exact im_in_ker b,
+  end
+
+definition subgroup_iso_exact_at_A_triangle : ab_kernel_incl i ~ ab_image_incl k ∘g subgroup_iso_exact_at_A :=
+  begin
+    fapply ab_subgroup_iso_triangle,
+    intro a b, induction b with f, induction f with b p, induction p,
+    induction EC, induction exact_ki, exact im_in_ker b,
+  end
+
+definition subgroup_homom_ker_to_im : ab_kernel i →g ab_image d :=
+  (image_homomorphism k j) ∘g subgroup_iso_exact_at_A
+
+open eq
+
+definition left_square_derived_ses_aux : j_factor ∘g ab_image_incl k ~ (SES.f (SES_of_differential d H)) ∘g (image_homomorphism k j) :=
+  begin
+    intro x,
+    induction x with a p, induction p with f, induction f with b p, induction p,
+    fapply subtype_eq,
+    reflexivity,
+  end
+
+definition left_square_derived_ses : j_factor ∘g (ab_kernel_incl i) ~ (SES.f (SES_of_differential d H)) ∘g subgroup_homom_ker_to_im :=
+  begin
+    intro x,
+    exact (ap j_factor (subgroup_iso_exact_at_A_triangle x)) ⬝ (left_square_derived_ses_aux (subgroup_iso_exact_at_A x)),
+  end
+
+definition derived_couple_j_unique :
+    is_contr (Σ hC, group_fun (hC ∘g SES.g SES_of_exact_couple_at_i) ~ group_fun
+       (SES.g (SES_of_differential d H) ∘g j_factor)) :=
+quotient_extend_unique_SES (SES_of_exact_couple_at_i) (SES_of_differential d H) (subgroup_homom_ker_to_im) (j_factor) (left_square_derived_ses)
+
+definition derived_couple_j : derived_couple_A →g derived_couple_B :=
+   begin
+     exact pr1 (center' (derived_couple_j_unique)),
+   end
+
+definition derived_couple_j_htpy : group_fun (derived_couple_j ∘g SES.g SES_of_exact_couple_at_i) ~ group_fun
+       (SES.g (SES_of_differential d H) ∘g j_factor) :=
+   begin
+     exact pr2 (center' (derived_couple_j_unique)),
+   end
+
+definition SES_im_i_trivial : SES trivial_ab_group derived_couple_A derived_couple_A :=
+  begin
+    fapply SES_of_isomorphism_right,
+    fapply isomorphism.refl,
+  end
+
+definition subgroup_iso_exact_kerj_imi : ab_kernel j ≃g ab_image i :=
+  begin
+    fapply iso_ker_im_of_exact,
+    induction EC,
+    exact exact_ij,
+  end
+
+definition k_restrict_aux : ab_kernel d →g ab_kernel j :=
+  begin
+    fapply ab_hom_lift_kernel,
+    exact k ∘g ab_kernel_incl d,
+    intro p, induction p with b p, exact p,
+  end
+
+definition k_restrict : ab_kernel d →g derived_couple_A :=
+  subgroup_iso_exact_kerj_imi ∘g k_restrict_aux
+
+definition k_restrict_square_left : k_restrict ∘g (SES.f (SES_of_differential d H)) ~ λ x, 1 :=
+  begin
+    intro x,
+    induction x with b' p,
+    induction p with q,
+    induction q with b p,
+    induction p,
+    fapply subtype_eq,
+    induction EC,
+    induction exact_jk,
+    fapply im_in_ker,
+  end
+
+definition derived_couple_k_unique :   is_contr
+    (Σ hC, group_fun (hC ∘g SES.g (SES_of_differential d H)) ~ group_fun
+       (SES.g SES_im_i_trivial ∘g k_restrict))
+  :=
+quotient_extend_unique_SES (SES_of_differential d H) (SES_im_i_trivial) (trivial_homomorphism (ab_image d) trivial_ab_group) (k_restrict) (k_restrict_square_left)
+
+definition derived_couple_k : derived_couple_B →g derived_couple_A :=
+   begin
+     exact pr1 (center' (derived_couple_k_unique)),
+   end
+
+definition derived_couple_k_htpy : group_fun (derived_couple_k ∘g SES.g (SES_of_differential d H)) ~ group_fun
+       (SES.g (SES_im_i_trivial) ∘g k_restrict) :=
+   begin
+     exact pr2 (center' (derived_couple_k_unique)),
+   end
+
+definition derived_couple_exact_ij : is_exact_ag derived_couple_i derived_couple_j :=
+  begin
+    fapply is_exact.mk,
+    intro a,
+    induction a with a' t,
+    induction t with q, induction q with a p, induction p,
+    repeat exact sorry,
+  end
+
+end derived_couple
+
+-/
diff --git a/algebra/left_module.hlean b/algebra/left_module.hlean
index 9ed0444..83ee6ea 100644
--- a/algebra/left_module.hlean
+++ b/algebra/left_module.hlean
@@ -473,6 +473,63 @@ end
 
 end
 
+  /- we say that an left module D is built from the sequence E if
+     D is a "twisted sum" of the E, and E has only finitely many nontrivial values -/
+  open nat
+  structure is_built_from.{u v w} {R : Ring} (D : LeftModule.{u v} R)
+      (E : ℕ → LeftModule.{u w} R) : Type.{max u (v+1) w} :=
+    (part : ℕ → LeftModule.{u v} R)
+    (ses : Πn, short_exact_mod (E n) (part n) (part (n+1)))
+    (e0 : part 0 ≃lm D)
+    (n₀ : ℕ)
+    (HD' : Π(s : ℕ), n₀ ≤ s → is_contr (part s))
+
+  open is_built_from
+  universe variables u v w
+  variables {R : Ring.{u}} {D D' : LeftModule.{u v} R} {E E' : ℕ → LeftModule.{u w} R}
+
+  definition is_built_from_shift (H : is_built_from D E) :
+    is_built_from (part H 1) (λn, E (n+1)) :=
+  is_built_from.mk (λn, part H (n+1)) (λn, ses H (n+1)) isomorphism.rfl (pred (n₀ H))
+    (λs Hle, HD' H _ (le_succ_of_pred_le Hle))
+
+  definition isomorphism_of_is_contr_part (H : is_built_from D E) (n : ℕ) (HE : is_contr (E n)) :
+    part H n ≃lm part H (n+1) :=
+  isomorphism_of_is_contr_left (ses H n) HE
+
+  definition is_contr_submodules (H : is_built_from D E) (HD : is_contr D) (n : ℕ) :
+    is_contr (part H n) :=
+  begin
+    induction n with n IH,
+    { exact is_trunc_equiv_closed_rev -2 (equiv_of_isomorphism (e0 H)) _ },
+    { exact is_contr_right_of_short_exact_mod (ses H n) IH }
+  end
+
+  definition is_contr_quotients (H : is_built_from D E) (HD : is_contr D) (n : ℕ) :
+    is_contr (E n) :=
+  begin
+    apply is_contr_left_of_short_exact_mod (ses H n),
+    exact is_contr_submodules H HD n
+  end
+
+  definition is_contr_total (H : is_built_from D E) (HE : Πn, is_contr (E n)) : is_contr D :=
+  have is_contr (part H 0), from
+  nat.rec_down (λn, is_contr (part H n)) _ (HD' H _ !le.refl)
+    (λn H2, is_contr_middle_of_short_exact_mod (ses H n) (HE n) H2),
+  is_contr_equiv_closed (equiv_of_isomorphism (e0 H)) _
+
+  definition is_built_from_isomorphism (e : D ≃lm D') (f : Πn, E n ≃lm E' n)
+    (H : is_built_from D E) : is_built_from D' E' :=
+  ⦃is_built_from, H, e0 := e0 H ⬝lm e,
+    ses := λn, short_exact_mod_isomorphism (f n)⁻¹ˡᵐ isomorphism.rfl isomorphism.rfl (ses H n)⦄
+
+  definition is_built_from_isomorphism_left (e : D ≃lm D') (H : is_built_from D E) :
+    is_built_from D' E :=
+  ⦃is_built_from, H, e0 := e0 H ⬝lm e⦄
+
+  definition isomorphism_zero_of_is_built_from (H : is_built_from D E) (p : n₀ H = 1) : E 0 ≃lm D :=
+  isomorphism_of_is_contr_right (ses H 0) (HD' H 1 (le_of_eq p)) ⬝lm e0 H
+
 section int
 open int
 definition left_module_int_of_ab_group [constructor] (A : Type) [add_ab_group A] : left_module rℤ A :=
diff --git a/algebra/spectral_sequence.hlean b/algebra/spectral_sequence.hlean
index 4807766..9a33df5 100644
--- a/algebra/spectral_sequence.hlean
+++ b/algebra/spectral_sequence.hlean
@@ -1,984 +1,143 @@
-/- Exact couples of graded (left-) R-modules. This file includes:
-  - Constructing exact couples from sequences of maps
-  - Deriving an exact couple
-  - The convergence theorem for exact couples -/
+/- Spectral sequences
+  - basic properties of spectral sequences
+  - currently, we only construct an spectral sequence from an exact couple
+ -/
 
 -- Author: Floris van Doorn
 
-import .graded ..spectrum.basic .product_group
+import .exact_couple
 
 open algebra is_trunc left_module is_equiv equiv eq function nat sigma set_quotient group
-
-/- exact couples -/
-
-namespace left_module
-
-  section
-  /- move to left_module -/
-  structure is_built_from.{u v w} {R : Ring} (D : LeftModule.{u v} R)
-      (E : ℕ → LeftModule.{u w} R) : Type.{max u (v+1) w} :=
-    (part : ℕ → LeftModule.{u v} R)
-    (ses : Πn, short_exact_mod (E n) (part n) (part (n+1)))
-    (e0 : part 0 ≃lm D)
-    (n₀ : ℕ)
-    (HD' : Π(s : ℕ), n₀ ≤ s → is_contr (part s))
-
-  open is_built_from
-  universe variables u v w
-  variables {R : Ring.{u}} {D D' : LeftModule.{u v} R} {E E' : ℕ → LeftModule.{u w} R}
-
-  definition is_built_from_shift (H : is_built_from D E) :
-    is_built_from (part H 1) (λn, E (n+1)) :=
-  is_built_from.mk (λn, part H (n+1)) (λn, ses H (n+1)) isomorphism.rfl (pred (n₀ H))
-    (λs Hle, HD' H _ (le_succ_of_pred_le Hle))
-
-  definition isomorphism_of_is_contr_part (H : is_built_from D E) (n : ℕ) (HE : is_contr (E n)) :
-    part H n ≃lm part H (n+1) :=
-  isomorphism_of_is_contr_left (ses H n) HE
-
-  definition is_contr_submodules (H : is_built_from D E) (HD : is_contr D) (n : ℕ) :
-    is_contr (part H n) :=
-  begin
-    induction n with n IH,
-    { exact is_trunc_equiv_closed_rev -2 (equiv_of_isomorphism (e0 H)) _ },
-    { exact is_contr_right_of_short_exact_mod (ses H n) IH }
-  end
-
-  definition is_contr_quotients (H : is_built_from D E) (HD : is_contr D) (n : ℕ) :
-    is_contr (E n) :=
-  begin
-    apply is_contr_left_of_short_exact_mod (ses H n),
-    exact is_contr_submodules H HD n
-  end
-
-  definition is_contr_total (H : is_built_from D E) (HE : Πn, is_contr (E n)) : is_contr D :=
-  have is_contr (part H 0), from
-  nat.rec_down (λn, is_contr (part H n)) _ (HD' H _ !le.refl)
-    (λn H2, is_contr_middle_of_short_exact_mod (ses H n) (HE n) H2),
-  is_contr_equiv_closed (equiv_of_isomorphism (e0 H)) _
-
-  definition is_built_from_isomorphism (e : D ≃lm D') (f : Πn, E n ≃lm E' n)
-    (H : is_built_from D E) : is_built_from D' E' :=
-  ⦃is_built_from, H, e0 := e0 H ⬝lm e,
-    ses := λn, short_exact_mod_isomorphism (f n)⁻¹ˡᵐ isomorphism.rfl isomorphism.rfl (ses H n)⦄
-
-  definition is_built_from_isomorphism_left (e : D ≃lm D') (H : is_built_from D E) :
-    is_built_from D' E :=
-  ⦃is_built_from, H, e0 := e0 H ⬝lm e⦄
-
-  definition isomorphism_zero_of_is_built_from (H : is_built_from D E) (p : n₀ H = 1) : E 0 ≃lm D :=
-  isomorphism_of_is_contr_right (ses H 0) (HD' H 1 (le_of_eq p)) ⬝lm e0 H
-
-  end
-
-  structure exact_couple (R : Ring) (I : AddAbGroup) : Type :=
-    (D E : graded_module R I)
-    (i : D →gm D) (j : D →gm E) (k : E →gm D)
-    (ij : is_exact_gmod i j)
-    (jk : is_exact_gmod j k)
-    (ki : is_exact_gmod k i)
-
-  open exact_couple
-
-  definition exact_couple_reindex [constructor] {R : Ring} {I J : AddAbGroup}
-    (e : AddGroup_of_AddAbGroup J ≃g AddGroup_of_AddAbGroup I)
-    (X : exact_couple R I) : exact_couple R J :=
-  ⦃exact_couple, D := λy, D X (e y), E := λy, E X (e y),
-    i := graded_hom_reindex e (i X),
-    j := graded_hom_reindex e (j X),
-    k := graded_hom_reindex e (k X),
-    ij := is_exact_gmod_reindex e (ij X),
-    jk := is_exact_gmod_reindex e (jk X),
-    ki := is_exact_gmod_reindex e (ki X)⦄
-
-  namespace derived_couple
-  section
-
-  parameters {R : Ring} {I : AddAbGroup} (X : exact_couple R I)
-  local abbreviation D := D X
-  local abbreviation E := E X
-  local abbreviation i := i X
-  local abbreviation j := j X
-  local abbreviation k := k X
-  local abbreviation ij := ij X
-  local abbreviation jk := jk X
-  local abbreviation ki := ki X
-
-  definition d : E →gm E := j ∘gm k
-  definition D' : graded_module R I := graded_image i
-  definition E' : graded_module R I := graded_homology d d
-
-  definition is_contr_E' {x : I} (H : is_contr (E x)) : is_contr (E' x) :=
-  !is_contr_homology
-
-  definition is_contr_D' {x : I} (H : is_contr (D x)) : is_contr (D' x) :=
-  !is_contr_image_module
-
-  definition E'_isomorphism {x : I} (H1 : is_contr (E ((deg d)⁻¹ᵉ x)))
-    (H2 : is_contr (E (deg d x))) : E' x ≃lm E x :=
-  @(homology_isomorphism _ _) H1 H2
-
-  definition i' : D' →gm D' :=
-  graded_image_lift i ∘gm  graded_submodule_incl (λx, image (i ← x))
-
-  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))) _ ⬝
-      !to_respect_zero,
-    exact compose_constant.elim (gmod_im_in_ker (jk)) x m
-  end
-
-  lemma j_lemma2 : Π⦃x : I⦄ ⦃m : D x⦄ (p : i x m = 0),
-    (graded_homology_intro _ _ ∘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)
-      (s : ap (deg j) q = r) ⦃m : D y⦄ (p : i y m = 0), image (d ↘ r) (j y m),
-    begin
-      intros, induction s, induction q,
-      note m_in_im_k := is_exact.ker_in_im (ki idp _) _ p,
-      induction m_in_im_k with e q,
-      induction q,
-      apply image.mk e idp
-    end,
-    have Π⦃x : I⦄ ⦃m : D x⦄ (p : i x m = 0), image (d ← (deg j x)) (j x m),
-    begin
-      intros,
-      refine this _ _ _ p,
-      exact to_right_inv (deg k) _ ⬝ to_left_inv (deg j) x,
-      apply is_set.elim
-      -- rewrite [ap_con, -adj],
-    end,
-    intros,
-    rewrite [graded_hom_compose_fn],
-    exact @quotient_map_eq_zero _ _ _ _ _ (this p)
-  end
-
-  definition j' : D' →gm E' :=
-  graded_image_elim (graded_homology_intro d d ∘gm graded_hom_lift _ j j_lemma1) j_lemma2
-  -- degree deg j - deg i
-
-  lemma k_lemma1 ⦃x : I⦄ (m : E x) (p : d x m = 0) : image (i ← (deg k x)) (k x m) :=
-  gmod_ker_in_im (exact_couple.ij X) (k x m) p
-
-  definition k₂ : graded_kernel d →gm D' := graded_submodule_functor k k_lemma1
-
-  lemma k_lemma2 ⦃x : I⦄ (m : E x) (h₁ : lm_kernel (d x) m) (h₂ : image (d ← x) m) :
-    k₂ x ⟨m, h₁⟩ = 0 :=
-  begin
-    assert H₁ : Π⦃x' y z w : I⦄ (p : deg k x' = y) (q : deg j y = z) (r : deg k z = w) (n : E x'),
-      k ↘ r (j ↘ q (k ↘ p n)) = 0,
-    { intros, exact gmod_im_in_ker (exact_couple.jk X) q r (k ↘ p n) },
-    induction h₂ with n p,
-    assert H₂ : k x m = 0,
-    { rewrite [-p], refine ap (k x) (graded_hom_compose_fn_out j k x n) ⬝ _, apply H₁ },
-    exact subtype_eq H₂
-  end
-
-  definition k' : E' →gm D' :=
-  @graded_quotient_elim _ _ _ _ _ _ k₂
-                       (by intro x m h; cases m with [m1, m2]; exact k_lemma2 m1 m2 h)
-
-  open sigma.ops
-  definition i'_eq ⦃x : I⦄ (m : D x) (h : image (i ← x) m) : (i' x ⟨m, h⟩).1 = i x m :=
-  by reflexivity
-
-  definition k'_eq ⦃x : I⦄ (m : E x) (h : d x m = 0) : (k' x (class_of ⟨m, h⟩)).1 = k x m :=
-  by reflexivity
-
-  lemma j'_eq {x : I} (m : D x) : j' ↘ (ap (deg j) (left_inv (deg i) x)) (graded_image_lift i x m) =
-    class_of (graded_hom_lift _ j proof j_lemma1 qed x m) :=
-  begin
-    refine graded_image_elim_destruct _ _ _ idp _ m,
-    apply is_set.elim,
-  end
-
-  definition deg_i' : deg i' ~ deg i := by reflexivity
-  definition deg_j' : deg j' ~ deg j ∘ (deg i)⁻¹ := by reflexivity
-  definition deg_k' : deg k' ~ deg k := by reflexivity
-
-  open group
-  set_option pp.coercions true
-  lemma i'j' : is_exact_gmod i' j' :=
-  begin
-    intro x, refine equiv_rect (deg i) _ _,
-    intros y z p q, revert z q x p,
-    refine eq.rec_grading (deg i ⬝e deg j') (deg j) (ap (deg j) (left_inv (deg i) y)) _,
-    intro x, revert y, refine eq.rec_equiv (deg i) _,
-    apply transport (λx, is_exact_mod x _) (idpath (i' x)),
-    apply transport (λx, is_exact_mod _ (j' ↘ (ap (deg j) (left_inv (deg i) x)))) (idpath x),
-    apply is_exact_mod.mk,
-    { revert x, refine equiv_rect (deg i) _ _, intro x,
-      refine graded_image.rec _, intro m,
-      transitivity j' ↘ _ (graded_image_lift i (deg i x) (i x m)),
-        apply ap (λx, j' ↘ _ x), apply subtype_eq, apply i'_eq,
-      refine !j'_eq ⬝ _,
-      apply ap class_of, apply subtype_eq, exact is_exact.im_in_ker (exact_couple.ij X idp idp) m },
-    { revert x, refine equiv_rect (deg k) _ _, intro x,
-      refine graded_image.rec _, intro m p,
-      assert q : graded_homology_intro d d (deg j (deg k x))
-                   (graded_hom_lift _ j j_lemma1 (deg k x) m) = 0,
-      { exact !j'_eq⁻¹ ⬝ p },
-      note q2 := image_of_graded_homology_intro_eq_zero idp (graded_hom_lift _ j _ _ m) q,
-      induction q2 with n r,
-      assert s : j (deg k x) (m - k x n) = 0,
-      { refine respect_sub (j (deg k x)) m (k x n) ⬝ _,
-        refine ap (sub _) r ⬝ _, apply sub_self },
-      assert t : trunctype.carrier (image (i ← (deg k x)) (m - k x n)),
-      { exact is_exact.ker_in_im (exact_couple.ij X _ _) _ s },
-      refine image.mk ⟨m - k x n, t⟩ _,
-      apply subtype_eq, refine !i'_eq ⬝ !to_respect_sub ⬝ _,
-      refine ap (@sub (D (deg i (deg k x))) _ _) _ ⬝ @sub_zero _ _ _,
-      apply is_exact.im_in_ker (exact_couple.ki X _ _) }
-  end
-
-  lemma j'k' : is_exact_gmod j' k' :=
-  begin
-    refine equiv_rect (deg i) _ _,
-    intros x y z p, revert y p z,
-    refine eq.rec_grading (deg i ⬝e deg j') (deg j) (ap (deg j) (left_inv (deg i) x)) _,
-    intro z q, induction q,
-    apply is_exact_mod.mk,
-    { refine graded_image.rec _, intro m,
-      refine ap (k' _) (j'_eq m) ⬝ _,
-      apply subtype_eq,
-      refine k'_eq _ _ ⬝ _,
-      exact is_exact.im_in_ker (exact_couple.jk X idp idp) m },
-    { intro m p, induction m using set_quotient.rec_prop with m,
-      induction m with m h, note q := (k'_eq m h)⁻¹ ⬝ ap pr1 p,
-      induction is_exact.ker_in_im (exact_couple.jk X idp idp) m q with n r,
-      apply image.mk (graded_image_lift i x n),
-      refine !j'_eq ⬝ _,
-      apply ap class_of, apply subtype_eq, exact r }
-  end
-
-  lemma k'i' : is_exact_gmod k' i' :=
-  begin
-    apply is_exact_gmod.mk,
-    { intro x m, induction m using set_quotient.rec_prop with m,
-      cases m with m p, apply subtype_eq,
-      change i (deg k x) (k x m) = 0,
-      exact is_exact.im_in_ker (exact_couple.ki X idp idp) m },
-    { intro x m, induction m with m h, intro p,
-      have i (deg k x) m = 0, from ap pr1 p,
-      induction is_exact.ker_in_im (exact_couple.ki X idp idp) m this with n q,
-      have j (deg k x) m = 0, from @(is_exact.im_in_ker2 (exact_couple.ij X _ _)) m h,
-      have d x n = 0, from ap (j (deg k x)) q ⬝ this,
-      exact image.mk (class_of ⟨n, this⟩) (subtype_eq q) }
-  end
-
-  end
-  end derived_couple
-
-  open derived_couple
-
-  definition derived_couple [constructor] {R : Ring} {I : AddAbGroup}
-    (X : exact_couple R I) : exact_couple R I :=
-  ⦃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⦄
-
-  /- if an exact couple is bounded, we can prove the convergence theorem for it -/
-  structure is_bounded {R : Ring} {I : AddAbGroup} (X : exact_couple R I) : Type :=
-  mk' :: (B B' : I → ℕ)
-    (Dub : Π⦃x y⦄ ⦃s : ℕ⦄, (deg (i X))^[s] x = y → B x ≤ s → is_contr (D X y))
-    (Dlb : Π⦃x y z⦄ ⦃s : ℕ⦄ (p : deg (i X) x = y), (deg (i X))^[s] y = z → B' z ≤ s →
-      is_surjective (i X ↘ p))
-    (Elb : Π⦃x y⦄ ⦃s : ℕ⦄, (deg (i X))⁻¹ᵉ^[s] x = y → B x ≤ s → is_contr (E X y))
-
-/- Note: Elb proves Dlb for some bound B', but we want tight control over when B' = 0 -/
-  protected definition is_bounded.mk [constructor] {R : Ring} {I : AddAbGroup} {X : exact_couple R I}
-    (B B' B'' : I → ℕ)
-    (Dub : Π⦃x : I⦄ ⦃s : ℕ⦄, B x ≤ s → is_contr (D X ((deg (i X))^[s] x)))
-    (Dlb : Π⦃x : I⦄ ⦃s : ℕ⦄, B' x ≤ s → is_surjective (i X (((deg (i X))⁻¹ᵉ^[s + 1] x))))
-    (Elb : Π⦃x : I⦄ ⦃s : ℕ⦄, B'' x ≤ s → is_contr (E X ((deg (i X))⁻¹ᵉ^[s] x))) : is_bounded X :=
-  begin
-    apply is_bounded.mk' (λx, max (B x) (B'' x)) B',
-    { intro x y s p h, induction p, exact Dub (le.trans !le_max_left h) },
-    { exact abstract begin intro x y z s p q h, induction p, induction q,
-      refine transport (λx, is_surjective (i X x)) _ (Dlb h),
-      rewrite [-iterate_succ], apply iterate_left_inv end end },
-    { intro x y s p h, induction p, exact Elb (le.trans !le_max_right h) }
-  end
-
-  open is_bounded
-  definition is_bounded_reindex [constructor] {R : Ring} {I J : AddAbGroup}
-    (e : AddGroup_of_AddAbGroup J ≃g AddGroup_of_AddAbGroup I)
-    {X : exact_couple R I} (HH : is_bounded X) : is_bounded (exact_couple_reindex e X) :=
-  begin
-    apply is_bounded.mk' (B HH ∘ e) (B' HH ∘ e),
-    { intros x y s p h, refine Dub HH _ h,
-      refine (iterate_hsquare e _ s x)⁻¹ ⬝ ap e p, intro x,
-      exact to_right_inv (group.equiv_of_isomorphism e) _ },
-    { intros x y z s p q h, refine Dlb HH _ _ h,
-      refine (iterate_hsquare e _ s y)⁻¹ ⬝ ap e q, intro x,
-      exact to_right_inv (group.equiv_of_isomorphism e) _ },
-    { intro x y s p h, refine Elb HH _ h,
-      refine (iterate_hsquare e _ s x)⁻¹ ⬝ ap e p, intro x,
-      exact to_right_inv (group.equiv_of_isomorphism e) _ },
-
-  end
-
-  namespace convergence_theorem
-  section
-
-  parameters {R : Ring} {I : AddAbGroup} (X : exact_couple R I) (HH : is_bounded X)
-
-  local abbreviation B := B HH
-  local abbreviation B' := B' HH
-  local abbreviation Dub := Dub HH
-  local abbreviation Dlb := Dlb HH
-  local abbreviation Elb := Elb HH
-
-  /- We start counting pages at 0, which corresponds to what is usually called the second page -/
-  definition page (r : ℕ) : exact_couple R I :=
-  iterate derived_couple r X
-
-  definition is_contr_E (r : ℕ) (x : I) (h : is_contr (E X x)) :
-    is_contr (E (page r) x) :=
-  by induction r with r IH; exact h; exact is_contr_E' (page r) IH
-
-  definition is_contr_D (r : ℕ) (x : I) (h : is_contr (D X x)) :
-    is_contr (D (page r) x) :=
-  by induction r with r IH; exact h; exact is_contr_D' (page r) IH
-
-  definition deg_i (r : ℕ) : deg (i (page r)) ~ deg (i X) :=
-  begin
-    induction r with r IH,
-    { reflexivity },
-    { exact IH }
-  end
-
-  definition deg_k (r : ℕ) : deg (k (page r)) ~ deg (k X) :=
-  begin
-    induction r with r IH,
-    { reflexivity },
-    { exact IH }
-  end
-
-  definition deg_j (r : ℕ) :
-    deg (j (page r)) ~ deg (j X) ∘ iterate (deg (i X))⁻¹ r :=
-  begin
-    induction r with r IH,
-    { reflexivity },
-    { refine hwhisker_left (deg (j (page r)))
-        (to_inv_homotopy_inv (deg_i r)) ⬝hty _,
-      refine hwhisker_right _ IH ⬝hty _,
-      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_inv H x ⬝ iterate_inv (deg (i X))⁻¹ᵉ r ((deg (j X))⁻¹ x)
-
-  definition deg_dr (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_dr_inv (r : ℕ) :
-    (deg (d (page r)))⁻¹ ~ (deg (k X))⁻¹ ∘ iterate (deg (i X)) r ∘ (deg (j X))⁻¹ :=
-  compose2 (to_inv_homotopy_inv (deg_k r)) (deg_j_inv r)
-
-  definition E_isomorphism' {x : I} {r₁ r₂ : ℕ} (H : r₁ ≤ r₂)
-    (H1 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E X ((deg (d (page r)))⁻¹ᵉ x)))
-    (H2 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E X (deg (d (page r)) x))) :
-    E (page r₂) x ≃lm E (page r₁) x :=
-  begin
-    assert H2 : Π⦃r⦄, r₁ ≤ r → r ≤ r₂ → E (page r) x ≃lm E (page r₁) x,
-    { intro r Hr₁ Hr₂,
-      induction Hr₁ with r Hr₁ IH, reflexivity,
-      let Hr₂' := le_of_succ_le Hr₂,
-      exact E'_isomorphism (page r) (is_contr_E r _ (H1 Hr₁ Hr₂)) (is_contr_E r _ (H2 Hr₁ Hr₂))
-        ⬝lm IH Hr₂' },
-    exact H2 H (le.refl _)
-  end
-
-  definition E_isomorphism0' {x : I} {r : ℕ}
-    (H1 : Πr, is_contr (E X ((deg (d (page r)))⁻¹ᵉ x)))
-    (H2 : Πr, is_contr (E X (deg (d (page r)) x))) : E (page r) x ≃lm E X x :=
-  E_isomorphism' (zero_le r) _ _
-
-  parameter {X}
-
-  definition deg_iterate_ik_commute (n : ℕ) :
-    hsquare (deg (k X)) (deg (k X)) ((deg (i X))^[n]) ((deg (i X))^[n]) :=
-  iterate_commute n (deg_commute (k X) (i X))
-
-  definition deg_iterate_ij_commute (n : ℕ) :
-    hsquare (deg (j X)) (deg (j X)) ((deg (i X))⁻¹ᵉ^[n]) ((deg (i X))⁻¹ᵉ^[n]) :=
-  iterate_commute n (deg_commute (j X) (i X))⁻¹ʰᵗʸᵛ
-
-  definition B2 (x : I) : ℕ := max (B (deg (k X) x)) (B ((deg (j X))⁻¹ x))
-  definition Eub ⦃x y : I⦄ ⦃s : ℕ⦄ (p : (deg (i X))^[s] x = y) (h : B2 x ≤ s) :
-    is_contr (E X y) :=
-  begin
-    induction p,
-    refine @(is_contr_middle_of_is_exact (exact_couple.jk X (right_inv (deg (j X)) _) idp)) _ _ _,
-    exact Dub (iterate_commute s (deg_commute (j X) (i X))⁻¹ʰᵗʸʰ x) (le.trans !le_max_right h),
-    exact Dub (deg_iterate_ik_commute s x) (le.trans !le_max_left h)
-  end
-
-  definition B3 (x : I) : ℕ :=
-  max (B (deg (j X) (deg (k X) x))) (B2 ((deg (k X))⁻¹ ((deg (j X))⁻¹ x)))
-
-  definition Estable {x : I} {r : ℕ} (H : B3 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: apply is_contr_E,
-    exact Eub (hhinverse (deg_iterate_ik_commute r) _ ⬝ (deg_dr_inv r x)⁻¹)
-              (le.trans !le_max_right H),
-    exact Elb (deg_iterate_ij_commute r _ ⬝ (deg_dr r x)⁻¹)
-              (le.trans !le_max_left H)
-  end
-
-  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
-    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) :
-    D (page (r + 1)) x ≃lm D (page r) x :=
-  begin
-    change image_module (i (page r) ← x) ≃lm D (page r) x,
-    refine image_module_isomorphism (i (page r) ← x)
-      (is_surjective_i (le.trans H (le_of_eq !zero_add⁻¹)) _ _),
-    reflexivity
-  end
-
-  /- the infinity pages of E and D -/
-  definition Einf : graded_module R I :=
-  λx, E (page (B3 x)) x
-
-  definition Dinf : graded_module R I :=
-  λx, D (page (B' x)) x
-
-  definition Einfstable {x y : I} {r : ℕ} (Hr : B3 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
-
-  definition Einf_isomorphism' {x : I} (r₁ : ℕ)
-    (H1 : Π⦃r⦄, r₁ ≤ r → is_contr (E X ((deg (d (page r)))⁻¹ᵉ x)))
-    (H2 : Π⦃r⦄, r₁ ≤ r → is_contr (E X (deg (d (page r)) x))) :
-    Einf x ≃lm E (page r₁) x :=
-  begin
-    cases le.total r₁ (B3 x) with Hr Hr,
-    exact E_isomorphism' Hr (λr Hr₁ Hr₂, H1 Hr₁) (λr Hr₁ Hr₂, H2 Hr₁),
-    exact Einfstable Hr idp
-  end
-
-  definition Einf_isomorphism0' {x : I}
-    (H1 : Π⦃r⦄, is_contr (E X ((deg (d (page r)))⁻¹ᵉ x)))
-    (H2 : Π⦃r⦄, is_contr (E X (deg (d (page r)) x))) :
-    Einf x ≃lm E X x :=
-  E_isomorphism0' _ _
-
-  parameters (x : I)
-
-  definition rb (n : ℕ) : ℕ :=
-  max (max (B (deg (j X) (deg (k X) x)) + n + 1) (B3 ((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 : ℕ) : rb n ≥ n + 1 :=
-  ge.trans !le_max_left (ge.trans !le_max_left !le_add_left)
-  lemma rb1 (n : ℕ) : B (deg (j X) (deg (k X) x)) ≤ rb n - (n + 1) :=
-  nat.le_sub_of_add_le (le.trans !le_max_left !le_max_left)
-  lemma rb2 (n : ℕ) : B3 ((deg (i X))^[n] x) ≤ rb n :=
-  le.trans !le_max_right !le_max_left
-  lemma rb3 (n : ℕ) : B' (deg (k X) ((deg (i X))^[n] x)) ≤ rb n :=
-  le.trans !le_max_left !le_max_right
-  lemma rb4 (n : ℕ) : B' (deg (k X) ((deg (i X))^[n+1] x)) ≤ rb 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)) ≤ rb 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))
-
-  definition short_exact_mod_page_r (n : ℕ) : short_exact_mod
-    (E (page (rb n)) ((deg (i X))^[n] x))
-    (D (page (rb n)) (deg (k (page (rb n))) ((deg (i X))^[n] x)))
-    (D (page (rb n)) (deg (i (page (rb n))) (deg (k (page (rb n))) ((deg (i X))^[n] x)))) :=
-  begin
-    fapply short_exact_mod_of_is_exact,
-    { exact j (page (rb n)) ← ((deg (i X))^[n] x) },
-    { exact k (page (rb n)) ((deg (i X))^[n] x) },
-    { exact i (page (rb n)) (deg (k (page (rb n))) ((deg (i X))^[n] x)) },
-    { exact j (page (rb n)) _ },
-    { apply is_contr_D, refine Dub !deg_j_inv⁻¹ (rb5 n) },
-    { apply is_contr_E, refine Elb _ (rb1 n),
-      refine !deg_iterate_ij_commute ⬝ _,
-      refine ap (deg (j X)) _ ⬝ !deg_j⁻¹,
-      refine iterate_sub _ !rb0 _ ⬝ _, apply ap (_^[rb n]),
-      exact ap (deg (i X)) (!deg_iterate_ik_commute ⬝ !deg_k⁻¹) ⬝ !deg_i⁻¹ },
-    { apply jk (page (rb n)) },
-    { apply ki (page (rb n)) },
-    { apply ij (page (rb 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_commute (k X) (i X) _) }
-  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
-
-  lemma Dinfdiag_stable {s : ℕ} (h : B (deg (k X) x) ≤ s) : is_contr (Dinfdiag s) :=
-  is_contr_D _ _ (Dub !deg_iterate_ik_commute h)
-
-  /- some useful immediate properties -/
-
-  definition short_exact_mod_infpage0 (bound_zero : B' (deg (k X) x) = 0) :
-    short_exact_mod (Einfdiag 0) (D X (deg (k X) x)) (Dinfdiag 1) :=
-  begin
-    refine short_exact_mod_isomorphism _ _ _ (short_exact_mod_infpage 0),
-    { reflexivity },
-    { exact (Dinfdiag0 bound_zero)⁻¹ˡᵐ },
-    { reflexivity }
-  end
-
-  /- the convergence theorem is the following result -/
-  definition is_built_from_infpage (bound_zero : B' (deg (k X) x) = 0) :
-    is_built_from (D X (deg (k X) x)) Einfdiag :=
-  is_built_from.mk Dinfdiag short_exact_mod_infpage (Dinfdiag0 bound_zero) (B (deg (k X) x))
-    (λs, Dinfdiag_stable)
-
-  end
-
-  definition deg_dr_reindex {R : Ring} {I J : AddAbGroup}
-    (e : AddGroup_of_AddAbGroup J ≃g AddGroup_of_AddAbGroup I) (X : exact_couple R I)
-    (r : ℕ) : deg (d (page (exact_couple_reindex e X) r)) ~
-    e⁻¹ᵍ ∘ deg (d (page X r)) ∘ e :=
-  begin
-    intro x, refine !deg_dr ⬝ _ ⬝ ap e⁻¹ᵍ !deg_dr⁻¹,
-    apply ap (e⁻¹ᵍ ∘ deg (j X)),
-    note z := @iterate_hsquare _ _ (deg (i (exact_couple_reindex e X)))⁻¹ᵉ (deg (i X))⁻¹ᵉ e
-      (λx, proof to_right_inv (group.equiv_of_isomorphism e) _ qed)⁻¹ʰᵗʸʰ r,
-    refine z _ ⬝ _, apply ap ((deg (i X))⁻¹ᵉ^[r]),
-    exact to_right_inv (group.equiv_of_isomorphism e) _
-  end
-
-  end convergence_theorem
-
-  open int group prod convergence_theorem prod.ops
-
-  definition Z2 [constructor] : AddAbGroup := agℤ ×aa agℤ
-
-  structure convergent_exact_couple.{u v w} {R : Ring} (E' : agℤ → agℤ → LeftModule.{u v} R)
-                                 (Dinf : agℤ → LeftModule.{u w} R) : Type.{max u (v+1) (w+1)} :=
-    (X : exact_couple.{u 0 w v} R Z2)
-    (HH : is_bounded X)
-    (st : agℤ → Z2)
-    (HB : Π(n : agℤ), is_bounded.B' HH (deg (k X) (st n)) = 0)
-    (e : Π(x : Z2), exact_couple.E X x ≃lm E' x.1 x.2)
-    (f : Π(n : agℤ), exact_couple.D X (deg (k X) (st n)) ≃lm Dinf n)
-    (deg_d : ℕ → Z2)
-    (deg_d_eq0 : Π(r : ℕ), deg (d (page X r)) 0 = deg_d r)
-
-  structure convergent_spectral_sequence.{u v w} {R : Ring} (E' : agℤ → agℤ → LeftModule.{u v} R)
-                                 (Dinf : agℤ → LeftModule.{u w} R) : Type.{max u (v+1) (w+1)} :=
-    (E : ℕ → graded_module.{u 0 v} R Z2)
-    (d : Π(r : ℕ), E r →gm E r)
-    (deg_d : ℕ → Z2)
-    (deg_d_eq0 : Π(r : ℕ), deg (d r) 0 = deg_d r)
-    (α : Π(r : ℕ) (x : Z2), E (r+1) x ≃lm graded_homology (d r) (d r) x)
-    (e : Π(x : Z2), E 0 x ≃lm E' x.1 x.2)
-    (s₀ : Z2 → ℕ)
-    (f : Π{r : ℕ} {x : Z2} (h : s₀ x ≤ r), E (s₀ x) x ≃lm E r x)
-    (lb : ℤ → ℤ)
-    (HDinf : Π(n : agℤ), is_built_from (Dinf n)
-                                       (λ(k : ℕ), (λx, E (s₀ x) x) (n - (k + lb n), k + lb n)))
-
-  infix ` ⟹ `:25 := convergent_exact_couple -- todo: maybe this should define convergent_spectral_sequence
-
-  definition convergent_exact_couple_g [reducible] (E' : agℤ → agℤ → AbGroup) (Dinf : agℤ → AbGroup) : Type :=
-  (λn s, LeftModule_int_of_AbGroup (E' n s)) ⟹ (λn, LeftModule_int_of_AbGroup (Dinf n))
-
-  definition convergent_spectral_sequence_g [reducible] (E' : agℤ → agℤ → AbGroup) (Dinf : agℤ → AbGroup) :
-    Type :=
-  convergent_spectral_sequence (λn s, LeftModule_int_of_AbGroup (E' n s))
-                               (λn, LeftModule_int_of_AbGroup (Dinf n))
-
-  infix ` ⟹ᵍ `:25 := convergent_exact_couple_g
-
-  section
-  open convergent_exact_couple
-  parameters {R : Ring} {E' : agℤ → agℤ → LeftModule R} {Dinf : agℤ → LeftModule R} (c : E' ⟹ Dinf)
-  local abbreviation X := X c
-  local abbreviation i := i X
-  local abbreviation HH := HH c
-  local abbreviation st := st c
-  local abbreviation Dinfdiag (n : agℤ) (k : ℕ) := Dinfdiag HH (st n) k
-  local abbreviation Einfdiag (n : agℤ) (k : ℕ) := Einfdiag HH (st n) k
-
-  definition deg_d_eq (r : ℕ) (ns : Z2) : (deg (d (page X r))) ns = ns + deg_d c r :=
-  !deg_eq ⬝ ap (λx, _ + x) (deg_d_eq0 c r)
-
-  definition deg_d_inv_eq (r : ℕ) (ns : Z2) :
-    (deg (d (page X r)))⁻¹ᵉ ns = ns - deg_d c r :=
-  inv_eq_of_eq (!deg_d_eq ⬝ proof !neg_add_cancel_right qed)⁻¹
-
-  definition convergent_exact_couple_isomorphism {E'' : agℤ → agℤ → LeftModule R} {Dinf' : graded_module R agℤ}
-    (e' : Πn s, E' n s ≃lm E'' n s) (f' : Πn, Dinf n ≃lm Dinf' n) : E'' ⟹ Dinf' :=
-  convergent_exact_couple.mk X HH st (HB c)
-    begin intro x, induction x with n s, exact e c (n, s) ⬝lm e' n s end
-    (λn, f c n ⬝lm f' n) (deg_d c) (deg_d_eq0 c)
-
-  include c
-  definition convergent_exact_couple_reindex (i : agℤ ×ag agℤ ≃g agℤ ×ag agℤ) :
-    (λp q, E' (i (p, q)).1 (i (p, q)).2) ⟹ Dinf :=
-  begin
-    fapply convergent_exact_couple.mk (exact_couple_reindex i X) (is_bounded_reindex i HH),
-    { exact λn, i⁻¹ᵍ (st n) },
-    { intro n, refine ap (B' HH) _ ⬝ HB c n,
-      refine to_right_inv (group.equiv_of_isomorphism i) _ ⬝ _,
-      apply ap (deg (k X)), exact to_right_inv (group.equiv_of_isomorphism i) _ },
-    { intro x, induction x with p q, exact e c (i (p, q)) },
-    { intro n, refine _ ⬝lm f c n, refine isomorphism_of_eq (ap (D X) _),
-      refine to_right_inv (group.equiv_of_isomorphism i) _ ⬝ _,
-      apply ap (deg (k X)), exact to_right_inv (group.equiv_of_isomorphism i) _ },
-    { exact λn, i⁻¹ᵍ (deg_d c n) },
-    { intro r, esimp, refine !deg_dr_reindex ⬝ ap i⁻¹ᵍ (ap (deg (d _)) (group.to_respect_zero i) ⬝
-        deg_d_eq0 c r) }
-  end
-
-  definition convergent_exact_couple_negate_abutment : E' ⟹ (λn, Dinf (-n)) :=
-  convergent_exact_couple.mk X HH (st ∘ neg) (λn, HB c (-n)) (e c) (λn, f c (-n))
-                             (deg_d c) (deg_d_eq0 c)
-  omit c
-
-  definition is_built_from_of_convergent_exact_couple (n : ℤ) : is_built_from (Dinf n) (Einfdiag n) :=
-  is_built_from_isomorphism_left (f c n) (is_built_from_infpage HH (st n) (HB c n))
-
-  /- TODO: reprove this using is_built_of -/
-  theorem is_contr_convergent_exact_couple_precise (n : agℤ)
-  (H : Π(n : agℤ) (l : ℕ), is_contr (E' ((deg i)^[l] (st n)).1 ((deg i)^[l] (st n)).2)) :
-    is_contr (Dinf n) :=
-  begin
-    assert H2 : Π(l : ℕ), is_contr (Einfdiag n l),
-    { intro l, apply is_contr_E,
-      refine is_trunc_equiv_closed_rev -2 (equiv_of_isomorphism (e c _)) (H n l) },
-    assert H3 : is_contr (Dinfdiag n 0),
-    { fapply nat.rec_down (λk, is_contr (Dinfdiag n k)),
-      { exact is_bounded.B HH (deg (k X) (st n)) },
-      { apply Dinfdiag_stable, reflexivity },
-      { intro l H,
-        exact is_contr_middle_of_short_exact_mod (short_exact_mod_infpage HH (st n) l)
-                (H2 l) H }},
-    refine is_trunc_equiv_closed _ _ H3,
-    exact equiv_of_isomorphism (Dinfdiag0 HH (st n) (HB c n) ⬝lm f c n)
-  end
-
-  theorem is_contr_convergent_exact_couple (n : agℤ) (H : Π(n s : agℤ), is_contr (E' n s)) : is_contr (Dinf n) :=
-  is_contr_convergent_exact_couple_precise n (λn s, !H)
-
-  definition E_isomorphism {r₁ r₂ : ℕ} {n s : agℤ} (H : r₁ ≤ r₂)
-    (H1 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E X ((n, s) - deg_d c r)))
-    (H2 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E X ((n, s) + deg_d c r))) :
-    E (page X r₂) (n, s) ≃lm E (page X r₁) (n, s) :=
-  E_isomorphism' X H
-    (λr Hr₁ Hr₂, transport (is_contr ∘ E X) (deg_d_inv_eq r (n, s))⁻¹ᵖ (H1 Hr₁ Hr₂))
-    (λr Hr₁ Hr₂, transport (is_contr ∘ E X) (deg_d_eq r (n, s))⁻¹ᵖ (H2 Hr₁ Hr₂))
-
-  definition E_isomorphism0 {r : ℕ} {n s : agℤ} (H1 : Πr, is_contr (E X ((n, s) - deg_d c r)))
-    (H2 : Πr, is_contr (E X ((n, s) + deg_d c r))) : E (page X r) (n, s) ≃lm E' n s :=
-  E_isomorphism (zero_le r) _ _ ⬝lm e c (n, s)
-
-  definition Einf_isomorphism (r₁ : ℕ) {n s : agℤ}
-    (H1 : Π⦃r⦄, r₁ ≤ r → is_contr (E X ((n,s) - deg_d c r)))
-    (H2 : Π⦃r⦄, r₁ ≤ r → is_contr (E X ((n,s) + deg_d c r))) :
-    Einf HH (n, s) ≃lm E (page X r₁) (n, s) :=
-  Einf_isomorphism' HH r₁ (λr Hr₁, transport (is_contr ∘ E X) (deg_d_inv_eq r (n, s))⁻¹ᵖ (H1 Hr₁))
-                         (λr Hr₁, transport (is_contr ∘ E X) (deg_d_eq r (n, s))⁻¹ᵖ (H2 Hr₁))
-
-  definition Einf_isomorphism0 {n s : agℤ}
-    (H1 : Π⦃r⦄, is_contr (E X ((n,s) - deg_d c r)))
-    (H2 : Π⦃r⦄, is_contr (E X ((n,s) + deg_d c r))) :
-    Einf HH (n, s) ≃lm E' n s :=
-  E_isomorphism0 _ _
-
-  definition convergent_spectral_sequence_of_exact_couple
-    (st_eq : Πn, (st n).1 + (st n).2 = n) (deg_i_eq : deg i 0 = (-(1 : ℤ), (1 : ℤ))) :
+     left_module group int prod prod.ops
+open exact_couple (Z2)
+
+structure convergent_spectral_sequence.{u v w} {R : Ring} (E' : agℤ → agℤ → LeftModule.{u v} R)
+                               (Dinf : agℤ → LeftModule.{u w} R) : Type.{max u (v+1) (w+1)} :=
+  (E : ℕ → graded_module.{u 0 v} R Z2)
+  (d : Π(r : ℕ), E r →gm E r)
+  (deg_d : ℕ → Z2)
+  (deg_d_eq0 : Π(r : ℕ), deg (d r) 0 = deg_d r)
+  (α : Π(r : ℕ) (x : Z2), E (r+1) x ≃lm graded_homology (d r) (d r) x)
+  (e : Π(x : Z2), E 0 x ≃lm E' x.1 x.2)
+  (s₀ : Z2 → ℕ)
+  (f : Π{r : ℕ} {x : Z2} (h : s₀ x ≤ r), E (s₀ x) x ≃lm E r x)
+  (lb : ℤ → ℤ)
+  (HDinf : Π(n : agℤ), is_built_from (Dinf n)
+                                     (λ(k : ℕ), (λx, E (s₀ x) x) (n - (k + lb n), k + lb n)))
+
+definition convergent_spectral_sequence_g [reducible] (E' : agℤ → agℤ → AbGroup)
+  (Dinf : agℤ → AbGroup) : Type :=
+convergent_spectral_sequence (λn s, LeftModule_int_of_AbGroup (E' n s))
+                             (λn, LeftModule_int_of_AbGroup (Dinf n))
+
+  section exact_couple
+  open exact_couple exact_couple.exact_couple exact_couple.convergent_exact_couple
+       exact_couple.convergence_theorem exact_couple.derived_couple
+
+  definition convergent_spectral_sequence_of_exact_couple {R : Ring} {E' : agℤ → agℤ → LeftModule R}
+    {Dinf : agℤ → LeftModule R} (c : convergent_exact_couple E' Dinf)
+    (st_eq : Πn, (st c n).1 + (st c n).2 = n) (deg_i_eq : deg (i (X c)) 0 = (-(1 : ℤ), (1 : ℤ))) :
     convergent_spectral_sequence E' Dinf :=
-  convergent_spectral_sequence.mk (λr, E (page X r)) (λr, d (page X r)) (deg_d c) (deg_d_eq0 c)
-    (λr ns, by reflexivity) (e c) (B3 HH) (λr ns Hr, Einfstable HH Hr idp)
-    (λn, (st n).2)
+  convergent_spectral_sequence.mk (λr, E (page (X c) r)) (λr, d (page (X c) r))
+    (deg_d c) (deg_d_eq0 c)
+    (λr ns, by reflexivity) (e c) (B3 (HH c)) (λr ns Hr, Einfstable (HH c) Hr idp)
+    (λn, (st c n).2)
     begin
       intro n,
-      refine is_built_from_isomorphism (f c n) _ (is_built_from_infpage HH (st n) (HB c n)),
-      intro p, apply isomorphism_of_eq, apply ap (λx, E (page X (B3 HH x)) x),
+      refine is_built_from_isomorphism (f c n) _ (is_built_from_infpage (HH c) (st c n) (HB c n)),
+      intro p, apply isomorphism_of_eq, apply ap (λx, E (page (X c) (B3 (HH c) x)) x),
       induction p with p IH,
-      { exact !prod.eta⁻¹ ⬝ prod_eq (eq_sub_of_add_eq (ap (add _) !zero_add ⬝ st_eq n)) (zero_add (st n).2)⁻¹ },
+      { exact !prod.eta⁻¹ ⬝ prod_eq (eq_sub_of_add_eq (ap (add _) !zero_add ⬝ st_eq n))
+                                    (zero_add (st c n).2)⁻¹ },
       { assert H1 : Π(a : ℤ), n - (p + a) - (1 : ℤ) = n - (succ p + a),
         exact λa, !sub_add_eq_sub_sub⁻¹ ⬝ ap (sub n) (add_comm_middle p a (1 : ℤ) ⬝ proof idp qed),
         assert H2 : Π(a : ℤ), p + a + 1 = succ p + a,
         exact λa, add_comm_middle p a 1,
-        refine ap (deg i) IH ⬝ !deg_eq ⬝ ap (add _) deg_i_eq ⬝ prod_eq !H1 !H2 }
+        refine ap (deg (i (X c))) IH ⬝ !deg_eq ⬝ ap (add _) deg_i_eq ⬝ prod_eq !H1 !H2 }
     end
-  end
+    end exact_couple
 
-  variables {E' : agℤ → agℤ → AbGroup} {Dinf : agℤ → AbGroup}
-  definition convergent_exact_couple_g_isomorphism {E'' : agℤ → agℤ → AbGroup}
-    {Dinf' : agℤ → AbGroup} (c : E' ⟹ᵍ Dinf)
-    (e' : Πn s, E' n s ≃g E'' n s) (f' : Πn, Dinf n ≃g Dinf' n) : E'' ⟹ᵍ Dinf' :=
-  convergent_exact_couple_isomorphism c (λn s, lm_iso_int.mk (e' n s)) (λn, lm_iso_int.mk (f' n))
+namespace spectral_sequence
+  open convergent_spectral_sequence
 
+  variables {R : Ring} {E' : agℤ → agℤ → LeftModule R} {Dinf : agℤ → LeftModule R}
+    (c : convergent_spectral_sequence E' Dinf)
 
-end left_module
-open left_module
-namespace pointed
+    -- (E : ℕ → graded_module.{u 0 v} R Z2)
+    -- (d : Π(r : ℕ), E r →gm E r)
+    -- (deg_d : ℕ → Z2)
+    -- (deg_d_eq0 : Π(r : ℕ), deg (d r) 0 = deg_d r)
+    -- (α : Π(r : ℕ) (x : Z2), E (r+1) x ≃lm graded_homology (d r) (d r) x)
+    -- (e : Π(x : Z2), E 0 x ≃lm E' x.1 x.2)
+    -- (s₀ : Z2 → ℕ)
+    -- (f : Π{r : ℕ} {x : Z2} (h : s₀ x ≤ r), E (s₀ x) x ≃lm E r x)
+    -- (lb : ℤ → ℤ)
+    -- (HDinf : Π(n : agℤ), is_built_from (Dinf n)
+    --                                    (λ(k : ℕ), (λx, E (s₀ x) x) (n - (k + lb n), k + lb n)))
 
-  open pointed int group is_trunc trunc is_conn
+  definition Einf (x : Z2) : LeftModule R := E c (s₀ c x) x
 
-  definition homotopy_group_conn_nat (n : ℕ) (A : Type*[1]) : AbGroup :=
-  AbGroup.mk (π[n] A) (ab_group_homotopy_group_of_is_conn n A)
+  definition is_contr_E_succ (r : ℕ) (x : Z2) (h : is_contr (E c r x)) : is_contr (E c (r+1) x) :=
+  is_contr_equiv_closed_rev (equiv_of_isomorphism (α c r x)) (is_contr_homology _ _ _)
 
-  definition homotopy_group_conn : Π(n : ℤ) (A : Type*[1]), AbGroup
-  | (of_nat n) A := homotopy_group_conn_nat n A
-  | (-[1+ n])  A := trivial_ab_group_lift
+  definition deg_d_eq (r : ℕ) (x : Z2) : deg (d c r) x = x + deg_d c r :=
+  !deg_eq ⬝ ap (add _) !deg_d_eq0
 
-  notation `πc[`:95 n:0 `]`:0 := homotopy_group_conn n
+  definition deg_d_inv_eq (r : ℕ) (x : Z2) : (deg (d c r))⁻¹ᵉ x = x - deg_d c r :=
+  inv_eq_of_eq (!deg_d_eq ⬝ !neg_add_cancel_right)⁻¹
 
-  definition homotopy_group_conn_nat_functor (n : ℕ) {A B : Type*[1]} (f : A →* B) :
-    homotopy_group_conn_nat n A →g homotopy_group_conn_nat n B :=
+  definition is_contr_E_of_le {r₁ r₂ : ℕ} (H : r₁ ≤ r₂) (x : Z2) (h : is_contr (E c r₁ x)) :
+    is_contr (E c r₂ x) :=
   begin
-    cases n with n, { apply trivial_homomorphism },
-    cases n with n, { apply trivial_homomorphism },
-    exact π→g[n+2] f
+    induction H with r₂ H IH,
+    { exact h },
+    { apply is_contr_E_succ, exact IH }
   end
 
-  definition homotopy_group_conn_functor :
-    Π(n : ℤ) {A B : Type*[1]} (f : A →* B), πc[n] A →g πc[n] B
-  | (of_nat n) A B f := homotopy_group_conn_nat_functor n f
-  | (-[1+ n])  A B f := trivial_homomorphism _ _
+  definition is_contr_E (r : ℕ) (x : Z2) (h : is_contr (E' x.1 x.2)) : is_contr (E c r x) :=
+  is_contr_E_of_le c !zero_le x (is_contr_equiv_closed_rev (equiv_of_isomorphism (e c x)) h)
 
-  notation `π→c[`:95 n:0 `]`:0 := homotopy_group_conn_functor n
+  definition is_contr_Einf (x : Z2) (h : is_contr (E' x.1 x.2)) : is_contr (Einf c x) :=
+  is_contr_E c (s₀ c x) x h
 
-  section
-  open prod prod.ops fiber
-  parameters {A : ℤ → Type*[1]} (f : Π(n : ℤ), A n →* A (n - 1)) [Hf : Πn, is_conn_fun 1 (f n)]
-  include Hf
-  local abbreviation I [constructor] := Z2
-
-  -- definition D_sequence : graded_module rℤ I :=
-  -- λv, LeftModule_int_of_AbGroup (πc[v.2] (A (v.1)))
-
-  -- definition E_sequence : graded_module rℤ I :=
-  -- λv, LeftModule_int_of_AbGroup (πc[v.2] (pconntype.mk (pfiber (f (v.1))) !Hf pt))
-
-  /- first need LES of these connected homotopy groups -/
-
-  -- definition exact_couple_sequence : exact_couple rℤ I :=
-  -- exact_couple.mk D_sequence E_sequence sorry sorry sorry sorry sorry sorry
-
-  end
-
-
-end pointed
-
-namespace spectrum
-  open pointed int group is_trunc trunc is_conn prod prod.ops group fin chain_complex
-  section
-
-  parameters {A : ℤ → spectrum} (f : Π(s : ℤ), A s →ₛ A (s - 1))
-
-  local abbreviation I [constructor] := Z2
-
-  definition D_sequence : graded_module rℤ I :=
-  λv, LeftModule_int_of_AbGroup (πₛ[v.1] (A (v.2)))
-
-  definition E_sequence : graded_module rℤ I :=
-  λv, LeftModule_int_of_AbGroup (πₛ[v.1] (sfiber (f (v.2))))
-
-  include f
-
-  definition i_sequence : D_sequence →gm D_sequence :=
+  definition E_isomorphism {r₁ r₂ : ℕ} {ns : Z2} (H : r₁ ≤ r₂)
+    (H1 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E c r (ns - deg_d c r)))
+    (H2 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E c r (ns + deg_d c r))) :
+    E c r₂ ns ≃lm E c r₁ ns :=
   begin
-    fapply graded_hom.mk, exact (prod_equiv_prod erfl (add_right_action (- (1 : ℤ)))),
-    { intro i, exact pair_eq !add_zero⁻¹ idp },
-    intro v,
-    apply lm_hom_int.mk, esimp,
-    rexact πₛ→[v.1] (f v.2)
+    assert H3 : Π⦃r⦄, r₁ ≤ r → r ≤ r₂ → E c r ns ≃lm E c r₁ ns,
+    { intro r Hr₁ Hr₂,
+      induction Hr₁ with r Hr₁ IH, reflexivity,
+      let Hr₂' := le_of_succ_le Hr₂,
+      refine α c r ns  ⬝lm homology_isomorphism _ _ _ _ ⬝lm IH Hr₂',
+      exact is_contr_equiv_closed (equiv_ap (E c r) !deg_d_inv_eq⁻¹) (H1 Hr₁ Hr₂),
+      exact is_contr_equiv_closed (equiv_ap (E c r) !deg_d_eq⁻¹) (H2 Hr₁ Hr₂) },
+    exact H3 H (le.refl _)
   end
 
-  definition deg_j_seq_inv [constructor] : I ≃ I :=
-  prod_equiv_prod (add_right_action (1 : ℤ)) (add_right_action (- (1 : ℤ)))
+  definition E_isomorphism0 {r : ℕ} {n s : agℤ}
+    (H1 : Πr', r' < r → is_contr (E' (n - (deg_d c r').1) (s - (deg_d c r').2)))
+    (H2 : Πr', r' < r → is_contr (E' (n + (deg_d c r').1) (s + (deg_d c r').2))) :
+    E c r (n, s) ≃lm E' n s :=
+  E_isomorphism c !zero_le (λr' Hr₁ Hr₂, is_contr_E c r' _ (H1 r' Hr₂))
+   (λr' Hr₁ Hr₂, is_contr_E c r' _ (H2 r' Hr₂)) ⬝lm
+  e c (n, s)
 
-  definition fn_j_sequence [unfold 3] (x : I) :
-    D_sequence (deg_j_seq_inv x) →lm E_sequence x :=
+  definition Einf_isomorphism (r₁ : ℕ) {ns : Z2}
+    (H1 : Π⦃r⦄, r₁ ≤ r → is_contr (E c r (ns - deg_d c r)))
+    (H2 : Π⦃r⦄, r₁ ≤ r → is_contr (E c r (ns + deg_d c r))) :
+    Einf c ns ≃lm E c r₁ ns :=
   begin
-    induction x with n s,
-    apply lm_hom_int.mk, esimp,
-    rexact shomotopy_groups_fun (f s) (n, 2)
+    cases le.total r₁ (s₀ c ns) with Hr Hr,
+    exact E_isomorphism c Hr (λr Hr₁ Hr₂, H1 Hr₁) (λr Hr₁ Hr₂, H2 Hr₁),
+    exact f c Hr
   end
 
-  definition j_sequence : D_sequence →gm E_sequence :=
-  graded_hom.mk_out deg_j_seq_inv⁻¹ᵉ (λi, idp) fn_j_sequence
+  definition Einf_isomorphism0 {n s : agℤ}
+    (H1 : Πr, is_contr (E' (n - (deg_d c r).1) (s - (deg_d c r).2)))
+    (H2 : Πr, is_contr (E' (n + (deg_d c r).1) (s + (deg_d c r).2))) :
+    Einf c (n, s) ≃lm E' n s :=
+  E_isomorphism0 c (λr Hr, H1 r) (λr Hr, H2 r)
 
-  definition k_sequence : E_sequence →gm D_sequence :=
-  begin
-    fapply graded_hom.mk erfl deg_eq_id,
-    intro v, induction v with n s,
-    apply lm_hom_int.mk, esimp,
-    exact πₛ→[n] (spoint (f s))
-  end
 
-  lemma ij_sequence : is_exact_gmod i_sequence j_sequence :=
-  begin
-    intro x y z p q,
-    revert y z q p,
-    refine eq.rec_right_inv (deg j_sequence) _,
-    intro y, induction x with n s, induction y with m t,
-    refine equiv_rect !pair_eq_pair_equiv⁻¹ᵉ _ _,
-    intro pq, esimp at pq, induction pq with p q,
-    revert t q, refine eq.rec_equiv (add_right_action (-(1 : ℤ))) _,
-    induction p using eq.rec_symm,
-    apply is_exact_homotopy homotopy.rfl,
-    { symmetry, exact graded_hom_mk_out_destruct deg_j_seq_inv⁻¹ᵉ (λi, idp) fn_j_sequence },
-    rexact is_exact_of_is_exact_at (is_exact_LES_of_shomotopy_groups (f s) (m, 2)),
-  end
-
-  lemma jk_sequence : is_exact_gmod j_sequence k_sequence :=
-  begin
-    intro x y z p q, induction q,
-    revert x y p, refine eq.rec_right_inv (deg j_sequence) _,
-    intro x, induction x with n s,
-    apply is_exact_homotopy,
-    { symmetry, exact graded_hom_mk_out_destruct deg_j_seq_inv⁻¹ᵉ (λi, idp) fn_j_sequence },
-    { reflexivity },
-    rexact is_exact_of_is_exact_at (is_exact_LES_of_shomotopy_groups (f s) (n, 1)),
-  end
-
-  lemma ki_sequence : is_exact_gmod k_sequence i_sequence :=
-  begin
-    intro i j k p q, induction p, induction q, induction i with n s,
-    rexact is_exact_of_is_exact_at (is_exact_LES_of_shomotopy_groups (f s) (n, 0)),
-  end
-
-  definition exact_couple_sequence [constructor] : exact_couple rℤ I :=
-  exact_couple.mk D_sequence E_sequence i_sequence j_sequence k_sequence
-                  ij_sequence jk_sequence ki_sequence
-
-  open int
-  parameters (ub : ℤ → ℤ) (lb : ℤ → ℤ)
-    (Aub : Π(s n : ℤ), s ≥ ub n + (1 : ℤ) → is_equiv (πₛ→[n] (f s)))
-    (Alb : Π(s n : ℤ), s ≤ lb n → is_contr (πₛ[n] (A s)))
-
-  definition B : I → ℕ
-  | (n, s) := max0 (s - lb n)
-
-  definition B' : I → ℕ
-  | (n, s) := max0 (ub n - s)
-
-  definition B'' : I → ℕ
-  | (n, s) := max0 (max (ub n + (1 : ℤ) - s) (ub (n+(1 : ℤ)) + (1 : ℤ) - s))
-
-  lemma iterate_deg_i (n s : ℤ) (m : ℕ) : (deg i_sequence)^[m] (n, s) = (n, s - m) :=
-  begin
-    induction m with m IH,
-    { exact prod_eq idp !sub_zero⁻¹ },
-    { exact ap (deg i_sequence) IH ⬝ (prod_eq idp !sub_sub) }
-  end
-
-  lemma iterate_deg_i_inv (n s : ℤ) (m : ℕ) : (deg i_sequence)⁻¹ᵉ^[m] (n, s) = (n, s + m) :=
-  begin
-    induction m with m IH,
-    { exact prod_eq idp !add_zero⁻¹ },
-    { exact ap (deg i_sequence)⁻¹ᵉ IH ⬝ (prod_eq idp !add.assoc) }
-  end
-
-  include Aub Alb
-  lemma Dub ⦃x : I⦄ ⦃t : ℕ⦄ (h : B x ≤ t) : is_contr (D_sequence ((deg i_sequence)^[t] x)) :=
-  begin
-    apply Alb, induction x with n s, rewrite [iterate_deg_i],
-    apply sub_le_of_sub_le,
-    exact le_of_max0_le h,
-  end
-
-  lemma Dlb ⦃x : I⦄ ⦃t : ℕ⦄ (h : B' x ≤ t) :
-    is_surjective (i_sequence ((deg i_sequence)⁻¹ᵉ^[t+1] x)) :=
-  begin
-    apply is_surjective_of_is_equiv,
-    apply Aub, induction x with n s,
-    rewrite [iterate_deg_i_inv, ▸*, of_nat_add, -add.assoc],
-    apply add_le_add_right,
-    apply le_add_of_sub_left_le,
-    exact le_of_max0_le h
-  end
-
-  lemma Elb ⦃x : I⦄ ⦃t : ℕ⦄ (h : B'' x ≤ t) : is_contr (E_sequence ((deg i_sequence)⁻¹ᵉ^[t] x)) :=
-  begin
-    induction x with n s,
-    rewrite [iterate_deg_i_inv, ▸*],
-    apply is_contr_shomotopy_group_sfiber_of_is_equiv,
-    apply Aub, apply le_add_of_sub_left_le, apply le_of_max0_le, refine le.trans _ h,
-    apply max0_monotone, apply le_max_left,
-    apply Aub, apply le_add_of_sub_left_le, apply le_of_max0_le, refine le.trans _ h,
-    apply max0_monotone, apply le_max_right
-  end
-
-  definition is_bounded_sequence [constructor] : is_bounded exact_couple_sequence :=
-  is_bounded.mk B B' B'' Dub Dlb Elb
-    -- (by intro x; reflexivity)
-    -- begin
-    --   intro x, induction x with n s, apply pair_eq, esimp, esimp, esimp [j_sequence, i_sequence],
-    --   refine !add.assoc ⬝ ap (add s) !add.comm ⬝ !add.assoc⁻¹,
-    -- end
-
-  definition convergent_exact_couple_sequence : (λn s, πₛ[n] (sfiber (f s))) ⟹ᵍ (λn, πₛ[n] (A (ub n))) :=
-  begin
-    fapply convergent_exact_couple.mk,
-    { exact exact_couple_sequence },
-    { exact is_bounded_sequence },
-    { exact λn, (n, ub n) },
-    { intro n, change max0 (ub n - ub n) = 0, exact ap max0 (sub_self (ub n)) },
-    { intro ns, reflexivity },
-    { intro n, reflexivity },
-    { intro r, exact (-(1 : ℤ), r + (1 : ℤ)) },
-    { intro r, refine !convergence_theorem.deg_dr ⬝ _,
-      refine ap (deg j_sequence) !iterate_deg_i_inv ⬝ _,
-      exact prod_eq idp !zero_add }
-  end
-
-  end
-
--- Uncomment the next line to see that the proof uses univalence, but that there are no holes
---('sorry') in the proof:
-
--- print axioms is_bounded_sequence
-
--- It depends on univalence in an essential way. The reason is that the long exact sequence
--- of homotopy groups already depends on univalence. Namely, in that proof we need to show that if f
--- : A → B and g : B → C are exact at B, then ∥A∥₀ → ∥B∥₀ → ∥C∥₀ is exact at ∥B∥₀. For this we need
--- that the equality |b|₀ = |b'|₀ is equivalent to ∥b = b'∥₋₁, which requires univalence.
-end spectrum
+end spectral_sequence
diff --git a/algebra/submodule.hlean b/algebra/submodule.hlean
index feaaaea..0e2722e 100644
--- a/algebra/submodule.hlean
+++ b/algebra/submodule.hlean
@@ -160,11 +160,11 @@ begin
   apply h (of_mem_property_of Sm)
 end
 
-definition is_prop_submodule (S : property M) [is_submodule M S] [H : is_prop M] : is_prop (submodule S) :=
-begin apply @is_trunc_sigma, exact H end
-local attribute is_prop_submodule [instance]
-definition is_contr_submodule [instance] (S : property M) [is_submodule M S] [is_contr M] : is_contr (submodule S) :=
-is_contr_of_inhabited_prop 0 _
+definition is_contr_submodule (S : property M) [is_submodule M S] (H : is_contr M) :
+  is_contr (submodule S) :=
+have is_prop M, from _,
+have is_prop (submodule S), from @is_trunc_sigma _ _ _ this _,
+is_contr_of_inhabited_prop 0 this
 
 definition submodule_isomorphism [constructor] (S : property M) [is_submodule M S] (h : Πg, g ∈ S) :
   submodule S ≃lm M :=
@@ -240,11 +240,12 @@ lm_homomorphism_of_group_homomorphism
 
 definition is_prop_quotient_module (S : property M) [is_submodule M S] [H : is_prop M] : is_prop (quotient_module S) :=
 begin apply @set_quotient.is_trunc_set_quotient, exact H end
-local attribute is_prop_quotient_module [instance]
 
-definition is_contr_quotient_module [instance] (S : property M) [is_submodule M S] [is_contr M] :
-  is_contr (quotient_module S) :=
-is_contr_of_inhabited_prop 0 _
+definition is_contr_quotient_module [instance] (S : property M) [is_submodule M S]
+  (H : is_contr M) : is_contr (quotient_module S) :=
+have is_prop M, from _,
+have is_prop (quotient_module S), from @set_quotient.is_trunc_set_quotient _ _ _ this,
+is_contr_of_inhabited_prop 0 this
 
 definition rel_of_is_contr_quotient_module (S : property M) [is_submodule M S]
   (H : is_contr (quotient_module S)) (m : M) : S m :=
@@ -331,11 +332,11 @@ end
 --   reflexivity
 -- end
 
-definition is_contr_image_module [instance] (φ : M₁ →lm M₂) [is_contr M₂] :
+definition is_contr_image_module [instance] (φ : M₁ →lm M₂) (H : is_contr M₂) :
   is_contr (image_module φ) :=
-!is_contr_submodule
+is_contr_submodule _ _
 
-definition is_contr_image_module_of_is_contr_dom (φ : M₁ →lm M₂) [is_contrM₁ : is_contr M₁] :
+definition is_contr_image_module_of_is_contr_dom (φ : M₁ →lm M₂) (H : is_contr M₁) :
   is_contr (image_module φ) :=
 is_contr.mk 0
   begin
@@ -343,7 +344,7 @@ is_contr.mk 0
     apply @total_image.rec,
     exact this,
     intro m,
-    have h : is_contr (LeftModule.carrier M₁), from is_contrM₁,
+    have h : is_contr (LeftModule.carrier M₁), from H,
     induction (eq_of_is_contr 0 m), apply subtype_eq,
     exact (to_respect_zero φ)⁻¹
   end
@@ -369,19 +370,21 @@ is_submodule.mk
        begin apply @is_subgroup.mul_mem, apply is_subgroup_kernel, exact hg₁, exact hg₂ end)
   (has_scalar_kernel φ)
 
-definition kernel_full (φ : M₁ →lm M₂) [is_contr M₂] (m : M₁) : m ∈ lm_kernel φ :=
+definition kernel_full (φ : M₁ →lm M₂) (H : is_contr M₂) (m : M₁) : m ∈ lm_kernel φ :=
 !is_prop.elim
 
 definition kernel_module [reducible] (φ : M₁ →lm M₂) : LeftModule R := submodule (lm_kernel φ)
 
-definition is_contr_kernel_module [instance] (φ : M₁ →lm M₂) [is_contr M₁] :
+definition is_contr_kernel_module [instance] (φ : M₁ →lm M₂) (H : is_contr M₁) :
   is_contr (kernel_module φ) :=
-!is_contr_submodule
+is_contr_submodule _ _
 
-definition kernel_module_isomorphism [constructor] (φ : M₁ →lm M₂) [is_contr M₂] : kernel_module φ ≃lm M₁ :=
-submodule_isomorphism _ (kernel_full φ)
+definition kernel_module_isomorphism [constructor] (φ : M₁ →lm M₂) (H : is_contr M₂) :
+  kernel_module φ ≃lm M₁ :=
+submodule_isomorphism _ (kernel_full φ _)
 
-definition homology_quotient_property (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) : property (kernel_module ψ) :=
+definition homology_quotient_property (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) :
+  property (kernel_module ψ) :=
 property_submodule (lm_kernel ψ) (image (homomorphism_fn φ))
 
 definition is_submodule_homology_property [instance] (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) :
@@ -417,14 +420,14 @@ quotient_elim (θ ∘lm submodule_incl _)
     exact ap θ p⁻¹ ⬝ H v -- m'
   end
 
-definition is_contr_homology [instance] (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) [is_contr M₂] :
+definition is_contr_homology [instance] (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) (H : is_contr M₂) :
   is_contr (homology ψ φ) :=
-begin apply @is_contr_quotient_module end
+is_contr_quotient_module _ (is_contr_kernel_module _ _)
 
 definition homology_isomorphism [constructor] (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂)
-  [is_contr M₁] [is_contr M₃] : homology ψ φ ≃lm M₂ :=
+  (H₁ : is_contr M₁) (H₃ : is_contr M₃) : homology ψ φ ≃lm M₂ :=
 (quotient_module_isomorphism (homology_quotient_property ψ φ)
-  (eq_zero_of_mem_property_submodule_trivial (image_trivial _))) ⬝lm (kernel_module_isomorphism ψ)
+  (eq_zero_of_mem_property_submodule_trivial (image_trivial _))) ⬝lm (kernel_module_isomorphism ψ _)
 
 definition ker_in_im_of_is_contr_homology (ψ : M₂ →lm M₃) {φ : M₁ →lm M₂}
   (H₁ : is_contr (homology ψ φ)) {m : M₂} (p : ψ m = 0) : image φ m :=
diff --git a/cohomology/projective_space.hlean b/cohomology/projective_space.hlean
index 5a7dffe..1d7b020 100644
--- a/cohomology/projective_space.hlean
+++ b/cohomology/projective_space.hlean
@@ -5,7 +5,7 @@ Author: Floris van Doorn-/
 import .serre
 
 open eq spectrum EM EM.ops int pointed cohomology left_module algebra group fiber is_equiv equiv
-     prod is_trunc function
+     prod is_trunc function exact_couple
 
 namespace temp
 
@@ -22,9 +22,9 @@ namespace temp
   λx, pt
 
   definition fserre :
-    (λp q, uoH^p[K agℤ 2, H^q[circle₊]]) ⟹ᵍ (λn, H^-n[unit₊]) :=
+    (λp q, uoH^p[K agℤ 2, H^q[circle₊]]) ⟹ᵍ (λn, H^n[unit₊]) :=
   proof
-  converges_to_g_isomorphism
+  convergent_exact_couple_g_isomorphism
     (serre_convergence_map_of_is_conn pt f (EM_spectrum agℤ) 0
       (is_strunc_EM_spectrum agℤ) (is_conn_EM agℤ 2))
     begin
diff --git a/cohomology/serre.hlean b/cohomology/serre.hlean
index 8dee31d..6059149 100644
--- a/cohomology/serre.hlean
+++ b/cohomology/serre.hlean
@@ -126,6 +126,8 @@ pfiber_postnikov_map_pred' A n k _ idp ⬝e*
 pequiv_ap (EM_spectrum (πₛ[n] A)) (add.comm n k)
 qed
 
+open exact_couple
+
 section atiyah_hirzebruch
   parameters {X : Type*} (Y : X → spectrum) (s₀ : ℤ) (H : Πx, is_strunc s₀ (Y x))
   include H
@@ -249,14 +251,14 @@ convergent_exact_couple_g_isomorphism
     intro n, reflexivity
   end
 
-  definition unreduced_atiyah_hirzebruch_spectral_sequence {X : Type} (Y : X → spectrum) (s₀ : ℤ)
-    (H : Πx, is_strunc s₀ (Y x)) :
-    convergent_spectral_sequence_g (λp q, uopH^p[(x : X), πₛ[-q] (Y x)]) (λn, upH^n[(x : X), Y x]) :=
-  begin
-    apply convergent_spectral_sequence_of_exact_couple (unreduced_atiyah_hirzebruch_convergence Y s₀ H),
-    { intro n, exact add.comm (s₀ - -n) (-s₀) ⬝ !neg_add_cancel_left ⬝ !neg_neg },
-    { reflexivity }
-  end
+definition unreduced_atiyah_hirzebruch_spectral_sequence {X : Type} (Y : X → spectrum) (s₀ : ℤ)
+  (H : Πx, is_strunc s₀ (Y x)) :
+  convergent_spectral_sequence_g (λp q, uopH^p[(x : X), πₛ[-q] (Y x)]) (λn, upH^n[(x : X), Y x]) :=
+begin
+  apply convergent_spectral_sequence_of_exact_couple (unreduced_atiyah_hirzebruch_convergence Y s₀ H),
+  { intro n, exact add.comm (s₀ - -n) (-s₀) ⬝ !neg_add_cancel_left ⬝ !neg_neg },
+  { reflexivity }
+end
 
 end unreduced_atiyah_hirzebruch
 
diff --git a/homotopy/three_by_three.hlean b/homotopy/three_by_three.hlean
index 9379b32..cae70a3 100644
--- a/homotopy/three_by_three.hlean
+++ b/homotopy/three_by_three.hlean
@@ -28,7 +28,7 @@ namespace pushout
 
   open three_by_three_span
   variable (E : three_by_three_span)
-check (pushout.functor (f₂₁ E) (f₀₁ E) (f₄₁ E) (s₁₁ E) (s₃₁ E))
+-- check (pushout.functor (f₂₁ E) (f₀₁ E) (f₄₁ E) (s₁₁ E) (s₃₁ E))
   definition pushout2hv (E : three_by_three_span) : Type :=
   pushout (pushout.functor (f₂₁ E) (f₀₁ E) (f₄₁ E) (s₁₁ E) (s₃₁ E))
           (pushout.functor (f₂₃ E) (f₀₃ E) (f₄₃ E) (s₁₃ E) (s₃₃ E))