AdicCompletionInverseLimit.lean

def adicCompletionUnitsEquiv
    {R : Type*} [CommRing R] (I : Ideal R) [IsAdicComplete I R] :
    Rˣ ≃* (AdicCompletion I R)ˣ

theorem adicCompletionUnitsEquiv_apply
    {R : Type*} [CommRing R] (I : Ideal R) [IsAdicComplete I R] (u : Rˣ) :
    (adicCompletionUnitsEquiv I u :
      AdicCompletion I R) =
      adicCompletionAlgEquiv I (u : R)

theorem adicCompletion_units_coordinates_injective
    {R : Type*} [CommRing R] (I : Ideal R) [IsAdicComplete I R]
    {u v : Rˣ}
    (h : ∀ n : ℕ,
      unitReduction (I ^ n) u = unitReduction (I ^ n) v) :
    u = v

theorem adicCompletion_units_coordinates_surjective
    {R : Type*} [CommRing R] (I : Ideal R) [IsAdicComplete I R]
    (z : (AdicCompletion I R)ˣ) :
    ∃ u : Rˣ,
      adicCompletionUnitsEquiv I u = z ∧
        ∀ n : ℕ,
          unitReduction (I ^ n) u =
            Units.map (AdicCompletion.evalₐ I n).toMonoidHom z

def unitsModIdealEquivQuotientUnits
    {R : Type*} [CommRing R] (I : Ideal R)
    [IsLocalHom (Ideal.Quotient.mk I)] :
    Rˣ ⧸ (unitReduction I).ker ≃* (R ⧸ I)ˣ

theorem unitsModIdealEquivQuotientUnits_mk
    {R : Type*} [CommRing R] (I : Ideal R)
    [IsLocalHom (Ideal.Quotient.mk I)] (u : Rˣ) :
    unitsModIdealEquivQuotientUnits I (QuotientGroup.mk u) =
      unitReduction I u

theorem isLocalHom_quotient_maximalIdeal_pow
    {R : Type*} [CommRing R] [IsLocalRing R]
    {n : ℕ} (hn : 1 ≤ n) :
    IsLocalHom (Ideal.Quotient.mk ((IsLocalRing.maximalIdeal R) ^ n))

def unitsModMaximalIdealPowEquiv
    {R : Type*} [CommRing R] [IsLocalRing R]
    {n : ℕ} (hn : 1 ≤ n) :
    Rˣ ⧸ (unitReduction ((IsLocalRing.maximalIdeal R) ^ n)).ker ≃*
      (R ⧸ (IsLocalRing.maximalIdeal R) ^ n)ˣ

theorem unitsModMaximalIdealPowEquiv_mk
    {R : Type*} [CommRing R] [IsLocalRing R]
    {n : ℕ} (hn : 1 ≤ n) (u : Rˣ) :
    unitsModMaximalIdealPowEquiv (R := R) hn
        (QuotientGroup.mk u) =
      unitReduction ((IsLocalRing.maximalIdeal R) ^ n) u

def adicUnitInverseLimit
    {R : Type*} [CommRing R] (I : Ideal R) : Type _

def adicUnitInverseLimitCompatibleFamiliesEquiv
    {R : Type*} [CommRing R] (I : Ideal R) :
    adicUnitInverseLimit I ≃
      compatibleGroupFamilies (fun n : ℕ => (R ⧸ I ^ n)ˣ)
        (fun {_ _} hmn =>
          Units.map (Ideal.Quotient.factorPow I hmn).toMonoidHom) := by
  unfold adicUnitInverseLimit
  exact Equiv.refl _

instance adicUnitInverseLimit.instCommGroup
    {R : Type*} [CommRing R] (I : Ideal R) :
    CommGroup (adicUnitInverseLimit I)

def adicUnitInverseLimitRepresentation
    {R : Type*} [CommRing R] (I : Ideal R) :
    adicUnitInverseLimit I ≃*
      compatibleGroupFamilies (fun n : ℕ => (R ⧸ I ^ n)ˣ)
        (fun {_ _} hmn =>
          Units.map (Ideal.Quotient.factorPow I hmn).toMonoidHom) :=
  (adicUnitInverseLimitCompatibleFamiliesEquiv I).mulEquiv

def adicUnitInverseLimit_mk
    {R : Type*} [CommRing R] (I : Ideal R)
    (x : ∀ n : ℕ, (R ⧸ I ^ n)ˣ)
    (compatible : ∀ {m n : ℕ} (hmn : m ≤ n),
      Units.map (Ideal.Quotient.factorPow I hmn).toMonoidHom (x n) = x m) :
    adicUnitInverseLimit I

def adicUnitInverseLimit_eval
    {R : Type*} [CommRing R] (I : Ideal R) (n : ℕ) :
    adicUnitInverseLimit I →* (R ⧸ I ^ n)ˣ where
  toFun x := (adicUnitInverseLimitCompatibleFamiliesEquiv I x).1 n
  map_one' := by rfl
  map_mul' _ _ := by rfl

theorem adicUnitInverseLimit_eval_mk
    {R : Type*} [CommRing R] (I : Ideal R)
    (x : ∀ n : ℕ, (R ⧸ I ^ n)ˣ)
    (compatible : ∀ {m n : ℕ} (hmn : m ≤ n),
      Units.map (Ideal.Quotient.factorPow I hmn).toMonoidHom (x n) = x m)
    (n : ℕ) :
    adicUnitInverseLimit_eval I n (adicUnitInverseLimit_mk I x compatible) =
      x n

theorem adicUnitInverseLimit_ext
    {R : Type*} [CommRing R] (I : Ideal R)
    {x y : adicUnitInverseLimit I}
    (h : ∀ n : ℕ, adicUnitInverseLimit_eval I n x =
      adicUnitInverseLimit_eval I n y) :
    x = y

theorem adicUnitInverseLimit_eval_transition
    {R : Type*} [CommRing R] (I : Ideal R)
    {m n : ℕ} (hmn : m ≤ n) (x : adicUnitInverseLimit I) :
    Units.map (Ideal.Quotient.factorPow I hmn).toMonoidHom
        (adicUnitInverseLimit_eval I n x) =
      adicUnitInverseLimit_eval I m x

def adicQuotientInverseLimitUnitsEquiv
    {R : Type*} [CommRing R] (I : Ideal R) :
    (adicQuotientInverseLimit I)ˣ ≃*
      adicUnitInverseLimit I where
  toFun u := adicUnitInverseLimit_mk I
    (fun n => Units.map (adicQuotientInverseLimit_eval I n).toMonoidHom u)
    (fun hmn => by
      ext
      exact adicQuotientInverseLimit_eval_factorPow I hmn
        (u : adicQuotientInverseLimit I))
  invFun u :=
    { val := adicQuotientInverseLimit_mk I
        (fun n => (adicUnitInverseLimit_eval I n u : R ⧸ I ^ n))
        (fun hmn => congrArg Units.val
          (adicUnitInverseLimit_eval_transition I hmn u))
      inv := adicQuotientInverseLimit_mk I
        (fun n =>
          (((adicUnitInverseLimit_eval I n u)⁻¹ : (R ⧸ I ^ n)ˣ) :
            R ⧸ I ^ n))
        (fun hmn => by
          have h := congrArg Units.val
            (congrArg Inv.inv
              (adicUnitInverseLimit_eval_transition I hmn u))
          simpa using h)
      val_inv := by
        ext n
        exact Units.mul_inv (adicUnitInverseLimit_eval I n u)
      inv_val := by
        ext n
        exact Units.inv_mul (adicUnitInverseLimit_eval I n u) }
  left_inv u := by
    ext n
    rfl
  right_inv u := by
    ext n
    rfl
  map_mul' u v := by
    ext n
    rfl

def adicCompletionUnitsEquivUnitInverseLimit
    {R : Type*} [CommRing R] (I : Ideal R) :
    (AdicCompletion I R)ˣ ≃* adicUnitInverseLimit I

def unitsEquivUnitInverseLimit
    {R : Type*} [CommRing R] (I : Ideal R) [IsAdicComplete I R] :
    Rˣ ≃* adicUnitInverseLimit I

theorem unitsEquivUnitInverseLimit_apply
    {R : Type*} [CommRing R] (I : Ideal R) [IsAdicComplete I R]
    (u : Rˣ) (n : ℕ) :
    adicUnitInverseLimit_eval I n (unitsEquivUnitInverseLimit I u) =
      unitReduction (I ^ n) u

def adicPositiveUnitInverseLimit
    {R : Type*} [CommRing R] (I : Ideal R) : Type _

def adicPositiveUnitInverseLimitCompatibleFamiliesEquiv
    {R : Type*} [CommRing R] (I : Ideal R) :
    adicPositiveUnitInverseLimit I ≃
      compatibleGroupFamilies (fun n : ℕ => (R ⧸ I ^ (n + 1))ˣ)
        (fun {_ _} hmn =>
          Units.map
            (Ideal.Quotient.factorPow I
              (Nat.succ_le_succ hmn)).toMonoidHom) := by
  unfold adicPositiveUnitInverseLimit
  exact Equiv.refl _

instance adicPositiveUnitInverseLimit.instCommGroup
    {R : Type*} [CommRing R] (I : Ideal R) :
    CommGroup (adicPositiveUnitInverseLimit I)

def adicPositiveUnitInverseLimitRepresentation
    {R : Type*} [CommRing R] (I : Ideal R) :
    adicPositiveUnitInverseLimit I ≃*
      compatibleGroupFamilies (fun n : ℕ => (R ⧸ I ^ (n + 1))ˣ)
        (fun {_ _} hmn =>
          Units.map
            (Ideal.Quotient.factorPow I
              (Nat.succ_le_succ hmn)).toMonoidHom) :=
  (adicPositiveUnitInverseLimitCompatibleFamiliesEquiv I).mulEquiv

def adicPositiveUnitInverseLimit_mk
    {R : Type*} [CommRing R] (I : Ideal R)
    (x : ∀ n : ℕ, (R ⧸ I ^ (n + 1))ˣ)
    (compatible : ∀ {m n : ℕ} (hmn : m ≤ n),
      Units.map
          (Ideal.Quotient.factorPow I
            (Nat.succ_le_succ hmn)).toMonoidHom (x n) = x m) :
    adicPositiveUnitInverseLimit I

def adicPositiveUnitInverseLimit_eval
    {R : Type*} [CommRing R] (I : Ideal R) (n : ℕ) :
    adicPositiveUnitInverseLimit I →* (R ⧸ I ^ (n + 1))ˣ where
  toFun x :=
    (adicPositiveUnitInverseLimitCompatibleFamiliesEquiv I x).1 n
  map_one' := by rfl
  map_mul' _ _ := by rfl

theorem adicPositiveUnitInverseLimit_eval_mk
    {R : Type*} [CommRing R] (I : Ideal R)
    (x : ∀ n : ℕ, (R ⧸ I ^ (n + 1))ˣ)
    (compatible : ∀ {m n : ℕ} (hmn : m ≤ n),
      Units.map
          (Ideal.Quotient.factorPow I
            (Nat.succ_le_succ hmn)).toMonoidHom (x n) = x m)
    (n : ℕ) :
    adicPositiveUnitInverseLimit_eval I n
        (adicPositiveUnitInverseLimit_mk I x compatible) = x n

theorem adicPositiveUnitInverseLimit_ext
    {R : Type*} [CommRing R] (I : Ideal R)
    {x y : adicPositiveUnitInverseLimit I}
    (h : ∀ n : ℕ, adicPositiveUnitInverseLimit_eval I n x =
      adicPositiveUnitInverseLimit_eval I n y) :
    x = y

theorem adicPositiveUnitInverseLimit_eval_transition
    {R : Type*} [CommRing R] (I : Ideal R)
    {m n : ℕ} (hmn : m ≤ n) (x : adicPositiveUnitInverseLimit I) :
    Units.map
        (Ideal.Quotient.factorPow I
          (Nat.succ_le_succ hmn)).toMonoidHom
        (adicPositiveUnitInverseLimit_eval I n x) =
      adicPositiveUnitInverseLimit_eval I m x

def adicUnitInverseLimit_toPositive
    {R : Type*} [CommRing R] (I : Ideal R) :
    adicUnitInverseLimit I →
      adicPositiveUnitInverseLimit I

def adicPositiveUnitInverseLimit_toAll
    {R : Type*} [CommRing R] (I : Ideal R) :
    adicPositiveUnitInverseLimit I →
      adicUnitInverseLimit I

theorem adicPositiveUnitInverseLimit_toPositive_toAll
    {R : Type*} [CommRing R] (I : Ideal R)
    (u : adicPositiveUnitInverseLimit I) :
    adicUnitInverseLimit_toPositive I
        (adicPositiveUnitInverseLimit_toAll I u) = u

theorem adicUnitInverseLimit_toAll_toPositive
    {R : Type*} [CommRing R] (I : Ideal R)
    (u : adicUnitInverseLimit I) :
    adicPositiveUnitInverseLimit_toAll I
        (adicUnitInverseLimit_toPositive I u) = u

def adicUnitInverseLimitEquivPositive
    {R : Type*} [CommRing R] (I : Ideal R) :
    adicUnitInverseLimit I ≃*
      adicPositiveUnitInverseLimit I where
  toFun := adicUnitInverseLimit_toPositive I
  invFun := adicPositiveUnitInverseLimit_toAll I
  left_inv := adicUnitInverseLimit_toAll_toPositive I
  right_inv := adicPositiveUnitInverseLimit_toPositive_toAll I
  map_mul' u v := by
    ext n
    rfl

def unitsEquivPositiveUnitInverseLimit
    {R : Type*} [CommRing R] (I : Ideal R) [IsAdicComplete I R] :
    Rˣ ≃* adicPositiveUnitInverseLimit I

theorem unitsEquivPositiveUnitInverseLimit_apply
    {R : Type*} [CommRing R] (I : Ideal R) [IsAdicComplete I R]
    (u : Rˣ) (n : ℕ) :
    adicPositiveUnitInverseLimit_eval I n
        (unitsEquivPositiveUnitInverseLimit I u) =
      unitReduction (I ^ (n + 1)) u

theorem dvrPowerIdeal_one_pow
    {O : Type*} [CommRing O] (π : O) (n : ℕ) :
    (uniformizerPowerIdeal π 1) ^ n = uniformizerPowerIdeal π n

theorem dvrPowerIdeal_le_of_le
    {O : Type*} [CommRing O] (π : O) {m n : ℕ} (hmn : m ≤ n) :
    uniformizerPowerIdeal π n ≤ uniformizerPowerIdeal π m

def dvrPowerIdealUnitTransition
    {O : Type*} [CommRing O] (π : O) {m n : ℕ} (hmn : m ≤ n) :
    O ⧸ uniformizerPowerIdeal π (n + 1) →+*
      O ⧸ uniformizerPowerIdeal π (m + 1)

def dvrPowerIdealUnitInverseLimit
    {O : Type*} [CommRing O] (π : O) : Type _

def dvrPowerIdealUnitInverseLimitCompatibleFamiliesEquiv
    {O : Type*} [CommRing O] (π : O) :
    dvrPowerIdealUnitInverseLimit π ≃
      compatibleGroupFamilies
        (fun n : ℕ => (O ⧸ uniformizerPowerIdeal π (n + 1))ˣ)
        (fun {_ _} hmn =>
          Units.map
            (dvrPowerIdealUnitTransition π hmn).toMonoidHom) := by
  unfold dvrPowerIdealUnitInverseLimit
  exact Equiv.refl _

instance dvrPowerIdealUnitInverseLimit.instCommGroup
    {O : Type*} [CommRing O] (π : O) :
    CommGroup (dvrPowerIdealUnitInverseLimit π)

def dvrPowerIdealUnitInverseLimitRepresentation
    {O : Type*} [CommRing O] (π : O) :
    dvrPowerIdealUnitInverseLimit π ≃*
      compatibleGroupFamilies
        (fun n : ℕ => (O ⧸ uniformizerPowerIdeal π (n + 1))ˣ)
        (fun {_ _} hmn =>
          Units.map
            (dvrPowerIdealUnitTransition π hmn).toMonoidHom) :=
  (dvrPowerIdealUnitInverseLimitCompatibleFamiliesEquiv π).mulEquiv

def dvrPowerIdealUnitInverseLimit_mk
    {O : Type*} [CommRing O] (π : O)
    (x : ∀ n : ℕ, (O ⧸ uniformizerPowerIdeal π (n + 1))ˣ)
    (compatible : ∀ {m n : ℕ} (hmn : m ≤ n),
      Units.map (dvrPowerIdealUnitTransition π hmn).toMonoidHom (x n) = x m) :
    dvrPowerIdealUnitInverseLimit π

def dvrPowerIdealUnitInverseLimit_eval
    {O : Type*} [CommRing O] (π : O) (n : ℕ) :
    dvrPowerIdealUnitInverseLimit π →*
      (O ⧸ uniformizerPowerIdeal π (n + 1))ˣ where
  toFun x :=
    (dvrPowerIdealUnitInverseLimitCompatibleFamiliesEquiv π x).1 n
  map_one' := by rfl
  map_mul' _ _ := by rfl

theorem dvrPowerIdealUnitInverseLimit_ext
    {O : Type*} [CommRing O] (π : O)
    {x y : dvrPowerIdealUnitInverseLimit π}
    (h : ∀ n : ℕ, dvrPowerIdealUnitInverseLimit_eval π n x =
      dvrPowerIdealUnitInverseLimit_eval π n y) :
    x = y

def powerIdealStageEquiv
    {O : Type*} [CommRing O] (π : O) (n : ℕ) :
    (O ⧸ (uniformizerPowerIdeal π 1) ^ (n + 1))ˣ ≃*
      (O ⧸ uniformizerPowerIdeal π (n + 1))ˣ

theorem powerIdealStageEquiv_apply
    {O : Type*} [CommRing O] (π : O) (n : ℕ)
    (u : (O ⧸ (uniformizerPowerIdeal π 1) ^ (n + 1))ˣ) :
    (powerIdealStageEquiv π n u :
      O ⧸ uniformizerPowerIdeal π (n + 1)) =
      (Ideal.quotientEquivAlgOfEq O
        (dvrPowerIdeal_one_pow π (n + 1))) (u : _)

theorem powerIdealStageEquiv_factorPow
    {O : Type*} [CommRing O] (π : O) {m n : ℕ} (hmn : m ≤ n)
    (x : O ⧸ (uniformizerPowerIdeal π 1) ^ (n + 1)) :
    (Ideal.quotientEquivAlgOfEq O
      (dvrPowerIdeal_one_pow π (m + 1)))
        (Ideal.Quotient.factorPow (uniformizerPowerIdeal π 1)
          (Nat.succ_le_succ hmn) x) =
      dvrPowerIdealUnitTransition π hmn
        ((Ideal.quotientEquivAlgOfEq O
          (dvrPowerIdeal_one_pow π (n + 1))) x)

def adicPositiveUnitInverseLimitEquivDVRPowerIdealUnitInverseLimit
    {O : Type*} [CommRing O] (π : O) :
    adicPositiveUnitInverseLimit (uniformizerPowerIdeal π 1) ≃*
      dvrPowerIdealUnitInverseLimit π

def dvrHigherUnitQuotientTransition
    {O : Type*} [CommRing O] (π : O) {m n : ℕ} (hmn : m ≤ n) :
    Oˣ ⧸ higherUnitSubgroup π (n + 1) →*
      Oˣ ⧸ higherUnitSubgroup π (m + 1)

theorem dvrHigherUnitQuotientTransition_mk
    {O : Type*} [CommRing O] (π : O) {m n : ℕ} (hmn : m ≤ n) (u : Oˣ) :
    dvrHigherUnitQuotientTransition π hmn
        (u : Oˣ ⧸ higherUnitSubgroup π (n + 1)) =
      (u : Oˣ ⧸ higherUnitSubgroup π (m + 1))

structure DiscreteHigherUnitQuotient
    {O : Type*} [CommRing O] (π : O) (n : ℕ) where
  /-- The underlying higher-unit quotient class. -/
  val : Oˣ ⧸ higherUnitSubgroup π n

def equiv {O : Type*} [CommRing O] (π : O) (n : ℕ) :
    DiscreteHigherUnitQuotient π n ≃
      Oˣ ⧸ higherUnitSubgroup π n where
  toFun := val
  invFun := fun x => ⟨x⟩
  left_inv := fun x => by cases x; rfl
  right_inv := fun _ => rfl

instance {O : Type*} [CommRing O] (π : O) (n : ℕ) :
    CommGroup (DiscreteHigherUnitQuotient π n)

instance {O : Type*} [CommRing O] (π : O) (n : ℕ) :
    TopologicalSpace (DiscreteHigherUnitQuotient π n)

instance {O : Type*} [CommRing O] (π : O) (n : ℕ) :
    DiscreteTopology (DiscreteHigherUnitQuotient π n)

def of {O : Type*} [CommRing O] (π : O) (n : ℕ)
    (x : Oˣ ⧸ higherUnitSubgroup π n) :
    DiscreteHigherUnitQuotient π n

theorem val_of {O : Type*} [CommRing O] (π : O) (n : ℕ)
    (x : Oˣ ⧸ higherUnitSubgroup π n) : (of π n x).val = x

def homeomorph {O : Type*} [CommRing O] (π : O) (n : ℕ) :
    @Homeomorph (DiscreteHigherUnitQuotient π n)
      (Oˣ ⧸ higherUnitSubgroup π n)
      (inferInstance : TopologicalSpace
        (DiscreteHigherUnitQuotient π n))
      (⊥ : TopologicalSpace (Oˣ ⧸ higherUnitSubgroup π n))

theorem homeomorph_apply {O : Type*} [CommRing O] (π : O) (n : ℕ)
    (x : DiscreteHigherUnitQuotient π n) : homeomorph π n x = x.val

theorem equiv_symm_apply {O : Type*} [CommRing O]
    (π : O) (n : ℕ) (x : Oˣ ⧸ higherUnitSubgroup π n) :
    (equiv π n).symm x = of π n x

def dvrHigherUnitQuotientInverseLimit
    {O : Type*} [CommRing O] (π : O) : Type _

def dvrHigherUnitQuotientInverseLimitCompatibleFamiliesEquiv
    {O : Type*} [CommRing O] (π : O) :
    dvrHigherUnitQuotientInverseLimit π ≃
      compatibleGroupFamilies
        (fun n : ℕ => Oˣ ⧸ higherUnitSubgroup π (n + 1))
        (fun {_ _} hmn => dvrHigherUnitQuotientTransition π hmn) := by
  unfold dvrHigherUnitQuotientInverseLimit
  exact Equiv.refl _

instance dvrHigherUnitQuotientInverseLimit.instCommGroup
    {O : Type*} [CommRing O] (π : O) :
    CommGroup (dvrHigherUnitQuotientInverseLimit π)

def dvrHigherUnitQuotientInverseLimitRepresentation
    {O : Type*} [CommRing O] (π : O) :
    dvrHigherUnitQuotientInverseLimit π ≃*
      compatibleGroupFamilies
        (fun n : ℕ => Oˣ ⧸ higherUnitSubgroup π (n + 1))
        (fun {_ _} hmn => dvrHigherUnitQuotientTransition π hmn) :=
  (dvrHigherUnitQuotientInverseLimitCompatibleFamiliesEquiv π).mulEquiv

def dvrHigherUnitQuotientInverseLimit_mk
    {O : Type*} [CommRing O] (π : O)
    (x : ∀ n : ℕ, Oˣ ⧸ higherUnitSubgroup π (n + 1))
    (compatible : ∀ {m n : ℕ} (hmn : m ≤ n),
      dvrHigherUnitQuotientTransition π hmn (x n) = x m) :
    dvrHigherUnitQuotientInverseLimit π

def dvrHigherUnitQuotientInverseLimit_eval
    {O : Type*} [CommRing O] (π : O) (n : ℕ) :
    dvrHigherUnitQuotientInverseLimit π →*
      Oˣ ⧸ higherUnitSubgroup π (n + 1) where
  toFun x :=
    (dvrHigherUnitQuotientInverseLimitCompatibleFamiliesEquiv π x).1 n
  map_one' := by rfl
  map_mul' _ _ := by rfl

theorem dvrHigherUnitQuotientInverseLimit_eval_mk
    {O : Type*} [CommRing O] (π : O)
    (x : ∀ n : ℕ, Oˣ ⧸ higherUnitSubgroup π (n + 1))
    (compatible : ∀ {m n : ℕ} (hmn : m ≤ n),
      dvrHigherUnitQuotientTransition π hmn (x n) = x m)
    (n : ℕ) :
    dvrHigherUnitQuotientInverseLimit_eval π n
        (dvrHigherUnitQuotientInverseLimit_mk π x compatible) = x n

theorem dvrHigherUnitQuotientInverseLimit_ext
    {O : Type*} [CommRing O] (π : O)
    {x y : dvrHigherUnitQuotientInverseLimit π}
    (h : ∀ n : ℕ, dvrHigherUnitQuotientInverseLimit_eval π n x =
      dvrHigherUnitQuotientInverseLimit_eval π n y) :
    x = y

theorem dvrHigherUnitQuotientInverseLimit_eval_transition
    {O : Type*} [CommRing O] (π : O)
    {m n : ℕ} (hmn : m ≤ n)
    (x : dvrHigherUnitQuotientInverseLimit π) :
    dvrHigherUnitQuotientTransition π hmn
        (dvrHigherUnitQuotientInverseLimit_eval π n x) =
      dvrHigherUnitQuotientInverseLimit_eval π m x

instance dvrHigherUnitQuotientInverseLimit.instTopologicalSpace
    {O : Type*} [CommRing O] (π : O) :
    TopologicalSpace (dvrHigherUnitQuotientInverseLimit π)

def
    dvrHigherUnitQuotientInverseLimitRepresentationHomeomorph
    {O : Type*} [CommRing O] (π : O) :
    letI : (n : ℕ) → TopologicalSpace
      (Oˣ ⧸ higherUnitSubgroup π (n + 1)) := fun _ => ⊥
    dvrHigherUnitQuotientInverseLimit π ≃ₜ
      compatibleGroupFamilies
        (fun n : ℕ => Oˣ ⧸ higherUnitSubgroup π (n + 1))
        (fun {_ _} hmn => dvrHigherUnitQuotientTransition π hmn) := by
  letI : (n : ℕ) → TopologicalSpace
      (Oˣ ⧸ higherUnitSubgroup π (n + 1)) := fun _ => ⊥
  exact
    (dvrHigherUnitQuotientInverseLimitCompatibleFamiliesEquiv π).homeomorph

def dvrHigherUnitQuotientInverseLimit_discreteEval
    {O : Type*} [CommRing O] (π : O) (n : ℕ) :
    dvrHigherUnitQuotientInverseLimit π →
      DiscreteHigherUnitQuotient π (n + 1)

theorem dvrHigherUnitQuotientInverseLimit_discreteEval_continuous
    {O : Type*} [CommRing O] (π : O) (n : ℕ) :
    Continuous (dvrHigherUnitQuotientInverseLimit_discreteEval π n)

theorem dvrHigherUnitQuotientInverseLimit_continuous_iff
    {O : Type*} [CommRing O] {α : Type*} [TopologicalSpace α]
    (π : O) (f : α → dvrHigherUnitQuotientInverseLimit π) :
    Continuous f ↔
      ∀ n : ℕ, Continuous fun x =>
        dvrHigherUnitQuotientInverseLimit_discreteEval π n (f x) := by
  constructor
  · intro hf n
    exact
      (dvrHigherUnitQuotientInverseLimit_discreteEval_continuous π n).comp hf
  · intro h
    let : (n : ℕ) → TopologicalSpace
        (Oˣ ⧸ higherUnitSubgroup π (n + 1)) := fun _ => ⊥
    let : (n : ℕ) → DiscreteTopology
        (Oˣ ⧸ higherUnitSubgroup π (n + 1)) := fun _ => ⟨rfl⟩
    let representation :=
      dvrHigherUnitQuotientInverseLimitRepresentationHomeomorph π
    have hrepresentation : Continuous fun x => representation (f x) :=
      Continuous.subtype_mk
        (continuous_pi fun n => by
          have hraw :=
            (DiscreteHigherUnitQuotient.homeomorph π (n + 1)).continuous.comp
              (h n)
          change Continuous fun x =>
            dvrHigherUnitQuotientInverseLimit_eval π n (f x)
          exact hraw)
        (fun x => by
          change ∀ {i j : ℕ} (hij : i ≤ j),
            dvrHigherUnitQuotientTransition π hij
                ((dvrHigherUnitQuotientInverseLimitCompatibleFamiliesEquiv π
                  (f x)).1 j) =
              (dvrHigherUnitQuotientInverseLimitCompatibleFamiliesEquiv π
                (f x)).1 i
          exact
            (dvrHigherUnitQuotientInverseLimitCompatibleFamiliesEquiv π
              (f x)).2)
    have hback := representation.symm.continuous.comp hrepresentation
    exact hback.congr fun x => representation.symm_apply_apply (f x)

def unitsToHigherUnitQuotientInverseLimit
    {O : Type*} [CommRing O] (π : O) :
    Oˣ →* dvrHigherUnitQuotientInverseLimit π where
  toFun u := dvrHigherUnitQuotientInverseLimit_mk π
    (fun _ => QuotientGroup.mk u)
    (fun {m n} hmn =>
      dvrHigherUnitQuotientTransition_mk π (m := m) (n := n) hmn u)
  map_one' := by ext n; rfl
  map_mul' u v := by ext n; rfl

theorem higherUnitQuotient_finiteStage_compat
    {O : Type*} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    {π : O} (hπ : Irreducible π) {m n : ℕ} (hmn : m ≤ n)
    (q : Oˣ ⧸ higherUnitSubgroup π (n + 1)) :
    units_quotient_equiv hπ
        (Nat.succ_pos m)
        (dvrHigherUnitQuotientTransition π hmn q) =
      Units.map (dvrPowerIdealUnitTransition π hmn).toMonoidHom
        (units_quotient_equiv hπ
          (Nat.succ_pos n) q)

def higherUnitQuotientInverseLimitEquivPowerIdealUnitInverseLimit
    {O : Type*} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    {π : O} (hπ : Irreducible π) :
    dvrHigherUnitQuotientInverseLimit π ≃*
      dvrPowerIdealUnitInverseLimit π

def dvrUnitsEquivHigherUnitQuotientInverseLimit
    {O : Type*} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    {π : O} (hπ : Irreducible π) [IsAdicComplete (uniformizerPowerIdeal π 1) O] :
    Oˣ ≃* dvrHigherUnitQuotientInverseLimit π

theorem dvrUnitsEquivHigherUnitQuotientInverseLimit_apply
    {O : Type*} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    {π : O} (hπ : Irreducible π) [IsAdicComplete (uniformizerPowerIdeal π 1) O]
    (u : Oˣ) (n : ℕ) :
    dvrHigherUnitQuotientInverseLimit_eval π n
        (dvrUnitsEquivHigherUnitQuotientInverseLimit hπ u) =
      QuotientGroup.mk u

theorem higherUnitQuotient_mk_eq_mk_iff_sub_mem
    {O : Type*} [CommRing O] (π : O) (n : ℕ) (u v : Oˣ) :
    (QuotientGroup.mk v : Oˣ ⧸ higherUnitSubgroup π n) =
        QuotientGroup.mk u ↔
      (v : O) - (u : O) ∈ uniformizerPowerIdeal π n

def adicUnitsTopology
    {O : Type*} [CommRing O] (I : Ideal O) : TopologicalSpace Oˣ

theorem higherUnitQuotient_mk_continuous_adic_raw
    {O : Type*} [CommRing O] (π : O) (n : ℕ) :
    @Continuous Oˣ (Oˣ ⧸ higherUnitSubgroup π n)
      (adicUnitsTopology (uniformizerPowerIdeal π 1))
      (⊥ : TopologicalSpace (Oˣ ⧸ higherUnitSubgroup π n))
      (fun u : Oˣ =>
        (QuotientGroup.mk u : Oˣ ⧸ higherUnitSubgroup π n)) := by
  let : TopologicalSpace O := (uniformizerPowerIdeal π 1).adicTopology
  let : TopologicalSpace (Oˣ ⧸ higherUnitSubgroup π n) := ⊥
  let : DiscreteTopology (Oˣ ⧸ higherUnitSubgroup π n) := ⟨rfl⟩
  rw [continuous_iff_continuousAt]
  intro u
  change Filter.Tendsto
    (fun v : Oˣ => (QuotientGroup.mk v :
      Oˣ ⧸ higherUnitSubgroup π n)) (𝓝 u)
    (𝓝 (QuotientGroup.mk u : Oˣ ⧸ higherUnitSubgroup π n))
  rw [@nhds_discrete (Oˣ ⧸ higherUnitSubgroup π n) _ _]
  rw [Filter.tendsto_def]
  intro s hs
  rw [mem_pure] at hs
  let ball : Set O :=
    (fun y => (u : O) + y) ''
      (((uniformizerPowerIdeal π 1) ^ n : Ideal O) : Set O)
  have hball : ball ∈ 𝓝 (u : O) :=
    (Ideal.hasBasis_nhds_adic (uniformizerPowerIdeal π 1) (u : O)).mem_iff.mpr
      ⟨n, trivial, subset_rfl⟩
  have hpre : {v : Oˣ | (v : O) ∈ ball} ∈ 𝓝 u :=
    Units.continuous_val.continuousAt hball
  exact mem_of_superset hpre (by
    intro v hv
    rcases hv with ⟨z, hz, hzv⟩
    have hsub : (v : O) - (u : O) ∈ uniformizerPowerIdeal π n := by
      rw [← dvrPowerIdeal_one_pow π n]
      have hz_eq : (v : O) - (u : O) = z := by
        rw [← hzv]
        ring
      simpa [hz_eq] using hz
    have hq :
        (QuotientGroup.mk v : Oˣ ⧸ higherUnitSubgroup π n) =
          QuotientGroup.mk u :=
      (higherUnitQuotient_mk_eq_mk_iff_sub_mem
        π n u v).2 hsub
    simpa [hq] using hs)

theorem higherUnitQuotient_mk_continuous_adic
    {O : Type*} [CommRing O] (π : O) (n : ℕ) :
    Continuous fun u : WithTopology Oˣ
        (adicUnitsTopology (uniformizerPowerIdeal π 1)) =>
      DiscreteHigherUnitQuotient.of π n
        (QuotientGroup.mk u.ofTopology : Oˣ ⧸ higherUnitSubgroup π n) := by
  let : TopologicalSpace O := (uniformizerPowerIdeal π 1).adicTopology
  let : TopologicalSpace (Oˣ ⧸ higherUnitSubgroup π n) := ⊥
  let : DiscreteTopology (Oˣ ⧸ higherUnitSubgroup π n) := ⟨rfl⟩
  have hraw := higherUnitQuotient_mk_continuous_adic_raw π n
  have hunderlying : Continuous fun u :
      WithTopology Oˣ
      (adicUnitsTopology (uniformizerPowerIdeal π 1)) =>
        (QuotientGroup.mk u.ofTopology : Oˣ ⧸ higherUnitSubgroup π n) :=
    hraw.comp (WithTopology.continuous_ofTopology
      (adicUnitsTopology (uniformizerPowerIdeal π 1)))
  have hmodel :=
    (DiscreteHigherUnitQuotient.homeomorph π n).symm.continuous.comp
      hunderlying
  change Continuous (fun u : WithTopology Oˣ
      (adicUnitsTopology (uniformizerPowerIdeal π 1)) =>
    (DiscreteHigherUnitQuotient.equiv π n).symm
      (QuotientGroup.mk u.ofTopology : Oˣ ⧸ higherUnitSubgroup π n)) at hmodel
  simpa only [DiscreteHigherUnitQuotient.equiv_symm_apply] using hmodel

def unitsCompatibleFamiliesHomeomorph
    {O : Type*} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    {π : O} (hπ : Irreducible π) [IsAdicComplete (uniformizerPowerIdeal π 1) O] :
    letI : TopologicalSpace O := (uniformizerPowerIdeal π 1).adicTopology
    letI : (n : ℕ) →
      TopologicalSpace (Oˣ ⧸ higherUnitSubgroup π (n + 1)) := fun _ => ⊥
    Oˣ ≃ₜ compatibleGroupFamilies
      (fun n : ℕ => Oˣ ⧸ higherUnitSubgroup π (n + 1))
      (fun {_ _} hmn => dvrHigherUnitQuotientTransition π hmn) := by
  letI : TopologicalSpace O := (uniformizerPowerIdeal π 1).adicTopology
  letI : (n : ℕ) →
      TopologicalSpace (Oˣ ⧸ higherUnitSubgroup π (n + 1)) := fun _ => ⊥
  letI : (n : ℕ) →
      DiscreteTopology (Oˣ ⧸ higherUnitSubgroup π (n + 1)) :=
    fun _ => ⟨rfl⟩
  let e := (dvrUnitsEquivHigherUnitQuotientInverseLimit hπ).trans
    (dvrHigherUnitQuotientInverseLimitRepresentation π)
  let c := (dvrHigherUnitQuotientInverseLimitRepresentation π).toMonoidHom.comp
    (unitsToHigherUnitQuotientInverseLimit π)
  refine
    { toFun := fun u => c u
      invFun := fun q => e.symm q
      left_inv := ?_
      right_inv := ?_
      continuous_toFun := ?_
      continuous_invFun := ?_ }
  · intro u
    have hc : c u = e u := by
      ext n
      exact (dvrUnitsEquivHigherUnitQuotientInverseLimit_apply
        hπ u n).symm
    change e.symm (c u) = u
    rw [hc]
    exact e.left_inv u
  · intro q
    ext n
    change (QuotientGroup.mk (e.symm q) :
        Oˣ ⧸ higherUnitSubgroup π (n + 1)) = q.1 n
    calc
      (QuotientGroup.mk (e.symm q) :
          Oˣ ⧸ higherUnitSubgroup π (n + 1)) =
          (e (e.symm q)).1 n :=
        (dvrUnitsEquivHigherUnitQuotientInverseLimit_apply
          hπ (e.symm q) n).symm
      _ = q.1 n := by simp [e.apply_symm_apply q]
  · change Continuous fun u : Oˣ => c u
    exact Continuous.subtype_mk
      (continuous_pi fun n => by
        simpa [c, unitsToHigherUnitQuotientInverseLimit] using
          (higherUnitQuotient_mk_continuous_adic_raw π (n + 1)))
      (by
        intro u m n hmn
        exact dvrHigherUnitQuotientTransition_mk π hmn u)
  · apply Units.continuous_iff.mpr
    constructor
    · rw [continuous_iff_continuousAt]
      intro q
      rw [ContinuousAt, Filter.tendsto_def]
      intro s hs
      rcases (Ideal.hasBasis_nhds_adic (uniformizerPowerIdeal π 1)
          ((e.symm q : Oˣ) : O)).mem_iff.mp hs with
        ⟨n, _hn, hns⟩
      let cylinder : Set (compatibleGroupFamilies
          (fun n : ℕ => Oˣ ⧸ higherUnitSubgroup π (n + 1))
          (fun {_ _} hmn => dvrHigherUnitQuotientTransition π hmn)) :=
        {q' | q'.1 n = q.1 n}
      have hcont_coord :
          Continuous fun q' : compatibleGroupFamilies
              (fun n : ℕ => Oˣ ⧸ higherUnitSubgroup π (n + 1))
              (fun {_ _} hmn => dvrHigherUnitQuotientTransition π hmn) =>
            q'.1 n := by
        exact (continuous_apply n).comp continuous_subtype_val
      have hcyl_open : IsOpen cylinder := by
        exact
          (isOpen_discrete
            ({q.1 n} : Set (Oˣ ⧸ higherUnitSubgroup π (n + 1)))).preimage
              hcont_coord
      have hqmem : q ∈ cylinder := rfl
      exact mem_of_superset (hcyl_open.mem_nhds hqmem) (by
        intro q' hq'
        apply hns
        have hmk :
            (QuotientGroup.mk (e.symm q') :
                Oˣ ⧸ higherUnitSubgroup π (n + 1)) =
              QuotientGroup.mk (e.symm q) := by
          calc
            (QuotientGroup.mk (e.symm q') :
                Oˣ ⧸ higherUnitSubgroup π (n + 1)) =
                (e (e.symm q')).1 n :=
              (dvrUnitsEquivHigherUnitQuotientInverseLimit_apply
                hπ (e.symm q') n).symm
            _ = q'.1 n := by simp [e.apply_symm_apply q']
            _ = q.1 n := hq'
            _ = (e (e.symm q)).1 n := by simp [e.apply_symm_apply q]
            _ = QuotientGroup.mk (e.symm q) :=
              dvrUnitsEquivHigherUnitQuotientInverseLimit_apply
                hπ (e.symm q) n
        have hsub_succ :
            ((e.symm q' : Oˣ) : O) - ((e.symm q : Oˣ) : O) ∈
              uniformizerPowerIdeal π (n + 1) :=
          (higherUnitQuotient_mk_eq_mk_iff_sub_mem
            π (n + 1) (e.symm q) (e.symm q')).1 hmk
        have hsub :
            ((e.symm q' : Oˣ) : O) - ((e.symm q : Oˣ) : O) ∈
              (uniformizerPowerIdeal π 1) ^ n := by
          rw [dvrPowerIdeal_one_pow π n]
          exact dvrPowerIdeal_le_of_le π (Nat.le_succ n) hsub_succ
        refine ⟨((e.symm q' : Oˣ) : O) - ((e.symm q : Oˣ) : O), hsub, ?_⟩
        change ((e.symm q : Oˣ) : O) +
            (((e.symm q' : Oˣ) : O) - ((e.symm q : Oˣ) : O)) =
          ((e.symm q' : Oˣ) : O)
        ring)
    · rw [continuous_iff_continuousAt]
      intro q
      rw [ContinuousAt, Filter.tendsto_def]
      intro s hs
      rcases (Ideal.hasBasis_nhds_adic (uniformizerPowerIdeal π 1)
          (((e.symm q)⁻¹ : Oˣ) : O)).mem_iff.mp hs with
        ⟨n, _hn, hns⟩
      let cylinder : Set (compatibleGroupFamilies
          (fun n : ℕ => Oˣ ⧸ higherUnitSubgroup π (n + 1))
          (fun {_ _} hmn => dvrHigherUnitQuotientTransition π hmn)) :=
        {q' | q'.1 n = q.1 n}
      have hcont_coord :
          Continuous fun q' : compatibleGroupFamilies
              (fun n : ℕ => Oˣ ⧸ higherUnitSubgroup π (n + 1))
              (fun {_ _} hmn => dvrHigherUnitQuotientTransition π hmn) =>
            q'.1 n := by
        exact (continuous_apply n).comp continuous_subtype_val
      have hcyl_open : IsOpen cylinder := by
        exact
          (isOpen_discrete
            ({q.1 n} : Set (Oˣ ⧸ higherUnitSubgroup π (n + 1)))).preimage
              hcont_coord
      have hqmem : q ∈ cylinder := rfl
      exact mem_of_superset (hcyl_open.mem_nhds hqmem) (by
        intro q' hq'
        apply hns
        have hmk :
            (QuotientGroup.mk (e.symm q') :
                Oˣ ⧸ higherUnitSubgroup π (n + 1)) =
              QuotientGroup.mk (e.symm q) := by
          calc
            (QuotientGroup.mk (e.symm q') :
                Oˣ ⧸ higherUnitSubgroup π (n + 1)) =
                (e (e.symm q')).1 n :=
              (dvrUnitsEquivHigherUnitQuotientInverseLimit_apply
                hπ (e.symm q') n).symm
            _ = q'.1 n := by simp [e.apply_symm_apply q']
            _ = q.1 n := hq'
            _ = (e (e.symm q)).1 n := by simp [e.apply_symm_apply q]
            _ = QuotientGroup.mk (e.symm q) :=
              dvrUnitsEquivHigherUnitQuotientInverseLimit_apply
                hπ (e.symm q) n
        have hinv_mk :
            (QuotientGroup.mk ((e.symm q')⁻¹ : Oˣ) :
                Oˣ ⧸ higherUnitSubgroup π (n + 1)) =
              QuotientGroup.mk ((e.symm q)⁻¹ : Oˣ) := by
          simpa using congrArg Inv.inv hmk
        have hinv_sub_succ :
            (((e.symm q')⁻¹ : Oˣ) : O) - (((e.symm q)⁻¹ : Oˣ) : O) ∈
              uniformizerPowerIdeal π (n + 1) :=
          (higherUnitQuotient_mk_eq_mk_iff_sub_mem
            π (n + 1) ((e.symm q)⁻¹ : Oˣ) ((e.symm q')⁻¹ : Oˣ)).1 hinv_mk
        have hinv_sub :
            (((e.symm q')⁻¹ : Oˣ) : O) - (((e.symm q)⁻¹ : Oˣ) : O) ∈
              (uniformizerPowerIdeal π 1) ^ n := by
          rw [dvrPowerIdeal_one_pow π n]
          exact dvrPowerIdeal_le_of_le π (Nat.le_succ n)
            hinv_sub_succ
        refine
          ⟨(((e.symm q')⁻¹ : Oˣ) : O) - (((e.symm q)⁻¹ : Oˣ) : O),
            hinv_sub, ?_⟩
        change (((e.symm q)⁻¹ : Oˣ) : O) +
            ((((e.symm q')⁻¹ : Oˣ) : O) - (((e.symm q)⁻¹ : Oˣ) : O)) =
          (((e.symm q')⁻¹ : Oˣ) : O)
        ring)

def unitsEquivHigherUnitQuotientInverseLimitHomeomorph
    {O : Type*} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    {π : O} (hπ : Irreducible π)
    [IsAdicComplete (uniformizerPowerIdeal π 1) O] :
    WithTopology Oˣ
        (adicUnitsTopology (uniformizerPowerIdeal π 1)) ≃ₜ
      dvrHigherUnitQuotientInverseLimit π

def completeDVF_valuationSubring_adicCompletionAlgEquiv
    {K : Type u} [Field K]
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) :
    F.valuationSubring ≃ₐ[F.valuationSubring]
      AdicCompletion F.maximalIdeal F.valuationSubring

def completeDVF_valuationSubring_quotientInverseLimitEquiv
    {K : Type u} [Field K]
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) :
    F.valuationSubring ≃+*
      adicQuotientInverseLimit F.maximalIdeal

theorem completeDVF_valuationSubring_quotientInverseLimitEquiv_apply
    {K : Type u} [Field K]
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
    (x : F.valuationSubring) (n : ℕ) :
    adicQuotientInverseLimit_eval F.maximalIdeal n
        (completeDVF_valuationSubring_quotientInverseLimitEquiv F x) =
      Ideal.Quotient.mk (F.maximalIdeal ^ n) x

def completeDVF_units_adicCompletionUnitsEquiv
    {K : Type u} [Field K]
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) :
    F.valuationSubringˣ ≃*
      (AdicCompletion F.maximalIdeal F.valuationSubring)ˣ

theorem completeDVF_units_adicCompletionUnitsEquiv_apply
    {K : Type u} [Field K]
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
    (u : F.valuationSubringˣ) :
    (completeDVF_units_adicCompletionUnitsEquiv F u :
      AdicCompletion F.maximalIdeal F.valuationSubring) =
      completeDVF_valuationSubring_adicCompletionAlgEquiv F
        (u : F.valuationSubring)

theorem completeDVF_units_coordinates_injective
    {K : Type u} [Field K]
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
    {u₁ u₂ : F.valuationSubringˣ}
    (h :
      ∀ n : ℕ,
        unitReduction (F.maximalIdeal ^ n) u₁ =
          unitReduction (F.maximalIdeal ^ n) u₂) :
    u₁ = u₂

theorem completeDVF_units_coordinates_surjective
    {K : Type u} [Field K]
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
    (z : (AdicCompletion F.maximalIdeal F.valuationSubring)ˣ) :
    ∃ u : F.valuationSubringˣ,
      completeDVF_units_adicCompletionUnitsEquiv F u = z ∧
        ∀ n : ℕ,
          unitReduction (F.maximalIdeal ^ n) u =
            Units.map (AdicCompletion.evalₐ F.maximalIdeal n).toMonoidHom z

def completeDVF_unitsEquivUnitInverseLimit
    {K : Type u} [Field K]
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) :
    F.valuationSubringˣ ≃*
      adicUnitInverseLimit F.maximalIdeal

theorem completeDVF_unitsEquivUnitInverseLimit_apply
    {K : Type u} [Field K]
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
    (u : F.valuationSubringˣ) (n : ℕ) :
    adicUnitInverseLimit_eval F.maximalIdeal n
        (completeDVF_unitsEquivUnitInverseLimit F u) =
      unitReduction (F.maximalIdeal ^ n) u

def completeDVF_unitsModMaximalIdealPowEquiv
    {K : Type u} [Field K]
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
    {n : ℕ} (hn : 1 ≤ n) :
    F.valuationSubringˣ ⧸
        (unitReduction (F.maximalIdeal ^ n)).ker ≃*
      (F.valuationSubring ⧸ F.maximalIdeal ^ n)ˣ

theorem completeDVF_unitsModMaximalIdealPowEquiv_mk
    {K : Type u} [Field K]
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
    {n : ℕ} (hn : 1 ≤ n) (u : F.valuationSubringˣ) :
    completeDVF_unitsModMaximalIdealPowEquiv F hn
        (QuotientGroup.mk u) =
      unitReduction (F.maximalIdeal ^ n) u

theorem completeDVF_valuationSubring_quotient_coordinates_injective
    {K : Type u} [Field K]
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
    {x y : F.valuationSubring}
    (h :
      ∀ n : ℕ,
        Ideal.Quotient.mk (F.maximalIdeal ^ n) x =
          Ideal.Quotient.mk (F.maximalIdeal ^ n) y) :
    x = y

theorem completeDVF_units_quotient_coordinates_injective
    {K : Type u} [Field K]
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
    {u₁ u₂ : F.valuationSubringˣ}
    (h :
      ∀ n : ℕ,
        Ideal.Quotient.mk (F.maximalIdeal ^ n) (u₁ : F.valuationSubring) =
          Ideal.Quotient.mk (F.maximalIdeal ^ n) (u₂ : F.valuationSubring)) :
    u₁ = u₂

def completeValuedField_valuationSubringEquivPositiveQuotientInverseLimit
    {K : Type u} [Field K] {Gamma : Type v}
    [LinearOrderedCommGroupWithZero Gamma] [MulArchimedean Gamma]
    [Valued K Gamma]
    [(Valued.v : Valuation K Gamma).IsRankOneDiscrete]
    [CompleteSpace K] :
    let val := (Valued.v : Valuation K Gamma)
    let O := val.valuationSubring
    let m := IsLocalRing.maximalIdeal O
    O ≃+* adicPositiveQuotientInverseLimit m := by
  dsimp only
  let F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K :=
    completeDVFOfCompleteValuedField (K := K) (Gamma := Gamma)
  exact
    (completeDVF_valuationSubring_quotientInverseLimitEquiv F).trans
      (adicQuotientInverseLimitEquivPositive F.maximalIdeal)

theorem completeValuedField_valuationSubringEquivPositiveQuotientInverseLimit_apply
    {K : Type u} [Field K] {Gamma : Type v}
    [LinearOrderedCommGroupWithZero Gamma] [MulArchimedean Gamma]
    [Valued K Gamma]
    [(Valued.v : Valuation K Gamma).IsRankOneDiscrete]
    [CompleteSpace K]
    (x : (Valued.v : Valuation K Gamma).valuationSubring) (n : ℕ) :
    adicPositiveQuotientInverseLimit_eval
        (IsLocalRing.maximalIdeal
          (Valued.v : Valuation K Gamma).valuationSubring) n
        (completeValuedField_valuationSubringEquivPositiveQuotientInverseLimit
          (K := K) (Gamma := Gamma) x) =
      Ideal.Quotient.mk
        ((IsLocalRing.maximalIdeal
          (Valued.v : Valuation K Gamma).valuationSubring) ^ (n + 1)) x

def completeValuedField_valuationSubringPositiveQuotientInverseLimitHomeomorph
    {K : Type u} [Field K] {Gamma : Type v}
    [LinearOrderedCommGroupWithZero Gamma] [MulArchimedean Gamma]
    [Valued K Gamma]
    [(Valued.v : Valuation K Gamma).IsRankOneDiscrete]
    [CompleteSpace K] :
    let val := (Valued.v : Valuation K Gamma)
    let O := val.valuationSubring
    let m := IsLocalRing.maximalIdeal O
    O ≃ₜ adicPositiveQuotientInverseLimit m := by
  dsimp only
  let val := (Valued.v : Valuation K Gamma)
  let O := val.valuationSubring
  let m := IsLocalRing.maximalIdeal O
  letI : IsAdicComplete m O :=
    rankOneDiscreteValuationSubring_isAdicComplete
      (K := K) (Gamma := Gamma)
  have hadic : IsAdic m :=
    rankOneDiscreteValuationSubring_isAdic
      (K := K) (Gamma := Gamma)
  let hAdic := adicPositiveQuotientInverseLimitHomeomorph m
  let hNative := hadic.symm ▸ hAdic
  exact
    (WithTopology.homeomorph
      (α := O)
      (topology := (inferInstance : TopologicalSpace O))).symm.trans hNative

theorem completeValuedField_uniformizer_irreducible
    {K : Type u} [Field K] {Gamma : Type v}
    [LinearOrderedCommGroupWithZero Gamma] [MulArchimedean Gamma]
    [Valued K Gamma]
    [(Valued.v : Valuation K Gamma).IsRankOneDiscrete]
    [CompleteSpace K]
    {pi : (Valued.v : Valuation K Gamma).valuationSubring}
    (hpi : (Valued.v : Valuation K Gamma).IsUniformizer (pi : K)) :
    Irreducible pi

theorem completeValuedField_uniformizerPowerIdeal_one_eq_maximalIdeal
    {K : Type u} [Field K] {Gamma : Type v}
    [LinearOrderedCommGroupWithZero Gamma] [MulArchimedean Gamma]
    [Valued K Gamma]
    [(Valued.v : Valuation K Gamma).IsRankOneDiscrete]
    [CompleteSpace K]
    {pi : (Valued.v : Valuation K Gamma).valuationSubring}
    (hpi : (Valued.v : Valuation K Gamma).IsUniformizer (pi : K)) :
    uniformizerPowerIdeal pi 1 =
      IsLocalRing.maximalIdeal
        (Valued.v : Valuation K Gamma).valuationSubring

theorem completeValuedField_uniformizerIdeal_isAdicComplete
    {K : Type u} [Field K] {Gamma : Type v}
    [LinearOrderedCommGroupWithZero Gamma] [MulArchimedean Gamma]
    [Valued K Gamma]
    [(Valued.v : Valuation K Gamma).IsRankOneDiscrete]
    [CompleteSpace K]
    {pi : (Valued.v : Valuation K Gamma).valuationSubring}
    (hpi : (Valued.v : Valuation K Gamma).IsUniformizer (pi : K)) :
    IsAdicComplete (uniformizerPowerIdeal pi 1)
      (Valued.v : Valuation K Gamma).valuationSubring

theorem completeValuedField_uniformizerIdeal_isAdic
    {K : Type u} [Field K] {Gamma : Type v}
    [LinearOrderedCommGroupWithZero Gamma] [MulArchimedean Gamma]
    [Valued K Gamma]
    [(Valued.v : Valuation K Gamma).IsRankOneDiscrete]
    [CompleteSpace K]
    {pi : (Valued.v : Valuation K Gamma).valuationSubring}
    (hpi : (Valued.v : Valuation K Gamma).IsUniformizer (pi : K)) :
    IsAdic (uniformizerPowerIdeal pi 1)

def completeValuedField_unitsEquivHigherUnitQuotientInverseLimit
    {K : Type u} [Field K] {Gamma : Type v}
    [LinearOrderedCommGroupWithZero Gamma] [MulArchimedean Gamma]
    [Valued K Gamma]
    [(Valued.v : Valuation K Gamma).IsRankOneDiscrete]
    [CompleteSpace K]
    {pi : (Valued.v : Valuation K Gamma).valuationSubring}
    (hpi : (Valued.v : Valuation K Gamma).IsUniformizer (pi : K)) :
    (Valued.v : Valuation K Gamma).valuationSubringˣ ≃*
      dvrHigherUnitQuotientInverseLimit pi

theorem completeValuedField_unitsEquivHigherUnitQuotientInverseLimit_apply
    {K : Type u} [Field K] {Gamma : Type v}
    [LinearOrderedCommGroupWithZero Gamma] [MulArchimedean Gamma]
    [Valued K Gamma]
    [(Valued.v : Valuation K Gamma).IsRankOneDiscrete]
    [CompleteSpace K]
    {pi : (Valued.v : Valuation K Gamma).valuationSubring}
    (hpi : (Valued.v : Valuation K Gamma).IsUniformizer (pi : K))
    (u : (Valued.v : Valuation K Gamma).valuationSubringˣ) (n : ℕ) :
    dvrHigherUnitQuotientInverseLimit_eval pi n
      (completeValuedField_unitsEquivHigherUnitQuotientInverseLimit
        hpi u) = QuotientGroup.mk u

def completeValuedField_unitsHigherUnitQuotientInverseLimitHomeomorph
    {K : Type u} [Field K] {Gamma : Type v}
    [LinearOrderedCommGroupWithZero Gamma] [MulArchimedean Gamma]
    [Valued K Gamma]
    [(Valued.v : Valuation K Gamma).IsRankOneDiscrete]
    [CompleteSpace K]
    {pi : (Valued.v : Valuation K Gamma).valuationSubring}
    (hpi : (Valued.v : Valuation K Gamma).IsUniformizer (pi : K)) :
    let O := (Valued.v : Valuation K Gamma).valuationSubring
    Oˣ ≃ₜ dvrHigherUnitQuotientInverseLimit pi := by
  dsimp only
  let O := (Valued.v : Valuation K Gamma).valuationSubring
  letI : IsDiscreteValuationRing O :=
    rankOneDiscreteValuationSubring_isDiscreteValuationRing
      (K := K) (Gamma := Gamma)
  letI : IsAdicComplete (uniformizerPowerIdeal pi 1) O :=
    completeValuedField_uniformizerIdeal_isAdicComplete hpi
  have hadic : IsAdic (uniformizerPowerIdeal pi 1) :=
    completeValuedField_uniformizerIdeal_isAdic hpi
  let hirr := completeValuedField_uniformizer_irreducible hpi
  let hAdic :
      WithTopology Oˣ
          (adicUnitsTopology (uniformizerPowerIdeal pi 1)) ≃ₜ
        dvrHigherUnitQuotientInverseLimit pi :=
    unitsEquivHigherUnitQuotientInverseLimitHomeomorph hirr
  have hUnitsTopology :
      (inferInstance : TopologicalSpace Oˣ) =
        adicUnitsTopology (uniformizerPowerIdeal pi 1) := by
    unfold adicUnitsTopology
    rw [← hadic]
  let hNative :
      WithTopology Oˣ
          (inferInstance : TopologicalSpace Oˣ) ≃ₜ
        dvrHigherUnitQuotientInverseLimit pi :=
    hUnitsTopology.symm ▸ hAdic
  exact
    (WithTopology.homeomorph
      (α := Oˣ)
      (topology := (inferInstance : TopologicalSpace Oˣ))).symm.trans hNative