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
x : (K →+* ℂ) → ℂ
h_zero : Eq (α := mixedSpace K) ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x : mixedSpace K) (0 : mixedSpace K)
h_mem :
  Membership.mem (γ := Submodule ℝ ((K →+* ℂ) → ℂ))
    (Submodule.span ℝ (Set.range (ι := K) (⇑(canonicalEmbedding K) : (a : K) → (K →+* ℂ) → ℂ))) x
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
pos : (x φ).re = Complex.re 0
pos₁ : (x φ).im = Complex.im 0
⊢ x φ = 0

Tactic:
apply Complex.ext

Premises used: Complex.ext
-- 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 →+* ℂ
hφ : ComplexEmbedding.IsReal φ
pos :
  ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x).1
      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (InfinitePlace.mk φ) ⋯) =
    Complex.re 0
⊢ (x φ).re = Complex.re 0

Tactic:
rw [← embedding_mk_eq_of_isReal hφ, ← commMap_apply_of_isReal K x ⟨φ, hφ, rfl⟩]

Premises used: NumberField.InfinitePlace.embedding_mk_eq_of_isReal, And.intro, Exists.intro, NumberField.mixedEmbedding.commMap_apply_of_isReal, rfl
-- 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 →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x).1
      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (InfinitePlace.mk φ) ⋯) =
    Complex.re 0

Tactic:
congrFun (congrArg (fun x => x.1) h_zero) ⟨InfinitePlace.mk φ, _⟩

Premises used: congrFun
-- 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 →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ ((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x).1
      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (InfinitePlace.mk φ) ⋯) =
    Complex.re 0

Tactic:
exact congrFun (congrArg (fun x => x.1) h_zero) ⟨InfinitePlace.mk φ, _⟩

Premises used: congrFun
-- 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 →+* ℂ
hφ : ComplexEmbedding.IsReal φ
pos : (x φ).im = 0
pos₁ : (starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) = x φ
pos₂ : x (ComplexEmbedding.conjugate φ) = x φ
pos₃ pos₄ : x φ = x φ
⊢ (x φ).im = Complex.im 0

Tactic:
rw [Complex.zero_im, ← Complex.conj_eq_iff_im, canonicalEmbedding.conj_apply _ h_mem,
        ComplexEmbedding.isReal_iff.mp hφ]

Premises used: Complex.zero_im, Iff.mp, NumberField.ComplexEmbedding.isReal_iff, Complex.conj_eq_iff_im, NumberField.canonicalEmbedding.conj_apply
-- 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 →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
⊢ 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 φ) ⋯))

Tactic:
have := congrFun (congrArg (fun x => x.2) h_zero) ⟨InfinitePlace.mk φ, ⟨φ, hφ, rfl⟩⟩
-- 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 →+* ℂ
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
neg₁ neg₂ neg₃ neg₄ :
  Eq (α := ℂ)
    (((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x).2
      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) (InfinitePlace.mk φ) ⋯))
    0
⊢ x φ = 0

Tactic:
rwa [← h, ← commMap_apply_of_isComplex K x ⟨φ, hφ, rfl⟩]

Premises used: NumberField.mixedEmbedding.commMap_apply_of_isComplex, And.intro, Exists.intro, rfl
-- 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 →+* ℂ
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 : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 0 : ℂ)
⊢ x φ = 0

Tactic:
apply RingHom.injective (starRingEnd ℂ)

Premises used: RingHom.injective, Complex, starRingEnd
-- 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 →+* ℂ
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
neg₃ neg₄ neg₅ neg₆ :
  Eq (α := ℂ)
    (((commMap K : (a : (K →+* ℂ) → ℂ) → mixedSpace K) x).2
      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) (InfinitePlace.mk φ) ⋯))
    0
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (x φ) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 0 : ℂ)

Tactic:
rwa [canonicalEmbedding.conj_apply _ h_mem, ← h, map_zero,
          ← commMap_apply_of_isComplex K x ⟨φ, hφ, rfl⟩]

Premises used: NumberField.mixedEmbedding.commMap_apply_of_isComplex, map_zero, And.intro, Exists.intro, NumberField.canonicalEmbedding.conj_apply, rfl
-- 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 →+* ℂ
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 φ) ⋯))
⊢ (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⟩]

Premises used: NumberField.mixedEmbedding.commMap_apply_of_isComplex, map_zero, RingHom.injective, NumberField.InfinitePlace.embedding_mk_eq, And.intro, Exists.intro, NumberField.canonicalEmbedding.conj_apply, Complex, starRingEnd, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
⊢ Eq (α := ℝ)
    (if hw : w.IsReal then norm (E := ℝ) (0.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw))
    else norm (E := ℂ) (0.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)))
    0

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
⊢ Eq (α := ℝ)
    (if hw : w.IsReal then norm (E := ℝ) (1.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw))
    else norm (E := ℂ) (1.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)))
    1

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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)‖
neg :
  ∀ (h : ¬w.IsReal),
    ‖(x * y).2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖ =
      ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖ *
        ‖y.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖
⊢ (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 ⋯)‖)

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x y : mixedSpace K
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:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x y : mixedSpace K
h : ¬w.IsReal
⊢ ‖(x * y).2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖ =
    ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖ *
      ‖y.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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)‖
neg : ∀ (h : ¬w.IsReal), 0 ≤ ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖
⊢ 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 ⋯)‖)

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : mixedSpace K
h : w.IsReal
⊢ 0 ≤ ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖

Tactic:
norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : mixedSpace K
h : w.IsReal
⊢ 0 ≤ ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖

Tactic:
exact norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : mixedSpace K
h : ¬w.IsReal
⊢ 0 ≤ ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖

Tactic:
norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : mixedSpace K
h : ¬w.IsReal
⊢ 0 ≤ ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖

Tactic:
exact norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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)‖
neg :
  ∀ (h : ¬w.IsReal),
    ‖(-x).2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖ =
      ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖
⊢ 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 ⋯)‖)

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : mixedSpace K
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:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : mixedSpace K
h : ¬w.IsReal
⊢ ‖(-x).2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖ =
    ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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)‖
neg :
  ∀ (h : ¬w.IsReal),
    ‖(x + y).2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖ ≤
      ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖ +
        ‖y.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖
⊢ (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 ⋯)‖)

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x y : mixedSpace K
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:
norm_add_le _ _

Premises used: norm_add_le
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x y : mixedSpace K
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:
exact norm_add_le _ _

Premises used: norm_add_le
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x y : mixedSpace K
h : ¬w.IsReal
⊢ ‖(x + y).2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖ ≤
    ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖ +
      ‖y.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖

Tactic:
norm_add_le _ _

Premises used: norm_add_le
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x y : mixedSpace K
h : ¬w.IsReal
⊢ ‖(x + y).2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖ ≤
    ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖ +
      ‖y.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖

Tactic:
exact norm_add_le _ _

Premises used: norm_add_le
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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)‖
neg :
  ∀ (h : ¬w.IsReal),
    ‖(c • x).2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖ =
      |c| * ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖
⊢ (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 ⋯)‖

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : mixedSpace K
c : ℝ
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:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : mixedSpace K
c : ℝ
h : ¬w.IsReal
⊢ ‖(c • x).2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖ =
    |c| * ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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
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
⊢ (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

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
c : ℝ
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:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
c : ℝ
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:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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|
rw₃ rw₄ : |c| = |c|
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ)
      (fun (x : { w : InfinitePlace K // w.IsReal }) ↦ c, fun (x : { w : InfinitePlace K // w.IsComplex }) ↦ (↑c : ℂ)) =
    |c|

Tactic:
rw [show ((fun _ ↦ c, fun _ ↦ c) : (mixedSpace K)) = c • 1 by ext <;> simp, normAtPlace_smul,
    map_one, mul_one]

Premises used: map_one, NumberField.mixedEmbedding.normAtPlace_smul, mul_one