-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.CanonicalTensor (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
ι : Type u_2
inst_3 : Fintype ι
v : OrthonormalBasis ι ℝ E
w : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
calc :
  Eq.{u_1 + 1} (α := E ⊗[ℝ] E)
    (∑ m : Fin (Module.finrank ℝ E),
      (w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) m)
    (∑ m : Fin (Module.finrank ℝ E),
      ∑ n : Fin (Module.finrank ℝ E),
        HSMul.hSMul (β := E ⊗[ℝ] E)
          (inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) m : E)
            ((w : (a : Fin (Module.finrank ℝ E)) → E) n : E))
          ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) n : E ⊗[ℝ] E))
calc₁ :
  Eq.{u_1 + 1} (α := E ⊗[ℝ] E)
    (∑ m : Fin (Module.finrank ℝ E),
      ∑ n : Fin (Module.finrank ℝ E),
        HSMul.hSMul (β := E ⊗[ℝ] E)
          (inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) m : E)
            ((w : (a : Fin (Module.finrank ℝ E)) → E) n : E))
          ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) n : E ⊗[ℝ] E))
    (∑ m : Fin (Module.finrank ℝ E),
      ∑ n : Fin (Module.finrank ℝ E),
        HSMul.hSMul (α := ℝ) (β := E ⊗[ℝ] E)
          (∑ i : ι,
            inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) m : E) ((v : (a : ι) → E) i : E) *
              inner.{0, u_1} ℝ (E := E) ((v : (a : ι) → E) i : E) ((w : (a : Fin (Module.finrank ℝ E)) → E) n : E))
          ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) n : E ⊗[ℝ] E))
calc₂ :
  Eq.{u_1 + 1} (α := E ⊗[ℝ] E)
    (∑ m : Fin (Module.finrank ℝ E),
      ∑ n : Fin (Module.finrank ℝ E),
        HSMul.hSMul (α := ℝ) (β := E ⊗[ℝ] E)
          (∑ i : ι,
            inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) m : E) ((v : (a : ι) → E) i : E) *
              inner.{0, u_1} ℝ (E := E) ((v : (a : ι) → E) i : E) ((w : (a : Fin (Module.finrank ℝ E)) → E) n : E))
          ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) n : E ⊗[ℝ] E))
    (∑ m : Fin (Module.finrank ℝ E),
      ∑ n : Fin (Module.finrank ℝ E),
        HSMul.hSMul (α := ℝ) (β := E ⊗[ℝ] E)
          (∑ i : ι,
            inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) m : E) ((v : (a : ι) → E) i : E) *
              inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) n : E) ((v : (a : ι) → E) i : E))
          ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) n : E ⊗[ℝ] E))
calc₃ :
  Eq.{u_1 + 1} (α := E ⊗[ℝ] E)
    (∑ m : Fin (Module.finrank ℝ E),
      ∑ n : Fin (Module.finrank ℝ E),
        HSMul.hSMul (α := ℝ) (β := E ⊗[ℝ] E)
          (∑ i : ι,
            inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) m : E) ((v : (a : ι) → E) i : E) *
              inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) n : E) ((v : (a : ι) → E) i : E))
          ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) n : E ⊗[ℝ] E))
    (∑ i : ι,
      (∑ m : Fin (Module.finrank ℝ E),
          HSMul.hSMul (β := E)
            (inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) m : E) ((v : (a : ι) → E) i : E))
            ((w : (a : Fin (Module.finrank ℝ E)) → E) m : E)) ⊗ₜ[ℝ]
        ∑ n : Fin (Module.finrank ℝ E),
          HSMul.hSMul (β := E)
            (inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) n : E) ((v : (a : ι) → E) i : E))
            ((w : (a : Fin (Module.finrank ℝ E)) → E) n : E))
⊢ Eq (α := E ⊗[ℝ] E) (canonicalCovariantTensor E) (∑ i : ι, (v : (a : ι) → E) i ⊗ₜ[ℝ] (v : (a : ι) → E) i)
have calc₄ : Eq.{u_1 + 1} (α := E ⊗[ℝ] E)
  (∑ i : ι,
    (∑ m : Fin (Module.finrank ℝ E),
        HSMul.hSMul (β := E)
          (inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) m : E) ((v : (a : ι) → E) i : E))
          ((w : (a : Fin (Module.finrank ℝ E)) → E) m : E)) ⊗ₜ[ℝ]
      ∑ n : Fin (Module.finrank ℝ E),
        HSMul.hSMul (β := E)
          (inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) n : E) ((v : (a : ι) → E) i : E))
          ((w : (a : Fin (Module.finrank ℝ E)) → E) n : E))
  (∑ i : ι, (v : (a : ι) → E) i ⊗ₜ[ℝ] (v : (a : ι) → E) i)
Tactic: calc ∑ m, w m ⊗ₜ[ℝ] w m
  _ = ∑ m, ∑ n, ⟪w m, w n⟫_ℝ • w m ⊗ₜ[ℝ] w n := by
    congr 1 with m
    rw [Fintype.sum_eq_single m _, orthonormal_iff_ite.1 w.orthonormal]
    · simp only [↓reduceIte, one_smul]
    simp only [orthonormal_iff_ite.1 w.orthonormal, ite_smul, one_smul, zero_smul,
      ite_eq_right_iff]
    tauto
  _ = ∑ m, ∑ n, (∑ i, ⟪w m, v i⟫_ℝ * ⟪v i, w n⟫_ℝ) • w m ⊗ₜ[ℝ] w n := by
    simp_rw [OrthonormalBasis.sum_inner_mul_inner v]
  _ = ∑ m, ∑ n, (∑ i, ⟪w m, v i⟫_ℝ * ⟪w n, v i⟫_ℝ) • w m ⊗ₜ[ℝ] w n := by
    simp only [real_inner_comm (w _)]
  _ = ∑ i, (∑ m, ⟪w m, v i⟫_ℝ • w m) ⊗ₜ[ℝ] ∑ n, ⟪w n, v i⟫_ℝ • w n := by
    simp only [sum_tmul, tmul_sum, smul_tmul_smul, Finset.sum_comm (γ := ι), Finset.sum_smul]
    rw [Finset.sum_comm]
  _ = ∑ i, v i ⊗ₜ[ℝ] v i := by
    simp only [w.sum_repr' (v _)]