FieldUnitDecomposition.lean

theorem exists_roots_principalUnit_uniformizer_zpow_of_completeDVF
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (x : Kˣ) :
    ∃ ζ : residueRootsOfUnityGroup F,
    ∃ p : (LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1,
    ∃ n : ℤ,
      x =
        valuationSubringUnitFieldUnitHom F
            (ζ : F.valuationSubringˣ) *
          valuationSubringUnitFieldUnitHom F
            (p : F.valuationSubringˣ) *
          (Units.mk0 (π : K) hπ.ne_zero) ^ n

theorem roots_principalUnit_uniformizer_zpow_eq_iff_of_completeDVF
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (ζ η : residueRootsOfUnityGroup F)
    (p q : (higherPrincipalUnitGroup F) 1) (m n : ℤ) :
    valuationSubringUnitFieldUnitHom F
          (ζ : F.valuationSubringˣ) *
        valuationSubringUnitFieldUnitHom F
          (p : F.valuationSubringˣ) *
        (Units.mk0 (π : K) hπ.ne_zero) ^ m =
      valuationSubringUnitFieldUnitHom F
          (η : F.valuationSubringˣ) *
        valuationSubringUnitFieldUnitHom F
          (q : F.valuationSubringˣ) *
        (Units.mk0 (π : K) hπ.ne_zero) ^ n ↔
      ζ = η ∧ p = q ∧ m = n

def fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K)) :
    fieldUnitDecompositionFactors F ≃* Kˣ

theorem fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF_apply
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (z : fieldUnitDecompositionFactors F) :
    fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
        F hπ z =
      valuationSubringUnitFieldUnitHom F
          (z.1.1 : F.valuationSubringˣ) *
        valuationSubringUnitFieldUnitHom F
          (z.1.2 : F.valuationSubringˣ) *
        (Units.mk0 (π : K) hπ.ne_zero) ^ Multiplicative.toAdd z.2

theorem multiplicativeIntegerValuationOfUniformizer_fieldUnitsEquivRootsPrincipalUnitsUniformizer
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (z : fieldUnitDecompositionFactors F) :
    ((multiplicativeIntegerValuationOfUniformizer F) hπ).val
        (fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
          F hπ z) =
      Multiplicative.toAdd z.2

theorem uniformizerValueExponent_fieldUnitsEquivRootsPrincipalUnitsUniformizer
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (z : fieldUnitDecompositionFactors F) :
    (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.uniformizerValueExponent F) hπ
        (fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
          F hπ z) =
      Multiplicative.toAdd z.2

theorem uniformizerValueExponent_fieldUnitsEquivRootsPrincipalUnitsUniformizer_symm
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (x : Kˣ) :
    Multiplicative.toAdd
        ((fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
          F hπ).symm x).2 =
      (uniformizerValueExponent F) hπ x

theorem fieldUnitsEquivRootsPrincipalUnitsUniformizer_symm_snd
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (x : Kˣ) :
    ((fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
      F hπ).symm x).2 =
      Multiplicative.ofAdd ((uniformizerValueExponent F) hπ x)

theorem fieldUnitsEquivRootsPrincipalUnitsUniformizer_symm_factors_mul_uniformizer_zpow
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (x : Kˣ) :
    valuationSubringUnitFieldUnitHom F
          (((fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
            F hπ).symm x).1.1 : F.valuationSubringˣ) *
        valuationSubringUnitFieldUnitHom F
          (((fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
            F hπ).symm x).1.2 : F.valuationSubringˣ) *
        (Units.mk0 (π : K) hπ.ne_zero) ^ (uniformizerValueExponent F) hπ x =
      x

theorem fieldUnitsEquivRootsPrincipalUnitsUniformizer_symm_unitPart_eq_mul_uniformizer_zpow_neg
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (x : Kˣ) :
    valuationSubringUnitFieldUnitHom F
          (((fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
            F hπ).symm x).1.1 : F.valuationSubringˣ) *
        valuationSubringUnitFieldUnitHom F
          (((fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
            F hπ).symm x).1.2 : F.valuationSubringˣ) =
      x * (Units.mk0 (π : K) hπ.ne_zero) ^
        (-((uniformizerValueExponent F) hπ x))

theorem fieldUnitsEquivRootsPrincipalUnitsUniformizer_unitPart_mem_unitGroup
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (x : Kˣ) :
    x * (Units.mk0 (π : K) hπ.ne_zero) ^
        (-((uniformizerValueExponent F) hπ x)) ∈
      F.valuation.valuationSubring.unitGroup

def fieldUnitUniformizerUnitPart
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (x : Kˣ) : F.valuationSubringˣ

theorem valuationSubringUnitFieldUnitHom_fieldUnitUniformizerUnitPart
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (x : Kˣ) :
    valuationSubringUnitFieldUnitHom F
        (fieldUnitUniformizerUnitPart F hπ x) =
      x * (Units.mk0 (π : K) hπ.ne_zero) ^
        (-((uniformizerValueExponent F) hπ x))

theorem fieldUnitsEquivRootsPrincipalUnitsUniformizer_symm_unitSubringUnit_eq
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (x : Kˣ) :
    (((fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
      F hπ).symm x).1.1 : F.valuationSubringˣ) *
        (((fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
          F hπ).symm x).1.2 : F.valuationSubringˣ) =
      fieldUnitUniformizerUnitPart F hπ x

theorem fieldUnitsEquivRootsPrincipalUnitsUniformizer_symm_fst_eq_unitPart
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (x : Kˣ) :
    ((fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
      F hπ).symm x).1 =
      (valuationSubringUnitsEquivRootsTimesPrincipalUnits
        F).symm
        (fieldUnitUniformizerUnitPart F hπ x)

theorem uniformizerValueExponent_eq_of_mrangeRestrict_eq
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    {x y : Kˣ}
    (hxy :
      (mrangeRestrict F) (y : K) = (mrangeRestrict F) (x : K)) :
    (uniformizerValueExponent F) hπ y =
      (uniformizerValueExponent F) hπ x

theorem eventually_uniformizerValueExponent_eq_mrangeRestrict
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (x : Kˣ) :
    letI : Valued K
        (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
      (mrangeRestrictValued F)
    ∀ᶠ y : Kˣ in 𝓝 x,
      (uniformizerValueExponent F) hπ y =
        (uniformizerValueExponent F) hπ x := by
  let Γ : Type v :=
    MonoidHom.mrange F.valuation.toMonoidWithZeroHom
  let : Valued K Γ := (mrangeRestrictValued F)
  have hxne : ((Valued.v : _root_.Valuation K Γ) (x : K) : Γ) ≠ 0 :=
    ((_root_.Valuation.ne_zero_iff
      (Valued.v : _root_.Valuation K Γ)).2 x.ne_zero)
  have hlocK :
      { y : K |
          (Valued.v : _root_.Valuation K Γ) y =
            (Valued.v : _root_.Valuation K Γ) (x : K) } ∈ 𝓝 (x : K) :=
    by
      have hxrestrictne :
          (Valued.v : _root_.Valuation K Γ).restrict (x : K) ≠ 0 :=
        ne_of_gt
          ((_root_.Valuation.restrict_pos_iff
            (Valued.v : _root_.Valuation K Γ) (x : K)).2
              (zero_lt_iff.mpr hxne))
      simpa only [_root_.Valuation.restrict_inj] using
        (Valued.isOpen_sphere K hxrestrictne).mem_nhds (by rfl)
  have hlocUnits :
      { y : Kˣ |
          (Valued.v : _root_.Valuation K Γ) (y : K) =
            (Valued.v : _root_.Valuation K Γ) (x : K) } ∈ 𝓝 x := by
    simpa [Set.preimage] using Units.continuous_val.continuousAt hlocK
  exact Filter.mem_of_superset hlocUnits fun y hy =>
    uniformizerValueExponent_eq_of_mrangeRestrict_eq
      F hπ (by
        apply Subtype.ext
        change F.valuation (y : K) = F.valuation (x : K)
        have hval := congrArg Subtype.val hy
        change F.valuation (y : K) = F.valuation (x : K) at hval
        exact hval)

theorem continuous_uniformizerValueExponent_mrangeRestrict
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K)) :
    letI : Valued K
        (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
      (mrangeRestrictValued F)
    Continuous (fun x : Kˣ => (uniformizerValueExponent F) hπ x) := by
  let Γ : Type v :=
    MonoidHom.mrange F.valuation.toMonoidWithZeroHom
  let : Valued K Γ := (mrangeRestrictValued F)
  rw [continuous_iff_continuousAt]
  intro x
  rw [continuousAt_def]
  intro s hs
  have hxmem : (uniformizerValueExponent F) hπ x ∈ s :=
    mem_of_mem_nhds hs
  exact
    Filter.mem_of_superset
      (eventually_uniformizerValueExponent_eq_mrangeRestrict
        F hπ x)
      (fun y hy => by
        change (uniformizerValueExponent F) hπ y ∈ s
        rw [hy]
        exact hxmem)

theorem continuous_fieldUnitsEquivRootsPrincipalUnitsUniformizer_symm_snd_mrangeRestrict
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K)) :
    letI : Valued K
        (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
      (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
    Continuous (fun x : Kˣ =>
      ((fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
        F hπ).symm x).2) := by
  let : Valued K
      (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
    (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
  have hval :
      Continuous (fun x : Kˣ => (uniformizerValueExponent F) hπ x) :=
    continuous_uniformizerValueExponent_mrangeRestrict
      F hπ
  have hofAdd :
      Continuous (fun n : ℤ => (Multiplicative.ofAdd n : Multiplicative ℤ)) :=
    continuous_of_discreteTopology
  exact (hofAdd.comp hval).congr fun x =>
    (fieldUnitsEquivRootsPrincipalUnitsUniformizer_symm_snd
      F hπ x).symm

theorem continuous_fieldUnitUniformizerUnitPart_mrangeRestrict
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K)) :
    letI : Valued K
        (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
      (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
    Continuous (fun x : Kˣ =>
      fieldUnitUniformizerUnitPart F hπ x) := by
  let : Valued K
      (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
    (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
  let ϖ : Kˣ := Units.mk0 (π : K) hπ.ne_zero
  have hval :
      Continuous (fun x : Kˣ => (uniformizerValueExponent F) hπ x) :=
    continuous_uniformizerValueExponent_mrangeRestrict
      F hπ
  have hpow :
      Continuous (fun n : ℤ => ϖ ^ (-n)) :=
    continuous_of_discreteTopology
  have hfield :
      Continuous (fun x : Kˣ =>
        x * ϖ ^ (-((uniformizerValueExponent F) hπ x))) :=
    continuous_id.mul (hpow.comp hval)
  rw [Units.continuous_iff]
  constructor
  · have hfieldK :
        Continuous (fun x : Kˣ =>
          ((x * ϖ ^ (-((uniformizerValueExponent F) hπ x)) : Kˣ) : K)) :=
      Units.continuous_val.comp hfield
    have hcoerced :
        Continuous (fun x : Kˣ =>
          ((fieldUnitUniformizerUnitPart F hπ x :
              F.valuationSubring) : K)) := by
      convert hfieldK using 1
      funext x
      calc
        _ = ((valuationSubringUnitFieldUnitHom F
              (fieldUnitUniformizerUnitPart F hπ x) : Kˣ) : K) :=
          (coe_valuationSubringUnitFieldUnitHom_apply F
            (fieldUnitUniformizerUnitPart F hπ x)).symm
        _ = _ :=
          congrArg (fun y : Kˣ => (y : K))
            (valuationSubringUnitFieldUnitHom_fieldUnitUniformizerUnitPart
              F hπ x)
    exact Continuous.subtype_mk hcoerced fun x =>
      (fieldUnitUniformizerUnitPart F hπ x :
        F.valuationSubring).2
  · have hfieldInvK :
        Continuous (fun x : Kˣ =>
          (((x * ϖ ^ (-((uniformizerValueExponent F) hπ x)) : Kˣ)⁻¹ :
              Kˣ) : K)) :=
      Units.continuous_val.comp hfield.inv
    have hcoercedInv :
        Continuous (fun x : Kˣ =>
          ((((fieldUnitUniformizerUnitPart F hπ x)⁻¹ :
              F.valuationSubringˣ) : F.valuationSubring) : K)) := by
      convert hfieldInvK using 1
      funext x
      calc
        _ = ((valuationSubringUnitFieldUnitHom F
              ((fieldUnitUniformizerUnitPart F hπ x)⁻¹) : Kˣ) : K) :=
          (coe_valuationSubringUnitFieldUnitHom_apply F
            ((fieldUnitUniformizerUnitPart F hπ x)⁻¹)).symm
        _ = (((valuationSubringUnitFieldUnitHom F
              (fieldUnitUniformizerUnitPart F hπ x))⁻¹ : Kˣ) : K) := by
          rw [map_inv]
        _ = _ :=
          congrArg (fun y : Kˣ => ((y⁻¹ : Kˣ) : K))
            (valuationSubringUnitFieldUnitHom_fieldUnitUniformizerUnitPart
              F hπ x)
    exact Continuous.subtype_mk hcoercedInv fun x =>
      (((fieldUnitUniformizerUnitPart F hπ x)⁻¹ :
          F.valuationSubringˣ) : F.valuationSubring).2

theorem isOpen_higherPrincipalUnitGroup_one_mrangeRestrict
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) :
    letI : Valued K
        (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
      (mrangeRestrictValued F)
    IsOpen (((higherPrincipalUnitGroup F) 1 : Set F.valuationSubringˣ)) := by
  let Γ : Type v :=
    MonoidHom.mrange F.valuation.toMonoidWithZeroHom
  let : Valued K Γ := (mrangeRestrictValued F)
  rw [isOpen_iff_mem_nhds]
  intro u hu
  have hu_lt :
      F.valuation (((u : F.valuationSubring) - 1 : F.valuationSubring) : K) < 1 := by
    have hu_mem :
        ((u : F.valuationSubring) - 1 : F.valuationSubring) ∈ F.maximalIdeal := by
      simpa [mem_iff] using hu
    simpa using
      (_root_.Valuation.mem_maximalIdeal_iff K F.valuation).1 hu_mem
  have htoK :
      Continuous (fun y : F.valuationSubringˣ =>
        ((y : F.valuationSubring) : K)) :=
    continuous_subtype_val.comp Units.continuous_val
  have hballK :
      { y : K |
          (Valued.v : _root_.Valuation K Γ)
            (y - ((u : F.valuationSubring) : K)) < (1 : Γ) } ∈
        𝓝 (((u : F.valuationSubring) : K)) := by
    rw [Valued.mem_nhds]
    refine ⟨1, ?_⟩
    intro y hy
    have hy' :
      (Valued.v : _root_.Valuation K Γ).restrict
          (y - ((u : F.valuationSubring) : K)) < 1 := by
      simpa only [Set.mem_ofPred_eq, Units.val_one] using hy
    have hval :
      (Valued.v : _root_.Valuation K Γ)
          (y - ((u : F.valuationSubring) : K)) < 1 :=
      (_root_.Valuation.restrict_lt_one_iff
        (Valued.v : _root_.Valuation K Γ)).1 hy'
    simpa only [Set.mem_ofPred_eq] using hval
  have hballUnits :
      { y : F.valuationSubringˣ |
          (Valued.v : _root_.Valuation K Γ)
            (((y : F.valuationSubring) : K) -
              ((u : F.valuationSubring) : K)) < (1 : Γ) } ∈
        𝓝 u := by
    simpa [Set.preimage] using htoK.continuousAt hballK
  exact Filter.mem_of_superset hballUnits fun y hy => by
    have hy_lt :
        F.valuation
            (((y : F.valuationSubring) : K) -
              ((u : F.valuationSubring) : K)) < 1 := by
      exact hy
    have hdecomp :
        (((y : F.valuationSubring) - 1 : F.valuationSubring) : K) =
          (((y : F.valuationSubring) : K) -
              ((u : F.valuationSubring) : K)) +
            (((u : F.valuationSubring) - 1 : F.valuationSubring) : K) := by
      change ((y : F.valuationSubring) : K) - 1 =
        (((y : F.valuationSubring) : K) - ((u : F.valuationSubring) : K)) +
          (((u : F.valuationSubring) : K) - 1)
      ring
    have hyu_lt :
        F.valuation (((y : F.valuationSubring) - 1 : F.valuationSubring) : K) < 1 := by
      rw [hdecomp]
      exact (F.valuation.map_add _ _).trans_lt (max_lt hy_lt hu_lt)
    have hy_mem :
        ((y : F.valuationSubring) - 1 : F.valuationSubring) ∈ F.maximalIdeal :=
      (_root_.Valuation.mem_maximalIdeal_iff K F.valuation).2 hyu_lt
    simpa [mem_iff] using hy_mem

theorem eventually_residueUnitHom_eq_mrangeRestrict
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
    (u : F.valuationSubringˣ) :
    letI : Valued K
        (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
      (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
    ∀ᶠ y : F.valuationSubringˣ in 𝓝 u,
      residueUnitHom F y =
        residueUnitHom F u := by
  let : Valued K
      (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
    (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
  let Γ : Type v :=
    MonoidHom.mrange F.valuation.toMonoidWithZeroHom
  have htoK :
      Continuous (fun y : F.valuationSubringˣ =>
        ((y : F.valuationSubring) : K)) :=
    continuous_subtype_val.comp Units.continuous_val
  have hballK :
      { y : K |
          (Valued.v : _root_.Valuation K Γ)
            (y - ((u : F.valuationSubring) : K)) < (1 : Γ) } ∈
        𝓝 (((u : F.valuationSubring) : K)) := by
    rw [Valued.mem_nhds]
    refine ⟨1, ?_⟩
    intro y hy
    simpa using hy
  have hballUnits :
      { y : F.valuationSubringˣ |
          (Valued.v : _root_.Valuation K Γ)
            (((y : F.valuationSubring) : K) -
              ((u : F.valuationSubring) : K)) < (1 : Γ) } ∈
        𝓝 u := by
    simpa [Set.preimage] using htoK.continuousAt hballK
  exact Filter.mem_of_superset hballUnits fun y hy => by
    have hy_lt :
        F.valuation
            (((y : F.valuationSubring) : K) -
              ((u : F.valuationSubring) : K)) < 1 := by
      exact hy
    have hdiff_mem :
        ((y : F.valuationSubring) - (u : F.valuationSubring) :
          F.valuationSubring) ∈ F.maximalIdeal :=
      (_root_.Valuation.mem_maximalIdeal_iff K F.valuation).2 (by
        simpa using hy_lt)
    have hres :
        F.residueMap (y : F.valuationSubring) =
          F.residueMap (u : F.valuationSubring) :=
      (ResidueField.residue_eq_residue_iff_sub_mem_maximalIdeal
        (R := F.valuationSubring) (y : F.valuationSubring)
        (u : F.valuationSubring)).2 hdiff_mem
    exact
      (residueUnitHom_eq_iff_residue_eq F y u).2 hres

theorem valuationSubringUnitsEquivRootsTimesPrincipalUnits_symm_fst_eq_residue
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField]
    (u : F.valuationSubringˣ) :
    ((valuationSubringUnitsEquivRootsTimesPrincipalUnits
      F).symm u).1 =
      (residueRootsOfUnityEquivResidueFieldUnits F).symm
        (residueUnitHom F u)

theorem valuationSubringUnitsEquivRootsTimesPrincipalUnits_symm_snd_eq
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField]
    (u : F.valuationSubringˣ) :
    (((valuationSubringUnitsEquivRootsTimesPrincipalUnits
      F).symm u).2 : F.valuationSubringˣ) =
      (((valuationSubringUnitsEquivRootsTimesPrincipalUnits
        F).symm u).1 : F.valuationSubringˣ)⁻¹ * u

theorem eventually_valuationSubringUnitsEquivRootsTimesPrincipalUnits_symm_fst_eq_mrangeRestrict
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField]
    (u : F.valuationSubringˣ) :
    letI : Valued K
        (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
      (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
    ∀ᶠ y : F.valuationSubringˣ in 𝓝 u,
      ((valuationSubringUnitsEquivRootsTimesPrincipalUnits
        F).symm y).1 =
        ((valuationSubringUnitsEquivRootsTimesPrincipalUnits
          F).symm u).1 := by
  let : Valued K
      (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
    (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
  exact
    (eventually_residueUnitHom_eq_mrangeRestrict
      F u).mono fun y hy => by
      rw [
        valuationSubringUnitsEquivRootsTimesPrincipalUnits_symm_fst_eq_residue
          F y,
        valuationSubringUnitsEquivRootsTimesPrincipalUnits_symm_fst_eq_residue
          F u,
        hy]

theorem continuous_valuationSubringUnitsEquivRootsTimesPrincipalUnits_symm_fst_mrangeRestrict
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField] :
    letI : Valued K
        (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
      (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
    Continuous (fun u : F.valuationSubringˣ =>
      ((valuationSubringUnitsEquivRootsTimesPrincipalUnits
        F).symm u).1) := by
  let : Valued K
      (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
    (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
  rw [continuous_iff_continuousAt]
  intro u
  rw [continuousAt_def]
  intro s hs
  have humem :
      ((valuationSubringUnitsEquivRootsTimesPrincipalUnits
        F).symm u).1 ∈ s :=
    mem_of_mem_nhds hs
  exact
    Filter.mem_of_superset
      (eventually_valuationSubringUnitsEquivRootsTimesPrincipalUnits_symm_fst_eq_mrangeRestrict
        F u)
      (fun y hy => by
        change
          ((valuationSubringUnitsEquivRootsTimesPrincipalUnits
            F).symm y).1 ∈ s
        rw [hy]
        exact humem)

theorem continuous_valuationSubringUnitFieldUnitHom_mrangeRestrict
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) :
    letI : Valued K
        (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
      (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
    Continuous (fun u : F.valuationSubringˣ =>
      valuationSubringUnitFieldUnitHom F u) := by
  let : Valued K
      (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
    (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
  have hsub : Continuous (fun x : F.valuationSubring => (x : K)) :=
    continuous_subtype_val
  rw [Units.continuous_iff]
  constructor
  · convert hsub.comp Units.continuous_val using 1
    funext u
    exact
      (coe_valuationSubringUnitFieldUnitHom_apply F u).symm
  · convert hsub.comp Units.continuous_coe_inv using 1
    funext u
    change
      (((valuationSubringUnitFieldUnitHom F u)⁻¹ : Kˣ) : K) =
        (((u⁻¹ : F.valuationSubringˣ) : F.valuationSubring) : K)
    rw [← map_inv]
    exact coe_valuationSubringUnitFieldUnitHom_apply F (u⁻¹)

theorem continuous_valuationSubringUnitsEquivRootsTimesPrincipalUnits_symm_snd_coe_mrangeRestrict
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField] :
    letI : Valued K
        (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
      (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
    Continuous (fun u : F.valuationSubringˣ =>
      (((valuationSubringUnitsEquivRootsTimesPrincipalUnits
        F).symm u).2 : F.valuationSubringˣ)) := by
  let : Valued K
      (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
    (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
  let E :=
    valuationSubringUnitsEquivRootsTimesPrincipalUnits
      F
  let rootToField : F.valuationSubringˣ → Kˣ := fun u =>
    valuationSubringUnitFieldUnitHom F
      (((E.symm u).1 : F.valuationSubringˣ))
  let unitToField : F.valuationSubringˣ → Kˣ := fun u =>
    valuationSubringUnitFieldUnitHom F u
  have hroot :
      Continuous (fun u : F.valuationSubringˣ => (E.symm u).1) :=
    continuous_valuationSubringUnitsEquivRootsTimesPrincipalUnits_symm_fst_mrangeRestrict
      F
  have hrootUnit :
      Continuous (fun u : F.valuationSubringˣ =>
        (((E.symm u).1 : F.valuationSubringˣ))) :=
    continuous_subtype_val.comp hroot
  have hrootField : Continuous rootToField :=
    (continuous_valuationSubringUnitFieldUnitHom_mrangeRestrict
      F).comp hrootUnit
  have hunitField : Continuous unitToField :=
    continuous_valuationSubringUnitFieldUnitHom_mrangeRestrict
      F
  have hpartField :
      Continuous (fun u : F.valuationSubringˣ =>
        (rootToField u)⁻¹ * unitToField u) :=
    hrootField.inv.mul hunitField
  rw [Units.continuous_iff]
  constructor
  · have hpartK :
        Continuous (fun u : F.valuationSubringˣ =>
          (((rootToField u)⁻¹ * unitToField u : Kˣ) : K)) :=
      Units.continuous_val.comp hpartField
    have hcoerced :
        Continuous (fun u : F.valuationSubringˣ =>
          ((((E.symm u).2 : F.valuationSubringˣ) :
            F.valuationSubring) : K)) := by
      convert hpartK using 1
      ext u
      have hsnd :=
        valuationSubringUnitsEquivRootsTimesPrincipalUnits_symm_snd_eq
          F u
      have hfield :=
        congrArg
          (fun a : F.valuationSubringˣ =>
            ((valuationSubringUnitFieldUnitHom F a : Kˣ) : K))
          hsnd
      simpa [rootToField, unitToField, map_mul] using hfield
    exact Continuous.subtype_mk hcoerced fun u =>
      (((E.symm u).2 : F.valuationSubringˣ) : F.valuationSubring).2
  · have hpartInvK :
        Continuous (fun u : F.valuationSubringˣ =>
          ((((rootToField u)⁻¹ * unitToField u : Kˣ)⁻¹ : Kˣ) : K)) :=
      Units.continuous_val.comp hpartField.inv
    have hcoercedInv :
        Continuous (fun u : F.valuationSubringˣ =>
          (((((E.symm u).2 : F.valuationSubringˣ)⁻¹ :
            F.valuationSubringˣ) : F.valuationSubring) : K)) := by
      convert hpartInvK using 1
      ext u
      have hsnd :=
        valuationSubringUnitsEquivRootsTimesPrincipalUnits_symm_snd_eq
          F u
      have hsndInv :
          (((E.symm u).2 : F.valuationSubringˣ)⁻¹ : F.valuationSubringˣ) =
            ((((E.symm u).1 : F.valuationSubringˣ)⁻¹ * u)⁻¹ :
              F.valuationSubringˣ) := by
        rw [hsnd]
      have hfieldInv :=
        congrArg
          (fun a : F.valuationSubringˣ =>
            ((valuationSubringUnitFieldUnitHom F a : Kˣ) : K))
          hsndInv
      change
        (((valuationSubringUnitFieldUnitHom F
          (((E.symm u).2 : F.valuationSubringˣ)))⁻¹ : Kˣ) : K) =
          ((((rootToField u)⁻¹ * unitToField u : Kˣ)⁻¹ : Kˣ) : K)
      simpa [E, rootToField, unitToField, map_mul] using hfieldInv
    exact Continuous.subtype_mk hcoercedInv fun u =>
      ((((E.symm u).2 : F.valuationSubringˣ)⁻¹ :
        F.valuationSubringˣ) : F.valuationSubring).2

theorem continuous_valuationSubringUnitsEquivRootsTimesPrincipalUnits_symm_snd_mrangeRestrict
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField] :
    letI : Valued K
        (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
      (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
    Continuous (fun u : F.valuationSubringˣ =>
      ((valuationSubringUnitsEquivRootsTimesPrincipalUnits
        F).symm u).2) := by
  let : Valued K
      (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
    (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
  let E :=
    valuationSubringUnitsEquivRootsTimesPrincipalUnits
      F
  exact
    Continuous.subtype_mk
      (continuous_valuationSubringUnitsEquivRootsTimesPrincipalUnits_symm_snd_coe_mrangeRestrict
        F)
      (fun u => (E.symm u).2.property)

theorem continuous_valuationSubringUnitsEquivRootsTimesPrincipalUnits_symm_mrangeRestrict
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField] :
    letI : Valued K
        (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
      (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
    Continuous (fun u : F.valuationSubringˣ =>
      (valuationSubringUnitsEquivRootsTimesPrincipalUnits
        F).symm u) := by
  let : Valued K
      (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
    (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
  have hfst :
      Continuous (fun u : F.valuationSubringˣ =>
        ((valuationSubringUnitsEquivRootsTimesPrincipalUnits
          F).symm u).1) :=
    continuous_valuationSubringUnitsEquivRootsTimesPrincipalUnits_symm_fst_mrangeRestrict
      F
  have hsnd :
      Continuous (fun u : F.valuationSubringˣ =>
        ((valuationSubringUnitsEquivRootsTimesPrincipalUnits
          F).symm u).2) :=
    continuous_valuationSubringUnitsEquivRootsTimesPrincipalUnits_symm_snd_mrangeRestrict
      F
  rw [continuous_iff_continuousAt]
  intro u
  rw [ContinuousAt, nhds_prod_eq]
  intro s hs
  rcases Filter.mem_prod_iff.1 hs with ⟨s₁, hs₁, s₂, hs₂, hsubset⟩
  have hpre₁ :
      {x : F.valuationSubringˣ |
        ((valuationSubringUnitsEquivRootsTimesPrincipalUnits
          F).symm x).1 ∈ s₁} ∈ 𝓝 u :=
    hfst.tendsto u hs₁
  have hpre₂ :
      {x : F.valuationSubringˣ |
        ((valuationSubringUnitsEquivRootsTimesPrincipalUnits
          F).symm x).2 ∈ s₂} ∈ 𝓝 u :=
    hsnd.tendsto u hs₂
  exact Filter.mem_of_superset (Filter.inter_mem hpre₁ hpre₂) fun x hx =>
    hsubset ⟨hx.1, hx.2⟩

theorem continuous_rootsPrincipalUnitUniformizerMulHom_mrangeRestrict
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K)) :
    letI : Valued K
        (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
      (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
    Continuous (fun z : fieldUnitDecompositionFactors F =>
      rootsPrincipalUnitUniformizerMulHom F
        (Units.mk0 (π : K) hπ.ne_zero) z) := by
  let : Valued K
      (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
    (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
  dsimp [rootsPrincipalUnitUniformizerMulHom]
  have hζ :
      Continuous fun z : fieldUnitDecompositionFactors F =>
        valuationSubringUnitFieldUnitHom F
          (z.1.1 : F.valuationSubringˣ) := by
    exact
      (continuous_valuationSubringUnitFieldUnitHom_mrangeRestrict
        F).comp
        (continuous_subtype_val.comp (continuous_fst.comp continuous_fst))
  have hp :
      Continuous fun z : fieldUnitDecompositionFactors F =>
        valuationSubringUnitFieldUnitHom F
          (z.1.2 : F.valuationSubringˣ) := by
    exact
      (continuous_valuationSubringUnitFieldUnitHom_mrangeRestrict
        F).comp
        (continuous_subtype_val.comp (continuous_snd.comp continuous_fst))
  have hn :
      Continuous fun z : fieldUnitDecompositionFactors F =>
        (Units.mk0 (π : K) hπ.ne_zero : Kˣ) ^ Multiplicative.toAdd z.2 := by
    exact continuous_of_discreteTopology.comp continuous_snd
  exact (hζ.mul hp).mul hn

theorem continuous_fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF_mrangeRestrict
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K)) :
    letI : Valued K
        (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
      (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
    Continuous (fun z : fieldUnitDecompositionFactors F =>
      fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
        F hπ z) := by
  let : Valued K
      (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
    (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
  simpa only
      [fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF_apply,
        rootsPrincipalUnitUniformizerMulHom_apply]
    using
      continuous_rootsPrincipalUnitUniformizerMulHom_mrangeRestrict
        F hπ

theorem continuous_fieldUnitsEquivRootsPrincipalUnitsUniformizer_symm_mrangeRestrict
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K)) :
    letI : Valued K
        (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
      (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
    Continuous (fun x : Kˣ =>
      (fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
        F hπ).symm x) := by
  let : Valued K
      (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
    (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
  let E :=
    fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
      F hπ
  have hfstComp :
      Continuous (fun x : Kˣ =>
        (valuationSubringUnitsEquivRootsTimesPrincipalUnits
          F).symm
          (fieldUnitUniformizerUnitPart F hπ x)) :=
    (continuous_valuationSubringUnitsEquivRootsTimesPrincipalUnits_symm_mrangeRestrict
      F).comp
      (continuous_fieldUnitUniformizerUnitPart_mrangeRestrict
        F hπ)
  have hfst :
      Continuous (fun x : Kˣ => (E.symm x).1) := by
    rw [continuous_iff_continuousAt]
    intro x
    rw [ContinuousAt]
    have hpoint (y : Kˣ) :
        (E.symm y).1 =
          (valuationSubringUnitsEquivRootsTimesPrincipalUnits F).symm
            (fieldUnitUniformizerUnitPart F hπ y) := by
      dsimp only [E]
      exact
        fieldUnitsEquivRootsPrincipalUnitsUniformizer_symm_fst_eq_unitPart
          F hπ y
    rw [hpoint x]
    exact Filter.Tendsto.congr'
      (Filter.Eventually.of_forall fun y => (hpoint y).symm)
      (hfstComp.tendsto x)
  have hsnd :
      Continuous (fun x : Kˣ => (E.symm x).2) := by
    simpa [E] using
      continuous_fieldUnitsEquivRootsPrincipalUnitsUniformizer_symm_snd_mrangeRestrict
        F hπ
  rw [continuous_iff_continuousAt]
  intro x
  rw [ContinuousAt, nhds_prod_eq]
  intro s hs
  rcases Filter.mem_prod_iff.1 hs with ⟨s₁, hs₁, s₂, hs₂, hsubset⟩
  have hpre₁ : {y : Kˣ | (E.symm y).1 ∈ s₁} ∈ 𝓝 x :=
    hfst.tendsto x hs₁
  have hpre₂ : {y : Kˣ | (E.symm y).2 ∈ s₂} ∈ 𝓝 x :=
    hsnd.tendsto x hs₂
  exact Filter.mem_of_superset (Filter.inter_mem hpre₁ hpre₂) fun y hy =>
    hsubset ⟨hy.1, hy.2⟩

def
  fieldUnitsContinuousMulEquivRootsPrincipalUnitsUniformizer_of_completeDVF_mrangeRestrict
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K)) :
    letI : Valued K
        (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
      (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
    fieldUnitDecompositionFactors F ≃ₜ* Kˣ := by
  letI : Valued K
      (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
    (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
  exact
    { fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
        F hπ with
      continuous_toFun :=
        continuous_fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF_mrangeRestrict
          F hπ
      continuous_invFun :=
        continuous_fieldUnitsEquivRootsPrincipalUnitsUniformizer_symm_mrangeRestrict
          F hπ }

theorem exists_roots_principalUnit_uniformizer_zpow_of_withZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)]
    {ϖ : Kˣ} (hϖ : v (ϖ : K) = WithZero.exp (-1 : ℤ)) (x : Kˣ) :
    let F : CompleteDVF K :=
      { ValueGroup := WithZero (Multiplicative ℤ)
        valuation := v
        instCompleteDiscrete := inferInstance }
    letI : Finite F.residueField := by
      change Finite (IsLocalRing.ResidueField v.valuationSubring)
      infer_instance
    ∃ ζ : residueRootsOfUnityGroup F,
    ∃ p : (LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1,
    ∃ n : ℤ,
      x =
        valuationSubringUnitFieldUnitHom F
            (ζ : F.valuationSubringˣ) *
          valuationSubringUnitFieldUnitHom F
            (p : F.valuationSubringˣ) *
          ϖ ^ n := by
  let F : CompleteDVF K :=
    { ValueGroup := WithZero (Multiplicative ℤ)
      valuation := v
      instCompleteDiscrete := inferInstance }
  let V : MultiplicativeIntegerValuation Kˣ :=
    MultiplicativeIntegerValuation.ofWithZeroValuation v
  have : Finite F.residueField := by
    change Finite (IsLocalRing.ResidueField v.valuationSubring)
    infer_instance
  have hzero : V.zeroSubgroup = F.valuation.valuationSubring.unitGroup := by
    simpa [F, V] using
      MultiplicativeIntegerValuation.ofWithZeroValuation_zeroSubgroup_eq_unitGroup
        (K := K) v
  have hϖV : V.IsUniformizer ϖ := by
    simpa [V] using
      MultiplicativeIntegerValuation.ofWithZeroValuation_isUniformizer_of_valuation_eq_exp_neg
        (K := K) v ϖ hϖ
  simpa [F, V] using
    exists_roots_principalUnit_uniformizer_zpow_of_zeroSubgroup_eq_unitGroup
      (F := F) V hzero hϖV x

theorem roots_principalUnit_uniformizer_zpow_eq_iff_of_withZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)]
    {ϖ : Kˣ} (hϖ : v (ϖ : K) = WithZero.exp (-1 : ℤ)) :
    let F : CompleteDVF K :=
      { ValueGroup := WithZero (Multiplicative ℤ)
        valuation := v
        instCompleteDiscrete := inferInstance }
    letI : Finite F.residueField := by
      change Finite (IsLocalRing.ResidueField v.valuationSubring)
      infer_instance
    ∀ (ζ η : residueRootsOfUnityGroup F)
      (p q : (higherPrincipalUnitGroup F) 1) (m n : ℤ),
        valuationSubringUnitFieldUnitHom F
              (ζ : F.valuationSubringˣ) *
            valuationSubringUnitFieldUnitHom F
              (p : F.valuationSubringˣ) *
            ϖ ^ m =
          valuationSubringUnitFieldUnitHom F
              (η : F.valuationSubringˣ) *
            valuationSubringUnitFieldUnitHom F
              (q : F.valuationSubringˣ) *
            ϖ ^ n ↔
          ζ = η ∧ p = q ∧ m = n := by
  let F : CompleteDVF K :=
    { ValueGroup := WithZero (Multiplicative ℤ)
      valuation := v
      instCompleteDiscrete := inferInstance }
  let V : MultiplicativeIntegerValuation Kˣ :=
    MultiplicativeIntegerValuation.ofWithZeroValuation v
  have : Finite F.residueField := by
    change Finite (IsLocalRing.ResidueField v.valuationSubring)
    infer_instance
  have hzero :
      ∀ y : Kˣ, y ∈ V.zeroSubgroup ↔
        ∃ u : F.valuationSubringˣ,
          valuationSubringUnitFieldUnitHom F u = y := by
    intro y
    exact
      mem_zeroSubgroup_iff_exists_valuationSubringUnitFieldUnitHom_eq
        (F := F) V
        (by
          simpa [F, V] using
            MultiplicativeIntegerValuation.ofWithZeroValuation_zeroSubgroup_eq_unitGroup
              (K := K) v)
        y
  have hϖV : V.IsUniformizer ϖ := by
    simpa [V] using
      MultiplicativeIntegerValuation.ofWithZeroValuation_isUniformizer_of_valuation_eq_exp_neg
        (K := K) v ϖ hϖ
  dsimp
  intro ζ η p q m n
  simpa [F, V] using
    higherPrincipalUnitGroup.roots_principalUnit_uniformizer_zpow_eq_iff
      F V hzero hϖV ζ η p q m n