awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
hw : w.IsReal
x : mixedSpace K
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 ⋯)‖,
          map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ } :
        (a : mixedSpace K) → ℝ)
      x =
    ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
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 ⋯)‖,
          map_zero' := ⋯ } :
        (a : mixedSpace K) → ℝ)
      x =
    ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
rw₂ :
  (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 ⋯)‖) =
    ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
rw₃ :
  ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖ =
    ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
hc : w.IsReal
rw₄ :
  ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖ =
    ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
hc₁ : w.IsReal
⊢ (normAtPlace w : (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]

Premises used: MonoidWithZeroHom.coe_mk, dif_pos, ZeroHom.coe_mk, NumberField.mixedEmbedding.normAtPlace
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
hw : w.IsComplex
x : mixedSpace K
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 ⋯)‖,
          map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ } :
        (a : mixedSpace K) → ℝ)
      x =
    ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)‖
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 ⋯)‖,
          map_zero' := ⋯ } :
        (a : mixedSpace K) → ℝ)
      x =
    ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)‖
rw₂ :
  (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 ⋯)‖) =
    ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)‖
rw₃ rw₄ :
  ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖ =
    ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)‖
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ) x = ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)‖

Tactic:
rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk,
    dif_neg (not_isReal_iff_isComplex.mpr hw)]

Premises used: Iff.mpr, MonoidWithZeroHom.coe_mk, dif_neg, ZeroHom.coe_mk, NumberField.mixedEmbedding.normAtPlace, NumberField.InfinitePlace.not_isReal_iff_isComplex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
⊢ (∀ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)) ↔ x = 0

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
refine_1 : ∀ (h : ∀ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)), x = 0
refine_2 : ∀ (h : x = 0) (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
⊢ (∀ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)) ↔ x = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
h : ∀ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
refine_1 : ∀ (w : { w : InfinitePlace K // w.IsReal }), x.1 w = 0.1 w
refine_1₁ : ∀ (w : { w : InfinitePlace K // w.IsComplex }), x.2 w = 0.2 w
⊢ x = 0

Tactic:
ext w
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
h : ∀ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
w : { w : InfinitePlace K // w.IsReal }
⊢ x.1 w = 0.1 w

Tactic:
norm_eq_zero.mp (normAtPlace_apply_of_isReal w.prop _ ▸ h w.1)

Premises used: norm_eq_zero, NumberField.mixedEmbedding.normAtPlace_apply_of_isReal, Eq.rec, Subtype.prop, Iff.mp, Subtype.val
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
h : ∀ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
w : { w : InfinitePlace K // w.IsReal }
⊢ x.1 w = 0.1 w

Tactic:
exact norm_eq_zero.mp (normAtPlace_apply_of_isReal w.prop _ ▸ h w.1)

Premises used: norm_eq_zero, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
h : ∀ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
w : { w : InfinitePlace K // w.IsComplex }
⊢ x.2 w = 0.2 w

Tactic:
norm_eq_zero.mp (normAtPlace_apply_of_isComplex w.prop _ ▸ h w.1)

Premises used: norm_eq_zero, Eq.rec, NumberField.mixedEmbedding.normAtPlace_apply_of_isComplex, Subtype.prop, Iff.mp, Subtype.val
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
h : ∀ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
w : { w : InfinitePlace K // w.IsComplex }
⊢ x.2 w = 0.2 w

Tactic:
exact norm_eq_zero.mp (normAtPlace_apply_of_isComplex w.prop _ ▸ h w.1)

Premises used: norm_eq_zero, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
h : x = 0
refine_2 : ∀ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) 0 : ℝ) (0 : ℝ)
refine_2₁ : ∀ (w : InfinitePlace K), True
⊢ ∀ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
simp_rw [h, map_zero, implies_true]

Premises used: map_zero, implies_true
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
rw : (∃ (w : InfinitePlace K), Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)) ↔ ¬x = 0
rw₁ :
  (∃ (w : InfinitePlace K), Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)) ↔
    ¬∀ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
rw₂ rw₃ :
  (∃ (w : InfinitePlace K), Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)) ↔
    ∃ (x_1 : InfinitePlace K), ¬Eq (α := ℝ) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
⊢ (∃ (w : InfinitePlace K), Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)) ↔ x ≠ 0

Tactic:
rw [ne_eq, ← forall_normAtPlace_eq_zero_iff, not_forall]

Premises used: ne_eq, NumberField.mixedEmbedding.forall_normAtPlace_eq_zero_iff, Classical.not_forall
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
pos :
  ∀ (h : w.IsReal),
    Continuous (Y := ℝ) fun (x : mixedSpace K) ↦ ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖
neg :
  ∀ (h : ¬w.IsReal),
    Continuous (Y := ℝ) fun (x : mixedSpace K) ↦ ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖
⊢ Continuous (Y := ℝ) 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 ⋯)‖

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

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
h : ¬w.IsReal
⊢ Continuous (Y := ℝ) fun (x : mixedSpace K) ↦ ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)‖

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
h :
  ∀ (a : InfinitePlace K),
    Membership.mem (γ := Finset (InfinitePlace K)) univ a ↔
      Membership.mem (γ := Finset (InfinitePlace K))
        (image (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (↑w : InfinitePlace K)) univ ∪
          image (fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K)) univ)
        a
⊢ Eq.{u_1 + 1} (α := Finset (InfinitePlace K)) univ
    (image (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (↑w : InfinitePlace K)) univ ∪
      image (fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K)) univ)

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
a : InfinitePlace K
⊢ Membership.mem (γ := Finset (InfinitePlace K)) univ a ↔
    Membership.mem (γ := Finset (InfinitePlace K))
      (image (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (↑w : InfinitePlace K)) univ ∪
        image (fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K)) univ)
      a

Tactic:
simp [isReal_or_isComplex]

Premises used: NumberField.InfinitePlace.isReal_or_isComplex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
⊢ Eq.{u_1 + 1} (α := Finset (InfinitePlace K)) univ
    (image (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (↑w : InfinitePlace K)) univ ∪
      image (fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K)) univ)

Tactic:
have :
      (univ : Finset (InfinitePlace K)) =
      (univ.image (fun w : {w : InfinitePlace K // IsReal w} ↦ w.1)) ∪
      (univ.image (fun w : {w : InfinitePlace K // IsComplex w} ↦ w.1)) := by
    ext; simp [isReal_or_isComplex]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
this :
  Eq.{u_1 + 1} (α := Finset (InfinitePlace K)) univ
    (image (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (↑w : InfinitePlace K)) univ ∪
      image (fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K)) univ)
rw :
  Eq (α := NNReal)
    (max (sup univ fun (b : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 b‖₊)
      (sup univ fun (b : { w : InfinitePlace K // w.IsComplex }) ↦ ‖x.2 b‖₊))
    (max
      (sup.{0, u_1} (β := { w : InfinitePlace K // w.IsReal }) univ
        ((fun (w : InfinitePlace K) ↦ NNReal.mk ((normAtPlace w : (a : mixedSpace K) → ℝ) x) ⋯) ∘
          fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (↑w : InfinitePlace K)))
      (sup.{0, u_1} (β := { w : InfinitePlace K // w.IsComplex }) univ
        ((fun (w : InfinitePlace K) ↦ NNReal.mk ((normAtPlace w : (a : mixedSpace K) → ℝ) x) ⋯) ∘
          fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K))))
⊢ ‖x‖₊ = sup univ fun (w : InfinitePlace K) ↦ NNReal.mk ((normAtPlace w : (a : mixedSpace K) → ℝ) x) ⋯

Tactic:
rw [this, sup_union, univ.sup_image, univ.sup_image,
    Prod.nnnorm_def, Pi.nnnorm_def, Pi.nnnorm_def]

Premises used: Finset.univ, Prod.nnnorm_def, Finset.sup_union, Finset.sup_image, Pi.nnnorm_def
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
this :
  Eq.{u_1 + 1} (α := Finset (InfinitePlace K)) univ
    (image (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (↑w : InfinitePlace K)) univ ∪
      image (fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K)) univ)
e_a :
  Eq.{u_1 + 1} (α := { w : InfinitePlace K // w.IsReal } → NNReal)
    (fun (b : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 b‖₊)
    ((fun (w : InfinitePlace K) ↦ NNReal.mk ((normAtPlace w : (a : mixedSpace K) → ℝ) x) ⋯) ∘
      fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (↑w : InfinitePlace K))
e_a₁ :
  Eq.{u_1 + 1} (α := { w : InfinitePlace K // w.IsComplex } → NNReal)
    (fun (b : { w : InfinitePlace K // w.IsComplex }) ↦ ‖x.2 b‖₊)
    ((fun (w : InfinitePlace K) ↦ NNReal.mk ((normAtPlace w : (a : mixedSpace K) → ℝ) x) ⋯) ∘
      fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K))
⊢ Eq (α := NNReal)
    (max (sup univ fun (b : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 b‖₊)
      (sup univ fun (b : { w : InfinitePlace K // w.IsComplex }) ↦ ‖x.2 b‖₊))
    (max
      (sup.{0, u_1} (β := { w : InfinitePlace K // w.IsReal }) univ
        ((fun (w : InfinitePlace K) ↦ NNReal.mk ((normAtPlace w : (a : mixedSpace K) → ℝ) x) ⋯) ∘
          fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (↑w : InfinitePlace K)))
      (sup.{0, u_1} (β := { w : InfinitePlace K // w.IsComplex }) univ
        ((fun (w : InfinitePlace K) ↦ NNReal.mk ((normAtPlace w : (a : mixedSpace K) → ℝ) x) ⋯) ∘
          fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K))))

Tactic:
congr
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
this :
  Eq.{u_1 + 1} (α := Finset (InfinitePlace K)) univ
    (image (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (↑w : InfinitePlace K)) univ ∪
      image (fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K)) univ)
e_a :
  ∀ (w : { w : InfinitePlace K // w.IsReal }),
    (↑‖x.1 w‖₊ : ℝ) =
      (↑(((fun (w : InfinitePlace K) ↦ NNReal.mk ((normAtPlace w : (a : mixedSpace K) → ℝ) x) ⋯) ∘
              fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (↑w : InfinitePlace K))
            w) :
        ℝ)
⊢ Eq.{u_1 + 1} (α := { w : InfinitePlace K // w.IsReal } → NNReal)
    (fun (b : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 b‖₊)
    ((fun (w : InfinitePlace K) ↦ NNReal.mk ((normAtPlace w : (a : mixedSpace K) → ℝ) x) ⋯) ∘
      fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (↑w : InfinitePlace K))

Tactic:
ext w
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
this :
  Eq.{u_1 + 1} (α := Finset (InfinitePlace K)) univ
    (image (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (↑w : InfinitePlace K)) univ ∪
      image (fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K)) univ)
w : { w : InfinitePlace K // w.IsReal }
⊢ (↑‖x.1 w‖₊ : ℝ) =
    (↑(((fun (w : InfinitePlace K) ↦ NNReal.mk ((normAtPlace w : (a : mixedSpace K) → ℝ) x) ⋯) ∘
            fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (↑w : InfinitePlace K))
          w) :
      ℝ)

Tactic:
simp [normAtPlace_apply_of_isReal w.prop]

Premises used: NumberField.mixedEmbedding.normAtPlace_apply_of_isReal, Subtype.prop
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
this :
  Eq.{u_1 + 1} (α := Finset (InfinitePlace K)) univ
    (image (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (↑w : InfinitePlace K)) univ ∪
      image (fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K)) univ)
e_a :
  ∀ (w : { w : InfinitePlace K // w.IsComplex }),
    (↑‖x.2 w‖₊ : ℝ) =
      (↑(((fun (w : InfinitePlace K) ↦ NNReal.mk ((normAtPlace w : (a : mixedSpace K) → ℝ) x) ⋯) ∘
              fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K))
            w) :
        ℝ)
⊢ Eq.{u_1 + 1} (α := { w : InfinitePlace K // w.IsComplex } → NNReal)
    (fun (b : { w : InfinitePlace K // w.IsComplex }) ↦ ‖x.2 b‖₊)
    ((fun (w : InfinitePlace K) ↦ NNReal.mk ((normAtPlace w : (a : mixedSpace K) → ℝ) x) ⋯) ∘
      fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K))

Tactic:
ext w
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
this :
  Eq.{u_1 + 1} (α := Finset (InfinitePlace K)) univ
    (image (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (↑w : InfinitePlace K)) univ ∪
      image (fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K)) univ)
w : { w : InfinitePlace K // w.IsComplex }
⊢ (↑‖x.2 w‖₊ : ℝ) =
    (↑(((fun (w : InfinitePlace K) ↦ NNReal.mk ((normAtPlace w : (a : mixedSpace K) → ℝ) x) ⋯) ∘
            fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K))
          w) :
      ℝ)

Tactic:
simp [normAtPlace_apply_of_isComplex w.prop]

Premises used: NumberField.mixedEmbedding.normAtPlace_apply_of_isComplex, Subtype.prop
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
rw :
  Eq (α := ℝ)
    (sup'.{0, u_1} (β := InfinitePlace K) univ ⋯
      (Function.comp (β := { r : ℝ // 0 ≤ r }) (Subtype.val (p := fun (r : ℝ) ↦ 0 ≤ r)) fun (w : InfinitePlace K) ↦
        NNReal.mk ((normAtPlace w : (a : mixedSpace K) → ℝ) x) ⋯))
    (sup' univ ⋯ fun (w : InfinitePlace K) ↦ (normAtPlace w : (a : mixedSpace K) → ℝ) x)
⊢ ‖x‖ = sup' univ ⋯ fun (w : InfinitePlace K) ↦ (normAtPlace w : (a : mixedSpace K) → ℝ) x

Tactic:
rw [← coe_nnnorm, nnnorm_eq_sup_normAtPlace, ← sup'_eq_sup univ_nonempty, ← NNReal.val_eq_coe,
    ← OrderHom.Subtype.val_coe, map_finset_sup', OrderHom.Subtype.val_coe]

Premises used: OrderHom.Subtype.val_coe, map_finset_sup', Finset.univ_nonempty, NNReal.val_eq_coe, coe_nnnorm, Finset.sup'_eq_sup, NumberField.mixedEmbedding.nnnorm_eq_sup_normAtPlace
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
⊢ Eq (α := ℝ)
    (sup'.{0, u_1} (β := InfinitePlace K) univ ⋯
      (Function.comp (β := { r : ℝ // 0 ≤ r }) (Subtype.val (p := fun (r : ℝ) ↦ 0 ≤ r)) fun (w : InfinitePlace K) ↦
        NNReal.mk ((normAtPlace w : (a : mixedSpace K) → ℝ) x) ⋯))
    (sup' univ ⋯ fun (w : InfinitePlace K) ↦ (normAtPlace w : (a : mixedSpace K) → ℝ) x)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) 0 : ℝ) w.mult) 0

Tactic:
simp [mult]

Premises used: NumberField.InfinitePlace.mult
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) 1 : ℝ) w.mult) 1

Tactic:
simp only [map_one, one_pow, prod_const_one]

Premises used: one_pow, Finset.prod_const_one, map_one
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x x_1 : mixedSpace K
⊢ ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (x * x_1) : ℝ) w.mult =
    HMul.hMul (α := ℝ)
      (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) w.mult)
      (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x_1 : ℝ) w.mult)

Tactic:
simp only [map_mul, mul_pow, prod_mul_distrib]

Premises used: Finset.prod_mul_distrib, map_mul, mul_pow
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
⊢ Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)
    (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) w.mult : ℝ)

Tactic:
rfl

Premises used: Multiset.foldr, Multiset.prod, Multiset.dedup, Finset.prod, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
⊢ LE.le (α := ℝ) (0 : ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)

Tactic:
univ.prod_nonneg fun _ _ ↦ pow_nonneg (normAtPlace_nonneg _ _) _

Premises used: Multiset.foldr, pow_nonneg, Multiset.prod, NumberField.InfinitePlace.mult, Multiset.dedup, Finset.prod, NumberField.mixedEmbedding.normAtPlace_nonneg, Finset.prod_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
simp_rw :
  Eq (α := ℝ)
      (({
              toFun := fun (x : mixedSpace K) ↦
                ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) w.mult,
              map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ } :
            (a : mixedSpace K) → ℝ)
          x :
        ℝ)
      (0 : ℝ) ↔
    ∃ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
simp_rw₁ :
  Eq (α := ℝ)
      (({
              toFun := fun (x : mixedSpace K) ↦
                ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) w.mult,
              map_zero' := ⋯ } :
            (a : mixedSpace K) → ℝ)
          x :
        ℝ)
      (0 : ℝ) ↔
    ∃ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
simp_rw₂ :
  Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) w.mult) 0 ↔
    ∃ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
simp_rw₃ :
  (∃ (a : InfinitePlace K),
      Membership.mem (γ := Finset (InfinitePlace K)) univ a ∧
        HPow.hPow (α := ℝ) ((normAtPlace a : (a : mixedSpace K) → ℝ) x : ℝ) a.mult = 0) ↔
    ∃ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
simp_rw₄ :
  (∃ (a : InfinitePlace K), True ∧ HPow.hPow (α := ℝ) ((normAtPlace a : (a : mixedSpace K) → ℝ) x : ℝ) a.mult = 0) ↔
    ∃ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
simp_rw₅ :
  (∃ (a : InfinitePlace K), HPow.hPow (α := ℝ) ((normAtPlace a : (a : mixedSpace K) → ℝ) x : ℝ) a.mult = 0) ↔
    ∃ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ) ↔
    ∃ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
simp_rw [mixedEmbedding.norm, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, prod_eq_zero_iff,
    mem_univ, true_and, pow_eq_zero_iff mult_ne_zero]

Premises used: Finset.mem_univ, pow_eq_zero_iff, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, NumberField.InfinitePlace.mult_ne_zero, Finset.prod_eq_zero_iff, NumberField.mixedEmbedding.norm, true_and
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
rw :
  ¬Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ) ↔
    ¬∀ (w : InfinitePlace K), Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
⊢ Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ) ↔
    ∀ (w : InfinitePlace K), Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
rw [← not_iff_not]

Premises used: not_iff_not