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
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
h₁ :
  ∀ (hx : ∃ (a : { w : InfinitePlace K // w.IsReal }), x.1 a = 0),
    (∃ (i : Set { w : InfinitePlace K // w.IsReal }),
        Membership.mem (γ := Set (mixedSpace K)) ((⇑(negAt i) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) x) ∨
      x ∈ A ∧
        ∃ (i : { w : InfinitePlace K // w.IsReal }),
          Membership.mem (γ := Set (mixedSpace K)) {x : mixedSpace K | x.1 i = 0} x
⊢ (∃ (i : Set { w : InfinitePlace K // w.IsReal }),
      Membership.mem (γ := Set (mixedSpace K)) ((⇑(negAt i) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) x) ∨
    x ∈ A ∧
      ∃ (i : { w : InfinitePlace K // w.IsReal }),
        Membership.mem (γ := Set (mixedSpace K)) {x : mixedSpace K | x.1 i = 0} x
have h₂ : ∀ (hx : ∀ (a : { w : InfinitePlace K // w.IsReal }), ¬x.1 a = 0),
  (∃ (i : Set { w : InfinitePlace K // w.IsReal }),
      Membership.mem (γ := Set (mixedSpace K)) ((⇑(negAt i) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) x) ∨
    x ∈ A ∧
      ∃ (i : { w : InfinitePlace K // w.IsReal }),
        Membership.mem (γ := Set (mixedSpace K)) {x : mixedSpace K | x.1 i = 0} x
Tactic: obtain hx | hx := exists_or_forall_not (fun w ↦ x.1 w = 0)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
⊢ (∃ (i : Set { w : InfinitePlace K // w.IsReal }),
      Membership.mem (γ := Set (mixedSpace K)) ((⇑(negAt i) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) x) ∨
    x ∈ A ∧
      ∃ (i : { w : InfinitePlace K // w.IsReal }),
        Membership.mem (γ := Set (mixedSpace K)) {x : mixedSpace K | x.1 i = 0} x
have h₁ : ∀ (w : { w : InfinitePlace K // w.IsReal }) (hw : w ∈ signSet x), x.1 w < 0
Tactic: refine Or.inl ⟨signSet x,
        (mem_negAt_plusPart_of_mem A hA h hx).mpr ⟨fun w hw ↦ ?_, fun w hw ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
h₁ : ∀ (w : { w : InfinitePlace K // w.IsReal }) (hw : w ∈ signSet x), x.1 w < 0
⊢ (∃ (i : Set { w : InfinitePlace K // w.IsReal }),
      Membership.mem (γ := Set (mixedSpace K)) ((⇑(negAt i) : (a : mixedSpace K) → mixedSpace K) '' plusPart A) x) ∨
    x ∈ A ∧
      ∃ (i : { w : InfinitePlace K // w.IsReal }),
        Membership.mem (γ := Set (mixedSpace K)) {x : mixedSpace K | x.1 i = 0} x
have h₂ : ∀ (w : { w : InfinitePlace K // w.IsReal }) (hw : w ∉ signSet x), x.1 w > 0
Tactic: refine Or.inl ⟨signSet x,
        (mem_negAt_plusPart_of_mem A hA h hx).mpr ⟨fun w hw ↦ ?_, fun w hw ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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]
    A
have 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}
Tactic: nth_rewrite 2 [← iUnion_negAt_plusPart_union A hA]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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}
have 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)
Tactic: refine (MeasureTheory.union_ae_eq_left_of_ae_eq_empty (ae_eq_empty.mpr ?_)).symm
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hm : MeasurableSet A
⊢ MeasurableSet (plusPart A)
have h : plusPart A = A ∩ ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : mixedSpace K | 0 < x.1 w}
Tactic: convert_to MeasurableSet (A ∩ (⋂ w, {x | 0 < x.1 w}))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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}
⊢ MeasurableSet (plusPart A)
have convert_to : MeasurableSet (A ∩ ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : mixedSpace K | 0 < x.1 w})
Tactic: convert_to MeasurableSet (A ∩ (⋂ w, {x | 0 < x.1 w}))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hm : MeasurableSet A
⊢ plusPart A = A ∩ ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : mixedSpace K | 0 < x.1 w}
have h : ∀ (x : mixedSpace K),
  x ∈ plusPart A ↔ x ∈ A ∩ ⋂ (w : { w : InfinitePlace K // w.IsReal }), {x : mixedSpace K | 0 < x.1 w}
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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})
have refine : ∀ (x : { w : InfinitePlace K // w.IsReal }), MeasurableSet.{u_1} (α := mixedSpace K) {x_1 : mixedSpace K | 0 < x_1.1 x}
Tactic: refine hm.inter (MeasurableSet.iInter fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [← negAt_symm, ContinuousLinearEquiv.image_symm_eq_preimage,
    volume_preserving_negAt.measure_preimage (measurableSet_plusPart hm).nullMeasurableSet]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← negAt_symm, ContinuousLinearEquiv.image_symm_eq_preimage,
    volume_preserving_negAt.measure_preimage (measurableSet_plusPart hm).nullMeasurableSet]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← negAt_symm, ContinuousLinearEquiv.image_symm_eq_preimage,
    volume_preserving_negAt.measure_preimage (measurableSet_plusPart hm).nullMeasurableSet]
-- 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
A : AffineSubspace ℝ (realSpace K) :=
  Submodule.toAffineSubspace
    { carrier := {x : InfinitePlace K → ℝ | x w = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ Eq (α := ENNReal)
    (((volume : Measure (realSpace K)) : (a : Set (realSpace K)) → ENNReal) {x : realSpace K | x 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
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := realSpace K) (β := mixedSpace K)
    (⇑mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K)
have refine : ∀ (x : realSpace K)
  (h :
    Eq (α := mixedSpace K) ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K)
      (0 : mixedSpace K)),
  x = 0
Tactic: refine (injective_iff_map_eq_zero mixedSpaceOfRealSpace).mpr fun _ h ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (hypothesis)
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 = 0
have 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
Tactic: rw [mixedSpaceOfRealSpace_apply, Prod.mk_eq_zero, funext_iff, funext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
⊢ x = 0
have h₁ : ∀ (w : InfinitePlace K), x w = 0 w
Tactic: ext w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
⊢ x w = 0 w
have h₁ : ∀ (hw : w.IsReal), x w = 0 w
Tactic: obtain hw | hw := isReal_or_isComplex w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
⊢ x w = 0 w
have h₂ : ∀ (hw : w.IsComplex), x w = 0 w
Tactic: obtain hw | hw := isReal_or_isComplex w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : realSpace K
w : InfinitePlace K
hx : 0 ≤ x w
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ)
      ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K) =
    x w
have 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
Tactic: simp only [mixedSpaceOfRealSpace_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : realSpace K
w : InfinitePlace K
hx : 0 ≤ 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
have 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
Tactic: obtain hw | hw := isReal_or_isComplex w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
⊢ (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
have 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
Tactic: obtain hw | hw := isReal_or_isComplex w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : realSpace K
w : InfinitePlace K
hx : 0 ≤ x w
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
have 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
Tactic: rw [normAtPlace_apply_of_isReal hw, Real.norm_of_nonneg hx]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
⊢ (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
have inl₁ : x w = x w
Tactic: rw [normAtPlace_apply_of_isReal hw, Real.norm_of_nonneg hx]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : realSpace K
w : InfinitePlace K
hx : 0 ≤ x w
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
have 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
Tactic: rw [normAtPlace_apply_of_isComplex hw, Complex.norm_of_nonneg hx]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
⊢ (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
have inr₁ : x w = x w
Tactic: rw [normAtPlace_apply_of_isComplex hw, Complex.norm_of_nonneg hx]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
w : { w : InfinitePlace K // w.IsReal }
⊢ normAtComplexPlaces x (↑w : InfinitePlace K) = x.1 w
have 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
Tactic: rw [normAtComplexPlaces, dif_pos]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
⊢ normAtComplexPlaces x (↑w : InfinitePlace K) = x.1 w
have rw₁ : x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (↑w : InfinitePlace K) sorry) = x.1 w
Tactic: rw [normAtComplexPlaces, dif_pos]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
⊢ normAtComplexPlaces x (↑w : InfinitePlace K) = x.1 w
have hc : (↑w : InfinitePlace K).IsReal
Tactic: rw [normAtComplexPlaces, dif_pos]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
w : { w : InfinitePlace K // w.IsComplex }
⊢ normAtComplexPlaces x (↑w : InfinitePlace K) = ‖x.2 w‖
have 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.2 w‖
Tactic: rw [normAtComplexPlaces, dif_neg (not_isReal_iff_isComplex.mpr w.prop),
    normAtPlace_apply_of_isComplex]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
w : { w : InfinitePlace K // w.IsComplex }
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.2 w‖
⊢ normAtComplexPlaces x (↑w : InfinitePlace K) = ‖x.2 w‖
have rw₁ : (normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x = ‖x.2 w‖
Tactic: rw [normAtComplexPlaces, dif_neg (not_isReal_iff_isComplex.mpr w.prop),
    normAtPlace_apply_of_isComplex]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
w : { w : InfinitePlace K // w.IsComplex }
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.2 w‖
rw₁ : (normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x = ‖x.2 w‖
⊢ normAtComplexPlaces x (↑w : InfinitePlace K) = ‖x.2 w‖
have rw₂ : ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) (↑w : InfinitePlace K) sorry)‖ = ‖x.2 w‖
Tactic: rw [normAtComplexPlaces, dif_neg (not_isReal_iff_isComplex.mpr w.prop),
    normAtPlace_apply_of_isComplex]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
w : { w : InfinitePlace K // w.IsComplex }
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.2 w‖
rw₁ : (normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x = ‖x.2 w‖
rw₂ : ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) (↑w : InfinitePlace K) ⋯)‖ = ‖x.2 w‖
⊢ normAtComplexPlaces x (↑w : InfinitePlace K) = ‖x.2 w‖
have hw : (↑w : InfinitePlace K).IsComplex
Tactic: rw [normAtComplexPlaces, dif_neg (not_isReal_iff_isComplex.mpr w.prop),
    normAtPlace_apply_of_isComplex]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), w.IsComplex → 0 ≤ x w
⊢ normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) = x
have h : ∀ (w : InfinitePlace K), normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) w = x w
Tactic: ext w