-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι_1 : Type u_2
α_1 : ι_1 → Type u_3
β : ι_1 → Type u_4
hp : Fact (1 ≤ p)
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
inst_6 : Fintype ι
inst_7 : (i : ι) → Fintype (κ i)
α : (i : ι) → κ i → Type u_7
inst_8 : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)
inst_9 : (i : ι) → (k : κ i) → Module.{u_1, u_7} 𝕜 (α i k)
x : (i : Sigma κ) → (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) i
inst_10 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
__LinearEquiv : (PiLp ∞ fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) ≃ₗ[𝕜]
  PiLp ∞ fun (i : ι) ↦ PiLp ∞ (α i) :=
  (WithLp.linearEquiv ∞ 𝕜 ((i : Sigma κ) → (fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ))) i) ≪≫ₗ
        LinearEquiv.piCurry 𝕜 (κ := κ) α ≪≫ₗ
      LinearEquiv.piCongrRight (φ := fun (i : ι) ↦ (j : κ i) → α i j) (ψ := fun (x : ι) ↦ WithLp ∞ ((j : κ x) → α x j))
        fun (x : ι) ↦ LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 ((j : κ x) → α x j))) ≪≫ₗ
    LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 ((i : ι) → WithLp ∞ ((j : κ i) → α i j)))
inl :
  Eq (α := ℝ≥0)
    (Finset.sup Finset.univ fun (b : ι) ↦
      Finset.sup Finset.univ fun (b_1 : κ b) ↦
        nnnorm.{u_7} (E := α b b_1)
          (ofLp (p := ∞)
            (ofLp (p := ∞)
              (((WithLp.linearEquiv ∞ 𝕜 ((i : Sigma κ) → α (i.fst (β := κ)) (i.snd (β := κ))) ≪≫ₗ
                        LinearEquiv.piCurry 𝕜 (κ := κ) α ≪≫ₗ
                      LinearEquiv.piCongrRight (φ := fun (i : ι) ↦ (j : κ i) → α i j) (ψ := fun (x : ι) ↦
                        WithLp ∞ ((j : κ x) → α x j)) fun (x : ι) ↦
                        LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 ((j : κ x) → α x j))) ≪≫ₗ
                    LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 ((i : ι) → WithLp ∞ ((j : κ i) → α i j))) :
                  (a : PiLp ∞ fun (i : Sigma κ) ↦ α i.fst i.snd) → PiLp ∞ fun (i : ι) ↦ PiLp ∞ (α i))
                (Equiv.invFun
                  (AddEquiv.toEquiv (WithLp.addEquiv ∞ ((i : Sigma κ) → α (i.fst (β := κ)) (i.snd (β := κ))))) x))
              b)
            b_1))
    (Finset.sup Finset.univ fun (b : Sigma κ) ↦
      ‖ofLp (p := ∞)
          (Equiv.invFun (AddEquiv.toEquiv (WithLp.addEquiv ∞ ((i : Sigma κ) → α (i.fst (β := κ)) (i.snd (β := κ))))) x)
          b‖₊)
⊢ nnnorm (E := PiLp ∞ fun (i : ι) ↦ PiLp ∞ (α i))
      (((WithLp.linearEquiv ∞ 𝕜 ((i : Sigma κ) → α (i.fst (β := κ)) (i.snd (β := κ))) ≪≫ₗ
                  LinearEquiv.piCurry 𝕜 (κ := κ) α ≪≫ₗ
                LinearEquiv.piCongrRight (φ := fun (i : ι) ↦ (j : κ i) → α i j) (ψ := fun (x : ι) ↦
                  WithLp ∞ ((j : κ x) → α x j)) fun (x : ι) ↦
                  LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 ((j : κ x) → α x j))) ≪≫ₗ
              LinearEquiv.symm (WithLp.linearEquiv ∞ 𝕜 ((i : ι) → WithLp ∞ ((j : κ i) → α i j))) :
            (a : PiLp ∞ fun (i : Sigma κ) ↦ α i.fst i.snd) → PiLp ∞ fun (i : ι) ↦ PiLp ∞ (α i))
          (Equiv.invFun (AddEquiv.toEquiv (WithLp.addEquiv ∞ ((i : Sigma κ) → α (i.fst (β := κ)) (i.snd (β := κ)))))
            x) :
        PiLp ∞ fun (i : ι) ↦ PiLp ∞ (α i)) =
    nnnorm (E := PiLp ∞ fun (i : Sigma κ) ↦ α (i.fst (β := κ)) (i.snd (β := κ)))
      (Equiv.invFun (AddEquiv.toEquiv (WithLp.addEquiv ∞ ((i : Sigma κ) → α (i.fst (β := κ)) (i.snd (β := κ))))) x)

Tactic:
simp_rw [← PiLp.nnnorm_ofLp, Pi.nnnorm_def, ← PiLp.nnnorm_ofLp, Pi.nnnorm_def]

Premises used: Pi.nnnorm_def, PiLp.nnnorm_ofLp