awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
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
⊢ 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)))
have 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)))
Tactic: rw [← adjoint_lTensor, ← adjoint_rTensor, ← toLinearEquiv_assocIsometry,
      ← (assocIsometry 𝕜 _ _ _).symm_symm, ← adjoint_toLinearMap_eq_symm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
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
⊢ 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)))
have 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))
Tactic: simp_rw [← adjoint_comp]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
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
⊢ 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))
have 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))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
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
⊢ (((↑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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
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
⊢ 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)
have 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)
Tactic: rw [← adjoint_toSpanSingleton, ← adjoint_rTensor, ← adjoint_comp, ← toLinearMap_symm_lid,
      ← toLinearEquiv_lidIsometry, ← toLinearEquiv_symm, ← adjoint_toLinearMap_eq_symm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
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
⊢ 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)
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
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
⊢ ((↑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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
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
⊢ 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)
have 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 ⊗[𝕜] 𝕜)
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
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
⊢ 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 ⊗[𝕜] 𝕜)
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
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
⊢ ((↑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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
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 * z)
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
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
⊢ 1 * x = x
have 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
Tactic: dsimp [OfNat.ofNat]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
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
⊢ (((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
have rw : ((↑(toLinearEquiv (LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (lidIsometry 𝕜 E)))) : 𝕜 ⊗[𝕜] E →ₗ[𝕜] E) :
      (a : 𝕜 ⊗[𝕜] E) → E)
    (One.one ⊗ₜ[𝕜] x) =
  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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
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 * 1 = x
have 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
Tactic: dsimp [OfNat.ofNat]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
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
⊢ (((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
have rw : ((↑(toLinearEquiv
            (LinearIsometryEquiv.symm
              (LinearIsometryEquiv.symm (LinearIsometryEquiv.trans (commIsometry 𝕜 E 𝕜) (lidIsometry 𝕜 E))))) :
        E ⊗[𝕜] 𝕜 →ₗ[𝕜] E) :
      (a : E ⊗[𝕜] 𝕜) → E)
    (x ⊗ₜ[𝕜] One.one) =
  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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
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 : 𝕜
⊢ (((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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
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 : 𝕜
⊢ 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)
have simp : (((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) (x * y) =
  HSMul.hSMul (β := E) x ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) y : E)
Tactic: simp only [LinearIsometryEquiv.symm_symm, toLinearEquiv_lidIsometry, adjoint_lTensor,
          coe_comp, LinearEquiv.coe_coe, Function.comp_apply, lTensor_tmul, lid_tmul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
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 : 𝕜
⊢ (((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) (x * y) =
    HSMul.hSMul (β := E) x ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) y : E)
have rw : (((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) (x • y) =
  HSMul.hSMul (β := E) x ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) y : E)
Tactic: rw [← smul_eq_mul, ← _root_.map_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Coalgebra (goal)
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 : 𝕜
rw :
  (((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) (x • y) =
    HSMul.hSMul (β := E) x ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) y : E)
⊢ (((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) (x * y) =
    HSMul.hSMul (β := E) x ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) y : E)
have rw₁ : Eq.{u_2 + 1} (α := E) ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) (x • y) : E)
  ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) (x • y) : E)
Tactic: rw [← smul_eq_mul, ← _root_.map_smul]