awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
this : Subgroup.index.{u_1} (G := ↥(torsion K)) (MonoidHom.range (powMonoidHom 2)) = 2
⊢ Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) ∣ 2
have refine : LE.le (α := Subgroup ↥(torsion K)) (MonoidHom.range (powMonoidHom 2)) (MonoidHom.range (unitsMulComplexConjInv K))
Tactic: refine this ▸ Subgroup.index_dvd_of_le ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
⊢ Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) ∣ 2
have suffices : Subgroup.index.{u_1} (G := ↥(torsion K)) (MonoidHom.range (powMonoidHom 2)) = 2
Tactic: suffices (powMonoidHom 2 : _ →* torsion K).range.index = 2 by
    refine this ▸ Subgroup.index_dvd_of_le ?_
    rintro _ ⟨ζ, _, rfl⟩
    exact ⟨ζ, Subtype.ext_iff.mpr (by simp [pow_two])⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
⊢ Subgroup.index.{u_1} (G := ↥(torsion K)) (MonoidHom.range (powMonoidHom 2)) = 2
have rw : 2 ∣ Fintype.card.{u_1} ↥(torsion K)
Tactic: rw [IsCyclic.index_powMonoidHom_range, Nat.gcd_eq_right_iff_dvd, Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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
have rw : Subgroup.index (G := (𝓞 K)ˣ) (torsion K ⊔ realUnits K) *
    Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) =
  2
Tactic: rw [indexRealUnits, sup_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
⊢ Subgroup.index (G := (𝓞 K)ˣ) (torsion K ⊔ realUnits K) *
      Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) =
    2
have h : Eq (α := Subgroup (𝓞 K)ˣ) (realUnits K) (MonoidHom.ker (unitsMulComplexConjInv K))
Tactic: convert! (Subgroup.index_map (torsion K) (unitsMulComplexConjInv K)).symm
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
h : Eq (α := Subgroup (𝓞 K)ˣ) (realUnits K) (MonoidHom.ker (unitsMulComplexConjInv K))
⊢ Subgroup.index (G := (𝓞 K)ˣ) (torsion K ⊔ realUnits K) *
      Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) =
    2
have h₁ : 2 = Subgroup.index (G := ↥(torsion K)) (Subgroup.map (unitsMulComplexConjInv K) (torsion K))
Tactic: convert! (Subgroup.index_map (torsion K) (unitsMulComplexConjInv K)).symm
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
⊢ Eq (α := Subgroup (𝓞 K)ˣ) (realUnits K) (MonoidHom.ker (unitsMulComplexConjInv K))
have h : Eq (α := Subgroup (𝓞 K)ˣ) (realUnits K) (realUnits K)
Tactic: rw [unitsMulComplexConjInv_ker]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
⊢ 2 = Subgroup.index (G := ↥(torsion K)) (Subgroup.map (unitsMulComplexConjInv K) (torsion K))
have h : 2 ∣ Nat.card.{u_1} ↥(torsion K)
Tactic: rw [map_unitsMulComplexConjInv_torsion, IsCyclic.index_powMonoidHom_range, Nat.gcd_eq_right]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
⊢ 2 ∣ Nat.card.{u_1} ↥(torsion K)
have h : 2 ∣ Fintype.card.{u_1} ↥(torsion K)
Tactic: rw [Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
⊢ indexRealUnits K = 1 ∨ indexRealUnits K = 2
have h₁ : indexRealUnits K * Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2
Tactic: have h₁ := indexRealUnits_mul_eq K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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
⊢ indexRealUnits K = 1 ∨ indexRealUnits K = 2
have inl : ∀ (h₂ : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1),
  indexRealUnits K = 1 ∨ indexRealUnits K = 2
Tactic: obtain h₂ | h₂ := (Nat.dvd_prime Nat.prime_two).mp <| index_unitsMulComplexConjInv_range_dvd K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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
⊢ indexRealUnits K = 1 ∨ indexRealUnits K = 2
have inr : ∀ (h₂ : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2),
  indexRealUnits K = 1 ∨ indexRealUnits K = 2
Tactic: obtain h₂ | h₂ := (Nat.dvd_prime Nat.prime_two).mp <| index_unitsMulComplexConjInv_range_dvd K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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 = 2
have rwa : ∀ (h₁ : indexRealUnits K * 1 = 2)
  (h₂ : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1), indexRealUnits K = 2
Tactic: rwa [h₂, mul_one] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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
⊢ indexRealUnits K = 2
have rwa₁ : ∀ (h₁ : indexRealUnits K = 2)
  (h₂ : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1), indexRealUnits K = 2
Tactic: rwa [h₂, mul_one] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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
have rwa : ∀ (h₁ : indexRealUnits K * 2 = 2)
  (h₂ : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2), indexRealUnits K = 1
Tactic: rwa [h₂, Nat.mul_eq_right two_ne_zero] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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
⊢ indexRealUnits K = 1
have rwa₁ : ∀ (h₁ : indexRealUnits K = 1)
  (h₂ : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2), indexRealUnits K = 1
Tactic: rwa [h₂, Nat.mul_eq_right two_ne_zero] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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 = 2 ↔
    ∃ (u : (𝓞 K)ˣ),
      Eq (α := Subgroup ↥(torsion K))
        (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
        (⊤ : Subgroup ↥(torsion K))
have rw : indexRealUnits K = 2 ↔ Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (hypothesis)
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 = 2 ↔ Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
have h_eq : indexRealUnits K * Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2
Tactic: have h_eq := indexRealUnits_mul_eq K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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
have refine_1 : ∀ (h : indexRealUnits K = 2), Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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
⊢ indexRealUnits K = 2 ↔ Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
have refine_2 : ∀ (h : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1), indexRealUnits K = 2
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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
⊢ Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
have 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
Tactic: rwa [h, Nat.mul_eq_left two_ne_zero] at h_eq
Cleared hypotheses: h_eq, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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
⊢ Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1
have 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
Tactic: rwa [h, Nat.mul_eq_left two_ne_zero] at h_eq
Cleared hypotheses: h_eq, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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
⊢ indexRealUnits K = 2
have refine_2 : ∀ (h_eq : indexRealUnits K * 1 = 2)
  (h : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1), indexRealUnits K = 2
Tactic: rwa [h, mul_one] at h_eq
Cleared hypotheses: h_eq, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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
⊢ indexRealUnits K = 2
have refine_2₁ : ∀ (h_eq : indexRealUnits K = 2)
  (h : Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 1), indexRealUnits K = 2
Tactic: rwa [h, mul_one] at h_eq
Cleared hypotheses: h_eq, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
⊢ indexRealUnits K = 2 ↔
    ∃ (u : (𝓞 K)ˣ),
      Eq (α := Subgroup ↥(torsion K))
        (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
        (⊤ : Subgroup ↥(torsion K))
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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
have 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))
Tactic: refine ⟨fun ⟨u, hu⟩ ↦ Subgroup.index_eq_one.mpr (top_le_iff.mp ?_), fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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))
⊢ (∃ (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
have 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))
Tactic: refine ⟨fun ⟨u, hu⟩ ↦ Subgroup.index_eq_one.mpr (top_le_iff.mp ?_), fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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))
have refine_1 : ⊤ = Subgroup.map (unitsMulComplexConjInv K) (Subgroup.zpowers u)
Tactic: refine le_of_eq_of_le ?_ ((Subgroup.zpowers u).map_le_range (unitsMulComplexConjInv K))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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))
⊢ ⊤ = Subgroup.map (unitsMulComplexConjInv K) (Subgroup.zpowers u)
have refine_1 : Eq (α := Subgroup ↥(torsion K)) (⊤ : Subgroup ↥(torsion K))
  (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
Tactic: rw [MonoidHom.map_zpowers, ← hu]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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))
⊢ ⊤ = Subgroup.map (unitsMulComplexConjInv K) (Subgroup.zpowers u)
have 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))
Tactic: rw [MonoidHom.map_zpowers, ← hu]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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
⊢ ∃ (u : (𝓞 K)ˣ),
    Eq (α := Subgroup ↥(torsion K))
      (Subgroup.zpowers ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : Subgroup ↥(torsion K))
      (⊤ : Subgroup ↥(torsion K))
have 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))
Tactic: obtain ⟨ζ, hζ⟩ := exists_zpow_surjective (torsion K)