-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
b b' : OrthonormalBasis ι 𝕜 E
h :
  Eq (α := (a : ι) → E)
    ((fun (b : OrthonormalBasis ι 𝕜 E) (i : ι) ↦
        ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E) (EuclideanSpace.single i 1) : E))
      b)
    ((fun (b : OrthonormalBasis ι 𝕜 E) (i : ι) ↦
        ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E) (EuclideanSpace.single i 1) : E))
      b')
rw rw₁ rw₂ :
  (↑b.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
      (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜)) =
    (↑b'.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
      (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜))
rw₃ :
  (↑b.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
      (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜)) =
    (↑b'.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
      (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜))
rw₄ :
  ∀ (i : ι) (k : 𝕜),
    Eq.{u_4 + 1} (α := E)
      (((↑b.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
              (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜)) :
            (a : (i : ι) → 𝕜) → E)
          (Pi.single (M := fun (i : ι) ↦ 𝕜) i k) :
        E)
      (((↑b'.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
              (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜)) :
            (a : (i : ι) → 𝕜) → E)
          (Pi.single (M := fun (i : ι) ↦ 𝕜) i k) :
        E)
rw₅ :
  ∀ (i : ι) (k : 𝕜) (this : k = HSMul.hSMul (β := 𝕜) k 1),
    Eq.{u_4 + 1} (α := E)
      (((↑b.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
              (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜)) :
            (a : (i : ι) → 𝕜) → E)
          (Pi.single (M := fun (i : ι) ↦ 𝕜) i k) :
        E)
      (((↑b'.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
              (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜)) :
            (a : (i : ι) → 𝕜) → E)
          (Pi.single (M := fun (i : ι) ↦ 𝕜) i k) :
        E)
rw₆ :
  ∀ (i : ι) (k : 𝕜) (this : k = HSMul.hSMul (β := 𝕜) k 1),
    Eq.{u_4 + 1} (α := E)
      (((↑b.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
              (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜)) :
            (a : (i : ι) → 𝕜) → E)
          (HSMul.hSMul (β := (j : ι) → 𝕜) k (Pi.single (M := fun (i : ι) ↦ 𝕜) i 1)) :
        E)
      (((↑b'.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
              (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜)) :
            (a : (i : ι) → 𝕜) → E)
          (HSMul.hSMul (β := (j : ι) → 𝕜) k (Pi.single (M := fun (i : ι) ↦ 𝕜) i 1)) :
        E)
rw₇ :
  ∀ (i : ι) (k : 𝕜) (this : k = HSMul.hSMul (β := 𝕜) k 1)
    (h :
      Eq.{u_4 + 1} (α := E)
        ((fun (b : OrthonormalBasis ι 𝕜 E) (i : ι) ↦
            ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E) (EuclideanSpace.single i 1) : E))
          b i)
        ((fun (b : OrthonormalBasis ι 𝕜 E) (i : ι) ↦
            ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E) (EuclideanSpace.single i 1) : E))
          b' i)),
    Eq.{u_4 + 1} (α := E)
      (((↑b.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
              (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜)) :
            (a : (i : ι) → 𝕜) → E)
          (HSMul.hSMul (β := (j : ι) → 𝕜) k (Pi.single (M := fun (i : ι) ↦ 𝕜) i 1)) :
        E)
      (((↑b'.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) ∘ₗ
              (↑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (ι → 𝕜))) : (ι → 𝕜) →ₗ[𝕜] WithLp 2 (ι → 𝕜)) :
            (a : (i : ι) → 𝕜) → E)
          (HSMul.hSMul (β := (j : ι) → 𝕜) k (Pi.single (M := fun (i : ι) ↦ 𝕜) i 1)) :
        E)
rw₈ :
  ∀ (i : ι) (k : 𝕜) (this : k = HSMul.hSMul (β := 𝕜) k 1)
    (h :
      Eq.{u_4 + 1} (α := E) ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E) (EuclideanSpace.single i 1) : E)
        ((b'.repr.symm : (a : EuclideanSpace 𝕜 ι) → E) (EuclideanSpace.single i 1) : E)),
    HSMul.hSMul (β := E) k ((b.repr.symm : (a : WithLp 2 (ι → 𝕜)) → E) (PiLp.single 2 (β := fun (i : ι) ↦ 𝕜) i 1) : E) =
      HSMul.hSMul (β := E) k
        ((b'.repr.symm : (a : WithLp 2 (ι → 𝕜)) → E) (PiLp.single 2 (β := fun (i : ι) ↦ 𝕜) i 1) : E)
⊢ (↑b.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) = (↑b'.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E)

Tactic:
classical
        rw [← LinearMap.cancel_right (WithLp.linearEquiv 2 𝕜 (_ → 𝕜)).symm.surjective]
        simp +instances only
        refine LinearMap.pi_ext fun i k => ?_
        have : k = k • (1 : 𝕜) := by rw [smul_eq_mul, mul_one]
        rw [this, Pi.single_smul]
        replace h := congr_fun h i
        simp only [LinearEquiv.comp_coe, map_smul, LinearEquiv.coe_coe, LinearEquiv.trans_apply,
          coe_symm_linearEquiv, PiLp.toLp_single,
          LinearIsometryEquiv.coe_symm_toLinearEquiv] at h ⊢
        rw [h]

Premises used: LinearEquiv.symm, PiLp.toLp_single, LinearMap.pi_ext, LinearEquiv.surjective, LinearMap.cancel_right, LinearEquiv.trans_apply, Pi.single_smul, LinearIsometryEquiv.coe_symm_toLinearEquiv, LinearEquiv.comp_coe, OfNat.ofNat, WithLp.coe_symm_linearEquiv, LinearEquiv.coe_coe, WithLp.linearEquiv, map_smul