awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
pos :
  ∀ (h : 0 < r),
    ContDiffOn ℝ (↑n : WithTop ℕ∞)
      (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯)) : E → E)
      (ball c r)
⊢ ContDiffOn ℝ (F := E) (↑n : WithTop ℕ∞)
    (↑(OpenPartialHomeomorph.symm
          (if h : 0 < r then OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯
          else Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))) :
      E → E)
    (ball c r)
have neg : ∀ (h : ¬0 < r),
  ContDiffOn ℝ (↑n : WithTop ℕ∞)
    (↑(OpenPartialHomeomorph.symm
          (Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c)))) :
      E → E)
    (ball c r)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ ContDiffOn ℝ (↑n : WithTop ℕ∞)
    (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯)) : E → E)
    (ball c r)
have pos : Set.MapsTo (↑(toPartialEquiv (unitBallBall c r h)).symm : E → E) (ball c r) (ball 0 1)
Tactic: refine contDiffOn_univUnitBall_symm.comp (contDiff_unitBallBall_symm h).contDiffOn ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Calculus (goal)
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ Set.MapsTo (↑(toPartialEquiv (unitBallBall c r h)).symm : E → E) (ball c r) (ball 0 1)
have pos : Set.MapsTo (↑(toPartialEquiv (unitBallBall c r h)).symm : E → E) (toPartialEquiv (unitBallBall c r h)).target
  (toPartialEquiv (unitBallBall c r h)).source
Tactic: rw [← unitBallBall_source c r h, ← unitBallBall_target c r h]
-- 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
⊢ 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))
have e_f : ∀ (m : Fin (Module.finrank ℝ E)),
  Eq (α := E ⊗[ℝ] E)
    ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) m : E ⊗[ℝ] 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) :
      E ⊗[ℝ] E)
Tactic: congr 1 with m
-- 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
m : Fin (Module.finrank ℝ E)
⊢ Eq (α := E ⊗[ℝ] E)
    ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) m : E ⊗[ℝ] 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) :
      E ⊗[ℝ] E)
have e_f : (w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) m =
  HSMul.hSMul (α := ℝ) (β := E ⊗[ℝ] E) (if m = m then 1 else 0)
    ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) m : E ⊗[ℝ] E)
Tactic: rw [Fintype.sum_eq_single m _, orthonormal_iff_ite.1 w.orthonormal]
-- 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
m : Fin (Module.finrank ℝ E)
e_f :
  (w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) m =
    HSMul.hSMul (α := ℝ) (β := E ⊗[ℝ] E) (if m = m then 1 else 0)
      ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) m : E ⊗[ℝ] E)
⊢ Eq (α := E ⊗[ℝ] E)
    ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) m : E ⊗[ℝ] 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) :
      E ⊗[ℝ] E)
have rw : ∀ (x : Fin (Module.finrank ℝ E)),
  x ≠ m →
    HSMul.hSMul (β := E ⊗[ℝ] E)
        (inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) m : E)
          ((w : (a : Fin (Module.finrank ℝ E)) → E) x : E))
        ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) x : E ⊗[ℝ] E) =
      0
Tactic: rw [Fintype.sum_eq_single m _, orthonormal_iff_ite.1 w.orthonormal]
-- 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
m : Fin (Module.finrank ℝ E)
⊢ ∀ (x : Fin (Module.finrank ℝ E)),
    x ≠ m →
      HSMul.hSMul (β := E ⊗[ℝ] E)
          (inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) m : E)
            ((w : (a : Fin (Module.finrank ℝ E)) → E) x : E))
          ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) x : E ⊗[ℝ] E) =
        0
have simp : ∀ (x : Fin (Module.finrank ℝ E)),
  x ≠ m →
    m = x →
      Eq (α := E ⊗[ℝ] E)
        ((w : (a : Fin (Module.finrank ℝ E)) → E) m ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) x : E ⊗[ℝ] E)
        (0 : E ⊗[ℝ] E)
Tactic: simp only [orthonormal_iff_ite.1 w.orthonormal, ite_smul, one_smul, zero_smul,
      ite_eq_right_iff]
-- 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
⊢ 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))
have simp : Eq.{u_1 + 1} (α := E ⊗[ℝ] E)
  (∑ x : Fin (Module.finrank ℝ E),
    ∑ x_1 : Fin (Module.finrank ℝ E),
      ∑ i : ι,
        HSMul.hSMul (β := E ⊗[ℝ] E)
          (inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) x : E) ((v : (a : ι) → E) i : E) *
            inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) x_1 : E) ((v : (a : ι) → E) i : E))
          ((w : (a : Fin (Module.finrank ℝ E)) → E) x ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) x_1 : E ⊗[ℝ] E))
  (∑ x : Fin (Module.finrank ℝ E),
    ∑ y : Fin (Module.finrank ℝ E),
      ∑ x_1 : ι,
        HSMul.hSMul (β := E ⊗[ℝ] E)
          (inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) y : E) ((v : (a : ι) → E) x_1 : E) *
            inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) x : E) ((v : (a : ι) → E) x_1 : E))
          ((w : (a : Fin (Module.finrank ℝ E)) → E) y ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) x : E ⊗[ℝ] E))
Tactic: simp only [sum_tmul, tmul_sum, smul_tmul_smul, Finset.sum_comm (γ := ι), Finset.sum_smul]
-- 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
⊢ Eq.{u_1 + 1} (α := E ⊗[ℝ] E)
    (∑ x : Fin (Module.finrank ℝ E),
      ∑ x_1 : Fin (Module.finrank ℝ E),
        ∑ i : ι,
          HSMul.hSMul (β := E ⊗[ℝ] E)
            (inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) x : E) ((v : (a : ι) → E) i : E) *
              inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) x_1 : E) ((v : (a : ι) → E) i : E))
            ((w : (a : Fin (Module.finrank ℝ E)) → E) x ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) x_1 : E ⊗[ℝ] E))
    (∑ x : Fin (Module.finrank ℝ E),
      ∑ y : Fin (Module.finrank ℝ E),
        ∑ x_1 : ι,
          HSMul.hSMul (β := E ⊗[ℝ] E)
            (inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) y : E) ((v : (a : ι) → E) x_1 : E) *
              inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) x : E) ((v : (a : ι) → E) x_1 : E))
            ((w : (a : Fin (Module.finrank ℝ E)) → E) y ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) x : E ⊗[ℝ] E))
have rw : Eq.{u_1 + 1} (α := E ⊗[ℝ] E)
  (∑ y : Fin (Module.finrank ℝ E),
    ∑ x : Fin (Module.finrank ℝ E),
      ∑ i : ι,
        HSMul.hSMul (β := E ⊗[ℝ] E)
          (inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) x : E) ((v : (a : ι) → E) i : E) *
            inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) y : E) ((v : (a : ι) → E) i : E))
          ((w : (a : Fin (Module.finrank ℝ E)) → E) x ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) y : E ⊗[ℝ] E))
  (∑ x : Fin (Module.finrank ℝ E),
    ∑ y : Fin (Module.finrank ℝ E),
      ∑ x_1 : ι,
        HSMul.hSMul (β := E ⊗[ℝ] E)
          (inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) y : E) ((v : (a : ι) → E) x_1 : E) *
            inner ℝ (E := E) ((w : (a : Fin (Module.finrank ℝ E)) → E) x : E) ((v : (a : ι) → E) x_1 : E))
          ((w : (a : Fin (Module.finrank ℝ E)) → E) y ⊗ₜ[ℝ] (w : (a : Fin (Module.finrank ℝ E)) → E) x : E ⊗[ℝ] E))
Tactic: rw [Finset.sum_comm]
-- 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
⊢ Eq (α := E ⊗[ℝ] E) (canonicalCovariantTensor E) (∑ i : ι, (v : (a : ι) → E) i ⊗ₜ[ℝ] (v : (a : ι) → E) i)
have 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))
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 _)]
-- 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))
⊢ Eq (α := E ⊗[ℝ] E) (canonicalCovariantTensor E) (∑ i : ι, (v : (a : ι) → E) i ⊗ₜ[ℝ] (v : (a : ι) → E) i)
have 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))
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 _)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_3
inst_1 : Fintype n
inst_2 : DecidableEq n
⊢ comul =
    map (↑(↑(equiv n 𝕜) : EuclideanSpace 𝕜 n ≃ₗ[𝕜] n → 𝕜) : EuclideanSpace 𝕜 n →ₗ[𝕜] n → 𝕜)
        (↑(↑(equiv n 𝕜) : EuclideanSpace 𝕜 n ≃ₗ[𝕜] n → 𝕜) : EuclideanSpace 𝕜 n →ₗ[𝕜] n → 𝕜) ∘ₗ
      (adjoint :
            (a : EuclideanSpace 𝕜 n ⊗[𝕜] EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) →
              EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n ⊗[𝕜] EuclideanSpace 𝕜 n)
          ((↑(↑(ContinuousLinearEquiv.symm (equiv n 𝕜)) : (n → 𝕜) ≃ₗ[𝕜] EuclideanSpace 𝕜 n) :
              (n → 𝕜) →ₗ[𝕜] EuclideanSpace 𝕜 n) ∘ₗ
            mul' 𝕜 (n → 𝕜) ∘ₗ
              map (↑(↑(equiv n 𝕜) : EuclideanSpace 𝕜 n ≃ₗ[𝕜] n → 𝕜) : EuclideanSpace 𝕜 n →ₗ[𝕜] n → 𝕜)
                (↑(↑(equiv n 𝕜) : EuclideanSpace 𝕜 n ≃ₗ[𝕜] n → 𝕜) : EuclideanSpace 𝕜 n →ₗ[𝕜] n → 𝕜)) ∘ₗ
        (↑(↑(ContinuousLinearEquiv.symm (equiv n 𝕜)) : (n → 𝕜) ≃ₗ[𝕜] EuclideanSpace 𝕜 n) :
          (n → 𝕜) →ₗ[𝕜] EuclideanSpace 𝕜 n)
have h : ∀ (i : n),
  Eq (α := (n → 𝕜) ⊗[𝕜] (n → 𝕜))
    (((comul ∘ₗ LinearMap.single 𝕜 (fun (i : n) ↦ 𝕜) i : 𝕜 →ₗ[𝕜] (n → 𝕜) ⊗[𝕜] (n → 𝕜)) : (a : 𝕜) → (n → 𝕜) ⊗[𝕜] (n → 𝕜))
      1)
    (((map (↑(↑(equiv n 𝕜) : EuclideanSpace 𝕜 n ≃ₗ[𝕜] n → 𝕜) : EuclideanSpace 𝕜 n →ₗ[𝕜] n → 𝕜)
              (↑(↑(equiv n 𝕜) : EuclideanSpace 𝕜 n ≃ₗ[𝕜] n → 𝕜) : EuclideanSpace 𝕜 n →ₗ[𝕜] n → 𝕜) ∘ₗ
            (adjoint :
                  (a : EuclideanSpace 𝕜 n ⊗[𝕜] EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) →
                    EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n ⊗[𝕜] EuclideanSpace 𝕜 n)
                ((↑(↑(ContinuousLinearEquiv.symm (equiv n 𝕜)) : (n → 𝕜) ≃ₗ[𝕜] EuclideanSpace 𝕜 n) :
                    (n → 𝕜) →ₗ[𝕜] EuclideanSpace 𝕜 n) ∘ₗ
                  mul' 𝕜 (n → 𝕜) ∘ₗ
                    map (↑(↑(equiv n 𝕜) : EuclideanSpace 𝕜 n ≃ₗ[𝕜] n → 𝕜) : EuclideanSpace 𝕜 n →ₗ[𝕜] n → 𝕜)
                      (↑(↑(equiv n 𝕜) : EuclideanSpace 𝕜 n ≃ₗ[𝕜] n → 𝕜) : EuclideanSpace 𝕜 n →ₗ[𝕜] n → 𝕜)) ∘ₗ
              (↑(↑(ContinuousLinearEquiv.symm (equiv n 𝕜)) : (n → 𝕜) ≃ₗ[𝕜] EuclideanSpace 𝕜 n) :
                (n → 𝕜) →ₗ[𝕜] EuclideanSpace 𝕜 n)) ∘ₗ
          LinearMap.single 𝕜 (fun (i : n) ↦ 𝕜) i :
        (a : 𝕜) → (n → 𝕜) ⊗[𝕜] (n → 𝕜))
      1)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_3
inst_1 : Fintype n
inst_2 : DecidableEq n
i : n
⊢ Eq (α := (n → 𝕜) ⊗[𝕜] (n → 𝕜))
    (((comul ∘ₗ LinearMap.single 𝕜 (fun (i : n) ↦ 𝕜) i : 𝕜 →ₗ[𝕜] (n → 𝕜) ⊗[𝕜] (n → 𝕜)) : (a : 𝕜) → (n → 𝕜) ⊗[𝕜] (n → 𝕜))
      1)
    (((map (↑(↑(equiv n 𝕜) : EuclideanSpace 𝕜 n ≃ₗ[𝕜] n → 𝕜) : EuclideanSpace 𝕜 n →ₗ[𝕜] n → 𝕜)
              (↑(↑(equiv n 𝕜) : EuclideanSpace 𝕜 n ≃ₗ[𝕜] n → 𝕜) : EuclideanSpace 𝕜 n →ₗ[𝕜] n → 𝕜) ∘ₗ
            (adjoint :
                  (a : EuclideanSpace 𝕜 n ⊗[𝕜] EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) →
                    EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n ⊗[𝕜] EuclideanSpace 𝕜 n)
                ((↑(↑(ContinuousLinearEquiv.symm (equiv n 𝕜)) : (n → 𝕜) ≃ₗ[𝕜] EuclideanSpace 𝕜 n) :
                    (n → 𝕜) →ₗ[𝕜] EuclideanSpace 𝕜 n) ∘ₗ
                  mul' 𝕜 (n → 𝕜) ∘ₗ
                    map (↑(↑(equiv n 𝕜) : EuclideanSpace 𝕜 n ≃ₗ[𝕜] n → 𝕜) : EuclideanSpace 𝕜 n →ₗ[𝕜] n → 𝕜)
                      (↑(↑(equiv n 𝕜) : EuclideanSpace 𝕜 n ≃ₗ[𝕜] n → 𝕜) : EuclideanSpace 𝕜 n →ₗ[𝕜] n → 𝕜)) ∘ₗ
              (↑(↑(ContinuousLinearEquiv.symm (equiv n 𝕜)) : (n → 𝕜) ≃ₗ[𝕜] EuclideanSpace 𝕜 n) :
                (n → 𝕜) →ₗ[𝕜] EuclideanSpace 𝕜 n)) ∘ₗ
          LinearMap.single 𝕜 (fun (i : n) ↦ 𝕜) i :
        (a : 𝕜) → (n → 𝕜) ⊗[𝕜] (n → 𝕜))
      1)
have h : Eq (α := EuclideanSpace 𝕜 n ⊗[𝕜] EuclideanSpace 𝕜 n)
  (((TensorProduct.congr (↑(equiv n 𝕜) : EuclideanSpace 𝕜 n ≃ₗ[𝕜] n → 𝕜)
          (↑(equiv n 𝕜) : EuclideanSpace 𝕜 n ≃ₗ[𝕜] n → 𝕜)).symm :
      (a : (n → 𝕜) ⊗[𝕜] (n → 𝕜)) → EuclideanSpace 𝕜 n ⊗[𝕜] EuclideanSpace 𝕜 n)
    ((comul : (a : (i : n) → 𝕜) → (n → 𝕜) ⊗[𝕜] (n → 𝕜))
      (((LinearMap.single 𝕜 (fun (i : n) ↦ 𝕜) i : 𝕜 →ₗ[𝕜] (i : n) → 𝕜) : (a : 𝕜) → (i : n) → 𝕜) 1)))
  ((((adjoint :
            (a : EuclideanSpace 𝕜 n ⊗[𝕜] EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) →
              EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n ⊗[𝕜] EuclideanSpace 𝕜 n)
          ((↑(↑(ContinuousLinearEquiv.symm (equiv n 𝕜)) : (n → 𝕜) ≃ₗ[𝕜] EuclideanSpace 𝕜 n) :
              (n → 𝕜) →ₗ[𝕜] EuclideanSpace 𝕜 n) ∘ₗ
            mul' 𝕜 (n → 𝕜) ∘ₗ
              (↑(TensorProduct.congr (↑(equiv n 𝕜) : EuclideanSpace 𝕜 n ≃ₗ[𝕜] n → 𝕜)
                    (↑(equiv n 𝕜) : EuclideanSpace 𝕜 n ≃ₗ[𝕜] n → 𝕜)) :
                EuclideanSpace 𝕜 n ⊗[𝕜] EuclideanSpace 𝕜 n →ₗ[𝕜] (n → 𝕜) ⊗[𝕜] (n → 𝕜))) :
        EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n ⊗[𝕜] EuclideanSpace 𝕜 n) :
      (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n ⊗[𝕜] EuclideanSpace 𝕜 n)
    (((↑(ContinuousLinearEquiv.symm (equiv n 𝕜)) : (n → 𝕜) ≃ₗ[𝕜] EuclideanSpace 𝕜 n) :
        (a : (i : n) → 𝕜) → EuclideanSpace 𝕜 n)
      (((LinearMap.single 𝕜 (fun (i : n) ↦ 𝕜) i : 𝕜 →ₗ[𝕜] (i : n) → 𝕜) : (a : 𝕜) → (i : n) → 𝕜) 1)))
Tactic: simp only [comp_apply, ← toLinearMap_congr, LinearEquiv.coe_coe, ← LinearEquiv.symm_apply_eq]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_3
inst_1 : Fintype n
inst_2 : DecidableEq n
⊢ counit =
    (adjoint : (a : 𝕜 →ₗ[𝕜] EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →ₗ[𝕜] 𝕜)
        ((↑(↑(ContinuousLinearEquiv.symm (equiv n 𝕜)) : (n → 𝕜) ≃ₗ[𝕜] EuclideanSpace 𝕜 n) :
            (n → 𝕜) →ₗ[𝕜] EuclideanSpace 𝕜 n) ∘ₗ
          Algebra.linearMap 𝕜 (n → 𝕜)) ∘ₗ
      (↑(↑(ContinuousLinearEquiv.symm (equiv n 𝕜)) : (n → 𝕜) ≃ₗ[𝕜] EuclideanSpace 𝕜 n) :
        (n → 𝕜) →ₗ[𝕜] EuclideanSpace 𝕜 n)
have h : ∀ (i : n),
  Eq (α := 𝕜) (((counit ∘ₗ LinearMap.single 𝕜 (fun (i : n) ↦ 𝕜) i : 𝕜 →ₗ[𝕜] 𝕜) : (a : 𝕜) → 𝕜) 1 : 𝕜)
    ((((adjoint : (a : 𝕜 →ₗ[𝕜] EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n →ₗ[𝕜] 𝕜)
                ((↑(↑(ContinuousLinearEquiv.symm (equiv n 𝕜)) : (n → 𝕜) ≃ₗ[𝕜] EuclideanSpace 𝕜 n) :
                    (n → 𝕜) →ₗ[𝕜] EuclideanSpace 𝕜 n) ∘ₗ
                  Algebra.linearMap 𝕜 (n → 𝕜)) ∘ₗ
              (↑(↑(ContinuousLinearEquiv.symm (equiv n 𝕜)) : (n → 𝕜) ≃ₗ[𝕜] EuclideanSpace 𝕜 n) :
                (n → 𝕜) →ₗ[𝕜] EuclideanSpace 𝕜 n)) ∘ₗ
            LinearMap.single 𝕜 (fun (i : n) ↦ 𝕜) i :
          (a : 𝕜) → 𝕜)
        1 :
      𝕜)
Tactic: ext