Units.lean

structure AntitoneSubgroupFiltration (G : Type u) [Group G] where
  /-- The subgroup at each natural-number filtration level. -/
  subgroup : ℕ → Subgroup G
  /-- Higher filtration levels are contained in lower ones. -/
  antitone : ∀ {m n : ℕ}, m ≤ n → subgroup n ≤ subgroup m

def principalUnitSubgroup (n : ℕ) : Subgroup G

theorem mem_principalUnitSubgroup_iff (n : ℕ) (x : G) :
    x ∈ U.principalUnitSubgroup n ↔ x ∈ U.subgroup n

theorem principalUnitSubgroup_antitone {m n : ℕ} (h : m ≤ n) :
    U.principalUnitSubgroup n ≤ U.principalUnitSubgroup m

theorem mem_of_mem_of_le {m n : ℕ} (h : m ≤ n) {x : G}
    (hx : x ∈ U.principalUnitSubgroup n) :
    x ∈ U.principalUnitSubgroup m

theorem one_mem_principalUnitSubgroup (n : ℕ) :
    (1 : G) ∈ U.principalUnitSubgroup n

theorem principalUnitSubgroup_mul_mem (n : ℕ) {x y : G}
    (hx : x ∈ U.principalUnitSubgroup n)
    (hy : y ∈ U.principalUnitSubgroup n) :
    x * y ∈ U.principalUnitSubgroup n

theorem principalUnitSubgroup_inv_mem (n : ℕ) {x : G}
    (hx : x ∈ U.principalUnitSubgroup n) :
    x⁻¹ ∈ U.principalUnitSubgroup n

theorem principalUnitSubgroup_div_mem (n : ℕ) {x y : G}
    (hx : x ∈ U.principalUnitSubgroup n)
    (hy : y ∈ U.principalUnitSubgroup n) :
    x / y ∈ U.principalUnitSubgroup n

theorem principalUnitSubgroup_pow_mem (n : ℕ) {x : G}
    (hx : x ∈ U.principalUnitSubgroup n) (m : ℕ) :
    x ^ m ∈ U.principalUnitSubgroup n

theorem principalUnitSubgroup_zpow_mem (n : ℕ) {x : G}
    (hx : x ∈ U.principalUnitSubgroup n) (m : ℤ) :
    x ^ m ∈ U.principalUnitSubgroup n

theorem principalUnitSubgroup_mul_iff_right (n : ℕ) {x u : G}
    (hu : u ∈ U.principalUnitSubgroup n) :
    x * u ∈ U.principalUnitSubgroup n ↔ x ∈ U.principalUnitSubgroup n

theorem principalUnitSubgroup_mul_iff_left (n : ℕ) {u x : G}
    (hu : u ∈ U.principalUnitSubgroup n) :
    u * x ∈ U.principalUnitSubgroup n ↔ x ∈ U.principalUnitSubgroup n

theorem principalUnitSubgroup_div_iff_right (n : ℕ) {x u : G}
    (hu : u ∈ U.principalUnitSubgroup n) :
    x / u ∈ U.principalUnitSubgroup n ↔ x ∈ U.principalUnitSubgroup n

theorem principalUnitSubgroup_div_iff_left (n : ℕ) {u x : G}
    (hu : u ∈ U.principalUnitSubgroup n) :
    u / x ∈ U.principalUnitSubgroup n ↔ x ∈ U.principalUnitSubgroup n

theorem principalUnitSubgroup_div_mem_iff_inv_mul_mem
    (n : ℕ) [(U.principalUnitSubgroup n).Normal] (x y : G) :
    x / y ∈ U.principalUnitSubgroup n ↔
      y⁻¹ * x ∈ U.principalUnitSubgroup n

theorem principalUnitSubgroup_inv_mul_mem_iff_div_mem
    (n : ℕ) [(U.principalUnitSubgroup n).Normal] (x y : G) :
    y⁻¹ * x ∈ U.principalUnitSubgroup n ↔
      x / y ∈ U.principalUnitSubgroup n

theorem quotient_principalUnitSubgroup_mk_eq_one_iff
    (n : ℕ) [(U.principalUnitSubgroup n).Normal] (x : G) :
    QuotientGroup.mk' (U.principalUnitSubgroup n) x = 1 ↔
      x ∈ U.principalUnitSubgroup n

theorem quotient_principalUnitSubgroup_mk_eq_iff_div_mem
    (n : ℕ) [(U.principalUnitSubgroup n).Normal] (x y : G) :
    QuotientGroup.mk' (U.principalUnitSubgroup n) x =
        QuotientGroup.mk' (U.principalUnitSubgroup n) y ↔
      x / y ∈ U.principalUnitSubgroup n

theorem quotient_principalUnitSubgroup_mk_eq_iff_inv_mul_mem
    (n : ℕ) [(U.principalUnitSubgroup n).Normal] (x y : G) :
    QuotientGroup.mk' (U.principalUnitSubgroup n) x =
        QuotientGroup.mk' (U.principalUnitSubgroup n) y ↔
      y⁻¹ * x ∈ U.principalUnitSubgroup n

def quotient_principalUnitSubgroup_mapOfLe {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal] :
    G ⧸ U.principalUnitSubgroup n →*
      G ⧸ U.principalUnitSubgroup m

theorem quotient_principalUnitSubgroup_mapOfLe_apply_mk
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal] (x : G) :
    U.quotient_principalUnitSubgroup_mapOfLe hmn (QuotientGroup.mk x) =
      QuotientGroup.mk x

theorem quotient_principalUnitSubgroup_mapOfLe_apply_mk'
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal] (x : G) :
    U.quotient_principalUnitSubgroup_mapOfLe hmn
        (QuotientGroup.mk' (U.principalUnitSubgroup n) x) =
      QuotientGroup.mk' (U.principalUnitSubgroup m) x

def principalUnitSubgroupClassInQuotient (m n : ℕ)
    [(U.principalUnitSubgroup n).Normal] :
    Subgroup (G ⧸ U.principalUnitSubgroup n)

instance principalUnitSubgroupClassInQuotient_normal
    (m n : ℕ) [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal] :
    (U.principalUnitSubgroupClassInQuotient m n).Normal

theorem mem_principalUnitSubgroupClassInQuotient_iff
    (m n : ℕ) [(U.principalUnitSubgroup n).Normal]
    (q : G ⧸ U.principalUnitSubgroup n) :
    q ∈ U.principalUnitSubgroupClassInQuotient m n ↔
      ∃ x : G, x ∈ U.principalUnitSubgroup m ∧
        QuotientGroup.mk' (U.principalUnitSubgroup n) x = q

theorem principalUnitSubgroupClassInQuotient_mk_mem
    {m n : ℕ} [(U.principalUnitSubgroup n).Normal] {x : G}
    (hx : x ∈ U.principalUnitSubgroup m) :
    QuotientGroup.mk' (U.principalUnitSubgroup n) x ∈
      U.principalUnitSubgroupClassInQuotient m n

def principalUnitSubquotient (m n : ℕ) : Type u

instance principalUnitSubquotientGroup
    (m n : ℕ) [(U.principalUnitSubgroup n).Normal] :
    Group (U.principalUnitSubquotient m n)

def principalUnitSubquotientConcreteEquiv
    (m n : ℕ) [(U.principalUnitSubgroup n).Normal] :
    U.principalUnitSubquotient m n ≃*
      (U.principalUnitSubgroup m ⧸
        (U.principalUnitSubgroup n).subgroupOf
          (U.principalUnitSubgroup m))

instance principalUnitSubquotientCommGroup
    {H : Type u} [CommGroup H] (V : AntitoneSubgroupFiltration H)
    (m n : ℕ) [(V.principalUnitSubgroup n).Normal] :
    CommGroup (V.principalUnitSubquotient m n)

def principalUnitSubquotientMk
    (m n : ℕ) [(U.principalUnitSubgroup n).Normal] :
    U.principalUnitSubgroup m →* U.principalUnitSubquotient m n

theorem principalUnitSubquotientConcreteEquiv_mk
    (m n : ℕ) [(U.principalUnitSubgroup n).Normal]
    (x : U.principalUnitSubgroup m) :
    U.principalUnitSubquotientConcreteEquiv m n
        (U.principalUnitSubquotientMk m n x) =
      QuotientGroup.mk x

theorem principalUnitSubquotientMk_surjective
    (m n : ℕ) [(U.principalUnitSubgroup n).Normal] :
    Function.Surjective (U.principalUnitSubquotientMk m n)

theorem principalUnitSubquotient.inductionOn
    (m n : ℕ) [(U.principalUnitSubgroup n).Normal]
    {motive : U.principalUnitSubquotient m n → Prop}
    (q : U.principalUnitSubquotient m n)
    (h : ∀ x : U.principalUnitSubgroup m,
      motive (U.principalUnitSubquotientMk m n x)) :
    motive q

def principalUnitSubquotientLift
    {H : Type*} [Group H] (m n : ℕ)
    [(U.principalUnitSubgroup n).Normal]
    (f : U.principalUnitSubgroup m →* H)
    (h : (U.principalUnitSubgroup n).subgroupOf
      (U.principalUnitSubgroup m) ≤ f.ker) :
    U.principalUnitSubquotient m n →* H

theorem principalUnitSubquotientLift_mk
    {H : Type*} [Group H] (m n : ℕ)
    [(U.principalUnitSubgroup n).Normal]
    (f : U.principalUnitSubgroup m →* H)
    (h : (U.principalUnitSubgroup n).subgroupOf
      (U.principalUnitSubgroup m) ≤ f.ker)
    (x : U.principalUnitSubgroup m) :
    U.principalUnitSubquotientLift m n f h
        (U.principalUnitSubquotientMk m n x) = f x

def principalUnitGradedPiece (n : ℕ) : Type u

instance principalUnitGradedPieceGroup
    (n : ℕ) [(U.principalUnitSubgroup (n + 1)).Normal] :
    Group (U.principalUnitGradedPiece n)

def principalUnitGradedPieceMk
    (n : ℕ) [(U.principalUnitSubgroup (n + 1)).Normal] :
    U.principalUnitSubgroup n →* U.principalUnitGradedPiece n

def principalUnitGradedPieceEquivSubquotient
    (n : ℕ) [(U.principalUnitSubgroup (n + 1)).Normal] :
    U.principalUnitGradedPiece n ≃*
      U.principalUnitSubquotient n (n + 1)

instance principalUnitGradedPieceFinite
    (n : ℕ) [(U.principalUnitSubgroup (n + 1)).Normal]
    [Finite (U.principalUnitSubquotient n (n + 1))] :
    Finite (U.principalUnitGradedPiece n)

theorem card_principalUnitSubquotient_succ_eq_gradedPiece
    (n : ℕ) [(U.principalUnitSubgroup (n + 1)).Normal]
    [Finite (U.principalUnitSubquotient n (n + 1))] :
    Nat.card (U.principalUnitSubquotient n (n + 1)) =
      Nat.card (U.principalUnitGradedPiece n)

theorem principalUnitSubquotient_mk_eq_one_iff
    {m n : ℕ} [(U.principalUnitSubgroup n).Normal]
    (x : U.principalUnitSubgroup m) :
    U.principalUnitSubquotientMk m n x = 1 ↔
      (x : G) ∈ U.principalUnitSubgroup n

theorem principalUnitSubquotient_mk_eq_iff_div_mem
    {m n : ℕ} [(U.principalUnitSubgroup n).Normal]
    (x y : U.principalUnitSubgroup m) :
    U.principalUnitSubquotientMk m n x =
      U.principalUnitSubquotientMk m n y ↔
      ((x / y : U.principalUnitSubgroup m) : G) ∈
        U.principalUnitSubgroup n

theorem principalUnitSubquotient_mk_eq_iff_inv_mul_mem
    {m n : ℕ} [(U.principalUnitSubgroup n).Normal]
    (x y : U.principalUnitSubgroup m) :
    U.principalUnitSubquotientMk m n x =
      U.principalUnitSubquotientMk m n y ↔
      ((y⁻¹ * x : U.principalUnitSubgroup m) : G) ∈
        U.principalUnitSubgroup n

def principalUnitSubgroupToQuotient {m n : ℕ} (_hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal] :
    U.principalUnitSubgroup m →* G ⧸ U.principalUnitSubgroup n

theorem principalUnitSubgroupToQuotient_apply
    {m n : ℕ} (hmn : m ≤ n) [(U.principalUnitSubgroup n).Normal]
    (x : U.principalUnitSubgroup m) :
    U.principalUnitSubgroupToQuotient hmn x =
      QuotientGroup.mk' (U.principalUnitSubgroup n) (x : G)

theorem principalUnitSubgroupToQuotient_ker_eq
    {m n : ℕ} (hmn : m ≤ n) [(U.principalUnitSubgroup n).Normal] :
    (U.principalUnitSubgroupToQuotient hmn).ker =
      (U.principalUnitSubgroup n).subgroupOf
        (U.principalUnitSubgroup m)

theorem principalUnitSubgroupToQuotient_range_eq_classInQuotient
    {m n : ℕ} (hmn : m ≤ n) [(U.principalUnitSubgroup n).Normal] :
    (U.principalUnitSubgroupToQuotient hmn).range =
      U.principalUnitSubgroupClassInQuotient m n

def principalUnitSubquotientEquivClassInQuotientOfLe
    {m n : ℕ} (hmn : m ≤ n) [(U.principalUnitSubgroup n).Normal] :
    U.principalUnitSubquotient m n ≃*
      U.principalUnitSubgroupClassInQuotient m n

theorem coe_principalUnitSubquotientEquivClassInQuotientOfLe_mk
    {m n : ℕ} (hmn : m ≤ n) [(U.principalUnitSubgroup n).Normal]
    (x : U.principalUnitSubgroup m) :
    ((U.principalUnitSubquotientEquivClassInQuotientOfLe hmn
        (U.principalUnitSubquotientMk m n x) :
      U.principalUnitSubgroupClassInQuotient m n) :
      G ⧸ U.principalUnitSubgroup n) =
      QuotientGroup.mk' (U.principalUnitSubgroup n) (x : G)

def principalUnitGradedPieceEquivClassInQuotient
    (n : ℕ) [(U.principalUnitSubgroup (n + 1)).Normal] :
    U.principalUnitGradedPiece n ≃*
      U.principalUnitSubgroupClassInQuotient n (n + 1)

theorem coe_principalUnitGradedPieceEquivClassInQuotient_mk
    (n : ℕ) [(U.principalUnitSubgroup (n + 1)).Normal]
    (x : U.principalUnitSubgroup n) :
    ((U.principalUnitGradedPieceEquivClassInQuotient n
        (U.principalUnitGradedPieceMk n x) :
      U.principalUnitSubgroupClassInQuotient n (n + 1)) :
      G ⧸ U.principalUnitSubgroup (n + 1)) =
      QuotientGroup.mk' (U.principalUnitSubgroup (n + 1)) (x : G)

theorem quotient_principalUnitSubgroup_mapOfLe_mk_eq_one_iff
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal] (x : G) :
    U.quotient_principalUnitSubgroup_mapOfLe hmn (QuotientGroup.mk x) = 1 ↔
      x ∈ U.principalUnitSubgroup m

theorem quotient_principalUnitSubgroup_mapOfLe_mk_eq_iff_div_mem
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal] (x y : G) :
    U.quotient_principalUnitSubgroup_mapOfLe hmn (QuotientGroup.mk x) =
        U.quotient_principalUnitSubgroup_mapOfLe hmn (QuotientGroup.mk y) ↔
      x / y ∈ U.principalUnitSubgroup m

theorem quotient_principalUnitSubgroup_mapOfLe_mk_eq_iff_inv_mul_mem
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal] (x y : G) :
    U.quotient_principalUnitSubgroup_mapOfLe hmn (QuotientGroup.mk x) =
        U.quotient_principalUnitSubgroup_mapOfLe hmn (QuotientGroup.mk y) ↔
      y⁻¹ * x ∈ U.principalUnitSubgroup m

theorem quotient_principalUnitSubgroup_mapOfLe_surjective
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal] :
    Function.Surjective (U.quotient_principalUnitSubgroup_mapOfLe hmn)

theorem quotient_principalUnitSubgroup_mapOfLe_range_eq_top
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal] :
    (U.quotient_principalUnitSubgroup_mapOfLe hmn).range = ⊤

theorem quotient_principalUnitSubgroup_mapOfLe_ker_eq_classInQuotient
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal] :
    (U.quotient_principalUnitSubgroup_mapOfLe hmn).ker =
      U.principalUnitSubgroupClassInQuotient m n

theorem quotient_principalUnitSubgroup_mapOfLe_mem_classInQuotient
    {l m n : ℕ} (_hlm : l ≤ m) (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal]
    {q : G ⧸ U.principalUnitSubgroup n}
    (hq : q ∈ U.principalUnitSubgroupClassInQuotient l n) :
    U.quotient_principalUnitSubgroup_mapOfLe hmn q ∈
      U.principalUnitSubgroupClassInQuotient l m

def principalUnitClassMapOfLe {l m n : ℕ} (hlm : l ≤ m) (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal] :
    U.principalUnitSubgroupClassInQuotient l n →*
      U.principalUnitSubgroupClassInQuotient l m

theorem principalUnitClassMapOfLe_apply {l m n : ℕ}
    (hlm : l ≤ m) (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal]
    (q : U.principalUnitSubgroupClassInQuotient l n) :
    ((U.principalUnitClassMapOfLe hlm hmn q :
      U.principalUnitSubgroupClassInQuotient l m) :
      G ⧸ U.principalUnitSubgroup m) =
      U.quotient_principalUnitSubgroup_mapOfLe hmn
        (q : G ⧸ U.principalUnitSubgroup n)

theorem principalUnitClassMapOfLe_ker_eq {l m n : ℕ}
    (hlm : l ≤ m) (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal] :
    (U.principalUnitClassMapOfLe hlm hmn).ker =
      (U.principalUnitSubgroupClassInQuotient m n).subgroupOf
        (U.principalUnitSubgroupClassInQuotient l n)

theorem principalUnitClassMapOfLe_surjective {l m n : ℕ}
    (hlm : l ≤ m) (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal] :
    Function.Surjective (U.principalUnitClassMapOfLe hlm hmn)

def principalUnitClassQuotientKerEquivClassOfLe {l m n : ℕ}
    (hlm : l ≤ m) (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal] :
    U.principalUnitSubgroupClassInQuotient l n ⧸
        (U.principalUnitClassMapOfLe hlm hmn).ker ≃*
      U.principalUnitSubgroupClassInQuotient l m

theorem principalUnitClassQuotientKerEquivClassOfLe_mk'
    {l m n : ℕ} (hlm : l ≤ m) (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal]
    (q : U.principalUnitSubgroupClassInQuotient l n) :
    U.principalUnitClassQuotientKerEquivClassOfLe hlm hmn
        (QuotientGroup.mk' (U.principalUnitClassMapOfLe hlm hmn).ker q) =
      U.principalUnitClassMapOfLe hlm hmn q

def principalUnitClassSubgroupOfEquivClassOfLe {l m n : ℕ}
    (hlm : l ≤ m) [(U.principalUnitSubgroup n).Normal] :
    (U.principalUnitSubgroupClassInQuotient m n).subgroupOf
        (U.principalUnitSubgroupClassInQuotient l n) ≃*
      U.principalUnitSubgroupClassInQuotient m n where
  toFun q :=
    ⟨((q : U.principalUnitSubgroupClassInQuotient l n) :
        G ⧸ U.principalUnitSubgroup n), by
      exact q.property⟩
  invFun q :=
    ⟨⟨(q : G ⧸ U.principalUnitSubgroup n), by
        rcases (U.mem_principalUnitSubgroupClassInQuotient_iff m n
            (q : G ⧸ U.principalUnitSubgroup n)).1 q.property with
          ⟨x, hx, hxq⟩
        exact ⟨x, U.mem_of_mem_of_le hlm hx, hxq⟩⟩, by
      change (q : G ⧸ U.principalUnitSubgroup n) ∈
        U.principalUnitSubgroupClassInQuotient m n
      exact q.property⟩
  left_inv q := by
    ext
    rfl
  right_inv q := by
    ext
    rfl
  map_mul' q r := by
    ext
    rfl

def principalUnitClassMapOfLeKerEquivClass {l m n : ℕ}
    (hlm : l ≤ m) (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal] :
    (U.principalUnitClassMapOfLe hlm hmn).ker ≃*
      U.principalUnitSubgroupClassInQuotient m n

theorem card_principalUnitClassInQuotient_eq_mul_of_le {l m n : ℕ}
    (hlm : l ≤ m) (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal]
    [Finite (U.principalUnitSubgroupClassInQuotient l n)]
    [Finite (U.principalUnitSubgroupClassInQuotient m n)]
    [Finite (U.principalUnitSubgroupClassInQuotient l m)] :
    Nat.card (U.principalUnitSubgroupClassInQuotient l n) =
      Nat.card (U.principalUnitSubgroupClassInQuotient m n) *
        Nat.card (U.principalUnitSubgroupClassInQuotient l m)

theorem card_principalUnitSubquotient_eq_classInQuotient_of_le
    {m n : ℕ} (hmn : m ≤ n) [(U.principalUnitSubgroup n).Normal]
    [Finite (U.principalUnitSubquotient m n)]
    [Finite (U.principalUnitSubgroupClassInQuotient m n)] :
    Nat.card (U.principalUnitSubquotient m n) =
      Nat.card (U.principalUnitSubgroupClassInQuotient m n)

theorem card_principalUnitSubquotient_self
    (n : ℕ) [(U.principalUnitSubgroup n).Normal]
    [Finite (U.principalUnitSubquotient n n)] :
    Nat.card (U.principalUnitSubquotient n n) = 1

theorem card_principalUnitSubquotient_eq_mul_of_le {l m n : ℕ}
    (hlm : l ≤ m) (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal]
    [Finite (U.principalUnitSubquotient l n)]
    [Finite (U.principalUnitSubquotient m n)]
    [Finite (U.principalUnitSubquotient l m)] :
    Nat.card (U.principalUnitSubquotient l n) =
      Nat.card (U.principalUnitSubquotient m n) *
      Nat.card (U.principalUnitSubquotient l m)

theorem card_principalUnitSubquotient_eq_prod_gradedPiece
    (hN : ∀ i : ℕ, (U.principalUnitSubgroup i).Normal)
    [∀ i j : ℕ, Finite (U.principalUnitSubquotient i j)]
    (l r : ℕ) :
    Nat.card (U.principalUnitSubquotient l (l + r)) =
      ∏ i ∈ Finset.range r,
        Nat.card (U.principalUnitGradedPiece (l + i))

theorem mem_quotient_principalUnitSubgroup_mapOfLe_ker_iff
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal]
    (q : G ⧸ U.principalUnitSubgroup n) :
    q ∈ (U.quotient_principalUnitSubgroup_mapOfLe hmn).ker ↔
      q ∈ U.principalUnitSubgroupClassInQuotient m n

theorem quotient_principalUnitSubgroup_mapOfLe_eq_one_iff_mem_classInQuotient
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal]
    (q : G ⧸ U.principalUnitSubgroup n) :
    U.quotient_principalUnitSubgroup_mapOfLe hmn q = 1 ↔
      q ∈ U.principalUnitSubgroupClassInQuotient m n

theorem quotient_principalUnitSubgroup_mapOfLe_eq_one_iff_exists_mem_repr
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal]
    (q : G ⧸ U.principalUnitSubgroup n) :
    U.quotient_principalUnitSubgroup_mapOfLe hmn q = 1 ↔
      ∃ x : G, x ∈ U.principalUnitSubgroup m ∧
        QuotientGroup.mk' (U.principalUnitSubgroup n) x = q

theorem quotient_principalUnitSubgroup_mapOfLe_eq_iff_div_mem_classInQuotient
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal]
    (q r : G ⧸ U.principalUnitSubgroup n) :
    U.quotient_principalUnitSubgroup_mapOfLe hmn q =
        U.quotient_principalUnitSubgroup_mapOfLe hmn r ↔
      q / r ∈ U.principalUnitSubgroupClassInQuotient m n

theorem quotient_principalUnitSubgroup_mapOfLe_eq_iff_exists_mem_div_repr
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal]
    (q r : G ⧸ U.principalUnitSubgroup n) :
    U.quotient_principalUnitSubgroup_mapOfLe hmn q =
        U.quotient_principalUnitSubgroup_mapOfLe hmn r ↔
      ∃ x : G, x ∈ U.principalUnitSubgroup m ∧
        QuotientGroup.mk' (U.principalUnitSubgroup n) x = q / r

theorem quotient_principalUnitSubgroup_mapOfLe_eq_iff_inv_mul_mem_classInQuotient
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal]
    (q r : G ⧸ U.principalUnitSubgroup n) :
    U.quotient_principalUnitSubgroup_mapOfLe hmn q =
        U.quotient_principalUnitSubgroup_mapOfLe hmn r ↔
      r⁻¹ * q ∈ U.principalUnitSubgroupClassInQuotient m n

theorem quotient_principalUnitSubgroup_mapOfLe_eq_iff_exists_mem_inv_mul_repr
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal]
    (q r : G ⧸ U.principalUnitSubgroup n) :
    U.quotient_principalUnitSubgroup_mapOfLe hmn q =
        U.quotient_principalUnitSubgroup_mapOfLe hmn r ↔
      ∃ x : G, x ∈ U.principalUnitSubgroup m ∧
        QuotientGroup.mk' (U.principalUnitSubgroup n) x = r⁻¹ * q

theorem quotient_principalUnitSubgroup_mk_mem_classInQuotient_iff
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal] (x : G) :
    QuotientGroup.mk' (U.principalUnitSubgroup n) x ∈
        U.principalUnitSubgroupClassInQuotient m n ↔
      x ∈ U.principalUnitSubgroup m

def quotientModuloPrincipalUnitClassEquivQuotientOfLe
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal] :
    (G ⧸ U.principalUnitSubgroup n) ⧸
        U.principalUnitSubgroupClassInQuotient m n ≃*
      G ⧸ U.principalUnitSubgroup m

theorem quotientModuloPrincipalUnitClassEquivQuotientOfLe_mk
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal]
    (q : G ⧸ U.principalUnitSubgroup n) :
    U.quotientModuloPrincipalUnitClassEquivQuotientOfLe hmn
        (QuotientGroup.mk'
          (U.principalUnitSubgroupClassInQuotient m n) q) =
      U.quotient_principalUnitSubgroup_mapOfLe hmn q

theorem quotientModuloPrincipalUnitClassEquivQuotientOfLe_mk_mk
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal] (x : G) :
    U.quotientModuloPrincipalUnitClassEquivQuotientOfLe hmn
        (QuotientGroup.mk'
          (U.principalUnitSubgroupClassInQuotient m n)
          (QuotientGroup.mk' (U.principalUnitSubgroup n) x)) =
      QuotientGroup.mk' (U.principalUnitSubgroup m) x

theorem quotientModuloPrincipalUnitClassEquivQuotientOfLe_symm_mk
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal] (x : G) :
    (U.quotientModuloPrincipalUnitClassEquivQuotientOfLe hmn).symm
        (QuotientGroup.mk' (U.principalUnitSubgroup m) x) =
      QuotientGroup.mk' (U.principalUnitSubgroupClassInQuotient m n)
        (QuotientGroup.mk' (U.principalUnitSubgroup n) x)

theorem quotientModuloPrincipalUnitClass_mk_eq_one_iff
    (m n : ℕ)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal]
    (q : G ⧸ U.principalUnitSubgroup n) :
    QuotientGroup.mk' (U.principalUnitSubgroupClassInQuotient m n) q = 1 ↔
      q ∈ U.principalUnitSubgroupClassInQuotient m n

theorem quotientModuloPrincipalUnitClass_mk_eq_one_iff_exists_mem_repr
    (m n : ℕ)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal]
    (q : G ⧸ U.principalUnitSubgroup n) :
    QuotientGroup.mk' (U.principalUnitSubgroupClassInQuotient m n) q = 1 ↔
      ∃ x : G, x ∈ U.principalUnitSubgroup m ∧
        QuotientGroup.mk' (U.principalUnitSubgroup n) x = q

theorem quotientModuloPrincipalUnitClass_mk_mk_eq_one_iff
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal] (x : G) :
    QuotientGroup.mk' (U.principalUnitSubgroupClassInQuotient m n)
        (QuotientGroup.mk' (U.principalUnitSubgroup n) x) = 1 ↔
      x ∈ U.principalUnitSubgroup m

theorem quotientModuloPrincipalUnitClass_mk_eq_iff_div_mem
    (m n : ℕ)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal]
    (q r : G ⧸ U.principalUnitSubgroup n) :
    QuotientGroup.mk' (U.principalUnitSubgroupClassInQuotient m n) q =
        QuotientGroup.mk' (U.principalUnitSubgroupClassInQuotient m n) r ↔
      q / r ∈ U.principalUnitSubgroupClassInQuotient m n

theorem quotientModuloPrincipalUnitClass_mk_eq_iff_exists_mem_div_repr
    (m n : ℕ)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal]
    (q r : G ⧸ U.principalUnitSubgroup n) :
    QuotientGroup.mk' (U.principalUnitSubgroupClassInQuotient m n) q =
        QuotientGroup.mk' (U.principalUnitSubgroupClassInQuotient m n) r ↔
      ∃ x : G, x ∈ U.principalUnitSubgroup m ∧
        QuotientGroup.mk' (U.principalUnitSubgroup n) x = q / r

theorem quotientModuloPrincipalUnitClass_mk_eq_iff_inv_mul_mem
    (m n : ℕ)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal]
    (q r : G ⧸ U.principalUnitSubgroup n) :
    QuotientGroup.mk' (U.principalUnitSubgroupClassInQuotient m n) q =
        QuotientGroup.mk' (U.principalUnitSubgroupClassInQuotient m n) r ↔
      r⁻¹ * q ∈ U.principalUnitSubgroupClassInQuotient m n

theorem quotientModuloPrincipalUnitClass_mk_eq_iff_exists_mem_inv_mul_repr
    (m n : ℕ)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal]
    (q r : G ⧸ U.principalUnitSubgroup n) :
    QuotientGroup.mk' (U.principalUnitSubgroupClassInQuotient m n) q =
        QuotientGroup.mk' (U.principalUnitSubgroupClassInQuotient m n) r ↔
      ∃ x : G, x ∈ U.principalUnitSubgroup m ∧
        QuotientGroup.mk' (U.principalUnitSubgroup n) x = r⁻¹ * q

theorem quotientModuloPrincipalUnitClass_mk_mk_eq_iff_div_mem
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal] (x y : G) :
    QuotientGroup.mk' (U.principalUnitSubgroupClassInQuotient m n)
        (QuotientGroup.mk' (U.principalUnitSubgroup n) x) =
      QuotientGroup.mk' (U.principalUnitSubgroupClassInQuotient m n)
        (QuotientGroup.mk' (U.principalUnitSubgroup n) y) ↔
      x / y ∈ U.principalUnitSubgroup m

theorem quotientModuloPrincipalUnitClass_mk_mk_eq_iff_inv_mul_mem
    {m n : ℕ} (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal] (x y : G) :
    QuotientGroup.mk' (U.principalUnitSubgroupClassInQuotient m n)
        (QuotientGroup.mk' (U.principalUnitSubgroup n) x) =
      QuotientGroup.mk' (U.principalUnitSubgroupClassInQuotient m n)
        (QuotientGroup.mk' (U.principalUnitSubgroup n) y) ↔
      y⁻¹ * x ∈ U.principalUnitSubgroup m

theorem quotient_principalUnitSubgroup_mapOfLe_comp
    {k m n : ℕ} (hkm : k ≤ m) (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal]
    [(U.principalUnitSubgroup k).Normal] :
    (U.quotient_principalUnitSubgroup_mapOfLe hkm).comp
        (U.quotient_principalUnitSubgroup_mapOfLe hmn) =
      U.quotient_principalUnitSubgroup_mapOfLe (le_trans hkm hmn)

theorem quotient_principalUnitSubgroup_mapOfLe_refl
    (n : ℕ) [(U.principalUnitSubgroup n).Normal] :
    U.quotient_principalUnitSubgroup_mapOfLe (le_rfl : n ≤ n) =
      MonoidHom.id (G ⧸ U.principalUnitSubgroup n)

theorem principalUnitSubgroupClassInQuotient_refl_eq_bot
    (n : ℕ) [(U.principalUnitSubgroup n).Normal] :
    U.principalUnitSubgroupClassInQuotient n n = ⊥

theorem principalUnitClassMapOfLe_refl
    {l n : ℕ} (hln : l ≤ n) [(U.principalUnitSubgroup n).Normal] :
    U.principalUnitClassMapOfLe hln (le_rfl : n ≤ n) =
      MonoidHom.id (U.principalUnitSubgroupClassInQuotient l n)

theorem principalUnitClassMapOfLe_comp
    {k l m n : ℕ} (hkl : k ≤ l) (hlm : l ≤ m) (hmn : m ≤ n)
    [(U.principalUnitSubgroup n).Normal]
    [(U.principalUnitSubgroup m).Normal]
    [(U.principalUnitSubgroup l).Normal] :
    (U.principalUnitClassMapOfLe hkl hlm).comp
        (U.principalUnitClassMapOfLe (le_trans hkl hlm) hmn) =
      U.principalUnitClassMapOfLe hkl (le_trans hlm hmn)