PrincipalUnits.lean

theorem fieldPrincipalUnits_le_normSubgroup_cyclotomic_odd
    {k : ℕ} (hp2 : p ≠ 2)
    {L : Type} [Field L] [Algebra ℚ_[p] L]
    (zeta : L) (hzeta : IsPrimitiveRoot zeta (p ^ (k + 1)))
    (hgen : Algebra.adjoin ℚ_[p] ({zeta} : Set L) = ⊤) :
    LocalFieldTheory.fieldPrincipalUnits ℚ_[p] (k + 1) ≤ localNormSubgroup ℚ_[p] L

theorem padicPrimeUnit_mem_normSubgroup_cyclotomic
    {k : ℕ} {L : Type} [Field L] [Algebra ℚ_[p] L]
    (zeta : L) (hzeta : IsPrimitiveRoot zeta (p ^ (k + 1)))
    (hgen : Algebra.adjoin ℚ_[p] ({zeta} : Set L) = ⊤) :
    padicPrimeUnit p ∈ localNormSubgroup ℚ_[p] L

theorem uniformizerPrincipalSubgroup_le_normSubgroup_cyclotomic_odd
    {k : ℕ} (hp2 : p ≠ 2)
    {L : Type} [Field L] [Algebra ℚ_[p] L]
    (zeta : L) (hzeta : IsPrimitiveRoot zeta (p ^ (k + 1)))
    (hgen : Algebra.adjoin ℚ_[p] ({zeta} : Set L) = ⊤) :
    LocalFieldTheory.uniformizerPrincipalSubgroup ℚ_[p] (padicPrimeUnit p) 1 (k + 1) ≤
      localNormSubgroup ℚ_[p] L

theorem localNormSubgroup_eq_uniformizerPrincipalSubgroup_cyclotomicPrimePower_odd
    {k : ℕ} (hp2 : p ≠ 2)
    {L : Type} [Field L] [Algebra ℚ_[p] L]
    (zeta : L) (hzeta : IsPrimitiveRoot zeta (p ^ (k + 1)))
    (hgen : Algebra.adjoin ℚ_[p] ({zeta} : Set L) = ⊤) :
    localNormSubgroup ℚ_[p] L =
      LocalFieldTheory.uniformizerPrincipalSubgroup ℚ_[p] (padicPrimeUnit p) 1 (k + 1)

theorem minpoly_two_add_primitiveFourthRoot
    {L : Type*} [Field L] [Algebra ℚ_[2] L]
    (i : L) (hi : IsPrimitiveRoot i 4) :
    minpoly ℚ_[2] ((2 : L) + i) =
      (Polynomial.cyclotomic 4 ℚ_[2]).comp
        (Polynomial.X - Polynomial.C (2 : ℚ_[2]))

theorem cyclotomic_four_padic :
    Polynomial.cyclotomic 4 ℚ_[2] =
      Polynomial.X ^ 2 + 1

theorem norm_adjoin_two_add_primitiveFourthRoot
    {L : Type*} [Field L] [Algebra ℚ_[2] L]
    (i : L) (hi : IsPrimitiveRoot i 4) :
    Algebra.norm ℚ_[2]
        (IntermediateField.AdjoinSimple.gen ℚ_[2] ((2 : L) + i)) =
      (5 : ℚ_[2])

theorem norm_two_add_fourthRoot_cyclotomic_two
    (m : ℕ) {L : Type*} [Field L] [Algebra ℚ_[2] L]
    (zeta : L) (hzeta : IsPrimitiveRoot zeta (2 ^ (m + 2)))
    (hgen : Algebra.adjoin ℚ_[2] ({zeta} : Set L) = ⊤) :
    Algebra.norm ℚ_[2] ((2 : L) + zeta ^ (2 ^ m)) =
      (5 : ℚ_[2]) ^ (2 ^ m)

theorem padicInt_exists_two_power_root_of_mem_maximalIdeal_pow_add_two
    (m : ℕ) (z : ℤ_[2])
    (hz : z ∈ IsLocalRing.maximalIdeal ℤ_[2] ^ (m + 2)) :
    ∃ b : ℤ_[2],
      b ∈ IsLocalRing.maximalIdeal ℤ_[2] ^ 2 ∧
      (2 ^ m) • b = z

theorem padicDVR_logExp_level_two :
    (LocalFieldTheory.DiscreteValuationField.LocalField.ramificationIndexOfWithZeroValuation
          (LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicDVRValuation 2) : ℚ) /
        (((LocalFieldTheory.DiscreteValuationField.LocalField.ofWithZeroValuation
          (
            (open _root_.LocalFieldTheory.DiscreteValuationField.Examples.Qp in
              padicDVRValuation 2))).residueCharacteristic : ℚ) - 1) <
      (2 : ℚ)

theorem padicDVR_logExp_level_add_two (m : ℕ) :
    (LocalFieldTheory.DiscreteValuationField.LocalField.ramificationIndexOfWithZeroValuation
          (LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicDVRValuation 2) : ℚ) /
        (((LocalFieldTheory.DiscreteValuationField.LocalField.ofWithZeroValuation
          (
            (open _root_.LocalFieldTheory.DiscreteValuationField.Examples.Qp in
              padicDVRValuation 2))).residueCharacteristic : ℚ) - 1) <
      ((m + 2 : ℕ) : ℚ)

theorem padicDVR_higherPrincipalUnit_two_power
    (m : ℕ) :
    let v := LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicDVRValuation 2
    let F :=
      (open _root_.LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation in
        completeDVFOfWithZeroValuation v)
    ∀ u : LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F (m + 2),
      ∃ r : LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F 2,
        (r : F.valuationSubringˣ) ^ (2 ^ m) =
          (u : F.valuationSubringˣ) := by
  let : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
  let v := LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicDVRValuation 2
  let F :=
    (open _root_.LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation in
      completeDVFOfWithZeroValuation v)
  change ∀ u :
    (open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF in
      higherPrincipalUnitGroup F (m + 2)),
    ∃ r : LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F 2,
      (r : F.valuationSubringˣ) ^ (2 ^ m) =
        (u : F.valuationSubringˣ)
  have hv : Function.Surjective v :=
    (IsDiscreteValuationRing.maximalIdeal ℤ_[2]).valuation_surjective ℚ_[2]
  let E2 := expLogMulEquivOfWithZeroValuation v hv 2
    padicDVR_logExp_level_two
  let En := expLogMulEquivOfWithZeroValuation v hv (m + 2)
    (padicDVR_logExp_level_add_two m)
  let eO : ℤ_[2] ≃+* F.valuationSubring :=
    LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicIntEquivValuationSubring 2
  intro u
  let a : Multiplicative (F.maximalIdeal ^ (m + 2) : Ideal F.valuationSubring) :=
    En.symm u
  let z : ℤ_[2] := eO.symm (a.toAdd : F.valuationSubring)
  have hz : z ∈ IsLocalRing.maximalIdeal ℤ_[2] ^ (m + 2) := by
    apply (ringEquiv_mem_maximalIdeal_pow_iff eO (m + 2) z).1
    simp [z]
  obtain ⟨b, hb, hdb⟩ :=
    padicInt_exists_two_power_root_of_mem_maximalIdeal_pow_add_two m z hz
  have hbO : eO b ∈ F.maximalIdeal ^ 2 := by
    exact (ringEquiv_mem_maximalIdeal_pow_iff eO 2 b).2 hb
  let b2 : (F.maximalIdeal ^ 2 : Ideal F.valuationSubring) :=
    ⟨eO b, hbO⟩
  have hdbO : (2 ^ m) • (eO b) = (a.toAdd : F.valuationSubring) := by
    rw [← map_nsmul eO (2 ^ m) b, hdb]
    simp [z]
  let r :
    (open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF in
      higherPrincipalUnitGroup F 2) := E2 (Multiplicative.ofAdd b2)
  refine ⟨r, ?_⟩
  have hua : En a = u := En.apply_symm_apply u
  have hrpow :
      r ^ (2 ^ m) =
        E2 ((Multiplicative.ofAdd b2) ^ (2 ^ m)) := by
    change E2 (Multiplicative.ofAdd b2) ^ (2 ^ m) =
      E2 ((Multiplicative.ofAdd b2) ^ (2 ^ m))
    exact (map_pow E2 (Multiplicative.ofAdd b2) (2 ^ m)).symm
  change ((r ^ (2 ^ m) :
    (open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF in
      higherPrincipalUnitGroup F 2)) :
      F.valuationSubringˣ) = (u : F.valuationSubringˣ)
  rw [hrpow, ← hua]
  apply Units.ext
  apply Subtype.ext
  have hleft := expLogMulEquivOfWithZeroValuation_fieldVal v hv 2
    padicDVR_logExp_level_two
    ((Multiplicative.ofAdd b2) ^ (2 ^ m))
  have hright := expLogMulEquivOfWithZeroValuation_fieldVal v hv (m + 2)
    (padicDVR_logExp_level_add_two m) a
  have hleft' :
      ((((E2 ((Multiplicative.ofAdd b2) ^ (2 ^ m)) :
          (open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF in
            higherPrincipalUnitGroup F 2)) : F.valuationSubringˣ) :
          F.valuationSubring) : ℚ_[2]) =
        (open _root_.LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation in
          expSeriesFieldOfWithZeroValuation
            v ((((Multiplicative.ofAdd b2) ^ (2 ^ m)).toAdd :
              F.valuationSubring) : ℚ_[2])
              (fun q =>
                Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero q))) := by
    exact hleft
  have hright' :
      ((((En a :
        (open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF in
          higherPrincipalUnitGroup F (m + 2))) : F.valuationSubringˣ) :
          F.valuationSubring) : ℚ_[2]) =
        (open _root_.LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation in
          expSeriesFieldOfWithZeroValuation
            v ((a.toAdd : F.valuationSubring) : ℚ_[2])
              (fun q =>
                Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero q))) := by
    exact hright
  rw [hleft', hright']
  congr 2

def padicDVR_five :
    letI : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
    let F := LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF 2
    LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F 2 := by
  letI : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
  let F := LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF 2
  let eO : ℤ_[2] ≃+* F.valuationSubring :=
    LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicIntEquivValuationSubring 2
  have hfive : IsUnit (5 : ℤ_[2]) := by
    rw [PadicInt.isUnit_iff]
    exact PadicInt.norm_natCast_eq_one_iff.mpr (by norm_num)
  let fiveZ : ℤ_[2]ˣ := hfive.unit
  let fiveO : F.valuationSubringˣ := Units.mapEquiv eO.toMulEquiv fiveZ
  refine ⟨fiveO, ?_⟩
  rw [LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.mem_iff]
  have hval : (fiveO : F.valuationSubring) = eO (5 : ℤ_[2]) := by
    simp [fiveO, fiveZ]
  rw [hval, ← map_one eO, ← map_sub]
  apply (ringEquiv_mem_maximalIdeal_pow_iff eO 2 ((5 : ℤ_[2]) - 1)).2
  rw [PadicInt.maximalIdeal_eq_span_p, Ideal.span_singleton_pow,
    Ideal.mem_span_singleton]
  refine ⟨1, ?_⟩
  norm_num

theorem padicDVR_five_val :
    letI : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
    let F := LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF 2
    ((((padicDVR_five :
      (open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF in
        higherPrincipalUnitGroup F 2)) :
      F.valuationSubringˣ) : F.valuationSubring) : ℚ_[2]) = 5 := by
  let : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
  let F := LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF 2
  let eO : ℤ_[2] ≃+* F.valuationSubring :=
    LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicIntEquivValuationSubring 2
  change (((Units.mapEquiv eO.toMulEquiv _ : F.valuationSubringˣ) :
    F.valuationSubring) : ℚ_[2]) = 5
  rfl

theorem padicDVR_U2_split (u :
    letI : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
    let F := LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF 2
    LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F 2) :
    letI : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
    let F := LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF 2
    (u : F.valuationSubringˣ) ∈
      (open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF in
        higherPrincipalUnitGroup F 3) ∨
      (u : F.valuationSubringˣ) /
          (padicDVR_five :
            (open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF in
              higherPrincipalUnitGroup F 2)) ∈
        LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F 3 := by
  let : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
  let F := LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF 2
  let eO : ℤ_[2] ≃+* F.valuationSubring :=
    LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicIntEquivValuationSubring 2
  let x : ℤ_[2] := eO.symm (((u : F.valuationSubringˣ) : F.valuationSubring))
  have hu2 :
      ((u : F.valuationSubringˣ) : F.valuationSubring) - 1 ∈
        F.maximalIdeal ^ 2 :=
    (LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.mem_iff
      F 2 (u : F.valuationSubringˣ)).1 u.property
  have hx2 : x - 1 ∈ IsLocalRing.maximalIdeal ℤ_[2] ^ 2 := by
    apply (ringEquiv_mem_maximalIdeal_pow_iff eO 2 (x - 1)).1
    rw [map_sub, map_one]
    simpa [x] using hu2
  rw [PadicInt.maximalIdeal_eq_span_p, Ideal.span_singleton_pow,
    Ideal.mem_span_singleton] at hx2
  obtain ⟨c, hc⟩ := hx2
  have hcmod : PadicInt.toZMod c = 0 ∨ PadicInt.toZMod c = 1 := by
    have hlt := ZMod.val_lt (PadicInt.toZMod c)
    have hle : (PadicInt.toZMod c).val ≤ 1 := by omega
    rcases Nat.le_one_iff_eq_zero_or_eq_one.1 hle with h | h
    · left
      calc
        PadicInt.toZMod c = ((PadicInt.toZMod c).val : ZMod 2) :=
          (ZMod.natCast_zmod_val _).symm
        _ = 0 := by rw [h]; norm_num
    · right
      calc
        PadicInt.toZMod c = ((PadicInt.toZMod c).val : ZMod 2) :=
          (ZMod.natCast_zmod_val _).symm
        _ = 1 := by rw [h]; norm_num
  rcases hcmod with hc0 | hc1
  · left
    rw [LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.mem_iff]
    have hxe : eO x =
        ((u : F.valuationSubringˣ) : F.valuationSubring) := by simp [x]
    rw [← hxe, ← map_one eO, ← map_sub]
    apply (ringEquiv_mem_maximalIdeal_pow_iff eO 3 (x - 1)).2
    rw [PadicInt.maximalIdeal_eq_span_p, Ideal.span_singleton_pow,
      Ideal.mem_span_singleton]
    have hcm : c ∈ IsLocalRing.maximalIdeal ℤ_[2] := by
      rw [← PadicInt.ker_toZMod, RingHom.mem_ker]
      exact hc0
    rw [PadicInt.maximalIdeal_eq_span_p, Ideal.mem_span_singleton] at hcm
    obtain ⟨d, hd⟩ := hcm
    refine ⟨d, ?_⟩
    calc
      x - 1 = (2 : ℤ_[2]) ^ 2 * c := hc
      _ = (2 : ℤ_[2]) ^ 3 * d := by rw [hd]; ring
  · right
    have hcsub : c - 1 ∈ IsLocalRing.maximalIdeal ℤ_[2] := by
      rw [← PadicInt.ker_toZMod, RingHom.mem_ker]
      rw [map_sub, map_one, hc1]
      change (1 : ZMod 2) - 1 = 0
      decide
    rw [PadicInt.maximalIdeal_eq_span_p, Ideal.mem_span_singleton] at hcsub
    obtain ⟨d, hd⟩ := hcsub
    have hx5 : x - 5 ∈ IsLocalRing.maximalIdeal ℤ_[2] ^ 3 := by
      rw [PadicInt.maximalIdeal_eq_span_p, Ideal.span_singleton_pow,
        Ideal.mem_span_singleton]
      refine ⟨d, ?_⟩
      calc
        x - 5 = (x - 1) - 4 := by ring
        _ = (2 : ℤ_[2]) ^ 2 * (c - 1) := by rw [hc]; ring
        _ = (2 : ℤ_[2]) ^ 3 * d := by rw [hd]; ring
    have hdiff :
        ((u : F.valuationSubringˣ) : F.valuationSubring) -
            (((padicDVR_five :
              (open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF in
                higherPrincipalUnitGroup F 2)) :
              F.valuationSubringˣ) : F.valuationSubring) ∈
          F.maximalIdeal ^ 3 := by
      have hxe : eO x =
          ((u : F.valuationSubringˣ) : F.valuationSubring) := by
        simp [x]
      have hefive : eO (5 : ℤ_[2]) =
          (((padicDVR_five :
              LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F 2) :
            F.valuationSubringˣ) : F.valuationSubring) := by
        apply Subtype.ext
        rfl
      have hmapped :=
        (ringEquiv_mem_maximalIdeal_pow_iff eO 3 (x - 5)).2 hx5
      rw [map_sub, hxe, hefive] at hmapped
      exact hmapped
    have hq :
        (open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup in
          quotientUnitHom F 3
              (u : F.valuationSubringˣ)) =
          (open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF in
            higherPrincipalUnitGroup.quotientUnitHom F 3
              ((padicDVR_five :
                (open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF in
                  higherPrincipalUnitGroup F 2)) :
                F.valuationSubringˣ)) := by
      apply Units.ext
      exact (Ideal.Quotient.mk_eq_mk_iff_sub_mem
        (I := F.maximalIdeal ^ 3)
        (((u : F.valuationSubringˣ) : F.valuationSubring))
        ((((padicDVR_five :
          (open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF in
            higherPrincipalUnitGroup F 2)) :
          F.valuationSubringˣ) : F.valuationSubring))).2 hdiff
    rw [←
      (open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup in
        quotientUnitHom_ker_eq F 3),
      MonoidHom.mem_ker]
    rw [map_div, hq]
    exact div_self' _

theorem padicDVR_U2_square_class
    (u :
      letI : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
      let F := LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF 2
      LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F 2) :
    letI : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
    let F := LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF 2
    ∃ r : LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F 2,
      (u : F.valuationSubringˣ) = (r : F.valuationSubringˣ) ^ 2 ∨
      (u : F.valuationSubringˣ) =
        (padicDVR_five :
          (open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF in
            higherPrincipalUnitGroup F 2)) *
          (r : F.valuationSubringˣ) ^ 2 := by
  let : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
  let F := LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF 2
  let F' :=
    (open _root_.LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation in
      completeDVFOfWithZeroValuation
        (LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicDVRValuation 2))
  have hroot :
      ∀ w : LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F 3,
        ∃ r : LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F 2,
          (r : F.valuationSubringˣ) ^ 2 =
            (w : F.valuationSubringˣ) := by
    change ∀ w :
        LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F' 3,
      ∃ r :
          LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F' 2,
        (r : F'.valuationSubringˣ) ^ 2 = (w : F'.valuationSubringˣ)
    simpa using (padicDVR_higherPrincipalUnit_two_power 1)
  rcases padicDVR_U2_split u with hu | hu
  · let w :
    (open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF in
      higherPrincipalUnitGroup F 3) := ⟨u, hu⟩
    obtain ⟨r, hr⟩ := hroot w
    exact ⟨r, Or.inl hr.symm⟩
  · let w : LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F 3 :=
      ⟨(u : F.valuationSubringˣ) /
          (padicDVR_five :
            (open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF in
              higherPrincipalUnitGroup F 2)), hu⟩
    obtain ⟨r, hr⟩ := hroot w
    have hr' : (r : F.valuationSubringˣ) ^ 2 =
        (u : F.valuationSubringˣ) /
          (padicDVR_five :
            (open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF in
              higherPrincipalUnitGroup F 2)) := by
      simpa [w] using hr
    refine ⟨r, Or.inr ?_⟩
    calc
      (u : F.valuationSubringˣ) =
          (padicDVR_five :
            (open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF in
              higherPrincipalUnitGroup F 2)) *
            ((u : F.valuationSubringˣ) /
              (padicDVR_five :
                (open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF in
                  higherPrincipalUnitGroup F 2))) := by
                symm
                rw [mul_comm]
                exact div_mul_cancel _ _
      _ = (padicDVR_five :
        (open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF in
          higherPrincipalUnitGroup F 2)) *
            (r : F.valuationSubringˣ) ^ 2 := by rw [← hr']

theorem fieldPrincipalUnits_le_normSubgroup_cyclotomic_two_zero
    {L : Type} [Field L] [Algebra ℚ_[2] L]
    (zeta : L) (hzeta : IsPrimitiveRoot zeta (2 ^ 1))
    (hgen : Algebra.adjoin ℚ_[2] ({zeta} : Set L) = ⊤) :
    LocalFieldTheory.fieldPrincipalUnits ℚ_[2] 1 ≤ localNormSubgroup ℚ_[2] L

theorem fieldPrincipalUnits_le_normSubgroup_cyclotomic_two_succ
    (m : ℕ) {L : Type} [Field L] [Algebra ℚ_[2] L]
    (zeta : L) (hzeta : IsPrimitiveRoot zeta (2 ^ (m + 2)))
    (hgen : Algebra.adjoin ℚ_[2] ({zeta} : Set L) = ⊤) :
    LocalFieldTheory.fieldPrincipalUnits ℚ_[2] (m + 2) ≤ localNormSubgroup ℚ_[2] L

theorem fieldPrincipalUnits_le_normSubgroup_cyclotomic_two
    (k : ℕ) {L : Type} [Field L] [Algebra ℚ_[2] L]
    (zeta : L) (hzeta : IsPrimitiveRoot zeta (2 ^ (k + 1)))
    (hgen : Algebra.adjoin ℚ_[2] ({zeta} : Set L) = ⊤) :
    LocalFieldTheory.fieldPrincipalUnits ℚ_[2] (k + 1) ≤ localNormSubgroup ℚ_[2] L

theorem uniformizerPrincipalSubgroup_le_normSubgroup_cyclotomic_two
    (k : ℕ) {L : Type} [Field L] [Algebra ℚ_[2] L]
    (zeta : L) (hzeta : IsPrimitiveRoot zeta (2 ^ (k + 1)))
    (hgen : Algebra.adjoin ℚ_[2] ({zeta} : Set L) = ⊤) :
    LocalFieldTheory.uniformizerPrincipalSubgroup ℚ_[2] (padicPrimeUnit 2) 1 (k + 1) ≤
      localNormSubgroup ℚ_[2] L

theorem localNormSubgroup_eq_uniformizerPrincipalSubgroup_cyclotomicPrimePower_two
    {k : ℕ} {L : Type} [Field L] [Algebra ℚ_[2] L]
    (zeta : L) (hzeta : IsPrimitiveRoot zeta (2 ^ (k + 1)))
    (hgen : Algebra.adjoin ℚ_[2] ({zeta} : Set L) = ⊤) :
    localNormSubgroup ℚ_[2] L =
      LocalFieldTheory.uniformizerPrincipalSubgroup ℚ_[2]
        (padicPrimeUnit 2) 1 (k + 1)

theorem localNormSubgroup_eq_uniformizerPrincipalSubgroup_cyclotomicPrimePower
    {k : ℕ} {L : Type} [Field L] [Algebra ℚ_[p] L]
    (zeta : L) (hzeta : IsPrimitiveRoot zeta (p ^ (k + 1)))
    (hgen : Algebra.adjoin ℚ_[p] ({zeta} : Set L) = ⊤) :
    localNormSubgroup ℚ_[p] L =
      LocalFieldTheory.uniformizerPrincipalSubgroup ℚ_[p]
        (padicPrimeUnit p) 1 (k + 1)