awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- 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 (α := E →ₗ[𝕜] 𝕜 ⊗[𝕜] E)
    ((adjoint : (a : 𝕜 ⊗[𝕜] E →ₗ[𝕜] E) → E →ₗ[𝕜] 𝕜 ⊗[𝕜] E)
        (((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)) ∘ₗ
          LinearMap.rTensor E (toSpanSingleton 𝕜 E ((e.symm : (a : A) → E) 1))) :
      E →ₗ[𝕜] 𝕜 ⊗[𝕜] E)
    ((adjoint : (a : 𝕜 ⊗[𝕜] E →ₗ[𝕜] E) → E →ₗ[𝕜] 𝕜 ⊗[𝕜] E) (↑(toLinearEquiv (lidIsometry 𝕜 E)) : 𝕜 ⊗[𝕜] E →ₗ[𝕜] E) :
      E →ₗ[𝕜] 𝕜 ⊗[𝕜] E)
⊢ Eq (α := E →ₗ[𝕜] 𝕜 ⊗[𝕜] E)
    (LinearMap.rTensor E ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) ((e.symm : (a : A) → E) 1)) ∘ₗ
      (adjoint : (a : E ⊗[𝕜] E →ₗ[𝕜] E) → E →ₗ[𝕜] E ⊗[𝕜] E)
        ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)))
    ((TensorProduct.mk 𝕜 𝕜 E : (a : 𝕜) → E →ₗ[𝕜] 𝕜 ⊗[𝕜] E) 1)

Tactic:
rw [← adjoint_toSpanSingleton, ← adjoint_rTensor, ← adjoint_comp, ← toLinearMap_symm_lid,
      ← toLinearEquiv_lidIsometry, ← toLinearEquiv_symm, ← adjoint_toLinearMap_eq_symm]

Premises used: TensorProduct.toLinearEquiv_lidIsometry, LinearIsometryEquiv.toLinearEquiv_symm, LinearIsometryEquiv.adjoint_toLinearMap_eq_symm, LinearMap.adjoint_rTensor, LinearMap.adjoint_toSpanSingleton, LinearMap.adjoint_comp, TensorProduct.toLinearMap_symm_lid
-- 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 (toSpanSingleton 𝕜 E ((e.symm : (a : A) → E) 1)) =
    (↑(toLinearEquiv (lidIsometry 𝕜 E)) : 𝕜 ⊗[𝕜] E →ₗ[𝕜] E)
⊢ Eq (α := E →ₗ[𝕜] 𝕜 ⊗[𝕜] E)
    ((adjoint : (a : 𝕜 ⊗[𝕜] E →ₗ[𝕜] E) → E →ₗ[𝕜] 𝕜 ⊗[𝕜] E)
        (((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)) ∘ₗ
          LinearMap.rTensor E (toSpanSingleton 𝕜 E ((e.symm : (a : A) → E) 1))) :
      E →ₗ[𝕜] 𝕜 ⊗[𝕜] E)
    ((adjoint : (a : 𝕜 ⊗[𝕜] E →ₗ[𝕜] E) → E →ₗ[𝕜] 𝕜 ⊗[𝕜] E) (↑(toLinearEquiv (lidIsometry 𝕜 E)) : 𝕜 ⊗[𝕜] 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 : E),
    Eq (α := E)
      ((((AlgebraTensorModule.curry
                    (((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)) ∘ₗ
                      LinearMap.rTensor E (toSpanSingleton 𝕜 E ((e.symm : (a : A) → E) 1))) :
                  LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id 𝕜) 𝕜 (E →ₗ[𝕜] E)) :
                (a : 𝕜) → E →ₗ[𝕜] E)
              1 :
            (a : E) → E)
          x :
        E)
      ((((AlgebraTensorModule.curry (↑(toLinearEquiv (lidIsometry 𝕜 E)) : 𝕜 ⊗[𝕜] E →ₗ[𝕜] E) :
                  LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id 𝕜) 𝕜 (E →ₗ[𝕜] E)) :
                (a : 𝕜) → E →ₗ[𝕜] E)
              1 :
            (a : E) → E)
          x :
        E)
⊢ ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)) ∘ₗ
      LinearMap.rTensor E (toSpanSingleton 𝕜 E ((e.symm : (a : A) → E) 1)) =
    (↑(toLinearEquiv (lidIsometry 𝕜 E)) : 𝕜 ⊗[𝕜] E →ₗ[𝕜] E)

Tactic:
ext
-- 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
x : E
⊢ Eq (α := E)
    ((((AlgebraTensorModule.curry
                  (((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)) ∘ₗ
                    LinearMap.rTensor E (toSpanSingleton 𝕜 E ((e.symm : (a : A) → E) 1))) :
                LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id 𝕜) 𝕜 (E →ₗ[𝕜] E)) :
              (a : 𝕜) → E →ₗ[𝕜] E)
            1 :
          (a : E) → E)
        x :
      E)
    ((((AlgebraTensorModule.curry (↑(toLinearEquiv (lidIsometry 𝕜 E)) : 𝕜 ⊗[𝕜] E →ₗ[𝕜] E) :
                LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id 𝕜) 𝕜 (E →ₗ[𝕜] E)) :
              (a : 𝕜) → E →ₗ[𝕜] E)
            1 :
          (a : E) → E)
        x :
      E)

Tactic:
simp
-- 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 (α := E →ₗ[𝕜] E ⊗[𝕜] 𝕜)
    ((adjoint : (a : E ⊗[𝕜] 𝕜 →ₗ[𝕜] E) → E →ₗ[𝕜] E ⊗[𝕜] 𝕜)
        (((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)) ∘ₗ
          LinearMap.lTensor E (toSpanSingleton 𝕜 E ((e.symm : (a : A) → E) 1))) :
      E →ₗ[𝕜] E ⊗[𝕜] 𝕜)
    ((adjoint : (a : E ⊗[𝕜] 𝕜 →ₗ[𝕜] E) → E →ₗ[𝕜] E ⊗[𝕜] 𝕜)
        (↑(toLinearEquiv (LinearIsometryEquiv.trans (commIsometry 𝕜 E 𝕜) (lidIsometry 𝕜 E))) : E ⊗[𝕜] 𝕜 →ₗ[𝕜] E) :
      E →ₗ[𝕜] E ⊗[𝕜] 𝕜)
⊢ Eq (α := E →ₗ[𝕜] E ⊗[𝕜] 𝕜)
    (LinearMap.lTensor E ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) ((e.symm : (a : A) → E) 1)) ∘ₗ
      (adjoint : (a : E ⊗[𝕜] E →ₗ[𝕜] E) → E →ₗ[𝕜] E ⊗[𝕜] E)
        ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)))
    ((LinearMap.flip (TensorProduct.mk 𝕜 E 𝕜) : (a : 𝕜) → E →ₗ[𝕜] E ⊗[𝕜] 𝕜) 1)

Tactic:
rw [← adjoint_toSpanSingleton, ← adjoint_lTensor, ← adjoint_comp, ← toLinearMap_symm_rid,
      ← comm_trans_lid, ← toLinearEquiv_commIsometry, ← toLinearEquiv_lidIsometry,
      ← toLinearEquiv_trans, ← toLinearEquiv_symm, ← adjoint_toLinearMap_eq_symm]

Premises used: TensorProduct.toLinearEquiv_lidIsometry, LinearIsometryEquiv.toLinearEquiv_symm, LinearIsometryEquiv.adjoint_toLinearMap_eq_symm, TensorProduct.comm_trans_lid, TensorProduct.toLinearEquiv_commIsometry, LinearMap.adjoint_toSpanSingleton, LinearMap.adjoint_lTensor, LinearMap.adjoint_comp, TensorProduct.toLinearMap_symm_rid, LinearIsometryEquiv.toLinearEquiv_trans
-- 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.lTensor E (toSpanSingleton 𝕜 E ((e.symm : (a : A) → E) 1)) =
    (↑(toLinearEquiv (LinearIsometryEquiv.trans (commIsometry 𝕜 E 𝕜) (lidIsometry 𝕜 E))) : E ⊗[𝕜] 𝕜 →ₗ[𝕜] E)
⊢ Eq (α := E →ₗ[𝕜] E ⊗[𝕜] 𝕜)
    ((adjoint : (a : E ⊗[𝕜] 𝕜 →ₗ[𝕜] E) → E →ₗ[𝕜] E ⊗[𝕜] 𝕜)
        (((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)) ∘ₗ
          LinearMap.lTensor E (toSpanSingleton 𝕜 E ((e.symm : (a : A) → E) 1))) :
      E →ₗ[𝕜] E ⊗[𝕜] 𝕜)
    ((adjoint : (a : E ⊗[𝕜] 𝕜 →ₗ[𝕜] E) → E →ₗ[𝕜] E ⊗[𝕜] 𝕜)
        (↑(toLinearEquiv (LinearIsometryEquiv.trans (commIsometry 𝕜 E 𝕜) (lidIsometry 𝕜 E))) : 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 : E),
    Eq.{u_2 + 1} (α := E)
      (((((AlgebraTensorModule.curry
                      (((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)) ∘ₗ
                        LinearMap.lTensor E (toSpanSingleton 𝕜 E ((e.symm : (a : A) → E) 1))) :
                    E →ₗ[𝕜] 𝕜 →ₗ[𝕜] E) :
                  (a : E) → 𝕜 →ₗ[𝕜] E)
                x :
              𝕜 →ₗ[𝕜] E) :
            (a : 𝕜) → E)
          1 :
        E)
      (((((AlgebraTensorModule.curry
                      (↑(toLinearEquiv (LinearIsometryEquiv.trans (commIsometry 𝕜 E 𝕜) (lidIsometry 𝕜 E))) :
                        E ⊗[𝕜] 𝕜 →ₗ[𝕜] E) :
                    E →ₗ[𝕜] 𝕜 →ₗ[𝕜] E) :
                  (a : E) → 𝕜 →ₗ[𝕜] E)
                x :
              𝕜 →ₗ[𝕜] E) :
            (a : 𝕜) → E)
          1 :
        E)
⊢ ((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)) ∘ₗ
      LinearMap.lTensor E (toSpanSingleton 𝕜 E ((e.symm : (a : A) → E) 1)) =
    (↑(toLinearEquiv (LinearIsometryEquiv.trans (commIsometry 𝕜 E 𝕜) (lidIsometry 𝕜 E))) : E ⊗[𝕜] 𝕜 →ₗ[𝕜] E)

Tactic:
ext
-- 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
x : E
⊢ Eq.{u_2 + 1} (α := E)
    (((((AlgebraTensorModule.curry
                    (((↑e.symm : A →ₗ[𝕜] E) ∘ₗ mul' 𝕜 A ∘ₗ map (↑e : E →ₗ[𝕜] A) (↑e : E →ₗ[𝕜] A)) ∘ₗ
                      LinearMap.lTensor E (toSpanSingleton 𝕜 E ((e.symm : (a : A) → E) 1))) :
                  E →ₗ[𝕜] 𝕜 →ₗ[𝕜] E) :
                (a : E) → 𝕜 →ₗ[𝕜] E)
              x :
            𝕜 →ₗ[𝕜] E) :
          (a : 𝕜) → E)
        1 :
      E)
    (((((AlgebraTensorModule.curry
                    (↑(toLinearEquiv (LinearIsometryEquiv.trans (commIsometry 𝕜 E 𝕜) (lidIsometry 𝕜 E))) :
                      E ⊗[𝕜] 𝕜 →ₗ[𝕜] E) :
                  E →ₗ[𝕜] 𝕜 →ₗ[𝕜] E) :
                (a : E) → 𝕜 →ₗ[𝕜] E)
              x :
            𝕜 →ₗ[𝕜] E) :
          (a : 𝕜) → E)
        1 :
      E)

Tactic:
simp
-- 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
inst_4 : Coalgebra 𝕜 E
x y : E
⊢ x * y =
    (((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E) (x ⊗ₜ[𝕜] y)

Tactic:
rfl

Premises used: rfl
-- 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
inst_4 : Coalgebra 𝕜 E
x y z : E
simp_rw :
  Eq (α := E)
    ((((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E)
        ((LinearMap.lTensor E ((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul) :
              (a : E ⊗[𝕜] (E ⊗[𝕜] E)) → E ⊗[𝕜] E)
            (((↑(toLinearEquiv (LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (assocIsometry 𝕜 E E E)))) :
                  E ⊗[𝕜] E ⊗[𝕜] E →ₗ[𝕜] E ⊗[𝕜] (E ⊗[𝕜] E)) :
                (a : E ⊗[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] (E ⊗[𝕜] E))
              (x ⊗ₜ[𝕜] y ⊗ₜ[𝕜] z)) :
          E ⊗[𝕜] E) :
      E)
    ((((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E)
        (x ⊗ₜ[𝕜]
            (((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E)
              (y ⊗ₜ[𝕜] z) :
          E ⊗[𝕜] E) :
      E)
⊢ x * y * z = x * (y * z)

Tactic:
simp_rw [AlgebraOfCoalgebra.mul_def, ← rTensor_tmul, ← comp_apply, ← adjoint_rTensor,
      ← adjoint_comp, ← coassoc_symm, adjoint_comp, adjoint_lTensor, comp_apply,
      ← toLinearEquiv_assocIsometry, ← toLinearEquiv_symm, adjoint_toLinearMap_eq_symm]

Premises used: LinearMap.rTensor_tmul, LinearIsometryEquiv.toLinearEquiv_symm, LinearIsometryEquiv.adjoint_toLinearMap_eq_symm, LinearMap.adjoint_rTensor, LinearMap.comp_apply, InnerProductSpace.AlgebraOfCoalgebra.mul_def, LinearMap.adjoint_lTensor, TensorProduct.toLinearEquiv_assocIsometry, LinearMap.adjoint_comp, Coalgebra.coassoc_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
inst_4 : Coalgebra 𝕜 E
x y z : E
⊢ Eq (α := E)
    ((((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E)
        ((LinearMap.lTensor E ((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul) :
              (a : E ⊗[𝕜] (E ⊗[𝕜] E)) → E ⊗[𝕜] E)
            (((↑(toLinearEquiv (LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (assocIsometry 𝕜 E E E)))) :
                  E ⊗[𝕜] E ⊗[𝕜] E →ₗ[𝕜] E ⊗[𝕜] (E ⊗[𝕜] E)) :
                (a : E ⊗[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] (E ⊗[𝕜] E))
              (x ⊗ₜ[𝕜] y ⊗ₜ[𝕜] z)) :
          E ⊗[𝕜] E) :
      E)
    ((((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E)
        (x ⊗ₜ[𝕜]
            (((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E)
              (y ⊗ₜ[𝕜] z) :
          E ⊗[𝕜] E) :
      E)

Tactic:
simp only [symm_symm, toLinearEquiv_assocIsometry, LinearEquiv.coe_coe, assoc_tmul,
      lTensor_tmul]

Premises used: TensorProduct.assoc_tmul, TensorProduct.toLinearEquiv_assocIsometry, LinearIsometryEquiv.symm_symm, LinearEquiv.coe_coe, LinearMap.lTensor_tmul
-- 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
inst_4 : Coalgebra 𝕜 E
x : E
dsimp :
  (((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E)
      ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) One.one ⊗ₜ[𝕜] x : E ⊗[𝕜] E) =
    x
⊢ 1 * x = x

Tactic:
dsimp [OfNat.ofNat]

Premises used: OfNat.ofNat
-- 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
inst_4 : Coalgebra 𝕜 E
x : E
rw :
  ((↑(toLinearEquiv (LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (lidIsometry 𝕜 E)))) : 𝕜 ⊗[𝕜] E →ₗ[𝕜] E) :
        (a : 𝕜 ⊗[𝕜] E) → E)
      (One.one ⊗ₜ[𝕜] x) =
    x
⊢ (((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E)
      ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) One.one ⊗ₜ[𝕜] x : E ⊗[𝕜] E) =
    x

Tactic:
rw [← rTensor_tmul, ← comp_apply, ← adjoint_rTensor, ← adjoint_comp, rTensor_counit_comp_comul,
      ← toLinearMap_symm_lid, ← toLinearEquiv_lidIsometry, ← toLinearEquiv_symm,
      adjoint_toLinearMap_eq_symm]

Premises used: TensorProduct.toLinearEquiv_lidIsometry, LinearMap.rTensor_tmul, LinearIsometryEquiv.toLinearEquiv_symm, LinearIsometryEquiv.adjoint_toLinearMap_eq_symm, LinearMap.adjoint_rTensor, LinearMap.comp_apply, Coalgebra.rTensor_counit_comp_comul, LinearMap.adjoint_comp, TensorProduct.toLinearMap_symm_lid
-- 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
inst_4 : Coalgebra 𝕜 E
x : E
⊢ ((↑(toLinearEquiv (LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (lidIsometry 𝕜 E)))) : 𝕜 ⊗[𝕜] E →ₗ[𝕜] E) :
        (a : 𝕜 ⊗[𝕜] E) → E)
      (One.one ⊗ₜ[𝕜] x) =
    x

Tactic:
one_smul _ _

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, one_smul, FreeAddMonoid.sumAux
-- 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
inst_4 : Coalgebra 𝕜 E
x : E
⊢ ((↑(toLinearEquiv (LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (lidIsometry 𝕜 E)))) : 𝕜 ⊗[𝕜] E →ₗ[𝕜] E) :
        (a : 𝕜 ⊗[𝕜] E) → E)
      (One.one ⊗ₜ[𝕜] x) =
    x

Tactic:
exact one_smul _ _

Premises used: one_smul
-- 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
inst_4 : Coalgebra 𝕜 E
x : E
dsimp :
  (((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E)
      (x ⊗ₜ[𝕜] (((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) One.one : E ⊗[𝕜] E) =
    x
⊢ x * 1 = x

Tactic:
dsimp [OfNat.ofNat]

Premises used: OfNat.ofNat
-- 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
inst_4 : Coalgebra 𝕜 E
x : E
rw :
  ((↑(toLinearEquiv
              (LinearIsometryEquiv.symm
                (LinearIsometryEquiv.symm (LinearIsometryEquiv.trans (commIsometry 𝕜 E 𝕜) (lidIsometry 𝕜 E))))) :
          E ⊗[𝕜] 𝕜 →ₗ[𝕜] E) :
        (a : E ⊗[𝕜] 𝕜) → E)
      (x ⊗ₜ[𝕜] One.one) =
    x
⊢ (((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E)
      (x ⊗ₜ[𝕜] (((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) One.one : E ⊗[𝕜] E) =
    x

Tactic:
rw [← lTensor_tmul, ← comp_apply, ← adjoint_lTensor, ← adjoint_comp, lTensor_counit_comp_comul,
      ← toLinearMap_symm_rid, ← comm_trans_lid, ← toLinearEquiv_commIsometry,
      ← toLinearEquiv_lidIsometry, ← toLinearEquiv_trans, ← toLinearEquiv_symm,
      adjoint_toLinearMap_eq_symm]

Premises used: TensorProduct.toLinearEquiv_lidIsometry, LinearIsometryEquiv.toLinearEquiv_symm, LinearIsometryEquiv.adjoint_toLinearMap_eq_symm, TensorProduct.comm_trans_lid, LinearMap.comp_apply, TensorProduct.toLinearEquiv_commIsometry, LinearMap.adjoint_lTensor, LinearMap.adjoint_comp, Coalgebra.lTensor_counit_comp_comul, TensorProduct.toLinearMap_symm_rid, LinearMap.lTensor_tmul, LinearIsometryEquiv.toLinearEquiv_trans
-- 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
inst_4 : Coalgebra 𝕜 E
x : E
⊢ ((↑(toLinearEquiv
              (LinearIsometryEquiv.symm
                (LinearIsometryEquiv.symm (LinearIsometryEquiv.trans (commIsometry 𝕜 E 𝕜) (lidIsometry 𝕜 E))))) :
          E ⊗[𝕜] 𝕜 →ₗ[𝕜] E) :
        (a : E ⊗[𝕜] 𝕜) → E)
      (x ⊗ₜ[𝕜] One.one) =
    x

Tactic:
one_smul _ _

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, one_smul, FreeAddMonoid.sumAux
-- 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
inst_4 : Coalgebra 𝕜 E
x : E
⊢ ((↑(toLinearEquiv
              (LinearIsometryEquiv.symm
                (LinearIsometryEquiv.symm (LinearIsometryEquiv.trans (commIsometry 𝕜 E 𝕜) (lidIsometry 𝕜 E))))) :
          E ⊗[𝕜] 𝕜 →ₗ[𝕜] E) :
        (a : E ⊗[𝕜] 𝕜) → E)
      (x ⊗ₜ[𝕜] One.one) =
    x

Tactic:
exact one_smul _ _

Premises used: one_smul
-- 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
inst_4 : Coalgebra 𝕜 E
x : E
⊢ 0 * x = 0

Tactic:
simp
-- 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
inst_4 : Coalgebra 𝕜 E
x : E
⊢ x * 0 = 0

Tactic:
simp
-- 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
inst_4 : Coalgebra 𝕜 E
x y z : E
⊢ x * (y + z) = x * y + x * z

Tactic:
simp [tmul_add]

Premises used: TensorProduct.tmul_add
-- 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
inst_4 : Coalgebra 𝕜 E
x y z : E
⊢ (x + y) * z = x * z + y * z

Tactic:
simp [add_tmul]

Premises used: TensorProduct.add_tmul
-- 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
inst_4 : Coalgebra 𝕜 E
x y : 𝕜
simp_rw :
  Eq.{u_2 + 1} (α := E) ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) (x * y) : E)
    (((↑(toLinearEquiv (LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (lidIsometry 𝕜 E)))) : 𝕜 ⊗[𝕜] E →ₗ[𝕜] E) ∘ₗ
            (adjoint : (a : 𝕜 ⊗[𝕜] E →ₗ[𝕜] 𝕜 ⊗[𝕜] 𝕜) → 𝕜 ⊗[𝕜] 𝕜 →ₗ[𝕜] 𝕜 ⊗[𝕜] E) (LinearMap.lTensor 𝕜 counit) :
          (a : 𝕜 ⊗[𝕜] 𝕜) → E)
        (x ⊗ₜ[𝕜] y) :
      E)
⊢ (((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) (x * y) =
    HMul.hMul (α := E) (β := E) ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) x : E)
      ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) y : E)

Tactic:
simp_rw [AlgebraOfCoalgebra.mul_def, ← map_tmul, ← adjoint_map, ← comp_apply,
          ← adjoint_comp, ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul,
          adjoint_comp, ← toLinearMap_symm_lid, ← toLinearEquiv_lidIsometry, ← toLinearEquiv_symm,
          adjoint_toLinearMap_eq_symm]

Premises used: TensorProduct.toLinearEquiv_lidIsometry, TensorProduct.adjoint_map, LinearIsometryEquiv.toLinearEquiv_symm, LinearIsometryEquiv.adjoint_toLinearMap_eq_symm, LinearMap.comp_assoc, LinearMap.comp_apply, InnerProductSpace.AlgebraOfCoalgebra.mul_def, Coalgebra.rTensor_counit_comp_comul, LinearMap.lTensor_comp_rTensor, TensorProduct.map_tmul, LinearMap.adjoint_comp, TensorProduct.toLinearMap_symm_lid