diff --git a/DividedPowers/DPAlgebra/Dpow.lean b/DividedPowers/DPAlgebra/Dpow.lean
index 5133692..eefbe7d 100644
--- a/DividedPowers/DPAlgebra/Dpow.lean
+++ b/DividedPowers/DPAlgebra/Dpow.lean
@@ -34,8 +34,6 @@ to the degree 1 part of `DividedPowerAlgebra R M`.
 
 - `onDPAlgebra_unique`: uniqueness of this structure.
 
-
-
 ## Reference
 
 * [Roby1965]
@@ -116,8 +114,7 @@ section TensorProduct
 open scoped TensorProduct
 
 /-- The ideal `K := I + J` in the tensor product `R ⊗[A] S`. -/
-def K (A : Type uA) [CommRing A]
-    {R : Type uR} [CommRing R] [Algebra A R] (I : Ideal R)
+def K (A : Type uA) [CommRing A] {R : Type uR} [CommRing R] [Algebra A R] (I : Ideal R)
     {S : Type uS} [CommRing S] [Algebra A S] (J : Ideal S) : Ideal (R ⊗[A] S) :=
   I.map (Algebra.TensorProduct.includeLeft : R →ₐ[A] R ⊗[A] S)
     ⊔ J.map Algebra.TensorProduct.includeRight
@@ -160,7 +157,9 @@ def CondT (A : Type u) [CommRing A] : Prop :=
     (S : Type u) [CommRing S] [Algebra A S] {J : Ideal S} (hJ : DividedPowers J), Condτ A hI hJ -/
 
 /-- Existence of divided powers on the ideal of a tensor product
-  of any two *split* divided power algebras (universalization of `Condτ`). -/
+  of any two *split* divided power algebras (universalization of `Condτ`).
+  Note that this differs from the definition in Roby, who does not required the algebras
+  to be split. -/
 def CondT (A : Type u) [CommRing A] : Prop :=
   ∀ (R : Type u) [CommRing R] [Algebra A R] {I : Ideal R} (hI : DividedPowers I)
     {R₀ : Subalgebra A R} (_ : I.IsAugmentation R₀) (S : Type u) [CommRing S] [Algebra A S]
@@ -210,7 +209,7 @@ open scoped TensorProduct
 
 -- Roby, lemma 3
 /-- Any divided power structure on the divided power algebra makes the canonical morphisms to a
-  divided power ring a DP morphism -/
+  divided power ring a DP morphism. -/
 theorem cond_D_uniqueness [DecidableEq R] {M : Type uM} [AddCommGroup M] [Module R M]
     (h : DividedPowers (augIdeal R M)) (hh : ∀ (n : ℕ) (x : M), h.dpow n (ι R M x) = dp R n x)
     {S : Type uS} [CommRing S] [Algebra R S] {J : Ideal S} (hJ : DividedPowers J)
@@ -233,16 +232,14 @@ theorem cond_D_uniqueness [DecidableEq R] {M : Type uM} [AddCommGroup M] [Module
       apply congr_arg₂ _ rfl
       rw [hh, lift_apply_dp]
 
-
 -- We open a namespace to privatize the complicated construction
 namespace roby4
-
 variable (A : Type u) [CommRing A]
 
 /- The goal of this section is to establish [Roby1963, Lemme 4] (`condTFree_and_condD_to_condQ`),
   that under the above assumptions, `CondQ A` holds. It involves a lifting construction. -/
 
-variable (S : Type u) [CommRing S] [Algebra A S] {I : Ideal S} (hI : DividedPowers I)
+variable {S : Type u} [CommRing S] [Algebra A S] (I : Ideal S)
   (S₀ : Subalgebra A S) (hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (I.restrictScalars A))
 
 -- We construct MvPolynomial S₀ A = A[S₀] →ₐ[A] S₀
@@ -261,10 +258,9 @@ theorem algebraMap_eq :
     simp only [AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, _root_.map_mul, AlgHom.commutes]
     rw [← mul_assoc] } -/
 
-variable {S} (I) in
+/-- The linear map `(I →₀ A) →ₗ[A] S` sending `single i 1` to `i : S`. -/
 def f : (I →₀ A) →ₗ[A] S := (Basis.constr (Finsupp.basisSingleOne) A) (fun i ↦ (i : S))
 
-variable {S} (I) in
 theorem f_mem_I (p) : f A I p ∈ I := by
   suffices LinearMap.range (f A I) ≤ Submodule.restrictScalars A I by
     apply this
@@ -273,8 +269,6 @@ theorem f_mem_I (p) : f A I p ∈ I := by
   rintro _ ⟨i, rfl⟩
   simp only [Submodule.coe_restrictScalars, SetLike.mem_coe, SetLike.coe_mem]
 
--- variable  (condTFree : CondTFree A) (condD : CondD A)
-
 open Algebra Algebra.TensorProduct
 section DecidableEq
 
@@ -287,17 +281,21 @@ instance hdpM_free : Module.Free A (DividedPowerAlgebra A (I →₀ A)) :=
 instance hR_free : Module.Free A (MvPolynomial S A) :=
   Module.Free.of_basis (MvPolynomial.basisMonomials _ _)
 
+/-- The divided power structure on the ideal `0` of `MvPolynomial S A`. -/
 def hR [DecidableEq (MvPolynomial S A)] := dividedPowersBot (MvPolynomial S A)
 
-variable (I) in
 theorem condτ [DecidableEq (MvPolynomial (↥S₀) A)] (condTFree : CondTFree A) :
     Condτ A (dividedPowersBot (MvPolynomial S₀ A)) hM := by apply condTFree
 
+variable {I} (hI : DividedPowers I)
+
+/-- The canonical extension of the map `f` to `DividedPowerAlgebra A (I →₀ A)`. -/
 def Φ : DividedPowerAlgebra A (I →₀ A) →ₐ[A] S :=
   DividedPowerAlgebra.lift hI (f A I) (f_mem_I _ _)
 
+/-- The map `Φ` as a DP morphism. -/
 def dpΦ : DPMorphism hM hI := by
-  apply DPMorphism.fromGens hM hI (augIdeal_eq_span _ _) (f := (Φ A S hI).toRingHom)
+  apply DPMorphism.fromGens hM hI (augIdeal_eq_span _ _) (f := (Φ A hI).toRingHom)
   · rw [Ideal.map_le_iff_le_comap, augIdeal_eq_span, span_le]
     rintro x ⟨n, hn, b, _, rfl⟩
     simp only [AlgHom.toRingHom_eq_coe, SetLike.mem_coe, mem_comap, RingHom.coe_coe,
@@ -310,19 +308,24 @@ def dpΦ : DPMorphism hM hI := by
     apply congr_arg₂ _ rfl
     rw [hM_eq, lift_apply_dp]
 
+variable {A}
+
 -- We consider `(MvPolynomial S₀ A) ⊗[A] DividedPowerAlgebra A (I →₀ A) →ₐ[A] S`
+/-- The product of the algebra map `MvPolynomial S₀ A → S` and `Φ A hI`. -/
 def Ψ : MvPolynomial S₀ A ⊗[A] DividedPowerAlgebra A (I →₀ A) →ₐ[A] S :=
   productMap ((Subalgebra.val S₀).comp (IsScalarTower.toAlgHom A (MvPolynomial S₀ A) S₀))
-    (Φ A S hI)
+    (Φ A hI)
 
 end DecidableEq
 
+variable {A} {I} (hI : DividedPowers I)
+
 theorem Ψ_eq (i) (hi : i ∈ I) :
-    Ψ A S hI S₀ (includeRight (ι A _ (Finsupp.single ⟨i, hi⟩ 1 : I →₀ A))) = i := by
+    Ψ S₀ hI (includeRight (ι A _ (Finsupp.single ⟨i, hi⟩ 1 : I →₀ A))) = i := by
   simp [Ψ, Φ, f, Basis.constr_apply]
 
 theorem Ψ_surjective (hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (I.restrictScalars A)) :
-    Function.Surjective (Ψ A S hI S₀) := by
+    Function.Surjective (Ψ S₀ hI) := by
   rw [← range_top_iff_surjective _, _root_.eq_top_iff]
   intro s _
   obtain ⟨s₀, hs₀, s₁, hs₁, rfl⟩ := Submodule.exists_add_eq_of_codisjoint (hIS₀.codisjoint) s
@@ -338,7 +341,7 @@ theorem Ψ_surjective (hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (I.restric
       lift_ι_apply, one_mul, Basis.constr_apply, Finsupp.basisSingleOne_repr,
       LinearEquiv.refl_apply, zero_smul, Finsupp.sum_single_index, one_smul]
 
-theorem Ψ_map_eq : Subalgebra.map (Ψ A S hI S₀)
+theorem Ψ_map_eq : Subalgebra.map (Ψ S₀ hI)
     (Subalgebra.restrictScalars A (⊥ : Subalgebra (MvPolynomial S₀ A) _)) = S₀ := by
   ext x
   simp only [Subalgebra.mem_map, Subalgebra.mem_restrictScalars, Algebra.mem_bot, Set.mem_range,
@@ -353,20 +356,23 @@ theorem Ψ_map_eq : Subalgebra.map (Ψ A S hI S₀)
       IsScalarTower.coe_toAlgHom', Function.comp_apply, map_one, mul_one, algebraMap_eq,
       AlgHom.toRingHom_eq_coe, RingHom.coe_coe, aeval_X, id_eq]
 
-variable (I) in
+variable (I)
+
 theorem K_eq_span [DecidableEq A] :
     K A (⊥ : Ideal (MvPolynomial S₀ A)) (augIdeal A (↥I →₀ A))
       = span (Set.image2 (fun n a ↦ 1 ⊗ₜ[A] dp A n a) {n | 0 < n} Set.univ) := by
   simp only [K, Ideal.map_bot, ge_iff_le, bot_le, sup_of_le_right, augIdeal_eq_span,
     Ideal.map_span, includeRight_apply, Set.image_image2]
 
+variable {I}
+
+/-- The divided power morphism from `(condτ A I S₀ hM condTFree).choose` to `hI`. -/
 def dpΨ [DecidableEq A] [DecidableEq (MvPolynomial (↥S₀) A)]
-   (hM : DividedPowers (augIdeal A (I →₀ A)))
-   (hM_eq : ∀ n x, hM.dpow n ((ι A (I →₀ A)) x) = dp A n x)
-   (condTFree : CondTFree A) :
-    DPMorphism (condτ A S I S₀ hM condTFree).choose hI := by
-  apply DPMorphism.fromGens (condτ A S I S₀ hM condTFree).choose hI
-    (f := (Ψ A S hI S₀).toRingHom) (K_eq_span A S I S₀)
+    (hM : DividedPowers (augIdeal A (I →₀ A)))
+    (hM_eq : ∀ n x, hM.dpow n ((ι A (I →₀ A)) x) = dp A n x) (condTFree : CondTFree A) :
+    DPMorphism (condτ A I S₀ hM condTFree).choose hI := by
+  apply DPMorphism.fromGens (condτ A I S₀ hM condTFree).choose hI
+    (f := (Ψ S₀ hI).toRingHom) (K_eq_span I S₀)
   · -- Ideal.map (Ψ A S hI S₀).toRingHom (K A ⊥ (augIdeal A (↥I →₀ A))) ≤ I
     -- TODO: extract as equality in lemma
     simp only [AlgHom.toRingHom_eq_coe, K, Ideal.map_bot, ge_iff_le,
@@ -374,17 +380,15 @@ def dpΨ [DecidableEq A] [DecidableEq (MvPolynomial (↥S₀) A)]
     rintro _ ⟨n, hn, b, _, rfl⟩
     simp only [SetLike.mem_coe, mem_comap, Algebra.TensorProduct.includeRight_apply,
       RingHom.coe_coe, Ψ, Algebra.TensorProduct.productMap_apply_tmul, map_one, one_mul]
-    exact (dpΦ A S hI hM hM_eq).ideal_comp
+    exact (dpΦ A hM hM_eq hI).ideal_comp
       (Ideal.mem_map_of_mem _ (dp_mem_augIdeal A (I →₀ A) hn b))
   · rintro n _ ⟨m, hm, b, _, rfl⟩
     simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe]
-    erw [← ((condτ A S I S₀ hM condTFree).choose_spec.2).map_dpow]
+    erw [← ((condτ A I S₀ hM condTFree).choose_spec.2).map_dpow (dp_mem_augIdeal _ _ hm _)]
     simp only [Ψ, RingHom.coe_coe, Algebra.TensorProduct.includeRight_apply,
       Algebra.TensorProduct.productMap_apply_tmul, map_one, one_mul]
-    erw [(dpΦ A S hI hM hM_eq).dpow_comp]
-    · rfl
-    all_goals
-      apply dp_mem_augIdeal _ _ hm
+    erw [(dpΦ A hM hM_eq hI).dpow_comp _ (dp_mem_augIdeal _ _ hm _)]
+    rfl
 
 -- TODO: add to Mathlib (with _apply, as in Polynomial case)
 /-- `MvPolynomial.C` as an `AlgHom`. -/
@@ -397,7 +401,6 @@ def _root_.MvPolynomial.CAlgHom {R : Type*} [CommRing R] {A : Type*} [CommRing A
 -- NOTE: we are having the same issues with `map_zero` and `map_add` that we did with `map_smul`
 -- (previously `AlgHom.map_smul`) in RobyLemma9.
 
-
 lemma Subalgebra_tensorProduct_top_bot [Algebra A R]
     (S : Type*) [CommRing S] [Algebra A S] {S₀ : Subalgebra A S} (hS₀ : S₀ = ⊥)
     {T₀ : Subalgebra A R} (hT₀ : T₀ = ⊤) :
@@ -436,21 +439,16 @@ lemma Subalgebra_tensorProduct_top_bot [Algebra A R]
 
 lemma map_psi_augIdeal_eq [DecidableEq A] (hM : DividedPowers (augIdeal A (I →₀ A)))
     (hM_eq : ∀ n x, hM.dpow n ((ι A (I →₀ A)) x) = dp A n x)
-
-    (condTFree: CondTFree A) :
-    Ideal.map (Ψ A S hI S₀) (K A ⊥ (augIdeal A (I →₀ A))) = I := by
+    (condTFree : CondTFree A) :
+    Ideal.map (Ψ S₀ hI) (K A ⊥ (augIdeal A (I →₀ A))) = I := by
   classical
-  apply le_antisymm (dpΨ A S hI S₀ hM hM_eq condTFree).ideal_comp
+  apply le_antisymm (dpΨ S₀ hI hM hM_eq condTFree).ideal_comp
   intro i hi
-  rw [← Ψ_eq A S hI S₀ i hi]
-  apply Ideal.mem_map_of_mem
-  apply Ideal.mem_sup_right
-  apply Ideal.mem_map_of_mem
-  apply ι_mem_augIdeal
+  rw [← Ψ_eq S₀ hI i hi]
+  exact mem_map_of_mem _ (mem_sup_right (mem_map_of_mem _ (ι_mem_augIdeal _ _ _)))
 
 -- set_option trace.profiler true -- < 6 sec here!
 -- Roby, lemma 4
-variable {A} in
 theorem _root_.DividedPowerAlgebra.condTFree_and_condD_to_condQ [DecidableEq A]
     (condTFree: CondTFree A) (condD : CondD A) : CondQ A := by
   classical
@@ -464,93 +462,73 @@ theorem _root_.DividedPowerAlgebra.condTFree_and_condD_to_condQ [DecidableEq A]
     Module.Free.of_basis (MvPolynomial.basisMonomials _ _)
   -- We consider `R ⊗[A] DividedPowerAlgebra A M` as a comm ring and an A-algebra
   use R ⊗[A] D, by infer_instance, by infer_instance
-  /- We need to add the fact that `R ⊗ DividedPowerAlgebra A M``
-     is pregraduated in the sense of Roby,
-     that is, the ideal is an augmentation ideal (given by tensor product).
-     Note : in this case, it could maybe be given by base change,
-     and it is not clear to me why this (simpler) approach does not suffice.
-     In fact, `dpΨ` was proved above using that! -/
+  /- We need to add the fact that `R ⊗ DividedPowerAlgebra A M` is pregraduated in the sense of
+    Roby, that is, the ideal is an augmentation ideal (given by tensor product).
+    Note : in this case, it could maybe be given by base change, and it is not clear to me why
+    this (simpler) approach does not suffice.
+    In fact, `dpΨ` was proved above using that! -/
   have htop : Ideal.IsAugmentation (⊤ : Subalgebra A R) (⊥ : Ideal R) := by
-    rw [isAugmentation_subalgebra_iff A]
+    rw [isAugmentation_subalgebra_iff]
     exact isCompl_top_bot
-  refine ⟨_, (condτ A S I S₀ hM condTFree).choose, _,
+  refine ⟨_, (condτ A I S₀ hM condTFree).choose, _,
     Ideal.isAugmentation_tensorProduct A htop (isAugmentation A M), ?_⟩
-  use Ψ A S hI S₀
-  refine ⟨map_psi_augIdeal_eq A S hI S₀ hM hM_eq condTFree, ?_⟩
+  use Ψ S₀ hI
+  refine ⟨map_psi_augIdeal_eq S₀ hI hM hM_eq condTFree, ?_⟩
   constructor
   · -- Ψ maps the 0 part to S₀
-    convert Ψ_map_eq A S hI S₀ using 2
-    exact Subalgebra_tensorProduct_top_bot A D (gradeZeroSubalgebra_eq_bot _ _) rfl
-  constructor
-  · apply Ψ_surjective A S hI S₀
-    simp only [← isAugmentation_subalgebra_iff, hIS₀]
-  constructor
-  · exact (dpΨ A S hI S₀ hM hM_eq condTFree).isDPMorphism
-  · infer_instance -- tensor product of free modules is free
+    convert Ψ_map_eq S₀ hI using 2
+    exact Subalgebra_tensorProduct_top_bot D (gradeZeroSubalgebra_eq_bot _ _) rfl
+  exact ⟨Ψ_surjective S₀ hI (isAugmentation_subalgebra_iff.mp hIS₀),
+    ⟨(dpΨ S₀ hI hM hM_eq condTFree).isDPMorphism, by infer_instance⟩⟩
+  -- The `inferInstance` finds that the tensor product of free modules is free
 
--- the freeness of DividedPowerAlgebra of a free module still uses `sorry`
+-- The freeness of DividedPowerAlgebra of a free module still uses `sorry`
 --#print axioms DividedPowerAlgebra.condTFree_and_condD_to_condQ
 
 end roby4
 
+lemma _root_.Ideal.map_toRingHom (A R S : Type*) [CommSemiring A] [Semiring R] [Algebra A R]
+    [Semiring S] [Algebra A S] (f : R →ₐ[A] S) (I : Ideal R) :
+    Ideal.map f I = Ideal.map f.toRingHom I := rfl
 
-example {A : Type*} [CommRing A] (a : A) (n : ℕ) : n • a = n * a := by refine' nsmul_eq_mul n a
 
-lemma _root_.Ideal.map_toRingHom (A R S : Type*) [CommSemiring A]
-    [Semiring R] [Algebra A R] [Semiring S] [Algebra A S] (f : R →ₐ[A] S)
-    (I : Ideal R) : Ideal.map f I = Ideal.map f.toRingHom I := rfl
+/- In Roby, all DP-algebras `A` considered are of the form `A₀ ⊕ A₊`, where `A₊` is the DP-ideal.
+In other words, the DP-ideal is an augmentation ideal. Moreover, DP-morphisms map `A₀` to `B₀` and
+`A₊` to `B₊`, so that their kernel is a direct sum `K₀ ⊕ K₊`.
 
+Roby's framework is stated in terms of `pre-graded algebras`, namely graded algebras by the monoid
+`{⊥, ⊤}` with carrier set `Fin 2` (with multiplication, `⊤ = 0` and `⊥ = 1`).
 
-/- In Roby, all PD-algebras A considered are of the form A₀ ⊕ A₊,
-where A₊ is the PD-ideal. In other words, the PD-ideal is an augmentation ideal.
-Moreover, PD-morphisms map A₀ to B₀ and A₊ to B₊,
-so that their kernel is a direct sum K₀ ⊕ K₊
+Most of the paper works in greater generality, as noted by Berthelot, but not all the results hold
+in general. Berthelot gives an example (1.7) of a tensor product of algebras with divided power
+ideals whose natural ideal does not have compatible divided powers.
 
-Roby's framework is stated in terms of `pre-graded algebras`,
-namely graded algebras by the monoid {⊥, ⊤} with carrier set `Fin 2`
-(with multiplication, ⊤ = 0 and ⊥ = 1)
+[Berthelot, 1.7.1] gives the explicit property that holds for tensor products.
+For an `A`-algebra `R` and `I : Ideal R`, one assumes the existence of `R₀ : Subalgebra A R` such
+that `R = R₀ ⊕ I` as an `A`-module. Equivalently, the map `R →ₐ[A] R ⧸ I` has a left inverse.
 
-Most of the paper works in greater generality, as noted by Berthelot,
-but not all the results hold in general.
-Berthelot gives an example (1.7) of a tensor product of algebras
-with divided power ideals whose natural ideal does not have compatible
-divided powers.
+In lemma 6, we have two surjective algebra morphisms `f : R →+* R'`,  `g : S →+* S'` and we consider
+the induced surjective morphism `fg : R ⊗ S →+* R' ⊗ S'`.
+`R` has a DP-ideal `I`,  `R'` has a DP-ideal `I'`, `S` has a DP-ideal `J`,  `S'` has a DP-ideal `J'`
+with assumptions that `I' = map f I` and `J' = map g J`, with quotient DP structures.
 
-[Berthelot, 1.7.1] gives the explicit property that holds for tensor products.
-For an `A`-algebra `R` and `I : Ideal R`, one assumes the
-existence of `R₀ : Subalgebra A R` such that `R = R₀ ⊕ I` as an `A`-module.
-Equivalently, the map `R →ₐ[A] R ⧸ I` has a left inverse.
-
-In lemma 6, we have two surjective algebra morphisms
- f : R →+* R',  g : S →+* S'
-and we consider the induced surjective morphism fg : R ⊗ S →+* R' ⊗ S'
-R has a PD-ideal I,  R' has a PD-ideal I',
-S has a PD-ideal J,  S' has a PD-ideal J'
-with assumptions that I' = map f I and J' = map g J,
-with quotient PD structures
-
-Lemma 5 has proved that  fg.ker = (f.ker ⊗ 1) ⊔ (1 ⊗ g.ker)
-
-The implicit hypothesis in lemma 6 is that f is homogeneous,
-ie, maps R₊ = I to R'₊ = J and R₀ to R'₀, and same for g
-
-In the end, Roby applies his proposition 4 which we
-apparently haven't formalized and make use of yet another definition,
-namely of a `divised ideal` :
-Up to the homogeneous condition, this is exactly that `K ⊓ I` is a sub-pd-ideal.
-The proof of proposition goes by using that
-`Ideal.span (s ∩ ↑I) = Ideal.span s ⊓ I`
-if `s` consists of homogeneous elements.
-
-So we assume the `roby` condition in the statement, in the hope
-that will be possible to prove it each time we apply cond_τ_rel
+Lemma 5 has proved that `fg.ker = (f.ker ⊗ 1) ⊔ (1 ⊗ g.ker)`.
+
+The implicit hypothesis in lemma 6 is that `f` is homogeneous, i.e., maps `R₊ = I` to `R'₊ = J`
+and `R₀` to `R'₀`, and same for `g`.
+
+In the end, Roby applies his proposition 4 and makes use of yet another definition, namely of a
+`divised ideal` : up to the homogeneous condition, this is exactly that `K ⊓ I` is a sub-pd-ideal.
+The proof of proposition goes by using that `Ideal.span (s ∩ ↑I) = Ideal.span s ⊓ I` if `s`
+consists of homogeneous elements.
+
+So we assume the `roby` condition in the statement, in the hope that will be possible to prove it
+each time we apply `condτ_rel`.
 -/
 
-/- While the following form is mathematically sufficient,
-   it is probably simpler to prove lemma 6 as in Roby
-   the hypothsis will be that `RingHom.ker (Algebra.TensorProduct.map f g)`
-   is generated by a bunch of things
-   that allow to prove that it is a “divised ideal” -/
+/- While the following form is mathematically sufficient, it is probably simpler to prove lemma 6
+as in Roby. The hypothsis will be that `RingHom.ker (Algebra.TensorProduct.map f g)` is generated
+by a bunch of things that allow to prove that it is a “divised ideal” -/
 
 -- Roby, abstracting lemma 6
 example (A : Type u) [CommRing A] {R S R' S' : Type u} [CommRing R] [CommRing S]
@@ -629,25 +607,11 @@ example (A : Type u) [CommRing A] {R S R' S' : Type u} [CommRing R] [CommRing S]
       simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, Algebra.TensorProduct.map_tmul, map_one,
         fg]
 
-example (A : Type*) [CommRing A] (R : Type*) [CommRing R] [Algebra A R]
-    (R₀ : Subalgebra A R) -- (I : Ideal R) (hcI : Codisjoint (R₀) (I.restrictScalars R₀))
-    :
-    Module R₀ R₀ := by
-    exact Semiring.toModule
-
-example (A : Type*) [CommRing A] (R : Type*) [CommRing R] [Algebra A R]
-    (R₀ : Subalgebra A R) -- (I : Ideal R) (hcI : Codisjoint (R₀) (I.restrictScalars R₀))
-    :
-    Module R₀ R := by
-    exact R₀.module
-
-
-
-theorem RingHom.ker_eq_span_union (A : Type*) [CommRing A]
-    (R : Type*) [CommRing R] [Algebra A R]
-    (R₀ : Subalgebra A R) (I : Ideal R) (hcI : Codisjoint (Subalgebra.toSubmodule R₀) (I.restrictScalars A))
-    (S : Type*) [CommRing S] [Algebra A S]
-    (S₀ : Subalgebra A S) (J : Ideal S) (hdJ : Disjoint (Subalgebra.toSubmodule S₀) (J.restrictScalars A))
+theorem RingHom.ker_eq_span_union {A : Type*} [CommRing A] {R : Type*} [CommRing R] [Algebra A R]
+    {R₀ : Subalgebra A R} {I : Ideal R}
+    (hcI : Codisjoint (Subalgebra.toSubmodule R₀) (I.restrictScalars A)) {S : Type*} [CommRing S]
+    [Algebra A S] {S₀ : Subalgebra A S} {J : Ideal S}
+    (hdJ : Disjoint (Subalgebra.toSubmodule S₀) (J.restrictScalars A))
     (f : R →ₐ[A] S) (hf0 : f '' R₀ ≤ S₀) (hfI : f '' I ≤ J) :
     RingHom.ker f = Submodule.span _ (RingHom.ker f ∩ R₀ ∪ RingHom.ker f ∩ I) := by
   apply le_antisymm
@@ -694,7 +658,7 @@ theorem RingHom.ker_eq_span_union' (A : Type*) [CommRing A]
     (f : R →ₐ[A] S) (hf0 : f '' R₀ ≤ S₀) (hfI : f '' I ≤ J) :
     RingHom.ker f ⊓ I = Submodule.span _ (RingHom.ker f ∩ I) := by
   apply le_antisymm
-  · rw [RingHom.ker_eq_span_union A R R₀ I ?_ S S₀ J ?_ f hf0 hfI]
+  · rw [RingHom.ker_eq_span_union ?_  ?_ f hf0 hfI]
     sorry
     · convert hI.codisjoint
       sorry
@@ -702,7 +666,6 @@ theorem RingHom.ker_eq_span_union' (A : Type*) [CommRing A]
       sorry
   · sorry
 
-
 /-- Roby, Lemma 6, the condition τ descends by quotient -/
 theorem condτ_rel (A : Type u) [CommRing A]
     {R : Type u} [CommRing R] [Algebra A R]
@@ -734,25 +697,16 @@ theorem condτ_rel (A : Type u) [CommRing A]
         Algebra.TensorProduct.includeLeft_apply, Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.map_tmul, map_one]
   have hK'_pd : IsSubDPIdeal hK (RingHom.ker fg ⊓ K A I J) := by
     have := Algebra.TensorProduct.map_ker _ _ hf hg
-    have hkerf := RingHom.ker_eq_span_union A R R₀ I
-      ((Ideal.isAugmentation_subalgebra_iff A).mp hR₀I).codisjoint
-      R' R₀' I'
-      ((Ideal.isAugmentation_subalgebra_iff A).mp hR₀I').disjoint
-      f
+    have hkerf := RingHom.ker_eq_span_union (isAugmentation_subalgebra_iff.mp hR₀I).codisjoint
+      (isAugmentation_subalgebra_iff.mp hR₀I').disjoint f
       (by simp only [hfR₀, Subalgebra.coe_map, le_refl])
-      (by simp only [hI'I, Ideal.map, Set.le_eq_subset]
-          apply Submodule.subset_span)
-    have hkerg := RingHom.ker_eq_span_union A S S₀ J
-      ((Ideal.isAugmentation_subalgebra_iff A).mp hS₀J).codisjoint
-      S' S₀' J'
-      ((Ideal.isAugmentation_subalgebra_iff A).mp hS₀J').disjoint
-      g
+      (by simp only [hI'I, Ideal.map, Set.le_eq_subset]; apply Submodule.subset_span)
+    have hkerg := RingHom.ker_eq_span_union (isAugmentation_subalgebra_iff.mp hS₀J).codisjoint
+      (isAugmentation_subalgebra_iff.mp hS₀J').disjoint g
       (by simp only [hgS₀, Subalgebra.coe_map, le_refl])
-      (by simp only [hJ'J, Ideal.map, Set.le_eq_subset]
-          apply Submodule.subset_span)
+      (by simp only [hJ'J, Ideal.map, Set.le_eq_subset]; apply Submodule.subset_span)
     rw [hkerf, hkerg] at this
-    simp only [submodule_span_eq] at this
-    simp only [Ideal.span_union, Ideal.map_sup] at this
+    simp only [submodule_span_eq, Ideal.span_union, Ideal.map_sup] at this
     rw [sup_sup_sup_comm] at this
     simp only [Ideal.map_span] at this
     rw [this]
@@ -781,110 +735,80 @@ theorem condτ_rel (A : Type u) [CommRing A]
   constructor
   · -- hI'.is_pd_morphism hK' ↑(i_1 A R' S')
     constructor
-    · rw [← hK_map]
-      rw [Ideal.map_le_iff_le_comap]; intro a' ha'
-      rw [Ideal.mem_comap]
-      apply Ideal.mem_sup_left; apply Ideal.mem_map_of_mem; exact ha'
+    · rw [← hK_map, Ideal.map_le_iff_le_comap]
+      exact fun _ ha' ↦ Ideal.mem_sup_left (Ideal.mem_map_of_mem _ ha')
     · intro n a' ha'
       simp only [hI'I, Ideal.mem_map_iff_of_surjective f hf] at ha'
       obtain ⟨a, ha, rfl⟩ := ha'
       simp only [AlgHom.coe_toRingHom, Algebra.TensorProduct.includeLeft_apply]
-      rw [← map_one g, ← Algebra.TensorProduct.map_tmul]
-      rw [← AlgHom.coe_toRingHom f, hfDP.2 a ha, RingHom.coe_coe]
-      rw [← Algebra.TensorProduct.map_tmul]
-      erw [Quotient.OfSurjective.dpow_apply hK s_fg hK'_pd]
-      apply congr_arg
-      exact hK_pd.1.2 a ha
-      apply Ideal.mem_sup_left
-      apply Ideal.mem_map_of_mem _ ha
+      rw [← map_one g, ← Algebra.TensorProduct.map_tmul, ← AlgHom.coe_toRingHom f, hfDP.2 a ha,
+        RingHom.coe_coe, ← Algebra.TensorProduct.map_tmul]
+      erw [Quotient.OfSurjective.dpow_apply hK s_fg hK'_pd (mem_sup_left (mem_map_of_mem _ ha))]
+      exact congr_arg _ (hK_pd.1.2 a ha)
   · -- hJ'.is_pd_morphism hK' ↑(i_2 A R' S')
     constructor
-    · rw [← hK_map]
-      rw [Ideal.map_le_iff_le_comap]; intro a' ha'
-      rw [Ideal.mem_comap]
-      apply Ideal.mem_sup_right; apply Ideal.mem_map_of_mem; exact ha'
+    · rw [← hK_map, map_le_iff_le_comap]
+      exact fun _ ha' ↦ mem_sup_right (Ideal.mem_map_of_mem _ ha')
     · intro n a' ha'
       simp only [hJ'J, Ideal.mem_map_iff_of_surjective g hg] at ha'
       obtain ⟨a, ha, rfl⟩ := ha'
       simp only [AlgHom.coe_toRingHom, Algebra.TensorProduct.includeRight_apply]
       suffices ∀ y : S, fg.toRingHom (1 ⊗ₜ[A] y) = 1 ⊗ₜ[A] g y by
-        rw [← this]
-        rw [Quotient.OfSurjective.dpow_apply hK s_fg]
-        have that := hgDP.2 (n := n) a ha
-        simp only [AlgHom.coe_toRingHom] at that ; rw [that]
-        rw [← this]
-        apply congr_arg
-        simp only [← Algebra.TensorProduct.includeRight_apply]
-        exact hK_pd.2.2 a ha
-        apply Ideal.mem_sup_right
-        apply Ideal.mem_map_of_mem _ ha
+        rw [← this, Quotient.OfSurjective.dpow_apply hK s_fg]
+        · have that := hgDP.2 (n := n) a ha
+          simp only [AlgHom.coe_toRingHom] at that;
+          rw [that, ← this]
+          exact congr_arg _ (hK_pd.2.2 a ha)
+        exact mem_sup_right (mem_map_of_mem _ ha)
       intro x
-      simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, Algebra.TensorProduct.map_tmul, map_one,
-        fg]
+      simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, Algebra.TensorProduct.map_tmul,
+        map_one, fg]
 
-        --((S.val '' FS) ∪ (I.subtype '' FI) : Set R)
+open Submodule
 
 -- Roby, Variante de la proposition 4
-theorem roby_prop_4'
-    (A : Type*) [CommRing A] (R : Type*) [CommRing R] [Algebra A R]
-    {I : Ideal R} {R₀ : Subalgebra A R} (hsplit : IsAugmentation R₀ I)
-    {J : Ideal R} {F₀ : Set R₀} {FI : Set I}
-    (hJ : J = Submodule.span R ((R₀.val '' F₀) ∪ (I.subtype '' FI) : Set R)) :
-    J.restrictScalars R₀
-      = (Subalgebra.toSubmodule ⊥ ⊓ J.restrictScalars R₀)
-          ⊔ (I.restrictScalars R₀ ⊓ J.restrictScalars R₀) := by
+theorem roby_prop_4' {A : Type*} [CommRing A] {R : Type*} [CommRing R] [Algebra A R] {I : Ideal R}
+    {R₀ : Subalgebra A R} (hsplit : IsAugmentation R₀ I) {J : Ideal R} {F₀ : Set R₀} {FI : Set I}
+    (hJ : J = span R ((R₀.val '' F₀) ∪ (I.subtype '' FI) : Set R)) :
+    J.restrictScalars R₀ = (Subalgebra.toSubmodule ⊥ ⊓ J.restrictScalars R₀)
+      ⊔ (I.restrictScalars R₀ ⊓ J.restrictScalars R₀) := by
   rcases hsplit with ⟨hd, hc⟩
-  simp only [Submodule.disjoint_def, Subalgebra.mem_toSubmodule,
-    Submodule.restrictScalars_mem] at hd
+  simp only [disjoint_def, Subalgebra.mem_toSubmodule, restrictScalars_mem] at hd
   refine le_antisymm ?_ (sup_le inf_le_right inf_le_right)
   intro x hx
-  simp only [hJ, SetLike.coe_sort_coe, Submodule.restrictScalars_mem] at hx
-  apply Submodule.span_induction hx (p := fun x ↦ x ∈ _)
+  simp only [hJ, SetLike.coe_sort_coe, restrictScalars_mem] at hx
+  apply span_induction hx (p := fun x ↦ x ∈ _) _ (zero_mem _) (fun x y hx hy ↦ add_mem hx hy)
+  · intro a x hx
+    obtain ⟨a, ha, b, hb, rfl⟩ := Submodule.exists_add_eq_of_codisjoint hc a
+    simp only [Submodule.mem_sup, Submodule.mem_inf, Subalgebra.mem_toSubmodule,
+      restrictScalars_mem] at hx
+    obtain ⟨y, hy, z, hz, rfl⟩ := hx
+    simp only [Subalgebra.mem_toSubmodule, Algebra.mem_bot, Set.mem_range, Subtype.exists] at ha
+    obtain ⟨a, ha, rfl⟩ := ha
+    rw [add_smul]
+    refine add_mem ?_ (Submodule.mem_sup_right
+        ⟨mul_mem_right (y + z) I hb, mul_mem_left J b (add_mem hy.right hz.right)⟩)
+    apply smul_mem _ _ (add_mem (Submodule.mem_sup_left _) (Submodule.mem_sup_right _)) <;>
+    simp only [Submodule.mem_inf, Subalgebra.mem_toSubmodule, hy, Submodule.restrictScalars_mem,
+        and_self, hz]
   · rintro _ (⟨⟨x, hx'⟩, hx, rfl⟩ | ⟨y, hy, rfl⟩)
     · apply Submodule.mem_sup_left
-      simp only [Submodule.mem_inf, Subalgebra.mem_toSubmodule, Submodule.restrictScalars_mem]
-      constructor
-      · rw [Algebra.mem_bot]
-        exact ⟨⟨x, hx'⟩, rfl⟩
+      simp only [Submodule.mem_inf, Subalgebra.mem_toSubmodule, restrictScalars_mem]
+      refine ⟨⟨⟨x, hx'⟩, rfl⟩, ?_⟩
       · rw [hJ]
-        apply Submodule.subset_span
-        apply Set.mem_union_left
+        apply Submodule.subset_span (Set.mem_union_left _ _)
         simp only [Subalgebra.coe_val, Set.mem_image, Subtype.exists, exists_and_right,
           exists_eq_right, hx, hx', exists_const]
     · apply Submodule.mem_sup_right
       simp only [hJ, SetLike.coe_sort_coe, submodule_span_eq, Submodule.mem_inf,
-        Submodule.restrictScalars_mem, SetLike.coe_mem, true_and]
-      constructor
-      . simp only [Submodule.coe_subtype, SetLike.coe_mem]
-      · apply Submodule.subset_span
-        apply Set.mem_union_right
+        restrictScalars_mem, SetLike.coe_mem, true_and]
+      refine ⟨by simp only [Submodule.coe_subtype, SetLike.coe_mem], ?_⟩
+      · apply Submodule.subset_span (Set.mem_union_right _ _)
         simp only [Submodule.coe_subtype, Set.mem_image, SetLike.coe_eq_coe, exists_eq_right, hy]
-  · exact zero_mem _
-  · exact fun x y hx hy ↦ add_mem hx hy
-  · intro a x hx
-    obtain ⟨a, ha, b, hb, rfl⟩ := Submodule.exists_add_eq_of_codisjoint hc a
-    simp only [Submodule.mem_sup, Submodule.mem_inf, Subalgebra.mem_toSubmodule, Submodule.restrictScalars_mem] at hx
-    obtain ⟨y, hy, z, hz, rfl⟩ := hx
-    simp only [Subalgebra.mem_toSubmodule, Algebra.mem_bot, Set.mem_range, Subtype.exists] at ha
-    obtain ⟨a, ha, rfl⟩ := ha
-    simp only [Submodule.restrictScalars_mem] at hb
-    rw [add_smul]
-    apply add_mem
-    · apply Submodule.smul_mem
-      apply add_mem
-      · apply Submodule.mem_sup_left
-        simp only [Submodule.mem_inf, Subalgebra.mem_toSubmodule, hy, Submodule.restrictScalars_mem,
-          and_self]
-      · apply Submodule.mem_sup_right
-        simp only [Submodule.mem_inf, Submodule.restrictScalars_mem, hz, and_self]
-    · apply Submodule.mem_sup_right
-      exact ⟨mul_mem_right (y + z) I hb, mul_mem_left J b (add_mem hy.right hz.right)⟩
 
 -- Roby, Variante de la proposition 4
-theorem roby_prop_4''
-    (A : Type*) [CommRing A] (R : Type*) [CommRing R] [Algebra A R]
-    {I : Ideal R} {R₀ : Subalgebra A R} (hsplit : IsAugmentation R₀ I)
-    {J : Ideal R} {F₀ : Set R₀} {FI : Set I}
+theorem roby_prop_4'' {A : Type*} [CommRing A] {R : Type*} [CommRing R] [Algebra A R] {I : Ideal R}
+    {R₀ : Subalgebra A R} (hsplit : IsAugmentation R₀ I) {J : Ideal R} {F₀ : Set R₀} {FI : Set I}
     (hJ : J = Submodule.span R ((R₀.val '' F₀) ∪ (I.subtype '' FI) : Set R)) :
     J ⊓ I = span (I.subtype '' FI) := by
   rcases hsplit with ⟨hd, hc⟩
@@ -894,10 +818,9 @@ theorem roby_prop_4''
     intro hx hx'
     rw [hJ] at hx
     sorry
-
-  · simp only [span_le, SetLike.coe_sort_coe, Submodule.inf_coe,
+  · simp only [Ideal.span_le, SetLike.coe_sort_coe, Submodule.inf_coe,
       Set.subset_inter_iff]
-    exact ⟨hJ ▸ subset_trans Set.subset_union_right subset_span, Subtype.coe_image_subset _ _⟩
+    exact ⟨hJ ▸ subset_trans Set.subset_union_right Ideal.subset_span, Subtype.coe_image_subset _ _⟩
 
 
 /-
@@ -954,13 +877,15 @@ theorem ne_zero_of_mem_antidiagonal_ne_zero {M : Type*} [AddCommMonoid M] [HasAn
   apply hm
   simpa only [mem_antidiagonal, h.1, h.2, eq_comm, add_zero] using hx
 
-theorem Submodule.restrictScalars_sup {A R M : Type*} [CommSemiring A] [Semiring R] [Algebra A R] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower A R M] {U V : Submodule R M} :
-    Submodule.restrictScalars A (U ⊔ V) = Submodule.restrictScalars A U ⊔ Submodule.restrictScalars A V := by
-  exact Submodule.sup_restrictScalars A U V
+-- I don't think this is needed.
+/- theorem Submodule.restrictScalars_sup {A R M : Type*} [CommSemiring A] [Semiring R] [Algebra A R]
+    [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower A R M] {U V : Submodule R M} :
+    Submodule.restrictScalars A (U ⊔ V) =
+      Submodule.restrictScalars A U ⊔ Submodule.restrictScalars A V :=
+  Submodule.sup_restrictScalars A U V -/
 
 -- Roby, Proposition 4
-theorem roby_prop_4
-    {A : Type*} [CommRing A] {R : Type*} [CommRing R] [Algebra A R] {I : Ideal R}
+theorem roby_prop_4 {A : Type*} [CommRing A] {R : Type*} [CommRing R] [Algebra A R] {I : Ideal R}
     {R₀ : Subalgebra A R} (hsplit : IsAugmentation R₀ I) (hI : DividedPowers I) {J : Ideal R}
     {F₀ : Set R₀} {FI : Set I}
     (hJ : J = Submodule.span R ((R₀.val '' F₀) ∪ (I.subtype '' FI) : Set R)) :
@@ -973,7 +898,7 @@ theorem roby_prop_4
     apply inf_le_left (b := I)
     apply hJ'.dpow_mem hn
     simp only [Ideal.mem_inf, SetLike.coe_mem, and_true]
-    exact hJ ▸ subset_span (Set.mem_union_right _ ⟨a, ha, rfl⟩)
+    exact hJ ▸ Ideal.subset_span (Set.mem_union_right _ ⟨a, ha, rfl⟩)
   · intro H
     set T := { s ∈ J ⊓ I | ∀ n ≠ 0, hI.dpow n s ∈ J } with hT
     -- We prove that T is a subideal of J ⊓ I
@@ -981,30 +906,24 @@ theorem roby_prop_4
     have hT' : T = span T := by
       ext t
       refine ⟨fun ht ↦ Ideal.subset_span ht, ?_⟩
-      intro (ht  : t ∈ span T)
-      rw [hT]
-      simp only [Set.mem_setOf_eq]
-      constructor
-      · exact hT_le ht
-      · induction ht using Submodule.span_induction' with
-        | mem t ht => exact fun n hn ↦ ht.2 n hn
-        | zero => exact fun n hn ↦ by simp only [hI.dpow_eval_zero hn, zero_mem]
-        | add a ha b hb ha' hb' =>
-          intro n hn
-          rw [hI.dpow_add]
-          · apply Ideal.sum_mem
-            rintro ⟨u, v⟩ h
-            simp only
-            rcases ne_zero_of_mem_antidiagonal_ne_zero h hn with (hu | hv)
-            · exact J.mul_mem_right _ (ha' u hu)
-            · exact J.mul_mem_left _ (hb' v hv)
-          · exact inf_le_right (a := J) (hT_le ha)
-          · exact inf_le_right (a := J) (hT_le hb)
-        | smul a x hx hx' =>
-          intro n hn
-          rw [smul_eq_mul, hI.dpow_smul]
-          exact Ideal.mul_mem_left _ _ (hx' n hn)
-          exact inf_le_right (a := J) (hT_le hx)
+      intro (ht : t ∈ span T)
+      simp only [hT, Set.mem_setOf_eq]
+      refine ⟨hT_le ht, ?_⟩
+      induction ht using Submodule.span_induction' with
+      | mem t ht => exact fun n hn ↦ ht.2 n hn
+      | zero => exact fun n hn ↦ by simp only [hI.dpow_eval_zero hn, zero_mem]
+      | add a ha b hb ha' hb' =>
+        intro n hn
+        rw [hI.dpow_add (inf_le_right (a := J) (hT_le ha)) (inf_le_right (a := J) (hT_le hb))]
+        apply Ideal.sum_mem
+        rintro ⟨u, v⟩ h
+        rcases ne_zero_of_mem_antidiagonal_ne_zero h hn with (hu | hv)
+        · exact J.mul_mem_right _ (ha' u hu)
+        · exact J.mul_mem_left _ (hb' v hv)
+      | smul a x hx hx' =>
+        intro n hn
+        rw [smul_eq_mul, hI.dpow_smul (inf_le_right (a := J) (hT_le hx))]
+        exact Ideal.mul_mem_left _ _ (hx' n hn)
     suffices T = J ⊓ I by exact {
       isSubideal := inf_le_right
       dpow_mem := fun hn a ha ↦ by
@@ -1018,102 +937,80 @@ theorem roby_prop_4
       rw [hT']
       ext t
       simp only [SetLike.mem_coe]
-      constructor
-      · exact fun ht ↦ hT_le ht
-      · simp only [Ideal.mem_inf]
-        rintro ⟨ht, ht'⟩
-        rw [← Submodule.restrictScalars_mem A, ← this, Submodule.mem_sup] at ht
-        obtain ⟨y, hy, z, hz, rfl⟩ := ht
-        simp only [Submodule.mem_inf, Submodule.restrictScalars_mem,
-          Subalgebra.mem_toSubmodule] at hy hz
-        apply Submodule.add_mem _ _ hz
-        suffices y = 0 by
-          simp only [this, zero_mem]
-        have hz' := Ideal.mem_inf.mp (hT_le hz)
-        apply Submodule.disjoint_def.mp hsplit.disjoint
-        simp only [Subalgebra.mem_toSubmodule, hy.2]
-        simp only [Submodule.restrictScalars_mem]
-        rw [← add_sub_cancel_right y z]
-        apply Submodule.sub_mem _ ht' hz'.2
+      refine ⟨fun ht ↦ hT_le ht, ?_⟩
+      simp only [Ideal.mem_inf]
+      rintro ⟨ht, ht'⟩
+      rw [← Submodule.restrictScalars_mem A, ← this, Submodule.mem_sup] at ht
+      obtain ⟨y, hy, z, hz, rfl⟩ := ht
+      simp only [Submodule.mem_inf, Submodule.restrictScalars_mem,
+        Subalgebra.mem_toSubmodule] at hy hz
+      apply Submodule.add_mem _ _ hz
+      suffices y = 0 by
+        simp only [this, zero_mem]
+      have hz' := Ideal.mem_inf.mp (hT_le hz)
+      apply Submodule.disjoint_def.mp hsplit.disjoint
+      simp only [Subalgebra.mem_toSubmodule, hy.2, Submodule.restrictScalars_mem]
+      exact add_sub_cancel_right y z ▸ Submodule.sub_mem _ ht' hz'.2
     suffices Submodule.span R U = J by
       ext u
       simp only [← this, Submodule.restrictScalars_mem]
-      constructor
-      · exact fun hu ↦ Submodule.subset_span hu
-      · intro hu
-        induction hu using Submodule.span_induction' with
-        | mem _ hu => exact hu
-        | zero => exact zero_mem U
-        | add x _ y _ hx' hy' => exact U.add_mem hx' hy'
-        | smul a x hx hx' =>
-          obtain ⟨b, hb, c, hc, rfl⟩ := Submodule.exists_add_eq_of_codisjoint hsplit.codisjoint a
-          simp only [Subalgebra.mem_toSubmodule, Submodule.restrictScalars_mem] at hb hc
-          rw [add_smul, smul_eq_mul]
-          rw [hU]
-          simp only [hU, Submodule.mem_sup, Submodule.mem_inf,
-              Submodule.restrictScalars_mem, Subalgebra.mem_toSubmodule] at hx'
-          obtain ⟨y, ⟨hy, hy'⟩, z, hz, rfl⟩ := hx'
-          apply Submodule.add_mem
-          · simp only [mul_add]
-            apply Submodule.add_mem
-            apply Submodule.mem_sup_left
-            simp only [Submodule.mem_inf, Submodule.restrictScalars_mem, Subalgebra.mem_toSubmodule]
-            exact ⟨J.mul_mem_left b hy, R₀.mul_mem hb hy'⟩
-            apply Submodule.mem_sup_right
-            simp only [Submodule.restrictScalars_mem]
-            exact Ideal.mul_mem_left _ b hz
-          · apply Submodule.mem_sup_right
-            simp only [smul_eq_mul, Submodule.restrictScalars_mem, mul_add]
-            apply Submodule.add_mem _ _ (Ideal.mul_mem_left _ _ hz)
-            suffices c * y ∈ T by rwa [hT', SetLike.mem_coe] at this
-            simp only [hT, Ideal.mem_inf, Set.mem_setOf_eq]
-            constructor
-            constructor
-            · exact Ideal.mul_mem_left _ _ hy
-            · exact Ideal.mul_mem_right _ _ hc
-            · intro n hn
-              rw [hI.dpow_mul_right hc]
-              apply Ideal.mul_mem_left
-              rw [← Nat.succ_pred_eq_of_ne_zero hn, pow_succ]
-              apply Ideal.mul_mem_left _ _ hy
+      refine ⟨fun hu ↦ Submodule.subset_span hu, fun hu ↦ ?_⟩
+      induction hu using Submodule.span_induction' with
+      | mem _ hu => exact hu
+      | zero => exact zero_mem U
+      | add x _ y _ hx' hy' => exact U.add_mem hx' hy'
+      | smul a x hx hx' =>
+        obtain ⟨b, hb, c, hc, rfl⟩ := Submodule.exists_add_eq_of_codisjoint hsplit.codisjoint a
+        simp only [Subalgebra.mem_toSubmodule, Submodule.restrictScalars_mem] at hb hc
+        rw [add_smul, smul_eq_mul]
+        simp only [hU, Submodule.mem_sup, Submodule.mem_inf,
+            Submodule.restrictScalars_mem, Subalgebra.mem_toSubmodule] at hx'
+        obtain ⟨y, ⟨hy, hy'⟩, z, hz, rfl⟩ := hx'
+        apply Submodule.add_mem
+        · simp only [mul_add]
+          exact Submodule.add_mem _
+            (Submodule.mem_sup_left ⟨J.mul_mem_left b hy, R₀.mul_mem hb hy'⟩)
+            (Submodule.mem_sup_right (Ideal.mul_mem_left _ b hz))
+        · apply Submodule.mem_sup_right
+          simp only [smul_eq_mul, Submodule.restrictScalars_mem, mul_add]
+          apply Submodule.add_mem _ _ (Ideal.mul_mem_left _ _ hz)
+          suffices c * y ∈ T by rwa [hT', SetLike.mem_coe] at this
+          simp only [hT, Ideal.mem_inf, Set.mem_setOf_eq]
+          refine ⟨⟨Ideal.mul_mem_left _ _ hy, Ideal.mul_mem_right _ _ hc⟩, fun _ hn ↦ ?_⟩
+          rw [hI.dpow_mul_right hc]
+          apply Ideal.mul_mem_left
+          rw [← Nat.succ_pred_eq_of_ne_zero hn, pow_succ]
+          exact Ideal.mul_mem_left _ _ hy
     apply le_antisymm
     · rw [Submodule.span_le, hU]
       intro j hj
       simp only [SetLike.mem_coe, Submodule.mem_sup, Submodule.mem_inf,
         Submodule.restrictScalars_mem, Subalgebra.mem_toSubmodule] at hj
       obtain ⟨y, ⟨hy, _⟩, z, hz, rfl⟩ := hj
-      simp only [SetLike.mem_coe]
       exact Submodule.add_mem _ hy (inf_le_left (b := I) (hT_le hz))
-    · simp only [hJ, SetLike.coe_sort_coe, span_union, submodule_span_eq, sup_le_iff]
+    · simp only [hJ, SetLike.coe_sort_coe, Ideal.span_union, submodule_span_eq, sup_le_iff]
       constructor
       · rw [Ideal.span_le]
         rintro a ⟨⟨b, hb⟩, hb', rfl⟩
-        simp only [SetLike.mem_coe]
-        apply Ideal.subset_span
-        apply Submodule.mem_sup_left
-        simp only [Submodule.mem_inf, Submodule.restrictScalars_mem, Subalgebra.mem_toSubmodule, hb,
-          and_true]
+        apply Ideal.subset_span (Submodule.mem_sup_left _)
+        simp only [Submodule.mem_inf, restrictScalars_mem, Subalgebra.mem_toSubmodule, hb, and_true]
         rw [hJ]
-        refine ⟨?_, hb⟩
-        apply Ideal.subset_span
-        apply Set.mem_union_left
-        use ⟨b, hb⟩
+        exact ⟨Ideal.subset_span (Set.mem_union_left _ ⟨⟨b, hb⟩, hb', rfl⟩) , hb⟩
       · rw [Ideal.span_le]
         rintro a ⟨⟨b, hb⟩, hb', rfl⟩
-        simp only [SetLike.mem_coe]
-        apply Ideal.subset_span
-        apply Submodule.mem_sup_right
-        simp only [Submodule.restrictScalars_mem]
+        apply Ideal.subset_span (Submodule.mem_sup_right _)
+        simp only [restrictScalars_mem]
         suffices b ∈ T by rwa [hT'] at this
         simp only [hT, Set.mem_setOf_eq]
-        exact ⟨Ideal.mem_inf.mpr ⟨hJ ▸ subset_span (Set.mem_union_right _ ⟨⟨b, hb⟩, hb', rfl⟩), hb⟩,
-          fun n hn ↦ H _ hb' n hn⟩
+        exact ⟨Ideal.mem_inf.mpr ⟨hJ ▸ Ideal.subset_span
+          (Set.mem_union_right _ ⟨⟨b, hb⟩, hb', rfl⟩), hb⟩, fun n hn ↦ H _ hb' n hn⟩
 
-theorem Ideal.map_coe_toRingHom
+-- Unused
+/- theorem Ideal.map_coe_toRingHom
   {A : Type*} [CommRing A] {R S : Type*} [CommRing R] [CommRing S]
   [Algebra A R] [Algebra A S] (f : R →ₐ[A] S)
   (I : Ideal R) : Ideal.map f I = Ideal.map f.toRingHom I := by
-  rfl
+  rfl -/
 
 example (A : Type*) [CommRing A]
     (R : Type*) [CommRing R] [Algebra A R]
@@ -1127,13 +1024,13 @@ example (A : Type*) [CommRing A]
     Ideal.IsAugmentation (T₀) (K A I J) := sorry
 
 -- Roby, lemma 7
-theorem CondQ_and_condTFree_imply_condT (A : Type*) [CommRing A]
-    (hQ : CondQ A) (hT_free : CondTFree A) : CondT A := by
+theorem CondQ_and_condTFree_imply_condT (A : Type*) [CommRing A] (hQ : CondQ A)
+    (hT_free : CondTFree A) : CondT A := by
   intro R' _ _ I' hI' R₀' hIR₀' S' _ _ J' hJ' S₀' hJS₀'
   obtain ⟨R, _, _, I, hI, R₀, hIR₀, f, hfI, hfR₀, hf, hfDP, hR_free⟩ := hQ R' I' hI' R₀' hIR₀'
   obtain ⟨S, _, _, J, hJ, S₀, hJS₀, g, hgJ, hgS₀, hg, hgDP, hS_free⟩ := hQ S' J' hJ' S₀' hJS₀'
-  apply condτ_rel A hIR₀ hI hJS₀ hJ hIR₀' hI' hJS₀' hJ' f hf hfDP hfR₀.symm hfI.symm g hg hgDP hgS₀.symm hgJ.symm
-  apply hT_free R
+  exact condτ_rel A hIR₀ hI hJS₀ hJ hIR₀' hI' hJS₀' hJ' f hf hfDP hfR₀.symm hfI.symm g hg hgDP
+    hgS₀.symm hgJ.symm (hT_free R _ _ _)
 
 -- Roby, lemma 8
 -- TODO: remove (the proof in Roby 65 is incorrect)
@@ -1157,28 +1054,26 @@ theorem condT_and_condD_imply_condD (A : Type u) [CommRing A] [DecidableEq A]
     exact IsCompl.symm { disjoint := fun ⦃x⦄ a a_1 ↦ a, codisjoint := fun ⦃x⦄ a a ↦ a }
   obtain ⟨hD, hhD1, hhD2⟩ := condT R hR hRa (DividedPowerAlgebra A M) hM hMa -/
 
-  /- Note (2024-07-12) — Roby claims that there is an “obvious” isomorphism
-    e : D ≃ₐ[R] DividedPowerAlgebra R M
-  that maps the ideal `K` t the augmentation ideal `augIdeal R M`.
-  Using this isomorphism, the divided powers `hD` on `D` would
-  be transfered to `DividedPowerAlgebra R M` to give the desired
-  divided power structure.
-  Unfortunately, [Roby, 1963, III.3] `dpScalarExtensionEquiv` proves
-  something else, namely
-      D ≃ₐ[R] DividedPowerAlgebra R (R ⊗[A] M)
-  I don't know how this can be repaired…
-
-  Note (2024-07-15) — When R = ℤ, Roby's construction of divided powers on
-  the augmentation ideal of DividedPowerAlgebra R M splits into two cases:
-  - he first considers the case where M is free.
-  - then he writes M as a quotient of a free R-module L and invokes
+/- Note (2024-07-12) — Roby claims that there is an “obvious” isomorphism
+`e : D ≃ₐ[R] DividedPowerAlgebra R M` that maps the ideal `K` to the augmentation ideal
+`augIdeal R M`. Using this isomorphism, the divided powers `hD` on `D` would
+be transfered to `DividedPowerAlgebra R M` to give the desired divided power structure.
+Unfortunately, [Roby, 1963, III.3] `dpScalarExtensionEquiv` proves something else, namely
+`D ≃ₐ[R] DividedPowerAlgebra R (R ⊗[A] M)`
+I don't know how this can be repaired…
+
+Note (2024-07-15) — When `R = ℤ`, Roby's construction of divided powers on the augmentation ideal
+of `DividedPowerAlgebra R M` splits into two cases:
+- he first considers the case where `M` is free.
+- then he writes `M` as a quotient of a free `R`-module `L` and invokes
   his earlier paper for a description of the kernel of the natural morphism
-    DividedPowerAlgebra R L →ₐ[R] DividedPowerAlgebra R M
+    `DividedPowerAlgebra R L →ₐ[R] DividedPowerAlgebra R M`.
   It seems that this approach could work in general. I hope so…
 
   -/
 
--- Roby, lemma 9 is in roby9 (other file)
+-- Roby, lemma 9 is in `RobyLemma9.lean`.
+
 -- Roby, lemma 10
 theorem condT_implies_condTFree (A : Type*) [CommRing A] (R : Type*) [CommRing R] [Algebra A R]
     (hA : CondT A) : CondTFree R :=
@@ -1198,16 +1093,15 @@ theorem CondQ_int : CondQ ℤ :=
 theorem condT_int : CondT ℤ :=
   CondQ_and_condTFree_imply_condT ℤ CondQ_int condTFree_int
 
+-- We need an alternative proof
 theorem condD_holds (A : Type*) [CommRing A] [DecidableEq A] : CondD A :=
-  condT_and_condD_imply_condD ℤ condT_int condD_int A
+  sorry --condT_and_condD_imply_condD ℤ condT_int condD_int A
 
 theorem condTFree_holds (A : Type*) [CommRing A] : CondTFree A :=
   condT_implies_condTFree ℤ A condT_int
 
 theorem CondQ_holds (A : Type*) [CommRing A] [DecidableEq A] : CondQ A :=
   condTFree_and_condD_to_condQ (condTFree_holds A) (condD_holds A)
-  --sorry
-  -- T_free_and_D_to_Q A (condTFree_holds A) (condD_holds A)
 
 theorem condT_holds (A : Type*) [CommRing A] [DecidableEq A] : CondT A :=
   CondQ_and_condTFree_imply_condT A (CondQ_holds A) (condTFree_holds A)
@@ -1221,6 +1115,7 @@ open DividedPowers DividedPowerAlgebra
 
 -- namespace divided_power_algebra
 -- Part of Roby65 Thm 1
+/-- The divided power structure on the augmentation ideal. -/
 def dividedPowers' (A : Type u) [CommRing A] [DecidableEq A] (M : Type u) [AddCommGroup M]
     [Module A M] : DividedPowers (augIdeal A M) :=
   (condD_holds A M).choose
@@ -1234,47 +1129,34 @@ theorem dp_comp (A : Type u) [CommRing A] [DecidableEq A] (M : Type u) [AddCommG
     dpow (dividedPowers' A M) m (dp A n x) = ↑(Nat.uniformBell m n) * dp A (m * n) x := by
   erw [← (condD_holds A M).choose_spec, dpow_comp _ hn (ι_mem_augIdeal A M x), dpow_ι]
 
-theorem roby_theorem_2 (R : Type u) [CommRing R]  [DecidableEq R]
-    (M : Type u) [AddCommGroup M] [Module R M]
-    {A : Type u} [CommRing A] [Algebra R A] {I : Ideal A} (hI : DividedPowers I)
+theorem roby_theorem_2 (R : Type u) [CommRing R]  [DecidableEq R] (M : Type u) [AddCommGroup M]
+    [Module R M] {A : Type u} [CommRing A] [Algebra R A] {I : Ideal A} (hI : DividedPowers I)
     {φ : M →ₗ[R] A} (hφ : ∀ m, φ m ∈ I) :
-    IsDPMorphism (dividedPowers' R M) hI (DividedPowerAlgebra.lift hI φ hφ) := by
-  apply cond_D_uniqueness
-  intro m n
-  rw [dpow_ι]
-
-lemma ι_comp_mem_augIdeal (R : Type u) [CommRing R]
-    {M : Type v} [AddCommGroup M] [Module R M]
-    (S : Type w) [CommRing S] [DecidableEq S] [Algebra R S]
-    {N : Type w} [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[R] N)
-    (m : M) : ((ι S N).restrictScalars R).comp f m ∈ augIdeal S N := by
+    IsDPMorphism (dividedPowers' R M) hI (DividedPowerAlgebra.lift hI φ hφ) :=
+  cond_D_uniqueness _ (fun _ _ ↦  dpow_ι _ _ _ _) _ _ _
+
+lemma ι_comp_mem_augIdeal (R : Type u) [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
+    (S : Type w) [CommRing S] [DecidableEq S] [Algebra R S] {N : Type w} [AddCommGroup N]
+    [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[R] N) (m : M) :
+    ((ι S N).restrictScalars R).comp f m ∈ augIdeal S N := by
   simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars,
-      Function.comp_apply, ι_mem_augIdeal S N (f m)]
-
-theorem lift_eq_DPLift (R : Type u) [CommRing R]
-    {M : Type v} [AddCommGroup M] [Module R M]
-    (S : Type w) [CommRing S] [DecidableEq S] [Algebra R S]
-    {N : Type w} [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[R] N) :
-      LinearMap.lift S f =
-        DividedPowerAlgebra.lift (dividedPowers' S N)
-          (((ι S N).restrictScalars R).comp f) (ι_comp_mem_augIdeal R S f) := by
-  apply DividedPowerAlgebra.algHom_ext
-  intro n m
-  simp only [lift_apply_dp, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
-    Function.comp_apply]
-  simp only [DividedPowerAlgebra.LinearMap.lift_apply_dp]
-  simp only [ι, LinearMap.coe_mk, AddHom.coe_mk]
-  rw [dp_comp _ _ _ _ Nat.one_ne_zero]
-  simp only [uniformBell_one', Nat.cast_one, mul_one, one_mul]
-
-theorem roby_prop_8 (R : Type u) [DecidableEq R] [CommRing R]
-    {M : Type u} [AddCommGroup M] [Module R M]
-    (S : Type u) [DecidableEq S] [CommRing S] [Algebra R S]
-    {N : Type u} [AddCommGroup N] [Module R N] [Module S N]
-    [IsScalarTower R S N] (f : M →ₗ[R] N) :
-    IsDPMorphism (dividedPowers' R M) (dividedPowers' S N) (LinearMap.lift S f) := by
-  rw [lift_eq_DPLift R S f]
-  exact roby_theorem_2 R M (dividedPowers' S N) (ι_comp_mem_augIdeal R S f)
+    Function.comp_apply, ι_mem_augIdeal S N (f m)]
+
+theorem lift_eq_DPLift (R : Type u) [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
+    (S : Type w) [CommRing S] [DecidableEq S] [Algebra R S] {N : Type w} [AddCommGroup N]
+    [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[R] N) :
+    LinearMap.lift S f = DividedPowerAlgebra.lift (dividedPowers' S N)
+      (((ι S N).restrictScalars R).comp f) (ι_comp_mem_augIdeal R S f) := by
+  refine DividedPowerAlgebra.algHom_ext (fun _ _ ↦ ?_)
+  simp only [lift_apply_dp, LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply,
+    DividedPowerAlgebra.LinearMap.lift_apply_dp, ι, LinearMap.coe_mk, AddHom.coe_mk,
+    dp_comp _ _ _ _ Nat.one_ne_zero, uniformBell_one', Nat.cast_one, mul_one, one_mul]
+
+theorem roby_prop_8 (R : Type u) [DecidableEq R] [CommRing R] {M : Type u} [AddCommGroup M]
+    [Module R M] (S : Type u) [DecidableEq S] [CommRing S] [Algebra R S] {N : Type u}
+    [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[R] N) :
+    IsDPMorphism (dividedPowers' R M) (dividedPowers' S N) (LinearMap.lift S f) :=
+  lift_eq_DPLift R S f ▸ roby_theorem_2 R M (dividedPowers' S N) (ι_comp_mem_augIdeal R S f)
 
 end Roby_section10
 
diff --git a/DividedPowers/DPAlgebra/Graded/GradeOne.lean b/DividedPowers/DPAlgebra/Graded/GradeOne.lean
index 3d11ffe..662abd3 100644
--- a/DividedPowers/DPAlgebra/Graded/GradeOne.lean
+++ b/DividedPowers/DPAlgebra/Graded/GradeOne.lean
@@ -36,7 +36,7 @@ instance [hR : DecidableEq R] : DecidablePred (fun x ↦ x ∈ kerIdeal R M) :=
 
 variable (M)
 
-/-- The canonical map from `DividedPowerAlgebr R M` into `TrivSqZeroExt R M`
+/-- The canonical map from `DividedPowerAlgebra R M` into `TrivSqZeroExt R M`
   that sends `DividedPowerAlgebra.ι` to `TrivSqZeroExt.inr`. -/
 def toTrivSqZeroExt : DividedPowerAlgebra R M →ₐ[R] TrivSqZeroExt R M :=
   lift (DividedPowers.OfSquareZero.dividedPowers
@@ -86,9 +86,8 @@ theorem grade_one_eq_span :
     rintro p ⟨m, rfl⟩
     exact dp_mem_grade R M 1 m
 
-theorem grade_one_eq_span' :
-    (⊤ : Submodule R (grade R M 1)) =
-      Submodule.span R (Set.range fun m => ⟨dp R 1 m, dp_mem_grade R M 1 m⟩) := by
+theorem grade_one_eq_span' : (⊤ : Submodule R (grade R M 1)) =
+    Submodule.span R (Set.range fun m => ⟨dp R 1 m, dp_mem_grade R M 1 m⟩) := by
   apply Submodule.map_injective_of_injective (grade R M 1).injective_subtype
   rw [Submodule.map_subtype_top, Submodule.map_span]
   simp_rw [grade_one_eq_span R M, ← Set.range_comp]
@@ -112,7 +111,7 @@ theorem deg_one_right_inv :
   ext
   dsimp only
   rw [← ι_def m, toTrivSqZeroExt_ι, ← ι_def, snd_inr, decompose_of_mem_same]
-  apply ι_mem_grade_one
+  exact ι_mem_grade_one _ _
 
 theorem deg_one_left_inv :
     LeftInverse (fun x : grade R M 1 => (toTrivSqZeroExt R M x.1).snd) (proj' R M 1 ∘ ι R M) := by
@@ -121,11 +120,10 @@ theorem deg_one_left_inv :
   rw [← TrivSqZeroExt.snd_inr R m, ← ι_def]
   apply congr_arg
   rw [snd_inr, decompose_of_mem_same, toTrivSqZeroExt_ι]
-  apply ι_mem_grade_one
+  exact ι_mem_grade_one _ _
 
 /-- The linear equivalence `(proj' R M 1).comp (ι R M) : M → grade R M 1`. -/
-def linearEquivDegreeOne :
-    LinearEquiv (RingHom.id R) M (grade R M 1) where
+def linearEquivDegreeOne : LinearEquiv (RingHom.id R) M (grade R M 1) where
   toFun         := (proj' R M 1).comp (ι R M)
   invFun x      := TrivSqZeroExt.sndHom R M (toTrivSqZeroExt R M x.1)
   map_add' x y  := by simp only [map_add]
@@ -136,11 +134,11 @@ def linearEquivDegreeOne :
 lemma ι_toTrivSqZeroExt_of_mem_grade_one {a} (ha : a ∈ grade R M 1) :
     (ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a)) = a := by
   suffices ⟨(ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a)), ι_mem_grade_one R _⟩ =
-    (⟨a, ha⟩ : grade R M 1) by
+      (⟨a, ha⟩ : grade R M 1) by
     simpa only [sndHom_apply, Subtype.mk.injEq] using this
   apply (linearEquivDegreeOne R M).symm.injective
-  rw [← LinearEquiv.invFun_eq_symm]
-  simp only [linearEquivDegreeOne, toTrivSqZeroExt_ι, sndHom_apply, snd_inr]
+  simp only [← LinearEquiv.invFun_eq_symm, linearEquivDegreeOne, toTrivSqZeroExt_ι,
+    sndHom_apply, snd_inr]
 
 theorem mem_grade_one_iff (a : DividedPowerAlgebra R M) :
     a ∈ grade R M 1 ↔ ∃ m, a = ι R M m := by
diff --git a/DividedPowers/DPAlgebra/Graded/GradeZero.lean b/DividedPowers/DPAlgebra/Graded/GradeZero.lean
index 77c27d9..49e3b34 100644
--- a/DividedPowers/DPAlgebra/Graded/GradeZero.lean
+++ b/DividedPowers/DPAlgebra/Graded/GradeZero.lean
@@ -5,7 +5,6 @@ Authors: Antoine Chambert-Loir, María Inés de Frutos-Fernández
 -/
 import DividedPowers.DPAlgebra.Graded.Basic
 import DividedPowers.ForMathlib.RingTheory.AugmentationIdeal
-import Mathlib.LinearAlgebra.TensorAlgebra.Basic
 
 universe u v
 
@@ -33,7 +32,6 @@ end MvPolynomial
 
 namespace DividedPowerAlgebra
 
-
 open DirectSum Finset Function Ideal Ideal.Quotient MvPolynomial RingEquiv RingQuot TrivSqZeroExt
 
 section CommSemiring
@@ -358,9 +356,7 @@ theorem isAugmentation [DecidableEq M] :
   · rw [Submodule.disjoint_def]
     intro x
     simp only [Subalgebra.mem_toSubmodule, Algebra.mem_bot, Set.mem_range, Subtype.exists,
-      Submodule.restrictScalars_mem, forall_exists_index]
-    simp only [gradeZeroSubalgebra_eq_bot, Algebra.mem_bot]
-    simp only [Set.mem_range, forall_exists_index]
+      Submodule.restrictScalars_mem, forall_exists_index, gradeZeroSubalgebra_eq_bot]
     rintro x y ⟨rfl⟩ ⟨rfl⟩ hy
     change algebraMap R _ y ∈ augIdeal R M at hy
     rw [mem_augIdeal_iff] at hy
diff --git a/DividedPowers/DPAlgebra/RobyLemma9.lean b/DividedPowers/DPAlgebra/RobyLemma9.lean
index 590e276..8ea9467 100644
--- a/DividedPowers/DPAlgebra/RobyLemma9.lean
+++ b/DividedPowers/DPAlgebra/RobyLemma9.lean
@@ -29,20 +29,6 @@ theorem AlgHom.ker_eq_ideal_iff {R A B : Type*} [CommRing R] [CommRing A] [Algeb
     RingHom.ker f = I ↔
       ∃ h : I ≤ RingHom.ker f, Function.Injective (Ideal.Quotient.liftₐ I f h) :=
     RingHom.ker_eq_ideal_iff f.toRingHom I
-  /- have : RingHom.ker f = RingHom.ker f.toRingHom := rfl
-  constructor
-  · intro hI; use le_of_eq hI.symm
-    suffices h : Function.Injective (Ideal.Quotient.lift I f.toRingHom (le_of_eq hI.symm)) by
-      intro x y hxy; apply h
-      simpa only [Ideal.Quotient.liftₐ_apply] using hxy
-    apply RingHom.lift_injective_of_ker_le_ideal
-    rw [← hI, ← this]
-  · rintro ⟨hI, h⟩
-    rw [this]; rw [RingHom.ker_eq_ideal_iff]
-    rw [this] at hI ; use hI
-    intro x y hxy
-    apply h
-    simpa only [Ideal.Quotient.liftₐ_apply] using hxy -/
 
 end AlgHom
 
@@ -56,19 +42,11 @@ end AlgHom
   much slower.
   -/
 
-variable (R : Type*) [CommRing R] (S : Type*) [CommRing S]
+variable (R : Type*) [CommRing R] (S : Type*) [CommRing S] [Algebra R S]
 
-variable (M : Type*) [CommRing M] [Algebra R M] [Algebra S M]
-  (N : Type*) [CommRing N] [Algebra R N] [Algebra S N]
+variable (M : Type*) [CommRing M] [Algebra R M] [Algebra S M] [IsScalarTower R S M]
+  (N : Type*) [CommRing N] [Algebra R N]
 
-variable [Algebra R S] [IsScalarTower R S M]
-
-/-- The ideal of `M ⊗[R] N` generated by the elements of the form
-  `(r • 1)) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (r •1)`, for `r : R`. -/
-def kerφ : Ideal (M ⊗[R] N) :=
-  Ideal.span ((fun r : S => (r • (1 : M)) ⊗ₜ[R] (1 : N) - (1 : M) ⊗ₜ[R] (r • (1 : N))) '' ⊤)
-
-omit [Algebra S N] in
 lemma mkₐ_smul_one_tmul_one'' (s : S) {B : Type*} [CommRing B] [Algebra S B]
     (f : M ⊗[R] N →ₐ[S] B) :
     f ((s • (1 : M)) ⊗ₜ[R] (1 : N)) = s • (1 : B) := by
@@ -76,19 +54,24 @@ lemma mkₐ_smul_one_tmul_one'' (s : S) {B : Type*} [CommRing B] [Algebra S B]
     rw [this, map_smul, map_one]
   rfl
 
-lemma mkₐ_smul_one_tmul_one' (s : S) :
-    (Ideal.Quotient.mkₐ S (kerφ R S M N)) ((s • (1 : M)) ⊗ₜ[R] (1 : N)) =
-      s • (1 : M ⊗[R] N ⧸ kerφ R S M N) := by
-  apply mkₐ_smul_one_tmul_one''
-
-omit [Algebra S N] in
 lemma mkₐ_smul_one_tmul_one (s : S) (I : Ideal (M ⊗[R] N)) :
-    (Ideal.Quotient.mkₐ S I) ((s • (1 : M)) ⊗ₜ[R] (1 : N)) =
-      s • (1 : M ⊗[R] N ⧸ I) := by
+    (Ideal.Quotient.mkₐ S I) ((s • (1 : M)) ⊗ₜ[R] (1 : N)) = s • (1 : M ⊗[R] N ⧸ I) := by
   suffices (s • (1 : M)) ⊗ₜ[R] (1 : N) = s • (1 : M ⊗[R] N) by
     rw [this, map_smul, map_one]
   rfl
 
+variable [Algebra S N]
+
+/-- The ideal of `M ⊗[R] N` generated by the elements of the form
+  `(r • 1)) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (r •1)`, for `r : R`. -/
+def kerφ : Ideal (M ⊗[R] N) :=
+  Ideal.span ((fun r : S => (r • (1 : M)) ⊗ₜ[R] (1 : N) - (1 : M) ⊗ₜ[R] (r • (1 : N))) '' ⊤)
+
+lemma mkₐ_smul_one_tmul_one' (s : S) :
+    (Ideal.Quotient.mkₐ S (kerφ R S M N)) ((s • (1 : M)) ⊗ₜ[R] (1 : N)) =
+      s • (1 : M ⊗[R] N ⧸ kerφ R S M N) := by
+  apply mkₐ_smul_one_tmul_one''
+
 lemma mkₐ_one_tmul_smul_one (s : S) :
     (Ideal.Quotient.mk (kerφ R S M N)) (1 ⊗ₜ[R] (s • 1)) = s • 1 := by
   rw [← (Ideal.Quotient.mk (kerφ R S M N)).map_one, ← Ideal.Quotient.mkₐ_eq_mk S, ← map_smul]
@@ -97,30 +80,8 @@ lemma mkₐ_one_tmul_smul_one (s : S) :
   rw [Ideal.Quotient.eq]
   exact Ideal.subset_span ⟨s, Set.mem_univ s, rfl⟩
 
-variable [IsScalarTower R S N]
-
 open Algebra.TensorProduct TensorProduct
 
-/-- The morphism `M ⊗[R] N →ₐ[R] M ⊗[S] N` from Roby65, Lemma 5. -/
-noncomputable def φ : M ⊗[R] N →ₐ[R] M ⊗[S] N :=
-  Algebra.TensorProduct.productMap
-    Algebra.TensorProduct.includeLeft
-    (Algebra.TensorProduct.includeRight.restrictScalars R)
-
-theorem φ_apply (m : M) (n : N) : φ R S M N (m ⊗ₜ[R] n) = m ⊗ₜ[S] n := by
-  simp only [φ, productMap_apply_tmul, AlgHom.coe_restrictScalars', includeLeft_apply,
-    includeRight_apply, tmul_mul_tmul, _root_.mul_one, _root_.one_mul]
-
-theorem φ_surjective : Function.Surjective (φ R S M N) := by
-  intro z
-  induction z using TensorProduct.induction_on with
-  | zero => use 0; simp only [map_zero]
-  | tmul m n => use m ⊗ₜ n; simp only [φ_apply]
-  | add x y hx hy =>
-      obtain ⟨a, rfl⟩ := hx
-      obtain ⟨b, rfl⟩ := hy
-      exact ⟨a + b, map_add _ _ _⟩
-
 noncomputable def ψLeft : M →ₐ[S] M ⊗[R] N ⧸ kerφ R S M N := {
   ((Ideal.Quotient.mkₐ S (kerφ R S M N)).restrictScalars R).comp
     Algebra.TensorProduct.includeLeft with
@@ -143,7 +104,6 @@ noncomputable def ψRight : N →ₐ[S] M ⊗[R] N ⧸ kerφ R S M N :=
 noncomputable def ψ : M ⊗[S] N →ₐ[S] M ⊗[R] N ⧸ kerφ R S M N :=
   productMap (ψLeft R S M N) (ψRight R S M N)
 
-omit [IsScalarTower R S N] in
 theorem ψ_apply (m : M) (n : N) :
     ψ R S M N (m ⊗ₜ[S] n) = Ideal.Quotient.mk (kerφ R S M N) (m ⊗ₜ[R] n) := by
   simp only [ψ, ψLeft, AlgHom.toRingHom_eq_coe, ψRight, productMap_apply_tmul, AlgHom.coe_mk,
@@ -151,6 +111,29 @@ theorem ψ_apply (m : M) (n : N) :
     Function.comp_apply, includeLeft_apply, includeRight_apply, ← RingHom.map_mul, tmul_mul_tmul,
     mul_one, one_mul]
 
+section IsScalarTower
+
+variable [IsScalarTower R S N]
+
+/-- The morphism `M ⊗[R] N →ₐ[R] M ⊗[S] N` from Roby65, Lemma 5. -/
+noncomputable def φ : M ⊗[R] N →ₐ[R] M ⊗[S] N :=
+  Algebra.TensorProduct.productMap Algebra.TensorProduct.includeLeft
+    (Algebra.TensorProduct.includeRight.restrictScalars R)
+
+theorem φ_apply (m : M) (n : N) : φ R S M N (m ⊗ₜ[R] n) = m ⊗ₜ[S] n := by
+  simp only [φ, productMap_apply_tmul, AlgHom.coe_restrictScalars', includeLeft_apply,
+    includeRight_apply, tmul_mul_tmul, _root_.mul_one, _root_.one_mul]
+
+theorem φ_surjective : Function.Surjective (φ R S M N) := by
+  intro z
+  induction z using TensorProduct.induction_on with
+  | zero => use 0; simp only [map_zero]
+  | tmul m n => use m ⊗ₜ n; simp only [φ_apply]
+  | add x y hx hy =>
+      obtain ⟨a, rfl⟩ := hx
+      obtain ⟨b, rfl⟩ := hy
+      exact ⟨a + b, map_add _ _ _⟩
+
 /-- We prove that the kernel of `φ` is equal to `kerφ` (see Roby65, Lemma 9). -/
 theorem kerφ_eq : RingHom.ker (φ R S M N).toRingHom = kerφ R S M N := by
   suffices h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom by
@@ -173,3 +156,5 @@ theorem kerφ_eq : RingHom.ker (φ R S M N).toRingHom = kerφ R S M N := by
   simp only [SetLike.mem_coe, RingHom.sub_mem_ker_iff,AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom,
     φ_apply, TensorProduct.tmul_smul]
   rfl
+
+end IsScalarTower
diff --git a/DividedPowers/ForMathlib/RingTheory/AugmentationIdeal.lean b/DividedPowers/ForMathlib/RingTheory/AugmentationIdeal.lean
index 4b3b77b..a19d882 100644
--- a/DividedPowers/ForMathlib/RingTheory/AugmentationIdeal.lean
+++ b/DividedPowers/ForMathlib/RingTheory/AugmentationIdeal.lean
@@ -519,7 +519,7 @@ def Ideal.IsAugmentation (R : Type*) [CommSemiring R]
     {A : Type*} [CommSemiring A] [Algebra R A] (J : Ideal A) : Prop :=
   IsCompl (Subalgebra.toSubmodule (⊥ : Subalgebra R A)) (J.restrictScalars R)
 
-theorem Ideal.isAugmentation_subalgebra_iff (A : Type*) [CommSemiring A]
+theorem Ideal.isAugmentation_subalgebra_iff {A : Type*} [CommSemiring A]
     {R : Type*} [CommSemiring R] [Algebra A R]
     {S : Subalgebra A R} {I : Ideal R} :
     I.IsAugmentation S ↔