awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
u : (𝓞 K)ˣ
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) u ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ), (algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) (↑v : 𝓞 ↥K⁺) = (↑u : 𝓞 K)

Tactic:
simp [realUnits, MonoidHom.mem_range, RingHom.toMonoidHom_eq_coe, Units.ext_iff]

Premises used: Units.ext_iff, RingHom.toMonoidHom_eq_coe, MonoidHom.mem_range, 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 : 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)
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)
⊢ (unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u = u ↔ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) u

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]

Premises used: Units.ext_iff, RingEquiv.coe_toMulEquiv, AlgEquiv.coe_ringEquiv, NumberField.IsCMField.mem_realUnits_iff, NumberField.RingOfIntegers.mapRingEquiv_apply, NumberField.RingOfIntegers.ext_iff, NumberField.IsCMField.Units.complexConj_eq_self_iff, Units.coe_mapEquiv
-- 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
ζ : ↥(torsion K)
φ : K →+* ℂ := Classical.choice ⋯
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) : ℂ)
⊢ 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)

Tactic:
apply φ.injective

Premises used: RingHom.injective
-- 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
ζ : ↥(torsion K)
φ : K →+* ℂ := Classical.choice ⋯
a :
  Membership.mem (α := ℂˣ) (γ := Subgroup ℂˣ) (rootsOfUnity (torsionOrder K) ℂ)
    ((Units.complexEmbedding φ : (a : (𝓞 K)ˣ) → ℂˣ) (↑ζ : (𝓞 K)ˣ) : ℂˣ)
⊢ 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:
rw [complexEmbedding_complexConj, ← Units.complexEmbedding_apply,
    Complex.conj_rootsOfUnity (n := torsionOrder K), Units.val_inv_eq_inv_val,
    Units.complexEmbedding_apply, map_inv₀]

Premises used: Complex.conj_rootsOfUnity, Units.val_inv_eq_inv_val, map_inv₀, NumberField.IsCMField.complexEmbedding_complexConj, NumberField.Units.complexEmbedding_apply
-- 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
ζ : ↥(torsion K)
φ : K →+* ℂ := Classical.choice ⋯
⊢ Membership.mem (α := ℂˣ) (γ := Subgroup ℂˣ) (rootsOfUnity (torsionOrder K) ℂ)
    ((Units.complexEmbedding φ : (a : (𝓞 K)ˣ) → ℂˣ) (↑ζ : (𝓞 K)ˣ) : ℂˣ)

Tactic:
map_complexEmbedding_torsion K φ ▸ Subgroup.apply_coe_mem_map _ _ _

Premises used: Subgroup.apply_coe_mem_map, NumberField.Units.map_complexEmbedding_torsion, Eq.rec
-- 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
ζ : ↥(torsion K)
φ : K →+* ℂ := Classical.choice ⋯
⊢ Membership.mem (α := ℂˣ) (γ := Subgroup ℂˣ) (rootsOfUnity (torsionOrder K) ℂ)
    ((Units.complexEmbedding φ : (a : (𝓞 K)ˣ) → ℂˣ) (↑ζ : (𝓞 K)ˣ) : ℂˣ)

Tactic:
exact map_complexEmbedding_torsion K φ ▸ Subgroup.apply_coe_mem_map _ _ _
-- 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
ζ : ↥(torsion K)
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)ˣ))
⊢ (unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) (↑ζ : (𝓞 K)ˣ) = (↑ζ⁻¹ : (𝓞 K)ˣ)

Tactic:
apply coe_injective

Premises used: NumberField.Units.coe_injective
-- 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
ζ : ↥(torsion K)
⊢ 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:
simp
-- 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)ˣ
x : InfinitePlace K
⊢ Eq (α := ℝ)
    ((x : (a : K) → ℝ)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (↑(HMul.hMul (β := (𝓞 K)ˣ) u (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u)⁻¹ : (𝓞 K)ˣ)) : 𝓞 K) :
          K) :
      ℝ)
    (1 : ℝ)

Tactic:
simp
-- 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
⊢ Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x)
      (HMul.hMul (α := (𝓞 K)ˣ) 1 ((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) 1)⁻¹) ⋯ =
    1

Tactic:
simp
-- 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)ˣ
_ :
  ∀ (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)ˣ)) ⋯
⊢ ∀ (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)ˣ)) ⋯

Tactic:
_
-- 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 y : (𝓞 K)ˣ
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)ˣ)
⊢ 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)ˣ)) ⋯

Tactic:
rw [MulMemClass.mk_mul_mk, Subtype.mk_eq_mk]

Premises used: Subtype.mk_eq_mk, MulMemClass.mk_mul_mk
-- 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 y : (𝓞 K)ˣ
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)ˣ)))
⊢ 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:
apply coe_injective

Premises used: NumberField.Units.coe_injective
-- 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 y : (𝓞 K)ˣ
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)
⊢ 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:
simp only [map_mul, mul_inv_rev, Units.val_mul, map_units_inv]

Premises used: map_units_inv, map_mul, mul_inv_rev, Units.val_mul
-- 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 y : (𝓞 K)ˣ
⊢ 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:
ring
-- 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)ˣ
⊢ (↑((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) u) : (𝓞 K)ˣ) =
    HMul.hMul (β := (𝓞 K)ˣ) u (((unitsComplexConj K : (a : (𝓞 K)ˣ) → (𝓞 K)ˣ) u)⁻¹ : (𝓞 K)ˣ)

Tactic:
rfl

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
ζ : ↥(torsion K)
⊢ (↑((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) (↑ζ : (𝓞 K)ˣ)) : (𝓞 K)ˣ) =
    (↑(HPow.hPow (β := ℕ) ζ 2) : (𝓞 K)ˣ)

Tactic:
simp [unitsMulComplexConjInv_apply, unitsComplexConj_torsion, pow_two]

Premises used: NumberField.IsCMField.unitsComplexConj_torsion, pow_two, NumberField.IsCMField.unitsMulComplexConjInv_apply
-- 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
rw :
  Eq.{u_1 + 1} (α := Subgroup ↥(torsion K))
    (MonoidHom.range (G := ↥(torsion K)) (MonoidHom.restrict (unitsMulComplexConjInv K) (torsion K)))
    (MonoidHom.range (powMonoidHom 2))
⊢ Eq (α := Subgroup ↥(torsion K)) (Subgroup.map (unitsMulComplexConjInv K) (torsion K))
    (MonoidHom.range (powMonoidHom 2))

Tactic:
rw [← MonoidHom.restrict_range]

Premises used: MonoidHom.restrict_range
-- 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
ζ : ↥(torsion K)
⊢ Eq (α := ↥(torsion K))
    ((MonoidHom.restrict (unitsMulComplexConjInv K) (torsion K) : (a : ↥(torsion K)) → ↥(torsion K)) ζ : ↥(torsion K))
    ((powMonoidHom 2 : (a : ↥(torsion K)) → ↥(torsion K)) ζ : ↥(torsion K))

Tactic:
simp
-- 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
⊢ Eq.{u_1 + 1} (α := Subgroup ↥(torsion K))
    (MonoidHom.range (G := ↥(torsion K)) (MonoidHom.restrict (unitsMulComplexConjInv K) (torsion K)))
    (MonoidHom.range (powMonoidHom 2))

Tactic:
exact congr_arg (MonoidHom.range ·) (MonoidHom.ext fun ζ ↦ by simp)

Premises used: MonoidHom.range, MonoidHom.ext, congr_arg
-- 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 :
  ∀ (x : (𝓞 K)ˣ),
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (MonoidHom.ker (unitsMulComplexConjInv K)) x ↔
      Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits K) x
⊢ Eq (α := Subgroup (𝓞 K)ˣ) (MonoidHom.ker (unitsMulComplexConjInv K)) (realUnits K)

Tactic:
ext
-- 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)ˣ
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
h₆ h₇ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (realUnits 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

Tactic:
rw [MonoidHom.mem_ker, Subtype.ext_iff, unitsMulComplexConjInv_apply, OneMemClass.coe_one,
    mul_inv_eq_one, eq_comm, unitsComplexConj_eq_self_iff]

Premises used: mul_inv_eq_one, OneMemClass.coe_one, MonoidHom.mem_ker, eq_comm, Subtype.ext_iff, NumberField.IsCMField.unitsMulComplexConjInv_apply, NumberField.IsCMField.unitsComplexConj_eq_self_iff
-- 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.index.{u_1} (G := ↥(torsion K)) (MonoidHom.range (powMonoidHom 2)) = 2
⊢ Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) ∣ 2

Tactic:
this ▸ Subgroup.index_dvd_of_le ?_

Premises used: Eq.rec, Subgroup.index_dvd_of_le
-- 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.index.{u_1} (G := ↥(torsion K)) (MonoidHom.range (powMonoidHom 2)) = 2
refine :
  LE.le (α := Subgroup ↥(torsion K)) (MonoidHom.range (powMonoidHom 2)) (MonoidHom.range (unitsMulComplexConjInv K))
⊢ Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) ∣ 2

Tactic:
refine this ▸ Subgroup.index_dvd_of_le ?_
-- 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.index.{u_1} (G := ↥(torsion K)) (MonoidHom.range (powMonoidHom 2)) = 2
ζ : ↥(torsion K)
⊢ Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (↑((unitsMulComplexConjInv K : (a : (𝓞 K)ˣ) → ↥(torsion K)) (↑ζ : (𝓞 K)ˣ)) : (𝓞 K)ˣ)
    (↑((powMonoidHom 2 : (a : ↥(torsion K)) → ↥(torsion K)) ζ) : (𝓞 K)ˣ)

Tactic:
simp [pow_two]

Premises used: pow_two
-- 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.index.{u_1} (G := ↥(torsion K)) (MonoidHom.range (powMonoidHom 2)) = 2
ζ : ↥(torsion K)
⊢ Membership.mem (α := ↥(torsion K)) (γ := Subgroup ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K))
    ((powMonoidHom 2 : (a : ↥(torsion K)) → ↥(torsion K)) ζ : ↥(torsion K))

Tactic:
exact ⟨ζ, Subtype.ext_iff.mpr (by simp [pow_two])⟩
-- 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 : Subgroup.index.{u_1} (G := ↥(torsion K)) (MonoidHom.range (powMonoidHom 2)) = 2
⊢ Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) ∣ 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])⟩
-- 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
rw : 2 ∣ Fintype.card.{u_1} ↥(torsion K)
⊢ Subgroup.index.{u_1} (G := ↥(torsion K)) (MonoidHom.range (powMonoidHom 2)) = 2

Tactic:
rw [IsCyclic.index_powMonoidHom_range, Nat.gcd_eq_right_iff_dvd, Nat.card_eq_fintype_card]

Premises used: IsCyclic.index_powMonoidHom_range, Nat.gcd_eq_right_iff_dvd, 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.two_dvd <| even_torsionOrder K

Premises used: Even.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.two_dvd <| even_torsionOrder K

Premises used: Even.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
rw :
  Subgroup.index (G := (𝓞 K)ˣ) (torsion K ⊔ realUnits K) *
      Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) =
    2
⊢ indexRealUnits K * Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) = 2

Tactic:
rw [indexRealUnits, sup_comm]

Premises used: NumberField.IsCMField.indexRealUnits, sup_comm
-- 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.index (G := (𝓞 K)ˣ) (torsion K ⊔ MonoidHom.ker (unitsMulComplexConjInv K)) *
      Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) =
    Subgroup.index (G := ↥(torsion K)) (Subgroup.map (unitsMulComplexConjInv K) (torsion K))

Tactic:
(Subgroup.index_map (torsion K) (unitsMulComplexConjInv K)).symm

Premises used: NumberField.Units.torsion, Subgroup.index_map, Eq.symm, 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 : Eq (α := Subgroup (𝓞 K)ˣ) (realUnits K) (MonoidHom.ker (unitsMulComplexConjInv K))
h₁ : 2 = Subgroup.index (G := ↥(torsion K)) (Subgroup.map (unitsMulComplexConjInv K) (torsion K))
⊢ Subgroup.index (G := (𝓞 K)ˣ) (torsion K ⊔ realUnits K) *
      Subgroup.index (G := ↥(torsion K)) (MonoidHom.range (unitsMulComplexConjInv K)) =
    2

Tactic:
convert! (Subgroup.index_map (torsion K) (unitsMulComplexConjInv K)).symm

Premises used: NumberField.Units.torsion, Subgroup.index_map, Eq.symm, 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 h₁ : Eq (α := Subgroup (𝓞 K)ˣ) (realUnits K) (realUnits K)
⊢ Eq (α := Subgroup (𝓞 K)ˣ) (realUnits K) (MonoidHom.ker (unitsMulComplexConjInv K))

Tactic:
rw [unitsMulComplexConjInv_ker]

Premises used: NumberField.IsCMField.unitsMulComplexConjInv_ker
-- 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 ∣ Nat.card.{u_1} ↥(torsion K)
⊢ 2 = Subgroup.index (G := ↥(torsion K)) (Subgroup.map (unitsMulComplexConjInv K) (torsion K))

Tactic:
rw [map_unitsMulComplexConjInv_torsion, IsCyclic.index_powMonoidHom_range, Nat.gcd_eq_right]

Premises used: IsCyclic.index_powMonoidHom_range, NumberField.IsCMField.map_unitsMulComplexConjInv_torsion, Nat.gcd_eq_right