awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsReal } → ℝ) +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₁ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₂ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, finrank ℝ ℂ =
    finrank ℚ K
rw₃ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, 2 = finrank ℚ K
rw₄ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ) 2 =
    finrank ℚ K
rw₅ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 =
    finrank ℚ K
rw₆ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 = finrank ℚ K
rw₇ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2 = finrank ℚ K
rw₈ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2 =
    finrank ℚ K
rw₉ : Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + nrComplexPlaces K * 2 = finrank ℚ K
rw₁₀ : Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + 2 * nrComplexPlaces K = finrank ℚ K
rw₁₁ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
      Fintype.card.{u_1} { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } =
    finrank ℚ K
rw₁₂ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
      Fintype.card.{u_1} { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } =
    Fintype.card.{u_1} (K →+* ℂ)
⊢ finrank.{0, u_1} ℝ (mixedSpace K) = finrank ℚ K
have rw₁₃ : Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
    (Fintype.card.{u_1} (K →+* ℂ) - Fintype.card.{u_1} { x : K →+* ℂ // ComplexEmbedding.IsReal x }) =
  Fintype.card.{u_1} (K →+* ℂ)
Tactic: classical
  rw [finrank_prod, finrank_pi, finrank_pi_fintype, Complex.finrank_real_complex, sum_const,
    card_univ, ← nrRealPlaces, ← nrComplexPlaces, ← card_real_embeddings, smul_eq_mul,
    mul_comm, ← card_complex_embeddings, ← NumberField.Embeddings.card K ℂ,
    Fintype.card_subtype_compl, Nat.add_sub_of_le (Fintype.card_subtype_le _)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsReal } → ℝ) +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₁ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      finrank.{0, u_1} ℝ ({ w : InfinitePlace K // w.IsComplex } → ℂ) =
    finrank ℚ K
rw₂ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, finrank ℝ ℂ =
    finrank ℚ K
rw₃ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } + ∑ i : { w : InfinitePlace K // w.IsComplex }, 2 = finrank ℚ K
rw₄ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (card.{u_1} (α := { w : InfinitePlace K // w.IsComplex }) univ) 2 =
    finrank ℚ K
rw₅ :
  Fintype.card.{u_1} { w : InfinitePlace K // w.IsReal } +
      HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 =
    finrank ℚ K
rw₆ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (Fintype.card.{u_1} { w : InfinitePlace K // w.IsComplex }) 2 = finrank ℚ K
rw₇ : nrRealPlaces K + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2 = finrank ℚ K
rw₈ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + HSMul.hSMul (β := ℕ) (nrComplexPlaces K) 2 =
    finrank ℚ K
rw₉ : Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + nrComplexPlaces K * 2 = finrank ℚ K
rw₁₀ : Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } + 2 * nrComplexPlaces K = finrank ℚ K
rw₁₁ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
      Fintype.card.{u_1} { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } =
    finrank ℚ K
rw₁₂ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
      Fintype.card.{u_1} { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ } =
    Fintype.card.{u_1} (K →+* ℂ)
rw₁₃ :
  Fintype.card.{u_1} { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } +
      (Fintype.card.{u_1} (K →+* ℂ) - Fintype.card.{u_1} { x : K →+* ℂ // ComplexEmbedding.IsReal x }) =
    Fintype.card.{u_1} (K →+* ℂ)
⊢ finrank.{0, u_1} ℝ (mixedSpace K) = finrank ℚ K
have rw₁₄ : Fintype.card.{u_1} (K →+* ℂ) = Fintype.card.{u_1} (K →+* ℂ)
Tactic: classical
  rw [finrank_prod, finrank_pi, finrank_pi_fintype, Complex.finrank_real_complex, sum_const,
    card_univ, ← nrRealPlaces, ← nrComplexPlaces, ← card_real_embeddings, smul_eq_mul,
    mul_comm, ← card_complex_embeddings, ← NumberField.Embeddings.card K ℂ,
    Fintype.card_subtype_compl, Nat.add_sub_of_le (Fintype.card_subtype_le _)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ NoAtoms.{u_1} (α := mixedSpace K) (m0 := MeasureSpace.toMeasurableSpace) volume
have obtain : ∀ (w : InfinitePlace K), NoAtoms.{u_1} (α := mixedSpace K) (m0 := MeasureSpace.toMeasurableSpace) volume
Tactic: obtain ⟨w⟩ := (inferInstance : Nonempty (InfinitePlace K))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
⊢ NoAtoms.{u_1} (α := mixedSpace K) (m0 := MeasureSpace.toMeasurableSpace) volume
have pos : ∀ (hw : w.IsReal), NoAtoms.{u_1} (α := mixedSpace K) (m0 := MeasureSpace.toMeasurableSpace) volume
Tactic: by_cases hw : IsReal w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
pos : ∀ (hw : w.IsReal), NoAtoms.{u_1} (α := mixedSpace K) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ NoAtoms.{u_1} (α := mixedSpace K) (m0 := MeasureSpace.toMeasurableSpace) volume
have neg : ∀ (hw : ¬w.IsReal), NoAtoms.{u_1} (α := mixedSpace K) (m0 := MeasureSpace.toMeasurableSpace) volume
Tactic: by_cases hw : IsReal w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : w.IsReal
⊢ NoAtoms.{u_1} (α := mixedSpace K) (m0 := MeasureSpace.toMeasurableSpace) volume
have this : NoAtoms.{u_1} (α := { w : InfinitePlace K // w.IsReal } → ℝ) (m0 := MeasureSpace.toMeasurableSpace) volume
Tactic: have : NoAtoms (volume : Measure ({w : InfinitePlace K // IsReal w} → ℝ)) := pi_noAtoms ⟨w, hw⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : ¬w.IsReal
⊢ NoAtoms.{u_1} (α := mixedSpace K) (m0 := MeasureSpace.toMeasurableSpace) volume
have this : NoAtoms.{u_1} (α := { w : InfinitePlace K // w.IsComplex } → ℂ) (m0 := MeasureSpace.toMeasurableSpace) volume
Tactic: have : NoAtoms (volume : Measure ({w : InfinitePlace K // IsComplex w} → ℂ)) :=
      pi_noAtoms ⟨w, not_isReal_iff_isComplex.mp hw⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : { w : InfinitePlace K // w.IsReal }
A : AffineSubspace ℝ (mixedSpace K) :=
  Submodule.toAffineSubspace
    {
      carrier :=
        {x : ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ) | x.1 w = 0},
      add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ Eq (α := ENNReal)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ENNReal) {x : mixedSpace K | x.1 w = 0} : ENNReal)
    (0 : ENNReal)
have convert! : ∀ (h : A = ⊤), False
Tactic: convert! Measure.addHaar_affineSubspace volume A fun h ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
⊢ ∀ (x y : (K →+* ℂ) → ℂ),
    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ((x + y) (↑w : InfinitePlace K).embedding).re,
        fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (x + y) (↑w : InfinitePlace K).embedding) =
      HAdd.hAdd (α := mixedSpace K)
        (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (x (↑w : InfinitePlace K).embedding).re,
          fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ x (↑w : InfinitePlace K).embedding)
        (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (y (↑w : InfinitePlace K).embedding).re,
          fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ y (↑w : InfinitePlace K).embedding)
have simp : ∀ (x y : (K →+* ℂ) → ℂ),
  ((fun (w : { w : InfinitePlace K // w.IsReal }) ↦
        (x (↑w : InfinitePlace K).embedding).re + (y (↑w : InfinitePlace K).embedding).re) =
      HAdd.hAdd (α := { w : InfinitePlace K // w.IsReal } → ℝ)
        (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (x (↑w : InfinitePlace K).embedding).re)
        fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (y (↑w : InfinitePlace K).embedding).re) ∧
    (fun (w : { w : InfinitePlace K // w.IsComplex }) ↦
        x (↑w : InfinitePlace K).embedding + y (↑w : InfinitePlace K).embedding) =
      HAdd.hAdd (α := { w : InfinitePlace K // w.IsComplex } → ℂ)
        (fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ x (↑w : InfinitePlace K).embedding)
        fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ y (↑w : InfinitePlace K).embedding
Tactic: simp only [Pi.add_apply, Complex.add_re, Prod.mk_add_mk, Prod.mk.injEq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
⊢ ∀ (m : ℝ) (x : (K →+* ℂ) → ℂ),
    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ((m • x) (↑w : InfinitePlace K).embedding).re,
        fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (m • x) (↑w : InfinitePlace K).embedding) =
      HSMul.hSMul (α := ℝ) (β := mixedSpace K) ((RingHom.id ℝ : (a : ℝ) → ℝ) m : ℝ)
        (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (x (↑w : InfinitePlace K).embedding).re,
          fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ x (↑w : InfinitePlace K).embedding)
have simp : ∀ (m : ℝ) (x : (K →+* ℂ) → ℂ),
  ((fun (w : { w : InfinitePlace K // w.IsReal }) ↦ m * (x (↑w : InfinitePlace K).embedding).re) =
      HSMul.hSMul (β := { w : InfinitePlace K // w.IsReal } → ℝ) m fun (w : { w : InfinitePlace K // w.IsReal }) ↦
        (x (↑w : InfinitePlace K).embedding).re) ∧
    (fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑m : ℂ) * x (↑w : InfinitePlace K).embedding) =
      HSMul.hSMul (β := { w : InfinitePlace K // w.IsComplex } → ℂ) m fun (w : { w : InfinitePlace K // w.IsComplex }) ↦
        x (↑w : InfinitePlace K).embedding
Tactic: simp only [Pi.smul_apply, Complex.real_smul, Complex.mul_re, Complex.ofReal_re,
      Complex.ofReal_im, zero_mul, sub_zero, RingHom.id_apply, Prod.smul_mk, Prod.mk.injEq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : K
⊢ Eq (α := mixedSpace K)
    ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) x) :
      mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K)
have simp : Eq (α := { w : InfinitePlace K // w.IsReal } → ℝ)
    (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ Complex.re (((↑w : InfinitePlace K).embedding : (a : K) → ℂ) x))
    ((Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsReal }) ↦ ℝ)
            fun (w : { w : InfinitePlace K // w.IsReal }) ↦ embedding_of_isReal sorry :
          (a : K) → { w : InfinitePlace K // w.IsReal } → ℝ)
        x :
      { w : InfinitePlace K // w.IsReal } → ℝ) ∧
  Eq (α := { w : InfinitePlace K // w.IsComplex } → ℂ)
    (fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (((↑w : InfinitePlace K).embedding : (a : K) → ℂ) x : ℂ))
    ((Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ)
            fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K).embedding :
          (a : K) → { w : InfinitePlace K // w.IsComplex } → ℂ)
        x :
      { w : InfinitePlace K // w.IsComplex } → ℂ)
Tactic: simp only [canonicalEmbedding, commMap, LinearMap.coe_mk, AddHom.coe_mk, Pi.ringHom_apply,
    mixedEmbedding, RingHom.prod_apply, Prod.mk.injEq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Disjoint (α := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ
      (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
        (⇑(canonicalEmbedding.latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)))
    (LinearMap.ker (commMap K))
have refine : ∀ (x : (K →+* ℂ) → ℂ)
  (h_mem :
    Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
      (Submodule.span ℝ
        (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
          (⇑(canonicalEmbedding.latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)))
      x)
  (h_zero :
    Eq (α := mixedSpace K) ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x : mixedSpace K) (0 : mixedSpace K)),
  x = 0
Tactic: refine LinearMap.disjoint_ker.mpr (fun x h_mem h_zero => ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
h_mem :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ
      (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
        (⇑(canonicalEmbedding.latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)))
    x
h_zero : Eq (α := mixedSpace K) ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x : mixedSpace K) (0 : mixedSpace K)
⊢ Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
have refine : Subset (α := Set ((K →+* ℂ) → ℂ))
  (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
    (⇑(canonicalEmbedding.latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
      (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ))
  (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))
Tactic: refine (Submodule.span_mono ?_) h_mem
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
h_mem :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ
      (Set.range (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
        (⇑(canonicalEmbedding.latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)))
    x
h_zero : Eq (α := mixedSpace K) ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x : mixedSpace K) (0 : mixedSpace K)
⊢ x = 0
have h_mem₁ : Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
  (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
Tactic: replace h_mem : x ∈ Submodule.span ℝ (Set.range (canonicalEmbedding K)) := by
    refine (Submodule.span_mono ?_) h_mem
    rintro _ ⟨i, rfl⟩
    exact ⟨integralBasis K i, (canonicalEmbedding.latticeBasis_apply K i).symm⟩
Cleared hypotheses: h_mem
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : Eq (α := mixedSpace K) ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x : mixedSpace K) (0 : mixedSpace K)
h_mem :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
⊢ x = 0
have h : ∀ (φ : K →+* ℂ), x φ = 0 φ
Tactic: ext1 φ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : Eq (α := mixedSpace K) ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x : mixedSpace K) (0 : mixedSpace K)
h_mem :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
φ : K →+* ℂ
⊢ x φ = 0
have pos : ∀ (hφ : ComplexEmbedding.IsReal φ), x φ = 0
Tactic: by_cases hφ : ComplexEmbedding.IsReal φ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : Eq (α := mixedSpace K) ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x : mixedSpace K) (0 : mixedSpace K)
h_mem :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
φ : K →+* ℂ
pos : ∀ (hφ : ComplexEmbedding.IsReal φ), x φ = 0
⊢ x φ = 0
have neg : ∀ (hφ : ¬ComplexEmbedding.IsReal φ), x φ = 0
Tactic: by_cases hφ : ComplexEmbedding.IsReal φ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : Eq (α := mixedSpace K) ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x : mixedSpace K) (0 : mixedSpace K)
h_mem :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ x φ = 0
have pos : (x φ).re = Complex.re 0
Tactic: apply Complex.ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : Eq (α := mixedSpace K) ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x : mixedSpace K) (0 : mixedSpace K)
h_mem :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
pos : (x φ).re = Complex.re 0
⊢ x φ = 0
have pos₁ : (x φ).im = Complex.im 0
Tactic: apply Complex.ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : Eq (α := mixedSpace K) ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x : mixedSpace K) (0 : mixedSpace K)
h_mem :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ (x φ).re = Complex.re 0
have pos : ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x).1
    (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (InfinitePlace.mk φ) sorry) =
  Complex.re 0
Tactic: rw [← embedding_mk_eq_of_isReal hφ, ← commMap_apply_of_isReal K x ⟨φ, hφ, rfl⟩]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : Eq (α := mixedSpace K) ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x : mixedSpace K) (0 : mixedSpace K)
h_mem :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ (x φ).im = Complex.im 0
have pos : (x φ).im = 0
Tactic: rw [Complex.zero_im, ← Complex.conj_eq_iff_im, canonicalEmbedding.conj_apply _ h_mem,
        ComplexEmbedding.isReal_iff.mp hφ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : Eq (α := mixedSpace K) ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x : mixedSpace K) (0 : mixedSpace K)
h_mem :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
pos : (x φ).im = 0
⊢ (x φ).im = Complex.im 0
have pos₁ : (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x φ
Tactic: rw [Complex.zero_im, ← Complex.conj_eq_iff_im, canonicalEmbedding.conj_apply _ h_mem,
        ComplexEmbedding.isReal_iff.mp hφ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : Eq (α := mixedSpace K) ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x : mixedSpace K) (0 : mixedSpace K)
h_mem :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
pos : (x φ).im = 0
pos₁ : (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x φ
⊢ (x φ).im = Complex.im 0
have pos₂ : x (ComplexEmbedding.conjugate φ) = x φ
Tactic: rw [Complex.zero_im, ← Complex.conj_eq_iff_im, canonicalEmbedding.conj_apply _ h_mem,
        ComplexEmbedding.isReal_iff.mp hφ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : Eq (α := mixedSpace K) ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x : mixedSpace K) (0 : mixedSpace K)
h_mem :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
pos : (x φ).im = 0
pos₁ : (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x φ
pos₂ : x (ComplexEmbedding.conjugate φ) = x φ
⊢ (x φ).im = Complex.im 0
have pos₃ : x φ = x φ
Tactic: rw [Complex.zero_im, ← Complex.conj_eq_iff_im, canonicalEmbedding.conj_apply _ h_mem,
        ComplexEmbedding.isReal_iff.mp hφ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : Eq (α := mixedSpace K) ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x : mixedSpace K) (0 : mixedSpace K)
h_mem :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
⊢ x φ = 0
have this : Eq (α := ℂ)
  ((fun (x : mixedSpace K) ↦ x.2) ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x)
    (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) (InfinitePlace.mk φ) sorry))
  ((fun (x : mixedSpace K) ↦ x.2) 0 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) (InfinitePlace.mk φ) sorry))
Tactic: have := congrFun (congrArg (fun x => x.2) h_zero) ⟨InfinitePlace.mk φ, ⟨φ, hφ, rfl⟩⟩