awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
⊢ ¬L = ⊥
have refine_1 : ∀ (h : L = ⊥), maximalRealSubfield K ≤ E
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (hypothesis)
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
h : L = ⊥
⊢ maximalRealSubfield K ≤ E
have h₁ : (↑(E ⊔ maximalRealSubfield K) : Set K) = (↑⊥ : Set K)
Tactic: rw [← SetLike.coe_set_eq, Subfield.coe_toIntermediateField] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
h : (↑(E ⊔ maximalRealSubfield K) : Set K) = (↑⊥ : Set K)
⊢ maximalRealSubfield K ≤ E
have refine_1 : Set.range (ι := ↥E) (⇑(algebraMap (↥E) K) : (a : ↥E) → K) = (↑E : Set K)
Tactic: rw [← sup_eq_left, ← SetLike.coe_set_eq, h, IntermediateField.coe_bot]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (hypothesis)
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
⊢ False
have h' : E ⊔ maximalRealSubfield K = ⊤
Tactic: have h' : E ⊔ (maximalRealSubfield K) = ⊤ := by
    let L : IntermediateField E K := (E ⊔ (maximalRealSubfield K)).toIntermediateField
      (fun x ↦ (le_sup_left (a := E)) x.prop)
    have := ((IntermediateField.isSimpleOrder_of_finrank_prime E K
      (IsQuadraticExtension.finrank_eq_two E K ▸ Nat.prime_two)).eq_bot_or_eq_top L).resolve_left ?_
    · simpa [L] using congr_arg IntermediateField.toSubfield this
    · contrapose h
      rw [← SetLike.coe_set_eq, Subfield.coe_toIntermediateField] at h
      rw [← sup_eq_left, ← SetLike.coe_set_eq, h, IntermediateField.coe_bot]
      aesop
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (hypothesis)
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
h' : E ⊔ maximalRealSubfield K = ⊤
⊢ False
have this : Algebra.IsAlgebraic (↥(maximalRealSubfield K)) K
Tactic: have : Algebra.IsAlgebraic (maximalRealSubfield K) K :=
    Algebra.IsAlgebraic.tower_top (K := ℚ) (maximalRealSubfield K)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (hypothesis)
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
h' : E ⊔ maximalRealSubfield K = ⊤
this : Algebra.IsAlgebraic (↥(maximalRealSubfield K)) K
⊢ False
have this₁ : IsTotallyReal K
Tactic: have : IsTotallyReal K := (h' ▸ isTotallyReal_sup).ofRingEquiv Subring.topEquiv
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : Algebra.IsIntegral ℚ K
inst_3 : IsTotallyComplex K
E : Subfield K
inst_4 : IsTotallyReal.{u_2} ↥E
inst_5 : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
h' : E ⊔ maximalRealSubfield K = ⊤
this_1 : Algebra.IsAlgebraic (↥(maximalRealSubfield K)) K
this : IsTotallyReal K
⊢ False
have obtain : ∀ (w : InfinitePlace K), False
Tactic: obtain w : InfinitePlace K := Classical.choice (inferInstance : Nonempty _)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (hypothesis)
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
⊢ Eq (α := Subfield K) (RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K)) (maximalRealSubfield K)
have this : IsTotallyReal.{u_2} ↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))
Tactic: have := IsTotallyReal.ofRingEquiv (algebraMap F K).rangeRestrictFieldEquiv
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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))
⊢ Eq (α := ↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K)) →+* K)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap F K)
      (RingEquiv.toRingHom (RingEquiv.symm (RingHom.rangeRestrictFieldEquiv (algebraMap F K)))))
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.refl K))
      (algebraMap (↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))) K))
have a : ∀ (x : ↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))),
  Eq (α := K)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap F K)
            (RingEquiv.toRingHom (RingEquiv.symm (RingHom.rangeRestrictFieldEquiv (algebraMap F K)))) :
          (a : ↥(algebraMap F K).fieldRange) → K)
        x :
      K)
    ((RingHom.comp (RingEquiv.toRingHom (RingEquiv.refl K))
            (algebraMap (↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))) K) :
          (a : ↥(algebraMap F K).fieldRange) → K)
        x :
      K)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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))
x : ↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))
⊢ Eq (α := K)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap F K)
            (RingEquiv.toRingHom (RingEquiv.symm (RingHom.rangeRestrictFieldEquiv (algebraMap F K)))) :
          (a : ↥(algebraMap F K).fieldRange) → K)
        x :
      K)
    ((RingHom.comp (RingEquiv.toRingHom (RingEquiv.refl K))
            (algebraMap (↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))) K) :
          (a : ↥(algebraMap F K).fieldRange) → K)
        x :
      K)
have a : (↑x : K) =
  (algebraMap (↥(RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K))) K : (a : ↥(algebraMap F K).fieldRange) → K) x
Tactic: simp
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (hypothesis)
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))
⊢ Eq (α := Subfield K) (RingHom.fieldRange.{u_1, u_2} (K := F) (algebraMap F K)) (maximalRealSubfield K)
have this₁ : 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) }
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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
⊢ 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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
have rw : σ ≠ 1
Tactic: rw [Nat.card_zpowers, orderOf_isConj_two_of_ne_one (hσ φ)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (hypothesis)
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 ⋯
⊢ IsCMField K
have hσ' : 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 φ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (hypothesis)
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
⊢ IsCMField K
have this : Finite.{u_2 + 1} ↥(Subgroup.zpowers σ)
Tactic: have : Finite (Subgroup.zpowers σ) := Nat.finite_of_card_ne_zero (by positivity)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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
⊢ w.IsReal
have obtain : ∀ (W : InfinitePlace K),
  InfinitePlace.IsReal.{u_2} (K := ↥L)
    ((fun (x : InfinitePlace K) ↦ (x.comap (algebraMap (↥L) K) : InfinitePlace ↥L)) W)
Tactic: obtain ⟨W, rfl⟩ := w.comap_surjective (K := K)
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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
⊢ InfinitePlace.IsReal (K := ↥L) (W.comap (algebraMap (↥L) K))
have rw : ComplexEmbedding.IsReal (K := ↥L) (W.embedding.comp (algebraMap (↥L) K))
Tactic: rw [← mk_embedding W, comap_mk, isReal_mk_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (hypothesis)
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 σ)
⊢ IsCMField K
have this₁ : 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)⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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
⊢ Module.finrank (↥L) K = 2
have rw₁ : Eq (α := ℕ) 2 2
Tactic: rw [IsGaloisGroup.finrank_fixedPoints_eq_card_subgroup, hσ']
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (hypothesis)
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
⊢ IsCMField K
have this₁ : IsQuadraticExtension (↥L) K
Tactic: have : IsQuadraticExtension L K := ⟨by
    rw [IsGaloisGroup.finrank_fixedPoints_eq_card_subgroup, hσ']⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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 ⋯
⊢ IsCMField K
have obtain : ∀ (σ : Gal(K/ℚ)) (hσ₁ : ComplexEmbedding.IsConj φ σ), IsCMField K
Tactic: obtain ⟨σ, hσ₁⟩ : ∃ σ : Gal(K/ℚ), ComplexEmbedding.IsConj φ σ :=
    exists_isConj_of_isRamified <|
      isRamified_iff.mpr ⟨IsTotallyComplex.isComplex _, IsTotallyReal.isReal _⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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 →+* ℂ
⊢ φ.comp (algebraMap ℚ K) = ψ.comp (algebraMap ℚ K)
have a : ∀ (x : ℚ), Eq (α := ℂ) ((φ.comp (algebraMap ℚ K) : (a : ℚ) → ℂ) x : ℂ) ((ψ.comp (algebraMap ℚ K) : (a : ℚ) → ℂ) x : ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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 ψ σ
have obtain : ∀ (ν : Gal(K/ℚ)), ComplexEmbedding.IsConj (φ.comp (↑ν.symm : K →+* K)) σ
Tactic: obtain ⟨ν, rfl⟩ := exists_comp_symm_eq_of_comp_eq (k := ℚ) φ ψ (by ext; simp)
Cleared hypotheses: ψ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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)) σ
have rw : ComplexEmbedding.IsConj (φ.comp (↑ν.symm : K →+* K)) (ν.symm⁻¹ * σ * ν.symm)
Tactic: rw [show σ = ν.symm⁻¹ * σ * ν.symm by simp]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (hypothesis)
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 φ σ
⊢ IsCMField K
have hσ₂ : ∀ (φ : 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 _
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
S : Set ℕ
hS : ∃ n ∈ S, 2 < n
inst_2 : IsCyclotomicExtension S ℚ K
⊢ IsCMField K
have this : Algebra.IsIntegral ℚ K
Tactic: have : Algebra.IsIntegral ℚ K := integral S ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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
⊢ IsCMField K
have obtain : ∀ (n : ℕ) (hn₁ : n ∈ S) (hn₂ : 2 < n), IsCMField K
Tactic: obtain ⟨n, hn₁, hn₂⟩ := hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (hypothesis)
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
⊢ IsCMField K
have this₁ : NeZero n
Tactic: have : NeZero n := ⟨by positivity⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
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
⊢ IsCMField K
have obtain : ∀ (ζ : K) (hζ : IsPrimitiveRoot ζ n), IsCMField K
Tactic: obtain ⟨ζ, hζ⟩ := exists_isPrimitiveRoot ℚ K hn₁ (by grind)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (hypothesis)
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
ζ : K
hζ : IsPrimitiveRoot ζ n
⊢ IsTotallyComplex K
have this₁ : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
Tactic: have : IsCyclotomicExtension {n} ℚ ℚ⟮ζ⟯ := hζ.intermediateField_adjoin_isCyclotomicExtension ℚ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (hypothesis)
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_2 : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
this : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
⊢ IsTotallyComplex K
have this₁ : IsTotallyComplex.{u_1} ↥ℚ⟮ζ⟯
Tactic: have : IsTotallyComplex ℚ⟮ζ⟯ := isTotallyComplex ℚ⟮ζ⟯ hn₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (hypothesis)
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
ζ : K
hζ : IsPrimitiveRoot ζ n
⊢ IsCMField K
have this₁ : IsTotallyComplex K
Tactic: have : IsTotallyComplex K := by
    have : IsCyclotomicExtension {n} ℚ ℚ⟮ζ⟯ := hζ.intermediateField_adjoin_isCyclotomicExtension ℚ
    have : IsTotallyComplex ℚ⟮ζ⟯ := isTotallyComplex ℚ⟮ζ⟯ hn₂
    exact isTotallyComplex_of_algebra ℚ⟮ζ⟯ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (hypothesis)
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_2 : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
this : IsTotallyComplex K
⊢ IsCMField K
have this₁ : IsAbelianGalois ℚ K
Tactic: have := isAbelianGalois S ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
have refine_1 : ∀ (x : (K →+* ℂ) → ℂ)
  (h :
    Membership.mem (γ := Set ((K →+* ℂ) → ℂ)) (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))
      x),
  (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
Tactic: refine Submodule.span_induction ?_ ?_ (fun _ _ _ _ hx hy => ?_) (fun a _ _ hx => ?_) hx
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
refine_1 :
  ∀ (x : (K →+* ℂ) → ℂ)
    (h :
      Membership.mem (γ := Set ((K →+* ℂ) → ℂ)) (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))
        x),
    (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
have refine_2 : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (0 φ) : ℂ) (0 (ComplexEmbedding.conjugate φ) : ℂ)
Tactic: refine Submodule.span_induction ?_ ?_ (fun _ _ _ _ hx hy => ?_) (fun a _ _ hx => ?_) hx
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
refine_1 :
  ∀ (x : (K →+* ℂ) → ℂ)
    (h :
      Membership.mem (γ := Set ((K →+* ℂ) → ℂ)) (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))
        x),
    (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
refine_2 : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (0 φ) : ℂ) (0 (ComplexEmbedding.conjugate φ) : ℂ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
have refine_3 : ∀ (x x_1 : (K →+* ℂ) → ℂ),
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
      (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x →
    Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
        (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x_1 →
      ∀ (hx : (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x (ComplexEmbedding.conjugate φ))
        (hy : (starRingEnd ℂ : (a : ℂ) → ℂ) (x_1 φ) = x_1 (ComplexEmbedding.conjugate φ)),
        (starRingEnd ℂ : (a : ℂ) → ℂ) ((x + x_1) φ) = (x + x_1) (ComplexEmbedding.conjugate φ)
Tactic: refine Submodule.span_induction ?_ ?_ (fun _ _ _ _ hx hy => ?_) (fun a _ _ hx => ?_) hx