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 : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
simp_rw :
  (↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u) : 𝓞 K) = (↑u : 𝓞 K) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) u
simp_rw₁ :
  (↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u) : 𝓞 K) = (↑u : 𝓞 K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ), (algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺) = (↑u : 𝓞 K)
simp_rw₂ :
  (↑(↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u) : 𝓞 K) : K) = (↑(↑u : 𝓞 K) : K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ), (↑((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺)) : K) = (↑(↑u : 𝓞 K) : K)
⊢ (unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u = u ↔ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) u
have simp_rw₃ : (↑(((↑(RingOfIntegers.mapRingEquiv (AlgEquiv.toRingEquiv (complexConj K))) : 𝓞 K ≃* 𝓞 K) : (a : 𝓞 K) → 𝓞 K)
          (↑u : 𝓞 K)) :
      K) =
    (↑(↑u : 𝓞 K) : K) ↔
  ∃ (v : (𝓞 ↥K⁺)ˣ), (↑((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺)) : K) = (↑(↑u : 𝓞 K) : K)
Tactic: simp_rw [Units.ext_iff, mem_realUnits_iff, RingOfIntegers.ext_iff, Units.coe_mapEquiv,
    RingEquiv.coe_toMulEquiv, RingOfIntegers.mapRingEquiv_apply,
    AlgEquiv.coe_ringEquiv, Units.complexConj_eq_self_iff,
    IsScalarTower.algebraMap_apply (𝓞 K⁺) (𝓞 K) 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 : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
simp_rw :
  (↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u) : 𝓞 K) = (↑u : 𝓞 K) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) u
simp_rw₁ :
  (↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u) : 𝓞 K) = (↑u : 𝓞 K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ), (algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺) = (↑u : 𝓞 K)
simp_rw₂ :
  (↑(↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u) : 𝓞 K) : K) = (↑(↑u : 𝓞 K) : K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ), (↑((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺)) : K) = (↑(↑u : 𝓞 K) : K)
simp_rw₃ :
  (↑(((↑(RingOfIntegers.mapRingEquiv (AlgEquiv.toRingEquiv (complexConj K))) : 𝓞 K ≃* 𝓞 K) : (a : 𝓞 K) → 𝓞 K)
            (↑u : 𝓞 K)) :
        K) =
      (↑(↑u : 𝓞 K) : K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ), (↑((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺)) : K) = (↑(↑u : 𝓞 K) : K)
⊢ (unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u = u ↔ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) u
have simp_rw₄ : (↑((RingOfIntegers.mapRingEquiv (AlgEquiv.toRingEquiv (complexConj K)) : (a : 𝓞 K) → 𝓞 K) (↑u : 𝓞 K)) : K) =
    (↑(↑u : 𝓞 K) : K) ↔
  ∃ (v : (𝓞 ↥K⁺)ˣ), (↑((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺)) : K) = (↑(↑u : 𝓞 K) : K)
Tactic: simp_rw [Units.ext_iff, mem_realUnits_iff, RingOfIntegers.ext_iff, Units.coe_mapEquiv,
    RingEquiv.coe_toMulEquiv, RingOfIntegers.mapRingEquiv_apply,
    AlgEquiv.coe_ringEquiv, Units.complexConj_eq_self_iff,
    IsScalarTower.algebraMap_apply (𝓞 K⁺) (𝓞 K) 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 : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
simp_rw :
  (↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u) : 𝓞 K) = (↑u : 𝓞 K) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) u
simp_rw₁ :
  (↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u) : 𝓞 K) = (↑u : 𝓞 K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ), (algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺) = (↑u : 𝓞 K)
simp_rw₂ :
  (↑(↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u) : 𝓞 K) : K) = (↑(↑u : 𝓞 K) : K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ), (↑((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺)) : K) = (↑(↑u : 𝓞 K) : K)
simp_rw₃ :
  (↑(((↑(RingOfIntegers.mapRingEquiv (AlgEquiv.toRingEquiv (complexConj K))) : 𝓞 K ≃* 𝓞 K) : (a : 𝓞 K) → 𝓞 K)
            (↑u : 𝓞 K)) :
        K) =
      (↑(↑u : 𝓞 K) : K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ), (↑((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺)) : K) = (↑(↑u : 𝓞 K) : K)
simp_rw₄ :
  (↑((RingOfIntegers.mapRingEquiv (AlgEquiv.toRingEquiv (complexConj K)) : (a : 𝓞 K) → 𝓞 K) (↑u : 𝓞 K)) : K) =
      (↑(↑u : 𝓞 K) : K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ), (↑((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺)) : K) = (↑(↑u : 𝓞 K) : K)
⊢ (unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u = u ↔ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) u
have simp_rw₅ : (AlgEquiv.toRingEquiv (complexConj K) : (a : K) → K) (↑(↑u : 𝓞 K) : K) = (↑(↑u : 𝓞 K) : K) ↔
  ∃ (v : (𝓞 ↥K⁺)ˣ), (↑((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺)) : K) = (↑(↑u : 𝓞 K) : K)
Tactic: simp_rw [Units.ext_iff, mem_realUnits_iff, RingOfIntegers.ext_iff, Units.coe_mapEquiv,
    RingEquiv.coe_toMulEquiv, RingOfIntegers.mapRingEquiv_apply,
    AlgEquiv.coe_ringEquiv, Units.complexConj_eq_self_iff,
    IsScalarTower.algebraMap_apply (𝓞 K⁺) (𝓞 K) 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 : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
simp_rw :
  (↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u) : 𝓞 K) = (↑u : 𝓞 K) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) u
simp_rw₁ :
  (↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u) : 𝓞 K) = (↑u : 𝓞 K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ), (algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺) = (↑u : 𝓞 K)
simp_rw₂ :
  (↑(↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u) : 𝓞 K) : K) = (↑(↑u : 𝓞 K) : K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ), (↑((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺)) : K) = (↑(↑u : 𝓞 K) : K)
simp_rw₃ :
  (↑(((↑(RingOfIntegers.mapRingEquiv (AlgEquiv.toRingEquiv (complexConj K))) : 𝓞 K ≃* 𝓞 K) : (a : 𝓞 K) → 𝓞 K)
            (↑u : 𝓞 K)) :
        K) =
      (↑(↑u : 𝓞 K) : K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ), (↑((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺)) : K) = (↑(↑u : 𝓞 K) : K)
simp_rw₄ :
  (↑((RingOfIntegers.mapRingEquiv (AlgEquiv.toRingEquiv (complexConj K)) : (a : 𝓞 K) → 𝓞 K) (↑u : 𝓞 K)) : K) =
      (↑(↑u : 𝓞 K) : K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ), (↑((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺)) : K) = (↑(↑u : 𝓞 K) : K)
simp_rw₅ :
  (AlgEquiv.toRingEquiv (complexConj K) : (a : K) → K) (↑(↑u : 𝓞 K) : K) = (↑(↑u : 𝓞 K) : K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ), (↑((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺)) : K) = (↑(↑u : 𝓞 K) : K)
⊢ (unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u = u ↔ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) u
have simp_rw₆ : (complexConj K : (a : K) → K) (↑(↑u : 𝓞 K) : K) = (↑(↑u : 𝓞 K) : K) ↔
  ∃ (v : (𝓞 ↥K⁺)ˣ), (↑((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺)) : K) = (↑(↑u : 𝓞 K) : K)
Tactic: simp_rw [Units.ext_iff, mem_realUnits_iff, RingOfIntegers.ext_iff, Units.coe_mapEquiv,
    RingEquiv.coe_toMulEquiv, RingOfIntegers.mapRingEquiv_apply,
    AlgEquiv.coe_ringEquiv, Units.complexConj_eq_self_iff,
    IsScalarTower.algebraMap_apply (𝓞 K⁺) (𝓞 K) 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 : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
simp_rw :
  (↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u) : 𝓞 K) = (↑u : 𝓞 K) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) u
simp_rw₁ :
  (↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u) : 𝓞 K) = (↑u : 𝓞 K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ), (algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺) = (↑u : 𝓞 K)
simp_rw₂ :
  (↑(↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u) : 𝓞 K) : K) = (↑(↑u : 𝓞 K) : K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ), (↑((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺)) : K) = (↑(↑u : 𝓞 K) : K)
simp_rw₃ :
  (↑(((↑(RingOfIntegers.mapRingEquiv (AlgEquiv.toRingEquiv (complexConj K))) : 𝓞 K ≃* 𝓞 K) : (a : 𝓞 K) → 𝓞 K)
            (↑u : 𝓞 K)) :
        K) =
      (↑(↑u : 𝓞 K) : K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ), (↑((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺)) : K) = (↑(↑u : 𝓞 K) : K)
simp_rw₄ :
  (↑((RingOfIntegers.mapRingEquiv (AlgEquiv.toRingEquiv (complexConj K)) : (a : 𝓞 K) → 𝓞 K) (↑u : 𝓞 K)) : K) =
      (↑(↑u : 𝓞 K) : K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ), (↑((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺)) : K) = (↑(↑u : 𝓞 K) : K)
simp_rw₅ :
  (AlgEquiv.toRingEquiv (complexConj K) : (a : K) → K) (↑(↑u : 𝓞 K) : K) = (↑(↑u : 𝓞 K) : K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ), (↑((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺)) : K) = (↑(↑u : 𝓞 K) : K)
simp_rw₆ :
  (complexConj K : (a : K) → K) (↑(↑u : 𝓞 K) : K) = (↑(↑u : 𝓞 K) : K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ), (↑((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺)) : K) = (↑(↑u : 𝓞 K) : K)
⊢ (unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u = u ↔ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) u
have simp_rw₇ : (∃ (v : (𝓞 ↥K⁺)ˣ),
    Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) (↑v : 𝓞 ↥K⁺) : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) ↔
  ∃ (v : (𝓞 ↥K⁺)ˣ), (↑((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺)) : K) = (↑(↑u : 𝓞 K) : K)
Tactic: simp_rw [Units.ext_iff, mem_realUnits_iff, RingOfIntegers.ext_iff, Units.coe_mapEquiv,
    RingEquiv.coe_toMulEquiv, RingOfIntegers.mapRingEquiv_apply,
    AlgEquiv.coe_ringEquiv, Units.complexConj_eq_self_iff,
    IsScalarTower.algebraMap_apply (𝓞 K⁺) (𝓞 K) 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
ζ : ↥(torsion K)
φ : K →+* ℂ := Classical.choice ⋯
⊢ Eq (α := K) ((complexConj K : (a : K) → K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑ζ : (𝓞 K)ˣ) : 𝓞 K) : K) : K)
    (((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑ζ : (𝓞 K)ˣ) : 𝓞 K))⁻¹ : K)
have a : Eq (α := ℂ)
  ((φ : (a : K) → ℂ)
      ((complexConj K : (a : K) → K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑ζ : (𝓞 K)ˣ) : 𝓞 K) : K) : K) :
    ℂ)
  ((φ : (a : K) → ℂ) (((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑ζ : (𝓞 K)ˣ) : 𝓞 K))⁻¹ : K) : ℂ)
Tactic: apply φ.injective
-- 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
ζ : ↥(torsion K)
φ : K →+* ℂ := Classical.choice ⋯
⊢ Eq (α := ℂ)
    ((φ : (a : K) → ℂ)
        ((complexConj K : (a : K) → K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑ζ : (𝓞 K)ˣ) : 𝓞 K) : K) : K) :
      ℂ)
    ((φ : (a : K) → ℂ) (((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(↑ζ : (𝓞 K)ˣ) : 𝓞 K))⁻¹ : K) : ℂ)
have a : Membership.mem (α := ℂˣ) (γ := Subgroup ℂˣ) (rootsOfUnity (torsionOrder K) ℂ)
  ((Units.complexEmbedding φ : (a : (𝓞 K)ˣ) → ℂˣ) (↑ζ : (𝓞 K)ˣ) : ℂˣ)
Tactic: rw [complexEmbedding_complexConj, ← Units.complexEmbedding_apply,
    Complex.conj_rootsOfUnity (n := torsionOrder K), Units.val_inv_eq_inv_val,
    Units.complexEmbedding_apply, map_inv₀]
-- 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
ζ : ↥(torsion K)
⊢ (unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) (↑ζ : (𝓞 K)ˣ) = (↑ζ⁻¹ : (𝓞 K)ˣ)
have a : Eq.{u_1 + 1} (α := K)
  ((fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))
    ((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) (↑ζ : (𝓞 K)ˣ)))
  ((fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) (↑ζ⁻¹ : (𝓞 K)ˣ))
Tactic: apply coe_injective
-- 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
x y : (𝓞 K)ˣ
⊢ Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x)
      (HMul.hMul (β := (𝓞 K)ˣ) (x * y) (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) (x * y))⁻¹ : (𝓞 K)ˣ)) ⋯ =
    Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x)
        (HMul.hMul (β := (𝓞 K)ˣ) x (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) x)⁻¹ : (𝓞 K)ˣ)) ⋯ *
      Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x)
        (HMul.hMul (β := (𝓞 K)ˣ) y (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) y)⁻¹ : (𝓞 K)ˣ)) ⋯
have rw : HMul.hMul (β := (𝓞 K)ˣ) (x * y) (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) (x * y))⁻¹ : (𝓞 K)ˣ) =
  HMul.hMul (β := (𝓞 K)ˣ) x (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) x)⁻¹ : (𝓞 K)ˣ) *
    HMul.hMul (β := (𝓞 K)ˣ) y (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) y)⁻¹ : (𝓞 K)ˣ)
Tactic: rw [MulMemClass.mk_mul_mk, Subtype.mk_eq_mk]
-- 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
x y : (𝓞 K)ˣ
⊢ HMul.hMul (β := (𝓞 K)ˣ) (x * y) (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) (x * y))⁻¹ : (𝓞 K)ˣ) =
    HMul.hMul (β := (𝓞 K)ˣ) x (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) x)⁻¹ : (𝓞 K)ˣ) *
      HMul.hMul (β := (𝓞 K)ˣ) y (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) y)⁻¹ : (𝓞 K)ˣ)
have a : Eq.{u_1 + 1} (α := K)
  ((fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))
    (HMul.hMul (β := (𝓞 K)ˣ) (x * y) (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) (x * y))⁻¹ : (𝓞 K)ˣ)))
  ((fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))
    (HMul.hMul (β := (𝓞 K)ˣ) x (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) x)⁻¹ : (𝓞 K)ˣ) *
      HMul.hMul (β := (𝓞 K)ˣ) y (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) y)⁻¹ : (𝓞 K)ˣ)))
Tactic: apply coe_injective
-- 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
x y : (𝓞 K)ˣ
⊢ Eq.{u_1 + 1} (α := K)
    ((fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))
      (HMul.hMul (β := (𝓞 K)ˣ) (x * y) (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) (x * y))⁻¹ : (𝓞 K)ˣ)))
    ((fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))
      (HMul.hMul (β := (𝓞 K)ˣ) x (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) x)⁻¹ : (𝓞 K)ˣ) *
        HMul.hMul (β := (𝓞 K)ˣ) y (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) y)⁻¹ : (𝓞 K)ˣ)))
have a : HMul.hMul (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑y : 𝓞 K) : K) *
    HMul.hMul (α := K) (β := K)
      (((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) y) : 𝓞 K))⁻¹ : K)
      (((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) x) : 𝓞 K))⁻¹ : K) =
  HMul.hMul (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)
      (((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) x) : 𝓞 K))⁻¹ : K) *
    HMul.hMul (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑y : 𝓞 K) : K)
      (((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) y) : 𝓞 K))⁻¹ : K)
Tactic: simp only [map_mul, mul_inv_rev, Units.val_mul, map_units_inv]
-- 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 ↥(torsion K)) (Subgroup.map (unitsMulComplexConjInv K) (torsion K))
    (MonoidHom.range (powMonoidHom 2))
have rw : Eq.{u_1 + 1} (α := Subgroup ↥(torsion K))
  (MonoidHom.range (G := ↥(torsion K)) (MonoidHom.restrict (unitsMulComplexConjInv K) (torsion K)))
  (MonoidHom.range (powMonoidHom 2))
Tactic: rw [← MonoidHom.restrict_range]
-- 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)ˣ) (MonoidHom.ker (unitsMulComplexConjInv K)) (realUnits K)
have h : ∀ (x : (𝓞 K)ˣ),
  Membership.mem (γ := Subgroup (𝓞 K)ˣ) (MonoidHom.ker (unitsMulComplexConjInv K)) x ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
Tactic: ext
-- 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
x : (𝓞 K)ˣ
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (MonoidHom.ker (unitsMulComplexConjInv K)) x ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
have h : Eq (α := ↥(torsion K)) ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) x : ↥(torsion K)) (1 : ↥(torsion K)) ↔
  Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
Tactic: rw [MonoidHom.mem_ker, Subtype.ext_iff, unitsMulComplexConjInv_apply, OneMemClass.coe_one,
    mul_inv_eq_one, eq_comm, unitsComplexConj_eq_self_iff]
-- 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
x : (𝓞 K)ˣ
h :
  Eq (α := ↥(torsion K)) ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) x : ↥(torsion K))
      (1 : ↥(torsion K)) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (MonoidHom.ker (unitsMulComplexConjInv K)) x ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
have h₁ : Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (↑((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) x) : (𝓞 K)ˣ) (↑1 : (𝓞 K)ˣ) ↔
  Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
Tactic: rw [MonoidHom.mem_ker, Subtype.ext_iff, unitsMulComplexConjInv_apply, OneMemClass.coe_one,
    mul_inv_eq_one, eq_comm, unitsComplexConj_eq_self_iff]
-- 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
x : (𝓞 K)ˣ
h :
  Eq (α := ↥(torsion K)) ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) x : ↥(torsion K))
      (1 : ↥(torsion K)) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
h₁ :
  Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (↑((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) x) : (𝓞 K)ˣ) (↑1 : (𝓞 K)ˣ) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (MonoidHom.ker (unitsMulComplexConjInv K)) x ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
have h₂ : HMul.hMul (β := (𝓞 K)ˣ) x (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) x)⁻¹ : (𝓞 K)ˣ) = (↑1 : (𝓞 K)ˣ) ↔
  Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
Tactic: rw [MonoidHom.mem_ker, Subtype.ext_iff, unitsMulComplexConjInv_apply, OneMemClass.coe_one,
    mul_inv_eq_one, eq_comm, unitsComplexConj_eq_self_iff]
-- 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
x : (𝓞 K)ˣ
h :
  Eq (α := ↥(torsion K)) ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) x : ↥(torsion K))
      (1 : ↥(torsion K)) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
h₁ :
  Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (↑((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) x) : (𝓞 K)ˣ) (↑1 : (𝓞 K)ˣ) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
h₂ :
  HMul.hMul (β := (𝓞 K)ˣ) x (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) x)⁻¹ : (𝓞 K)ˣ) = (↑1 : (𝓞 K)ˣ) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (MonoidHom.ker (unitsMulComplexConjInv K)) x ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
have h₃ : HMul.hMul (β := (𝓞 K)ˣ) x (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) x)⁻¹ : (𝓞 K)ˣ) = 1 ↔
  Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
Tactic: rw [MonoidHom.mem_ker, Subtype.ext_iff, unitsMulComplexConjInv_apply, OneMemClass.coe_one,
    mul_inv_eq_one, eq_comm, unitsComplexConj_eq_self_iff]
-- 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
x : (𝓞 K)ˣ
h :
  Eq (α := ↥(torsion K)) ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) x : ↥(torsion K))
      (1 : ↥(torsion K)) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
h₁ :
  Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (↑((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) x) : (𝓞 K)ˣ) (↑1 : (𝓞 K)ˣ) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
h₂ :
  HMul.hMul (β := (𝓞 K)ˣ) x (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) x)⁻¹ : (𝓞 K)ˣ) = (↑1 : (𝓞 K)ˣ) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
h₃ :
  HMul.hMul (β := (𝓞 K)ˣ) x (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) x)⁻¹ : (𝓞 K)ˣ) = 1 ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (MonoidHom.ker (unitsMulComplexConjInv K)) x ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
have h₄ : x = (unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) x ↔ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
Tactic: rw [MonoidHom.mem_ker, Subtype.ext_iff, unitsMulComplexConjInv_apply, OneMemClass.coe_one,
    mul_inv_eq_one, eq_comm, unitsComplexConj_eq_self_iff]
-- 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
x : (𝓞 K)ˣ
h :
  Eq (α := ↥(torsion K)) ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) x : ↥(torsion K))
      (1 : ↥(torsion K)) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
h₁ :
  Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (↑((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) x) : (𝓞 K)ˣ) (↑1 : (𝓞 K)ˣ) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
h₂ :
  HMul.hMul (β := (𝓞 K)ˣ) x (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) x)⁻¹ : (𝓞 K)ˣ) = (↑1 : (𝓞 K)ˣ) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
h₃ :
  HMul.hMul (β := (𝓞 K)ˣ) x (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) x)⁻¹ : (𝓞 K)ˣ) = 1 ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
h₄ : x = (unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) x ↔ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (MonoidHom.ker (unitsMulComplexConjInv K)) x ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
have h₅ : (unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) x = x ↔ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
Tactic: rw [MonoidHom.mem_ker, Subtype.ext_iff, unitsMulComplexConjInv_apply, OneMemClass.coe_one,
    mul_inv_eq_one, eq_comm, unitsComplexConj_eq_self_iff]
-- 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
x : (𝓞 K)ˣ
h :
  Eq (α := ↥(torsion K)) ((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) x : ↥(torsion K))
      (1 : ↥(torsion K)) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
h₁ :
  Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (↑((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) x) : (𝓞 K)ˣ) (↑1 : (𝓞 K)ˣ) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
h₂ :
  HMul.hMul (β := (𝓞 K)ˣ) x (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) x)⁻¹ : (𝓞 K)ˣ) = (↑1 : (𝓞 K)ˣ) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
h₃ :
  HMul.hMul (β := (𝓞 K)ˣ) x (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) x)⁻¹ : (𝓞 K)ˣ) = 1 ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
h₄ : x = (unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) x ↔ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
h₅ : (unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) x = x ↔ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (MonoidHom.ker (unitsMulComplexConjInv K)) x ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
have h₆ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x ↔ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
Tactic: rw [MonoidHom.mem_ker, Subtype.ext_iff, unitsMulComplexConjInv_apply, OneMemClass.coe_one,
    mul_inv_eq_one, eq_comm, unitsComplexConj_eq_self_iff]