awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h : x ∈ A
hx : ∀ (a : { w : InfinitePlace K // w.IsReal }), ¬x.1 a = 0
w : { w : InfinitePlace K // w.IsReal }
hw : w ∈ signSet x
⊢ x.1 w < 0

Tactic:
exact lt_of_le_of_ne hw (hx w)

Premises used: lt_of_le_of_ne
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h : x ∈ A
hx : ∀ (a : { w : InfinitePlace K // w.IsReal }), ¬x.1 a = 0
w : { w : InfinitePlace K // w.IsReal }
hw : w ∉ signSet x
⊢ x.1 w > 0

Tactic:
lt_of_le_of_ne (lt_of_not_ge hw).le (Ne.symm (hx w))

Premises used: lt_of_not_ge, LT.lt.le, Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h : x ∈ A
hx : ∀ (a : { w : InfinitePlace K // w.IsReal }), ¬x.1 a = 0
w : { w : InfinitePlace K // w.IsReal }
hw : w ∉ signSet x
⊢ x.1 w > 0

Tactic:
exact lt_of_le_of_ne (lt_of_not_ge hw).le (Ne.symm (hx w))

Premises used: lt_of_not_ge, LT.lt.le, Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
inst_1 : NumberField K
nth_rewrite :
  ⋃ (s : Set { w : InfinitePlace K // w.IsReal }),
      (⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' plusPart A =ᶠ[ae (F := Measure (mixedSpace K)) volume]
    (⋃ (s : Set { w : InfinitePlace K // w.IsReal }), (⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) ∪
      A ∩ ⋃ (w : { w : InfinitePlace K // w.IsReal }), {x : mixedSpace K | x.1 w = 0}
⊢ ⋃ (s : Set { w : InfinitePlace K // w.IsReal }),
      (⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' plusPart A =ᶠ[ae (F := Measure (mixedSpace K)) volume]
    A

Tactic:
nth_rewrite 2 [← iUnion_negAt_plusPart_union A hA]

Premises used: NumberField.mixedEmbedding.iUnion_negAt_plusPart_union
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
inst_1 : NumberField K
⊢ ⋃ (s : Set { w : InfinitePlace K // w.IsReal }),
      (⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' plusPart A =ᶠ[ae (F := Measure (mixedSpace K)) volume]
    (⋃ (s : Set { w : InfinitePlace K // w.IsReal }), (⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) ∪
      A ∩ ⋃ (w : { w : InfinitePlace K // w.IsReal }), {x : mixedSpace K | x.1 w = 0}

Tactic:
(MeasureTheory.union_ae_eq_left_of_ae_eq_empty (ae_eq_empty.mpr ?_)).symm

Premises used: Iff.mpr, MeasureTheory.ae_eq_empty, MeasureTheory.union_ae_eq_left_of_ae_eq_empty, Filter.EventuallyEq.symm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
inst_1 : NumberField K
refine :
  Eq (α := ENNReal)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ENNReal)
        (A ∩ ⋃ (w : { w : InfinitePlace K // w.IsReal }), {x : mixedSpace K | x.1 w = 0}) :
      ENNReal)
    (0 : ENNReal)
⊢ ⋃ (s : Set { w : InfinitePlace K // w.IsReal }),
      (⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' plusPart A =ᶠ[ae (F := Measure (mixedSpace K)) volume]
    (⋃ (s : Set { w : InfinitePlace K // w.IsReal }), (⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) ∪
      A ∩ ⋃ (w : { w : InfinitePlace K // w.IsReal }), {x : mixedSpace K | x.1 w = 0}

Tactic:
refine (MeasureTheory.union_ae_eq_left_of_ae_eq_empty (ae_eq_empty.mpr ?_)).symm

Premises used: Iff.mpr, MeasureTheory.ae_eq_empty, MeasureTheory.union_ae_eq_left_of_ae_eq_empty, Filter.EventuallyEq.symm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
inst_1 : NumberField K
⊢ Eq (α := ENNReal)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ENNReal)
        (A ∩ ⋃ (w : { w : InfinitePlace K // w.IsReal }), {x : mixedSpace K | x.1 w = 0}) :
      ENNReal)
    (0 : ENNReal)

Tactic:
measure_mono_null Set.inter_subset_right
    (measure_iUnion_null_iff.mpr fun _ ↦ volume_eq_zero _)

Premises used: Iff.mpr, MeasureTheory.measure_iUnion_null_iff, MeasureTheory.measure_mono_null, NumberField.mixedEmbedding.volume_eq_zero, Set.inter_subset_right
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
inst_1 : NumberField K
⊢ Eq (α := ENNReal)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ENNReal)
        (A ∩ ⋃ (w : { w : InfinitePlace K // w.IsReal }), {x : mixedSpace K | x.1 w = 0}) :
      ENNReal)
    (0 : ENNReal)

Tactic:
exact measure_mono_null Set.inter_subset_right
    (measure_iUnion_null_iff.mpr fun _ ↦ volume_eq_zero _)

Premises used: Iff.mpr, MeasureTheory.measure_iUnion_null_iff, MeasureTheory.measure_mono_null, NumberField.mixedEmbedding.volume_eq_zero, Set.inter_subset_right
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hm : MeasurableSet A
h : plusPart A = A ∩ ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : mixedSpace K | 0 < x.1 w}
convert_to : MeasurableSet (A ∩ ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : mixedSpace K | 0 < x.1 w})
⊢ MeasurableSet (plusPart A)

Tactic:
convert_to MeasurableSet (A ∩ (⋂ w, {x | 0 < x.1 w}))

Premises used: MeasurableSet, Set.iInter, setOf, Prod.fst, Inter.inter, LT.lt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hm : MeasurableSet A
h :
  ∀ (x : mixedSpace K),
    x ∈ plusPart A ↔ x ∈ A ∩ ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : mixedSpace K | 0 < x.1 w}
⊢ plusPart A = A ∩ ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : mixedSpace K | 0 < x.1 w}

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hm : MeasurableSet A
x : mixedSpace K
⊢ x ∈ plusPart A ↔ x ∈ A ∩ ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : mixedSpace K | 0 < x.1 w}

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hm : MeasurableSet A
⊢ MeasurableSet (A ∩ ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : mixedSpace K | 0 < x.1 w})

Tactic:
hm.inter (MeasurableSet.iInter fun _ ↦ ?_)

Premises used: MeasurableSet.iInter, MeasurableSet.inter
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hm : MeasurableSet A
refine :
  ∀ (x : { w : InfinitePlace K // w.IsReal }),
    MeasurableSet.{u_1} (α := mixedSpace K) {x_1 : mixedSpace K | 0 < x_1.1 x}
⊢ MeasurableSet (A ∩ ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : mixedSpace K | 0 < x.1 w})

Tactic:
refine hm.inter (MeasurableSet.iInter fun _ ↦ ?_)

Premises used: MeasurableSet.iInter, MeasurableSet.inter
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hm : MeasurableSet A
x : { w : InfinitePlace K // w.IsReal }
⊢ Measurable (β := ℝ) fun (x_1 : mixedSpace K) ↦ x_1.1 x

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hm : MeasurableSet A
x : { w : InfinitePlace K // w.IsReal }
⊢ MeasurableSet.{u_1} (α := mixedSpace K) {x_1 : mixedSpace K | 0 < x_1.1 x}

Tactic:
exact measurableSet_lt measurable_const (by fun_prop)

Premises used: measurableSet_lt, measurable_const
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
A : Set (mixedSpace K)
inst_1 : NumberField K
hm : MeasurableSet A
⊢ MeasurableSet (α := mixedSpace K) ((⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' plusPart A)

Tactic:
negAt_preimage s _ ▸ (measurableSet_plusPart hm).preimage (negAt s).continuous.measurable

Premises used: MeasurableSet.preimage, NumberField.mixedEmbedding.measurableSet_plusPart, NumberField.mixedEmbedding.negAt, NumberField.mixedEmbedding.negAt_preimage, Eq.rec, ContinuousLinearEquiv.continuous, Continuous.measurable
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
s : Set { w : InfinitePlace K // w.IsReal }
A : Set (mixedSpace K)
inst_1 : NumberField K
hm : MeasurableSet A
rw :
  Eq (α := ENNReal)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ENNReal)
        ((⇑(negAt s).symm : (a : mixedSpace K) → mixedSpace K) '' plusPart A) :
      ENNReal)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ENNReal) (plusPart A) : ENNReal)
rw₁ :
  Eq (α := ENNReal)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ENNReal)
        ((⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) ⁻¹' plusPart A) :
      ENNReal)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ENNReal) (plusPart A) : ENNReal)
rw₂ rw₃ :
  Eq (α := ENNReal) (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ENNReal) (plusPart A) : ENNReal)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ENNReal) (plusPart A) : ENNReal)
⊢ Eq (α := ENNReal)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ENNReal)
        ((⇑(negAt s) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) :
      ENNReal)
    (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ENNReal) (plusPart A) : ENNReal)

Tactic:
rw [← negAt_symm, ContinuousLinearEquiv.image_symm_eq_preimage,
    volume_preserving_negAt.measure_preimage (measurableSet_plusPart hm).nullMeasurableSet]

Premises used: NumberField.mixedEmbedding.measurableSet_plusPart, MeasurableSet.nullMeasurableSet, NumberField.mixedEmbedding.volume_preserving_negAt, NumberField.mixedEmbedding.negAt_symm, ContinuousLinearEquiv.image_symm_eq_preimage, MeasureTheory.MeasurePreserving.measure_preimage
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
inst_1 : NumberField K
hm : MeasurableSet A
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ENNReal) A =
    HMul.hMul (β := ENNReal) (HPow.hPow (α := ENNReal) 2 (nrRealPlaces K))
      (((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ENNReal) (plusPart A) : ENNReal)

Tactic:
simp only [← measure_congr (iUnion_negAt_plusPart_ae A hA),
    measure_iUnion (disjoint_negAt_plusPart A) (fun _ ↦ measurableSet_negAt_plusPart _ A hm),
    volume_negAt_plusPart hm, tsum_fintype, sum_const, card_univ, Fintype.card_set, nsmul_eq_mul,
    Nat.cast_pow, Nat.cast_ofNat, nrRealPlaces]

Premises used: Finset.card_univ, Nat.cast_ofNat, MeasureTheory.measure_congr, NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae, Fintype.card_set, NumberField.InfinitePlace.nrRealPlaces, MeasureTheory.measure_iUnion, NumberField.mixedEmbedding.volume_negAt_plusPart, tsum_fintype, nsmul_eq_mul, Nat.cast_pow, NumberField.mixedEmbedding.measurableSet_negAt_plusPart, NumberField.mixedEmbedding.disjoint_negAt_plusPart, Finset.sum_const
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
⊢ ∀ {a b : InfinitePlace K → ℝ},
    Membership.mem (γ := Set (InfinitePlace K → ℝ)) {x : InfinitePlace K → ℝ | x w = 0} a →
      Membership.mem (γ := Set (InfinitePlace K → ℝ)) {x : InfinitePlace K → ℝ | x w = 0} b →
        Membership.mem (γ := Set (InfinitePlace K → ℝ)) {x : InfinitePlace K → ℝ | x 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 : InfinitePlace K
⊢ ∀ (c : ℝ) {x : InfinitePlace K → ℝ},
    Membership.mem (γ := Set (InfinitePlace K → ℝ))
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup
            { carrier := {x : InfinitePlace K → ℝ | x w = 0}, add_mem' := ⋯, zero_mem' := ⋯ }))
        x →
      Membership.mem (γ := Set (InfinitePlace K → ℝ))
        (AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup
            { carrier := {x : InfinitePlace K → ℝ | x 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 : InfinitePlace K
A : AffineSubspace ℝ (realSpace K) :=
  Submodule.toAffineSubspace
    { carrier := {x : InfinitePlace K → ℝ | x w = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ Eq (α := ENNReal)
    (((volume : Measure (InfinitePlace K → ℝ)) : (a : Set (InfinitePlace K → ℝ)) → ENNReal)
        (↑A : Set (InfinitePlace K → ℝ)) :
      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 : InfinitePlace K
A : AffineSubspace ℝ (realSpace K) :=
  Submodule.toAffineSubspace
    { carrier := {x : InfinitePlace K → ℝ | x w = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
convert! : ∀ (h : A = ⊤), False
⊢ Eq (α := ENNReal)
    (((volume : Measure (realSpace K)) : (a : Set (realSpace K)) → ENNReal) {x : realSpace K | x 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 : InfinitePlace K
A : AffineSubspace ℝ (realSpace K) :=
  Submodule.toAffineSubspace
    { carrier := {x : InfinitePlace K → ℝ | x 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
x : realSpace K
⊢ Eq (α := mixedSpace K) ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K)
    ((fun (w : { w : InfinitePlace K // w.IsReal }) ↦ x (↑w : InfinitePlace K),
        fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑(x (↑w : InfinitePlace K)) : ℂ)) :
      ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ))

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := realSpace K) (β := mixedSpace K)
    (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)

Tactic:
(injective_iff_map_eq_zero mixedSpaceOfRealSpace).mpr fun _ h ↦ ?_

Premises used: Iff.mpr, NumberField.mixedEmbedding.mixedSpaceOfRealSpace, injective_iff_map_eq_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
refine :
  ∀ (x : realSpace K)
    (h :
      Eq (α := mixedSpace K) ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K)
        (0 : mixedSpace K)),
    x = 0
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := realSpace K) (β := mixedSpace K)
    (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)

Tactic:
refine (injective_iff_map_eq_zero mixedSpaceOfRealSpace).mpr fun _ h ↦ ?_

Premises used: Iff.mpr, NumberField.mixedEmbedding.mixedSpaceOfRealSpace, injective_iff_map_eq_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : realSpace K
h :
  Eq (α := mixedSpace K) ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K)
    (0 : mixedSpace K)
⊢ (∀ (x_1 : { w : InfinitePlace K // w.IsReal }), x (↑x_1 : InfinitePlace K) = 0 x_1) ∧
    ∀ (x_1 : { w : InfinitePlace K // w.IsComplex }), (↑(x (↑x_1 : InfinitePlace K)) : ℂ) = 0 x_1

Tactic:
rw [mixedSpaceOfRealSpace_apply, Prod.mk_eq_zero, funext_iff, funext_iff] at h

Premises used: funext_iff, Prod.mk_eq_zero, NumberField.mixedEmbedding.mixedSpaceOfRealSpace_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : realSpace K
h :
  (∀ (x_1 : { w : InfinitePlace K // w.IsReal }), x (↑x_1 : InfinitePlace K) = 0 x_1) ∧
    ∀ (x_1 : { w : InfinitePlace K // w.IsComplex }), (↑(x (↑x_1 : InfinitePlace K)) : ℂ) = 0 x_1
h₁ : ∀ (w : InfinitePlace K), x w = 0 w
⊢ x = 0

Tactic:
ext w
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : realSpace K
h :
  (∀ (x_1 : { w : InfinitePlace K // w.IsReal }), x (↑x_1 : InfinitePlace K) = 0 x_1) ∧
    ∀ (x_1 : { w : InfinitePlace K // w.IsComplex }), (↑(x (↑x_1 : InfinitePlace K)) : ℂ) = 0 x_1
w : InfinitePlace K
h₁ : ∀ (hw : w.IsReal), x w = 0 w
h₂ : ∀ (hw : w.IsComplex), x w = 0 w
⊢ x w = 0 w

Tactic:
obtain hw | hw := isReal_or_isComplex w

Premises used: NumberField.InfinitePlace.isReal_or_isComplex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : realSpace K
h :
  (∀ (x_1 : { w : InfinitePlace K // w.IsReal }), x (↑x_1 : InfinitePlace K) = 0 x_1) ∧
    ∀ (x_1 : { w : InfinitePlace K // w.IsComplex }), (↑(x (↑x_1 : InfinitePlace K)) : ℂ) = 0 x_1
w : InfinitePlace K
hw : w.IsReal
⊢ x w = 0 w

Tactic:
h.1 ⟨w, hw⟩

Premises used: Subtype.mk, And.left
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : realSpace K
h :
  (∀ (x_1 : { w : InfinitePlace K // w.IsReal }), x (↑x_1 : InfinitePlace K) = 0 x_1) ∧
    ∀ (x_1 : { w : InfinitePlace K // w.IsComplex }), (↑(x (↑x_1 : InfinitePlace K)) : ℂ) = 0 x_1
w : InfinitePlace K
hw : w.IsReal
⊢ x w = 0 w

Tactic:
exact h.1 ⟨w, hw⟩

Premises used: Subtype.mk, And.left
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : realSpace K
h :
  (∀ (x_1 : { w : InfinitePlace K // w.IsReal }), x (↑x_1 : InfinitePlace K) = 0 x_1) ∧
    ∀ (x_1 : { w : InfinitePlace K // w.IsComplex }), (↑(x (↑x_1 : InfinitePlace K)) : ℂ) = 0 x_1
w : InfinitePlace K
hw : w.IsComplex
⊢ x w = 0 w

Tactic:
Complex.ofReal_inj.mp <| h.2 ⟨w, hw⟩

Premises used: Subtype.mk, And.right, Iff.mp, Complex.ofReal_inj
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : realSpace K
h :
  (∀ (x_1 : { w : InfinitePlace K // w.IsReal }), x (↑x_1 : InfinitePlace K) = 0 x_1) ∧
    ∀ (x_1 : { w : InfinitePlace K // w.IsComplex }), (↑(x (↑x_1 : InfinitePlace K)) : ℂ) = 0 x_1
w : InfinitePlace K
hw : w.IsComplex
⊢ x w = 0 w

Tactic:
exact Complex.ofReal_inj.mp <| h.2 ⟨w, hw⟩

Premises used: Subtype.mk, And.right, Iff.mp, Complex.ofReal_inj
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : realSpace K
w : InfinitePlace K
hx : 0 ≤ x w
simp :
  (normAtPlace w : (a : mixedSpace K) → ℝ)
      (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ x (↑w : InfinitePlace K),
        fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑(x (↑w : InfinitePlace K)) : ℂ)) =
    x w
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ)
      ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K) =
    x w

Tactic:
simp only [mixedSpaceOfRealSpace_apply]

Premises used: NumberField.mixedEmbedding.mixedSpaceOfRealSpace_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : realSpace K
w : InfinitePlace K
hx : 0 ≤ x w
inl :
  ∀ (hw : w.IsReal),
    (normAtPlace w : (a : mixedSpace K) → ℝ)
        (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ x (↑w : InfinitePlace K),
          fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑(x (↑w : InfinitePlace K)) : ℂ)) =
      x w
inr :
  ∀ (hw : w.IsComplex),
    (normAtPlace w : (a : mixedSpace K) → ℝ)
        (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ x (↑w : InfinitePlace K),
          fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑(x (↑w : InfinitePlace K)) : ℂ)) =
      x w
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ)
      (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ x (↑w : InfinitePlace K),
        fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑(x (↑w : InfinitePlace K)) : ℂ)) =
    x w

Tactic:
obtain hw | hw := isReal_or_isComplex w

Premises used: NumberField.InfinitePlace.isReal_or_isComplex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : realSpace K
w : InfinitePlace K
hx : 0 ≤ x w
hw : w.IsReal
inl :
  norm (E := ℝ)
      ((fun (w : { w : InfinitePlace K // w.IsReal }) ↦ x (↑w : InfinitePlace K),
            fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑(x (↑w : InfinitePlace K)) : ℂ)).1
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)) =
    x w
inl₁ inl₂ : x w = x w
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ)
      (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ x (↑w : InfinitePlace K),
        fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑(x (↑w : InfinitePlace K)) : ℂ)) =
    x w

Tactic:
rw [normAtPlace_apply_of_isReal hw, Real.norm_of_nonneg hx]

Premises used: NumberField.mixedEmbedding.normAtPlace_apply_of_isReal, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : realSpace K
w : InfinitePlace K
hx : 0 ≤ x w
hw : w.IsComplex
inr :
  norm (E := ℂ)
      ((fun (w : { w : InfinitePlace K // w.IsReal }) ↦ x (↑w : InfinitePlace K),
            fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑(x (↑w : InfinitePlace K)) : ℂ)).2
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)) =
    x w
inr₁ inr₂ : x w = x w
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ)
      (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ x (↑w : InfinitePlace K),
        fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑(x (↑w : InfinitePlace K)) : ℂ)) =
    x w

Tactic:
rw [normAtPlace_apply_of_isComplex hw, Complex.norm_of_nonneg hx]

Premises used: Complex.norm_of_nonneg, NumberField.mixedEmbedding.normAtPlace_apply_of_isComplex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
w : { w : InfinitePlace K // w.IsReal }
rw :
  (if hw : (↑w : InfinitePlace K).IsReal then
      x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (↑w : InfinitePlace K) hw)
    else (normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) =
    x.1 w
rw₁ : x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (↑w : InfinitePlace K) ⋯) = x.1 w
hc : (↑w : InfinitePlace K).IsReal
rw₂ : x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (↑w : InfinitePlace K) ⋯) = x.1 w
hc₁ : (↑w : InfinitePlace K).IsReal
⊢ normAtComplexPlaces x (↑w : InfinitePlace K) = x.1 w

Tactic:
rw [normAtComplexPlaces, dif_pos]

Premises used: dif_pos, NumberField.mixedEmbedding.normAtComplexPlaces