PrincipalUnitExp.lean

def principalUnitExpSeriesOfWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime] (x : K)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hvx : v x < WithZero.exp (-1 : ℤ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1 := by
  let F : CompleteDVF.{u, 0} K := completeDVFOfWithZeroValuation v
  have hlt :
      v (expSeriesFieldOfWithZeroValuation v x hnK - 1) <
        (1 : WithZero (Multiplicative ℤ)) :=
    valuation_expSeriesField_sub_one_lt_one_ofWithZeroValuation_of_lt_exp_neg_one
      (v := v) (p := p) x hnK hnval hvx hcomplete
  let a : F.valuationSubring :=
    ⟨expSeriesFieldOfWithZeroValuation v x hnK - 1,
      (CompleteDVF.mem_valuationSubring_iff F
        (expSeriesFieldOfWithZeroValuation v x hnK - 1)).2
        (by
          change v (expSeriesFieldOfWithZeroValuation v x hnK - 1) ≤ 1
          exact le_of_lt hlt)⟩
  have ha : a ∈ F.maximalIdeal ^ 1 := by
    have ha0 : a ∈ F.maximalIdeal := by
      rw [CompleteDVF.mem_maximalIdeal_iff]
      change v (expSeriesFieldOfWithZeroValuation v x hnK - 1) < 1
      exact hlt
    simpa [pow_one] using ha0
  exact
    CompleteDVF.higherPrincipalUnitGroup.principalUnitOneAddOfMemPowSubgroup
      F (n := 1) le_rfl a ha

def principalUnitExpSeriesOfMaximalIdealPowOfWithZeroValuationScaled
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime] (e n : ℕ)
    {π : (completeDVFOfWithZeroValuation v).valuationSubring}
    (hπ : v.IsUniformizer (π : K))
    (hπval : v (π : K) = WithZero.exp (-1 : ℤ))
    (hn : 1 ≤ n)
    (hlevel : (e : ℚ) / ((p : ℚ) - 1) < (n : ℚ))
    (hnK : ∀ m : ℕ, (((m.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ m : ℕ,
      v (((m.factorial : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p m.factorial : ℤ))))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K)
    (a :
      ((completeDVFOfWithZeroValuation v).maximalIdeal ^ n :
        Ideal (completeDVFOfWithZeroValuation v).valuationSubring)) :
    (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) n := by
  let F : CompleteDVF.{u, 0} K := completeDVFOfWithZeroValuation v
  let x : K := ((a : F.valuationSubring) : K)
  have hxthreshold :
      ∀ hx : x ≠ 0,
        (e : ℚ) / ((p : ℚ) - 1) <
          ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℚ) := by
    intro hx
    have hge :
        (n : ℤ) ≤
          (ofWithZeroValuation v).val (Units.mk0 x hx) := by
      simpa [F, x] using
        ofWithZeroValuation_val_ge_of_mem_maximalIdeal_pow
          (v := v) (π := π) hπ hπval n
          (a := (a : F.valuationSubring)) a.property hx
    exact lt_of_lt_of_le hlevel (by exact_mod_cast hge)
  have hbLe :
      v (expSeriesFieldOfWithZeroValuation v x hnK - 1) ≤
        (1 : WithZero (Multiplicative ℤ)) := by
    by_cases hx : x = 0
    · simp [x, hx]
    · have hv :
          v (expSeriesFieldOfWithZeroValuation v x hnK - 1) = v x :=
        valuation_expSeriesField_sub_one_eq_self_ofWithZeroValuation_scaled_of_threshold
          (v := v) (p := p) e (x := x) hx hnK hnval
          (hxthreshold hx) hcomplete
      have hxInt : v x ≤ (1 : WithZero (Multiplicative ℤ)) := by
        have hxMem : x ∈ F.valuation.valuationSubring := by
          change ((a : F.valuationSubring) : K) ∈ F.valuation.valuationSubring
          exact (a : F.valuationSubring).property
        have hxBound := (CompleteDVF.mem_valuationSubring_iff F x).1 hxMem
        change v x ≤ 1 at hxBound
        exact hxBound
      simpa [hv] using hxInt
  let b : F.valuationSubring :=
    ⟨expSeriesFieldOfWithZeroValuation v x hnK - 1,
      (CompleteDVF.mem_valuationSubring_iff F
        (expSeriesFieldOfWithZeroValuation v x hnK - 1)).2
        (by
          change v (expSeriesFieldOfWithZeroValuation v x hnK - 1) ≤ 1
          exact hbLe)⟩
  have hbmem : b ∈ F.maximalIdeal ^ n := by
    apply
      mem_maximalIdeal_pow_ofWithZeroValuation_val_ge
        (v := v) (π := π) hπ hπval n b
    intro hbne
    by_cases hx : x = 0
    · have hbzero : (b : K) = 0 := by
        simp [b, x, hx]
      exact False.elim (hbne hbzero)
    · have hv :
          v (b : K) = v x := by
        simpa [b] using
          valuation_expSeriesField_sub_one_eq_self_ofWithZeroValuation_scaled_of_threshold
            (v := v) (p := p) e (x := x) hx hnK hnval
            (hxthreshold hx) hcomplete
      have hge :
          (n : ℤ) ≤
            (ofWithZeroValuation v).val (Units.mk0 x hx) := by
        simpa [F, x] using
          ofWithZeroValuation_val_ge_of_mem_maximalIdeal_pow
            (v := v) (π := π) hπ hπval n
            (a := (a : F.valuationSubring)) a.property hx
      have hvaleq :
          (ofWithZeroValuation v).val (Units.mk0 (b : K) hbne) =
            (ofWithZeroValuation v).val (Units.mk0 x hx) := by
        simp [ofWithZeroValuation_val, hv]
      rw [hvaleq]
      exact hge
  exact
    CompleteDVF.higherPrincipalUnitGroup.principalUnitOneAddOfMemPowSubgroup
      F hn b hbmem

theorem principalUnitExpSeries_maximalIdealPow_val_ofWithZeroValuationScaled
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime] (e n : ℕ)
    {π : (completeDVFOfWithZeroValuation v).valuationSubring}
    (hπ : v.IsUniformizer (π : K))
    (hπval : v (π : K) = WithZero.exp (-1 : ℤ))
    (hn : 1 ≤ n)
    (hlevel : (e : ℚ) / ((p : ℚ) - 1) < (n : ℚ))
    (hnK : ∀ m : ℕ, (((m.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ m : ℕ,
      v (((m.factorial : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p m.factorial : ℤ))))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K)
    (a :
      ((completeDVFOfWithZeroValuation v).maximalIdeal ^ n :
        Ideal (completeDVFOfWithZeroValuation v).valuationSubring)) :
    let F : CompleteDVF.{u, 0} K := completeDVFOfWithZeroValuation v
    ((((principalUnitExpSeriesOfMaximalIdealPowOfWithZeroValuationScaled
        (v := v) (p := p) e n (π := π) hπ hπval hn hlevel
        hnK hnval hcomplete a : (CompleteDVF.higherPrincipalUnitGroup F) n) :
        F.valuationSubringˣ) : F.valuationSubring) : K) =
      expSeriesFieldOfWithZeroValuation v
        (((a : F.valuationSubring) : K)) hnK := by
  simp [principalUnitExpSeriesOfMaximalIdealPowOfWithZeroValuationScaled]

theorem principalUnitExpSeries_maximalIdealPow_add_eq_mul_ofWithZeroValuationScaled
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime] (e n : ℕ)
    {π : (completeDVFOfWithZeroValuation v).valuationSubring}
    (hπ : v.IsUniformizer (π : K))
    (hπval : v (π : K) = WithZero.exp (-1 : ℤ))
    (hn : 1 ≤ n)
    (hlevel : (e : ℚ) / ((p : ℚ) - 1) < (n : ℚ))
    (hnK : ∀ m : ℕ, (((m.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ m : ℕ,
      v (((m.factorial : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p m.factorial : ℤ))))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K)
    (a b :
      ((completeDVFOfWithZeroValuation v).maximalIdeal ^ n :
        Ideal (completeDVFOfWithZeroValuation v).valuationSubring)) :
    principalUnitExpSeriesOfMaximalIdealPowOfWithZeroValuationScaled
        (v := v) (p := p) e n (π := π) hπ hπval hn hlevel
        hnK hnval hcomplete (a + b) =
      principalUnitExpSeriesOfMaximalIdealPowOfWithZeroValuationScaled
          (v := v) (p := p) e n (π := π) hπ hπval hn hlevel
          hnK hnval hcomplete a *
        principalUnitExpSeriesOfMaximalIdealPowOfWithZeroValuationScaled
          (v := v) (p := p) e n (π := π) hπ hπval hn hlevel
          hnK hnval hcomplete b := by
  let F : CompleteDVF.{u, 0} K := completeDVFOfWithZeroValuation v
  let x : K := ((a : F.valuationSubring) : K)
  let y : K := ((b : F.valuationSubring) : K)
  have hlevelR : (e : ℝ) / ((p : ℝ) - 1) < (n : ℝ) := by
    exact_mod_cast hlevel
  have hxthreshold : ∀ hx : x ≠ 0,
      (e : ℝ) / ((p : ℝ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℝ) := by
    intro hx
    have hge :
        (n : ℤ) ≤
          (ofWithZeroValuation v).val (Units.mk0 x hx) := by
      simpa [F, x] using
        ofWithZeroValuation_val_ge_of_mem_maximalIdeal_pow
          (v := v) (π := π) hπ hπval n
          (a := (a : F.valuationSubring)) a.property hx
    exact lt_of_lt_of_le hlevelR (by exact_mod_cast hge)
  have hythreshold : ∀ hy : y ≠ 0,
      (e : ℝ) / ((p : ℝ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 y hy) : ℝ) := by
    intro hy
    have hge :
        (n : ℤ) ≤
          (ofWithZeroValuation v).val (Units.mk0 y hy) := by
      simpa [F, y] using
        ofWithZeroValuation_val_ge_of_mem_maximalIdeal_pow
          (v := v) (π := π) hπ hπval n
          (a := (b : F.valuationSubring)) b.property hy
    exact lt_of_lt_of_le hlevelR (by exact_mod_cast hge)
  have hfield :
      expSeriesFieldOfWithZeroValuation v (x + y) hnK =
        expSeriesFieldOfWithZeroValuation v x hnK *
          expSeriesFieldOfWithZeroValuation v y hnK :=
    expSeriesField_add_eq_mul_ofWithZeroValuation_scaled_of_threshold
      (v := v) (p := p) e x y hnK hnval hxthreshold hythreshold
      hcomplete
  apply Subtype.ext
  apply Units.ext
  apply Subtype.ext
  simpa [F, x, y] using hfield

def principalUnitSubOneOfWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (u : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1) : K

theorem principalUnitSubOne_expSeries_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime] (x : K)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hvx : v x < WithZero.exp (-1 : ℤ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    principalUnitSubOneOfWithZeroValuation v
      (principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p) x hnK hnval hvx hcomplete) =
      expSeriesFieldOfWithZeroValuation v x hnK - 1 := by
  simp [principalUnitSubOneOfWithZeroValuation,
    principalUnitExpSeriesOfWithZeroValuation]

theorem principalUnitSubOne_expSeries_valuation_eq_self_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime] {x : K} (hx : x ≠ 0)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hvx : v x < WithZero.exp (-1 : ℤ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    v (principalUnitSubOneOfWithZeroValuation v
      (principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p) x hnK hnval hvx hcomplete)) =
      v x := by
  rw [principalUnitSubOne_expSeries_ofWithZeroValuation]
  exact
    valuation_expSeriesField_sub_one_eq_self_ofWithZeroValuation_of_lt_exp_neg_one
      (v := v) (p := p) (x := x) hx hnK hnval hvx hcomplete

theorem principalUnitSubOne_expSeries_ne_zero_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime] {x : K} (hx : x ≠ 0)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hvx : v x < WithZero.exp (-1 : ℤ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    principalUnitSubOneOfWithZeroValuation v
      (principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p) x hnK hnval hvx hcomplete) ≠ 0 := by
  rw [principalUnitSubOne_expSeries_ofWithZeroValuation]
  exact
    expSeriesField_sub_one_ne_zero_ofWithZeroValuation_of_lt_exp_neg_one
      (v := v) (p := p) (x := x) hx hnK hnval hvx hcomplete

theorem principalUnitSubOne_expSeries_ofWithZeroValuation_val_eq_self
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime] {x : K} (hx : x ≠ 0)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hvx : v x < WithZero.exp (-1 : ℤ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K)
    (hne : principalUnitSubOneOfWithZeroValuation v
      (principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p) x hnK hnval hvx hcomplete) ≠ 0) :
    (ofWithZeroValuation v).val
        (Units.mk0
          (principalUnitSubOneOfWithZeroValuation v
            (principalUnitExpSeriesOfWithZeroValuation
              (v := v) (p := p) x hnK hnval hvx hcomplete)) hne) =
      (ofWithZeroValuation v).val (Units.mk0 x hx) := by
  exact
    ofWithZeroValuation_val_eq_of_valuation_eq v
      (principalUnitSubOne_expSeries_valuation_eq_self_ofWithZeroValuation
        (v := v) (p := p) (x := x) hx hnK hnval hvx hcomplete)

theorem principalUnitSubOne_expSeries_threshold_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime] {x : K} (hx : x ≠ 0)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hvx : v x < WithZero.exp (-1 : ℤ))
    (hthreshold :
      1 / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℚ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K)
    (hne : principalUnitSubOneOfWithZeroValuation v
      (principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p) x hnK hnval hvx hcomplete) ≠ 0) :
    1 / ((p : ℚ) - 1) <
      ((ofWithZeroValuation v).val
        (Units.mk0
          (principalUnitSubOneOfWithZeroValuation v
            (principalUnitExpSeriesOfWithZeroValuation
              (v := v) (p := p) x hnK hnval hvx hcomplete)) hne) : ℚ) := by
  have hval :
      (ofWithZeroValuation v).val
          (Units.mk0
            (principalUnitSubOneOfWithZeroValuation v
              (principalUnitExpSeriesOfWithZeroValuation
                (v := v) (p := p) x hnK hnval hvx hcomplete)) hne) =
        (ofWithZeroValuation v).val (Units.mk0 x hx) :=
    principalUnitSubOne_expSeries_ofWithZeroValuation_val_eq_self
      (v := v) (p := p) (x := x) hx hnK hnval hvx hcomplete hne
  rw [hval]
  exact hthreshold

theorem principalUnitExpSeries_val_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime] (x : K)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hvx : v x < WithZero.exp (-1 : ℤ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    let F : CompleteDVF.{u, 0} K := completeDVFOfWithZeroValuation v
    ((((principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p) x hnK hnval hvx hcomplete :
          (CompleteDVF.higherPrincipalUnitGroup F) 1) : F.valuationSubringˣ) :
          F.valuationSubring) : K) =
      expSeriesFieldOfWithZeroValuation v x hnK := by
  simp [principalUnitExpSeriesOfWithZeroValuation]

theorem principalUnitExpSeries_val_valuation_eq_one_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime] (x : K)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hvx : v x < WithZero.exp (-1 : ℤ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    let F : CompleteDVF.{u, 0} K := completeDVFOfWithZeroValuation v
    v ((((principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p) x hnK hnval hvx hcomplete :
          (CompleteDVF.higherPrincipalUnitGroup F) 1) : F.valuationSubringˣ) :
          F.valuationSubring) : K) =
      (1 : WithZero (Multiplicative ℤ)) := by
  have hval :=
    principalUnitExpSeries_val_ofWithZeroValuation
      (v := v) (p := p) x hnK hnval hvx hcomplete
  dsimp at hval ⊢
  rw [hval]
  exact
    valuation_expSeriesField_eq_one_ofWithZeroValuation_of_lt_exp_neg_one
      (v := v) (p := p) x hnK hnval hvx hcomplete

theorem principalUnitExpSeries_zero_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    principalUnitExpSeriesOfWithZeroValuation
      (v := v) (p := p) (0 : K) hnK hnval
      (valuation_zero_lt_exp_neg_one (K := K) v) hcomplete =
      (1 : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1) := by
  apply Subtype.ext
  apply Units.ext
  apply Subtype.ext
  simp

theorem principalUnitExpSeries_eq_one_iff_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime] {x : K}
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hvx : v x < WithZero.exp (-1 : ℤ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p) x hnK hnval hvx hcomplete =
        (1 : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1) ↔
      x = 0 := by
  constructor
  · intro h
    by_contra hx
    have hne :
        principalUnitSubOneOfWithZeroValuation v
          (principalUnitExpSeriesOfWithZeroValuation
            (v := v) (p := p) x hnK hnval hvx hcomplete) ≠ 0 :=
      principalUnitSubOne_expSeries_ne_zero_ofWithZeroValuation
        (v := v) (p := p) (x := x) hx hnK hnval hvx hcomplete
    have hzero :
        principalUnitSubOneOfWithZeroValuation v
          (principalUnitExpSeriesOfWithZeroValuation
            (v := v) (p := p) x hnK hnval hvx hcomplete) = 0 := by
      simp [h, principalUnitSubOneOfWithZeroValuation]
    exact hne hzero
  · intro hx
    subst x
    simp

theorem principalUnitExpSeries_mul_val_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime] (x y : K)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hvx : v x < WithZero.exp (-1 : ℤ))
    (hvy : v y < WithZero.exp (-1 : ℤ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    let F : CompleteDVF.{u, 0} K := completeDVFOfWithZeroValuation v
    (((((principalUnitExpSeriesOfWithZeroValuation
          (v := v) (p := p) x hnK hnval hvx hcomplete) *
        (principalUnitExpSeriesOfWithZeroValuation
          (v := v) (p := p) y hnK hnval hvy hcomplete) :
          (CompleteDVF.higherPrincipalUnitGroup F) 1) : F.valuationSubringˣ) :
          F.valuationSubring) : K) =
      expSeriesFieldOfWithZeroValuation v x hnK *
        expSeriesFieldOfWithZeroValuation v y hnK := by
  simp

theorem principalUnitExpSeries_add_eq_mul_ofWithZeroValuation
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime] (x y : K)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hvx : v x < WithZero.exp (-1 : ℤ))
    (hvy : v y < WithZero.exp (-1 : ℤ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p) (x + y) hnK hnval
        (valuation_add_lt_exp_neg_one_of_lt_exp_neg_one v hvx hvy)
        hcomplete =
      (principalUnitExpSeriesOfWithZeroValuation
          (v := v) (p := p) x hnK hnval hvx hcomplete) *
        (principalUnitExpSeriesOfWithZeroValuation
          (v := v) (p := p) y hnK hnval hvy hcomplete) := by
  apply Subtype.ext
  apply Units.ext
  apply Subtype.ext
  simpa [principalUnitExpSeriesOfWithZeroValuation] using
    expSeriesField_add_eq_mul_ofWithZeroValuation_of_lt_exp_neg_one
      (v := v) (p := p) x y hnK hnval hvx hvy hcomplete

theorem principalUnitExpSeries_neg_mul_self_eq_one_ofWithZeroValuation
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime] (x : K)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hvx : v x < WithZero.exp (-1 : ℤ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    (principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p) (-x) hnK hnval
        (by simpa using hvx) hcomplete) *
      (principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p) x hnK hnval hvx hcomplete) =
        (1 : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1) := by
  have hmul :=
    principalUnitExpSeries_add_eq_mul_ofWithZeroValuation
      (v := v) (p := p) (-x) x hnK hnval (by simpa using hvx) hvx
      hcomplete
  simpa [neg_add_cancel] using hmul.symm

theorem principalUnitExpSeries_mul_neg_self_eq_one_ofWithZeroValuation
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime] (x : K)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hvx : v x < WithZero.exp (-1 : ℤ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    (principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p) x hnK hnval hvx hcomplete) *
      (principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p) (-x) hnK hnval
        (by simpa using hvx) hcomplete) =
        (1 : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1) := by
  have hmul :=
    principalUnitExpSeries_add_eq_mul_ofWithZeroValuation
      (v := v) (p := p) x (-x) hnK hnval hvx (by simpa using hvx)
      hcomplete
  simpa [add_neg_cancel] using hmul.symm

theorem principalUnitExpSeries_neg_eq_inv_self_ofWithZeroValuation
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime] (x : K)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hvx : v x < WithZero.exp (-1 : ℤ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p) (-x) hnK hnval
        (by simpa using hvx) hcomplete =
      (principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p) x hnK hnval hvx hcomplete)⁻¹ := by
  exact
    eq_inv_of_mul_eq_one_left
      (principalUnitExpSeries_neg_mul_self_eq_one_ofWithZeroValuation
        (v := v) (p := p) x hnK hnval hvx hcomplete)

theorem principalUnitExpSeries_inv_eq_neg_self_ofWithZeroValuation
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime] (x : K)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hvx : v x < WithZero.exp (-1 : ℤ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    (principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p) x hnK hnval hvx hcomplete)⁻¹ =
      principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p) (-x) hnK hnval
        (by simpa using hvx) hcomplete := by
  exact
    inv_eq_of_mul_eq_one_right
      (principalUnitExpSeries_mul_neg_self_eq_one_ofWithZeroValuation
        (v := v) (p := p) x hnK hnval hvx hcomplete)

def principalUnitExpSeriesHomOfWithZeroValuation
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    Multiplicative (expConvergenceAddSubgroupOfWithZeroValuation v) →*
      (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1 where
  toFun x :=
    principalUnitExpSeriesOfWithZeroValuation
      (v := v) (p := p) (x.toAdd : K) hnK hnval x.toAdd.property
      hcomplete
  map_one' := by
    simp
  map_mul' := by
    intro x y
    simpa using
      principalUnitExpSeries_add_eq_mul_ofWithZeroValuation
        (v := v) (p := p) (x.toAdd : K) (y.toAdd : K)
        hnK hnval x.toAdd.property y.toAdd.property hcomplete

theorem principalUnitExpSeriesHom_apply_ofAdd
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K)
    (x : expConvergenceAddSubgroupOfWithZeroValuation v) :
    principalUnitExpSeriesHomOfWithZeroValuation
        (v := v) (p := p) hnK hnval hcomplete
        (Multiplicative.ofAdd x) =
      principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p) (x : K) hnK hnval x.property hcomplete :=
  rfl

theorem principalUnitExpSeriesHom_eq_one_iff_ofWithZeroValuation
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K)
    (x : Multiplicative (expConvergenceAddSubgroupOfWithZeroValuation v)) :
    principalUnitExpSeriesHomOfWithZeroValuation
        (v := v) (p := p) hnK hnval hcomplete x = 1 ↔
      x = 1 := by
  constructor
  · intro hx
    have hx0 :
        ((x.toAdd : expConvergenceAddSubgroupOfWithZeroValuation v) : K) =
          0 := by
      exact
        (principalUnitExpSeries_eq_one_iff_ofWithZeroValuation
          (v := v) (p := p)
          (x := ((x.toAdd : expConvergenceAddSubgroupOfWithZeroValuation v) : K))
          hnK hnval x.toAdd.property hcomplete).1
          (by
            simpa [principalUnitExpSeriesHomOfWithZeroValuation] using hx)
    have hxSub :
        x.toAdd =
          (0 : expConvergenceAddSubgroupOfWithZeroValuation v) :=
      Subtype.ext hx0
    apply Multiplicative.ext
    simpa using hxSub
  · intro hx
    simp [hx]

theorem principalUnitExpSeriesHom_injective_ofWithZeroValuation
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    Function.Injective
      (principalUnitExpSeriesHomOfWithZeroValuation
        (v := v) (p := p) hnK hnval hcomplete) := by
  rw [injective_iff_map_eq_one']
  intro x
  exact
    principalUnitExpSeriesHom_eq_one_iff_ofWithZeroValuation
      (v := v) (p := p) hnK hnval hcomplete x

theorem principalUnitExpSeriesHom_ker_eq_bot_ofWithZeroValuation
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    (principalUnitExpSeriesHomOfWithZeroValuation
        (v := v) (p := p) hnK hnval hcomplete).ker = ⊥ := by
  exact
    (MonoidHom.ker_eq_bot_iff _).2
      (principalUnitExpSeriesHom_injective_ofWithZeroValuation
        (v := v) (p := p) hnK hnval hcomplete)

def principalUnitExpSeriesMulEquivRangeOfWithZeroValuation
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    Multiplicative (expConvergenceAddSubgroupOfWithZeroValuation v) ≃*
      (principalUnitExpSeriesHomOfWithZeroValuation
        (v := v) (p := p) hnK hnval hcomplete).range :=
  MonoidHom.ofInjective
    (principalUnitExpSeriesHom_injective_ofWithZeroValuation
      (v := v) (p := p) hnK hnval hcomplete)

theorem principalUnitExpSeriesMulEquivRange_apply_coe
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K)
    (x : Multiplicative (expConvergenceAddSubgroupOfWithZeroValuation v)) :
    ((principalUnitExpSeriesMulEquivRangeOfWithZeroValuation
        (v := v) (p := p) hnK hnval hcomplete x :
      (principalUnitExpSeriesHomOfWithZeroValuation
        (v := v) (p := p) hnK hnval hcomplete).range) :
      (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1) =
      principalUnitExpSeriesHomOfWithZeroValuation
        (v := v) (p := p) hnK hnval hcomplete x :=
  MonoidHom.ofInjective_apply
    (principalUnitExpSeriesHom_injective_ofWithZeroValuation
      (v := v) (p := p) hnK hnval hcomplete)

theorem principalUnitExpSeriesMulEquivRange_apply_ofAdd_coe
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K)
    (x : expConvergenceAddSubgroupOfWithZeroValuation v) :
    ((principalUnitExpSeriesMulEquivRangeOfWithZeroValuation
        (v := v) (p := p) hnK hnval hcomplete
        (Multiplicative.ofAdd x) :
      (principalUnitExpSeriesHomOfWithZeroValuation
        (v := v) (p := p) hnK hnval hcomplete).range) :
      (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1) =
      principalUnitExpSeriesOfWithZeroValuation
        (v := v) (p := p) (x : K) hnK hnval x.property hcomplete := by
  simp

theorem principalUnitExpSeriesHom_apply_mulEquivRange_symm
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime]
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K)
    (u :
      (principalUnitExpSeriesHomOfWithZeroValuation
        (v := v) (p := p) hnK hnval hcomplete).range) :
    principalUnitExpSeriesHomOfWithZeroValuation
        (v := v) (p := p) hnK hnval hcomplete
        ((principalUnitExpSeriesMulEquivRangeOfWithZeroValuation
          (v := v) (p := p) hnK hnval hcomplete).symm u) =
      u := by
  exact
    MonoidHom.apply_ofInjective_symm
      (principalUnitExpSeriesHom_injective_ofWithZeroValuation
        (v := v) (p := p) hnK hnval hcomplete) u

theorem principalUnitSubOne_val_lt_one_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (u : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1) :
    v (principalUnitSubOneOfWithZeroValuation v u) <
      (1 : WithZero (Multiplicative ℤ))

theorem principalUnitSubOne_isTopologicallyNilpotent_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (u : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    IsTopologicallyNilpotent
      (principalUnitSubOneOfWithZeroValuation v u) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  exact
    isTopologicallyNilpotent_ofWithZeroValuation_lt_one
      (v := v) (principalUnitSubOne_val_lt_one_ofWithZeroValuation v u)

theorem principalUnitSubOne_pair_hasEval_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (u w : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    MvPowerSeries.HasEval
      (fun i : Fin 2 =>
        if i = 0 then principalUnitSubOneOfWithZeroValuation v u
        else principalUnitSubOneOfWithZeroValuation v w) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  exact
    mvPowerSeries_hasEval_fin_two
      (principalUnitSubOne_isTopologicallyNilpotent_ofWithZeroValuation v u)
      (principalUnitSubOne_isTopologicallyNilpotent_ofWithZeroValuation v w)

theorem principalUnitSubOne_one_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v] :
    principalUnitSubOneOfWithZeroValuation v
        (1 : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1) =
      0

theorem principalUnitSubOne_eq_zero_iff_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (u : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1) :
    principalUnitSubOneOfWithZeroValuation v u = 0 ↔
      u = (1 : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1)

theorem principalUnitSubOne_mul_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (u w : (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v)) 1) :
    principalUnitSubOneOfWithZeroValuation v (u * w) =
      principalUnitSubOneOfWithZeroValuation v u +
        principalUnitSubOneOfWithZeroValuation v w +
          principalUnitSubOneOfWithZeroValuation v u *
            principalUnitSubOneOfWithZeroValuation v w

theorem principalUnitSubOne_expSeries_mul_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    {p : ℕ} [Fact p.Prime] (x y : K)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-(padicValNat p n.factorial : ℤ)))
    (hvx : v x < WithZero.exp (-1 : ℤ))
    (hvy : v y < WithZero.exp (-1 : ℤ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    principalUnitSubOneOfWithZeroValuation v
      ((principalUnitExpSeriesOfWithZeroValuation
          (v := v) (p := p) x hnK hnval hvx hcomplete) *
        (principalUnitExpSeriesOfWithZeroValuation
          (v := v) (p := p) y hnK hnval hvy hcomplete)) =
      (expSeriesFieldOfWithZeroValuation v x hnK - 1) +
        (expSeriesFieldOfWithZeroValuation v y hnK - 1) +
          (expSeriesFieldOfWithZeroValuation v x hnK - 1) *
            (expSeriesFieldOfWithZeroValuation v y hnK - 1) := by
  rw [principalUnitSubOne_mul_ofWithZeroValuation]
  simp