-- 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 : ℝ)
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 : ℝ)
⊢ 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 := ℝ)
        ((Pi.ringHom (f := fun (a : { w : InfinitePlace K // w.IsReal }) ↦ ℝ)
              fun (w : { w : InfinitePlace K // w.IsReal }) ↦ embedding_of_isReal sorry :
            (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 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]