make n implicit in SubDPIdeal

DividedPowers/DPAlgebra/Dpow.lean

@@ -998,7 +998,7 @@ theorem roby_prop_4
     apply inf_le_right (a := J)
     simp only [ge_iff_le, le_refl, inf_of_le_left]
     apply inf_le_left (b := I)
-    apply hJ'.dpow_mem n hn
+    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⟩)
   · intro H
@@ -1034,10 +1034,10 @@ theorem roby_prop_4
           exact inf_le_right (a := J) (hT_le hx)
     suffices T = J ⊓ I by exact {
       isSubideal := inf_le_right
-      dpow_mem := fun n hn a ha ↦ by
+      dpow_mem := fun hn a ha ↦ by
         simp only [Ideal.mem_inf] at ha ⊢
         suffices ha' : a ∈ T by
-          exact ⟨ha'.2 n hn, hI.dpow_mem hn ha.2⟩
+          exact ⟨ha'.2 _ hn, hI.dpow_mem hn ha.2⟩
         simp only [this, Submodule.inf_coe, Set.mem_inter_iff, SetLike.mem_coe, ha.2, ha.1, and_true] }
     set U := (J.restrictScalars A ⊓ Subalgebra.toSubmodule R₀) ⊔
       (Ideal.span T).restrictScalars A with hU

DividedPowers/DPAlgebra/Envelope.lean

@@ -160,7 +160,7 @@ theorem J12_IsSubDPIdeal [DecidableEq B] :
     IsSubDPIdeal (DividedPowerAlgebra.dividedPowers' B J)
       (J12 hI J hIJ ⊓ DividedPowerAlgebra.augIdeal B J) where
   isSubideal := inf_le_right
-  dpow_mem   := fun n hn x hx ↦ by
+  dpow_mem   := fun hn x hx ↦ by
     have hJ12 : J12 hI J hIJ ⊓ augIdeal B J = (J1 J  ⊓ augIdeal B J) + J2 hI J hIJ := sorry
     --simp only [dividedPowers', Subtype.forall, mem_inf]
     rw [hJ12, Submodule.add_eq_sup, Submodule.mem_sup'] at hx
@@ -184,7 +184,7 @@ theorem J12_IsSubDPIdeal [DecidableEq B] :
       have hss : J1 J * augIdeal B ↥J ≤ J12 hI J hIJ ⊓ augIdeal B ↥J :=
         heq ▸ inf_le_inf_right (augIdeal B ↥J) le_sup_left
       rw [heq] at hx1
-      exact hss (hsub.dpow_mem n hn hx1)
+      exact hss (hsub.dpow_mem hn hx1)
     · sorry/- revert n
       induction x2 using DividedPowerAlgebra.induction_on with
       | h_C b =>

DividedPowers/IdealAdd.lean

@@ -503,11 +503,11 @@ theorem dpow_unique (hsup : DividedPowers (I + J))
 
 lemma isDPMorphism_left (hIJ : ∀ {n : ℕ}, ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a) :
     hI.IsDPMorphism (IdealAdd.dividedPowers hI hJ hIJ) (RingHom.id A):=
-  ⟨by simp only [Ideal.map_id]; exact le_sup_left, fun _ ha ↦ dpow_eq_of_mem_left hI hJ hIJ ha⟩
+  ⟨by simp only [Ideal.map_id]; exact le_sup_left, fun _ ↦ dpow_eq_of_mem_left hI hJ hIJ⟩
 
 lemma isDPMorphism_right (hIJ : ∀ {n : ℕ}, ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a) :
     hJ.IsDPMorphism (IdealAdd.dividedPowers hI hJ hIJ) (RingHom.id A) :=
-  ⟨by simp only [Ideal.map_id]; exact le_sup_right, fun _ ha ↦ dpow_eq_of_mem_right hI hJ hIJ ha⟩
+  ⟨by simp only [Ideal.map_id]; exact le_sup_right, fun _ ↦ dpow_eq_of_mem_right hI hJ hIJ⟩
 
 end IdealAdd
 

DividedPowers/RatAlgebra.lean

@@ -227,7 +227,7 @@ namespace RatAlgebra
 variable {R : Type*} [CommSemiring R] (I : Ideal R) [DecidablePred (fun x ↦ x ∈ I)]
 
 /-- The family `ℕ → R → R` given by `dpow n x = x ^ n / n!`. -/
-noncomputable def dpow : ℕ → R → R := fun n => OfInvertibleFactorial.dpow I n
+noncomputable def dpow : ℕ → R → R := OfInvertibleFactorial.dpow I
 
 variable {I}
 
@@ -263,7 +263,7 @@ omit [DecidablePred fun x ↦ x ∈ I] in
 /-- If `I` is an ideal in a `ℚ`-algebra `A`, then the divided power structure on `I` given by
   `dpow n x = x ^ n / n!` is the only possible one. -/
 theorem dpow_eq_inv_fact_smul (hI : DividedPowers I) {n : ℕ} {x : R} (hx : x ∈ I) :
-    hI.dpow n x = (inverse (Nat.factorial n : ℚ) : ℚ) • x ^ n := by
+    hI.dpow n x = (inverse (n.factorial : ℚ)) • x ^ n := by
   rw [inverse_eq_inv', ← factorial_mul_dpow_eq_pow hI hx, ← smul_eq_mul, ← smul_assoc]
   nth_rewrite 1 [← one_smul R (hI.dpow n x)]
   congr

DividedPowers/SubDPIdeal.lean

@@ -70,7 +70,7 @@ namespace DividedPowers
 structure IsSubDPIdeal {A : Type*} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I)
     (J : Ideal A) : Prop where
   isSubideal : J ≤ I
-  dpow_mem : ∀ (n : ℕ) (_: n ≠ 0) {j : A} (_ : j ∈ J), hI.dpow n j ∈ J
+  dpow_mem : ∀ {n : ℕ} (_: n ≠ 0) {j : A} (_ : j ∈ J), hI.dpow n j ∈ J
 section  IsSubDPIdeal
 
 namespace IsSubDPIdeal
@@ -81,22 +81,22 @@ open Ideal
 
 theorem self : IsSubDPIdeal hI I where
   isSubideal := le_rfl
-  dpow_mem _ hn _ ha := hI.dpow_mem hn ha
+  dpow_mem hn _ ha := hI.dpow_mem hn ha
 
 def dividedPowers {J : Ideal A} (hJ : IsSubDPIdeal hI J) [∀ x, Decidable (x ∈ J)] :
     DividedPowers J where
   dpow n x        := if x ∈ J then hI.dpow n x else 0
   dpow_null hx    := by simp only [if_neg hx]
   dpow_zero hx    := by simp only [if_pos hx, hI.dpow_zero (hJ.isSubideal hx)]
   dpow_one hx     := by simp only [if_pos hx, hI.dpow_one (hJ.isSubideal hx)]
-  dpow_mem hn hx  := by simp only [if_pos hx, hJ.dpow_mem _ hn hx]
+  dpow_mem hn hx  := by simp only [if_pos hx, hJ.dpow_mem hn hx]
   dpow_add hx hy  := by simp_rw [if_pos hx, if_pos hy, if_pos (Ideal.add_mem J hx hy),
     hI.dpow_add (hJ.isSubideal hx) (hJ.isSubideal hy)]
   dpow_smul hx    := by
     simp only [if_pos hx, if_pos (mul_mem_left J _ hx), hI.dpow_smul (hJ.isSubideal hx)]
   dpow_mul hx     := by simp only [if_pos hx, hI.dpow_mul (hJ.isSubideal hx)]
   dpow_comp hn hx := by
-    simp only [if_pos hx, if_pos (hJ.dpow_mem _ hn hx), hI.dpow_comp hn (hJ.isSubideal hx)]
+    simp only [if_pos hx, if_pos (hJ.dpow_mem hn hx), hI.dpow_comp hn (hJ.isSubideal hx)]
 
 variable {J : Ideal A} (hJ : IsSubDPIdeal hI J) [∀ x, Decidable (x ∈ J)]
 
@@ -110,7 +110,7 @@ end IsSubDPIdeal
 
 open Finset Ideal
 
-/-- The ideal `J ⊓ I` is a sub-dp-ideal of `I` if and only if (on `I`) the divided powers have
+/-- The ideal `J ⊓ I` is a sub-dp-ideal of `I` if and only if (on `I`) the divided powers have
   some compatiblity mod `J`. (The necessity was proved as a sanity check.) -/
 theorem IsSubDPIdeal_inf_iff {A : Type*} [CommRing A] {I : Ideal A} (hI : DividedPowers I)
   {J : Ideal A} : IsSubDPIdeal hI (J ⊓ I) ↔
@@ -120,7 +120,7 @@ theorem IsSubDPIdeal_inf_iff {A : Type*} [CommRing A] {I : Ideal A} (hI : Divide
     rw [← add_sub_cancel b a, hI.dpow_add' hb hab', range_succ, sum_insert not_mem_range_self,
       tsub_self, hI.dpow_zero hab', mul_one,add_sub_cancel_left]
     exact J.sum_mem (fun i hi ↦  SemilatticeInf.inf_le_left J I ((J ⊓ I).smul_mem _
-      (hIJ.dpow_mem _ (ne_of_gt (Nat.sub_pos_of_lt (mem_range.mp hi))) ⟨hab, hab'⟩)))
+      (hIJ.dpow_mem (ne_of_gt (Nat.sub_pos_of_lt (mem_range.mp hi))) ⟨hab, hab'⟩)))
   · refine ⟨SemilatticeInf.inf_le_right J I, fun {n} hn {a} ha ↦ ⟨?_, hI.dpow_mem hn ha.right⟩⟩
     rw [← sub_zero (hI.dpow n a), ← hI.dpow_eval_zero hn]
     exact hIJ n a 0 ha.right I.zero_mem (J.sub_mem ha.left J.zero_mem)
@@ -130,32 +130,35 @@ variable {A B : Type*} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {J
 
 /-- Lemma 3.6 of [BO] (Antoine) -/
 theorem span_IsSubDPIdeal_iff (S : Set A) (hS : S ⊆ I) :
-    IsSubDPIdeal hI (span S) ↔ ∀ (n : ℕ) (_ : n ≠ 0), ∀ s ∈ S, hI.dpow n s ∈ span S := by
-  refine ⟨fun hhI n hn s hs ↦ hhI.dpow_mem _ hn (subset_span hs), ?_⟩
+    IsSubDPIdeal hI (span S) ↔ ∀ {n : ℕ} (_ : n ≠ 0), ∀ s ∈ S, hI.dpow n s ∈ span S := by
+  refine ⟨fun hhI n hn s hs ↦ hhI.dpow_mem hn (subset_span hs), ?_⟩
   · -- interesting direction,
     intro hhI
     have hSI := span_le.mpr hS
     apply IsSubDPIdeal.mk hSI
-    intro n hn z hz; revert n
-    refine Submodule.span_induction' ?_ ?_ ?_ ?_ hz
-    ·-- case of elements of S
-      exact fun s hs n hn ↦ hhI n hn s hs
-    ·-- case of 0
-      intro _ hn
-      rw [hI.dpow_eval_zero hn]
-      exact (span S).zero_mem
-    · -- case of sum
-      intro x hxI y hyI hx hy n hn
-      rw [hI.dpow_add' (hSI hxI) (hSI hyI)]
-      apply Submodule.sum_mem (span S)
-      intro m _
-      by_cases hm0 : m = 0
-      · exact hm0 ▸ mul_mem_left (span S) _ (hy _ hn)
-      · exact mul_mem_right _ (span S) (hx _ hm0)
-    · -- case : product,
-      intro a x hxI hx n hn
-      rw [Algebra.id.smul_eq_mul, hI.dpow_smul (hSI hxI)]
-      exact mul_mem_left (span S) (a ^ n) (hx n hn)
+    intro m hm z hz
+    -- This solution is a bit hacky, but it works...
+    have haux : ∀ (n : ℕ), n ≠ 0 → hI.dpow n z ∈ span S := by
+      refine Submodule.span_induction' ?_ ?_ ?_ ?_ hz
+      ·-- case of elements of S
+        exact fun s hs n hn ↦ hhI hn s hs
+      ·-- case of 0
+        intro _ hn
+        rw [hI.dpow_eval_zero hn]
+        exact (span S).zero_mem
+      · -- case of sum
+        intro x hxI y hyI hx hy n hn
+        rw [hI.dpow_add' (hSI hxI) (hSI hyI)]
+        apply Submodule.sum_mem (span S)
+        intro m _
+        by_cases hm0 : m = 0
+        · exact hm0 ▸ mul_mem_left (span S)  _ (hy _ hn)
+        · exact mul_mem_right _ (span S) (hx _ hm0)
+      · -- case : product,
+        intro a x hxI hx n hn
+        rw [Algebra.id.smul_eq_mul, hI.dpow_smul (hSI hxI)]
+        exact mul_mem_left (span S) (a ^ n) (hx n hn)
+    exact @haux m hm
 
 theorem generated_dpow_isSubideal {S : Set A} (hS : S ⊆ I) :
     span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x} ≤ I := by
@@ -169,21 +172,21 @@ theorem IsSubDPIdeal_sup {J K : Ideal A} (hJ : IsSubDPIdeal hI J) (hK : IsSubDPI
     span_IsSubDPIdeal_iff _ _ (Set.union_subset_iff.mpr ⟨hJ.1, hK.1⟩)]
   · intro n hn a ha
     rcases ha with ha | ha
-    . exact span_mono Set.subset_union_left (subset_span (hJ.2 n hn ha))
-    . exact span_mono Set.subset_union_right (subset_span (hK.2 n hn ha))
+    . exact span_mono Set.subset_union_left (subset_span (hJ.2 hn ha))
+    . exact span_mono Set.subset_union_right (subset_span (hK.2 hn ha))
 
 theorem IsSubDPIdeal_iSup {ι : Type*} {J : ι → Ideal A} (hJ : ∀ i, IsSubDPIdeal hI (J i)) :
     IsSubDPIdeal hI (iSup J) := by
   rw [iSup_eq_span, span_IsSubDPIdeal_iff _ _ (Set.iUnion_subset_iff.mpr <| fun i ↦ (hJ i).1)]
   simp_rw [Set.mem_iUnion]
   rintro n hn a ⟨i, ha⟩
-  exact span_mono (Set.subset_iUnion _ i) (subset_span ((hJ i).2 n hn ha))
+  exact span_mono (Set.subset_iUnion _ i) (subset_span ((hJ i).2 hn ha))
 
 theorem IsSubDPIdeal_map_of_IsSubDPIdeal {f : A →+* B} (hf : IsDPMorphism hI hJ f) {K : Ideal A}
     (hK : IsSubDPIdeal hI K) : IsSubDPIdeal hJ (map f K) := by
   rw [Ideal.map, span_IsSubDPIdeal_iff]
   · rintro n hn y ⟨x, hx, rfl⟩
-    exact hf.2 x (hK.1 hx) ▸ mem_map_of_mem _ (hK.2 n hn hx)
+    exact hf.2 x (hK.1 hx) ▸ mem_map_of_mem _ (hK.2 hn hx)
   · rintro y ⟨x, hx, rfl⟩
     exact hf.1 (mem_map_of_mem f (hK.1 hx))
 
@@ -199,7 +202,7 @@ end IsSubDPIdeal
 structure SubDPIdeal {A : Type*} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I) where
   carrier : Ideal A
   isSubideal : carrier ≤ I
-  dpow_mem : ∀ (n : ℕ) (_ : n ≠ 0), ∀ j ∈ carrier, hI.dpow n j ∈ carrier
+  dpow_mem : ∀ {n : ℕ} (_ : n ≠ 0), ∀ j ∈ carrier, hI.dpow n j ∈ carrier
 
 namespace SubDPIdeal
 
@@ -246,21 +249,22 @@ lemma SubDPIdeal_of_IsSubDPIdeal {J  : Ideal A} (hJ : IsSubDPIdeal hI J) :
 def prod (J : Ideal A) : SubDPIdeal hI where
   carrier := I • J
   isSubideal := mul_le_right
-  dpow_mem n hn x hx := by
-    revert n
-    apply @Submodule.smul_induction_on' A A _ _ _ I J _ hx
-    · -- mul
-      intro a ha b hb n hn
-      rw [Algebra.id.smul_eq_mul, smul_eq_mul, mul_comm a b, hI.dpow_smul ha, mul_comm]
-      exact Submodule.mul_mem_mul (J.pow_mem_of_mem hb n (zero_lt_iff.mpr hn)) (hI.dpow_mem hn ha)
-    · -- add
-      intro x hx y hy hx' hy' n hn
-      rw [hI.dpow_add' (mul_le_right hx) (mul_le_right hy)]
-      apply Submodule.sum_mem (I • J)
-      intro k _
-      by_cases hk0 : k = 0
-      · exact hk0 ▸ mul_mem_left (I • J) _ (hy' _ hn)
-      · exact mul_mem_right _ (I • J) (hx' k hk0)
+  dpow_mem hm x hx := by
+    have haux : ∀ (n : ℕ) (_ : n ≠ 0), hI.dpow n x ∈ I • J := by
+      apply @Submodule.smul_induction_on' A A _ _ _ I J _ hx
+      · -- mul
+        intro a ha b hb n hn
+        rw [Algebra.id.smul_eq_mul, smul_eq_mul, mul_comm a b, hI.dpow_smul ha, mul_comm]
+        exact Submodule.mul_mem_mul (J.pow_mem_of_mem hb n (zero_lt_iff.mpr hn)) (hI.dpow_mem hn ha)
+      · -- add
+        intro x hx y hy hx' hy' n hn
+        rw [hI.dpow_add' (mul_le_right hx) (mul_le_right hy)]
+        apply Submodule.sum_mem (I • J)
+        intro k _
+        by_cases hk0 : k = 0
+        · exact hk0 ▸ mul_mem_left (I • J) _ (hy' _ hn)
+        · exact mul_mem_right _ (I • J) (hx' k hk0)
+    exact @haux _ hm
 
 section CompleteLattice
 
@@ -278,23 +282,23 @@ theorem lt_iff {J J' : SubDPIdeal hI} : J < J' ↔ J.carrier < J'.carrier := Iff
 instance : Top (SubDPIdeal hI) :=
   ⟨{carrier    := I
     isSubideal := le_refl _
-    dpow_mem   := fun _ hn _ hx ↦ hI.dpow_mem hn hx }⟩
+    dpow_mem   := fun hn _ hx ↦ hI.dpow_mem hn hx }⟩
 
 instance inhabited : Inhabited hI.SubDPIdeal := ⟨⊤⟩
 
 /-- `(0)` is a sub-dp-ideal ot the dp-ideal `I`. -/
 instance : Bot (SubDPIdeal hI) :=
   ⟨{carrier    := ⊥
     isSubideal := bot_le
-    dpow_mem   := fun n hn x hx ↦ by rw [mem_bot.mp hx, hI.dpow_eval_zero hn, mem_bot]}⟩
+    dpow_mem   := fun hn x hx ↦ by rw [mem_bot.mp hx, hI.dpow_eval_zero hn, mem_bot]}⟩
 
 --Section 1.8 of [B]
 -- The intersection of two sub-dp-ideals is a sub-dp-ideal.
 instance : Inf (SubDPIdeal hI) :=
   ⟨fun J J' ↦
     { carrier    := J.carrier ⊓ J'.carrier
       isSubideal := fun _ hx ↦ J.isSubideal hx.1
-      dpow_mem   := fun n hn x hx ↦ ⟨J.dpow_mem n hn x hx.1, J'.dpow_mem n hn x hx.2⟩ }⟩
+      dpow_mem   := fun hn x hx ↦ ⟨J.dpow_mem hn x hx.1, J'.dpow_mem hn x hx.2⟩ }⟩
 
 theorem inf_carrier_def (J J' : SubDPIdeal hI) : (J ⊓ J').carrier = J.carrier ⊓ J'.carrier := rfl
 
@@ -304,9 +308,9 @@ instance : InfSet (SubDPIdeal hI) :=
       isSubideal := fun x hx ↦ by
         simp only [mem_iInf] at hx
         exact hx ⊤ (Set.mem_insert ⊤ S)
-      dpow_mem   := fun n hn x hx ↦ by
+      dpow_mem   := fun hn x hx ↦ by
         simp only [mem_iInf] at hx ⊢
-        exact fun s hs ↦ s.dpow_mem n hn x (hx s hs) }⟩
+        exact fun s hs ↦ s.dpow_mem hn x (hx s hs) }⟩
 
 theorem sInf_carrier_def (S : Set (SubDPIdeal hI)) :
     (sInf S).carrier = ⨅ s ∈ Insert.insert ⊤ S, (s : hI.SubDPIdeal).carrier := rfl
@@ -329,7 +333,7 @@ instance : SupSet (SubDPIdeal hI) :=
       apply subset_span
       apply Set.mem_biUnion hJ'
       obtain ⟨K, hKS, rfl⟩ := hJ'
-      exact K.dpow_mem n hn x h'⟩
+      exact K.dpow_mem hn x h'⟩
 
 theorem sSup_carrier_def (S : Set (SubDPIdeal hI)) :
     (sSup S).carrier = sSup ((toIdeal hI) '' S) := rfl
@@ -383,26 +387,28 @@ def generated (S : Set A) : SubDPIdeal hI := sInf {J : SubDPIdeal hI | S ⊆ J.c
 def generatedDpow {S : Set A} (hS : S ⊆ I) : SubDPIdeal hI where
   carrier := span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x}
   isSubideal := hI.generated_dpow_isSubideal hS
-  dpow_mem n hn z hz := by
+  dpow_mem hk z hz := by
     have hSI := hI.generated_dpow_isSubideal hS
-    revert n
-    refine Submodule.span_induction' ?_ ?_ ?_ ?_ hz
-    · -- Elements of S
-      rintro y ⟨m, hm, x, hxS, hxy⟩ n hn
-      rw [hxy, hI.dpow_comp hm (hS hxS)]
-      exact mul_mem_left _ _ (subset_span ⟨n * m, mul_ne_zero hn hm, x, hxS, rfl⟩)
-    · -- Zero
-      exact fun _ hn ↦ by simp only [hI.dpow_eval_zero hn, zero_mem]
-    · intro x hx y hy hx_pow hy_pow n hn
-      rw [hI.dpow_add' (hSI hx) (hSI hy)]
-      apply Submodule.sum_mem (span _)
-      intro m _
-      by_cases hm0 : m = 0
-      · rw [hm0]; exact (span _).mul_mem_left _ (hy_pow n hn)
-      · exact (span _).mul_mem_right _ (hx_pow m hm0)
-    · intro a x hx hx_pow n hn
-      rw [smul_eq_mul, hI.dpow_smul (hSI hx)]
-      exact mul_mem_left (span _) (a ^ n) (hx_pow n hn)
+    have haux : ∀ (n : ℕ) (_ : n ≠ 0),
+        hI.dpow n z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} := by
+      refine Submodule.span_induction' ?_ ?_ ?_ ?_ hz
+      · -- Elements of S
+        rintro y ⟨m, hm, x, hxS, hxy⟩ n hn
+        rw [hxy, hI.dpow_comp hm (hS hxS)]
+        exact mul_mem_left _ _ (subset_span ⟨n * m, mul_ne_zero hn hm, x, hxS, rfl⟩)
+      · -- Zero
+        exact fun _ hn ↦ by simp only [hI.dpow_eval_zero hn, zero_mem]
+      · intro x hx y hy hx_pow hy_pow n hn
+        rw [hI.dpow_add' (hSI hx) (hSI hy)]
+        apply Submodule.sum_mem (span _)
+        intro m _
+        by_cases hm0 : m = 0
+        · rw [hm0]; exact (span _).mul_mem_left _ (hy_pow n hn)
+        · exact (span _).mul_mem_right _ (hx_pow m hm0)
+      · intro a x hx hx_pow n hn
+        rw [smul_eq_mul, hI.dpow_smul (hSI hx)]
+        exact mul_mem_left (span _) (a ^ n) (hx_pow n hn)
+    exact haux _ hk
 
 theorem generatedDpow_carrier {S : Set A} (hS : S ⊆ I) :
     (generatedDpow hI hS).carrier =
@@ -415,7 +421,7 @@ theorem generated_dpow_le (S : Set A) (J : SubDPIdeal hI) (hSJ : S ⊆ J.carrier
     span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x} ≤ J.carrier := by
   rw [span_le]
   rintro y ⟨n, hn, x, hx, hxy⟩
-  exact hxy ▸ J.dpow_mem n hn x (hSJ hx)
+  exact hxy ▸ J.dpow_mem hn x (hSJ hx)
 
 theorem generated_carrier_eq {S : Set A} (hS : S ⊆ I) :
     (generated hI S).carrier =
@@ -457,7 +463,7 @@ open Ideal
 def DPMorphism.ker (f : DPMorphism hI hJ) : SubDPIdeal hI where
   carrier := RingHom.ker f.toRingHom ⊓ I
   isSubideal := inf_le_right
-  dpow_mem n hn a := by
+  dpow_mem hn a := by
     simp only [mem_inf, and_imp, RingHom.mem_ker]
     intro ha ha'
     rw [← f.isDPMorphism.2 a ha', ha]
@@ -496,12 +502,12 @@ theorem mem_dpEqualizer_iff {A : Type*} [CommSemiring A] {I : Ideal A} (hI hI' :
 
 theorem dpEqualizer_is_dp_ideal_left {A : Type*} [CommSemiring A] {I : Ideal A}
     (hI hI' : DividedPowers I) : DividedPowers.IsSubDPIdeal hI (dpEqualizer hI hI') :=
-  IsSubDPIdeal.mk (fun _ hx ↦ hx.1) (fun n hn x hx ↦ ⟨hI.dpow_mem hn hx.1,
+  IsSubDPIdeal.mk (fun _ hx ↦ hx.1) (fun hn x hx ↦ ⟨hI.dpow_mem hn hx.1,
     fun m ↦ by rw [hI.dpow_comp hn hx.1, hx.2, hx.2, hI'.dpow_comp hn hx.1]⟩)
 
 theorem dpEqualizer_is_dp_ideal_right {A : Type*} [CommSemiring A] {I : Ideal A}
     (hI hI' : DividedPowers I) : DividedPowers.IsSubDPIdeal hI' (dpEqualizer hI hI') :=
-  IsSubDPIdeal.mk (fun _ hx ↦ hx.1) (fun n hn x hx ↦ ⟨hI'.dpow_mem hn hx.1, fun m ↦ by
+  IsSubDPIdeal.mk (fun _ hx ↦ hx.1) (fun hn x hx ↦ ⟨hI'.dpow_mem hn hx.1, fun m ↦ by
     rw [← hx.2, hI.dpow_comp hn hx.1, hx.2, hx.2, hI'.dpow_comp hn hx.1]⟩)
 
 open Ideal
@@ -520,9 +526,9 @@ def interQuot {A : Type*} [CommRing A] {I : Ideal A} (hI : DividedPowers I)
     (J : Ideal A) (hJ : DividedPowers (I.map (Ideal.Quotient.mk J)))
     (φ : DPMorphism hI hJ) (hφ : φ.toRingHom = Ideal.Quotient.mk J) :
   SubDPIdeal hI where
-  carrier := J ⊓ I
+  carrier    := J ⊓ I
   isSubideal := by simp only [ge_iff_le, inf_le_right]
-  dpow_mem := fun n hn a ⟨haJ, haI⟩ ↦ by
+  dpow_mem   := fun hn a ⟨haJ, haI⟩ ↦ by
     refine ⟨?_, hI.dpow_mem hn haI⟩
     rw [SetLike.mem_coe, ← Quotient.eq_zero_iff_mem, ← hφ, ← φ.dpow_comp a haI]
     suffices ha0 : φ.toRingHom a = 0 by