awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
hw : ¬w.IsReal
this : NoAtoms.{u_1} (α := { w : InfinitePlace K // w.IsComplex } → ℂ) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ NoAtoms.{u_1} (α := mixedSpace K) (m0 := MeasureSpace.toMeasurableSpace) volume

Tactic:
exact prod.instNoAtoms_snd

Premises used: MeasureTheory.Measure.prod.instNoAtoms_snd
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : { w : InfinitePlace K // w.IsReal }
⊢ ∀ {a b : ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)},
    Membership.mem (γ := Set (({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)))
        {x : ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ) | x.1 w = 0} a →
      Membership.mem (γ :=
          Set (({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)))
          {x : ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ) | x.1 w = 0} b →
        Membership.mem (γ :=
          Set (({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)))
          {x : ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ) | x.1 w = 0}
          (a + b)

Tactic:
simp_all
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : { w : InfinitePlace K // w.IsReal }
⊢ ∀ (c : ℝ) {x : ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)},
    Membership.mem (γ := Set (({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)))
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup
            {
              carrier :=
                {x : ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ) |
                  x.1 w = 0},
              add_mem' := ⋯, zero_mem' := ⋯ }))
        x →
      Membership.mem (γ :=
        Set (({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)))
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup
            {
              carrier :=
                {x : ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ) |
                  x.1 w = 0},
              add_mem' := ⋯, zero_mem' := ⋯ }))
        (c • x)

Tactic:
simp_all
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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 (({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ))) :
          (a : Set (({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ))) →
            ENNReal)
        (↑A : Set (({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ))) :
      ENNReal)
    (0 : ENNReal)

Tactic:
Measure.addHaar_affineSubspace volume A fun h ↦ ?_

Premises used: MeasureTheory.Measure.addHaar_affineSubspace, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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' := ⋯ }
convert! : ∀ (h : A = ⊤), False
⊢ Eq (α := ENNReal)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ENNReal) {x : mixedSpace K | x.1 w = 0} : ENNReal)
    (0 : ENNReal)

Tactic:
convert! Measure.addHaar_affineSubspace volume A fun h ↦ ?_

Premises used: MeasureTheory.Measure.addHaar_affineSubspace, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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' := ⋯ }
h : A = ⊤
⊢ False

Tactic:
simpa [A] using (h ▸ Set.mem_univ _ : 1 ∈ A)

Premises used: Eq.rec, Set.mem_univ, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
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
⊢ ∀ (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)

Tactic:
simp only [Pi.add_apply, Complex.add_re, Prod.mk_add_mk, Prod.mk.injEq]

Premises used: Prod.mk_add_mk, Complex.add_re, Pi.add_apply, Prod.mk.injEq
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
⊢ ∀ (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:
fun _ _ => ⟨rfl, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
⊢ ∀ (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:
exact fun _ _ => ⟨rfl, rfl⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
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
⊢ ∀ (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)

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]

Premises used: Complex.real_smul, Complex.mul_re, RingHom.id_apply, sub_zero, MulZeroClass.zero_mul, Prod.mk.injEq, Complex.ofReal_re, Prod.smul_mk, Complex.ofReal_im, Pi.smul_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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) =
        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:
fun _ _ => ⟨rfl, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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) =
        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:
exact fun _ _ => ⟨rfl, rfl⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : (K →+* ℂ) → ℂ
w : InfinitePlace K
hw : w.IsReal
⊢ ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x).1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw) =
    (x w.embedding).re

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : (K →+* ℂ) → ℂ
w : InfinitePlace K
hw : w.IsComplex
⊢ ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x).2
      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw) =
    x w.embedding

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : K
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 ⋯ :
            (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 } → ℂ)
⊢ 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)

Tactic:
simp only [canonicalEmbedding, commMap, LinearMap.coe_mk, AddHom.coe_mk, Pi.ringHom_apply,
    mixedEmbedding, RingHom.prod_apply, Prod.mk.injEq]

Premises used: LinearMap.coe_mk, NumberField.mixedEmbedding, NumberField.mixedEmbedding.commMap, Prod.mk.injEq, Pi.ringHom_apply, RingHom.prod_apply, NumberField.canonicalEmbedding, AddHom.coe_mk
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : K
⊢ 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 ⋯ :
            (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:
⟨rfl, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : K
⊢ 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 ⋯ :
            (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:
exact ⟨rfl, rfl⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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))

Tactic:
LinearMap.disjoint_ker.mpr (fun x h_mem h_zero => ?_)

Premises used: Iff.mpr, LinearMap.disjoint_ker
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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
⊢ 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))

Tactic:
refine LinearMap.disjoint_ker.mpr (fun x h_mem h_zero => ?_)

Premises used: Iff.mpr, LinearMap.disjoint_ker
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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

Tactic:
(Submodule.span_mono ?_) h_mem

Premises used: Submodule.span_mono
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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)
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 →+* ℂ) → ℂ))
⊢ Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x

Tactic:
refine (Submodule.span_mono ?_) h_mem

Premises used: Submodule.span_mono
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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)
i : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ))
    (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))
    (((canonicalEmbedding.latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)
        i :
      (K →+* ℂ) → ℂ)

Tactic:
⟨integralBasis K i, (canonicalEmbedding.latticeBasis_apply K i).symm⟩

Premises used: NumberField.canonicalEmbedding.latticeBasis_apply, NumberField.integralBasis, Set.Mem, setOf, Exists.intro, Set.range, Eq.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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)
i : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ Membership.mem (α := (K →+* ℂ) → ℂ) (γ := Set ((K →+* ℂ) → ℂ))
    (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))
    (((canonicalEmbedding.latticeBasis K : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → (K →+* ℂ) → ℂ)
        i :
      (K →+* ℂ) → ℂ)

Tactic:
exact ⟨integralBasis K i, (canonicalEmbedding.latticeBasis_apply K i).symm⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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

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⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
h : ∀ (φ : K →+* ℂ), x φ = 0 φ
⊢ x = 0

Tactic:
ext1 φ
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
neg : ∀ (hφ : ¬ComplexEmbedding.IsReal φ), x φ = 0
⊢ x φ = 0

Tactic:
by_cases hφ : ComplexEmbedding.IsReal φ

Premises used: NumberField.ComplexEmbedding.IsReal