awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
h : 2 ∣ Fintype.card.{u_1} ↥(torsion K)
⊢ 2 ∣ Nat.card.{u_1} ↥(torsion K)

Tactic:
rw [Nat.card_eq_fintype_card]

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
⊢ 2 ∣ Fintype.card.{u_1} ↥(torsion K)

Tactic:
even_iff_two_dvd.mp (even_torsionOrder K)

Premises used: Iff.mp, even_iff_two_dvd, NumberField.Units.even_torsionOrder
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
⊢ 2 ∣ Fintype.card.{u_1} ↥(torsion K)

Tactic:
exact even_iff_two_dvd.mp (even_torsionOrder K)

Premises used: Iff.mp, even_iff_two_dvd, NumberField.Units.even_torsionOrder
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
⊢ indexRealUnits K * Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2

Tactic:
have h₁ := indexRealUnits_mul_eq K
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
h₁ : indexRealUnits K * Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2
inl :
  ∀ (h₂ : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1),
    indexRealUnits K = 1 ∨ indexRealUnits K = 2
inr :
  ∀ (h₂ : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2),
    indexRealUnits K = 1 ∨ indexRealUnits K = 2
⊢ indexRealUnits K = 1 ∨ indexRealUnits K = 2

Tactic:
obtain h₂ | h₂ := (Nat.dvd_prime Nat.prime_two).mp <| index_unitsMulComplexConjInv_range_dvd K

Premises used: Nat.dvd_prime, Nat.prime_two, Iff.mp, NumberField.IsCMField.index_unitsMulComplexConjInv_range_dvd
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
h₁ : indexRealUnits K * Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2
h₂ : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
rwa :
  ∀ (h₁ : indexRealUnits K * 1 = 2)
    (h₂ : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1), indexRealUnits K = 2
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (h₁ : indexRealUnits K = 2)
    (h₂ : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1), indexRealUnits K = 2
⊢ indexRealUnits K = 2

Tactic:
rwa [h₂, mul_one] at h₁

Premises used: mul_one
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
h₁ : indexRealUnits K * Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2
h₂ : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
⊢ indexRealUnits K = 1 ∨ indexRealUnits K = 2

Tactic:
exact Or.inr <| by rwa [h₂, mul_one] at h₁

Premises used: Or.inr
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
h₁ : indexRealUnits K * Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2
h₂ : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2
rwa :
  ∀ (h₁ : indexRealUnits K * 2 = 2)
    (h₂ : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2), indexRealUnits K = 1
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (h₁ : indexRealUnits K = 1)
    (h₂ : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2), indexRealUnits K = 1
⊢ indexRealUnits K = 1

Tactic:
rwa [h₂, Nat.mul_eq_right two_ne_zero] at h₁

Premises used: Nat.mul_eq_right, two_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
h₁ : indexRealUnits K * Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2
h₂ : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2
⊢ indexRealUnits K = 1 ∨ indexRealUnits K = 2

Tactic:
exact Or.inl <| by rwa [h₂, Nat.mul_eq_right two_ne_zero] at h₁

Premises used: Or.inl
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
this :
  (∃ (u : (𝓞 K)ˣ),
      Eq (α := Subgroup ↥(torsion K))
        (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
        (⊤ : Subgroup ↥(torsion K))) ↔
    Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
rw : indexRealUnits K = 2 ↔ Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
⊢ indexRealUnits K = 2 ↔
    ∃ (u : (𝓞 K)ˣ),
      Eq (α := Subgroup ↥(torsion K))
        (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
        (⊤ : Subgroup ↥(torsion K))

Tactic:
rw [this]
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
this :
  (∃ (u : (𝓞 K)ˣ),
      Eq (α := Subgroup ↥(torsion K))
        (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
        (⊤ : Subgroup ↥(torsion K))) ↔
    Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
⊢ indexRealUnits K * Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2

Tactic:
have h_eq := indexRealUnits_mul_eq K
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
this :
  (∃ (u : (𝓞 K)ˣ),
      Eq (α := Subgroup ↥(torsion K))
        (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
        (⊤ : Subgroup ↥(torsion K))) ↔
    Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
h_eq : indexRealUnits K * Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2
⊢ indexRealUnits K = 2 ↔ Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
this :
  (∃ (u : (𝓞 K)ˣ),
      Eq (α := Subgroup ↥(torsion K))
        (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
        (⊤ : Subgroup ↥(torsion K))) ↔
    Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
h_eq : indexRealUnits K * Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2
refine_1 :
  ∀ (h : indexRealUnits K = 2), Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
refine_2 :
  ∀ (h : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1), indexRealUnits K = 2
⊢ indexRealUnits K = 2 ↔ Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
this :
  (∃ (u : (𝓞 K)ˣ),
      Eq (α := Subgroup ↥(torsion K))
        (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
        (⊤ : Subgroup ↥(torsion K))) ↔
    Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
h_eq : indexRealUnits K * Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2
h : indexRealUnits K = 2
refine_1 :
  ∀ (h_eq : 2 * Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2)
    (h : indexRealUnits K = 2), Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
refine_1₁ refine_1₂ refine_1₃ refine_1₄ :
  ∀ (h_eq : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1)
    (h : indexRealUnits K = 2), Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
⊢ Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1

Tactic:
rwa [h, Nat.mul_eq_left two_ne_zero] at h_eq

Premises used: Nat.mul_eq_left, two_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
this :
  (∃ (u : (𝓞 K)ˣ),
      Eq (α := Subgroup ↥(torsion K))
        (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
        (⊤ : Subgroup ↥(torsion K))) ↔
    Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
h_eq : indexRealUnits K * Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2
h : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
refine_2 :
  ∀ (h_eq : indexRealUnits K * 1 = 2)
    (h : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1), indexRealUnits K = 2
refine_2₁ refine_2₂ refine_2₃ refine_2₄ :
  ∀ (h_eq : indexRealUnits K = 2)
    (h : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1), indexRealUnits K = 2
⊢ indexRealUnits K = 2

Tactic:
rwa [h, mul_one] at h_eq

Premises used: mul_one
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
suffices :
  (∃ (u : (𝓞 K)ˣ),
      Eq (α := Subgroup ↥(torsion K))
        (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
        (⊤ : Subgroup ↥(torsion K))) ↔
    Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
⊢ indexRealUnits K = 2 ↔
    ∃ (u : (𝓞 K)ˣ),
      Eq (α := Subgroup ↥(torsion K))
        (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
        (⊤ : Subgroup ↥(torsion K))

Tactic:
suffices (∃ u : (𝓞 K)ˣ, Subgroup.zpowers (unitsMulComplexConjInv K u) = ⊤) ↔
      (unitsMulComplexConjInv K).range.index = 1 by
    rw [this]
    have h_eq := indexRealUnits_mul_eq K
    refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
    · rwa [h, Nat.mul_eq_left two_ne_zero] at h_eq
    · rwa [h, mul_one] at h_eq
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
⊢ (∃ (u : (𝓞 K)ˣ),
      Eq (α := Subgroup ↥(torsion K))
        (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
        (⊤ : Subgroup ↥(torsion K))) ↔
    Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1

Tactic:
⟨fun ⟨u, hu⟩ ↦ Subgroup.index_eq_one.mpr (top_le_iff.mp ?_), fun h ↦ ?_⟩

Premises used: Iff.mpr, MonoidHom.range, _private.0.NumberField.IsCMField.indexRealUnits_eq_two_iff.match_1, Subgroup.index, Iff.intro, top_le_iff, Iff.mp, Subgroup.index_eq_one, OfNat.ofNat, Eq, NumberField.IsCMField.unitsMulComplexConjInv
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
refine_1 :
  (∃ (u : (𝓞 K)ˣ),
      Eq (α := Subgroup ↥(torsion K))
        (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
        (⊤ : Subgroup ↥(torsion K))) →
    ∀ (u : (𝓞 K)ˣ)
      (hu :
        Eq (α := Subgroup ↥(torsion K))
          (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
          (⊤ : Subgroup ↥(torsion K))),
      LE.le (α := Subgroup ↥(torsion K)) ⊤ (MonoidHom.range (unitsMulComplexConjInv K))
refine_2 :
  ∀ (h : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1),
    ∃ (u : (𝓞 K)ˣ),
      Eq (α := Subgroup ↥(torsion K))
        (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
        (⊤ : Subgroup ↥(torsion K))
⊢ (∃ (u : (𝓞 K)ˣ),
      Eq (α := Subgroup ↥(torsion K))
        (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
        (⊤ : Subgroup ↥(torsion K))) ↔
    Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1

Tactic:
refine ⟨fun ⟨u, hu⟩ ↦ Subgroup.index_eq_one.mpr (top_le_iff.mp ?_), fun h ↦ ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
h :
  ∃ (u : (𝓞 K)ˣ),
    Eq (α := Subgroup ↥(torsion K))
      (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
      (⊤ : Subgroup ↥(torsion K))
u : (𝓞 K)ˣ
hu :
  Eq (α := Subgroup ↥(torsion K))
    (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
    (⊤ : Subgroup ↥(torsion K))
⊢ LE.le (α := Subgroup ↥(torsion K)) ⊤ (MonoidHom.range (unitsMulComplexConjInv K))

Tactic:
le_of_eq_of_le ?_ ((Subgroup.zpowers u).map_le_range (unitsMulComplexConjInv K))

Premises used: Subgroup.map_le_range, Subgroup.zpowers, le_of_eq_of_le, NumberField.IsCMField.unitsMulComplexConjInv
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
h :
  ∃ (u : (𝓞 K)ˣ),
    Eq (α := Subgroup ↥(torsion K))
      (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
      (⊤ : Subgroup ↥(torsion K))
u : (𝓞 K)ˣ
hu :
  Eq (α := Subgroup ↥(torsion K))
    (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
    (⊤ : Subgroup ↥(torsion K))
refine_1 : ⊤ = Subgroup.map (unitsMulComplexConjInv K) (Subgroup.zpowers u)
⊢ LE.le (α := Subgroup ↥(torsion K)) ⊤ (MonoidHom.range (unitsMulComplexConjInv K))

Tactic:
refine le_of_eq_of_le ?_ ((Subgroup.zpowers u).map_le_range (unitsMulComplexConjInv K))

Premises used: Subgroup.map_le_range, Subgroup.zpowers, le_of_eq_of_le, NumberField.IsCMField.unitsMulComplexConjInv
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
h :
  ∃ (u : (𝓞 K)ˣ),
    Eq (α := Subgroup ↥(torsion K))
      (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
      (⊤ : Subgroup ↥(torsion K))
u : (𝓞 K)ˣ
hu :
  Eq (α := Subgroup ↥(torsion K))
    (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
    (⊤ : Subgroup ↥(torsion K))
refine_1 :
  Eq (α := Subgroup ↥(torsion K)) (⊤ : Subgroup ↥(torsion K))
    (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
refine_1₁ refine_1₂ :
  Eq (α := Subgroup ↥(torsion K))
    (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
    (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
⊢ ⊤ = Subgroup.map (unitsMulComplexConjInv K) (Subgroup.zpowers u)

Tactic:
rw [MonoidHom.map_zpowers, ← hu]

Premises used: MonoidHom.map_zpowers
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
h : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
refine_2 :
  ∀ (ζ : ↥(torsion K)) (hζ : Function.Surjective.{1, u_1 + 1} (β := ↥(torsion K)) fun (x : ℤ) ↦ ζ ^ x),
    ∃ (u : (𝓞 K)ˣ),
      Eq (α := Subgroup ↥(torsion K))
        (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
        (⊤ : Subgroup ↥(torsion K))
⊢ ∃ (u : (𝓞 K)ˣ),
    Eq (α := Subgroup ↥(torsion K))
      (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
      (⊤ : Subgroup ↥(torsion K))

Tactic:
obtain ⟨ζ, hζ⟩ := exists_zpow_surjective (torsion K)

Premises used: Membership.mem, Subtype, NumberField.Units.torsion, exists_zpow_surjective
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
h : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
ζ : ↥(torsion K)
hζ : Function.Surjective.{1, u_1 + 1} (β := ↥(torsion K)) fun (x : ℤ) ↦ ζ ^ x
refine_2 :
  ∀
    (h :
      Function.Surjective (α := (𝓞 K)ˣ) (β := ↥(torsion K)) (⇑(unitsMulComplexConjInv K) : (a : (𝓞 K)ˣ) → ↥(torsion K)))
    (ζ : ↥(torsion K)) (hζ : Function.Surjective.{1, u_1 + 1} (β := ↥(torsion K)) fun (x : ℤ) ↦ ζ ^ x),
    ∃ (u : (𝓞 K)ˣ),
      Eq (α := Subgroup ↥(torsion K))
        (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
        (⊤ : Subgroup ↥(torsion K))
⊢ ∃ (u : (𝓞 K)ˣ),
    Eq (α := Subgroup ↥(torsion K))
      (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
      (⊤ : Subgroup ↥(torsion K))

Tactic:
rw [Subgroup.index_eq_one, MonoidHom.range_eq_top] at h

Premises used: MonoidHom.range_eq_top, Subgroup.index_eq_one
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
h : Function.Surjective (α := (𝓞 K)ˣ) (β := ↥(torsion K)) (⇑(unitsMulComplexConjInv K) : (a : (𝓞 K)ˣ) → ↥(torsion K))
ζ : ↥(torsion K)
hζ : Function.Surjective.{1, u_1 + 1} (β := ↥(torsion K)) fun (x : ℤ) ↦ ζ ^ x
refine_2 :
  ∀ (u : (𝓞 K)ˣ)
    (hζ :
      Function.Surjective.{1, u_1 + 1} (β := ↥(torsion K)) fun (x : ℤ) ↦
        HPow.hPow (α := ↥(torsion K)) ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u : ↥(torsion K)) x),
    ∃ (u : (𝓞 K)ˣ),
      Eq (α := Subgroup ↥(torsion K))
        (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
        (⊤ : Subgroup ↥(torsion K))
⊢ ∃ (u : (𝓞 K)ˣ),
    Eq (α := Subgroup ↥(torsion K))
      (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
      (⊤ : Subgroup ↥(torsion K))

Tactic:
obtain ⟨u, rfl⟩ := h ζ

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
h : Function.Surjective (α := (𝓞 K)ˣ) (β := ↥(torsion K)) (⇑(unitsMulComplexConjInv K) : (a : (𝓞 K)ˣ) → ↥(torsion K))
u : (𝓞 K)ˣ
hζ :
  Function.Surjective.{1, u_1 + 1} (β := ↥(torsion K)) fun (x : ℤ) ↦
    HPow.hPow (α := ↥(torsion K)) ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u : ↥(torsion K)) x
⊢ ∃ (u : (𝓞 K)ˣ),
    Eq (α := Subgroup ↥(torsion K))
      (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
      (⊤ : Subgroup ↥(torsion K))

Tactic:
⟨u, (Subgroup.eq_top_iff' _).mpr hζ⟩

Premises used: Iff.mpr, Subgroup.eq_top_iff', Exists.intro
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
h : Function.Surjective (α := (𝓞 K)ˣ) (β := ↥(torsion K)) (⇑(unitsMulComplexConjInv K) : (a : (𝓞 K)ˣ) → ↥(torsion K))
u : (𝓞 K)ˣ
hζ :
  Function.Surjective.{1, u_1 + 1} (β := ↥(torsion K)) fun (x : ℤ) ↦
    HPow.hPow (α := ↥(torsion K)) ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u : ↥(torsion K)) x
⊢ ∃ (u : (𝓞 K)ˣ),
    Eq (α := Subgroup ↥(torsion K))
      (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
      (⊤ : Subgroup ↥(torsion K))

Tactic:
exact ⟨u, (Subgroup.eq_top_iff' _).mpr hζ⟩
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
x : (𝓞 ↥K⁺)ˣ
hx : x ∈ (↑(torsion ↥K⁺) : Set (𝓞 ↥K⁺)ˣ)
⊢ Membership.mem (α := (𝓞 K)ˣ) (γ := Subgroup (𝓞 K)ˣ) (torsion K)
    ((Units.map (↑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : 𝓞 ↥K⁺ →* 𝓞 K) : (a : (𝓞 ↥K⁺)ˣ) → (𝓞 K)ˣ) x : (𝓞 K)ˣ)

Tactic:
MonoidHom.isOfFinOrder _ hx

Premises used: Set.Mem, MonoidHom.isOfFinOrder, setOf, Function.periodicPts, IsOfFinOrder
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
x : (𝓞 ↥K⁺)ˣ
hx : x ∈ (↑(torsion ↥K⁺) : Set (𝓞 ↥K⁺)ˣ)
⊢ Membership.mem (α := (𝓞 K)ˣ) (γ := Subgroup (𝓞 K)ˣ) (torsion K)
    ((Units.map (↑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : 𝓞 ↥K⁺ →* 𝓞 K) : (a : (𝓞 ↥K⁺)ˣ) → (𝓞 K)ˣ) x : (𝓞 K)ˣ)

Tactic:
exact MonoidHom.isOfFinOrder _ hx

Premises used: MonoidHom.isOfFinOrder
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
⊢ Subgroup.map (Units.map (↑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : 𝓞 ↥K⁺ →* 𝓞 K)) (torsion ↥K⁺) ≤ torsion K

Tactic:
have : Subgroup.map (Units.map (algebraMap (𝓞 K⁺) (𝓞 K))) (torsion K⁺) ≤ torsion K := by
    rintro _ ⟨x, hx, rfl⟩
    exact MonoidHom.isOfFinOrder _ hx
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
this : Subgroup.map (Units.map (↑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : 𝓞 ↥K⁺ →* 𝓞 K)) (torsion ↥K⁺) ≤ torsion K
rw :
  Eq (α := Subgroup (𝓞 K)ˣ) (Subgroup.closure (Set.range (ι := Fin (rank K)) (realFundSystem K)) ⊔ torsion K)
    (Subgroup.closure
        (Set.image (α := (𝓞 ↥K⁺)ˣ) (⇑(Units.map (↑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : 𝓞 ↥K⁺ →* 𝓞 K)) : (a : (𝓞 ↥K⁺)ˣ) → (𝓞 K)ˣ)
          (Set.range (ι := Fin (rank.{u_1} ↥K⁺)) (fundSystem ↥K⁺))) ⊔
      torsion K)
⊢ Eq (α := Subgroup (𝓞 K)ˣ) (Subgroup.closure (Set.range (ι := Fin (rank K)) (realFundSystem K)) ⊔ torsion K)
    (realUnits K ⊔ torsion K)

Tactic:
rw [realUnits, MonoidHom.range_eq_map, ← closure_fundSystem_sup_torsion_eq_top, Subgroup.map_sup,
    sup_assoc, RingHom.toMonoidHom_eq_coe, sup_eq_right.mpr this, MonoidHom.map_closure]

Premises used: Iff.mpr, Subgroup.map_sup, RingHom.toMonoidHom_eq_coe, MonoidHom.range_eq_map, sup_assoc, NumberField.Units.closure_fundSystem_sup_torsion_eq_top, MonoidHom.map_closure, sup_eq_right, NumberField.IsCMField.realUnits
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
this : Subgroup.map (Units.map (↑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : 𝓞 ↥K⁺ →* 𝓞 K)) (torsion ↥K⁺) ≤ torsion K
e_a :
  Eq (α := Set (𝓞 K)ˣ) (Set.range (ι := Fin (rank K)) (realFundSystem K))
    (Set.image (α := (𝓞 ↥K⁺)ˣ) (⇑(Units.map (↑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : 𝓞 ↥K⁺ →* 𝓞 K)) : (a : (𝓞 ↥K⁺)ˣ) → (𝓞 K)ˣ)
      (Set.range (ι := Fin (rank.{u_1} ↥K⁺)) (fundSystem ↥K⁺)))
⊢ Eq (α := Subgroup (𝓞 K)ˣ) (Subgroup.closure (Set.range (ι := Fin (rank K)) (realFundSystem K)) ⊔ torsion K)
    (Subgroup.closure
        (Set.image (α := (𝓞 ↥K⁺)ˣ) (⇑(Units.map (↑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : 𝓞 ↥K⁺ →* 𝓞 K)) : (a : (𝓞 ↥K⁺)ˣ) → (𝓞 K)ˣ)
          (Set.range (ι := Fin (rank.{u_1} ↥K⁺)) (fundSystem ↥K⁺))) ⊔
      torsion K)

Tactic:
congr