-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p_1 : ℝ≥0∞
𝕜 : Type u_1
ι_1 : Type u_2
α_1 : ι_1 → Type u_3
β : ι_1 → Type u_4
hp : Fact (1 ≤ p_1)
inst : Fintype ι_1
inst_1 : Semiring 𝕜
inst_2 : (i : ι_1) → SeminormedAddCommGroup (α_1 i)
inst_3 : (i : ι_1) → SeminormedAddCommGroup (β i)
inst_4 : (i : ι_1) → Module.{u_1, u_3} 𝕜 (α_1 i)
inst_5 : (i : ι_1) → Module.{u_1, u_4} 𝕜 (β i)
c : 𝕜
ι : Type u_5
κ : ι → Type u_6
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
inst_7 : Fintype ι
inst_8 : (i : ι) → Fintype (κ i)
α : (i : ι) → κ i → Type u_7
inst_9 : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)
inst_10 : (i : ι) → (k : κ i) → Module.{u_1, u_7} 𝕜 (α i k)
x : (i : Sigma κ) → (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) i
⊢ Norm.norm (E := PiLp p fun (i : ι) ↦ PiLp p (α i))
      (((WithLp.linearEquiv p 𝕜 ((i : Sigma κ) → (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) i) ≪≫ₗ
                  LinearEquiv.piCurry 𝕜 (κ := κ) α ≪≫ₗ
                LinearEquiv.piCongrRight (φ := fun (i : ι) ↦ (j : κ i) → α i j) (ψ := fun (x : ι) ↦
                  WithLp p ((j : κ x) → α x j)) fun (x : ι) ↦
                  LinearEquiv.symm (WithLp.linearEquiv p 𝕜 ((j : κ x) → α x j))) ≪≫ₗ
              LinearEquiv.symm (WithLp.linearEquiv p 𝕜 ((i : ι) → WithLp p ((j : κ i) → α i j))) :
            (a : PiLp p fun (i : Sigma κ) ↦ α i.fst i.snd) → PiLp p fun (i : ι) ↦ PiLp p (α i))
          (((LinearEquiv.symm
                  (WithLp.linearEquiv p 𝕜
                    ((i : Sigma κ) → (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) i)) :
                ((i : Sigma κ) → (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) i) ≃ₗ[𝕜]
                  WithLp p ((i : Sigma κ) → (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) i)) :
              (a : (i : Sigma κ) → (fun (i : Sigma κ) ↦ α i.fst i.snd) i) →
                WithLp p ((i : Sigma κ) → (fun (i : Sigma κ) ↦ α i.fst i.snd) i))
            x) :
        PiLp p fun (i : ι) ↦ PiLp p (α i)) =
    Norm.norm (E := PiLp p fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ)))
      (((LinearEquiv.symm
                (WithLp.linearEquiv p 𝕜 ((i : Sigma κ) → (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) i)) :
              ((i : Sigma κ) → (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) i) ≃ₗ[𝕜]
                WithLp p ((i : Sigma κ) → (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) i)) :
            (a : (i : Sigma κ) → (fun (i : Sigma κ) ↦ α i.fst i.snd) i) →
              WithLp p ((i : Sigma κ) → (fun (i : Sigma κ) ↦ α i.fst i.snd) i))
          x :
        WithLp p ((i : Sigma κ) → (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) i))
have simp_rw : nnnorm (E := PiLp p fun (i : ι) ↦ PiLp p (α i))
    (((WithLp.linearEquiv p 𝕜 ((i : Sigma κ) → α (i.fst (β := κ)) (i.snd (β := κ))) ≪≫ₗ
                LinearEquiv.piCurry 𝕜 (κ := κ) α ≪≫ₗ
              LinearEquiv.piCongrRight (φ := fun (i : ι) ↦ (j : κ i) → α i j) (ψ := fun (x : ι) ↦
                WithLp p ((j : κ x) → α x j)) fun (x : ι) ↦
                LinearEquiv.symm (WithLp.linearEquiv p 𝕜 ((j : κ x) → α x j))) ≪≫ₗ
            LinearEquiv.symm (WithLp.linearEquiv p 𝕜 ((i : ι) → WithLp p ((j : κ i) → α i j))) :
          (a : PiLp p fun (i : Sigma κ) ↦ α i.fst i.snd) → PiLp p fun (i : ι) ↦ PiLp p (α i))
        (((LinearEquiv.symm (WithLp.linearEquiv p 𝕜 ((i : Sigma κ) → α (i.fst (β := κ)) (i.snd (β := κ)))) :
              ((i : Sigma κ) → α (i.fst (β := κ)) (i.snd (β := κ))) ≃ₗ[𝕜]
                WithLp p ((i : Sigma κ) → α (i.fst (β := κ)) (i.snd (β := κ)))) :
            (a : (i : Sigma κ) → α i.fst i.snd) → WithLp p ((i : Sigma κ) → α i.fst i.snd))
          x) :
      PiLp p fun (i : ι) ↦ PiLp p (α i)) =
  nnnorm (E := PiLp p fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ)))
    (((LinearEquiv.symm (WithLp.linearEquiv p 𝕜 ((i : Sigma κ) → α (i.fst (β := κ)) (i.snd (β := κ)))) :
            ((i : Sigma κ) → α (i.fst (β := κ)) (i.snd (β := κ))) ≃ₗ[𝕜]
              WithLp p ((i : Sigma κ) → α (i.fst (β := κ)) (i.snd (β := κ)))) :
          (a : (i : Sigma κ) → α i.fst i.snd) → WithLp p ((i : Sigma κ) → α i.fst i.snd))
        x :
      WithLp p ((i : Sigma κ) → α (i.fst (β := κ)) (i.snd (β := κ))))
Tactic: simp_rw [← coe_nnnorm, NNReal.coe_inj]