diff --git a/RamificationGroup/DecompositionGroup.lean b/RamificationGroup/DecompositionGroup.lean
index 00eb767..25a0281 100644
--- a/RamificationGroup/DecompositionGroup.lean
+++ b/RamificationGroup/DecompositionGroup.lean
@@ -27,9 +27,15 @@ def decompositionGroup : Subgroup (S ≃ₐ[R] S) where
     apply Valuation.IsEquiv_comap_symm
     exact h
 
+/-- This stupid theorem should be parametrized over `Subgroup (S ≃ₐ[R] S)`. -/
 theorem decompositionGroup_one : (1 : decompositionGroup R S).1 = .refl := by
   simp only [OneMemClass.coe_one, AlgEquiv.aut_one]
 
+/-- This stupid theorem should be parametrized over `Subgroup (S ≃ₐ[R] S)`. -/
+theorem refl_mem_decompositionGroup : .refl ∈ decompositionGroup R S := by
+  rw [← decompositionGroup_one R S]
+  exact (1 : decompositionGroup R S).2
+
 section eq_top
 
 variable {K L : Type*} [Field K] [Field L] [vK : Valued K ℤₘ₀] [IsDiscrete vK.v] [vL : Valued L ℤₘ₀] [Algebra K L] [FiniteDimensional K L]
diff --git a/RamificationGroup/ForMathlib/Algebra/Algebra/PowerBasis.lean b/RamificationGroup/ForMathlib/Algebra/Algebra/PowerBasis.lean
index d48e0db..10b8140 100644
--- a/RamificationGroup/ForMathlib/Algebra/Algebra/PowerBasis.lean
+++ b/RamificationGroup/ForMathlib/Algebra/Algebra/PowerBasis.lean
@@ -1,14 +1,28 @@
 import Mathlib.RingTheory.PowerBasis
 
-namespace PowerBasis
-
-variable {R S : Type*} [CommRing R] [Ring S] [Algebra R S]
-{S' : Type*} [Semiring S'] [Algebra R S']
-
-theorem algEquiv_ext (pb : PowerBasis R S) {f g : S ≃ₐ[R] S'} (h : f pb.gen = g pb.gen) :
-  f = g := by
-  ext x
-  rw [show f x = g x ↔ f.toAlgHom x = g.toAlgHom x by rfl]
-  revert x
-  rw [← AlgHom.ext_iff]
-  apply algHom_ext _ h
+open Algebra PowerBasis Polynomial
+
+variable {R A : Type*} [CommRing R] [Ring A] [Algebra R A]
+{B : Type*} [Semiring B] [Algebra R B]
+{F : Type*} [FunLike F A B] [AlgHomClass F R A B]
+
+theorem Algebra.exists_eq_aeval_generator {s : A} (hgen : adjoin R {s} = ⊤) (x : A) :
+  ∃ f : R[X], x = aeval s f := by
+  have hx : x ∈ (⊤ : Subalgebra R A) := trivial
+  rw [← hgen, adjoin_singleton_eq_range_aeval] at hx
+  rcases hx with ⟨p, hp⟩
+  exact ⟨p, hp.symm⟩
+
+theorem Algebra.algHomClass_ext_generator {s : A} (hgen : adjoin R {s} = ⊤)
+  {f g : F} (h : f s = g s) :
+    f = g := by
+  apply DFunLike.ext
+  intro x
+  have hx : x ∈ (⊤ : Subalgebra R A) := trivial
+  rw [← hgen, adjoin_singleton_eq_range_aeval] at hx
+  rcases hx with ⟨p, hp⟩
+  simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe] at hp
+  rw [← hp, ← Polynomial.aeval_algHom_apply, ← Polynomial.aeval_algHom_apply, h]
+
+theorem PowerBasis.algHom_ext' (pb : PowerBasis R A) {f g : F} (h : f pb.gen = g pb.gen) :
+  f = g := Algebra.algHomClass_ext_generator (adjoin_gen_eq_top pb) h
diff --git a/RamificationGroup/ForMathlib/DiscreteValuationRing/Basic.lean b/RamificationGroup/ForMathlib/DiscreteValuationRing/Basic.lean
index 820d30a..3a9cdb1 100644
--- a/RamificationGroup/ForMathlib/DiscreteValuationRing/Basic.lean
+++ b/RamificationGroup/ForMathlib/DiscreteValuationRing/Basic.lean
@@ -13,8 +13,7 @@ variable {ϖ x : A} (hϖ : Irreducible ϖ)
 
 theorem unit_mul_irreducible_of_irreducible (hx : Irreducible x) : ∃u : A, IsUnit u ∧ x = u * ϖ := by
   obtain ⟨u, hu⟩ : ∃u : A, x = u * ϖ := by
-    refine exists_eq_mul_left_of_dvd (addVal_le_iff_dvd.mp ?_)
-    apply le_of_eq
+    refine exists_eq_mul_left_of_dvd <| addVal_le_iff_dvd.mp <| le_of_eq ?_
     rw [addVal_uniformizer hx, addVal_uniformizer hϖ]
   have : IsUnit u := Or.resolve_right (Irreducible.isUnit_or_isUnit hx hu) hϖ.not_unit
   use u
@@ -39,8 +38,7 @@ theorem mul_irreducible_square_of_not_unit_of_not_irreducible (h1 : ¬Irreducibl
 theorem irreducible_of_irreducible_add_addVal_ge_two (hx : Irreducible x) {y : A} : Irreducible (x + y * ϖ ^ 2) := by
   rcases unit_mul_irreducible_of_irreducible hϖ hx with ⟨u, hu, hxu⟩
   rw [hxu, pow_two, ← mul_assoc, ← add_mul]
-  apply (irreducible_isUnit_mul _).mpr hϖ
-  apply LocalRing.is_unit_of_unit_add_nonunit hu
+  apply (irreducible_isUnit_mul (LocalRing.is_unit_of_unit_add_nonunit hu _)).mpr hϖ
   simp only [mem_nonunits_iff, IsUnit.mul_iff, not_and]
   exact fun _ ↦ Irreducible.not_unit hϖ
 
@@ -48,3 +46,9 @@ theorem maximalIdeal_pow_eq_span_irreducible_pow (n : ℕ) : maximalIdeal A ^ n
   rw [Irreducible.maximalIdeal_eq hϖ, Ideal.span_singleton_pow]
 
 end uniformiser
+
+section ramiIdx
+
+/- Show `p = P^e` under suitable conditions. -/
+
+end ramiIdx
diff --git a/RamificationGroup/ForMathlib/LocalRing/Basic.lean b/RamificationGroup/ForMathlib/LocalRing/Basic.lean
index ac098a9..761241b 100644
--- a/RamificationGroup/ForMathlib/LocalRing/Basic.lean
+++ b/RamificationGroup/ForMathlib/LocalRing/Basic.lean
@@ -9,7 +9,7 @@ noncomputable def ramificationIdx : ℕ := Ideal.ramificationIdx (algebraMap A B
 
 noncomputable def inertiaDeg : ℕ := Ideal.inertiaDeg (algebraMap A B) (maximalIdeal A) (maximalIdeal B)
 
-instance instAlgebraResidue : Algebra (ResidueField A) (ResidueField B) :=
+instance : Algebra (ResidueField A) (ResidueField B) :=
   Ideal.Quotient.algebraQuotientOfLEComap <| le_of_eq (((local_hom_TFAE <| algebraMap A B).out 0 4 rfl rfl).mp is_local).symm
 
 variable {A B}
diff --git a/RamificationGroup/LowerNumbering.lean b/RamificationGroup/LowerNumbering.lean
index c3beea1..b978db1 100644
--- a/RamificationGroup/LowerNumbering.lean
+++ b/RamificationGroup/LowerNumbering.lean
@@ -23,14 +23,24 @@ rename theorems, many theorem should be named as LowerRamificationGroup.xxx, not
 
 open DiscreteValuation Valued Valuation
 
+section general_algebra
+
+instance instAlgebraFiniteTypeToIsNoetherian (R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A] [IsNoetherian R A] :
+  Algebra.FiniteType R A where
+    out := by
+      apply Subalgebra.fg_of_fg_toSubmodule
+      rw [Algebra.top_toSubmodule]
+      apply isNoetherian_def.mp
+      assumption
+
+end general_algebra
+
 -- <-1 decomposition group
 -- >= -1 decompositiongroup and v (s x - x) ≤ 1
 section def_lower_rami_grp
 
 variable (R S : Type*) {ΓR : outParam Type*} [CommRing R] [Ring S] [vS : Valued S ℤₘ₀] [Algebra R S]
 
--- variable (K L : Type*) {ΓL : outParam Type*} [Field K] [Field L] [LinearOrderedCommGroupWithZero ΓL] [vL : Valued L ℤₘ₀] [Algebra K L]
-
 def lowerRamificationGroup (u : ℤ) : Subgroup (S ≃ₐ[R] S) where
     carrier := {s | s ∈ decompositionGroup R S ∧ ∀ x : vS.v.integer, Valued.v (s x - x) ≤ .coe (.ofAdd (- u - 1))}
     mul_mem' {a} {b} ha hb := by
@@ -64,28 +74,29 @@ def lowerRamificationGroup (u : ℤ) : Subgroup (S ≃ₐ[R] S) where
       _ = v ( s (s⁻¹ a) - s ⁻¹ a) := by
         rw [← Valuation.map_neg]
         congr
-        simp
+        simp only [neg_sub]
       _ ≤ _ := hs.2 ⟨s⁻¹ a, (val_map_le_one_iff (f := (s.symm : S →+* S))
         (Valuation.IsEquiv_comap_symm hs.1) a.1).mpr a.2⟩
 
 scoped [Valued] notation:max " G(" S:max "/" R:max ")_[" u:max "] " => lowerRamificationGroup R S u
 
 theorem lowerRamificationGroup.antitone : Antitone (lowerRamificationGroup R S) := by
-  rintro a b hab
+  intro a b hab
   simp only [lowerRamificationGroup, ofAdd_sub, ofAdd_neg, Subtype.forall, Subgroup.mk_le_mk,
     Set.setOf_subset_setOf, and_imp]
   rintro s hs1 hs2
   constructor
   · exact hs1
   · intro y hy
-    apply le_trans
-    apply hs2 y hy
+    apply le_trans (hs2 y hy)
     simp only [WithZero.coe_le_coe, div_le_iff_le_mul, div_mul_cancel, inv_le_inv_iff,
       Multiplicative.ofAdd_le]
     exact hab
 
 end def_lower_rami_grp
 
+instance Valuation.instNonemptyToValuation {R Γ₀: Type*} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀): Nonempty v.integer := Zero.instNonempty
+
 section autCongr
 
 variable {R S S': Type*} {ΓR : outParam Type*} [CommRing R] [Ring S] [Ring S'] [vS : Valued S ℤₘ₀] [vS : Valued S' ℤₘ₀] [Algebra R S] [Algebra R S']
@@ -105,10 +116,12 @@ theorem autCongr_mem_lowerRamificationGroup_iff {f : S ≃ₐ[R] S'} (hf : ∀ a
 end autCongr
 
 section WithBot
--- this should be put into a suitable place, Also add `WithOne`? `WithTop`, `WithBot`, `WithOne`, `Muliplicative`, `Additive`
+-- this should be put into a suitable place, Also add `WithOne`? `WithTop`, `WithBot`, `WithOne`, `Multiplicative`, `Additive`
 open Classical
-
+#check WithBot.instSupSet
+#check WithTop.conditionallyCompleteLattice
 -- there is no `ConditionallyCompleteLinearOrderTop` in mathlib ...
+-- # The definition of `WithTop.instInfSet` have to be changed
 #check WithBot.linearOrder
 noncomputable instance {α} [ConditionallyCompleteLinearOrder α] : ConditionallyCompleteLinearOrderBot (WithBot α) where
   toConditionallyCompleteLattice := WithBot.conditionallyCompleteLattice
@@ -117,11 +130,11 @@ noncomputable instance {α} [ConditionallyCompleteLinearOrder α] : Conditionall
   decidableEq := WithBot.decidableEq
   decidableLT := WithBot.decidableLT
   csSup_of_not_bddAbove s h := by
-    by_cases hbot : s ⊆ {⊥}
-    · simp [sSup, sInf]
-      sorry
-    · simp [sSup, sInf]
-      intro x hxs hx
+    rw [WithBot.csSup_empty]
+    simp only [sSup, sInf, Set.subset_singleton_iff]
+    by_cases hs : ∀ y ∈ s, y = (⊤ : WithTop αᵒᵈ)
+    · rw [if_pos hs]; rfl
+    · rw [if_neg hs]
       sorry
   csInf_of_not_bddBelow := sorry
   bot_le := WithBot.orderBot.bot_le
@@ -142,7 +155,7 @@ variable (R S : Type*) [CommRing R] [Ring S] [vS : Valued S ℤₘ₀] [Algebra
 open Classical
 -- 0 if lower than 0
 noncomputable def AlgEquiv.lowerIndex (s : S ≃ₐ[R] S) : ℕ∞ :=
-  if h : iSup (fun x : vS.v.integer => (Valued.v (s x - x))) = 0 then ⊤
+  if h : ⨆ x : vS.v.integer, vS.v (s x - x) = 0 then ⊤
   else (- Multiplicative.toAdd (WithZero.unzero h)).toNat
 
 scoped [Valued] notation:max " i_[" S:max "/" R:max "]" => AlgEquiv.lowerIndex R S
@@ -153,6 +166,85 @@ noncomputable def AlgEquiv.truncatedLowerIndex (u : ℚ) (s : (S ≃ₐ[R] S)) :
 
 scoped [Valued] notation:max " i_[" L:max "/" K:max "]ₜ" => AlgEquiv.truncatedLowerIndex K L
 
+section lowerIndex_inequality
+
+variable {R S}
+
+/-- One of `val_map_sub_le_one` and `sub_self_mem_integer` should be thrown away.-/
+theorem sub_self_mem_integer {s : S ≃ₐ[R] S} (hs' : s ∈ decompositionGroup R S)
+  (x : vS.v.integer) :
+    s x - x ∈ vS.v.integer := by
+  apply Subring.sub_mem
+  · rw [mem_integer_iff, val_map_le_one_iff hs']; exact x.2
+  · exact x.2
+
+/-- One of `val_map_sub_le_one` and `sub_self_mem_integer` should be thrown away.-/
+theorem val_map_sub_le_one {s : S ≃ₐ[R] S} (hs' : s ∈ decompositionGroup R S)
+  (x : vS.v.integer) :
+    v (s x - x) ≤ 1 := sub_self_mem_integer hs' x
+
+theorem toAdd_iSup_val_map_sub_le_zero_of_ne_zero {s : S ≃ₐ[R] S} (hs' : s ∈ decompositionGroup R S)
+  (h : ⨆ x : vS.v.integer, vS.v (s x - x) ≠ 0) :
+    Multiplicative.toAdd (WithZero.unzero h) ≤ 0 := by
+  change (WithZero.unzero h) ≤ 1
+  suffices ⨆ x : vS.v.integer, vS.v (s x - x) ≤ 1 from by
+    rw [← WithZero.coe_le_coe, WithZero.coe_unzero h]
+    exact this
+  apply ciSup_le <| val_map_sub_le_one hs'
+
+section adjoin_singleton
+
+variable {K L : Type*} [Field K] [Field L]
+[vK : Valued K ℤₘ₀] [vL : Valued L ℤₘ₀] [Algebra K L] [IsValExtension K L]
+
+/-- Should be strenthened to ` > 0`-/
+theorem decomp_val_map_generator_sub_ne_zero {gen : 𝒪[L]} (hgen : Algebra.adjoin 𝒪[K] {gen} = ⊤)
+  {s : L ≃ₐ[K] L} (hs' : s ∈ decompositionGroup K L) (hs : s ≠ .refl) :
+    vL.v (s gen - gen) ≠ 0 := by
+  by_contra h
+  rw [zero_iff, sub_eq_zero] at h
+  apply hs
+  rw [elem_decompositionGroup_eq_iff_ValuationSubring' hs' (refl_mem_decompositionGroup K L)]
+  apply Algebra.algHomClass_ext_generator hgen
+  ext
+  rw [DecompositionGroup.restrictValuationSubring_apply' hs',
+    DecompositionGroup.restrictValuationSubring_apply' (refl_mem_decompositionGroup K L),
+    h, AlgEquiv.coe_refl, id_eq]
+
+open Polynomial in
+theorem decomp_val_map_sub_le_generator {gen : 𝒪[L]} (hgen : Algebra.adjoin 𝒪[K] {gen} = ⊤) {s : L ≃ₐ[K] L} (hs' : s ∈ decompositionGroup K L) (x : 𝒪[L]) : v (s x - x) ≤ v (s gen - gen) := by
+  by_cases hs : s = .refl
+  · subst hs
+    simp only [AlgEquiv.coe_refl, id_eq, sub_self, _root_.map_zero, le_refl]
+  rcases Algebra.exists_eq_aeval_generator hgen x with ⟨f, hf⟩
+  subst hf
+  rcases taylor_order_zero_apply_aeval f gen ((DecompositionGroup.restrictValuationSubring' hs') gen - gen) with ⟨b, hb⟩
+  rw [add_sub_cancel, add_comm, ← sub_eq_iff_eq_add, aeval_algHom_apply, Subtype.ext_iff] at hb
+  simp only [AddSubgroupClass.coe_sub, DecompositionGroup.restrictValuationSubring_apply' hs', Submonoid.coe_mul, Subsemiring.coe_toSubmonoid, Subring.coe_toSubsemiring] at hb
+  rw [hb, Valuation.map_mul]
+  nth_rw 2 [← mul_one (v (s gen - gen))]
+  rw [mul_le_mul_left₀]
+  · exact b.2
+  · apply decomp_val_map_generator_sub_ne_zero hgen hs' hs
+
+theorem decomp_iSup_val_map_sub_eq_generator {gen : 𝒪[L]} (hgen : Algebra.adjoin 𝒪[K] {gen} = ⊤) {s : L ≃ₐ[K] L} (hs' : s ∈ decompositionGroup K L) :
+  ⨆ x : vL.v.integer, v (s x - x) = v (s gen - gen) := by
+  apply le_antisymm
+  · letI : Nonempty 𝒪[L] := inferInstanceAs (Nonempty vL.v.integer)
+    apply ciSup_le <| decomp_val_map_sub_le_generator hgen hs'
+  · apply le_ciSup (f := fun (x : 𝒪[L]) ↦ v (s x - x)) _ gen
+    use v (s gen - gen)
+    intro y hy
+    simp only [Set.mem_range, Subtype.exists, exists_prop] at hy
+    rcases hy with ⟨a, ha⟩
+    rw [← ha.2, show s a - a = s (⟨a, ha.1⟩ : 𝒪[L]) - (⟨a, ha.1⟩ : 𝒪[L]) by rfl]
+    apply decomp_val_map_sub_le_generator hgen hs'
+
+
+end adjoin_singleton
+
+end lowerIndex_inequality
+
 end lowerIndex
 
 section ScalarTower
@@ -161,14 +253,6 @@ variable {R : Type*} {R' S: Type*} {ΓR ΓS ΓA ΓB : outParam Type*} [CommRing
 [vS : Valued S ℤₘ₀]
 [Algebra R S] [Algebra R R'] [Algebra R' S] [IsScalarTower R R' S]
 
-/-- `This should be add to correct place` -/
-instance {R Γ₀: Type*} [Ring R] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀): Nonempty v.integer := by
-  use (0 : R)
-  change v 0 ≤ 1
-  simp only [_root_.map_zero, zero_le']
-
-instance {K Γ₀: Type*} [Field K] [LinearOrderedCommGroupWithZero Γ₀] [vK : Valued K Γ₀]: Nonempty 𝒪[K] := inferInstanceAs (Nonempty vK.v.integer)
-
 @[simp]
 theorem lowerIndex_refl : (i_[S/R] .refl) = ⊤ := by
   simp only [AlgEquiv.lowerIndex, AlgEquiv.coe_refl, id_eq, sub_self, _root_.map_zero, ciSup_const,
@@ -180,38 +264,18 @@ theorem truncatedLowerIndex_refl (u : ℚ) : AlgEquiv.truncatedLowerIndex R S u
 
 section lowerIndex_inequality
 
+section K_not_field
+
 variable {K K' L : Type*} {ΓK ΓK' : outParam Type*} [CommRing K] [Field K'] [Field L] [LinearOrderedCommGroupWithZero ΓK]
 [LinearOrderedCommGroupWithZero ΓK'] [vL : Valued L ℤₘ₀] [Algebra K L]
 [Algebra K K'] [Algebra K' L] [IsScalarTower K K' L]
 
-/-- `h` should be `𝒪[L] is finite over 𝒪[K]`-/
-theorem lowerIndex_ne_refl_of_FG (h : sorry) {s : L ≃ₐ[K] L} (hs : s ≠ .refl) : i_[L/K] s ≠ ⊤ := by
-  intro heq
-  simp only [AlgEquiv.lowerIndex, AddSubgroupClass.coe_sub,
-    dite_eq_left_iff, ENat.coe_ne_top, imp_false, not_not] at heq
-  have : ∀ x : vL.v.integer, v (s x - x) = 0 := by
-    intro x
-    apply le_of_eq at heq
-    rw [show (0 : ℤₘ₀) = ⊥ by rfl, eq_bot_iff]
-    refine (ciSup_le_iff' ?_).mp heq x -- this sorry is should be filled with bounded by one
-    use 1
-    intro a ha
-    rcases ha with ⟨y, hy⟩
-    rw [← hy, ← Valuation.mem_integer_iff]
-    apply Subring.sub_mem
-    sorry; sorry
-  apply hs
-  ext x
-  rw [AlgEquiv.coe_refl, id_eq, ← sub_eq_zero, ← Valuation.zero_iff vL.v]
-  rcases ValuationSubring.mem_or_inv_mem 𝒪[L] x with h | h
-  · sorry
-  · sorry
-
-theorem lowerIndex_ne_one {s : decompositionGroup K L} (hs : s ≠ 1) : i_[L/K] s ≠ ⊤ := by
+/-- Another version where `𝒪[L] is finite over 𝒪[K]` -/
+theorem lowerIndex_ne_one {s : L ≃ₐ[K] L} (hs' : s ∈ decompositionGroup K L) (hs : s ≠ .refl) : i_[L/K] s ≠ ⊤ := by
   intro heq
   simp only [AlgEquiv.lowerIndex, AddSubgroupClass.coe_sub,
     dite_eq_left_iff, ENat.coe_ne_top, imp_false, not_not] at heq
-  have hL : ∀ x : vL.v.integer, s.1 x = x := by
+  have hL : ∀ x : vL.v.integer, s x = x := by
     intro x
     apply le_of_eq at heq
     rw [← sub_eq_zero, ← Valuation.zero_iff vL.v, show (0 : ℤₘ₀) = ⊥ by rfl, eq_bot_iff]
@@ -219,54 +283,96 @@ theorem lowerIndex_ne_one {s : decompositionGroup K L} (hs : s ≠ 1) : i_[L/K]
     use 1
     intro a ha
     rcases ha with ⟨y, hy⟩
-    rw [← hy, ← Valuation.mem_integer_iff]
-    apply Subring.sub_mem
-    · rw [mem_integer_iff, val_map_le_one_iff s.2]
-      exact y.2
-    · exact y.2 -- should have be proved somewhere else?
+    rw [← hy]
+    exact sub_self_mem_integer hs' _
   apply hs
   ext x
-  rw [decompositionGroup_one, AlgEquiv.coe_refl, id_eq]
   rcases ValuationSubring.mem_or_inv_mem 𝒪[L] x with h | h
   · exact hL ⟨x, h⟩
   · calc
-    _ = (s.1 x⁻¹)⁻¹ := by simp only [inv_inv, map_inv₀]
-    _ = _ := by rw [hL ⟨x⁻¹, h⟩, inv_inv]
+    _ = (s x⁻¹)⁻¹ := by simp only [inv_inv, map_inv₀]
+    _ = _ := by rw [hL ⟨x⁻¹, h⟩, inv_inv, AlgEquiv.coe_refl, id_eq]
 
 @[simp]
-theorem lowerIndex_eq_top_iff_eq_refl {s : decompositionGroup K L} : i_[L/K] s = ⊤ ↔ s = 1 := by
+theorem lowerIndex_eq_top_iff_eq_refl {s : L ≃ₐ[K] L} (hs' : s ∈ decompositionGroup K L) : i_[L/K] s = ⊤ ↔ s = .refl := by
   constructor <;> intro h
   · contrapose! h
-    apply lowerIndex_ne_one h
-  · simp only [AlgEquiv.lowerIndex, h, OneMemClass.coe_one, AlgEquiv.one_apply, sub_self,
-    _root_.map_zero, ciSup_const, ↓reduceDite]
+    apply lowerIndex_ne_one hs' h
+  · simp only [h, lowerIndex_refl]
 
---the type of `n` should be changed
--- instead, change when use this theorem
-theorem mem_lowerRamificationGroup_iff {s : L ≃ₐ[K] L} (n : ℕ) : s ∈ G(L/K)_[n] ↔ (n + 1 : ℕ) ≤ i_[L/K] s := by
-  simp [AlgEquiv.truncatedLowerIndex]
-  constructor <;>
-  unfold lowerRamificationGroup AlgEquiv.lowerIndex
-  simp
-  rintro h
-  by_cases hs : iSup (fun x : vL.v.integer => (v (s x - x))) = 0
-  · simp at hs
-    simp [hs]
-  · simp at hs
-    simp [hs]
-    sorry
-  simp
-  sorry
+theorem iSup_val_map_sub_eq_zero_iff_eq_refl {s : L ≃ₐ[K] L} (hs' : s ∈ decompositionGroup K L) :
+  ⨆ x : vL.v.integer, vL.v (s x - x) = 0 ↔ s = .refl := by
+  rw [← lowerIndex_eq_top_iff_eq_refl]
+  simp only [AlgEquiv.toEquiv_eq_coe, EquivLike.coe_coe, AlgEquiv.lowerIndex, dite_eq_left_iff,
+    ENat.coe_ne_top, imp_false, Decidable.not_not]
+  exact hs'
+
+end K_not_field
+
+section K_is_field
 
+variable {K L : Type*} [Field K] [Field L]
+[vK : Valued K ℤₘ₀] [vL : Valued L ℤₘ₀] [Algebra K L] [IsValExtension K L]
+
+-- the type of `n` should be changed
+-- instead, change when use this theorem
+open Multiplicative in
+theorem mem_lowerRamificationGroup_iff_of_generator
+  {gen : 𝒪[L]} (hgen : Algebra.adjoin 𝒪[K] {gen} = ⊤)
+  {s : L ≃ₐ[K] L} (hs' : s ∈ decompositionGroup K L) (n : ℕ) :
+    s ∈ G(L/K)_[n] ↔ n + 1 ≤ i_[L/K] s := by
+  simp only [lowerRamificationGroup, Subtype.forall, Subgroup.mem_mk,
+    Set.mem_setOf_eq, AlgEquiv.lowerIndex]
+  by_cases hrefl : s = .refl
+  · simp only [hrefl, AlgEquiv.coe_refl, id_eq, sub_self, _root_.map_zero, ofAdd_sub, ofAdd_neg,
+    zero_le', implies_true, and_true, ciSup_const, ↓reduceDite, le_top, iff_true]
+    exact refl_mem_decompositionGroup K L
+  · have hne0 : ¬ ⨆ x : vL.v.integer, vL.v (s x - x) = 0 := by
+      rw [iSup_val_map_sub_eq_zero_iff_eq_refl hs']; exact hrefl
+    constructor
+    · intro ⟨_, hs⟩
+      simp only [hne0, ↓reduceDite, ge_iff_le]
+      rw [show (n : ℕ∞) + 1 = (n + 1 : ℕ) by rfl, ← ENat.some_eq_coe, WithTop.coe_le_coe,
+        Int.le_toNat (by simp only [Left.nonneg_neg_iff, toAdd_iSup_val_map_sub_le_zero_of_ne_zero hs']),
+        le_neg]
+      change _ ≤ toAdd (ofAdd (-(n + 1) : ℤ))
+      rw [toAdd_le]
+      /- The following part should be extracted.
+      It is also used in `toAdd_iSup_val_map_sub_le_zero_of_ne_zero`. -/
+      suffices ⨆ x : vL.v.integer, vL.v (s x - x) ≤ ofAdd (-(n + 1) : ℤ) from by
+        rw [← WithZero.coe_le_coe, WithZero.coe_unzero hne0]
+        exact this
+      apply ciSup_le
+      /- end -/
+      intro x
+      rw [neg_add']
+      exact hs x.1 x.2
+    · intro h
+      simp only [hs', true_and]
+      simp only [hne0, ↓reduceDite] at h
+      rw [show (n : ℕ∞) + 1 = (n + 1 : ℕ) by rfl, ← ENat.some_eq_coe, WithTop.coe_le_coe,
+        Int.le_toNat (by simp only [Left.nonneg_neg_iff, toAdd_iSup_val_map_sub_le_zero_of_ne_zero hs']),
+        le_neg] at h
+      change _ ≤ toAdd (ofAdd (-(n + 1) : ℤ)) at h
+      rw [toAdd_le, ← WithZero.coe_le_coe, WithZero.coe_unzero hne0, neg_add'] at h
+      intro x hx
+      apply le_trans _ h
+      apply le_ciSup (f := fun (x : vL.v.integer) ↦ v (s x - x)) _ ⟨x, hx⟩
+      use v (s gen - gen)
+      intro a
+      simp only [Set.mem_range, Subtype.exists, exists_prop, forall_exists_index, and_imp]
+      intro x hx heq
+      rw [← heq]
+      apply decomp_val_map_sub_le_generator hgen hs' ⟨x, hx⟩
 
-theorem mem_lowerRamificationGroup_of_le_truncatedLowerIndex_sub_one {s : L ≃ₐ[K] L} {u r : ℚ} (h : u ≤ i_[L/K]ₜ r s - 1) : s ∈ G(L/K)_[⌈u⌉] := by
+theorem mem_lowerRamificationGroup_of_le_truncatedLowerIndex_sub_one {s : L ≃ₐ[K] L} (hs' : s ∈ decompositionGroup K L) {u r : ℚ} (h : u ≤ i_[L/K]ₜ r s - 1) : s ∈ G(L/K)_[⌈u⌉] := by
   unfold AlgEquiv.truncatedLowerIndex at h
   by_cases hs : i_[L/K] s = ⊤
   · simp [hs] at h
     --maybe there is a better way
     have : (⌈u⌉.toNat + 1) ≤ i_[L/K] s := by simp [hs]
-    convert (mem_lowerRamificationGroup_iff ⌈u⌉.toNat).2 this
-    sorry
+    convert (mem_lowerRamificationGroup_iff_of_generator sorry hs' ⌈u⌉.toNat).2 this
+    sorry; sorry
   · simp [hs] at h
     have : (⌈u⌉.toNat + 1) ≤ i_[L/K] s := by
       have h' : u + 1 ≤ min r ↑(WithTop.untop (i_[L/K] s) hs) := by linarith [h]
@@ -274,22 +380,15 @@ theorem mem_lowerRamificationGroup_of_le_truncatedLowerIndex_sub_one {s : L ≃
       rw [hnt]
       convert (le_min_iff.1 h').right
       sorry
-    convert (mem_lowerRamificationGroup_iff ⌈u⌉.toNat).2 this
-    sorry
+    convert (mem_lowerRamificationGroup_iff_of_generator sorry hs' ⌈u⌉.toNat).2 this
+    sorry; sorry
 
 theorem le_truncatedLowerIndex_sub_one_iff_mem_lowerRamificationGroup (s : L ≃ₐ[K] L) (u : ℚ) (r : ℚ) (h : u + 1 ≤ r) : u ≤ i_[L/K]ₜ r s - 1 ↔ s ∈ G(L/K)_[⌈u⌉] := by
   constructor
   apply mem_lowerRamificationGroup_of_le_truncatedLowerIndex_sub_one
-  rintro hs
-  unfold AlgEquiv.truncatedLowerIndex
-  by_cases hc : i_[L/K] s = ⊤
-  · simp [hc]
-    linarith [h]
-  · have : ⌈u⌉.toNat + 1 ≤ i_[L/K] s := by
-      sorry
-      --apply (mem_lowerRamificationGroup_iff ⌈u⌉.toNat).1 hs
-    simp [hc]
-    sorry
+  sorry; sorry
+
+end K_is_field
 
 end lowerIndex_inequality
 
@@ -346,8 +445,8 @@ variable (K L : Type*) [Field K] [Field L] [vK : Valued K ℤₘ₀] [IsDiscrete
 
 section algebra_instances
 
-/-- The conditions might be too strong.
-The proof is almost the SAME with `Valuation.mem_integer_of_mem_integral_closure`. -/
+/-- 1. The conditions might be too strong.
+2. The proof is almost the SAME with `Valuation.mem_integer_of_mem_integral_closure`. -/
 instance instIsIntegrallyClosedToValuationSubring : IsIntegrallyClosed 𝒪[K] := by
   rw [isIntegrallyClosed_iff K]
   intro x ⟨p, hp⟩
@@ -374,9 +473,7 @@ attribute [local instance 1001] Algebra.toSMul
 
 instance : IsScalarTower 𝒪[K] 𝒪[L] L := inferInstanceAs (IsScalarTower vK.v.integer vL.v.integer L)
 
-#check IsIntegralClosure.of_isIntegrallyClosed
-
-instance [CompleteSpace K]: Algebra.IsIntegral 𝒪[K] 𝒪[L] where
+instance [CompleteSpace K] : Algebra.IsIntegral 𝒪[K] 𝒪[L] where
   isIntegral := by
     intro ⟨x, hx⟩
     rw [show 𝒪[L] = valuationSubring vL.v by rfl,
@@ -386,8 +483,7 @@ instance [CompleteSpace K]: Algebra.IsIntegral 𝒪[K] 𝒪[L] where
     rcases hx with ⟨p, hp⟩
     refine ⟨p, hp.1, ?_⟩
     ext
-    rw [show (0 : 𝒪[L]).val = 0 by rfl, ← hp.2,
-      show algebraMap (vK.v.valuationSubring) L = algebraMap 𝒪[K] L by rfl]
+    rw [show (0 : 𝒪[L]).val = 0 by rfl, ← hp.2]
     calc
       _ = 𝒪[L].subtype (eval₂ (algebraMap 𝒪[K] 𝒪[L]) ⟨x, hx⟩ p) := rfl
       _ = _ := by
@@ -395,60 +491,83 @@ instance [CompleteSpace K]: Algebra.IsIntegral 𝒪[K] 𝒪[L] where
         simp only [ValuationSubring.algebraMap_def]
         congr
 
-instance instIsIntegralClosureToValuationSubring [CompleteSpace K] : IsIntegralClosure 𝒪[L] 𝒪[K] L := by
+instance [CompleteSpace K] : IsIntegralClosure 𝒪[L] 𝒪[K] L := by
   apply IsIntegralClosure.of_isIntegrallyClosed 𝒪[L] 𝒪[K] L
 
-
 /-- Can't be inferred within 20000 heartbeats. -/
-instance instIsNoetherianToValuationSubring : IsNoetherianRing 𝒪[K] := PrincipalIdealRing.isNoetherianRing
+instance : IsNoetherianRing 𝒪[K] := PrincipalIdealRing.isNoetherianRing
 
-instance instNoethertianToValuationSubringExtension [CompleteSpace K] [IsSeparable K L] : IsNoetherian 𝒪[K] 𝒪[L] :=
+instance [CompleteSpace K] [IsSeparable K L] : IsNoetherian 𝒪[K] 𝒪[L] :=
   IsIntegralClosure.isNoetherian 𝒪[K] K L 𝒪[L]
 
 noncomputable def PowerBasisValExtension [CompleteSpace K] [IsSeparable K L] [IsSeparable (LocalRing.ResidueField 𝒪[K]) (LocalRing.ResidueField 𝒪[L])] : PowerBasis 𝒪[K] 𝒪[L] :=
   letI : Nontrivial vL.v := nontrivial_of_valExtension K L
   PowerBasisExtDVR (integerAlgebra_injective K L)
 
+example [CompleteSpace K] [IsSeparable K L] :
+  Algebra.FiniteType 𝒪[K] 𝒪[L] := inferInstance
+
 end algebra_instances
 
 variable {K L}
 variable [CompleteSpace K]
 
-theorem AlgEquiv.val_map_powerBasis_sub_ne_zero (pb : PowerBasis 𝒪[K] 𝒪[L]) {s : L ≃ₐ[K] L} (hs : s ≠ .refl) : vL.v (s pb.gen - pb.gen) ≠ 0 := by
+theorem AlgEquiv.mem_decompositionGroup [CompleteSpace K] (s : L ≃ₐ[K] L) : s ∈ decompositionGroup K L := by
+  rw [decompositionGroup_eq_top]
+  exact Subgroup.mem_top s
+
+/-- Should be strenthened to ` > 0`-/
+theorem AlgEquiv.val_map_generator_sub_ne_zero {gen : 𝒪[L]} (hgen : Algebra.adjoin 𝒪[K] {gen} = ⊤) {s : L ≃ₐ[K] L} (hs : s ≠ .refl) : vL.v (s gen - gen) ≠ 0 := by
   by_contra h
   rw [zero_iff, sub_eq_zero] at h
   apply hs
   rw [AlgEquiv.eq_iff_ValuationSubring]
-  apply PowerBasis.algEquiv_ext pb
+  apply Algebra.algHomClass_ext_generator hgen
   ext; simp only [AlgEquiv.restrictValuationSubring_apply, h, AlgEquiv.coe_refl, id_eq]
 
+/--  The orginal proof uses `PowerBasis.adjoin_gen_eq_top`.
+Should be strenthened to ` > 0`-/
+theorem AlgEquiv.val_map_powerBasis_sub_ne_zero (pb : PowerBasis 𝒪[K] 𝒪[L]) {s : L ≃ₐ[K] L} (hs : s ≠ .refl) :
+  vL.v (s pb.gen - pb.gen) ≠ 0 :=
+  s.val_map_generator_sub_ne_zero (PowerBasis.adjoin_gen_eq_top pb) hs
+
 open Polynomial in
-theorem AlgEquiv.val_map_sub_le_powerBasis (pb : PowerBasis 𝒪[K] 𝒪[L]) (s : L ≃ₐ[K] L) (x : 𝒪[L]) : vL.v (s x - x) ≤ vL.v (s pb.gen - pb.gen) := by
+theorem AlgEquiv.val_map_sub_le_generator {gen : 𝒪[L]} (hgen : Algebra.adjoin 𝒪[K] {gen} = ⊤) (s : L ≃ₐ[K] L) (x : 𝒪[L]) : v (s x - x) ≤ v (s gen - gen) := by
   by_cases hs : s = .refl
   · subst hs
     simp only [AlgEquiv.coe_refl, id_eq, sub_self, _root_.map_zero, le_refl]
-  rcases PowerBasis.exists_eq_aeval' pb x with ⟨f, hf⟩
+  rcases Algebra.exists_eq_aeval_generator hgen x with ⟨f, hf⟩
   subst hf
-  rcases taylor_order_zero_apply_aeval f pb.gen ((AlgEquiv.restrictValuationSubring s) pb.gen - pb.gen) with ⟨b, hb⟩
+  rcases taylor_order_zero_apply_aeval f gen ((AlgEquiv.restrictValuationSubring s) gen - gen) with ⟨b, hb⟩
   rw [add_sub_cancel, add_comm, ← sub_eq_iff_eq_add, aeval_algHom_apply, Subtype.ext_iff] at hb
   simp only [AddSubgroupClass.coe_sub, AlgEquiv.restrictValuationSubring_apply, Submonoid.coe_mul, Subsemiring.coe_toSubmonoid, Subring.coe_toSubsemiring] at hb
   rw [hb, Valuation.map_mul]
-  nth_rw 2 [← mul_one (v (s ↑pb.gen - ↑pb.gen))]
+  nth_rw 2 [← mul_one (v (s gen - gen))]
   rw [mul_le_mul_left₀]
   · exact b.2
-  · apply AlgEquiv.val_map_powerBasis_sub_ne_zero pb hs
+  · apply AlgEquiv.val_map_generator_sub_ne_zero hgen hs
 
-theorem AlgEquiv.iSup_val_map_sub_eq_powerBasis (pb : PowerBasis 𝒪[K] 𝒪[L]) (s : L ≃ₐ[K] L) :
-  ⨆ x : vL.v.integer, v (s x - x) = v (s pb.gen - pb.gen) := by
+open Polynomial in
+/-- The orginal proof uses `PowerBasis.exists_eq_aeval`. -/
+theorem AlgEquiv.val_map_sub_le_powerBasis (pb : PowerBasis 𝒪[K] 𝒪[L]) (s : L ≃ₐ[K] L) (x : 𝒪[L]) : vL.v (s x - x) ≤ vL.v (s pb.gen - pb.gen) := AlgEquiv.val_map_sub_le_generator (PowerBasis.adjoin_gen_eq_top pb) s x
+
+theorem AlgEquiv.iSup_val_map_sub_eq_generator {gen : 𝒪[L]} (hgen : Algebra.adjoin 𝒪[K] {gen} = ⊤) (s : L ≃ₐ[K] L) :
+  ⨆ x : vL.v.integer, v (s x - x) = v (s gen - gen) := by
   apply le_antisymm
-  · apply ciSup_le <| AlgEquiv.val_map_sub_le_powerBasis pb s
-  · apply le_ciSup (f := fun (x : 𝒪[L]) ↦ v (s x - x)) _ pb.gen
-    use v (s pb.gen - pb.gen)
+  · letI : Nonempty 𝒪[L] := inferInstanceAs (Nonempty vL.v.integer)
+    apply ciSup_le <| AlgEquiv.val_map_sub_le_generator hgen s
+  · apply le_ciSup (f := fun (x : 𝒪[L]) ↦ v (s x - x)) _ gen
+    use v (s gen - gen)
     intro y hy
     simp only [Set.mem_range, Subtype.exists, exists_prop] at hy
     rcases hy with ⟨a, ha⟩
     rw [← ha.2, show s a - a = s (⟨a, ha.1⟩ : 𝒪[L]) - (⟨a, ha.1⟩ : 𝒪[L]) by rfl]
-    apply AlgEquiv.val_map_sub_le_powerBasis
+    apply AlgEquiv.val_map_sub_le_generator hgen
+
+/-- The original proof uses `AlgEquiv.val_map_sub_le_powerBasis`. -/
+theorem AlgEquiv.iSup_val_map_sub_eq_powerBasis (pb : PowerBasis 𝒪[K] 𝒪[L]) (s : L ≃ₐ[K] L) :
+  ⨆ x : vL.v.integer, v (s x - x) = v (s pb.gen - pb.gen) :=
+  AlgEquiv.iSup_val_map_sub_eq_generator (PowerBasis.adjoin_gen_eq_top pb) s
 
 open Classical in
 /-- Should I `open Classical`? -/
@@ -460,39 +579,141 @@ theorem lowerIndex_of_powerBasis (pb : PowerBasis 𝒪[K] 𝒪[L]) (s : L ≃ₐ
   · unfold AlgEquiv.lowerIndex
     simp only [h, AlgEquiv.iSup_val_map_sub_eq_powerBasis pb, AlgEquiv.val_map_powerBasis_sub_ne_zero pb h, ↓reduceDite]
 
-#synth Fintype (L ≃ₐ[K] L)
-
 theorem lowerIndex_ne_refl {s : L ≃ₐ[K] L} (hs : s ≠ .refl) : i_[L/K] s ≠ ⊤ := by
-  have : s ∈ decompositionGroup K L := by
-    rw [decompositionGroup_eq_top]
-    exact Subgroup.mem_top s
-  rw [show s = (⟨s, this⟩ : decompositionGroup K L).1 by rfl]
   apply lowerIndex_ne_one
-  intro h
-  rw [Subtype.ext_iff, decompositionGroup_one] at h
-  exact hs h
+  rw [decompositionGroup_eq_top]
+  apply Subgroup.mem_top s
+  exact hs
 
 variable (K L) in
-theorem aux1 : ⨆ s : {s : (L ≃ₐ[K] L) // s ≠ .refl}, i_[L/K] s ≠ ⊤ := by
+theorem iSup_ne_refl_lowerIndex_ne_top [Nontrivial (L ≃ₐ[K] L)] :
+  ⨆ s : {s : (L ≃ₐ[K] L) // s ≠ .refl}, i_[L/K] s ≠ ⊤ := by
   rw [← lt_top_iff_ne_top, iSup_lt_iff]
-  sorry
-
-#check le_truncatedLowerIndex_sub_one_iff_mem_lowerRamificationGroup
-theorem aux0 {pb : PowerBasis 𝒪[K] 𝒪[L]}
-  {u : ℕ} (hu : u > ⨆ s : {s : (L ≃ₐ[K] L) // s ≠ .refl}, i_[L/K] s)
-  {s : L ≃ₐ[K] L} (hs : s ∈ G(L/K)_[u]) : s = .refl := by
-  sorry
-
+  let f : {s : (L ≃ₐ[K] L) // s ≠ .refl} → ℕ :=
+    fun s ↦ WithTop.untop _ (lowerIndex_ne_refl s.2)
+  letI : Nonempty {s : (L ≃ₐ[K] L) // s ≠ .refl} := Exists.casesOn (exists_ne AlgEquiv.refl)
+    fun s hs ↦ Nonempty.intro ⟨s, hs⟩
+  rcases Finite.exists_max f with ⟨a, ha⟩
+  use f a
+  constructor
+  · exact WithTop.coe_lt_top _
+  · intro s
+    have : i_[L/K] s = f s := by
+      rw [← ENat.some_eq_coe, WithTop.coe_untop]
+    simp only [ne_eq, this, Nat.cast_le, ha]
+
+theorem aux0 [IsSeparable K L] [IsSeparable (LocalRing.ResidueField 𝒪[K]) (LocalRing.ResidueField 𝒪[L])]
+  {n : ℕ} (hu : n > ⨆ s : {s : (L ≃ₐ[K] L) // s ≠ .refl}, i_[L/K] s)
+  {s : L ≃ₐ[K] L} (hs : s ∈ G(L/K)_[n]) : s = .refl := by
+  apply (mem_lowerRamificationGroup_iff_of_generator (PowerBasis.adjoin_gen_eq_top (PowerBasisValExtension K L)) s.mem_decompositionGroup n).mp at hs
+  by_contra! h
+  rw [ENat.add_one_le_iff (by simp only [ne_eq, ENat.coe_ne_top, not_false_eq_true])] at hs
+  have : i_[L/K] s < n := by
+    apply lt_of_le_of_lt _ hu
+    rw [show s = (⟨s, h⟩ : {s // s ≠ .refl}).1 by rfl]
+    apply le_iSup (fun (x : {s // s ≠ .refl}) => i_[L/K] x) (⟨s, h⟩ : {s // s ≠ .refl})
+  apply lt_asymm hs this
 
 -- this uses local fields and bichang's work, check if the condition is too strong..., It should be O_L is finitely generated over O_K
-theorem exist_lowerRamificationGroup_eq_bot [LocalField K] [LocalField L] : ∃ u : ℤ, G(L/K)_[u] = ⊥ := by
-  use (WithTop.untop _ (aux1 K L) : ℕ) + 1
-  sorry
+theorem exist_lowerRamificationGroup_eq_bot [CompleteSpace K] [IsSeparable K L]
+  [IsSeparable (LocalRing.ResidueField 𝒪[K]) (LocalRing.ResidueField 𝒪[L])] :
+    ∃ u : ℤ, G(L/K)_[u] = ⊥ := by
+  by_cases h : Nontrivial (L ≃ₐ[K] L)
+  · use (WithTop.untop _ (iSup_ne_refl_lowerIndex_ne_top K L) : ℕ) + 1
+    rw [eq_bot_iff]
+    intro s hs
+    rw [Subgroup.mem_bot, AlgEquiv.aut_one, aux0 _ hs]
+    rw [← ENat.some_eq_coe]
+    simp only [WithTop.coe_add, WithTop.coe_untop, WithTop.coe_one, gt_iff_lt]
+    nth_rw 1 [← add_zero (⨆ s : {s : (L ≃ₐ[K] L) // s ≠ .refl}, i_[L/K] s)]
+    have : (0 : ℕ∞) < 1 := by
+      rw [← ENat.coe_one, ← ENat.some_eq_coe, WithTop.zero_lt_coe]
+      exact zero_lt_one
+    convert WithTop.add_lt_add_left (iSup_ne_refl_lowerIndex_ne_top K L) this
+  · use 0
+    rw [eq_bot_iff]
+    intro s _
+    rw [Subgroup.mem_bot, AlgEquiv.aut_one]
+    letI : Subsingleton (L ≃ₐ[K] L) := not_nontrivial_iff_subsingleton.mp h
+    apply Subsingleton.allEq
+
+variable [LocalField K] [LocalField L] [IsSeparable K L]
 
 end eq_bot
 
 end ExhausiveSeperated
 
+section sum_lowerIndex
+#check lowerIndex_of_powerBasis
+#check PowerBasisValExtension
+
+open LocalField
+
+variable {K M L : Type*} [Field K] [Field M] [Field L]
+[Algebra K L] [Algebra K M] [Algebra M L] [IsScalarTower K M L]
+[FiniteDimensional K L] [FiniteDimensional K M] [FiniteDimensional M L]
+[Normal K M]
+[vK : Valued K ℤₘ₀] [IsDiscrete vK.v]
+[vM : Valued M ℤₘ₀] [IsDiscrete vM.v]
+[vL : Valued L ℤₘ₀] [IsDiscrete vL.v]
+[IsValExtension K L] [IsValExtension M L]
+[CompleteSpace K]
+
+-- #synth FiniteDimensional M L
+
+#check AlgEquiv.restrictNormalHom_surjective
+
+variable (σ : M ≃ₐ[K] M) (s : L ≃ₐ[K] L)
+#check s.restrictNormal M
+#check (AlgEquiv.restrictNormalHom (K₁ := L) M)⁻¹' {σ}
+#synth Finite ((AlgEquiv.restrictNormalHom (K₁ := L) M)⁻¹' {σ})
+#check Finset.sum
+
+#check LocalField
+
+#check aux2 K L
+
+#check Eq.subst
+
+open Finset in
+@[deprecated WithTop.sum_eq_top_iff]
+theorem ENat.sum_eq_top_of_map_eq_top {α : Type*} [DecidableEq α] {f : α → ℕ∞} {s : Finset α}
+  {a : α} (has : a ∈ s) (hfa : f a = ⊤) :
+    ∑ x ∈ s, f x = ⊤ := by
+  induction s using Finset.induction with
+  | empty => contradiction
+  | @insert b t hb ht =>
+    rcases mem_insert.mp has with h | h <;> rw [sum_insert hb]
+    · subst h
+      rw [hfa, WithTop.top_add]
+    · rw [ht h, WithTop.add_top]
+
+open Classical AlgEquiv in
+theorem prop3
+  (σ : M ≃ₐ[K] M) (x : PowerBasis 𝒪[K] 𝒪[L]) (y : PowerBasis 𝒪[M] 𝒪[L]) :
+    ∑ s ∈ ((restrictNormalHom M)⁻¹' {σ}), i_[L/K] s
+    = (ramificationIdx K L) * i_[M/K] σ := by
+  by_cases hσ : σ = .refl
+  · subst hσ
+    rw [lowerIndex_refl, ENat.mul_top]
+    · have : (.refl : L ≃ₐ[K] L) ∈ (restrictNormalHom M)⁻¹' {.refl} := by
+        rw [Set.mem_preimage, Set.mem_singleton_iff, ← AlgEquiv.aut_one, ← AlgEquiv.aut_one,
+          _root_.map_one]
+      rw [WithTop.sum_eq_top_iff]
+      exact ⟨.refl, Set.mem_toFinset.mpr this, lowerIndex_refl⟩
+    · intro h
+      rw [← ENat.coe_zero, ← ENat.some_eq_coe, WithTop.coe_eq_coe] at h
+      exact aux2 K L h
+  ·
+    /- Need:
+    2. all valuations are discrete
+    3. 𝒪[L] / 𝒪[M] admits a power basis b, so that the minpoly of b over M has coeff in 𝒪[M]
+    -/
+    sorry
+
+
+end sum_lowerIndex
+
 section aux
 
 variable {K K' L : Type*} {ΓK : outParam Type*} [Field K] [Field K'] [Field L] [vK' : Valued K' ℤₘ₀] [vL : Valued L ℤₘ₀] [IsDiscrete vK'.v] [IsDiscrete vL.v] [Algebra K L] [Algebra K K'] [Algebra K' L] [IsScalarTower K K' L] [IsValExtension K' L] [Normal K K'] [Normal K L] [FiniteDimensional K L] [FiniteDimensional K K']
diff --git a/RamificationGroup/Unused/RamificationIndex.lean b/RamificationGroup/Unused/RamificationIndex.lean
index ab652e3..7aaac51 100644
--- a/RamificationGroup/Unused/RamificationIndex.lean
+++ b/RamificationGroup/Unused/RamificationIndex.lean
@@ -1,8 +1,9 @@
 import RamificationGroup.Valued.Defs
 import RamificationGroup.Valued.Hom.Basic
 import RamificationGroup.Valued.Hom.Discrete
+import RamificationGroup.LowerNumbering
 
-open DiscreteValuation
+open DiscreteValuation Valuation Valued
 
 namespace ValRingHom
 
@@ -11,4 +12,20 @@ variable {R S : Type*} {ΓR ΓS : outParam Type*} [Ring R] [Ring S] [DiscretelyV
 def ramificationIndex {R S : Type*} {ΓR ΓS : outParam Type*} [Ring R] [Ring S] [DiscretelyValued R] [DiscretelyValued S] (f : ValRingHom R S) : ℕ := sorry -- min of .v (image of elements of R that has val > 1 in S)
 -- `ℕ, not WithTop ℕ`
 
+variable {K K' L : Type*} {ΓK ΓK' : outParam Type*} [CommRing K] [Field K'] [Field L] [LinearOrderedCommGroupWithZero ΓK]
+[LinearOrderedCommGroupWithZero ΓK'] [vL : Valued L ℤₘ₀] [Algebra K L]
+[Algebra K K'] [Algebra K' L] [IsScalarTower K K' L]
+
+/-- `h` should be `𝒪[L] is finite over 𝒪[K]`-/
+theorem lowerIndex_ne_refl_of_FG (h : sorry) {s : L ≃ₐ[K] L} (hs : s ≠ .refl) : i_[L/K] s ≠ ⊤ := by
+  intro heq
+  simp only [AlgEquiv.lowerIndex, AddSubgroupClass.coe_sub,
+    dite_eq_left_iff, ENat.coe_ne_top, imp_false, not_not] at heq
+  have : ∀ x : vL.v.integer, v (s x - x) = 0 := sorry
+  apply hs; ext x
+  rw [AlgEquiv.coe_refl, id_eq, ← sub_eq_zero, ← Valuation.zero_iff vL.v]
+  rcases ValuationSubring.mem_or_inv_mem 𝒪[L] x with h | h
+  sorry; sorry
+
+
 -- properties of ramification index, multiplicativity
diff --git a/RamificationGroup/Valuation/Discrete.lean b/RamificationGroup/Valuation/Discrete.lean
index aedd35c..195aec1 100644
--- a/RamificationGroup/Valuation/Discrete.lean
+++ b/RamificationGroup/Valuation/Discrete.lean
@@ -266,9 +266,9 @@ theorem isEquiv_ofNontrivial : v.IsEquiv (ofNontrivial v) := by sorry
 
 #check DiscreteValuationRing
 
-instance instIsDiscreteToOfNontrivial : IsDiscrete (ofNontrivial v) := by sorry
+instance : IsDiscrete (ofNontrivial v) := by sorry
 
-instance instDiscreteValuationRingToNontrivial : DiscreteValuationRing v.valuationSubring :=
+instance : DiscreteValuationRing v.valuationSubring :=
   valuationSubring_DVR_of_equiv_discrete (isEquiv_ofNontrivial v)
 
 end DiscreteValuation
diff --git a/RamificationGroup/Valuation/Extension.lean b/RamificationGroup/Valuation/Extension.lean
index 51c8228..741e36f 100644
--- a/RamificationGroup/Valuation/Extension.lean
+++ b/RamificationGroup/Valuation/Extension.lean
@@ -18,7 +18,7 @@ variable [Algebra A B] [IsLocalRingHom (algebraMap A B)]
 variable [IsSeparable (ResidueField A) (ResidueField B)]
 variable [Module.Finite A B]
 
-instance instFiniteExtResidue : FiniteDimensional (ResidueField A) (ResidueField B) := FiniteDimensional_of_finite
+instance : FiniteDimensional (ResidueField A) (ResidueField B) := FiniteDimensional_of_finite
 
 variable (A) (B) in
 /-- There exists `x : B` generating `k_B` over `k_A` -/
diff --git a/RamificationGroup/Valued/Hom/Lift.lean b/RamificationGroup/Valued/Hom/Lift.lean
index b084ccb..823cb26 100644
--- a/RamificationGroup/Valued/Hom/Lift.lean
+++ b/RamificationGroup/Valued/Hom/Lift.lean
@@ -122,6 +122,31 @@ theorem elem_decompositionGroup_eq_iff_ValuationSubring (s t : decompositionGrou
   · ext; simpa only [DecompositionGroup.restrictValuationSubring_apply] using h x
   · simp only [← DecompositionGroup.restrictValuationSubring_apply, h x]
 
+def DecompositionGroup.restrictValuationSubring' {s : L ≃ₐ[K] L}
+  (h : s ∈ decompositionGroup K L) :
+    𝒪[L] ≃ₐ[𝒪[K]] 𝒪[L] := {
+    AlgHom.restrictValuationSubring (f := s) (by apply h) with
+  invFun := (AlgHom.restrictValuationSubring (f := ((s⁻¹ : L ≃ₐ[K] L) : L →ₐ[K] L)) (by convert (⟨s, h⟩ : decompositionGroup K L)⁻¹.2))
+  left_inv := by
+    intro x; ext; simp
+    convert AlgEquiv.symm_apply_apply _ _
+  right_inv := by
+    intro x; ext; simp
+    convert AlgEquiv.apply_symm_apply _ _
+  }
+
+@[simp]
+theorem DecompositionGroup.restrictValuationSubring_apply'
+  {s : L ≃ₐ[K] L} (h : s ∈ decompositionGroup K L) (x : 𝒪[L]) :
+  (DecompositionGroup.restrictValuationSubring' h) x = s x := rfl
+
+theorem elem_decompositionGroup_eq_iff_ValuationSubring' {s t : L ≃ₐ[K] L} (hs : s ∈ decompositionGroup K L) (ht : t ∈ decompositionGroup K L) :
+  s = t ↔ DecompositionGroup.restrictValuationSubring' hs = DecompositionGroup.restrictValuationSubring' ht := by
+  rw [ringHomClass_eq_iff_valuationSubring, AlgEquiv.ext_iff]
+  constructor <;> intro h x
+  · ext; simpa only [DecompositionGroup.restrictValuationSubring_apply] using h x
+  · simp only [hs, ← DecompositionGroup.restrictValuationSubring_apply', AlgEquiv.toEquiv_eq_coe,
+    EquivLike.coe_coe, h x, ht]
 end decomposition_grp
 
 section discrete
diff --git a/RamificationGroup/Valued/Hom/ValExtension'.lean b/RamificationGroup/Valued/Hom/ValExtension'.lean
index 2582bdc..31efa66 100644
--- a/RamificationGroup/Valued/Hom/ValExtension'.lean
+++ b/RamificationGroup/Valued/Hom/ValExtension'.lean
@@ -1,4 +1,5 @@
 import RamificationGroup.Valued.Hom.ValExtension
+import RamificationGroup.ForMathlib.LocalRing.Basic
 import RamificationGroup.Valuation.Discrete
 
 /-!
@@ -7,13 +8,13 @@ This file is a continuation of the file ValExtension.
 We break this file to simplify the import temporarily
 
 -/
-open Valuation Valued IsValExtension
+open Valuation Valued IsValExtension DiscreteValuation
 
 section nontrivial
 
 variable {R A : Type*} {ΓR ΓA : outParam Type*} [CommRing R] [Ring A]
   [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓA]
-  [Algebra R A] [vR : Valued R ΓR] [Nontrivial vR.v] [vA : Valued A ΓA] [h : IsValExtension R A]
+  [Algebra R A] [vR : Valued R ΓR] [Nontrivial vR.v] [vA : Valued A ΓA] [IsValExtension R A]
 
 variable (R A) in
 theorem nontrivial_of_valExtension : Nontrivial vA.v where
@@ -25,3 +26,41 @@ theorem nontrivial_of_valExtension : Nontrivial vA.v where
     simp only [_root_.map_zero, h0, not_false_eq_true]
 
 end nontrivial
+
+section ramification
+
+section general
+
+variable (K L : Type*) {ΓK ΓL : outParam Type*} [Field K] [Field L]
+    [LinearOrderedCommGroupWithZero ΓK] [LinearOrderedCommGroupWithZero ΓL]
+    [Algebra K L] [vK : Valued K ΓK] [vL : Valued L ΓL] [IsValExtension K L]
+
+/-- Should be renamed -/
+noncomputable def LocalField.ramificationIdx : ℕ :=
+  LocalRing.ramificationIdx 𝒪[K] 𝒪[L]
+
+open LocalField
+
+theorem aux2 [FiniteDimensional K L] : ramificationIdx K L ≠ 0 := by
+
+  sorry
+
+end general
+
+open LocalField
+
+section discrete
+
+variable (K L : Type*) {ΓK ΓL : outParam Type*} [Field K] [Field L]
+    [Algebra K L] [vK : Valued K ℤₘ₀] [vL : Valued L ℤₘ₀] [IsValExtension K L]
+
+theorem aux3 [FiniteDimensional K L] [IsDiscrete vK.v] [IsDiscrete vL.v]
+  (x : K) : vL.v (algebraMap K L x) = (vK.v x) ^ (ramificationIdx K L) := by
+  sorry
+
+
+end discrete
+
+#check Ideal.ramificationIdx
+
+end ramification
diff --git a/RamificationGroup/Valued/Hom/ValExtension.lean b/RamificationGroup/Valued/Hom/ValExtension.lean
index 2751a14..35fc35d 100644
--- a/RamificationGroup/Valued/Hom/ValExtension.lean
+++ b/RamificationGroup/Valued/Hom/ValExtension.lean
@@ -10,7 +10,7 @@ import RamificationGroup.Valued.Defs
 # Extension of Valuation
 
 In this file, we define the typeclass for valuation extensions and prove basic facts about
-extension of valuations. Let `A` be a `R` algebra, both `R` and `A` are equipped with valued
+extension of valuations. Let `A` be an `R` algebra, both `R` and `A` are equipped with valued
 instance. Here, extension of valuation means that the pullback of valuation on `A` is equivalent
 to the valuation on `R`. We only require equivalence, not equality of valuations here.
 
@@ -210,8 +210,7 @@ instance : Algebra 𝒪[R] 𝒪[A] := inferInstanceAs (Algebra vR.v.integer vA.v
 
 @[simp, norm_cast]
 theorem coe_algebraMap_valuationSubring (r : 𝒪[R]) :
-    ((algebraMap 𝒪[R] 𝒪[A]) r : A) = (algebraMap R A) (r : R) := by
-  rfl
+    ((algebraMap 𝒪[R] 𝒪[A]) r : A) = (algebraMap R A) (r : R) := rfl
 
 instance : IsLocalRingHom (algebraMap 𝒪[R] 𝒪[A]) where
     map_nonunit r hr := by
diff --git a/blueprint/src/blueprint.sty b/blueprint/src/blueprint.sty
index b63ffeb..f841e5b 100644
--- a/blueprint/src/blueprint.sty
+++ b/blueprint/src/blueprint.sty
@@ -10,4 +10,4 @@
 \newcommand{\home}[1]{}
 \newcommand{\github}[1]{}
 \newcommand{\dochome}[1]{}
-\newcommand{\notready}[1]{}
+\newcommand{\notready}{}
diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex
index f3581d3..3f291b0 100644
--- a/blueprint/src/content.tex
+++ b/blueprint/src/content.tex
@@ -14,14 +14,13 @@
 \tableofcontents
 
 \section{Extension of Valuation}
+\input{content/ext_val.tex}
 
 \section{Lower Ramification Group}
-
-\begin{definition}[Decomposition Group]
-
-\end{definition}
+\input{content/lower_rami.tex}
 
 \section{Upper Ramification Group}
+\input{content/upper_rami.tex}
 
 \section{Example}
 Here you can use LaTex. \cite{marcus}. You must cite something to make it work.
diff --git a/blueprint/src/content/ext_val.tex b/blueprint/src/content/ext_val.tex
new file mode 100644
index 0000000..e69de29
diff --git a/blueprint/src/content/lower_rami.tex b/blueprint/src/content/lower_rami.tex
new file mode 100644
index 0000000..3d7226f
--- /dev/null
+++ b/blueprint/src/content/lower_rami.tex
@@ -0,0 +1,42 @@
+\begin{definition}[Decomposition Group]
+    \label{decompositionGroup}
+    \lean{decompositionGroup}
+    \leanok
+    \uses{Valuation.IsEquiv_comap_symm,ValRingHom.comp,ValAlgEquiv.refl,ValAlgEquiv.symm}
+    The decomposition group of $L/K$ is the subgroup \[\{\sigma\in\Gal(L/K)\mid \sigma(\mathcal{O}_L) \subset \mathcal{O}_L\}\] of $\Gal(L/K)$ 
+\end{definition}
+
+\begin{definition}[Lower Index]
+    \label{lowerIndex}
+    \lean{lowerIndex}
+    \leanok
+    The lower index of $\sigma\in\Gal(L/K)$ is \[i_{L/K}(\sigma) := \begin{cases}
+        \infty, &\sigma = 1,\\
+        , &\sigma\ne 1.
+    \end{cases}\]
+\end{definition}
+
+\begin{theorem}
+    \label{lowerIndex_ne_one}
+
+\end{theorem}
+
+\begin{theorem}
+    \label{lowerIndex_eq_top_iff_eq_refl}
+    \lean{lowerIndex_eq_top_iff_eq_refl}
+    \leanok
+    \uses{decompositionGroup, lowerIndex}
+    If $\sigma\in\Gal(L/K)$ lies in the decomposition group of $L/K$, then \[i_{L/K}(\sigma) = \infty\iff s = 1.\]
+\end{theorem}
+\begin{proof}
+    \leanok
+    \uses{lowerIndex_ne_one}
+\end{proof}
+
+\begin{theorem}
+    \label{exist_lowerRamificationGroup_eq_bot}
+    \leanok
+    \lean{exist_lowerRamificationGroup_eq_bot}
+    \uses{lowerRamificationGroup,aux1,RamificationGroup,ValAlgEquiv.refl,Valuation.Nontrivial}
+    The lower ramification groups $\Gal(L/K)_{u}$ vanish for $u\in\Z$ large enough. 
+\end{theorem}
diff --git a/blueprint/src/content/upper_rami.tex b/blueprint/src/content/upper_rami.tex
new file mode 100644
index 0000000..e69de29
diff --git a/blueprint/src/demo.tex b/blueprint/src/demo.tex
index f2aacf2..ac0535f 100644
--- a/blueprint/src/demo.tex
+++ b/blueprint/src/demo.tex
@@ -1,4 +1,55 @@
 
+\begin{theorem}\label{Valuation.IsEquiv_comap_symm}
+        \leanok
+        \lean{Valuation.IsEquiv_comap_symm}
+        \uses{ValAlgEquiv.symm}
+                No documentation.
+    \end{theorem}
+
+\begin{proof}
+    \leanok
+\end{proof}
+
+\begin{definition}\label{Valued.decompositionGroup}
+        \leanok
+        \lean{Valued.decompositionGroup}
+        \uses{Valuation.IsEquiv_comap_symm,ValRingHom.comp,ValAlgEquiv.refl,ValAlgEquiv.symm}
+                No documentation.
+    \end{definition}
+
+\begin{theorem}\label{Valued.decompositionGroup_one}
+        \leanok
+        \lean{Valued.decompositionGroup_one}
+        \uses{Valued.decompositionGroup,ValRingHom.comp,ValAlgEquiv.refl}
+                This stupid theorem should be parametrized over `Subgroup (S ≃ₐ[R] S)`.
+    \end{theorem}
+
+\begin{proof}
+    \leanok
+\end{proof}
+
+\begin{theorem}\label{Valued.refl_mem_decompositionGroup}
+        \leanok
+        \lean{Valued.refl_mem_decompositionGroup}
+        \uses{Valued.decompositionGroup,Valued.decompositionGroup_one,eq_top,ValRingHom.comp,ValAlgEquiv.refl}
+                This stupid theorem should be parametrized over `Subgroup (S ≃ₐ[R] S)`.
+    \end{theorem}
+
+\begin{proof}
+    \leanok
+\end{proof}
+
+\begin{theorem}\label{Valued.decompositionGroup_eq_top}
+        \leanok
+        \lean{Valued.decompositionGroup_eq_top}
+        \uses{Valued.decompositionGroup,eq_top,ValAlgEquiv.algEquiv_preserve_val,ValRingHom.comp,DiscreteValuation.algEquiv_preserve_val_of_complete,IsValExtension}
+                No documentation.
+    \end{theorem}
+
+\begin{proof}
+    \leanok
+\end{proof}
+
 \begin{theorem}\label{ceil_nonpos}
         \leanok
         \lean{ceil_nonpos}
@@ -129,7 +180,7 @@
 
 \begin{theorem}\label{HerbrandFunction.Ramification_Group_Disjoint}
         \lean{HerbrandFunction.Ramification_Group_Disjoint}
-        \uses{lowerRamificationGroup,lowerRamificationGroup.antitone,ValAlgEquiv.symm,RamificationGroup}
+        \uses{lowerRamificationGroup,lowerRamificationGroup.antitone,RamificationGroup,ValAlgEquiv.symm}
                 No documentation.
     \end{theorem}
 
@@ -152,7 +203,7 @@
 
 \begin{theorem}\label{HerbrandFunction.mem_all_lowerRamificationGroup_iff}
         \lean{HerbrandFunction.mem_all_lowerRamificationGroup_iff}
-        \uses{HerbrandFunction.x_in_G_n,lowerRamificationGroup,lowerIndex_refl,lowerIndex_eq_top_iff_eq_refl,mem_lowerRamificationGroup_iff,eq_top,ValAlgEquiv.refl,lowerIndex,RamificationGroup}
+        \uses{HerbrandFunction.x_in_G_n,lowerRamificationGroup,lowerIndex_refl,lowerIndex_eq_top_iff_eq_refl,mem_lowerRamificationGroup_iff,eq_top,lowerIndex,RamificationGroup,ValAlgEquiv.refl}
                 No documentation.
     \end{theorem}
 
@@ -164,7 +215,7 @@
 
 \begin{theorem}\label{HerbrandFunction.G_n_or_G_lt_n}
         \lean{HerbrandFunction.G_n_or_G_lt_n}
-        \uses{HerbrandFunction.x_in_G_n,HerbrandFunction.mem_all_lowerRamificationGroup_iff,HerbrandFunction.m_lt_n_of_in_G_m_of_notin_G_n,G_n_or_G_lt_n,lowerRamificationGroup,ValAlgEquiv.refl,RamificationGroup}
+        \uses{HerbrandFunction.x_in_G_n,HerbrandFunction.mem_all_lowerRamificationGroup_iff,HerbrandFunction.m_lt_n_of_in_G_m_of_notin_G_n,G_n_or_G_lt_n,lowerRamificationGroup,RamificationGroup,ValAlgEquiv.refl}
                 No documentation.
     \end{theorem}
 
@@ -181,7 +232,7 @@
 
 \begin{theorem}\label{HerbrandFunction.phi_eq_sum_card}
         \lean{HerbrandFunction.phi_eq_sum_card}
-        \uses{HerbrandFunction.relindex_aux,lowerRamificationGroup,lowerRamificationGroup.antitone,ext,ValAlgEquiv.symm,RamificationGroup}
+        \uses{HerbrandFunction.relindex_aux,lowerRamificationGroup,lowerRamificationGroup.antitone,RamificationGroup,ext,ValAlgEquiv.symm}
                 No documentation.
     \end{theorem}
 
@@ -259,7 +310,7 @@
 
 \begin{theorem}\label{HerbrandFunction.truncatedLowerindex_eq_of_lt}
         \lean{HerbrandFunction.truncatedLowerindex_eq_of_lt}
-        \uses{lowerRamificationGroup,mem_lowerRamificationGroup_iff,ValAlgEquiv.trans,RamificationGroup}
+        \uses{lowerRamificationGroup,mem_lowerRamificationGroup_iff,RamificationGroup,ValAlgEquiv.trans}
                 No documentation.
     \end{theorem}
 
@@ -292,27 +343,27 @@
 
 \begin{definition}\label{lowerRamificationGroup}
         \lean{lowerRamificationGroup}
-        \uses{Valuation.IsEquiv_comap_symm,Valued.decompositionGroup,Valued.zero_le,IsValExtension.val_map_le_one_iff,ValRingHom.comp,ValAlgEquiv.symm,ValAlgEquiv.one_apply,RamificationGroup}
+        \uses{Valuation.IsEquiv_comap_symm,Valued.decompositionGroup,RamificationGroup,Valued.zero_le,IsValExtension.val_map_le_one_iff,ValRingHom.comp,ValAlgEquiv.symm,ValAlgEquiv.one_apply}
                 No documentation.
     \end{definition}
 
 \begin{theorem}\label{lowerRamificationGroup.antitone}
         \lean{lowerRamificationGroup.antitone}
-        \uses{lowerRamificationGroup,ValAlgEquiv.trans,RamificationGroup}
+        \uses{lowerRamificationGroup,RamificationGroup,ValAlgEquiv.trans}
                 No documentation.
     \end{theorem}
 
 \begin{theorem}\label{autCongr_mem_lowerRamificationGroup_iff}
         \lean{autCongr_mem_lowerRamificationGroup_iff}
-        \uses{lowerRamificationGroup,mem_lowerRamificationGroup_iff,ValRingHom.id,ValRingHom.comp,ValAlgEquiv.trans,ValAlgEquiv.trans_apply,lowerIndex,RamificationGroup}
+        \uses{lowerRamificationGroup,mem_lowerRamificationGroup_iff,lowerIndex,RamificationGroup,ValRingHom.id,ValRingHom.comp,ValAlgEquiv.trans,ValAlgEquiv.trans_apply}
                 No documentation.
     \end{theorem}
 
 \begin{theorem}\label{lowerIndex_refl}
         \leanok
         \lean{lowerIndex_refl}
-        \uses{ValRingHom.id,ValAlgEquiv.refl,ValAlgEquiv.coe_refl,lowerIndex}
-                `This should be add to correct place`
+        \uses{lowerIndex,ValRingHom.id,ValAlgEquiv.refl,ValAlgEquiv.coe_refl}
+                No documentation.
     \end{theorem}
 
 \begin{proof}
@@ -322,7 +373,7 @@
 \begin{theorem}\label{truncatedLowerIndex_refl}
         \leanok
         \lean{truncatedLowerIndex_refl}
-        \uses{lowerIndex_refl,ValAlgEquiv.refl,lowerIndex}
+        \uses{lowerIndex_refl,lowerIndex,ValAlgEquiv.refl}
                 No documentation.
     \end{theorem}
 
@@ -332,14 +383,14 @@
 
 \begin{theorem}\label{lowerIndex_ne_refl_of_FG}
         \lean{lowerIndex_ne_refl_of_FG}
-        \uses{lowerIndex_ne_refl,ext,ValRingHom.id,ValAlgEquiv.refl,ValAlgEquiv.coe_refl,lowerIndex}
+        \uses{lowerIndex_ne_refl,lowerIndex,ext,ValRingHom.id,ValAlgEquiv.refl,ValAlgEquiv.coe_refl}
                 `h` should be `𝒪[L] is finite over 𝒪[K]`
     \end{theorem}
 
 \begin{theorem}\label{lowerIndex_ne_one}
         \leanok
         \lean{lowerIndex_ne_one}
-        \uses{Valued.decompositionGroup,Valued.decompositionGroup_one,IsValExtension.val_map_le_one_iff,ext,ValRingHom.id,ValRingHom.comp,ValAlgEquiv.refl,ValAlgEquiv.coe_refl,lowerIndex}
+        \uses{Valued.decompositionGroup,lowerIndex,IsValExtension.val_map_le_one_iff,ext,ValRingHom.id,ValRingHom.comp,ValAlgEquiv.refl,ValAlgEquiv.coe_refl}
                 No documentation.
     \end{theorem}
 
@@ -350,7 +401,18 @@
 \begin{theorem}\label{lowerIndex_eq_top_iff_eq_refl}
         \leanok
         \lean{lowerIndex_eq_top_iff_eq_refl}
-        \uses{lowerIndex_ne_one,eq_top,Valued.decompositionGroup,ValRingHom.comp,ValAlgEquiv.refl,ValAlgEquiv.one_apply,lowerIndex}
+        \uses{Valued.decompositionGroup,lowerIndex_refl,lowerIndex_ne_one,eq_top,lowerIndex,ValRingHom.comp,ValAlgEquiv.refl}
+                No documentation.
+    \end{theorem}
+
+\begin{proof}
+    \leanok
+\end{proof}
+
+\begin{theorem}\label{aux2}
+        \leanok
+        \lean{aux2}
+        \uses{Valued.decompositionGroup,lowerIndex_eq_top_iff_eq_refl,eq_top,lowerIndex,ValRingHom.id,ValRingHom.comp,ValAlgEquiv.refl}
                 No documentation.
     \end{theorem}
 
@@ -360,19 +422,19 @@
 
 \begin{theorem}\label{mem_lowerRamificationGroup_iff}
         \lean{mem_lowerRamificationGroup_iff}
-        \uses{lowerRamificationGroup,lowerIndex,RamificationGroup}
+        \uses{Valued.decompositionGroup,Valued.refl_mem_decompositionGroup,lowerRamificationGroup,aux2,lowerIndex,RamificationGroup,Valued.zero_le,ValRingHom.id,ValRingHom.comp,ValAlgEquiv.refl,ValAlgEquiv.coe_refl}
                 No documentation.
     \end{theorem}
 
 \begin{theorem}\label{mem_lowerRamificationGroup_of_le_truncatedLowerIndex_sub_one}
         \lean{mem_lowerRamificationGroup_of_le_truncatedLowerIndex_sub_one}
-        \uses{lowerRamificationGroup,mem_lowerRamificationGroup_iff,RamificationGroup}
+        \uses{Valued.decompositionGroup,lowerRamificationGroup,mem_lowerRamificationGroup_iff,RamificationGroup,ValRingHom.comp}
                 No documentation.
     \end{theorem}
 
 \begin{theorem}\label{le_truncatedLowerIndex_sub_one_iff_mem_lowerRamificationGroup}
         \lean{le_truncatedLowerIndex_sub_one_iff_mem_lowerRamificationGroup}
-        \uses{lowerRamificationGroup,mem_lowerRamificationGroup_iff,mem_lowerRamificationGroup_of_le_truncatedLowerIndex_sub_one,lowerIndex,RamificationGroup}
+        \uses{lowerRamificationGroup,mem_lowerRamificationGroup_of_le_truncatedLowerIndex_sub_one,lowerIndex,RamificationGroup}
                 No documentation.
     \end{theorem}
 
@@ -399,27 +461,38 @@
 
 \begin{theorem}\label{lowerRamificationGroup_restrictScalars}
         \lean{lowerRamificationGroup_restrictScalars}
-        \uses{lowerRamificationGroup,ValRingHom.comp,RamificationGroup,AlgEquiv.restrictScalarsHom}
+        \uses{lowerRamificationGroup,AlgEquiv.restrictScalarsHom,RamificationGroup,ValRingHom.comp}
                 No documentation.
     \end{theorem}
 
 \begin{theorem}\label{lowerRamificationGroup_eq_decompositionGroup}
         \lean{lowerRamificationGroup_eq_decompositionGroup}
-        \uses{lowerRamificationGroup,eq_decompositionGroup,eq_top,Valued.decompositionGroup,IsValExtension.val_map_le_one_iff,ext,ValRingHom.comp,RamificationGroup}
+        \uses{Valued.decompositionGroup,lowerRamificationGroup,eq_decompositionGroup,eq_top,RamificationGroup,IsValExtension.val_map_le_one_iff,ext,ValRingHom.comp}
                 No documentation.
     \end{theorem}
 
 \begin{theorem}\label{lowerRamificationGroup_eq_top}
         \lean{lowerRamificationGroup_eq_top}
-        \uses{lowerRamificationGroup,lowerRamificationGroup_eq_decompositionGroup,eq_decompositionGroup,eq_top,Valued.decompositionGroup,Valued.decompositionGroup_eq_top,ValRingHom.comp,RamificationGroup,Valuation.Nontrivial,IsValExtension}
+        \uses{Valued.decompositionGroup,Valued.decompositionGroup_eq_top,lowerRamificationGroup,lowerRamificationGroup_eq_decompositionGroup,eq_decompositionGroup,eq_top,RamificationGroup,ValRingHom.comp,Valuation.Nontrivial,IsValExtension}
                 No documentation.
     \end{theorem}
 
+\begin{theorem}\label{AlgEquiv.mem_decompositionGroup}
+        \leanok
+        \lean{AlgEquiv.mem_decompositionGroup}
+        \uses{Valued.decompositionGroup,Valued.decompositionGroup_eq_top,eq_top,ValRingHom.comp}
+                Can't be inferred within 20000 heartbeats.
+    \end{theorem}
+
+\begin{proof}
+    \leanok
+\end{proof}
+
 \begin{theorem}\label{AlgEquiv.val_map_powerBasis_sub_ne_zero}
         \leanok
         \lean{AlgEquiv.val_map_powerBasis_sub_ne_zero}
-        \uses{ext,ValRingHom.id,ValAlgEquiv.refl,ValAlgEquiv.coe_refl,PowerBasis.algEquiv_ext,Valued.AlgEquiv.restrictValuationSubring,Valued.AlgEquiv.restrictValuationSubring_apply,Valued.AlgEquiv.eq_iff_ValuationSubring}
-                Can't be inferred within 20000 heartbeats.
+        \uses{PowerBasis.algEquiv_ext,ext,ValRingHom.id,ValAlgEquiv.refl,ValAlgEquiv.coe_refl,Valued.AlgEquiv.restrictValuationSubring,Valued.AlgEquiv.restrictValuationSubring_apply,Valued.AlgEquiv.eq_iff_ValuationSubring}
+                No documentation.
     \end{theorem}
 
 \begin{proof}
@@ -451,7 +524,7 @@
 \begin{theorem}\label{lowerIndex_of_powerBasis}
         \leanok
         \lean{lowerIndex_of_powerBasis}
-        \uses{lowerIndex_refl,AlgEquiv.val_map_powerBasis_sub_ne_zero,AlgEquiv.iSup_val_map_sub_eq_powerBasis,ValAlgEquiv.refl,lowerIndex}
+        \uses{lowerIndex_refl,AlgEquiv.val_map_powerBasis_sub_ne_zero,AlgEquiv.iSup_val_map_sub_eq_powerBasis,lowerIndex,ValAlgEquiv.refl}
                 Should I `open Classical`?
     \end{theorem}
 
@@ -462,7 +535,7 @@
 \begin{theorem}\label{lowerIndex_ne_refl}
         \leanok
         \lean{lowerIndex_ne_refl}
-        \uses{lowerIndex_ne_one,eq_top,Valued.decompositionGroup,Valued.decompositionGroup_one,Valued.decompositionGroup_eq_top,ext,ValRingHom.comp,ValAlgEquiv.refl,lowerIndex}
+        \uses{Valued.decompositionGroup,Valued.decompositionGroup_eq_top,lowerIndex_ne_one,eq_top,lowerIndex,ValRingHom.comp,ValAlgEquiv.refl}
                 No documentation.
     \end{theorem}
 
@@ -471,20 +544,27 @@
 \end{proof}
 
 \begin{theorem}\label{aux1}
+        \leanok
         \lean{aux1}
-        \uses{lowerRamificationGroup,le_truncatedLowerIndex_sub_one_iff_mem_lowerRamificationGroup,ValAlgEquiv.refl,RamificationGroup}
+        \uses{lowerIndex_ne_refl,lowerIndex,ValAlgEquiv.refl,Valuation.Nontrivial}
                 No documentation.
     \end{theorem}
 
-\begin{theorem}\label{aux0}
-        \lean{aux0}
-        \uses{ValAlgEquiv.refl}
+\begin{proof}
+    \leanok
+\end{proof}
+
+\begin{theorem}\label{aux0
+}
+        \lean{aux0
+}
+        \uses{Valued.decompositionGroup,lowerRamificationGroup,mem_lowerRamificationGroup_iff,RamificationGroup,ValRingHom.comp,ValAlgEquiv.refl,ValAlgEquiv.symm}
                 No documentation.
     \end{theorem}
 
 \begin{theorem}\label{exist_lowerRamificationGroup_eq_bot}
         \lean{exist_lowerRamificationGroup_eq_bot}
-        \uses{lowerRamificationGroup,aux1,RamificationGroup}
+        \uses{lowerRamificationGroup,aux1,RamificationGroup,ValAlgEquiv.refl,Valuation.Nontrivial}
                 No documentation.
     \end{theorem}
 
@@ -496,7 +576,7 @@
 
 \begin{theorem}\label{autCongr_mem_upperRamificationGroup_aux_iff}
         \lean{autCongr_mem_upperRamificationGroup_aux_iff}
-        \uses{HerbrandFunction.psi_eq_ofEquiv,lowerRamificationGroup,autCongr_mem_lowerRamificationGroup_iff,mem_lowerRamificationGroup_iff,upperRamificationGroup_aux,upperRamificationGroup,ValAlgEquiv.symm,RamificationGroup,IsValExtension}
+        \uses{HerbrandFunction.psi_eq_ofEquiv,lowerRamificationGroup,autCongr_mem_lowerRamificationGroup_iff,mem_lowerRamificationGroup_iff,upperRamificationGroup_aux,upperRamificationGroup,RamificationGroup,ValAlgEquiv.symm,IsValExtension}
                 No documentation.
     \end{theorem}
 
@@ -537,7 +617,7 @@
 
 \begin{theorem}\label{le_truncatedJ_sub_one_iff_mem_lowerRamificationGroup}
         \lean{le_truncatedJ_sub_one_iff_mem_lowerRamificationGroup}
-        \uses{lowerRamificationGroup,le_truncatedLowerIndex_sub_one_iff_mem_lowerRamificationGroup,exist_truncatedLowerIndex_eq_truncatedJ,mem_lowerRamificationGroup_of_le_truncatedJ_sub_one,ext,RamificationGroup,IsValExtension}
+        \uses{lowerRamificationGroup,le_truncatedLowerIndex_sub_one_iff_mem_lowerRamificationGroup,exist_truncatedLowerIndex_eq_truncatedJ,mem_lowerRamificationGroup_of_le_truncatedJ_sub_one,RamificationGroup,ext,IsValExtension}
                 No documentation.
     \end{theorem}
 
@@ -573,7 +653,7 @@
 
 \begin{theorem}\label{herbrand}
         \lean{herbrand}
-        \uses{HerbrandFunction.phi_strictMono,lowerRamificationGroup,le_truncatedLowerIndex_sub_one_iff_mem_lowerRamificationGroup,phi_truncatedJ_sub_one,le_truncatedJ_sub_one_iff_mem_lowerRamificationGroup,ext,ValAlgEquiv.symm,RamificationGroup}
+        \uses{HerbrandFunction.phi_strictMono,lowerRamificationGroup,le_truncatedLowerIndex_sub_one_iff_mem_lowerRamificationGroup,phi_truncatedJ_sub_one,le_truncatedJ_sub_one_iff_mem_lowerRamificationGroup,RamificationGroup,ext,ValAlgEquiv.symm}
                 No documentation.
     \end{theorem}
 
@@ -585,19 +665,19 @@
 
 \begin{theorem}\label{UpperRamificationGroup_aux.eq_decompositionGroup}
         \lean{UpperRamificationGroup_aux.eq_decompositionGroup}
-        \uses{HerbrandFunction.psi_eq_self_of_le_neg_one,lowerRamificationGroup,lowerRamificationGroup_eq_decompositionGroup,upperRamificationGroup_aux,upperRamificationGroup,eq_decompositionGroup,Valued.decompositionGroup,ValRingHom.comp,RamificationGroup}
+        \uses{Valued.decompositionGroup,HerbrandFunction.psi_eq_self_of_le_neg_one,lowerRamificationGroup,lowerRamificationGroup_eq_decompositionGroup,upperRamificationGroup_aux,upperRamificationGroup,eq_decompositionGroup,RamificationGroup,ValRingHom.comp}
                 No documentation.
     \end{theorem}
 
 \begin{theorem}\label{UpperRamificationGroup_aux.eq_top}
         \lean{UpperRamificationGroup_aux.eq_top}
-        \uses{UpperRamificationGroup_aux.eq_decompositionGroup,eq_decompositionGroup,eq_top,Valued.decompositionGroup,Valued.decompositionGroup_eq_top,ValRingHom.comp,RamificationGroup,IsValExtension}
+        \uses{Valued.decompositionGroup,Valued.decompositionGroup_eq_top,UpperRamificationGroup_aux.eq_decompositionGroup,eq_decompositionGroup,eq_top,RamificationGroup,ValRingHom.comp,IsValExtension}
                 No documentation.
     \end{theorem}
 
 \begin{theorem}\label{UpperRamificationGroup_aux.exist_eq_bot}
         \lean{UpperRamificationGroup_aux.exist_eq_bot}
-        \uses{lowerRamificationGroup,exist_lowerRamificationGroup_eq_bot,upperRamificationGroup_aux,upperRamificationGroup,ValRingHom.id,ValRingHom.comp,RamificationGroup,IsValExtension}
+        \uses{lowerRamificationGroup,exist_lowerRamificationGroup_eq_bot,upperRamificationGroup_aux,upperRamificationGroup,RamificationGroup,ValRingHom.id,ValRingHom.comp,IsValExtension}
                 No documentation.
     \end{theorem}
 
@@ -644,19 +724,19 @@
 
 \begin{theorem}\label{eq_UpperRamificationGroup_aux}
         \lean{eq_UpperRamificationGroup_aux}
-        \uses{upperRamificationGroup_aux,herbrand,herbrand',upperRamificationGroup,ext,ValRingHom.id,RamificationGroup,IsValExtension}
+        \uses{upperRamificationGroup_aux,herbrand,herbrand',upperRamificationGroup,RamificationGroup,ext,ValRingHom.id,IsValExtension}
                 No documentation.
     \end{theorem}
 
 \begin{theorem}\label{mem_iff_mem_UpperRamificationGroup_aux}
         \lean{mem_iff_mem_UpperRamificationGroup_aux}
-        \uses{upperRamificationGroup_aux,upperRamificationGroup,mem_iff,ext,ValRingHom.comp,RamificationGroup,IsValExtension}
+        \uses{upperRamificationGroup_aux,upperRamificationGroup,mem_iff,RamificationGroup,ext,ValRingHom.comp,IsValExtension}
                 No documentation.
     \end{theorem}
 
 \begin{theorem}\label{map_restrictNormalHom}
         \lean{map_restrictNormalHom}
-        \uses{upperRamificationGroup_aux,upperRamificationGroup,mem_iff_mem_UpperRamificationGroup_aux,mem_iff,ext,RamificationGroup}
+        \uses{upperRamificationGroup_aux,upperRamificationGroup,mem_iff_mem_UpperRamificationGroup_aux,mem_iff,RamificationGroup,ext}
                 No documentation.
     \end{theorem}
 
@@ -674,7 +754,7 @@
 
 \begin{theorem}\label{eq_decompositionGroup}
         \lean{eq_decompositionGroup}
-        \uses{UpperRamificationGroup_aux.eq_decompositionGroup,eq_UpperRamificationGroup_aux,Valued.decompositionGroup,ValRingHom.comp,RamificationGroup,IsValExtension}
+        \uses{Valued.decompositionGroup,UpperRamificationGroup_aux.eq_decompositionGroup,eq_UpperRamificationGroup_aux,RamificationGroup,ValRingHom.comp,IsValExtension}
                 No documentation.
     \end{theorem}
 
@@ -701,10 +781,10 @@
                 No documentation.
     \end{definition}
 
-\begin{theorem}\label{Valuation.IsEquiv_comap_symm}
+\begin{theorem}\label{PowerBasis.algEquiv_ext}
         \leanok
-        \lean{Valuation.IsEquiv_comap_symm}
-        \uses{ValAlgEquiv.symm}
+        \lean{PowerBasis.algEquiv_ext}
+        \uses{ext}
                 No documentation.
     \end{theorem}
 
@@ -712,47 +792,66 @@
     \leanok
 \end{proof}
 
-\begin{definition}\label{Valued.decompositionGroup}
+\begin{definition}\label{AlgEquiv.restrictScalarsHom}
         \leanok
-        \lean{Valued.decompositionGroup}
-        \uses{Valuation.IsEquiv_comap_symm,ValRingHom.comp,ValAlgEquiv.refl,ValAlgEquiv.symm}
+        \lean{AlgEquiv.restrictScalarsHom}
+        \uses{ext}
                 No documentation.
     \end{definition}
 
-\begin{theorem}\label{Valued.decompositionGroup_one}
-        \lean{Valued.decompositionGroup_one}
-        \uses{eq_top,Valued.decompositionGroup,ValRingHom.comp,ValAlgEquiv.refl}
+\begin{theorem}\label{DiscreteValuationRing.unit_mul_irreducible_of_irreducible}
+        \leanok
+        \lean{DiscreteValuationRing.unit_mul_irreducible_of_irreducible}
                 No documentation.
     \end{theorem}
 
-\begin{theorem}\label{Valued.decompositionGroup_eq_top}
-        \lean{Valued.decompositionGroup_eq_top}
-        \uses{eq_top,Valued.decompositionGroup,ValAlgEquiv.algEquiv_preserve_val,ValRingHom.comp,DiscreteValuation.algEquiv_preserve_val_of_complete,IsValExtension}
+\begin{proof}
+    \leanok
+\end{proof}
+
+\begin{theorem}\label{DiscreteValuationRing.mul_irreducible_of_not_unit}
+        \leanok
+        \lean{DiscreteValuationRing.mul_irreducible_of_not_unit}
+        \uses{Valued.maximalIdeal,ValAlgEquiv.symm}
                 No documentation.
     \end{theorem}
 
-\begin{theorem}\label{Valuation.integral_closure_eq_integer_of_helselian}
-        \lean{Valuation.integral_closure_eq_integer_of_helselian}
-        \uses{Valued.valuationSubring}
+\begin{proof}
+    \leanok
+\end{proof}
+
+\begin{theorem}\label{DiscreteValuationRing.mul_irreducible_square_of_not_unit_of_not_irreducible}
+        \leanok
+        \lean{DiscreteValuationRing.mul_irreducible_square_of_not_unit_of_not_irreducible}
+        \uses{DiscreteValuationRing.mul_irreducible_of_not_unit,ValRingHom.id}
                 No documentation.
     \end{theorem}
 
-\begin{theorem}\label{Valuation.integral_closure_eq_integer_of_complete_of_ext}
-        \lean{Valuation.integral_closure_eq_integer_of_complete_of_ext}
-        \uses{Valued.valuationSubring,ext,ValRingHom.comp}
-                WARNING : not mathematically true? more conditions?
+\begin{proof}
+    \leanok
+\end{proof}
+
+\begin{theorem}\label{DiscreteValuationRing.irreducible_of_irreducible_add_addVal_ge_two}
+        \leanok
+        \lean{DiscreteValuationRing.irreducible_of_irreducible_add_addVal_ge_two}
+        \uses{DiscreteValuationRing.unit_mul_irreducible_of_irreducible,LocalRing.is_unit_of_unit_add_nonunit}
+                No documentation.
     \end{theorem}
 
-\begin{theorem}\label{Valuation.unique_valuationSubring_of_ext}
-        \lean{Valuation.unique_valuationSubring_of_ext}
-        \uses{Valuation.integral_closure_eq_integer_of_complete_of_ext,unique_valuationSubring_of_ext,Valued.valuationSubring,ext,ValRingHom.comp}
+\begin{proof}
+    \leanok
+\end{proof}
+
+\begin{theorem}\label{DiscreteValuationRing.maximalIdeal_pow_eq_span_irreducible_pow}
+        \lean{DiscreteValuationRing.maximalIdeal_pow_eq_span_irreducible_pow}
+        \uses{Valued.maximalIdeal,maximalIdeal_eq}
                 No documentation.
     \end{theorem}
 
-\begin{theorem}\label{Valuation.unique_val_of_ext}
+\begin{theorem}\label{LocalRing.algebraMap_residue_compat}
         \leanok
-        \lean{Valuation.unique_val_of_ext}
-        \uses{unique_valuationSubring_of_ext,ValAlgebra,Valued.valuationSubring,ext,ValAlgEquiv}
+        \lean{LocalRing.algebraMap_residue_compat}
+        \uses{Valued.ResidueField,ValRingHom.id,ValRingHom.comp}
                 No documentation.
     \end{theorem}
 
@@ -760,10 +859,10 @@
     \leanok
 \end{proof}
 
-\begin{theorem}\label{ValAlgEquiv.algEnd_preserve_val}
+\begin{theorem}\label{LocalRing.residue_irreducible_eq_zero}
         \leanok
-        \lean{ValAlgEquiv.algEnd_preserve_val}
-        \uses{Valuation.unique_val_of_ext,ValAlgebra,ext,ValAlgebra.val_isEquiv_comap}
+        \lean{LocalRing.residue_irreducible_eq_zero}
+        \uses{Valued.maximalIdeal,ValRingHom.id}
                 No documentation.
     \end{theorem}
 
@@ -771,10 +870,10 @@
     \leanok
 \end{proof}
 
-\begin{theorem}\label{ValAlgEquiv.algEquiv_preserve_val}
+\begin{theorem}\label{LocalRing.is_unit_iff_residue_ne_zero}
         \leanok
-        \lean{ValAlgEquiv.algEquiv_preserve_val}
-        \uses{ValAlgEquiv.algEnd_preserve_val}
+        \lean{LocalRing.is_unit_iff_residue_ne_zero}
+        \uses{ValRingHom.id}
                 No documentation.
     \end{theorem}
 
@@ -782,46 +881,48 @@
     \leanok
 \end{proof}
 
-\begin{definition}\label{ValAlgEquiv.fromAlgEquiv}
-        \lean{ValAlgEquiv.fromAlgEquiv}
-        \uses{ValAlgEquiv.algEquiv_preserve_val,DiscreteValuation.fromAlgEquiv,ValAlgEquiv.mk'}
-                No documentation.
-    \end{definition}
-
-\begin{definition}\label{ValAlgEquiv.equivAlgEquiv}
-        \lean{ValAlgEquiv.equivAlgEquiv}
-        \uses{DiscreteValuation.fromAlgEquiv,DiscreteValuation.equivAlgEquiv,ValAlgEquiv}
+\begin{theorem}\label{LocalRing.residue_eq_add_irreducible}
+        \leanok
+        \lean{LocalRing.residue_eq_add_irreducible}
+        \uses{LocalRing.residue_irreducible_eq_zero,ValRingHom.id}
                 No documentation.
-    \end{definition}
+    \end{theorem}
 
-\begin{definition}\label{ValRingHom.ramificationIndex}
-        \lean{ValRingHom.ramificationIndex}
-        \uses{ValRingHom}
-                No documentation.
-    \end{definition}
+\begin{proof}
+    \leanok
+\end{proof}
 
-\begin{definition}\label{DiscreteValuation.ofInt}
+\begin{theorem}\label{LocalRing.is_unit_of_unit_add_nonunit}
         \leanok
-        \lean{DiscreteValuation.ofInt}
-        \uses{ValRingHom.id,ExtDVR.3}
+        \lean{LocalRing.is_unit_of_unit_add_nonunit}
                 No documentation.
-    \end{definition}
+    \end{theorem}
 
-\begin{definition}\label{DiscretelyValued.extensionFiniteDimension}
-        \lean{DiscretelyValued.extensionFiniteDimension}
-        \uses{ext}
+\begin{proof}
+    \leanok
+\end{proof}
+
+\begin{theorem}\label{LocalRing.maximalIdeal_eq_jacobson_of_bot}
+        \lean{LocalRing.maximalIdeal_eq_jacobson_of_bot}
+        \uses{Valued.maximalIdeal,maximalIdeal_eq,ValAlgEquiv.symm}
                 No documentation.
-    \end{definition}
+    \end{theorem}
 
-\begin{theorem}\label{Valuation.isEquiv_of_finiteDimensional}
-        \lean{Valuation.isEquiv_of_finiteDimensional}
-        \uses{ValAlgebra,ext,ValAlgebra.val_isEquiv_comap,ValAlgEquiv}
+\begin{theorem}\label{unique_of_valuation_extension}
+        \lean{unique_of_valuation_extension}
+        \uses{ValAlgebra,ext}
                 No documentation.
     \end{theorem}
 
-\begin{definition}\label{AlgEquiv.toValAlgEquiv}
-        \lean{AlgEquiv.toValAlgEquiv}
-        \uses{ValAlgEquiv,toValAlgEquiv}
+\begin{definition}\label{toValAlgEquiv}
+        \lean{toValAlgEquiv}
+        \uses{ValAlgEquiv}
+                No documentation.
+    \end{definition}
+
+\begin{definition}\label{Ideal.quotientAlgebra'}
+        \leanok
+        \lean{Ideal.quotientAlgebra'}
                 No documentation.
     \end{definition}
 
@@ -846,38 +947,30 @@
                 A valued algebra over a valued commutative ring `R`, is a valued ring `A` together with a ring map into the center of `A` that preserves the valuation.
     \end{definition}
 
-\begin{definition}\label{multiplicity'}
-        \leanok
-        \lean{multiplicity'}
-        \uses{ValRingHom.id}
-                `multiplicity a b` returns the largest natural number `n` such that
-  `a ^ n ∣ b`, as a `PartENat` or natural with infinity. If `∀ n, a ^ n ∣ b`,
-  then it returns `⊤`
+\begin{definition}\label{DiscretelyValued.extensionFiniteDimension}
+        \lean{DiscretelyValued.extensionFiniteDimension}
+        \uses{ext}
+                No documentation.
     \end{definition}
 
-\begin{theorem}\label{finite_nat_iff'}
-        \lean{finite_nat_iff'}
+\begin{theorem}\label{Valuation.isEquiv_of_finiteDimensional}
+        \lean{Valuation.isEquiv_of_finiteDimensional}
+        \uses{ValAlgebra,ext,ValAlgebra.val_isEquiv_comap,ValAlgEquiv}
                 No documentation.
     \end{theorem}
 
-\begin{definition}\label{padicValNat'}
-        \leanok
-        \lean{padicValNat'}
-                For `p ≠ 1`, the `p`-adic valuation of a natural `n ≠ 0` is the largest natural number `k` such
-that `p^k` divides `z`. If `n = 0` or `p = 1`, then `padicValNat p q` defaults to `0`.
-    \end{definition}
-
-\begin{theorem}\label{finite_ideal_iff}
-        \lean{finite_ideal_iff}
-        \uses{ValRingHom.id,ValRingHom.comp}
+\begin{definition}\label{AlgEquiv.toValAlgEquiv}
+        \lean{AlgEquiv.toValAlgEquiv}
+        \uses{toValAlgEquiv,ValAlgEquiv}
                 No documentation.
-    \end{theorem}
+    \end{definition}
 
-\begin{theorem}\label{ord_top}
-        \lean{ord_top}
-        \uses{finite_ideal_iff,ValRingHom.id,ValRingHom.comp}
+\begin{definition}\label{DiscreteValuation.ofInt}
+        \leanok
+        \lean{DiscreteValuation.ofInt}
+        \uses{ValRingHom.id,ExtDVR.3}
                 No documentation.
-    \end{theorem}
+    \end{definition}
 
 \begin{definition}\label{Valuation.leIdeal}
         \lean{Valuation.leIdeal}
@@ -924,81 +1017,207 @@
 \begin{definition}\label{CompleteDiscreteValuationRing}
         \leanok
         \lean{CompleteDiscreteValuationRing}
-        \uses{ext,CompleteValuationRing}
+        \uses{CompleteValuationRing,ext}
                 No documentation.
     \end{definition}
 
 \begin{definition}\label{CompleteValuationField}
         \leanok
         \lean{CompleteValuationField}
-        \uses{ext,CompleteValuationRing}
+        \uses{CompleteValuationRing,ext}
                 No documentation.
     \end{definition}
 
 \begin{definition}\label{CompleteDiscreteValuationField}
         \leanok
         \lean{CompleteDiscreteValuationField}
-        \uses{ext,ValRingHom.comp,CompleteValuationRing}
+        \uses{CompleteValuationRing,ext,ValRingHom.comp}
                 No documentation.
     \end{definition}
 
-\begin{theorem}\label{lowerindex_ge_iff_lowerramificationGroup}
-        \lean{lowerindex_ge_iff_lowerramificationGroup}
-                No documentation.
-    \end{theorem}
-
-\begin{theorem}\label{lowerindex_eq_iff_lowerramificationGroup}
-        \lean{lowerindex_eq_iff_lowerramificationGroup}
+\begin{definition}\label{ValRingHom.ramificationIndex}
+        \lean{ValRingHom.ramificationIndex}
+        \uses{ValRingHom}
                 No documentation.
-    \end{theorem}
+    \end{definition}
 
-\begin{theorem}\label{lowerramificationGroup_has_top}
-        \lean{lowerramificationGroup_has_top}
-        \uses{ValRingHom.comp,ValAlgEquiv,lowerIndex}
+\begin{definition}\label{multiplicity'}
+        \leanok
+        \lean{multiplicity'}
+        \uses{ValRingHom.id}
+                `multiplicity a b` returns the largest natural number `n` such that
+  `a ^ n ∣ b`, as a `PartENat` or natural with infinity. If `∀ n, a ^ n ∣ b`,
+  then it returns `⊤`
+    \end{definition}
+
+\begin{theorem}\label{finite_nat_iff'}
+        \lean{finite_nat_iff'}
                 No documentation.
     \end{theorem}
 
-\begin{theorem}\label{varphi'_pos}
-        \lean{varphi'_pos}
-        \uses{phi'_pos}
+\begin{definition}\label{padicValNat'}
+        \leanok
+        \lean{padicValNat'}
+                For `p ≠ 1`, the `p`-adic valuation of a natural `n ≠ 0` is the largest natural number `k` such
+that `p^k` divides `z`. If `n = 0` or `p = 1`, then `padicValNat p q` defaults to `0`.
+    \end{definition}
+
+\begin{theorem}\label{finite_ideal_iff}
+        \lean{finite_ideal_iff}
+        \uses{ValRingHom.id,ValRingHom.comp}
                 No documentation.
     \end{theorem}
 
-\begin{theorem}\label{varphi_mono_int}
-        \lean{varphi_mono_int}
-        \uses{varphi_mono,phi_mono_int,phi_mono}
+\begin{theorem}\label{ord_top}
+        \lean{ord_top}
+        \uses{finite_ideal_iff,ValRingHom.id,ValRingHom.comp}
                 No documentation.
     \end{theorem}
 
-\begin{theorem}\label{varphi_lt_int_ceil}
-        \lean{varphi_lt_int_ceil}
+\begin{theorem}\label{Valuation.integral_closure_eq_integer_of_helselian}
+        \lean{Valuation.integral_closure_eq_integer_of_helselian}
+        \uses{Valued.valuationSubring}
                 No documentation.
     \end{theorem}
 
-\begin{theorem}\label{varphi_mono_section}
-        \lean{varphi_mono_section}
-        \uses{varphi'_pos,varphi_mono,phi'_pos,phi_mono}
+\begin{theorem}\label{Valuation.integral_closure_eq_integer_of_complete_of_ext}
+        \lean{Valuation.integral_closure_eq_integer_of_complete_of_ext}
+        \uses{Valued.valuationSubring,ext,ValRingHom.comp}
+                WARNING : not mathematically true? more conditions?
+    \end{theorem}
+
+\begin{theorem}\label{Valuation.unique_valuationSubring_of_ext}
+        \lean{Valuation.unique_valuationSubring_of_ext}
+        \uses{Valuation.integral_closure_eq_integer_of_complete_of_ext,unique_valuationSubring_of_ext,Valued.valuationSubring,ext,ValRingHom.comp}
                 No documentation.
     \end{theorem}
 
-\begin{theorem}\label{varphi_mono}
-        \lean{varphi_mono}
-        \uses{varphi_mono_int,varphi_lt_int_ceil,varphi_mono_section,phi_mono_int,phi_mono}
+\begin{theorem}\label{Valuation.unique_val_of_ext}
+        \leanok
+        \lean{Valuation.unique_val_of_ext}
+        \uses{ValAlgebra,unique_valuationSubring_of_ext,Valued.valuationSubring,ext,ValAlgEquiv}
                 No documentation.
     \end{theorem}
 
-\begin{theorem}\label{varphi_bij}
-        \lean{varphi_bij}
-        \uses{phi_bij}
+\begin{proof}
+    \leanok
+\end{proof}
+
+\begin{theorem}\label{ValAlgEquiv.algEnd_preserve_val}
+        \leanok
+        \lean{ValAlgEquiv.algEnd_preserve_val}
+        \uses{ValAlgebra,Valuation.unique_val_of_ext,ext,ValAlgebra.val_isEquiv_comap}
                 No documentation.
     \end{theorem}
 
-\begin{theorem}\label{psi_bij}
-        \lean{psi_bij}
-        \uses{ExtDVR.3}
+\begin{proof}
+    \leanok
+\end{proof}
+
+\begin{theorem}\label{ValAlgEquiv.algEquiv_preserve_val}
+        \leanok
+        \lean{ValAlgEquiv.algEquiv_preserve_val}
+        \uses{ValAlgEquiv.algEnd_preserve_val}
                 No documentation.
     \end{theorem}
 
+\begin{proof}
+    \leanok
+\end{proof}
+
+\begin{definition}\label{ValAlgEquiv.fromAlgEquiv}
+        \lean{ValAlgEquiv.fromAlgEquiv}
+        \uses{ValAlgEquiv.algEquiv_preserve_val,DiscreteValuation.fromAlgEquiv,ValAlgEquiv.mk'}
+                No documentation.
+    \end{definition}
+
+\begin{definition}\label{ValAlgEquiv.equivAlgEquiv}
+        \lean{ValAlgEquiv.equivAlgEquiv}
+        \uses{DiscreteValuation.fromAlgEquiv,DiscreteValuation.equivAlgEquiv,ValAlgEquiv}
+                No documentation.
+    \end{definition}
+
+\begin{definition}\label{CompleteValuationRing}
+        \leanok
+        \lean{CompleteValuationRing}
+        \uses{ext}
+                No documentation.
+    \end{definition}
+
+\begin{definition}\label{CompleteValuedField}
+        \leanok
+        \lean{CompleteValuedField}
+        \uses{CompleteValuationRing,ValRingHom.comp}
+                No documentation.
+    \end{definition}
+
+\begin{definition}\label{CompleteDiscreteValuedField}
+        \leanok
+        \lean{CompleteDiscreteValuedField}
+        \uses{CompleteValuedField,ext}
+                No documentation.
+    \end{definition}
+
+\begin{definition}\label{RingHom.liftValuationInteger}
+        \lean{RingHom.liftValuationInteger}
+                No documentation.
+    \end{definition}
+
+\begin{definition}\label{PreserveValuation}
+        \leanok
+        \lean{PreserveValuation}
+        \uses{ValRingHom.id}
+                No documentation.
+    \end{definition}
+
+\begin{definition}\label{ValuationExtension}
+        \leanok
+        \lean{ValuationExtension}
+        \uses{ext,ValRingHom.id}
+                No documentation.
+    \end{definition}
+
+\begin{definition}\label{ValuationExtension'}
+        \lean{ValuationExtension'}
+        \uses{PreserveValuation,ValuationExtension,ext,ValRingHom.id}
+                No documentation.
+    \end{definition}
+
+\begin{theorem}\label{Valuation.isEquiv_of_finiteDimensional_of_valuationExtension}
+        \lean{Valuation.isEquiv_of_finiteDimensional_of_valuationExtension}
+        \uses{Valuation.isEquiv_of_finiteDimensional,ValuationExtension}
+                No documentation.
+    \end{theorem}
+
+\begin{theorem}\label{Valuation.preserveValuation_of_finiteDimensional_algebra_hom}
+        \lean{Valuation.preserveValuation_of_finiteDimensional_algebra_hom}
+        \uses{PreserveValuation}
+                No documentation.
+    \end{theorem}
+
+\begin{definition}\label{AlgHom.liftValuationInteger}
+        \lean{AlgHom.liftValuationInteger}
+                No documentation.
+    \end{definition}
+
+\begin{definition}\label{AlgEquiv.liftValuationInteger}
+        \lean{AlgEquiv.liftValuationInteger}
+        \uses{AlgHom.liftValuationInteger}
+                No documentation.
+    \end{definition}
+
+\begin{definition}\label{AlgHom.liftResidueField}
+        \lean{AlgHom.liftResidueField}
+        \uses{Valued.ResidueField,ValRingHom.id,liftResidueField}
+                No documentation.
+    \end{definition}
+
+\begin{definition}\label{AlgEquiv.liftResidueField}
+        \lean{AlgEquiv.liftResidueField}
+        \uses{ValAlgebra,Valued.ResidueField,ValRingHom.id,ValAlgEquiv,liftResidueField}
+                No documentation.
+    \end{definition}
+
 \begin{theorem}\label{varphi_zero_eq_zero}
         \leanok
         \lean{varphi_zero_eq_zero}
@@ -1017,20 +1236,128 @@
     \end{theorem}
 
 \begin{theorem}\label{psi_zero_eq_zero}
-        \leanok
         \lean{psi_zero_eq_zero}
+        \uses{phi_zero_eq_zero,phi_bij,ValRingHom.id,ValRingHom.comp}
                 No documentation.
     \end{theorem}
 
-\begin{proof}
-    \leanok
-\end{proof}
+\begin{theorem}\label{varphi_bij}
+        \lean{varphi_bij}
+        \uses{phi_bij,varphi_mono,phi_mono,ValRingHom.comp}
+                No documentation.
+    \end{theorem}
+
+\begin{theorem}\label{psi_bij}
+        \lean{psi_bij}
+        \uses{phi_bij,injective,surjective}
+                No documentation.
+    \end{theorem}
 
 \begin{theorem}\label{Varphi_eq_Sum_Inf}
         \lean{Varphi_eq_Sum_Inf}
+        \uses{G_pairwiseDisjoint,G_split,Sum_Trunc_lower_Index_of_G_n,Sum_Trunc_lower_Index_of_diff_G,ValAlgEquiv.refl,ValAlgEquiv}
+                No documentation.
+    \end{theorem}
+
+\begin{definition}\label{ValuationExtension''}
+        \lean{ValuationExtension''}
+        \uses{PreserveValuation,ValuationExtension,ValuationExtension',ext,ValRingHom.id}
+                No documentation.
+    \end{definition}
+
+\begin{definition}\label{Valuation.ramificationIndex}
+        \lean{Valuation.ramificationIndex}
+        \uses{ValRingHom.ramificationIndex,ValuationExtension}
+                No documentation.
+    \end{definition}
+
+\begin{definition}\label{DiscreteValuation.toInt}
+        \lean{DiscreteValuation.toInt}
+                No documentation.
+    \end{definition}
+
+\begin{definition}\label{lowerIndex}
+        \leanok
+        \lean{lowerIndex}
+                No documentation.
+    \end{definition}
+
+\begin{definition}\label{RamificationGroup}
+        \lean{RamificationGroup}
+        \uses{ValuationExtension,lowerIndex,ValRingHom.id,ValRingHom.comp}
+                No documentation.
+    \end{definition}
+
+\begin{theorem}\label{lower_numbering_inf}
+        \lean{lower_numbering_inf}
+                No documentation.
+    \end{theorem}
+
+\begin{theorem}\label{index_subgroup}
+        \lean{index_subgroup}
+        \uses{ValuationExtension,ValRingHom.comp}
+                No documentation.
+    \end{theorem}
+
+\begin{theorem}\label{index_quotient_group}
+        \lean{index_quotient_group}
+                No documentation.
+    \end{theorem}
+
+\begin{definition}\label{ValuationRingTopology.ValuationRing.setoid}
+        \lean{ValuationRingTopology.ValuationRing.setoid}
+        \uses{ValRingHom.id}
+                The preorder of divisibility associated to a valuation ring, i.e. `a ≤ b` if there exist `c`, such that `a * c = b`.
+    \end{definition}
+
+\begin{definition}\label{ValuationRingTopology.ValuationRing.ValueMonoid}
+        \lean{ValuationRingTopology.ValuationRing.ValueMonoid}
+        \uses{ValuationRingTopology.ValuationRing.setoid,ValRingHom.id}
+                No documentation.
+    \end{definition}
+
+\begin{definition}\label{ValuationRingTopology.Valuation.leIdeal}
+        \lean{ValuationRingTopology.Valuation.leIdeal}
+        \uses{ValRingHom.id}
+                No documentation.
+    \end{definition}
+
+\begin{definition}\label{ValuationRingTopology.Valuation.ltIdeal}
+        \lean{ValuationRingTopology.Valuation.ltIdeal}
+        \uses{ValRingHom.id}
+                No documentation.
+    \end{definition}
+
+\begin{definition}\label{ValuationRingTopology.Valuation.maximalIdeal}
+        \lean{ValuationRingTopology.Valuation.maximalIdeal}
+        \uses{ValuationRingTopology.Valuation.ltIdeal,Valued.maximalIdeal,Valued.ResidueField,ValRingHom.id}
+                No documentation.
+    \end{definition}
+
+\begin{theorem}\label{Prop18}
+        \lean{Prop18}
                 No documentation.
     \end{theorem}
 
+\begin{definition}\label{aaa}
+        \leanok
+        \lean{aaa}
+                No documentation.
+    \end{definition}
+
+\begin{definition}\label{LinearEquiv.ofSubalgebraEqTop}
+        \lean{LinearEquiv.ofSubalgebraEqTop}
+        \uses{eq_top}
+                No documentation.
+    \end{definition}
+
+\begin{definition}\label{AlgEquiv.ofTop}
+        \leanok
+        \lean{AlgEquiv.ofTop}
+        \uses{ValAlgEquiv.symm}
+                No documentation.
+    \end{definition}
+
 \begin{theorem}\label{HerbrandFunction.sub_of_sum}
         \leanok
         \lean{HerbrandFunction.sub_of_sum}
@@ -1170,6 +1497,70 @@
                 No documentation.
     \end{theorem}
 
+\begin{theorem}\label{varphi'_pos}
+        \lean{varphi'_pos}
+        \uses{phi'_pos}
+                No documentation.
+    \end{theorem}
+
+\begin{theorem}\label{varphi_mono_int}
+        \lean{varphi_mono_int}
+        \uses{phi_mono_int,varphi_mono,phi_mono}
+                No documentation.
+    \end{theorem}
+
+\begin{theorem}\label{varphi_lt_int_ceil}
+        \lean{varphi_lt_int_ceil}
+                No documentation.
+    \end{theorem}
+
+\begin{theorem}\label{varphi_mono_section}
+        \lean{varphi_mono_section}
+        \uses{varphi'_pos,varphi_mono,phi'_pos,phi_mono}
+                No documentation.
+    \end{theorem}
+
+\begin{theorem}\label{varphi_mono}
+        \lean{varphi_mono}
+        \uses{phi_mono_int,varphi_mono_int,varphi_lt_int_ceil,varphi_mono_section,phi_mono}
+                No documentation.
+    \end{theorem}
+
+\begin{definition}\label{Lift_Galois_ValEquiv}
+        \lean{Lift_Galois_ValEquiv}
+                No documentation.
+    \end{definition}
+
+\begin{definition}\label{Galois_to_Quotient}
+        \lean{Galois_to_Quotient}
+        \uses{ValAlgebra,ValAlgebra.val_isEquiv_comap}
+                No documentation.
+    \end{definition}
+
+\begin{theorem}\label{Varphi_With_i'}
+        \lean{Varphi_With_i'}
+        \uses{Lift_Galois_ValEquiv,Galois_to_Quotient,ValAlgEquiv.mk'}
+                No documentation.
+    \end{theorem}
+
+\begin{theorem}\label{Herbrand_Thm}
+        \lean{Herbrand_Thm}
+        \uses{Lift_Galois_ValEquiv,Galois_to_Quotient,ValAlgEquiv.mk'}
+                No documentation.
+    \end{theorem}
+
+\begin{theorem}\label{varphi_comp_field_ext}
+        \lean{varphi_comp_field_ext}
+        \uses{ext,ValRingHom.comp}
+                No documentation.
+    \end{theorem}
+
+\begin{theorem}\label{psi_comp_field_ext}
+        \lean{psi_comp_field_ext}
+        \uses{ext,ValRingHom.comp}
+                No documentation.
+    \end{theorem}
+
 \begin{theorem}\label{sub_of_sum}
         \leanok
         \lean{sub_of_sum}
@@ -1339,62 +1730,19 @@
                 No documentation.
     \end{theorem}
 
-\begin{theorem}\label{Prop18}
-        \lean{Prop18}
-                No documentation.
-    \end{theorem}
-
-\begin{definition}\label{aaa}
-        \leanok
-        \lean{aaa}
-                No documentation.
-    \end{definition}
-
-\begin{definition}\label{LinearEquiv.ofSubalgebraEqTop}
-        \lean{LinearEquiv.ofSubalgebraEqTop}
-        \uses{eq_top}
-                No documentation.
-    \end{definition}
-
-\begin{definition}\label{AlgEquiv.ofTop}
-        \leanok
-        \lean{AlgEquiv.ofTop}
-        \uses{ValAlgEquiv.symm}
-                No documentation.
-    \end{definition}
-
-\begin{definition}\label{Lift_Galois_ValEquiv}
-        \lean{Lift_Galois_ValEquiv}
-                No documentation.
-    \end{definition}
-
-\begin{definition}\label{Galois_to_Quotient}
-        \lean{Galois_to_Quotient}
-        \uses{ValAlgebra,ValAlgebra.val_isEquiv_comap}
-                No documentation.
-    \end{definition}
-
-\begin{theorem}\label{Varphi_With_i'}
-        \lean{Varphi_With_i'}
-        \uses{Lift_Galois_ValEquiv,Galois_to_Quotient,ValAlgEquiv.mk'}
-                No documentation.
-    \end{theorem}
-
-\begin{theorem}\label{Herbrand_Thm}
-        \lean{Herbrand_Thm}
-        \uses{Lift_Galois_ValEquiv,Galois_to_Quotient,ValAlgEquiv.mk'}
+\begin{theorem}\label{lowerindex_ge_iff_lowerramificationGroup}
+        \lean{lowerindex_ge_iff_lowerramificationGroup}
                 No documentation.
     \end{theorem}
 
-\begin{theorem}\label{varphi_comp_field_ext}
-        \lean{varphi_comp_field_ext}
-        \uses{ext,ValRingHom.comp}
+\begin{theorem}\label{lowerindex_eq_iff_lowerramificationGroup}
+        \lean{lowerindex_eq_iff_lowerramificationGroup}
                 No documentation.
     \end{theorem}
 
-\begin{theorem}\label{psi_comp_field_ext}
-        \lean{psi_comp_field_ext}
-        \uses{ext,ValRingHom.comp}
+\begin{theorem}\label{lowerramificationGroup_has_top}
+        \lean{lowerramificationGroup_has_top}
+        \uses{lowerIndex,ValRingHom.comp,ValAlgEquiv}
                 No documentation.
     \end{theorem}
 
@@ -1494,86 +1842,10 @@
 \begin{definition}\label{Valued.ResidueField}
         \leanok
         \lean{Valued.ResidueField}
-        \uses{Valued.valuationSubring,liftInteger,ValRingHom.id,ValAlgEquiv.mk'}
+        \uses{Valued.valuationSubring,ValRingHom.id,ValAlgEquiv.mk',liftInteger}
                 An abbrevation for `LocalRing.ResidueField 𝒪[K]` of a `Valued` instance, enabling the notation `𝓀[K]`
     \end{definition}
 
-\begin{definition}\label{liftInteger}
-        \leanok
-        \lean{liftInteger}
-        \uses{ValAlgebra,ValRingEquiv,ext}
-                No documentation.
-    \end{definition}
-
-\begin{definition}\label{liftValuationSubring}
-        \leanok
-        \lean{liftValuationSubring}
-        \uses{liftInteger}
-                No documentation.
-    \end{definition}
-
-\begin{definition}\label{liftResidueField}
-        \lean{liftResidueField}
-        \uses{Valued.ResidueField,liftInteger,ValRingEquiv,ValRingHom.id,ValAlgHom,ValAlgEquiv}
-                No documentation.
-    \end{definition}
-
-\begin{definition}\label{ValAlgHom.liftValuationIntegerQuotientleIdeal}
-        \lean{ValAlgHom.liftValuationIntegerQuotientleIdeal}
-        \uses{ValAlgHom,AlgHom.liftValuationInteger}
-                No documentation.
-    \end{definition}
-
-\begin{definition}\label{ValAlgIso.liftValuationIntegerQuotientleIdeal}
-        \lean{ValAlgIso.liftValuationIntegerQuotientleIdeal}
-                No documentation.
-    \end{definition}
-
-\begin{definition}\label{AlgHom.liftResidueField}
-        \lean{AlgHom.liftResidueField}
-        \uses{Valued.ResidueField,liftResidueField,ValRingHom.id}
-                No documentation.
-    \end{definition}
-
-\begin{definition}\label{AlgEquiv.liftResidueField}
-        \lean{AlgEquiv.liftResidueField}
-        \uses{Valued.ResidueField,liftResidueField,ValRingHom.id}
-                No documentation.
-    \end{definition}
-
-\begin{theorem}\label{ValAlgEquiv.coe_liftInteger}
-        \leanok
-        \lean{ValAlgEquiv.coe_liftInteger}
-        \uses{liftInteger}
-                No documentation.
-    \end{theorem}
-
-\begin{proof}
-    \leanok
-\end{proof}
-
-\begin{theorem}\label{ValAlgEquiv.liftInteger_refl}
-        \leanok
-        \lean{ValAlgEquiv.liftInteger_refl}
-        \uses{ValAlgebra,liftInteger,ext,ValAlgEquiv.refl}
-                No documentation.
-    \end{theorem}
-
-\begin{proof}
-    \leanok
-\end{proof}
-
-\begin{theorem}\label{ValAlgEquiv.eq_refl_of_liftInteger_eq_refl}
-        \leanok
-        \lean{ValAlgEquiv.eq_refl_of_liftInteger_eq_refl}
-        \uses{liftInteger,ext,surjective,ValAlgEquiv.refl,ValAlgEquiv}
-                No documentation.
-    \end{theorem}
-
-\begin{proof}
-    \leanok
-\end{proof}
-
 \begin{definition}\label{ValRingEquiv}
         \leanok
         \lean{ValRingEquiv}
@@ -2446,149 +2718,69 @@
     \leanok
 \end{proof}
 
-\begin{definition}\label{ValuationExtension''}
-        \lean{ValuationExtension''}
-        \uses{ext,ValRingHom.id,PreserveValuation,ValuationExtension,ValuationExtension'}
-                No documentation.
-    \end{definition}
-
-\begin{definition}\label{Valuation.ramificationIndex}
-        \lean{Valuation.ramificationIndex}
-        \uses{ValRingHom.ramificationIndex,ValuationExtension}
-                No documentation.
-    \end{definition}
-
-\begin{definition}\label{DiscreteValuation.toInt}
-        \lean{DiscreteValuation.toInt}
-                No documentation.
-    \end{definition}
-
-\begin{definition}\label{lowerIndex}
+\begin{definition}\label{liftInteger}
         \leanok
-        \lean{lowerIndex}
-                No documentation.
-    \end{definition}
-
-\begin{definition}\label{RamificationGroup}
-        \lean{RamificationGroup}
-        \uses{ValRingHom.id,ValRingHom.comp,lowerIndex,ValuationExtension}
-                No documentation.
-    \end{definition}
-
-\begin{theorem}\label{lower_numbering_inf}
-        \lean{lower_numbering_inf}
-                No documentation.
-    \end{theorem}
-
-\begin{theorem}\label{index_subgroup}
-        \lean{index_subgroup}
-        \uses{ValRingHom.comp,ValuationExtension}
-                No documentation.
-    \end{theorem}
-
-\begin{theorem}\label{index_quotient_group}
-        \lean{index_quotient_group}
-                No documentation.
-    \end{theorem}
-
-\begin{definition}\label{ValuationRingTopology.ValuationRing.setoid}
-        \lean{ValuationRingTopology.ValuationRing.setoid}
-        \uses{ValRingHom.id}
-                The preorder of divisibility associated to a valuation ring, i.e. `a ≤ b` if there exist `c`, such that `a * c = b`.
-    \end{definition}
-
-\begin{definition}\label{ValuationRingTopology.ValuationRing.ValueMonoid}
-        \lean{ValuationRingTopology.ValuationRing.ValueMonoid}
-        \uses{ValuationRingTopology.ValuationRing.setoid,ValRingHom.id}
-                No documentation.
-    \end{definition}
-
-\begin{definition}\label{ValuationRingTopology.Valuation.leIdeal}
-        \lean{ValuationRingTopology.Valuation.leIdeal}
-        \uses{ValRingHom.id}
+        \lean{liftInteger}
+        \uses{ValAlgebra,ValRingEquiv,ext}
                 No documentation.
     \end{definition}
 
-\begin{definition}\label{ValuationRingTopology.Valuation.ltIdeal}
-        \lean{ValuationRingTopology.Valuation.ltIdeal}
-        \uses{ValRingHom.id}
+\begin{definition}\label{liftValuationSubring}
+        \leanok
+        \lean{liftValuationSubring}
+        \uses{liftInteger}
                 No documentation.
     \end{definition}
 
-\begin{definition}\label{ValuationRingTopology.Valuation.maximalIdeal}
-        \lean{ValuationRingTopology.Valuation.maximalIdeal}
-        \uses{ValuationRingTopology.Valuation.ltIdeal,Valued.maximalIdeal,Valued.ResidueField,ValRingHom.id}
+\begin{definition}\label{liftResidueField}
+        \lean{liftResidueField}
+        \uses{Valued.ResidueField,ValRingEquiv,ValRingHom.id,ValAlgHom,ValAlgEquiv,liftInteger}
                 No documentation.
     \end{definition}
 
-\begin{definition}\label{RingHom.liftValuationInteger}
-        \lean{RingHom.liftValuationInteger}
+\begin{definition}\label{ValAlgHom.liftValuationIntegerQuotientleIdeal}
+        \lean{ValAlgHom.liftValuationIntegerQuotientleIdeal}
+        \uses{AlgHom.liftValuationInteger,ValAlgHom}
                 No documentation.
     \end{definition}
 
-\begin{definition}\label{PreserveValuation}
-        \leanok
-        \lean{PreserveValuation}
-        \uses{ValRingHom.id}
+\begin{definition}\label{ValAlgIso.liftValuationIntegerQuotientleIdeal}
+        \lean{ValAlgIso.liftValuationIntegerQuotientleIdeal}
                 No documentation.
     \end{definition}
 
-\begin{definition}\label{ValuationExtension}
+\begin{theorem}\label{ValAlgEquiv.coe_liftInteger}
         \leanok
-        \lean{ValuationExtension}
-        \uses{ext,ValRingHom.id}
-                No documentation.
-    \end{definition}
-
-\begin{definition}\label{ValuationExtension'}
-        \lean{ValuationExtension'}
-        \uses{ext,ValRingHom.id,PreserveValuation,ValuationExtension}
-                No documentation.
-    \end{definition}
-
-\begin{theorem}\label{Valuation.isEquiv_of_finiteDimensional_of_valuationExtension}
-        \lean{Valuation.isEquiv_of_finiteDimensional_of_valuationExtension}
-        \uses{Valuation.isEquiv_of_finiteDimensional,ValuationExtension}
-                No documentation.
-    \end{theorem}
-
-\begin{theorem}\label{Valuation.preserveValuation_of_finiteDimensional_algebra_hom}
-        \lean{Valuation.preserveValuation_of_finiteDimensional_algebra_hom}
-        \uses{PreserveValuation}
+        \lean{ValAlgEquiv.coe_liftInteger}
+        \uses{liftInteger}
                 No documentation.
     \end{theorem}
 
-\begin{definition}\label{AlgHom.liftValuationInteger}
-        \lean{AlgHom.liftValuationInteger}
-                No documentation.
-    \end{definition}
-
-\begin{definition}\label{AlgEquiv.liftValuationInteger}
-        \lean{AlgEquiv.liftValuationInteger}
-        \uses{AlgHom.liftValuationInteger}
-                No documentation.
-    \end{definition}
+\begin{proof}
+    \leanok
+\end{proof}
 
-\begin{definition}\label{CompleteValuationRing}
+\begin{theorem}\label{ValAlgEquiv.liftInteger_refl}
         \leanok
-        \lean{CompleteValuationRing}
-        \uses{ext}
+        \lean{ValAlgEquiv.liftInteger_refl}
+        \uses{ValAlgebra,ext,ValAlgEquiv.refl,liftInteger}
                 No documentation.
-    \end{definition}
+    \end{theorem}
 
-\begin{definition}\label{CompleteValuedField}
-        \leanok
-        \lean{CompleteValuedField}
-        \uses{ValRingHom.comp,CompleteValuationRing}
-                No documentation.
-    \end{definition}
+\begin{proof}
+    \leanok
+\end{proof}
 
-\begin{definition}\label{CompleteDiscreteValuedField}
+\begin{theorem}\label{ValAlgEquiv.eq_refl_of_liftInteger_eq_refl}
         \leanok
-        \lean{CompleteDiscreteValuedField}
-        \uses{ext,CompleteValuedField}
+        \lean{ValAlgEquiv.eq_refl_of_liftInteger_eq_refl}
+        \uses{ext,surjective,ValAlgEquiv.refl,ValAlgEquiv,liftInteger}
                 No documentation.
-    \end{definition}
+    \end{theorem}
+
+\begin{proof}
+    \leanok
+\end{proof}
 
 \begin{theorem}\label{Int.eq_neg_one_of_dvd_neg_one}
         \leanok
@@ -2798,92 +2990,6 @@
                 No documentation.
     \end{theorem}
 
-\begin{theorem}\label{Polynomial.hasseDeriv_coeff_zero}
-        \leanok
-        \lean{Polynomial.hasseDeriv_coeff_zero}
-                No documentation.
-    \end{theorem}
-
-\begin{proof}
-    \leanok
-\end{proof}
-
-\begin{theorem}\label{Polynomial.hasseDeriv_coeff_one}
-        \leanok
-        \lean{Polynomial.hasseDeriv_coeff_one}
-                No documentation.
-    \end{theorem}
-
-\begin{proof}
-    \leanok
-\end{proof}
-
-\begin{theorem}\label{Polynomial.X_sq_dvd_hassDeriv_sub_coeff_sub_derivative_coeff}
-        \leanok
-        \lean{Polynomial.X_sq_dvd_hassDeriv_sub_coeff_sub_derivative_coeff}
-        \uses{Polynomial.hasseDeriv_coeff_zero,Polynomial.hasseDeriv_coeff_one}
-                No documentation.
-    \end{theorem}
-
-\begin{proof}
-    \leanok
-\end{proof}
-
-\begin{theorem}\label{Polynomial.taylor_order_one}
-        \leanok
-        \lean{Polynomial.taylor_order_one}
-        \uses{ValRingHom.comp,Polynomial.X_sq_dvd_hassDeriv_sub_coeff_sub_derivative_coeff}
-                No documentation.
-    \end{theorem}
-
-\begin{proof}
-    \leanok
-\end{proof}
-
-\begin{theorem}\label{Polynomial.taylor_order_one_apply}
-        \leanok
-        \lean{Polynomial.taylor_order_one_apply}
-        \uses{ValRingHom.comp,ValAlgEquiv.one_apply,Polynomial.taylor_order_one}
-                No documentation.
-    \end{theorem}
-
-\begin{proof}
-    \leanok
-\end{proof}
-
-\begin{theorem}\label{Polynomial.taylor_order_one_apply₂}
-        \leanok
-        \lean{Polynomial.taylor_order_one_apply₂}
-        \uses{ValAlgEquiv.one_apply,Polynomial.taylor_order_one,Polynomial.taylor_order_one_apply}
-                No documentation.
-    \end{theorem}
-
-\begin{proof}
-    \leanok
-\end{proof}
-
-\begin{theorem}\label{Polynomial.taylor_order_one_apply_aeval}
-        \leanok
-        \lean{Polynomial.taylor_order_one_apply_aeval}
-        \uses{ValAlgEquiv.one_apply,Polynomial.taylor_order_one,Polynomial.taylor_order_one_apply,Polynomial.taylor_order_one_apply₂}
-                No documentation.
-    \end{theorem}
-
-\begin{proof}
-    \leanok
-\end{proof}
-
-\begin{theorem}\label{Polynomial.taylor_order_zero_apply_aeval}
-        \leanok
-        \lean{Polynomial.taylor_order_zero_apply_aeval}
-        \uses{ValAlgEquiv.one_apply,Polynomial.taylor_order_one,Polynomial.taylor_order_one_apply,Polynomial.taylor_order_one_apply_aeval}
-                No documentation.
-    \end{theorem}
-
-\begin{proof}
-    \leanok
-\end{proof}
-
 \begin{theorem}\label{ExtDVR.exists_lift_residue_primitive}
         \leanok
         \lean{ExtDVR.exists_lift_residue_primitive}
@@ -2908,13 +3014,13 @@
 
 \begin{lemma}\label{ExtDVR.adjoin_lift_residue_primitive_and_irreducible_sup_maximalIdeal_eq_top}
         \lean{ExtDVR.adjoin_lift_residue_primitive_and_irreducible_sup_maximalIdeal_eq_top}
-        \uses{eq_top,Valued.maximalIdeal,maximalIdeal_eq,Valued.ResidueField,surjective,ValRingHom.id,ValRingHom.comp,LocalRing.algebraMap_residue_compat}
+        \uses{eq_top,LocalRing.algebraMap_residue_compat,Valued.maximalIdeal,maximalIdeal_eq,Valued.ResidueField,surjective,ValRingHom.id,ValRingHom.comp}
                 Auxiliary lemma: `A[x, ϖ] ⊔ m_B = ⊤`. Can be strenthened to `A[x] ⊔ m_B = B`
     \end{lemma}
 
 \begin{lemma}\label{ExtDVR.adjoin_lift_residue_primitive_and_irreducible_sup_maximalIdeal_pow_eq_top}
         \lean{ExtDVR.adjoin_lift_residue_primitive_and_irreducible_sup_maximalIdeal_pow_eq_top}
-        \uses{eq_top,Valued.maximalIdeal,maximalIdeal_eq,ValRingHom.id,ExtDVR.adjoin_lift_residue_primitive_and_irreducible_sup_maximalIdeal_eq_top,Algebra.pow_mem_adjoin_singleton,DiscreteValuationRing.maximalIdeal_pow_eq_span_irreducible_pow}
+        \uses{eq_top,DiscreteValuationRing.maximalIdeal_pow_eq_span_irreducible_pow,Valued.maximalIdeal,maximalIdeal_eq,ValRingHom.id,ExtDVR.adjoin_lift_residue_primitive_and_irreducible_sup_maximalIdeal_eq_top,Algebra.pow_mem_adjoin_singleton}
                 Auxiliary lemma: `A[x, ϖ] ⊔ m_B ^ i = ⊤` for any `i : ℕ`
     \end{lemma}
 
@@ -2944,7 +3050,7 @@
 \begin{theorem}\label{ExtDVR.residue_primitive_of_add_uniformizer}
         \leanok
         \lean{ExtDVR.residue_primitive_of_add_uniformizer}
-        \uses{Valued.ResidueField,ValRingHom.id,LocalRing.residue_eq_add_irreducible}
+        \uses{LocalRing.residue_eq_add_irreducible,Valued.ResidueField,ValRingHom.id}
                 No documentation.
     \end{theorem}
 
@@ -2955,7 +3061,7 @@
 \begin{theorem}\label{ExtDVR.not_unit_aeval_lift_residue_primitive}
         \leanok
         \lean{ExtDVR.not_unit_aeval_lift_residue_primitive}
-        \uses{ValRingHom.id,ValRingHom.comp,LocalRing.algebraMap_residue_compat,LocalRing.is_unit_iff_residue_ne_zero}
+        \uses{LocalRing.algebraMap_residue_compat,LocalRing.is_unit_iff_residue_ne_zero,ValRingHom.id,ValRingHom.comp}
                 No documentation.
     \end{theorem}
 
@@ -2966,7 +3072,7 @@
 \begin{theorem}\label{ExtDVR.irreducible_aeval_lift_redisue_primitive_add_irreducible_of_reducible_aeval_lift_residue_primitve}
         \leanok
         \lean{ExtDVR.irreducible_aeval_lift_redisue_primitive_add_irreducible_of_reducible_aeval_lift_residue_primitve}
-        \uses{ValRingHom.id,ValRingHom.comp,ValAlgEquiv.one_apply,Polynomial.taylor_order_one,Polynomial.taylor_order_one_apply,Polynomial.taylor_order_one_apply₂,ExtDVR.not_unit_aeval_lift_residue_primitive,LocalRing.algebraMap_residue_compat,LocalRing.is_unit_iff_residue_ne_zero,DiscreteValuationRing.mul_irreducible_square_of_not_unit_of_not_irreducible,DiscreteValuationRing.irreducible_of_irreducible_add_addVal_ge_two}
+        \uses{DiscreteValuationRing.mul_irreducible_square_of_not_unit_of_not_irreducible,DiscreteValuationRing.irreducible_of_irreducible_add_addVal_ge_two,LocalRing.algebraMap_residue_compat,LocalRing.is_unit_iff_residue_ne_zero,ValRingHom.id,ValRingHom.comp,ValAlgEquiv.one_apply,ExtDVR.not_unit_aeval_lift_residue_primitive,Polynomial.taylor_order_one,Polynomial.taylor_order_one_apply,Polynomial.taylor_order_one_apply₂}
                 This is the first part of lemma 4:
 If `f x` has valuation ≥ 2, then `f (x + ϖ)` is a uniformizer.
     \end{theorem}
@@ -2983,170 +3089,15 @@
     \end{theorem}
 
 \begin{theorem}\label{ExtDVR.exists_primitive}
-        \lean{ExtDVR.exists_primitive}
-        \uses{eq_top,ValRingHom.id,ExtDVR.exists_lift_residue_primitive,ExtDVR.exists_lift_polynomial_of_residue,ExtDVR.residue_primitive_of_add_uniformizer,ExtDVR.irreducible_aeval_lift_redisue_primitive_add_irreducible_of_reducible_aeval_lift_residue_primitve,ExtDVR.adjoin_lift_primitive_eq_top_of_irreducible_aeval_lift_residue_primitive}
-                For a finite extension of DVR `A ↪ B` with seperable residue field extension,
-there exists `x : B` s.t. `B = A[x]`
-    \end{theorem}
-
-\begin{theorem}\label{Algebra.pow_mem_adjoin_singleton}
-        \leanok
-        \lean{Algebra.pow_mem_adjoin_singleton}
-                No documentation.
-    \end{theorem}
-
-\begin{proof}
-    \leanok
-\end{proof}
-
-\begin{definition}\label{Ideal.quotientAlgebra'}
-        \leanok
-        \lean{Ideal.quotientAlgebra'}
-                No documentation.
-    \end{definition}
-
-\begin{theorem}\label{PowerBasis.algEquiv_ext}
-        \leanok
-        \lean{PowerBasis.algEquiv_ext}
-        \uses{ext}
-                No documentation.
-    \end{theorem}
-
-\begin{proof}
-    \leanok
-\end{proof}
-
-\begin{definition}\label{AlgEquiv.restrictScalarsHom}
-        \leanok
-        \lean{AlgEquiv.restrictScalarsHom}
-        \uses{ext}
-                No documentation.
-    \end{definition}
-
-\begin{theorem}\label{LocalRing.algebraMap_residue_compat}
-        \leanok
-        \lean{LocalRing.algebraMap_residue_compat}
-        \uses{Valued.ResidueField,ValRingHom.id,ValRingHom.comp}
-                No documentation.
-    \end{theorem}
-
-\begin{proof}
-    \leanok
-\end{proof}
-
-\begin{theorem}\label{LocalRing.residue_irreducible_eq_zero}
-        \leanok
-        \lean{LocalRing.residue_irreducible_eq_zero}
-        \uses{Valued.maximalIdeal,ValRingHom.id}
-                No documentation.
-    \end{theorem}
-
-\begin{proof}
-    \leanok
-\end{proof}
-
-\begin{theorem}\label{LocalRing.is_unit_iff_residue_ne_zero}
-        \leanok
-        \lean{LocalRing.is_unit_iff_residue_ne_zero}
-        \uses{ValRingHom.id}
-                No documentation.
-    \end{theorem}
-
-\begin{proof}
-    \leanok
-\end{proof}
-
-\begin{theorem}\label{LocalRing.residue_eq_add_irreducible}
-        \leanok
-        \lean{LocalRing.residue_eq_add_irreducible}
-        \uses{ValRingHom.id,LocalRing.residue_irreducible_eq_zero}
-                No documentation.
-    \end{theorem}
-
-\begin{proof}
-    \leanok
-\end{proof}
-
-\begin{theorem}\label{LocalRing.is_unit_of_unit_add_nonunit}
-        \leanok
-        \lean{LocalRing.is_unit_of_unit_add_nonunit}
-                No documentation.
-    \end{theorem}
-
-\begin{proof}
-    \leanok
-\end{proof}
-
-\begin{theorem}\label{LocalRing.maximalIdeal_eq_jacobson_of_bot}
-        \lean{LocalRing.maximalIdeal_eq_jacobson_of_bot}
-        \uses{Valued.maximalIdeal,maximalIdeal_eq,ValAlgEquiv.symm}
-                No documentation.
-    \end{theorem}
-
-\begin{theorem}\label{DiscreteValuationRing.unit_mul_irreducible_of_irreducible}
-        \leanok
-        \lean{DiscreteValuationRing.unit_mul_irreducible_of_irreducible}
-                No documentation.
-    \end{theorem}
-
-\begin{proof}
-    \leanok
-\end{proof}
-
-\begin{theorem}\label{DiscreteValuationRing.mul_irreducible_of_not_unit}
-        \leanok
-        \lean{DiscreteValuationRing.mul_irreducible_of_not_unit}
-        \uses{Valued.maximalIdeal,ValAlgEquiv.symm}
-                No documentation.
-    \end{theorem}
-
-\begin{proof}
-    \leanok
-\end{proof}
-
-\begin{theorem}\label{DiscreteValuationRing.mul_irreducible_square_of_not_unit_of_not_irreducible}
-        \leanok
-        \lean{DiscreteValuationRing.mul_irreducible_square_of_not_unit_of_not_irreducible}
-        \uses{ValRingHom.id,DiscreteValuationRing.mul_irreducible_of_not_unit}
-                No documentation.
-    \end{theorem}
-
-\begin{proof}
-    \leanok
-\end{proof}
-
-\begin{theorem}\label{DiscreteValuationRing.irreducible_of_irreducible_add_addVal_ge_two}
-        \leanok
-        \lean{DiscreteValuationRing.irreducible_of_irreducible_add_addVal_ge_two}
-        \uses{LocalRing.is_unit_of_unit_add_nonunit,DiscreteValuationRing.unit_mul_irreducible_of_irreducible}
-                No documentation.
-    \end{theorem}
-
-\begin{proof}
-    \leanok
-\end{proof}
-
-\begin{theorem}\label{DiscreteValuationRing.maximalIdeal_pow_eq_span_irreducible_pow}
-        \lean{DiscreteValuationRing.maximalIdeal_pow_eq_span_irreducible_pow}
-        \uses{Valued.maximalIdeal,maximalIdeal_eq}
-                No documentation.
-    \end{theorem}
-
-\begin{theorem}\label{unique_of_valuation_extension}
-        \lean{unique_of_valuation_extension}
-        \uses{ValAlgebra,ext}
-                No documentation.
-    \end{theorem}
-
-\begin{definition}\label{toValAlgEquiv}
-        \lean{toValAlgEquiv}
-        \uses{ValAlgEquiv}
-                No documentation.
-    \end{definition}
+        \lean{ExtDVR.exists_primitive}
+        \uses{eq_top,ValRingHom.id,ExtDVR.exists_lift_residue_primitive,ExtDVR.exists_lift_polynomial_of_residue,ExtDVR.residue_primitive_of_add_uniformizer,ExtDVR.irreducible_aeval_lift_redisue_primitive_add_irreducible_of_reducible_aeval_lift_residue_primitve,ExtDVR.adjoin_lift_primitive_eq_top_of_irreducible_aeval_lift_residue_primitive}
+                For a finite extension of DVR `A ↪ B` with seperable residue field extension,
+there exists `x : B` s.t. `B = A[x]`
+    \end{theorem}
 
-\begin{theorem}\label{integer_valuation_eq}
+\begin{theorem}\label{Polynomial.hasseDeriv_coeff_zero}
         \leanok
-        \lean{integer_valuation_eq}
+        \lean{Polynomial.hasseDeriv_coeff_zero}
                 No documentation.
     \end{theorem}
 
@@ -3154,14 +3105,9 @@
     \leanok
 \end{proof}
 
-\begin{theorem}\label{integerAlgebraMap.monotone}
-        \lean{integerAlgebraMap.monotone}
-                No documentation.
-    \end{theorem}
-
-\begin{theorem}\label{integer_val_coe}
+\begin{theorem}\label{Polynomial.hasseDeriv_coeff_one}
         \leanok
-        \lean{integer_val_coe}
+        \lean{Polynomial.hasseDeriv_coeff_one}
                 No documentation.
     \end{theorem}
 
@@ -3169,10 +3115,10 @@
     \leanok
 \end{proof}
 
-\begin{theorem}\label{valuationSubring_val_coe}
+\begin{theorem}\label{Polynomial.X_sq_dvd_hassDeriv_sub_coeff_sub_derivative_coeff}
         \leanok
-        \lean{valuationSubring_val_coe}
-        \uses{Valued.valuationSubring}
+        \lean{Polynomial.X_sq_dvd_hassDeriv_sub_coeff_sub_derivative_coeff}
+        \uses{Polynomial.hasseDeriv_coeff_zero,Polynomial.hasseDeriv_coeff_one}
                 No documentation.
     \end{theorem}
 
@@ -3180,9 +3126,10 @@
     \leanok
 \end{proof}
 
-\begin{theorem}\label{integer_val_le_one}
+\begin{theorem}\label{Polynomial.taylor_order_one}
         \leanok
-        \lean{integer_val_le_one}
+        \lean{Polynomial.taylor_order_one}
+        \uses{ValRingHom.comp,Polynomial.X_sq_dvd_hassDeriv_sub_coeff_sub_derivative_coeff}
                 No documentation.
     \end{theorem}
 
@@ -3190,16 +3137,10 @@
     \leanok
 \end{proof}
 
-\begin{theorem}\label{maximalIdeal_eq}
-        \lean{maximalIdeal_eq}
-        \uses{Valued.maximalIdeal,ValRingHom.id}
-                No documentation.
-    \end{theorem}
-
-\begin{theorem}\label{ringHomClass_eq_iff_valuationSubring}
+\begin{theorem}\label{Polynomial.taylor_order_one_apply}
         \leanok
-        \lean{ringHomClass_eq_iff_valuationSubring}
-        \uses{Valued.valuationSubring,ext}
+        \lean{Polynomial.taylor_order_one_apply}
+        \uses{ValRingHom.comp,ValAlgEquiv.one_apply,Polynomial.taylor_order_one}
                 No documentation.
     \end{theorem}
 
@@ -3207,17 +3148,10 @@
     \leanok
 \end{proof}
 
-\begin{definition}\label{Valued.RingHom.restrictInteger}
-        \leanok
-        \lean{Valued.RingHom.restrictInteger}
-        \uses{IsValExtension.val_map_le_one_iff,ValRingHom.id}
-                No documentation.
-    \end{definition}
-
-\begin{theorem}\label{Valued.RingHom.restrictInteger_apply}
+\begin{theorem}\label{Polynomial.taylor_order_one_apply₂}
         \leanok
-        \lean{Valued.RingHom.restrictInteger_apply}
-        \uses{Valued.valuationSubring,Valued.RingHom.restrictInteger,IsValExtension}
+        \lean{Polynomial.taylor_order_one_apply₂}
+        \uses{ValAlgEquiv.one_apply,Polynomial.taylor_order_one,Polynomial.taylor_order_one_apply}
                 No documentation.
     \end{theorem}
 
@@ -3225,17 +3159,21 @@
     \leanok
 \end{proof}
 
-\begin{definition}\label{Valued.RingHom.restrictValuationSubring}
+\begin{theorem}\label{Polynomial.taylor_order_one_apply_aeval}
         \leanok
-        \lean{Valued.RingHom.restrictValuationSubring}
-        \uses{Valued.RingHom.restrictInteger}
+        \lean{Polynomial.taylor_order_one_apply_aeval}
+        \uses{ValAlgEquiv.one_apply,Polynomial.taylor_order_one,Polynomial.taylor_order_one_apply,Polynomial.taylor_order_one_apply₂}
                 No documentation.
-    \end{definition}
+    \end{theorem}
 
-\begin{theorem}\label{Valued.RingHom.restrictValuationSubring_apply}
+\begin{proof}
+    \leanok
+\end{proof}
+
+\begin{theorem}\label{Polynomial.taylor_order_zero_apply_aeval}
         \leanok
-        \lean{Valued.RingHom.restrictValuationSubring_apply}
-        \uses{Valued.RingHom.restrictValuationSubring}
+        \lean{Polynomial.taylor_order_zero_apply_aeval}
+        \uses{ValAlgEquiv.one_apply,Polynomial.taylor_order_one,Polynomial.taylor_order_one_apply,Polynomial.taylor_order_one_apply_aeval}
                 No documentation.
     \end{theorem}
 
@@ -3243,17 +3181,19 @@
     \leanok
 \end{proof}
 
-\begin{definition}\label{Valued.AlgHom.restrictValuationSubring}
+\begin{theorem}\label{Algebra.pow_mem_adjoin_singleton}
         \leanok
-        \lean{Valued.AlgHom.restrictValuationSubring}
-        \uses{Valued.valuationSubring,ext,ValRingHom.id,Valued.RingHom.restrictValuationSubring,Valued.RingHom.restrictValuationSubring_apply,IsValExtension,IsValExtension.coe_algebraMap_valuationSubring}
+        \lean{Algebra.pow_mem_adjoin_singleton}
                 No documentation.
-    \end{definition}
+    \end{theorem}
 
-\begin{theorem}\label{Valued.AlgHom.restrictValuationSubring_apply}
+\begin{proof}
+    \leanok
+\end{proof}
+
+\begin{theorem}\label{integer_valuation_eq}
         \leanok
-        \lean{Valued.AlgHom.restrictValuationSubring_apply}
-        \uses{Valued.decompositionGroup,Valued.valuationSubring,ValRingHom.comp,Valued.AlgHom.restrictValuationSubring,IsValExtension}
+        \lean{integer_valuation_eq}
                 No documentation.
     \end{theorem}
 
@@ -3261,17 +3201,14 @@
     \leanok
 \end{proof}
 
-\begin{definition}\label{Valued.DecompositionGroup.restrictValuationSubring}
-        \leanok
-        \lean{Valued.DecompositionGroup.restrictValuationSubring}
-        \uses{Valued.decompositionGroup,ext,ValRingHom.comp,ValAlgEquiv.symm,ValAlgEquiv.apply_symm_apply,ValAlgEquiv.symm_apply_apply,Valued.AlgHom.restrictValuationSubring}
+\begin{theorem}\label{integerAlgebraMap.monotone}
+        \lean{integerAlgebraMap.monotone}
                 No documentation.
-    \end{definition}
+    \end{theorem}
 
-\begin{theorem}\label{Valued.DecompositionGroup.restrictValuationSubring_apply}
+\begin{theorem}\label{integer_val_coe}
         \leanok
-        \lean{Valued.DecompositionGroup.restrictValuationSubring_apply}
-        \uses{Valued.decompositionGroup,ValRingHom.comp,Valued.DecompositionGroup.restrictValuationSubring}
+        \lean{integer_val_coe}
                 No documentation.
     \end{theorem}
 
@@ -3279,10 +3216,10 @@
     \leanok
 \end{proof}
 
-\begin{theorem}\label{Valued.elem_decompositionGroup_eq_iff_ValuationSubring}
+\begin{theorem}\label{valuationSubring_val_coe}
         \leanok
-        \lean{Valued.elem_decompositionGroup_eq_iff_ValuationSubring}
-        \uses{Valued.decompositionGroup,Valued.valuationSubring,ext,ValRingHom.comp,ringHomClass_eq_iff_valuationSubring,Valued.DecompositionGroup.restrictValuationSubring,Valued.DecompositionGroup.restrictValuationSubring_apply,IsValExtension}
+        \lean{valuationSubring_val_coe}
+        \uses{Valued.valuationSubring}
                 No documentation.
     \end{theorem}
 
@@ -3290,21 +3227,19 @@
     \leanok
 \end{proof}
 
-\begin{definition}\label{Valued.AlgEquiv.restrictValuationSubring}
-        \lean{Valued.AlgEquiv.restrictValuationSubring}
-        \uses{eq_top,Valued.decompositionGroup,Valued.decompositionGroup_eq_top,ValRingHom.comp,Valued.DecompositionGroup.restrictValuationSubring}
-                No documentation.
-    \end{definition}
-
-\begin{theorem}\label{Valued.AlgEquiv.restrictValuationSubring_apply}
-        \lean{Valued.AlgEquiv.restrictValuationSubring_apply}
-        \uses{Valued.AlgEquiv.restrictValuationSubring}
+\begin{theorem}\label{integer_val_le_one}
+        \leanok
+        \lean{integer_val_le_one}
                 No documentation.
     \end{theorem}
 
-\begin{theorem}\label{Valued.AlgEquiv.eq_iff_ValuationSubring}
-        \lean{Valued.AlgEquiv.eq_iff_ValuationSubring}
-        \uses{Valued.decompositionGroup,ext,ValRingHom.comp,Valued.elem_decompositionGroup_eq_iff_ValuationSubring,Valued.AlgEquiv.restrictValuationSubring}
+\begin{proof}
+    \leanok
+\end{proof}
+
+\begin{theorem}\label{maximalIdeal_eq}
+        \lean{maximalIdeal_eq}
+        \uses{Valued.maximalIdeal,ValRingHom.id}
                 No documentation.
     \end{theorem}
 
@@ -3467,6 +3402,129 @@
                 No documentation.
     \end{definition}
 
+\begin{theorem}\label{ringHomClass_eq_iff_valuationSubring}
+        \leanok
+        \lean{ringHomClass_eq_iff_valuationSubring}
+        \uses{Valued.valuationSubring,ext}
+                No documentation.
+    \end{theorem}
+
+\begin{proof}
+    \leanok
+\end{proof}
+
+\begin{definition}\label{Valued.RingHom.restrictInteger}
+        \leanok
+        \lean{Valued.RingHom.restrictInteger}
+        \uses{IsValExtension.val_map_le_one_iff,ValRingHom.id}
+                No documentation.
+    \end{definition}
+
+\begin{theorem}\label{Valued.RingHom.restrictInteger_apply}
+        \leanok
+        \lean{Valued.RingHom.restrictInteger_apply}
+        \uses{Valued.valuationSubring,Valued.RingHom.restrictInteger,IsValExtension}
+                No documentation.
+    \end{theorem}
+
+\begin{proof}
+    \leanok
+\end{proof}
+
+\begin{definition}\label{Valued.RingHom.restrictValuationSubring}
+        \leanok
+        \lean{Valued.RingHom.restrictValuationSubring}
+        \uses{Valued.RingHom.restrictInteger}
+                No documentation.
+    \end{definition}
+
+\begin{theorem}\label{Valued.RingHom.restrictValuationSubring_apply}
+        \leanok
+        \lean{Valued.RingHom.restrictValuationSubring_apply}
+        \uses{Valued.RingHom.restrictValuationSubring}
+                No documentation.
+    \end{theorem}
+
+\begin{proof}
+    \leanok
+\end{proof}
+
+\begin{definition}\label{Valued.AlgHom.restrictValuationSubring}
+        \leanok
+        \lean{Valued.AlgHom.restrictValuationSubring}
+        \uses{Valued.valuationSubring,ext,ValRingHom.id,Valued.RingHom.restrictValuationSubring,Valued.RingHom.restrictValuationSubring_apply,IsValExtension,IsValExtension.coe_algebraMap_valuationSubring}
+                No documentation.
+    \end{definition}
+
+\begin{theorem}\label{Valued.AlgHom.restrictValuationSubring_apply}
+        \leanok
+        \lean{Valued.AlgHom.restrictValuationSubring_apply}
+        \uses{Valued.decompositionGroup,Valued.valuationSubring,ValRingHom.comp,Valued.AlgHom.restrictValuationSubring,IsValExtension}
+                No documentation.
+    \end{theorem}
+
+\begin{proof}
+    \leanok
+\end{proof}
+
+\begin{definition}\label{Valued.DecompositionGroup.restrictValuationSubring}
+        \leanok
+        \lean{Valued.DecompositionGroup.restrictValuationSubring}
+        \uses{Valued.decompositionGroup,ext,ValRingHom.comp,ValAlgEquiv.symm,ValAlgEquiv.apply_symm_apply,ValAlgEquiv.symm_apply_apply,Valued.AlgHom.restrictValuationSubring}
+                No documentation.
+    \end{definition}
+
+\begin{theorem}\label{Valued.DecompositionGroup.restrictValuationSubring_apply}
+        \leanok
+        \lean{Valued.DecompositionGroup.restrictValuationSubring_apply}
+        \uses{Valued.decompositionGroup,ValRingHom.comp,Valued.DecompositionGroup.restrictValuationSubring}
+                No documentation.
+    \end{theorem}
+
+\begin{proof}
+    \leanok
+\end{proof}
+
+\begin{theorem}\label{Valued.elem_decompositionGroup_eq_iff_ValuationSubring}
+        \leanok
+        \lean{Valued.elem_decompositionGroup_eq_iff_ValuationSubring}
+        \uses{Valued.decompositionGroup,Valued.valuationSubring,ext,ValRingHom.comp,ringHomClass_eq_iff_valuationSubring,Valued.DecompositionGroup.restrictValuationSubring,Valued.DecompositionGroup.restrictValuationSubring_apply,IsValExtension}
+                No documentation.
+    \end{theorem}
+
+\begin{proof}
+    \leanok
+\end{proof}
+
+\begin{definition}\label{Valued.AlgEquiv.restrictValuationSubring}
+        \lean{Valued.AlgEquiv.restrictValuationSubring}
+        \uses{Valued.decompositionGroup,Valued.decompositionGroup_eq_top,eq_top,ValRingHom.comp,Valued.DecompositionGroup.restrictValuationSubring}
+                No documentation.
+    \end{definition}
+
+\begin{theorem}\label{Valued.AlgEquiv.restrictValuationSubring_apply}
+        \lean{Valued.AlgEquiv.restrictValuationSubring_apply}
+        \uses{Valued.AlgEquiv.restrictValuationSubring}
+                No documentation.
+    \end{theorem}
+
+\begin{theorem}\label{Valued.AlgEquiv.eq_iff_ValuationSubring}
+        \lean{Valued.AlgEquiv.eq_iff_ValuationSubring}
+        \uses{Valued.decompositionGroup,ext,ValRingHom.comp,Valued.elem_decompositionGroup_eq_iff_ValuationSubring,Valued.AlgEquiv.restrictValuationSubring}
+                No documentation.
+    \end{theorem}
+
+\begin{theorem}\label{nontrivial_of_valExtension}
+        \leanok
+        \lean{nontrivial_of_valExtension}
+        \uses{ValAlgEquiv.symm,Valuation.Nontrivial,Valuation.nontrivial_def,IsValExtension.val_map_eq_iff,IsValExtension.val_map_eq_one_iff,IsValExtension}
+                No documentation.
+    \end{theorem}
+
+\begin{proof}
+    \leanok
+\end{proof}
+
 \begin{theorem}\label{IsValExtension.val_map_le_iff}
         \leanok
         \lean{IsValExtension.val_map_le_iff}
@@ -3572,9 +3630,3 @@
                 No documentation.
     \end{theorem}
 
-\begin{theorem}\label{nontrivial_of_valExtension}
-        \lean{nontrivial_of_valExtension}
-        \uses{ValAlgEquiv.symm,Valuation.Nontrivial,Valuation.nontrivial_def,IsValExtension.val_map_eq_iff,IsValExtension.val_map_eq_one_iff,IsValExtension}
-                No documentation.
-    \end{theorem}
-
diff --git a/blueprint/src/web.paux b/blueprint/src/web.paux
index 8a1aa39..4556554 100644
Binary files a/blueprint/src/web.paux and b/blueprint/src/web.paux differ