awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.CanonicalTensor
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
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))
⊢ 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))

Tactic:
simp only [sum_tmul, tmul_sum, smul_tmul_smul, Finset.sum_comm (γ := ι), Finset.sum_smul]

Premises used: Finset.sum_smul, TensorProduct.sum_tmul, TensorProduct.tmul_sum, TensorProduct.smul_tmul_smul, Finset.sum_comm
-- Module: Mathlib.Analysis.InnerProductSpace.CanonicalTensor
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
rw 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))
⊢ 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:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.Analysis.InnerProductSpace.CanonicalTensor
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)
    (∑ 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:
simp only [w.sum_repr' (v _)]

Premises used: DFunLike.coe, OrthonormalBasis.sum_repr'
-- Module: Mathlib.Analysis.InnerProductSpace.Coalgebra
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_3
inst_1 : Fintype n
inst_2 : DecidableEq n
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.Coalgebra
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_3
inst_1 : Fintype n
inst_2 : DecidableEq n
i : n
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)))
⊢ 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:
simp only [comp_apply, ← toLinearMap_congr, LinearEquiv.coe_coe, ← LinearEquiv.symm_apply_eq]

Premises used: LinearEquiv.symm_apply_eq, LinearMap.comp_apply, TensorProduct.toLinearMap_congr, LinearEquiv.coe_coe
-- Module: Mathlib.Analysis.InnerProductSpace.Coalgebra
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_3
inst_1 : Fintype n
inst_2 : DecidableEq n
i : n
⊢ 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 [TensorProduct.ext_iff_inner_left, adjoint_inner_right, inner_eq_star_dotProduct]

Premises used: TensorProduct.ext_iff_inner_left, LinearMap.adjoint_inner_right, EuclideanSpace.inner_eq_star_dotProduct
-- Module: Mathlib.Analysis.InnerProductSpace.Coalgebra
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_3
inst_1 : Fintype n
inst_2 : DecidableEq n
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 :
        𝕜)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.Coalgebra
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_3
inst_1 : Fintype n
inst_2 : DecidableEq n
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:
simp [← toSpanSingleton_one_eq_algebraLinearMap, comp_toSpanSingleton,
    adjoint_toSpanSingleton, inner_eq_star_dotProduct]

Premises used: LinearMap.comp_toSpanSingleton, LinearMap.toSpanSingleton_one_eq_algebraLinearMap, LinearMap.adjoint_toSpanSingleton, EuclideanSpace.inner_eq_star_dotProduct
-- Module: Mathlib.Analysis.InnerProductSpace.Coalgebra
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
A : Type u_3
inst_4 : Ring A
inst_5 : Module 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
e : E ≃ₗ[𝕜] A
rw :
  Eq.{u_2 + 1} (α := E →ₗ[𝕜] E ⊗[𝕜] (E ⊗[𝕜] E))
    ((adjoint : (a : E ⊗[𝕜] (E ⊗[𝕜] E) →ₗ[𝕜] E ⊗[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E ⊗[𝕜] E →ₗ[𝕜] E ⊗[𝕜] (E ⊗[𝕜] E))
        (↑(toLinearEquiv (LinearIsometryEquiv.symm (assocIsometry 𝕜 E E E))) :
          E ⊗[𝕜] (E ⊗[𝕜] E) →ₗ[𝕜] E ⊗[𝕜] E ⊗[𝕜] E) ∘ₗ
      (adjoint : (a : E ⊗[𝕜] E ⊗[𝕜] E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E ⊗[𝕜] E ⊗[𝕜] E)
          (LinearMap.rTensor E ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A))) ∘ₗ
        (adjoint : (a : E ⊗[𝕜] E →ₗ[𝕜] E) → E →ₗ[𝕜] E ⊗[𝕜] E)
          ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)))
    ((adjoint : (a : E ⊗[𝕜] (E ⊗[𝕜] E) →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E ⊗[𝕜] (E ⊗[𝕜] E))
        (LinearMap.lTensor E ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A))) ∘ₗ
      (adjoint : (a : E ⊗[𝕜] E →ₗ[𝕜] E) → E →ₗ[𝕜] E ⊗[𝕜] E)
        ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)))
⊢ Eq (α := E →ₗ[𝕜] E ⊗[𝕜] (E ⊗[𝕜] E))
    ((↑(TensorProduct.assoc 𝕜 E E E) : E ⊗[𝕜] E ⊗[𝕜] E →ₗ[𝕜] E ⊗[𝕜] (E ⊗[𝕜] E)) ∘ₗ
      LinearMap.rTensor E
          ((adjoint : (a : E ⊗[𝕜] E →ₗ[𝕜] E) → E →ₗ[𝕜] E ⊗[𝕜] E)
            ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A))) ∘ₗ
        (adjoint : (a : E ⊗[𝕜] E →ₗ[𝕜] E) → E →ₗ[𝕜] E ⊗[𝕜] E)
          ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)))
    (LinearMap.lTensor E
        ((adjoint : (a : E ⊗[𝕜] E →ₗ[𝕜] E) → E →ₗ[𝕜] E ⊗[𝕜] E)
          ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A))) ∘ₗ
      (adjoint : (a : E ⊗[𝕜] E →ₗ[𝕜] E) → E →ₗ[𝕜] E ⊗[𝕜] E)
        ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)))

Tactic:
rw [← adjoint_lTensor, ← adjoint_rTensor, ← toLinearEquiv_assocIsometry,
      ← (assocIsometry 𝕜 _ _ _).symm_symm, ← adjoint_toLinearMap_eq_symm]

Premises used: LinearIsometryEquiv.adjoint_toLinearMap_eq_symm, LinearMap.adjoint_rTensor, LinearMap.adjoint_lTensor, TensorProduct.assocIsometry, TensorProduct.toLinearEquiv_assocIsometry, LinearIsometryEquiv.symm_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Coalgebra
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
A : Type u_3
inst_4 : Ring A
inst_5 : Module 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
e : E ≃ₗ[𝕜] A
simp_rw :
  Eq (α := E →ₗ[𝕜] E ⊗[𝕜] (E ⊗[𝕜] E))
    ((adjoint : (a : E ⊗[𝕜] (E ⊗[𝕜] E) →ₗ[𝕜] E) → E →ₗ[𝕜] E ⊗[𝕜] (E ⊗[𝕜] E))
        ((((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)) ∘ₗ
            LinearMap.rTensor E ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A))) ∘ₗ
          (↑(toLinearEquiv (LinearIsometryEquiv.symm (assocIsometry 𝕜 E E E))) :
            E ⊗[𝕜] (E ⊗[𝕜] E) →ₗ[𝕜] E ⊗[𝕜] E ⊗[𝕜] E)) :
      E →ₗ[𝕜] E ⊗[𝕜] (E ⊗[𝕜] E))
    ((adjoint : (a : E ⊗[𝕜] (E ⊗[𝕜] E) →ₗ[𝕜] E) → E →ₗ[𝕜] E ⊗[𝕜] (E ⊗[𝕜] E))
        (((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)) ∘ₗ
          LinearMap.lTensor E ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A))) :
      E →ₗ[𝕜] E ⊗[𝕜] (E ⊗[𝕜] E))
⊢ Eq.{u_2 + 1} (α := E →ₗ[𝕜] E ⊗[𝕜] (E ⊗[𝕜] E))
    ((adjoint : (a : E ⊗[𝕜] (E ⊗[𝕜] E) →ₗ[𝕜] E ⊗[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E ⊗[𝕜] E →ₗ[𝕜] E ⊗[𝕜] (E ⊗[𝕜] E))
        (↑(toLinearEquiv (LinearIsometryEquiv.symm (assocIsometry 𝕜 E E E))) :
          E ⊗[𝕜] (E ⊗[𝕜] E) →ₗ[𝕜] E ⊗[𝕜] E ⊗[𝕜] E) ∘ₗ
      (adjoint : (a : E ⊗[𝕜] E ⊗[𝕜] E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E ⊗[𝕜] E ⊗[𝕜] E)
          (LinearMap.rTensor E ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A))) ∘ₗ
        (adjoint : (a : E ⊗[𝕜] E →ₗ[𝕜] E) → E →ₗ[𝕜] E ⊗[𝕜] E)
          ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)))
    ((adjoint : (a : E ⊗[𝕜] (E ⊗[𝕜] E) →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E ⊗[𝕜] (E ⊗[𝕜] E))
        (LinearMap.lTensor E ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A))) ∘ₗ
      (adjoint : (a : E ⊗[𝕜] E →ₗ[𝕜] E) → E →ₗ[𝕜] E ⊗[𝕜] E)
        ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)))

Tactic:
simp_rw [← adjoint_comp]

Premises used: LinearMap.adjoint_comp
-- Module: Mathlib.Analysis.InnerProductSpace.Coalgebra
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
A : Type u_3
inst_4 : Ring A
inst_5 : Module 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
e : E ≃ₗ[𝕜] A
h :
  (((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)) ∘ₗ
        LinearMap.rTensor E ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A))) ∘ₗ
      (↑(toLinearEquiv (LinearIsometryEquiv.symm (assocIsometry 𝕜 E E E))) : E ⊗[𝕜] (E ⊗[𝕜] E) →ₗ[𝕜] E ⊗[𝕜] E ⊗[𝕜] E) =
    ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)) ∘ₗ
      LinearMap.lTensor E ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A))
⊢ Eq (α := E →ₗ[𝕜] E ⊗[𝕜] (E ⊗[𝕜] E))
    ((adjoint : (a : E ⊗[𝕜] (E ⊗[𝕜] E) →ₗ[𝕜] E) → E →ₗ[𝕜] E ⊗[𝕜] (E ⊗[𝕜] E))
        ((((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)) ∘ₗ
            LinearMap.rTensor E ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A))) ∘ₗ
          (↑(toLinearEquiv (LinearIsometryEquiv.symm (assocIsometry 𝕜 E E E))) :
            E ⊗[𝕜] (E ⊗[𝕜] E) →ₗ[𝕜] E ⊗[𝕜] E ⊗[𝕜] E)) :
      E →ₗ[𝕜] E ⊗[𝕜] (E ⊗[𝕜] E))
    ((adjoint : (a : E ⊗[𝕜] (E ⊗[𝕜] E) →ₗ[𝕜] E) → E →ₗ[𝕜] E ⊗[𝕜] (E ⊗[𝕜] E))
        (((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)) ∘ₗ
          LinearMap.lTensor E ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A))) :
      E →ₗ[𝕜] E ⊗[𝕜] (E ⊗[𝕜] E))

Tactic:
congr 1
-- Module: Mathlib.Analysis.InnerProductSpace.Coalgebra
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
A : Type u_3
inst_4 : Ring A
inst_5 : Module 𝕜 A
inst_6 : SMulCommClass 𝕜 A A
inst_7 : IsScalarTower 𝕜 A A
e : E ≃ₗ[𝕜] A
h :
  ∀ (x x_1 x_2 : E),
    Eq (α := E)
      (((((AlgebraTensorModule.curry
                      (((AlgebraTensorModule.curry
                              ((((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)) ∘ₗ
                                  LinearMap.rTensor E
                                    ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A))) ∘ₗ
                                (↑(toLinearEquiv (LinearIsometryEquiv.symm (assocIsometry 𝕜 E E E))) :
                                  E ⊗[𝕜] (E ⊗[𝕜] E) →ₗ[𝕜] E ⊗[𝕜] E ⊗[𝕜] E)) :
                            E →ₗ[𝕜] E ⊗[𝕜] E →ₗ[𝕜] E) :
                          (a : E) → E ⊗[𝕜] E →ₗ[𝕜] E)
                        x) :
                    E →ₗ[𝕜] E →ₗ[𝕜] E) :
                  (a : E) → E →ₗ[𝕜] E)
                x_1 :
              E →ₗ[𝕜] E) :
            (a : E) → E)
          x_2 :
        E)
      (((((AlgebraTensorModule.curry
                      (((AlgebraTensorModule.curry
                              (((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)) ∘ₗ
                                LinearMap.lTensor E
                                  ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A))) :
                            E →ₗ[𝕜] E ⊗[𝕜] E →ₗ[𝕜] E) :
                          (a : E) → E ⊗[𝕜] E →ₗ[𝕜] E)
                        x) :
                    E →ₗ[𝕜] E →ₗ[𝕜] E) :
                  (a : E) → E →ₗ[𝕜] E)
                x_1 :
              E →ₗ[𝕜] E) :
            (a : E) → E)
          x_2 :
        E)
⊢ (((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)) ∘ₗ
        LinearMap.rTensor E ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A))) ∘ₗ
      (↑(toLinearEquiv (LinearIsometryEquiv.symm (assocIsometry 𝕜 E E E))) : E ⊗[𝕜] (E ⊗[𝕜] E) →ₗ[𝕜] E ⊗[𝕜] E ⊗[𝕜] E) =
    ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)) ∘ₗ
      LinearMap.lTensor E ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A))

Tactic:
ext