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
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)‖
⊢ (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 } :
      (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]
-- 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
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)‖
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ) x = ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
have 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 sorry)‖) =
  ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
Tactic: rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, dif_pos]
-- 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
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)‖
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ) x = ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
have 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)‖
Tactic: rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, dif_pos]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
hw : w.IsComplex
x : mixedSpace K
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ) x = ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) 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.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)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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)‖
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ) x = ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) 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 } :
      (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)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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)‖
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ) x = ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)‖
have 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 sorry)‖) =
  ‖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)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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)‖
⊢ (normAtPlace w : (a : mixedSpace K) → ℝ) x = ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)‖
have rw₃ : ‖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 hw)‖
Tactic: rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk,
    dif_neg (not_isReal_iff_isComplex.mpr hw)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : K
⊢ Eq (α := ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) : ℝ)
    ((w : (a : K) → ℝ) x : ℝ)
have simp_rw : Eq (α := ℝ)
  (({
          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) → ℝ)
      ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) :
    ℝ)
  ((w : (a : K) → ℝ) x : ℝ)
Tactic: simp_rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, mixedEmbedding,
    RingHom.prod_apply, Pi.ringHom_apply, norm_embedding_of_isReal, norm_embedding_eq, dite_eq_ite,
    ite_id]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : K
simp_rw :
  Eq (α := ℝ)
    (({
            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) → ℝ)
        ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) :
      ℝ)
    ((w : (a : K) → ℝ) x : ℝ)
⊢ Eq (α := ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) : ℝ)
    ((w : (a : K) → ℝ) x : ℝ)
have simp_rw₁ : Eq (α := ℝ)
  (({
          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 } :
        (a : mixedSpace K) → ℝ)
      ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) :
    ℝ)
  ((w : (a : K) → ℝ) x : ℝ)
Tactic: simp_rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, mixedEmbedding,
    RingHom.prod_apply, Pi.ringHom_apply, norm_embedding_of_isReal, norm_embedding_eq, dite_eq_ite,
    ite_id]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : K
simp_rw :
  Eq (α := ℝ)
    (({
            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) → ℝ)
        ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) :
      ℝ)
    ((w : (a : K) → ℝ) x : ℝ)
simp_rw₁ :
  Eq (α := ℝ)
    (({
            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) → ℝ)
        ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) :
      ℝ)
    ((w : (a : K) → ℝ) x : ℝ)
⊢ Eq (α := ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) : ℝ)
    ((w : (a : K) → ℝ) x : ℝ)
have simp_rw₂ : Eq (α := ℝ)
  (if hw : w.IsReal then
      norm (E := ℝ)
        (((mixedEmbedding K : (a : K) → mixedSpace K) x).1
          (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw))
    else
      norm (E := ℂ)
        (((mixedEmbedding K : (a : K) → mixedSpace K) x).2
          (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w sorry)) :
    ℝ)
  ((w : (a : K) → ℝ) x : ℝ)
Tactic: simp_rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, mixedEmbedding,
    RingHom.prod_apply, Pi.ringHom_apply, norm_embedding_of_isReal, norm_embedding_eq, dite_eq_ite,
    ite_id]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : K
simp_rw :
  Eq (α := ℝ)
    (({
            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) → ℝ)
        ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) :
      ℝ)
    ((w : (a : K) → ℝ) x : ℝ)
simp_rw₁ :
  Eq (α := ℝ)
    (({
            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) → ℝ)
        ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) :
      ℝ)
    ((w : (a : K) → ℝ) x : ℝ)
simp_rw₂ :
  Eq (α := ℝ)
    (if hw : w.IsReal then
        norm (E := ℝ)
          (((mixedEmbedding K : (a : K) → mixedSpace K) x).1
            (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw))
      else
        norm (E := ℂ)
          (((mixedEmbedding K : (a : K) → mixedSpace K) x).2
            (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)) :
      ℝ)
    ((w : (a : K) → ℝ) x : ℝ)
⊢ Eq (α := ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) : ℝ)
    ((w : (a : K) → ℝ) x : ℝ)
have simp_rw₃ : Eq (α := ℝ)
  (if hw : w.IsReal then
      norm (E := ℝ)
        (((RingHom.prod
                  (Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsReal }) ↦ ℝ)
                    fun (w : { w : InfinitePlace K // w.IsReal }) ↦ embedding_of_isReal sorry)
                  (Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ)
                    fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K).embedding) :
                (a : K) → mixedSpace K)
              x).1
          (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw))
    else
      norm (E := ℂ)
        (((RingHom.prod
                  (Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsReal }) ↦ ℝ)
                    fun (w : { w : InfinitePlace K // w.IsReal }) ↦ embedding_of_isReal sorry)
                  (Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ)
                    fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K).embedding) :
                (a : K) → mixedSpace K)
              x).2
          (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w sorry)) :
    ℝ)
  ((w : (a : K) → ℝ) x : ℝ)
Tactic: simp_rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, mixedEmbedding,
    RingHom.prod_apply, Pi.ringHom_apply, norm_embedding_of_isReal, norm_embedding_eq, dite_eq_ite,
    ite_id]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
⊢ (∀ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)) ↔ x = 0
have refine_1 : ∀ (h : ∀ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)), x = 0
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
⊢ (∀ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)) ↔ x = 0
have refine_2 : ∀ (h : x = 0) (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
h : ∀ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
⊢ x = 0
have refine_1 : ∀ (w : { w : InfinitePlace K // w.IsReal }), x.1 w = 0.1 w
Tactic: ext w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
⊢ x = 0
have refine_1₁ : ∀ (w : { w : InfinitePlace K // w.IsComplex }), x.2 w = 0.2 w
Tactic: ext w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
h : x = 0
⊢ ∀ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
have refine_2 : ∀ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) 0 : ℝ) (0 : ℝ)
Tactic: simp_rw [h, map_zero, implies_true]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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 : ℝ)
⊢ ∀ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
have refine_2₁ : ∀ (w : InfinitePlace K), True
Tactic: simp_rw [h, map_zero, implies_true]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
⊢ (∃ (w : InfinitePlace K), Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)) ↔ x ≠ 0
have rw : (∃ (w : InfinitePlace K), Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)) ↔ ¬x = 0
Tactic: rw [ne_eq, ← forall_normAtPlace_eq_zero_iff, not_forall]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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
⊢ (∃ (w : InfinitePlace K), Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)) ↔ x ≠ 0
have rw₁ : (∃ (w : InfinitePlace K), Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)) ↔
  ¬∀ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
Tactic: rw [ne_eq, ← forall_normAtPlace_eq_zero_iff, not_forall]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
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 : ℝ)
⊢ (∃ (w : InfinitePlace K), Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)) ↔ x ≠ 0
have 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 : ℝ)
Tactic: rw [ne_eq, ← forall_normAtPlace_eq_zero_iff, not_forall]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
⊢ 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 ⋯)‖
have pos : ∀ (h : w.IsReal),
  Continuous (Y := ℝ) fun (x : mixedSpace K) ↦ ‖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
pos :
  ∀ (h : w.IsReal),
    Continuous (Y := ℝ) fun (x : mixedSpace K) ↦ ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w h)‖
⊢ 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 ⋯)‖
have neg : ∀ (h : ¬w.IsReal),
  Continuous (Y := ℝ) fun (x : mixedSpace K) ↦ ‖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
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)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : mixedSpace K
⊢ ‖x‖₊ = sup univ fun (w : InfinitePlace K) ↦ NNReal.mk ((normAtPlace w : (a : mixedSpace K) → ℝ) x) ⋯
have 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)
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]