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 : 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)
⊢ ‖x‖₊ = sup univ fun (w : InfinitePlace K) ↦ NNReal.mk ((normAtPlace w : (a : mixedSpace K) → ℝ) x) ⋯
have 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) sorry) ∘
        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) sorry) ∘
        fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K))))
Tactic: rw [this, sup_union, univ.sup_image, univ.sup_image,
    Prod.nnnorm_def, Pi.nnnorm_def, Pi.nnnorm_def]
-- 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
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)
⊢ 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))))
have 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) sorry) ∘
    fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (↑w : InfinitePlace K))
Tactic: congr
-- 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
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))
⊢ 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))))
have 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) sorry) ∘
    fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K))
Tactic: congr
-- 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
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)
⊢ 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))
have e_a : ∀ (w : { w : InfinitePlace K // w.IsReal }),
  (↑‖x.1 w‖₊ : ℝ) =
    (↑(((fun (w : InfinitePlace K) ↦ NNReal.mk ((normAtPlace w : (a : mixedSpace K) → ℝ) x) sorry) ∘
            fun (w : { w : InfinitePlace K // w.IsReal }) ↦ (↑w : InfinitePlace K))
          w) :
      ℝ)
Tactic: ext w
-- 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
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)
⊢ 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))
have e_a : ∀ (w : { w : InfinitePlace K // w.IsComplex }),
  (↑‖x.2 w‖₊ : ℝ) =
    (↑(((fun (w : InfinitePlace K) ↦ NNReal.mk ((normAtPlace w : (a : mixedSpace K) → ℝ) x) sorry) ∘
            fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K))
          w) :
      ℝ)
Tactic: ext w
-- 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
⊢ ‖x‖ = sup' univ ⋯ fun (w : InfinitePlace K) ↦ (normAtPlace w : (a : mixedSpace K) → ℝ) x
have rw : Eq (α := ℝ)
  (sup'.{0, u_1} (β := InfinitePlace K) univ sorry
    (Function.comp (β := { r : ℝ // 0 ≤ r }) (Subtype.val (p := fun (r : ℝ) ↦ 0 ≤ r)) fun (w : InfinitePlace K) ↦
      NNReal.mk ((normAtPlace w : (a : mixedSpace K) → ℝ) x) sorry))
  (sup' univ sorry 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]
-- 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 (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ) ↔
    ∃ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
have simp_rw : Eq (α := ℝ)
    (({
            toFun := fun (x : mixedSpace K) ↦
              ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) w.mult,
            map_zero' := sorry, map_one' := sorry, map_mul' := sorry } :
          (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]
-- 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
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 : ℝ)
⊢ Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ) ↔
    ∃ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
have simp_rw₁ : Eq (α := ℝ)
    (({
            toFun := fun (x : mixedSpace K) ↦
              ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) w.mult,
            map_zero' := sorry } :
          (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]
-- 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
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 : ℝ)
⊢ Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ) ↔
    ∃ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
have 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 : ℝ)
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]
-- 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
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 : ℝ)
⊢ Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ) ↔
    ∃ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
have 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 : ℝ)
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]
-- 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
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 : ℝ)
⊢ Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ) ↔
    ∃ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
have 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 : ℝ)
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]
-- 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
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 : ℝ)
⊢ Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ) ↔
    ∃ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
have 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 : ℝ)
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]
-- 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
⊢ Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ) ↔
    ∀ (w : InfinitePlace K), Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
have rw : ¬Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ) ↔
  ¬∀ (w : InfinitePlace K), Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
Tactic: rw [← not_iff_not]
-- 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
⊢ ¬Ne (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ) ↔
    ¬∀ (w : InfinitePlace K), Ne (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
have simp_rw : ¬¬Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ) ↔
  ¬∀ (w : InfinitePlace K), ¬Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
Tactic: simp_rw [ne_eq, mixedEmbedding.norm_eq_zero_iff, not_not, not_forall, not_not]
-- 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
simp_rw :
  ¬¬Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ) ↔
    ¬∀ (w : InfinitePlace K), ¬Eq (α := ℝ) ((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 : ℝ)
have simp_rw₁ : (¬¬∃ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)) ↔
  ¬∀ (w : InfinitePlace K), ¬Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
Tactic: simp_rw [ne_eq, mixedEmbedding.norm_eq_zero_iff, not_not, not_forall, not_not]
-- 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
simp_rw :
  ¬¬Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ) ↔
    ¬∀ (w : InfinitePlace K), ¬Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
simp_rw₁ :
  (¬¬∃ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)) ↔
    ¬∀ (w : InfinitePlace K), ¬Eq (α := ℝ) ((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 : ℝ)
have simp_rw₂ : (∃ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)) ↔
  ¬∀ (w : InfinitePlace K), ¬Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
Tactic: simp_rw [ne_eq, mixedEmbedding.norm_eq_zero_iff, not_not, not_forall, not_not]
-- 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
simp_rw :
  ¬¬Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ) ↔
    ¬∀ (w : InfinitePlace K), ¬Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
simp_rw₁ :
  (¬¬∃ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)) ↔
    ¬∀ (w : InfinitePlace K), ¬Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
simp_rw₂ :
  (∃ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)) ↔
    ¬∀ (w : InfinitePlace K), ¬Eq (α := ℝ) ((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 : ℝ)
have simp_rw₃ : (∃ (w : InfinitePlace K), Eq (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)) ↔
  ∃ (x_1 : InfinitePlace K), ¬¬Eq (α := ℝ) ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ) (0 : ℝ)
Tactic: simp_rw [ne_eq, mixedEmbedding.norm_eq_zero_iff, not_not, not_forall, not_not]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : mixedSpace K
⊢ (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (c • x) =
    HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)
have simp_rw : ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (c • x) : ℝ) w.mult =
  |c| ^ finrank ℚ K * ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) w.mult
Tactic: simp_rw [mixedEmbedding.norm_apply, normAtPlace_smul, mul_pow, prod_mul_distrib,
    prod_pow_eq_pow_sum, sum_mult_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ℝ
x : mixedSpace K
simp_rw :
  ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) (c • x) : ℝ) w.mult =
    |c| ^ finrank ℚ K *
      ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) w.mult
⊢ (mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (c • x) =
    HMul.hMul (β := ℝ) (|c| ^ finrank ℚ K) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) x : ℝ)
have simp_rw₁ : ∏ x_1 : InfinitePlace K, HMul.hMul (β := ℝ) |c| ((normAtPlace x_1 : (a : mixedSpace K) → ℝ) x : ℝ) ^ x_1.mult =
  |c| ^ finrank ℚ K * ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ) w.mult
Tactic: simp_rw [mixedEmbedding.norm_apply, normAtPlace_smul, mul_pow, prod_mul_distrib,
    prod_pow_eq_pow_sum, sum_mult_eq]