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 : Algebra.IsIntegral ℚ K
refine : Nat.card.{u_1} ↥(Subgroup.zpowers (complexConj K)) = Nat.card.{u_1} Gal(K/↥K⁺)
⊢ Eq (α := Subgroup Gal(K/↥K⁺)) (Subgroup.zpowers (complexConj K)) ⊤

Tactic:
refine Subgroup.eq_top_of_card_eq _ ?_

Premises used: Subgroup.eq_top_of_card_eq
-- 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
rw : orderOf (G := Gal(K/↥K⁺)) (complexConj K) = Nat.card.{u_1} Gal(K/↥K⁺)
rw₁ : 2 = Nat.card.{u_1} Gal(K/↥K⁺)
rw₂ : 2 = Module.finrank (↥K⁺) K
rw₃ rw₄ : Eq (α := ℕ) 2 2
⊢ Nat.card.{u_1} ↥(Subgroup.zpowers (complexConj K)) = Nat.card.{u_1} Gal(K/↥K⁺)

Tactic:
rw [Nat.card_zpowers, orderOf_complexConj, IsGalois.card_aut_eq_finrank,
    IsQuadraticExtension.finrank_eq_two]

Premises used: IsGalois.card_aut_eq_finrank, NumberField.IsCMField.orderOf_complexConj, Algebra.IsQuadraticExtension.finrank_eq_two, Nat.card_zpowers
-- 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
x : K
⊢ (∀ (f : Gal(K/↥K⁺)), Membership.mem (γ := Subgroup Gal(K/↥K⁺)) ⊤ f → (f : (a : K) → K) x = x) ↔
    Membership.mem (γ := IntermediateField (↥K⁺) K) (IntermediateField.fixedField ⊤) x

Tactic:
(IntermediateField.mem_fixedField_iff (⊤ : Subgroup (K ≃ₐ[K⁺] K)) x).symm

Premises used: IntermediateField.mem_fixedField_iff, Top.top, Iff.symm
-- 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
x : K
h :
  (complexConj K : (a : K) → K) x = x ↔
    ∀ (f : Gal(K/↥K⁺)), Membership.mem (γ := Subgroup Gal(K/↥K⁺)) ⊤ f → (f : (a : K) → K) x = x
h₁ :
  Membership.mem (γ := Subfield K) K⁺ x ↔
    Membership.mem (γ := IntermediateField (↥K⁺) K) (IntermediateField.fixedField ⊤) x
⊢ (complexConj K : (a : K) → K) x = x ↔ Membership.mem (γ := Subfield K) K⁺ x

Tactic:
convert! (IntermediateField.mem_fixedField_iff (⊤ : Subgroup (K ≃ₐ[K⁺] K)) x).symm using 1
-- 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
x : K
h : (complexConj K : (a : K) → K) x = x ↔ ∀ (m : ℤ), (HPow.hPow (α := Gal(K/↥K⁺)) (complexConj K) m : (a : K) → K) x = x
⊢ (complexConj K : (a : K) → K) x = x ↔
    ∀ (f : Gal(K/↥K⁺)), Membership.mem (γ := Subgroup Gal(K/↥K⁺)) ⊤ f → (f : (a : K) → K) x = x

Tactic:
rw [← zpowers_complexConj_eq_top, Subgroup.forall_mem_zpowers]

Premises used: NumberField.IsCMField.zpowers_complexConj_eq_top, Subgroup.forall_mem_zpowers
-- 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
x : K
⊢ (complexConj K : (a : K) → K) x = x ↔ ∀ (m : ℤ), (HPow.hPow (α := Gal(K/↥K⁺)) (complexConj K) m : (a : K) → K) x = x

Tactic:
(MulAction.mem_fixedBy_zpowers_iff_mem_fixedBy (g := (complexConj K))).symm

Premises used: Set.Mem, setOf, MulAction.fixedBy, MulAction.mem_fixedBy_zpowers_iff_mem_fixedBy, Iff.symm
-- 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
x : K
⊢ (complexConj K : (a : K) → K) x = x ↔ ∀ (m : ℤ), (HPow.hPow (α := Gal(K/↥K⁺)) (complexConj K) m : (a : K) → K) x = x

Tactic:
exact (MulAction.mem_fixedBy_zpowers_iff_mem_fixedBy (g := (complexConj K))).symm

Premises used: MulAction.mem_fixedBy_zpowers_iff_mem_fixedBy, Iff.symm
-- 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
x : K
h :
  Membership.mem (γ := Subfield K) K⁺ x ↔
    Membership.mem (γ := Set K) (Set.range (ι := ↥K⁺) (⇑(algebraMap (↥K⁺) K) : (a : ↥K⁺) → K)) x
⊢ Membership.mem (γ := Subfield K) K⁺ x ↔
    Membership.mem (γ := IntermediateField (↥K⁺) K) (IntermediateField.fixedField ⊤) x

Tactic:
rw [IsGalois.fixedField_top, IntermediateField.mem_bot]

Premises used: IsGalois.fixedField_top, IntermediateField.mem_bot
-- 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
x : K
⊢ Membership.mem (γ := Subfield K) K⁺ x ↔
    Membership.mem (γ := Set K) (Set.range (ι := ↥K⁺) (⇑(algebraMap (↥K⁺) K) : (a : ↥K⁺) → K)) x

Tactic:
aesop
-- 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
x : 𝓞 K
rw : Membership.mem (γ := Subfield K) K⁺ (↑x : K) ↔ ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
⊢ (complexConj K : (a : K) → K) (↑x : K) = (↑x : K) ↔
    ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)

Tactic:
rw [complexConj_eq_self_iff]

Premises used: NumberField.IsCMField.complexConj_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 : Algebra.IsIntegral ℚ K
x : 𝓞 K
⊢ Membership.mem (γ := Subfield K) K⁺ (↑x : K) ↔ ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)

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

Premises used: NumberField.maximalRealSubfield, Membership.mem, NumberField.RingOfIntegers.val, _private.0.NumberField.IsCMField.RingOfIntegers.complexConj_eq_self_iff.match_1, 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 : Algebra.IsIntegral ℚ K
x : 𝓞 K
refine_1 :
  ∀ (h : Membership.mem (γ := Subfield K) K⁺ (↑x : K)),
    ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
refine_2 :
  (∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)) →
    ∀ (y : 𝓞 ↥K⁺) (hy : (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)),
      Membership.mem (γ := Subfield K) K⁺ (↑x : K)
⊢ Membership.mem (γ := Subfield K) K⁺ (↑x : K) ↔ ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨y, hy⟩ ↦ ?_⟩
-- 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
x : 𝓞 K
h : Membership.mem (γ := Subfield K) K⁺ (↑x : K)
⊢ IsIntegral ℤ (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subfield K) K⁺ x) (↑x : K) h)

Tactic:
have : IsIntegral ℤ (⟨x, h⟩ : K⁺) :=
      (isIntegral_algebraMap_iff (FaithfulSMul.algebraMap_injective K⁺ K)).mp x.isIntegral_coe
-- 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
x : 𝓞 K
h : Membership.mem (γ := Subfield K) K⁺ (↑x : K)
this : IsIntegral ℤ (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subfield K) K⁺ x) (↑x : K) h)
⊢ ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)

Tactic:
⟨⟨⟨x, h⟩, this⟩, ?_⟩

Premises used: NumberField.RingOfIntegers.val, Subtype.mk, 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 : Algebra.IsIntegral ℚ K
x : 𝓞 K
h : Membership.mem (γ := Subfield K) K⁺ (↑x : K)
this : IsIntegral ℤ (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subfield K) K⁺ x) (↑x : K) h)
refine_1 :
  (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K)
      (Subtype.mk (p := fun (x : ↥K⁺) ↦ Membership.mem (γ := Subalgebra ℤ ↥K⁺) (integralClosure ℤ ↥K⁺) x)
        (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subfield K) K⁺ x) (↑x : K) h) this) =
    (↑x : K)
⊢ ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)

Tactic:
refine ⟨⟨⟨x, h⟩, this⟩, ?_⟩
-- 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
x : 𝓞 K
h : Membership.mem (γ := Subfield K) K⁺ (↑x : K)
this : IsIntegral ℤ (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subfield K) K⁺ x) (↑x : K) h)
refine_1 :
  (algebraMap (↥K⁺) K : (a : ↥K⁺) → K)
      (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subfield K) K⁺ x) (↑x : K) h) =
    (↑x : K)
⊢ (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K)
      (Subtype.mk (p := fun (x : ↥K⁺) ↦ Membership.mem (γ := Subalgebra ℤ ↥K⁺) (integralClosure ℤ ↥K⁺) x)
        (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subfield K) K⁺ x) (↑x : K) h) this) =
    (↑x : K)

Tactic:
rw [IsScalarTower.algebraMap_apply (𝓞 K⁺) K⁺, RingOfIntegers.map_mk]

Premises used: NumberField.RingOfIntegers.map_mk
-- 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
x : 𝓞 K
h : Membership.mem (γ := Subfield K) K⁺ (↑x : K)
this : IsIntegral ℤ (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subfield K) K⁺ x) (↑x : K) h)
⊢ (algebraMap (↥K⁺) K : (a : ↥K⁺) → K)
      (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subfield K) K⁺ x) (↑x : K) h) =
    (↑x : K)

Tactic:
rfl
-- 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
x : 𝓞 K
h : ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
y : 𝓞 ↥K⁺
hy : (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
refine_2 :
  Membership.mem (α := K) (γ := Subfield K) K⁺
    ((algebraMap (↥K⁺) K : (a : ↥K⁺) → K) ((algebraMap (𝓞 ↥K⁺) ↥K⁺ : (a : 𝓞 ↥K⁺) → ↥K⁺) y : ↥K⁺) : K)
⊢ Membership.mem (γ := Subfield K) K⁺ (↑x : K)

Tactic:
rw [← hy, IsScalarTower.algebraMap_apply (𝓞 K⁺) K⁺]
-- 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
x : 𝓞 K
h : ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
y : 𝓞 ↥K⁺
hy : (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
⊢ Membership.mem (α := K) (γ := Subfield K) K⁺
    ((algebraMap (↥K⁺) K : (a : ↥K⁺) → K) ((algebraMap (𝓞 ↥K⁺) ↥K⁺ : (a : 𝓞 ↥K⁺) → ↥K⁺) y : ↥K⁺) : K)

Tactic:
SetLike.coe_mem _

Premises used: SetLike.coe_mem, Set.Mem, setOf
-- 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
x : 𝓞 K
h : ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
y : 𝓞 ↥K⁺
hy : (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
⊢ Membership.mem (α := K) (γ := Subfield K) K⁺
    ((algebraMap (↥K⁺) K : (a : ↥K⁺) → K) ((algebraMap (𝓞 ↥K⁺) ↥K⁺ : (a : 𝓞 ↥K⁺) → ↥K⁺) y : ↥K⁺) : K)

Tactic:
exact SetLike.coe_mem _

Premises used: SetLike.coe_mem
-- 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)ˣ
rw :
  (∃ (y : 𝓞 ↥K⁺),
      Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ),
      Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) (↑v : 𝓞 ↥K⁺) : K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
⊢ Eq (α := K) ((complexConj K : (a : K) → K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K) : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ),
      Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) (↑v : 𝓞 ↥K⁺) : K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)

Tactic:
rw [RingOfIntegers.complexConj_eq_self_iff, Units.coe_coe]

Premises used: NumberField.Units.coe_coe, NumberField.IsCMField.RingOfIntegers.complexConj_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 : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
h :
  ∃ (v : (𝓞 ↥K⁺)ˣ),
    Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) (↑v : 𝓞 ↥K⁺) : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
v : (𝓞 ↥K⁺)ˣ
hv :
  Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) (↑v : 𝓞 ↥K⁺) : K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
rw rw₁ :
  Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
⊢ Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) (↑v : 𝓞 ↥K⁺) : K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)

Tactic:
rw [hv]
-- 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)ˣ
refine :
  (∃ (y : 𝓞 ↥K⁺),
      Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) →
    ∀ (y : 𝓞 ↥K⁺)
      (hy :
        Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)),
      ∃ (v : (𝓞 ↥K⁺)ˣ),
        Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) (↑v : 𝓞 ↥K⁺) : K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
⊢ (∃ (y : 𝓞 ↥K⁺),
      Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) ↔
    ∃ (v : (𝓞 ↥K⁺)ˣ),
      Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) (↑v : 𝓞 ↥K⁺) : K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)

Tactic:
refine ⟨fun ⟨y, hy⟩ ↦ ?_, fun ⟨v, hv⟩ ↦ ⟨v, by rw [hv]⟩⟩
-- 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)ˣ
h_1 :
  ∃ (y : 𝓞 ↥K⁺),
    Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
y : 𝓞 ↥K⁺
hy : Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
h : IsUnit (M := 𝓞 K) ((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) y : 𝓞 K)
⊢ IsUnit y

Tactic:
apply IsUnit.of_map (algebraMap (𝓞 K⁺) (𝓞 K))
-- 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)ˣ
h :
  ∃ (y : 𝓞 ↥K⁺),
    Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
y : 𝓞 ↥K⁺
hy : Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
⊢ (algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) y = (↑u : 𝓞 K)

Tactic:
RingOfIntegers.ext hy

Premises used: NumberField.RingOfIntegers.ext
-- 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)ˣ
h :
  ∃ (y : 𝓞 ↥K⁺),
    Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
y : 𝓞 ↥K⁺
hy : Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
⊢ (algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) y = (↑u : 𝓞 K)

Tactic:
exact RingOfIntegers.ext hy

Premises used: NumberField.RingOfIntegers.ext
-- 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)ˣ
h_1 :
  ∃ (y : 𝓞 ↥K⁺),
    Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
y : 𝓞 ↥K⁺
hy : Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
h : IsUnit (↑u : 𝓞 K)
⊢ IsUnit (M := 𝓞 K) ((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) y : 𝓞 K)

Tactic:
rw [show algebraMap (𝓞 K⁺) (𝓞 K) y = u by exact RingOfIntegers.ext hy]
-- 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)ˣ
h :
  ∃ (y : 𝓞 ↥K⁺),
    Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
y : 𝓞 ↥K⁺
hy : Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
⊢ IsUnit (↑u : 𝓞 K)

Tactic:
u.isUnit

Premises used: Units.isUnit
-- 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)ˣ
h :
  ∃ (y : 𝓞 ↥K⁺),
    Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
y : 𝓞 ↥K⁺
hy : Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
⊢ IsUnit (↑u : 𝓞 K)

Tactic:
exact u.isUnit

Premises used: Units.isUnit
-- 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)ˣ
h :
  ∃ (y : 𝓞 ↥K⁺),
    Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
y : 𝓞 ↥K⁺
hy : Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
⊢ IsUnit y

Tactic:
have : IsUnit y := by
    apply IsUnit.of_map (algebraMap (𝓞 K⁺) (𝓞 K))
    rw [show algebraMap (𝓞 K⁺) (𝓞 K) y = u by exact RingOfIntegers.ext hy]
    exact u.isUnit
-- 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)ˣ
h :
  ∃ (y : 𝓞 ↥K⁺),
    Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
y : 𝓞 ↥K⁺
hy : Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
this : IsUnit y
⊢ Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) (↑this.unit : 𝓞 ↥K⁺) : K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)

Tactic:
simp [hy]
-- 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)ˣ
h :
  ∃ (y : 𝓞 ↥K⁺),
    Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
y : 𝓞 ↥K⁺
hy : Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
this : IsUnit y
⊢ ∃ (v : (𝓞 ↥K⁺)ˣ),
    Eq (α := K) ((algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) (↑v : 𝓞 ↥K⁺) : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)

Tactic:
exact ⟨this.unit, by simp [hy]⟩
-- 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
x x_1 : K
rw :
  HMul.hMul (α := K) (β := K) ((complexConj K : (a : K) → K) x : K) ((complexConj K : (a : K) → K) x_1 : K) =
    HMul.hMul (α := K) (β := K) ((complexConj K : (a : K) → K) x_1 : K) ((complexConj K : (a : K) → K) x : K)
rw₁ rw₂ :
  HMul.hMul (α := K) (β := K) ((complexConj K : (a : K) → K) x_1 : K) ((complexConj K : (a : K) → K) x : K) =
    HMul.hMul (α := K) (β := K) ((complexConj K : (a : K) → K) x_1 : K) ((complexConj K : (a : K) → K) x : K)
⊢ (complexConj K : (a : K) → K) (x * x_1) =
    HMul.hMul (α := K) (β := K) ((complexConj K : (a : K) → K) x_1 : K) ((complexConj K : (a : K) → K) x : K)

Tactic:
rw [map_mul, mul_comm]

Premises used: map_mul, mul_comm
-- 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
x x_1 : K
rw rw₁ :
  HAdd.hAdd (α := K) (β := K) ((complexConj K : (a : K) → K) x : K) ((complexConj K : (a : K) → K) x_1 : K) =
    HAdd.hAdd (α := K) (β := K) ((complexConj K : (a : K) → K) x : K) ((complexConj K : (a : K) → K) x_1 : K)
⊢ (complexConj K : (a : K) → K) (x + x_1) =
    HAdd.hAdd (α := K) (β := K) ((complexConj K : (a : K) → K) x : K) ((complexConj K : (a : K) → K) x_1 : K)

Tactic:
rw [map_add]

Premises used: map_add
-- 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
x : 𝓞 K
⊢ Eq (α := K) ((↑((ringOfIntegersComplexConj K : (a : 𝓞 K) → 𝓞 K) x) : K) : K)
    ((complexConj K : (a : K) → K) (↑x : K) : 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 : Algebra.IsIntegral ℚ K
x : 𝓞 K
⊢ (ringOfIntegersComplexConj K : (a : 𝓞 K) → 𝓞 K) x = x ↔
    Membership.mem (γ := Set (𝓞 K)) (Set.range (ι := 𝓞 ↥K⁺) (⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : (a : 𝓞 ↥K⁺) → 𝓞 K)) x

Tactic:
⟨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 : Algebra.IsIntegral ℚ K
x : 𝓞 K
refine_1 :
  ∀ (h : (ringOfIntegersComplexConj K : (a : 𝓞 K) → 𝓞 K) x = x),
    Membership.mem (γ := Set (𝓞 K)) (Set.range (ι := 𝓞 ↥K⁺) (⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : (a : 𝓞 ↥K⁺) → 𝓞 K)) x
refine_2 :
  Membership.mem (γ := Set (𝓞 K)) (Set.range (ι := 𝓞 ↥K⁺) (⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : (a : 𝓞 ↥K⁺) → 𝓞 K)) x →
    (ringOfIntegersComplexConj K : (a : 𝓞 K) → 𝓞 K) x = x
⊢ (ringOfIntegersComplexConj K : (a : 𝓞 K) → 𝓞 K) x = x ↔
    Membership.mem (γ := Set (𝓞 K)) (Set.range (ι := 𝓞 ↥K⁺) (⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : (a : 𝓞 ↥K⁺) → 𝓞 K)) x

Tactic:
refine ⟨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 : Algebra.IsIntegral ℚ K
x : 𝓞 K
h : (ringOfIntegersComplexConj K : (a : 𝓞 K) → 𝓞 K) x = x
⊢ ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)

Tactic:
rw [RingOfIntegers.ext_iff, coe_ringOfIntegersComplexConj,
      RingOfIntegers.complexConj_eq_self_iff] at h

Premises used: NumberField.IsCMField.coe_ringOfIntegersComplexConj, NumberField.RingOfIntegers.ext_iff, NumberField.IsCMField.RingOfIntegers.complexConj_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 : Algebra.IsIntegral ℚ K
x : 𝓞 K
h : ∃ (y : 𝓞 ↥K⁺), (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
refine_1 :
  ∀ (y : 𝓞 ↥K⁺) (hy : (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)),
    Membership.mem (γ := Set (𝓞 K)) (Set.range (ι := 𝓞 ↥K⁺) (⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : (a : 𝓞 ↥K⁺) → 𝓞 K)) x
⊢ Membership.mem (γ := Set (𝓞 K)) (Set.range (ι := 𝓞 ↥K⁺) (⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : (a : 𝓞 ↥K⁺) → 𝓞 K)) x

Tactic:
obtain ⟨y, hy⟩ := h
-- 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
x : 𝓞 K
y : 𝓞 ↥K⁺
hy : (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
⊢ Membership.mem (γ := Set (𝓞 K)) (Set.range (ι := 𝓞 ↥K⁺) (⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : (a : 𝓞 ↥K⁺) → 𝓞 K)) x

Tactic:
⟨y, RingOfIntegers.ext_iff.mpr hy⟩

Premises used: Iff.mpr, Set.Mem, setOf, Exists.intro, NumberField.RingOfIntegers.ext_iff, Set.range
-- 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
x : 𝓞 K
y : 𝓞 ↥K⁺
hy : (algebraMap (𝓞 ↥K⁺) K : (a : 𝓞 ↥K⁺) → K) y = (↑x : K)
⊢ Membership.mem (γ := Set (𝓞 K)) (Set.range (ι := 𝓞 ↥K⁺) (⇑(algebraMap (𝓞 ↥K⁺) (𝓞 K)) : (a : 𝓞 ↥K⁺) → 𝓞 K)) x

Tactic:
exact ⟨y, RingOfIntegers.ext_iff.mpr hy⟩
-- 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
y : 𝓞 ↥K⁺
⊢ Eq (α := 𝓞 K)
    ((ringOfIntegersComplexConj K : (a : 𝓞 K) → 𝓞 K) ((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) y) : 𝓞 K)
    ((algebraMap (𝓞 ↥K⁺) (𝓞 K) : (a : 𝓞 ↥K⁺) → 𝓞 K) y : 𝓞 K)

Tactic:
simp