-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
η : Type u_7
inst : Fintype η
inst_1 : DecidableEq η
ι : η → Type u_8
inst_2 : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst_3 : RCLike 𝕜
E : η → Type u_10
inst_4 : (i : η) → NormedAddCommGroup (E i)
inst_5 : (i : η) → InnerProductSpace.{u_9, u_10} 𝕜 (E i)
B : (i : η) → OrthonormalBasis.{u_8, u_9, u_10} (ι i) 𝕜 (E i)
j : (i : η) × ι i
h :
  ∀ (k : η),
    Eq.{u_10 + 1} (α := E k)
      (ofLp (p := 2) ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E) j) k : E k)
      (ofLp (p := 2)
          (PiLp.single 2 (β := E) (j.fst (β := fun (i : η) ↦ ι i))
            ((B (j.fst (β := fun (i : η) ↦ ι i)) : (a : ι j.fst) → E j.fst) (j.snd (β := fun (i : η) ↦ ι i))))
          k :
        E k)
h₁ :
  ∀ (k i : η) (j : ι i),
    Eq.{u_10 + 1} (α := E k)
      (ofLp (p := 2)
          ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E)
            (Sigma.mk (β := fun (i : η) ↦ ι i) i j))
          k :
        E k)
      (ofLp (p := 2)
          (PiLp.single 2 (β := E) ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).fst (β := fun (i : η) ↦ ι i))
            ((B ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).fst (β := fun (i : η) ↦ ι i)) :
                (a : ι ⟨i, j⟩.fst) → E ⟨i, j⟩.fst)
              ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).snd (β := fun (i : η) ↦ ι i))))
          k :
        E k)
h₂ :
  ∀ (k i : η) (j : ι i),
    Eq.{u_10 + 1} (α := E k)
      (((B k).repr.symm : (a : EuclideanSpace 𝕜 (ι k)) → E k)
          (toLp 2 (Pi.single (M := fun (j : η) ↦ (y : ι j) → 𝕜) i (Pi.single (M := fun (x : ι i) ↦ 𝕜) j 1) k)) :
        E k)
      (Pi.single (M := E) i ((B i : (a : ι i) → E i) j) k : E k)
h₃ :
  ∀ (i : η) (j : ι i),
    Eq.{u_10 + 1} (α := E i)
      (((B i).repr.symm : (a : EuclideanSpace 𝕜 (ι i)) → E i)
          (toLp 2 (Pi.single (M := fun (j : η) ↦ (y : ι j) → 𝕜) i (Pi.single (M := fun (x : ι i) ↦ 𝕜) j 1) i)) :
        E i)
      (Pi.single (M := E) i ((B i : (a : ι i) → E i) j) i : E i)
h₄ h₅ :
  ∀ (k i : η) (j : ι i) (hi : i ≠ k),
    Eq.{u_10 + 1} (α := E k)
      (((B k).repr.symm : (a : EuclideanSpace 𝕜 (ι k)) → E k)
          (toLp 2 (Pi.single (M := fun (j : η) ↦ (y : ι j) → 𝕜) i (Pi.single (M := fun (x : ι i) ↦ 𝕜) j 1) k)) :
        E k)
      (Pi.single (M := E) i ((B i : (a : ι i) → E i) j) k : E k)
⊢ Eq (α := PiLp 2 E) ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E) j : PiLp 2 E)
    (PiLp.single 2 (β := E) (j.fst (β := fun (i : η) ↦ ι i))
        ((B (j.fst (β := fun (i : η) ↦ ι i)) : (a : ι j.fst) → E j.fst) (j.snd (β := fun (i : η) ↦ ι i))) :
      PiLp 2 E)

Tactic:
classical
  ext k
  obtain ⟨i, j⟩ := j
  simp only [Pi.orthonormalBasis, coe_ofRepr, LinearIsometryEquiv.symm_trans,
    LinearIsometryEquiv.symm_symm, LinearIsometryEquiv.piLpCongrRight_symm,
    LinearIsometryEquiv.trans_apply, LinearIsometryEquiv.piLpCongrRight_apply,
    LinearIsometryEquiv.piLpCurry_apply, PiLp.ofLp_single, PiLp.toLp_apply,
    Sigma.curry_single (γ := fun _ _ => 𝕜)]
  obtain rfl | hi := Decidable.eq_or_ne i k
  · simp
  · simp [hi]

Premises used: LinearIsometryEquiv.piLpCongrRight_symm, PiLp.ofLp_single, LinearIsometryEquiv.piLpCongrRight_apply, OrthonormalBasis.coe_ofRepr, Pi.orthonormalBasis, LinearIsometryEquiv.piLpCurry_apply, Sigma.curry_single, LinearIsometryEquiv.trans_apply, LinearIsometryEquiv.symm_trans, PiLp.toLp_apply, LinearIsometryEquiv.symm_symm, rfl