-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
ι : Type u_4
ι' : Type u_5
ι'' : Type u_6
E' : Type u_7
inst_5 : SeminormedAddCommGroup E'
inst_6 : InnerProductSpace 𝕜 E'
E'' : Type u_8
inst_7 : SeminormedAddCommGroup E''
inst_8 : InnerProductSpace 𝕜 E''
f : E ≃ₗ[𝕜] E'
v : Basis ι 𝕜 E
hv : Orthonormal.{u_1, u_2, u_4} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
hf :
  Orthonormal.{u_1, u_7, u_4} 𝕜 (E := E') (ι := ι)
    (Function.comp.{u_4 + 1, u_2 + 1, u_7 + 1} (β := E) (⇑(↑f : E →ₗ[𝕜] E') : (a : E) → E') (⇑v : (a : ι) → E))
x y : E
classical :
  inner.{u_1, u_7} 𝕜 (E := E')
      ((f : (a : E) → E')
          ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E) :
        E')
      ((f : (a : E) → E') y : E') =
    ⟪(linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜), y⟫
classical₁ :
  inner.{u_1, u_7} 𝕜 (E := E')
      ((f : (a : E) → E')
          ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E) :
        E')
      ((f : (a : E) → E')
          ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E) :
        E') =
    inner.{u_1, u_2} 𝕜 (E := E)
      ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E)
      ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E)
classical₂ :
  inner.{u_1, u_7} 𝕜 (E := E')
      (((↑f : E →ₗ[𝕜] E') : (a : E) → E')
          ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E) :
        E')
      (((↑f : E →ₗ[𝕜] E') : (a : E) → E')
          ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E) :
        E') =
    inner.{u_1, u_2} 𝕜 (E := E)
      ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E)
      ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E)
classical₃ :
  inner.{u_1, u_7} 𝕜 (E := E')
      ((linearCombination 𝕜
              (Function.comp.{u_4 + 1, u_2 + 1, u_7 + 1} (β := E) (⇑(↑f : E →ₗ[𝕜] E') : (a : E) → E')
                (⇑v : (a : ι) → E)) :
            (a : ι →₀ 𝕜) → E')
          ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) :
        E')
      (((↑f : E →ₗ[𝕜] E') : (a : E) → E')
          ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E) :
        E') =
    inner.{u_1, u_2} 𝕜 (E := E)
      ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E)
      ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E)
classical₄ :
  inner.{u_1, u_7} 𝕜 (E := E')
      ((linearCombination 𝕜
              (Function.comp.{u_4 + 1, u_2 + 1, u_7 + 1} (β := E) (⇑(↑f : E →ₗ[𝕜] E') : (a : E) → E')
                (⇑v : (a : ι) → E)) :
            (a : ι →₀ 𝕜) → E')
          ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) :
        E')
      ((linearCombination 𝕜
              (Function.comp.{u_4 + 1, u_2 + 1, u_7 + 1} (β := E) (⇑(↑f : E →ₗ[𝕜] E') : (a : E) → E')
                (⇑v : (a : ι) → E)) :
            (a : ι →₀ 𝕜) → E')
          ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) :
        E') =
    inner.{u_1, u_2} 𝕜 (E := E)
      ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E)
      ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E)
classical₅ :
  inner.{u_1, u_7} 𝕜 (E := E')
      ((linearCombination 𝕜
              (Function.comp.{u_4 + 1, u_2 + 1, u_7 + 1} (β := E) (⇑(↑f : E →ₗ[𝕜] E') : (a : E) → E')
                (⇑v : (a : ι) → E)) :
            (a : ι →₀ 𝕜) → E')
          ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) :
        E')
      ((linearCombination 𝕜
              (Function.comp.{u_4 + 1, u_2 + 1, u_7 + 1} (β := E) (⇑(↑f : E →ₗ[𝕜] E') : (a : E) → E')
                (⇑v : (a : ι) → E)) :
            (a : ι →₀ 𝕜) → E')
          ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) :
        E') =
    sum ((v.repr : (a : E) → ι →₀ 𝕜) x) fun (i : ι) (y_1 : 𝕜) ↦
      HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y_1 : 𝕜)
        ((((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : (a : ι) → 𝕜) i : 𝕜)
⊢ inner.{u_1, u_7} 𝕜 (E := E') ((f : (a : E) → E') x : E') ((f : (a : E) → E') y : E') = ⟪x, y⟫
have classical₆ : Eq.{u_1 + 1} (α := 𝕜)
  (sum ((v.repr : (a : E) → ι →₀ 𝕜) x) fun (i : ι) (y_1 : 𝕜) ↦
    HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y_1 : 𝕜)
      ((((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : (a : ι) → 𝕜) i : 𝕜))
  (sum ((v.repr : (a : E) → ι →₀ 𝕜) x) fun (i : ι) (y_1 : 𝕜) ↦
    HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y_1 : 𝕜)
      ((((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : (a : ι) → 𝕜) i : 𝕜))
Tactic: classical rw [← v.linearCombination_repr x, ← v.linearCombination_repr y,
      ← LinearEquiv.coe_coe f, Finsupp.apply_linearCombination,
      Finsupp.apply_linearCombination, hv.inner_finsupp_eq_sum_left, hf.inner_finsupp_eq_sum_left]