-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
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 : ℝ)
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 ⋯)
                    (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 ⋯)
                    (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 ⋯)) :
      ℝ)
    ((w : (a : K) → ℝ) x : ℝ)
simp_rw₄ :
  Eq (α := ℝ)
    (if hw : w.IsReal then
        norm (E := ℝ)
          ((Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsReal }) ↦ ℝ)
                fun (w : { w : InfinitePlace K // w.IsReal }) ↦ embedding_of_isReal ⋯ :
              (a : K) → { w : InfinitePlace K // w.IsReal } → ℝ)
            x (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw))
      else
        norm (E := ℂ)
          ((Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsComplex }) ↦ ℂ)
                fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑w : InfinitePlace K).embedding :
              (a : K) → { w : InfinitePlace K // w.IsComplex } → ℂ)
            x (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w ⋯)) :
      ℝ)
    ((w : (a : K) → ℝ) x : ℝ)
simp_rw₅ :
  Eq (α := ℝ)
    (if hw : w.IsReal then norm (E := ℝ) ((embedding_of_isReal ⋯ : (a : K) → ℝ) x : ℝ)
      else norm (E := ℂ) ((w.embedding : (a : K) → ℂ) x : ℂ) :
      ℝ)
    ((w : (a : K) → ℝ) x : ℝ)
simp_rw₆ :
  Eq (α := ℝ) (if hw : w.IsReal then (w : (a : K) → ℝ) x else norm (E := ℂ) ((w.embedding : (a : K) → ℂ) x : ℂ) : ℝ)
    ((w : (a : K) → ℝ) x : ℝ)
simp_rw₇ :
  Eq (α := ℝ) (if hw : w.IsReal then (w : (a : K) → ℝ) x else (w : (a : K) → ℝ) x : ℝ) ((w : (a : K) → ℝ) x : ℝ)
simp_rw₈ : Eq (α := ℝ) (if w.IsReal then (w : (a : K) → ℝ) x else (w : (a : K) → ℝ) x : ℝ) ((w : (a : K) → ℝ) x : ℝ)
⊢ Eq (α := ℝ)
    ((normAtPlace w : (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]

Premises used: NumberField.InfinitePlace.norm_embedding_of_isReal, NumberField.mixedEmbedding, MonoidWithZeroHom.coe_mk, NumberField.InfinitePlace.norm_embedding_eq, ite_id, ZeroHom.coe_mk, NumberField.mixedEmbedding.normAtPlace, Pi.ringHom_apply, RingHom.prod_apply, dite_eq_ite