awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
this : IsTotallyReal.{u_2} ↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))
⊢ IsQuadraticExtension (↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))) K

Tactic:
have : IsQuadraticExtension (algebraMap F K).fieldRange K :=
    { finrank_eq_two' :=
        (IsQuadraticExtension.finrank_eq_two F K) ▸ Algebra.finrank_eq_of_equiv_equiv
          (algebraMap F K).rangeRestrictFieldEquiv.symm (RingEquiv.refl K) (by ext; simp; rfl) }
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
this_1 : IsTotallyReal.{u_2} ↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))
this : IsQuadraticExtension (↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))) K
⊢ Eq (α := Subfield K) (RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K)) (maximalRealSubfield K)

Tactic:
eq_maximalRealSubfield K (algebraMap F K).fieldRange

Premises used: Algebra.algebraMap, NumberField.CMExtension.eq_maximalRealSubfield, RingHom.fieldRange
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
this_1 : IsTotallyReal.{u_2} ↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))
this : IsQuadraticExtension (↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))) K
⊢ Eq (α := Subfield K) (RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K)) (maximalRealSubfield K)

Tactic:
exact eq_maximalRealSubfield K (algebraMap F K).fieldRange

Premises used: Algebra.algebraMap, NumberField.CMExtension.eq_maximalRealSubfield, RingHom.fieldRange
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
x : F
⊢ Eq.{u_2 + 1} (α := K)
    ((↑(((equivMaximalRealSubfield F K : RingEquiv.{u_1, u_2} F ↥(maximalRealSubfield K)) :
              (a : F) → ↥(maximalRealSubfield K))
            x) :
        K) :
      K)
    ((algebraMap F K : (a : F) → K) x : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
x : ↥(maximalRealSubfield K)
⊢ Eq.{u_2 + 1} (α := K)
    ((algebraMap F K : (a : F) → K)
        ((RingEquiv.symm (equivMaximalRealSubfield F K) : (a : ↥(maximalRealSubfield K)) → F) x : F) :
      K)
    ((algebraMap (↥(maximalRealSubfield K)) K : (a : ↥(maximalRealSubfield K)) → K) x : K)

Tactic:
simpa using (equivMaximalRealSubfield_apply F K ((equivMaximalRealSubfield F K).symm x)).symm

Premises used: NumberField.CMExtension.equivMaximalRealSubfield_apply, NumberField.CMExtension.equivMaximalRealSubfield, Eq.symm, DFunLike.coe, RingEquiv.symm
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
a :
  ∀ (x : ↥(maximalRealSubfield K)),
    Eq (α := K)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap F K)
              (RingEquiv.toRingHom (RingEquiv.symm (CMExtension.equivMaximalRealSubfield F K))) :
            (a : ↥(maximalRealSubfield K)) → K)
          x :
        K)
      ((RingHom.comp (RingEquiv.toRingHom (RingEquiv.refl K)) (algebraMap (↥(maximalRealSubfield K)) K) :
            (a : ↥(maximalRealSubfield K)) → K)
          x :
        K)
⊢ Eq (α := ↥(maximalRealSubfield K) →+* K)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap F K)
      (RingEquiv.toRingHom (RingEquiv.symm (CMExtension.equivMaximalRealSubfield F K))))
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.refl K)) (algebraMap (↥(maximalRealSubfield K)) K))

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
x : ↥(maximalRealSubfield K)
⊢ Eq (α := K)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap F K)
            (RingEquiv.toRingHom (RingEquiv.symm (CMExtension.equivMaximalRealSubfield F K))) :
          (a : ↥(maximalRealSubfield K)) → K)
        x :
      K)
    ((RingHom.comp (RingEquiv.toRingHom (RingEquiv.refl K)) (algebraMap (↥(maximalRealSubfield K)) K) :
          (a : ↥(maximalRealSubfield K)) → K)
        x :
      K)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
inst_4 : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
rw : σ ≠ 1
⊢ Nat.card.{u_2} ↥(Subgroup.zpowers σ) = 2

Tactic:
rw [Nat.card_zpowers, orderOf_isConj_two_of_ne_one (hσ φ)]

Premises used: Nat.card_zpowers, NumberField.ComplexEmbedding.orderOf_isConj_two_of_ne_one
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
inst_4 : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
⊢ σ ≠ 1

Tactic:
(isConj_ne_one_iff (hσ φ)).mpr <| IsTotallyComplex.complexEmbedding_not_isReal φ

Premises used: Iff.mpr, NumberField.ComplexEmbedding.isConj_ne_one_iff, NumberField.IsTotallyComplex.complexEmbedding_not_isReal
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
inst_4 : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
⊢ σ ≠ 1

Tactic:
exact (isConj_ne_one_iff (hσ φ)).mpr <| IsTotallyComplex.complexEmbedding_not_isReal φ

Premises used: Iff.mpr, NumberField.ComplexEmbedding.isConj_ne_one_iff, NumberField.IsTotallyComplex.complexEmbedding_not_isReal
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
inst_4 : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
⊢ Nat.card.{u_2} ↥(Subgroup.zpowers σ) = 2

Tactic:
have hσ' : Nat.card (Subgroup.zpowers σ) = 2 := by
    rw [Nat.card_zpowers, orderOf_isConj_two_of_ne_one (hσ φ)]
    exact (isConj_ne_one_iff (hσ φ)).mpr <| IsTotallyComplex.complexEmbedding_not_isReal φ
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
inst_4 : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card.{u_2} ↥(Subgroup.zpowers σ) = 2
⊢ Nat.card.{u_2} ↥(Subgroup.zpowers σ) ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
inst_4 : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card.{u_2} ↥(Subgroup.zpowers σ) = 2
⊢ Finite.{u_2 + 1} ↥(Subgroup.zpowers σ)

Tactic:
have : Finite (Subgroup.zpowers σ) := Nat.finite_of_card_ne_zero (by positivity)
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
inst_4 : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card.{u_2} ↥(Subgroup.zpowers σ) = 2
this : Finite.{u_2 + 1} ↥(Subgroup.zpowers σ)
L : IntermediateField ℚ K := FixedPoints.intermediateField ↥(Subgroup.zpowers σ)
w : InfinitePlace ↥L
obtain :
  ∀ (W : InfinitePlace K),
    InfinitePlace.IsReal.{u_2} (K := ↥L)
      ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap (↥L) K) : InfinitePlace ↥L)) W)
⊢ w.IsReal

Tactic:
obtain ⟨W, rfl⟩ := w.comap_surjective (K := K)

Premises used: NumberField.InfinitePlace.comap_surjective, rfl
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
inst_4 : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card.{u_2} ↥(Subgroup.zpowers σ) = 2
this : Finite.{u_2 + 1} ↥(Subgroup.zpowers σ)
L : IntermediateField ℚ K := FixedPoints.intermediateField ↥(Subgroup.zpowers σ)
W : InfinitePlace K
rw : ComplexEmbedding.IsReal (K := ↥L) (W.embedding.comp (algebraMap (↥L) K))
⊢ InfinitePlace.IsReal (K := ↥L) (W.comap (algebraMap (↥L) K))

Tactic:
rw [← mk_embedding W, comap_mk, isReal_mk_iff]

Premises used: NumberField.InfinitePlace.comap_mk, NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.isReal_mk_iff
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
inst_4 : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card.{u_2} ↥(Subgroup.zpowers σ) = 2
this : Finite.{u_2 + 1} ↥(Subgroup.zpowers σ)
L : IntermediateField ℚ K := FixedPoints.intermediateField ↥(Subgroup.zpowers σ)
W : InfinitePlace K
⊢ ComplexEmbedding.IsReal (K := ↥L) (W.embedding.comp (algebraMap (↥L) K))

Tactic:
ComplexEmbedding.IsConj.isReal_comp
     (σ := IsGaloisGroup.mulEquivAlgEquiv (Subgroup.zpowers σ) L K ⟨σ, Subgroup.mem_zpowers σ⟩)
      (hσ W.embedding)

Premises used: NumberField.ComplexEmbedding.IsConj.isReal_comp, NumberField.InfinitePlace.embedding
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
inst_4 : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card.{u_2} ↥(Subgroup.zpowers σ) = 2
this : Finite.{u_2 + 1} ↥(Subgroup.zpowers σ)
L : IntermediateField ℚ K := FixedPoints.intermediateField ↥(Subgroup.zpowers σ)
W : InfinitePlace K
⊢ ComplexEmbedding.IsReal (K := ↥L) (W.embedding.comp (algebraMap (↥L) K))

Tactic:
exact ComplexEmbedding.IsConj.isReal_comp
     (σ := IsGaloisGroup.mulEquivAlgEquiv (Subgroup.zpowers σ) L K ⟨σ, Subgroup.mem_zpowers σ⟩)
      (hσ W.embedding)

Premises used: NumberField.ComplexEmbedding.IsConj.isReal_comp, NumberField.InfinitePlace.embedding
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
inst_4 : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card.{u_2} ↥(Subgroup.zpowers σ) = 2
this : Finite.{u_2 + 1} ↥(Subgroup.zpowers σ)
L : IntermediateField ℚ K := FixedPoints.intermediateField ↥(Subgroup.zpowers σ)
⊢ IsTotallyReal.{u_2} ↥L

Tactic:
have : IsTotallyReal L := ⟨fun w ↦ by
    obtain ⟨W, rfl⟩ := w.comap_surjective (K := K)
    dsimp only
    rw [← mk_embedding W, comap_mk, isReal_mk_iff]
    exact ComplexEmbedding.IsConj.isReal_comp
     (σ := IsGaloisGroup.mulEquivAlgEquiv (Subgroup.zpowers σ) L K ⟨σ, Subgroup.mem_zpowers σ⟩)
      (hσ W.embedding)⟩
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
inst_4 : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card.{u_2} ↥(Subgroup.zpowers σ) = 2
this_1 : Finite.{u_2 + 1} ↥(Subgroup.zpowers σ)
L : IntermediateField ℚ K := FixedPoints.intermediateField ↥(Subgroup.zpowers σ)
this : IsTotallyReal.{u_2} ↥L
rw : Nat.card.{u_2} ↥(Subgroup.zpowers σ) = 2
rw₁ rw₂ : Eq (α := ℕ) 2 2
⊢ Module.finrank (↥L) K = 2

Tactic:
rw [IsGaloisGroup.finrank_fixedPoints_eq_card_subgroup, hσ']

Premises used: IsGaloisGroup.finrank_fixedPoints_eq_card_subgroup
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
inst_4 : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card.{u_2} ↥(Subgroup.zpowers σ) = 2
this_1 : Finite.{u_2 + 1} ↥(Subgroup.zpowers σ)
L : IntermediateField ℚ K := FixedPoints.intermediateField ↥(Subgroup.zpowers σ)
this : IsTotallyReal.{u_2} ↥L
⊢ IsQuadraticExtension (↥L) K

Tactic:
have : IsQuadraticExtension L K := ⟨by
    rw [IsGaloisGroup.finrank_fixedPoints_eq_card_subgroup, hσ']⟩
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
inst_4 : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card.{u_2} ↥(Subgroup.zpowers σ) = 2
this_1 : Finite.{u_2 + 1} ↥(Subgroup.zpowers σ)
L : IntermediateField ℚ K := FixedPoints.intermediateField ↥(Subgroup.zpowers σ)
this_2 : IsTotallyReal.{u_2} ↥L
this : IsQuadraticExtension (↥L) K
⊢ IsCMField K

Tactic:
IsCMField.ofCMExtension L K

Premises used: Membership.mem, Subtype, NumberField.IsCMField.ofCMExtension
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
inst_4 : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card.{u_2} ↥(Subgroup.zpowers σ) = 2
this_1 : Finite.{u_2 + 1} ↥(Subgroup.zpowers σ)
L : IntermediateField ℚ K := FixedPoints.intermediateField ↥(Subgroup.zpowers σ)
this_2 : IsTotallyReal.{u_2} ↥L
this : IsQuadraticExtension (↥L) K
⊢ IsCMField K

Tactic:
exact IsCMField.ofCMExtension L K

Premises used: Membership.mem, Subtype, NumberField.IsCMField.ofCMExtension
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
inst_8 : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
⊢ ∃ (σ : Gal(K/ℚ)), ComplexEmbedding.IsConj φ σ

Tactic:
exists_isConj_of_isRamified <|
      isRamified_iff.mpr ⟨IsTotallyComplex.isComplex _, IsTotallyReal.isReal _⟩

Premises used: Iff.mpr, NumberField.InfinitePlace.exists_isConj_of_isRamified, NumberField.InfinitePlace.isRamified_iff, NumberField.IsTotallyComplex.isComplex, And.intro, NumberField.IsTotallyReal.isReal
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
inst_8 : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
obtain : ∀ (σ : Gal(K/ℚ)) (hσ₁ : ComplexEmbedding.IsConj φ σ), IsCMField K
⊢ IsCMField K

Tactic:
obtain ⟨σ, hσ₁⟩ : ∃ σ : Gal(K/ℚ), ComplexEmbedding.IsConj φ σ :=
    exists_isConj_of_isRamified <|
      isRamified_iff.mpr ⟨IsTotallyComplex.isComplex _, IsTotallyReal.isReal _⟩

Premises used: Iff.mpr, NumberField.InfinitePlace.exists_isConj_of_isRamified, NumberField.InfinitePlace.isRamified_iff, NumberField.IsTotallyComplex.isComplex, And.intro, NumberField.IsTotallyReal.isReal
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
inst_8 : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
ψ : K →+* ℂ
a :
  ∀ (x : ℚ), Eq (α := ℂ) ((φ.comp (algebraMap ℚ K) : (a : ℚ) → ℂ) x : ℂ) ((ψ.comp (algebraMap ℚ K) : (a : ℚ) → ℂ) x : ℂ)
⊢ φ.comp (algebraMap ℚ K) = ψ.comp (algebraMap ℚ K)

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
inst_8 : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
ψ : K →+* ℂ
x : ℚ
⊢ Eq (α := ℂ) ((φ.comp (algebraMap ℚ K) : (a : ℚ) → ℂ) x : ℂ) ((ψ.comp (algebraMap ℚ K) : (a : ℚ) → ℂ) x : ℂ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
inst_8 : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
ψ : K →+* ℂ
obtain : ∀ (ν : Gal(K/ℚ)), ComplexEmbedding.IsConj (φ.comp (↑ν.symm : K →+* K)) σ
⊢ ComplexEmbedding.IsConj ψ σ

Tactic:
obtain ⟨ν, rfl⟩ := exists_comp_symm_eq_of_comp_eq (k := ℚ) φ ψ (by ext; simp)

Premises used: rfl, NumberField.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
inst_8 : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
ν : Gal(K/ℚ)
⊢ σ = ν.symm⁻¹ * σ * ν.symm

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
inst_8 : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
ν : Gal(K/ℚ)
rw : ComplexEmbedding.IsConj (φ.comp (↑ν.symm : K →+* K)) (ν.symm⁻¹ * σ * ν.symm)
⊢ ComplexEmbedding.IsConj (φ.comp (↑ν.symm : K →+* K)) σ

Tactic:
rw [show σ = ν.symm⁻¹ * σ * ν.symm by simp]
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
inst_8 : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
ν : Gal(K/ℚ)
⊢ ComplexEmbedding.IsConj (φ.comp (↑ν.symm : K →+* K)) (ν.symm⁻¹ * σ * ν.symm)

Tactic:
hσ₁.comp _

Premises used: NumberField.ComplexEmbedding.IsConj.comp
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
inst_8 : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
ν : Gal(K/ℚ)
⊢ ComplexEmbedding.IsConj (φ.comp (↑ν.symm : K →+* K)) (ν.symm⁻¹ * σ * ν.symm)

Tactic:
exact hσ₁.comp _

Premises used: NumberField.ComplexEmbedding.IsConj.comp
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
inst_8 : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
⊢ ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ

Tactic:
have hσ₂ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ := by
    intro ψ
    obtain ⟨ν, rfl⟩ := exists_comp_symm_eq_of_comp_eq (k := ℚ) φ ψ (by ext; simp)
    rw [show σ = ν.symm⁻¹ * σ * ν.symm by simp]
    exact hσ₁.comp _
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
inst_8 : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
hσ₂ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
⊢ IsCMField K

Tactic:
IsCMField.of_forall_isConj K hσ₂

Premises used: NumberField.IsCMField.of_forall_isConj
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : IsTotallyReal F
inst_2 : Field K
inst_3 : CharZero K
inst_4 : Algebra.IsIntegral ℚ K
inst_5 : IsTotallyComplex K
inst_6 : Algebra F K
inst_7 : IsQuadraticExtension F K
inst_8 : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
hσ₂ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
⊢ IsCMField K

Tactic:
exact IsCMField.of_forall_isConj K hσ₂

Premises used: NumberField.IsCMField.of_forall_isConj
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
S : Set ℕ
hS : ∃ n ∈ S, 2 < n
inst_2 : IsCyclotomicExtension S ℚ K
⊢ Algebra.IsIntegral ℚ K

Tactic:
have : Algebra.IsIntegral ℚ K := integral S ℚ K
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
S : Set ℕ
hS : ∃ n ∈ S, 2 < n
inst_2 : IsCyclotomicExtension S ℚ K
this : Algebra.IsIntegral ℚ K
obtain : ∀ (n : ℕ) (hn₁ : n ∈ S) (hn₂ : 2 < n), IsCMField K
⊢ IsCMField K

Tactic:
obtain ⟨n, hn₁, hn₂⟩ := hS
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
S : Set ℕ
inst_2 : IsCyclotomicExtension S ℚ K
this : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
⊢ n ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
S : Set ℕ
inst_2 : IsCyclotomicExtension S ℚ K
this : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
⊢ NeZero n

Tactic:
have : NeZero n := ⟨by positivity⟩
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
S : Set ℕ
inst_2 : IsCyclotomicExtension S ℚ K
this_1 : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
this : NeZero n
⊢ n ≠ 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
S : Set ℕ
inst_2 : IsCyclotomicExtension S ℚ K
this_1 : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
this : NeZero n
obtain : ∀ (ζ : K) (hζ : IsPrimitiveRoot ζ n), IsCMField K
⊢ IsCMField K

Tactic:
obtain ⟨ζ, hζ⟩ := exists_isPrimitiveRoot ℚ K hn₁ (by grind)

Premises used: Rat, IsCyclotomicExtension.exists_isPrimitiveRoot