-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
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)
⊢ (↑b.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E) = (↑b'.repr.symm : EuclideanSpace 𝕜 ι →ₗ[𝕜] E)
have 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)
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]