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
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 φ
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 φ) ⋯))
    ((fun (x : mixedSpace K) ↦ x.2) 0
      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) (InfinitePlace.mk φ) ⋯))
h : (InfinitePlace.mk φ).embedding = φ
⊢ x φ = 0
have neg : x (InfinitePlace.mk φ).embedding = 0
Tactic: rwa [← h, ← commMap_apply_of_isComplex 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 φ
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 φ) ⋯))
    ((fun (x : mixedSpace K) ↦ x.2) 0
      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) (InfinitePlace.mk φ) ⋯))
h : (InfinitePlace.mk φ).embedding = φ
neg : x (InfinitePlace.mk φ).embedding = 0
⊢ x φ = 0
have neg₁ : Eq (α := ℂ)
  (((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x).2
    (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) (InfinitePlace.mk φ) sorry))
  0
Tactic: rwa [← h, ← commMap_apply_of_isComplex 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 φ
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 φ) ⋯))
    ((fun (x : mixedSpace K) ↦ x.2) 0
      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) (InfinitePlace.mk φ) ⋯))
h : (InfinitePlace.mk φ).embedding = ComplexEmbedding.conjugate φ
⊢ x φ = 0
have neg : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 0 : ℂ)
Tactic: apply RingHom.injective (starRingEnd ℂ)
-- 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 φ
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 φ) ⋯))
    ((fun (x : mixedSpace K) ↦ x.2) 0
      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) (InfinitePlace.mk φ) ⋯))
h : (InfinitePlace.mk φ).embedding = ComplexEmbedding.conjugate φ
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 0 : ℂ)
have neg : x (ComplexEmbedding.conjugate φ) = (starRingEnd ℂ : (a : ℂ) → ℂ) 0
Tactic: rwa [canonicalEmbedding.conj_apply _ h_mem, ← h, map_zero,
          ← commMap_apply_of_isComplex 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 φ
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 φ) ⋯))
    ((fun (x : mixedSpace K) ↦ x.2) 0
      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) (InfinitePlace.mk φ) ⋯))
h : (InfinitePlace.mk φ).embedding = ComplexEmbedding.conjugate φ
neg : x (ComplexEmbedding.conjugate φ) = (starRingEnd ℂ : (a : ℂ) → ℂ) 0
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 0 : ℂ)
have neg₁ : x (InfinitePlace.mk φ).embedding = (starRingEnd ℂ : (a : ℂ) → ℂ) 0
Tactic: rwa [canonicalEmbedding.conj_apply _ h_mem, ← h, map_zero,
          ← commMap_apply_of_isComplex 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 φ
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 φ) ⋯))
    ((fun (x : mixedSpace K) ↦ x.2) 0
      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) (InfinitePlace.mk φ) ⋯))
h : (InfinitePlace.mk φ).embedding = ComplexEmbedding.conjugate φ
neg : x (ComplexEmbedding.conjugate φ) = (starRingEnd ℂ : (a : ℂ) → ℂ) 0
neg₁ : x (InfinitePlace.mk φ).embedding = (starRingEnd ℂ : (a : ℂ) → ℂ) 0
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 0 : ℂ)
have neg₂ : x (InfinitePlace.mk φ).embedding = 0
Tactic: rwa [canonicalEmbedding.conj_apply _ h_mem, ← h, map_zero,
          ← commMap_apply_of_isComplex 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 φ
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 φ) ⋯))
    ((fun (x : mixedSpace K) ↦ x.2) 0
      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) (InfinitePlace.mk φ) ⋯))
h : (InfinitePlace.mk φ).embedding = ComplexEmbedding.conjugate φ
neg : x (ComplexEmbedding.conjugate φ) = (starRingEnd ℂ : (a : ℂ) → ℂ) 0
neg₁ : x (InfinitePlace.mk φ).embedding = (starRingEnd ℂ : (a : ℂ) → ℂ) 0
neg₂ : x (InfinitePlace.mk φ).embedding = 0
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 0 : ℂ)
have neg₃ : Eq (α := ℂ)
  (((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x).2
    (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) (InfinitePlace.mk φ) sorry))
  0
Tactic: rwa [canonicalEmbedding.conj_apply _ h_mem, ← h, map_zero,
          ← commMap_apply_of_isComplex K x ⟨φ, hφ, rfl⟩]
-- 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 φ
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 φ) ⋯))
    ((fun (x : mixedSpace K) ↦ x.2) 0
      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) (InfinitePlace.mk φ) ⋯))
⊢ x φ = 0
have x₁ : (InfinitePlace.mk φ).embedding = φ ∨ (InfinitePlace.mk φ).embedding = ComplexEmbedding.conjugate φ
Tactic: cases embedding_mk_eq φ with
    | inl h => rwa [← h, ← commMap_apply_of_isComplex K x ⟨φ, hφ, rfl⟩]
    | inr h =>
        apply RingHom.injective (starRingEnd ℂ)
        rwa [canonicalEmbedding.conj_apply _ h_mem, ← h, map_zero,
          ← commMap_apply_of_isComplex K x ⟨φ, hφ, rfl⟩]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x y : mixedSpace K
⊢ (if hw : w.IsReal then ‖(x * y).1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
    else ‖(x * y).2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖) =
    HMul.hMul (α := ℝ)
      (if hw : w.IsReal then ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
      else ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖)
      (if hw : w.IsReal then ‖y.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
      else ‖y.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖)
have pos : ∀ (h : w.IsReal),
  ‖(x * y).1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖ =
    ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖ *
      ‖y.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x y : mixedSpace K
pos :
  ∀ (h : w.IsReal),
    ‖(x * y).1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖ =
      ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖ *
        ‖y.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖
⊢ (if hw : w.IsReal then ‖(x * y).1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
    else ‖(x * y).2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖) =
    HMul.hMul (α := ℝ)
      (if hw : w.IsReal then ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
      else ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖)
      (if hw : w.IsReal then ‖y.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
      else ‖y.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖)
have neg : ∀ (h : ¬w.IsReal),
  ‖(x * y).2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w sorry)‖ =
    ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w sorry)‖ *
      ‖y.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w sorry)‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : mixedSpace K
⊢ LE.le (α := ℝ) 0
    (if hw : w.IsReal then ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
    else ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖)
have pos : ∀ (h : w.IsReal), 0 ≤ ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : mixedSpace K
pos : ∀ (h : w.IsReal), 0 ≤ ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖
⊢ LE.le (α := ℝ) 0
    (if hw : w.IsReal then ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
    else ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖)
have neg : ∀ (h : ¬w.IsReal), 0 ≤ ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w sorry)‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : mixedSpace K
⊢ Eq (α := ℝ)
    (if hw : w.IsReal then ‖(-x).1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
    else ‖(-x).2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖)
    (if hw : w.IsReal then ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
    else ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖)
have pos : ∀ (h : w.IsReal),
  ‖(-x).1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖ =
    ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : mixedSpace K
pos :
  ∀ (h : w.IsReal),
    ‖(-x).1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖ =
      ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖
⊢ Eq (α := ℝ)
    (if hw : w.IsReal then ‖(-x).1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
    else ‖(-x).2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖)
    (if hw : w.IsReal then ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
    else ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖)
have neg : ∀ (h : ¬w.IsReal),
  ‖(-x).2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w sorry)‖ =
    ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w sorry)‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x y : mixedSpace K
⊢ (if hw : w.IsReal then ‖(x + y).1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
    else ‖(x + y).2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖) ≤
    HAdd.hAdd (α := ℝ)
      (if hw : w.IsReal then ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
      else ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖)
      (if hw : w.IsReal then ‖y.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
      else ‖y.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖)
have pos : ∀ (h : w.IsReal),
  ‖(x + y).1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖ ≤
    ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖ +
      ‖y.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x y : mixedSpace K
pos :
  ∀ (h : w.IsReal),
    ‖(x + y).1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖ ≤
      ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖ +
        ‖y.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖
⊢ (if hw : w.IsReal then ‖(x + y).1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
    else ‖(x + y).2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖) ≤
    HAdd.hAdd (α := ℝ)
      (if hw : w.IsReal then ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
      else ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖)
      (if hw : w.IsReal then ‖y.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
      else ‖y.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖)
have neg : ∀ (h : ¬w.IsReal),
  ‖(x + y).2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w sorry)‖ ≤
    ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w sorry)‖ +
      ‖y.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w sorry)‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : mixedSpace K
c : ℝ
⊢ (if hw : w.IsReal then ‖(c • x).1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
    else ‖(c • x).2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖) =
    |c| *
      if hw : w.IsReal then ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
      else ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖
have pos : ∀ (h : w.IsReal),
  ‖(c • x).1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖ =
    |c| * ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : mixedSpace K
c : ℝ
pos :
  ∀ (h : w.IsReal),
    ‖(c • x).1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖ =
      |c| * ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖
⊢ (if hw : w.IsReal then ‖(c • x).1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
    else ‖(c • x).2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖) =
    |c| *
      if hw : w.IsReal then ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
      else ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖
have neg : ∀ (h : ¬w.IsReal),
  ‖(c • x).2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w sorry)‖ =
    |c| * ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w sorry)‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
c : ℝ
⊢ (fun (x : { w : InfinitePlace K // w.IsReal }) ↦ c, fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ (↑c : ℂ)) =
    HSMul.hSMul (β := ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)) c 1
have fst : ∀ (x : { w : InfinitePlace K // w.IsReal }),
  (fun (x : { w : InfinitePlace K // w.IsReal }) ↦ c, fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ (↑c : ℂ)).1 x =
    (HSMul.hSMul (β := ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)) c 1).1
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
c : ℝ
fst :
  ∀ (x : { w : InfinitePlace K // w.IsReal }),
    (fun (x : { w : InfinitePlace K // w.IsReal }) ↦ c, fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ (↑c : ℂ)).1
        x =
      (HSMul.hSMul (β := ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)) c
            1).1
        x
⊢ (fun (x : { w : InfinitePlace K // w.IsReal }) ↦ c, fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ (↑c : ℂ)) =
    HSMul.hSMul (β := ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)) c 1
have snd : ∀ (x : { w : InfinitePlace K // w.IsComplex }),
  (fun (x : { w : InfinitePlace K // w.IsReal }) ↦ c, fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ (↑c : ℂ)).2 x =
    (HSMul.hSMul (β := ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)) c 1).2
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
c : ℝ
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ)
      (fun (x : { w : InfinitePlace K // w.IsReal }) ↦ c, fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ (↑c : ℂ)) =
    |c|
have rw : (normAtPlace w : (a : mixedSpace K) → ℝ)
    (HSMul.hSMul (β := ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)) c 1) =
  |c|
Tactic: rw [show ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = c • 1 by ext <;> simp, normAtPlace_smul,
    map_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
c : ℝ
rw :
  (normAtPlace w : (a : mixedSpace K) → ℝ)
      (HSMul.hSMul (β := ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)) c
        1) =
    |c|
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ)
      (fun (x : { w : InfinitePlace K // w.IsReal }) ↦ c, fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ (↑c : ℂ)) =
    |c|
have rw₁ : HMul.hMul (β := ℝ) |c| ((normAtPlace w : (a : mixedSpace K) → ℝ) 1 : ℝ) = |c|
Tactic: rw [show ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = c • 1 by ext <;> simp, normAtPlace_smul,
    map_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
c : ℝ
rw :
  (normAtPlace w : (a : mixedSpace K) → ℝ)
      (HSMul.hSMul (β := ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)) c
        1) =
    |c|
rw₁ : HMul.hMul (β := ℝ) |c| ((normAtPlace w : (a : mixedSpace K) → ℝ) 1 : ℝ) = |c|
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ)
      (fun (x : { w : InfinitePlace K // w.IsReal }) ↦ c, fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ (↑c : ℂ)) =
    |c|
have rw₂ : |c| * 1 = |c|
Tactic: rw [show ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = c • 1 by ext <;> simp, normAtPlace_smul,
    map_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
c : ℝ
rw :
  (normAtPlace w : (a : mixedSpace K) → ℝ)
      (HSMul.hSMul (β := ({ w : InfinitePlace K // w.IsReal } → ℝ) × ({ w : InfinitePlace K // w.IsComplex } → ℂ)) c
        1) =
    |c|
rw₁ : HMul.hMul (β := ℝ) |c| ((normAtPlace w : (a : mixedSpace K) → ℝ) 1 : ℝ) = |c|
rw₂ : |c| * 1 = |c|
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ)
      (fun (x : { w : InfinitePlace K // w.IsReal }) ↦ c, fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ (↑c : ℂ)) =
    |c|
have rw₃ : |c| = |c|
Tactic: rw [show ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = c • 1 by ext <;> simp, normAtPlace_smul,
    map_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
hw : w.IsReal
x : mixedSpace K
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ) x = ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
have rw : ({
        toFun := fun (x : mixedSpace K) ↦
          if hw : w.IsReal then ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
          else ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w sorry)‖,
        map_zero' := sorry, map_one' := sorry, map_mul' := sorry } :
      (a : mixedSpace K) → ℝ)
    x =
  ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
Tactic: rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, dif_pos]