awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
G : Type u_4
inst_10 : AddCommMonoid G
inst_11 : Module R G
inst_12 : StarAddMonoid G
inst_13 : StarModule R G
inst_14 : SMulCommClass R R F
x : R
x_1 : WithConv (E →ₗ[R] F)
h :
  ∀ (x_2 : E),
    Eq.{u_3 + 1} (α := F) (((star (x • x_1)).ofConv : (a : E) → F) x_2 : F)
      (((star x • star x_1).ofConv : (a : E) → F) x_2 : F)
⊢ star (x • x_1) = star x • star x_1

Tactic:
ext
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
G : Type u_4
inst_10 : AddCommMonoid G
inst_11 : Module R G
inst_12 : StarAddMonoid G
inst_13 : StarModule R G
inst_14 : SMulCommClass R R F
x : R
x_1 : WithConv (E →ₗ[R] F)
x_2 : E
⊢ Eq.{u_3 + 1} (α := F) (((star (x • x_1)).ofConv : (a : E) → F) x_2 : F)
    (((star x • star x_1).ofConv : (a : E) → F) x_2 : F)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_5
E : Type u_6
F : Type u_7
G : Type u_8
H : Type u_9
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid E
inst_3 : StarAddMonoid E
inst_4 : Module R E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : StarAddMonoid F
inst_8 : Module R F
inst_9 : StarModule R F
inst_10 : AddCommMonoid G
inst_11 : StarAddMonoid G
inst_12 : Module R G
inst_13 : StarModule R G
inst_14 : AddCommMonoid H
inst_15 : StarAddMonoid H
inst_16 : Module R H
inst_17 : StarModule R H
f : WithConv (E →ₗ[R] F)
g : WithConv (G →ₗ[R] H)
x : E
x_1 : G
⊢ Eq (α := TensorProduct R F H)
    (((star (toConv (TensorProduct.map f.ofConv g.ofConv))).ofConv : (a : TensorProduct R E G) → TensorProduct R F H)
        (x ⊗ₜ[R] x_1) :
      TensorProduct R F H)
    (((toConv (TensorProduct.map (star f).ofConv (star g).ofConv)).ofConv :
          (a : TensorProduct R E G) → TensorProduct R F H)
        (x ⊗ₜ[R] x_1) :
      TensorProduct R F H)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_5
E : Type u_6
F : Type u_7
G : Type u_8
H : Type u_9
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid E
inst_3 : StarAddMonoid E
inst_4 : Module R E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : StarAddMonoid F
inst_8 : Module R F
inst_9 : StarModule R F
inst_10 : AddCommMonoid G
inst_11 : StarAddMonoid G
inst_12 : Module R G
inst_13 : StarModule R G
inst_14 : AddCommMonoid H
inst_15 : StarAddMonoid H
inst_16 : Module R H
inst_17 : StarModule R H
f : WithConv (E →ₗ[R] F)
g : WithConv (G →ₗ[R] H)
x : TensorProduct R E G
⊢ Eq (α := TensorProduct R F H)
    (star ((TensorProduct.map f.ofConv g.ofConv : (a : TensorProduct R E G) → TensorProduct R F H) x) :
      TensorProduct R F H)
    ((TensorProduct.map (star f).ofConv (star g).ofConv : (a : TensorProduct R E G) → TensorProduct R F H) (star x) :
      TensorProduct R F H)

Tactic:
simpa using congr($(TensorProduct.intrinsicStar_map f g) (star x))
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_5
E : Type u_6
F : Type u_7
G : Type u_8
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid E
inst_3 : StarAddMonoid E
inst_4 : Module R E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : StarAddMonoid F
inst_8 : Module R F
inst_9 : StarModule R F
inst_10 : AddCommMonoid G
inst_11 : StarAddMonoid G
inst_12 : Module R G
inst_13 : StarModule R G
f : WithConv (F →ₗ[R] G)
h :
  ∀ (x : E) (x_1 : F),
    Eq (α := TensorProduct R E G)
      (((((TensorProduct.AlgebraTensorModule.curry (ofConv (star (toConv (lTensor E f.ofConv)))) :
                    E →ₗ[R] F →ₗ[R] TensorProduct R E G) :
                  (a : E) → F →ₗ[R] TensorProduct R E G)
                x :
              F →ₗ[R] TensorProduct R E G) :
            (a : F) → TensorProduct R E G)
          x_1 :
        TensorProduct R E G)
      (((((TensorProduct.AlgebraTensorModule.curry (ofConv (toConv (lTensor E (star f).ofConv))) :
                    E →ₗ[R] F →ₗ[R] TensorProduct R E G) :
                  (a : E) → F →ₗ[R] TensorProduct R E G)
                x :
              F →ₗ[R] TensorProduct R E G) :
            (a : F) → TensorProduct R E G)
          x_1 :
        TensorProduct R E G)
⊢ Eq (α := WithConv (TensorProduct R E F →ₗ[R] TensorProduct R E G)) (star (toConv (lTensor E f.ofConv)))
    (toConv (lTensor E (star f).ofConv))

Tactic:
ext
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_5
E : Type u_6
F : Type u_7
G : Type u_8
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid E
inst_3 : StarAddMonoid E
inst_4 : Module R E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : StarAddMonoid F
inst_8 : Module R F
inst_9 : StarModule R F
inst_10 : AddCommMonoid G
inst_11 : StarAddMonoid G
inst_12 : Module R G
inst_13 : StarModule R G
f : WithConv (F →ₗ[R] G)
x : E
x_1 : F
⊢ Eq (α := TensorProduct R E G)
    (((((TensorProduct.AlgebraTensorModule.curry (ofConv (star (toConv (lTensor E f.ofConv)))) :
                  E →ₗ[R] F →ₗ[R] TensorProduct R E G) :
                (a : E) → F →ₗ[R] TensorProduct R E G)
              x :
            F →ₗ[R] TensorProduct R E G) :
          (a : F) → TensorProduct R E G)
        x_1 :
      TensorProduct R E G)
    (((((TensorProduct.AlgebraTensorModule.curry (ofConv (toConv (lTensor E (star f).ofConv))) :
                  E →ₗ[R] F →ₗ[R] TensorProduct R E G) :
                (a : E) → F →ₗ[R] TensorProduct R E G)
              x :
            F →ₗ[R] TensorProduct R E G) :
          (a : F) → TensorProduct R E G)
        x_1 :
      TensorProduct R E G)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_5
E : Type u_6
F : Type u_7
G : Type u_8
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid E
inst_3 : StarAddMonoid E
inst_4 : Module R E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : StarAddMonoid F
inst_8 : Module R F
inst_9 : StarModule R F
inst_10 : AddCommMonoid G
inst_11 : StarAddMonoid G
inst_12 : Module R G
inst_13 : StarModule R G
f : WithConv (E →ₗ[R] F)
h :
  ∀ (x : E) (x_1 : G),
    Eq (α := TensorProduct R F G)
      (((((TensorProduct.AlgebraTensorModule.curry (ofConv (star (toConv (rTensor G f.ofConv)))) :
                    E →ₗ[R] G →ₗ[R] TensorProduct R F G) :
                  (a : E) → G →ₗ[R] TensorProduct R F G)
                x :
              G →ₗ[R] TensorProduct R F G) :
            (a : G) → TensorProduct R F G)
          x_1 :
        TensorProduct R F G)
      (((((TensorProduct.AlgebraTensorModule.curry (ofConv (toConv (rTensor G (star f).ofConv))) :
                    E →ₗ[R] G →ₗ[R] TensorProduct R F G) :
                  (a : E) → G →ₗ[R] TensorProduct R F G)
                x :
              G →ₗ[R] TensorProduct R F G) :
            (a : G) → TensorProduct R F G)
          x_1 :
        TensorProduct R F G)
⊢ Eq (α := WithConv (TensorProduct R E G →ₗ[R] TensorProduct R F G)) (star (toConv (rTensor G f.ofConv)))
    (toConv (rTensor G (star f).ofConv))

Tactic:
ext
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_5
E : Type u_6
F : Type u_7
G : Type u_8
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid E
inst_3 : StarAddMonoid E
inst_4 : Module R E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : StarAddMonoid F
inst_8 : Module R F
inst_9 : StarModule R F
inst_10 : AddCommMonoid G
inst_11 : StarAddMonoid G
inst_12 : Module R G
inst_13 : StarModule R G
f : WithConv (E →ₗ[R] F)
x : E
x_1 : G
⊢ Eq (α := TensorProduct R F G)
    (((((TensorProduct.AlgebraTensorModule.curry (ofConv (star (toConv (rTensor G f.ofConv)))) :
                  E →ₗ[R] G →ₗ[R] TensorProduct R F G) :
                (a : E) → G →ₗ[R] TensorProduct R F G)
              x :
            G →ₗ[R] TensorProduct R F G) :
          (a : G) → TensorProduct R F G)
        x_1 :
      TensorProduct R F G)
    (((((TensorProduct.AlgebraTensorModule.curry (ofConv (toConv (rTensor G (star f).ofConv))) :
                  E →ₗ[R] G →ₗ[R] TensorProduct R F G) :
                (a : E) → G →ₗ[R] TensorProduct R F G)
              x :
            G →ₗ[R] TensorProduct R F G) :
          (a : G) → TensorProduct R F G)
        x_1 :
      TensorProduct R F G)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_5
E : Type u_6
F : Type u_7
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid E
inst_3 : StarAddMonoid E
inst_4 : Module R E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : StarAddMonoid F
inst_8 : Module R F
inst_9 : StarModule R F
f : WithConv (E →ₗ[R] F)
⊢ star f = toConv ((↑(starLinearEquiv R) : F →ₗ⋆[R] F) ∘ₛₗ f.ofConv ∘ₛₗ (↑(starLinearEquiv R) : E →ₗ⋆[R] E))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_5
E : Type u_6
F : Type u_7
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid E
inst_3 : StarAddMonoid E
inst_4 : Module R E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : StarAddMonoid F
inst_8 : Module R F
inst_9 : StarModule R F
⊢ Eq (α := WithConv (E →ₗ[R] F) ≃ₗ⋆[R] WithConv (E →ₗ[R] F)) (starLinearEquiv R)
    (LinearEquiv.trans (re₂₃ := ⋯) (re₃₂ := ⋯) (WithConv.linearEquiv R (E →ₗ[R] F))
      (LinearEquiv.trans (LinearEquiv.arrowCongr (starLinearEquiv R) (starLinearEquiv R))
        (LinearEquiv.symm (WithConv.linearEquiv R (E →ₗ[R] F)))))

Tactic:
rfl

Premises used: LinearEquiv.trans, starLinearEquiv, rfl
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
E : Type u_2
inst : AddCommMonoid E
inst_1 : StarAddMonoid E
S : Type u_5
inst_2 : Semiring S
inst_3 : StarAddMonoid S
inst_4 : StarModule S S
inst_5 : Module S E
inst_6 : StarModule S E
a : E
h :
  Eq.{u_2 + 1} (α := E) ((ofConv (star (toConv (toSpanSingleton S E a))) : (a : S) → E) 1 : E)
    ((ofConv (toConv (toSpanSingleton S E (star a))) : (a : S) → E) 1 : E)
⊢ Eq (α := WithConv (S →ₗ[S] E)) (star (toConv (toSpanSingleton S E a))) (toConv (toSpanSingleton S E (star a)))

Tactic:
ext
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
E : Type u_2
inst : AddCommMonoid E
inst_1 : StarAddMonoid E
S : Type u_5
inst_2 : Semiring S
inst_3 : StarAddMonoid S
inst_4 : StarModule S S
inst_5 : Module S E
inst_6 : StarModule S E
a : E
⊢ Eq.{u_2 + 1} (α := E) ((ofConv (star (toConv (toSpanSingleton S E a))) : (a : S) → E) 1 : E)
    ((ofConv (toConv (toSpanSingleton S E (star a))) : (a : S) → E) 1 : E)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
E : Type u_2
F : Type u_3
inst : AddCommMonoid E
inst_1 : StarAddMonoid E
inst_2 : AddCommMonoid F
inst_3 : StarAddMonoid F
S : Type u_5
inst_4 : Semiring S
inst_5 : StarAddMonoid S
inst_6 : StarModule S S
inst_7 : Module S E
inst_8 : StarModule S E
inst_9 : Module S F
inst_10 : StarModule S F
f : WithConv (E →ₗ[S] S)
x : F
h :
  ∀ (x_1 : E),
    Eq.{u_3 + 1} (α := F) ((ofConv (star (toConv (f.ofConv.smulRight x))) : (a : E) → F) x_1 : F)
      ((ofConv (toConv ((star f).ofConv.smulRight (star x))) : (a : E) → F) x_1 : F)
⊢ Eq (α := WithConv (E →ₗ[S] F)) (star (toConv (f.ofConv.smulRight x))) (toConv ((star f).ofConv.smulRight (star x)))

Tactic:
ext
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
E : Type u_2
F : Type u_3
inst : AddCommMonoid E
inst_1 : StarAddMonoid E
inst_2 : AddCommMonoid F
inst_3 : StarAddMonoid F
S : Type u_5
inst_4 : Semiring S
inst_5 : StarAddMonoid S
inst_6 : StarModule S S
inst_7 : Module S E
inst_8 : StarModule S E
inst_9 : Module S F
inst_10 : StarModule S F
f : WithConv (E →ₗ[S] S)
x : F
x_1 : E
⊢ Eq.{u_3 + 1} (α := F) ((ofConv (star (toConv (f.ofConv.smulRight x))) : (a : E) → F) x_1 : F)
    ((ofConv (toConv ((star f).ofConv.smulRight (star x))) : (a : E) → F) x_1 : F)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_5
A : Type u_6
C : Type u_7
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : IsScalarTower R A A
inst_6 : StarRing A
inst_7 : StarModule R A
inst_8 : AddCommMonoid C
inst_9 : Module R C
inst_10 : StarAddMonoid C
inst_11 : StarModule R C
inst_12 : CoalgebraStruct R C
h :
  Eq (α := WithConv (C →ₗ[R] C ⊗[R] C)) (star (toConv comul))
    (toConv ((↑(TensorProduct.comm R C C) : C ⊗[R] C →ₗ[R] C ⊗[R] C) ∘ₗ comul))
f g : WithConv (C →ₗ[R] A)
simp_rw :
  toConv
      ((mul' R A ∘ₗ (↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A)) ∘ₗ
        ((↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A) ∘ₗ
            TensorProduct.map (star g).ofConv (star f).ofConv) ∘ₗ
          comul) =
    toConv (mul' R A ∘ₗ TensorProduct.map (star g).ofConv (star f).ofConv ∘ₗ comul)
⊢ star (f * g) = star g * star f

Tactic:
simp_rw [convMul_def, intrinsicStar_comp', intrinsicStar_mul', intrinsicStar_map,
    h, comp_assoc, ← comp_assoc _ _ (map _ _), map_comp_comm_eq,
    ← comp_assoc _ (TensorProduct.comm R A A).toLinearMap]

Premises used: LinearMap.convMul_def, TensorProduct.map_comp_comm_eq, TensorProduct.comm, LinearMap.comp_assoc, LinearMap.intrinsicStar_mul', LinearMap.intrinsicStar_comp', TensorProduct.intrinsicStar_map, TensorProduct.map, LinearEquiv.toLinearMap
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_5
A : Type u_6
C : Type u_7
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : IsScalarTower R A A
inst_6 : StarRing A
inst_7 : StarModule R A
inst_8 : AddCommMonoid C
inst_9 : Module R C
inst_10 : StarAddMonoid C
inst_11 : StarModule R C
inst_12 : CoalgebraStruct R C
h :
  Eq (α := WithConv (C →ₗ[R] C ⊗[R] C)) (star (toConv comul))
    (toConv ((↑(TensorProduct.comm R C C) : C ⊗[R] C →ₗ[R] C ⊗[R] C) ∘ₗ comul))
f g : WithConv (C →ₗ[R] A)
h₁ :
  ∀ (x : C),
    Eq.{u_6 + 1} (α := A)
      (((toConv
                ((mul' R A ∘ₗ (↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A)) ∘ₗ
                  ((↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A) ∘ₗ
                      TensorProduct.map (star g).ofConv (star f).ofConv) ∘ₗ
                    comul)).ofConv :
            (a : C) → A)
          x :
        A)
      (((toConv (mul' R A ∘ₗ TensorProduct.map (star g).ofConv (star f).ofConv ∘ₗ comul)).ofConv : (a : C) → A) x : A)
⊢ toConv
      ((mul' R A ∘ₗ (↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A)) ∘ₗ
        ((↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A) ∘ₗ
            TensorProduct.map (star g).ofConv (star f).ofConv) ∘ₗ
          comul) =
    toConv (mul' R A ∘ₗ TensorProduct.map (star g).ofConv (star f).ofConv ∘ₗ comul)

Tactic:
ext
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_5
A : Type u_6
C : Type u_7
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : SMulCommClass R A A
inst_5 : IsScalarTower R A A
inst_6 : StarRing A
inst_7 : StarModule R A
inst_8 : AddCommMonoid C
inst_9 : Module R C
inst_10 : StarAddMonoid C
inst_11 : StarModule R C
inst_12 : CoalgebraStruct R C
h :
  Eq (α := WithConv (C →ₗ[R] C ⊗[R] C)) (star (toConv comul))
    (toConv ((↑(TensorProduct.comm R C C) : C ⊗[R] C →ₗ[R] C ⊗[R] C) ∘ₗ comul))
f g : WithConv (C →ₗ[R] A)
x : C
⊢ Eq.{u_6 + 1} (α := A)
    (((toConv
              ((mul' R A ∘ₗ (↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A)) ∘ₗ
                ((↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A) ∘ₗ
                    TensorProduct.map (star g).ofConv (star f).ofConv) ∘ₗ
                  comul)).ofConv :
          (a : C) → A)
        x :
      A)
    (((toConv (mul' R A ∘ₗ TensorProduct.map (star g).ofConv (star f).ofConv ∘ₗ comul)).ofConv : (a : C) → A) x : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : StarRing R
n : Type u_8
inst_2 : DecidableEq n
B : n → Type u_9
inst_3 : (i : n) → AddCommMonoid (B i)
inst_4 : (i : n) → Module.{u_5, u_9} R (B i)
inst_5 : (i : n) → StarAddMonoid (B i)
inst_6 : ∀ (i : n), StarModule.{u_5, u_9} R (B i)
i : n
⊢ Eq (α := WithConv (B i →ₗ[R] (i : n) → B i)) (star (toConv (single R B i))) (toConv (single R B i))

Tactic:
aesop (add simp [Pi.single, Function.update])

Premises used: Function.update, Pi.single
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : StarRing R
n : Type u_8
inst_2 : DecidableEq n
B : n → Type u_9
inst_3 : (i : n) → AddCommMonoid (B i)
inst_4 : (i : n) → Module.{u_5, u_9} R (B i)
inst_5 : (i : n) → StarAddMonoid (B i)
inst_6 : ∀ (i : n), StarModule.{u_5, u_9} R (B i)
inst_7 : Fintype n
inst_8 : (i : n) → CoalgebraStruct.{u_5, u_9} R (B i)
h :
  ∀ (i : n),
    Eq.{u_9 + 1} (α := WithConv (B i →ₗ[R] B i ⊗[R] B i)) (star (toConv comul))
      (toConv ((↑(TensorProduct.comm R (B i) (B i)) : B i ⊗[R] B i →ₗ[R] B i ⊗[R] B i) ∘ₗ comul))
h₁ :
  ∀ (i : n) (x : B i),
    Eq (α := ((i : n) → B i) ⊗[R] ((i : n) → B i))
      ((ofConv (star (toConv comul)) ∘ₗ single R B i : (a : B i) → ((i : n) → B i) ⊗[R] ((i : n) → B i)) x :
        ((i : n) → B i) ⊗[R] ((i : n) → B i))
      ((ofConv
                (toConv
                  ((↑(TensorProduct.comm R ((i : n) → B i) ((i : n) → B i)) :
                      ((i : n) → B i) ⊗[R] ((i : n) → B i) →ₗ[R] ((i : n) → B i) ⊗[R] ((i : n) → B i)) ∘ₗ
                    comul)) ∘ₗ
              single R B i :
            (a : B i) → ((i : n) → B i) ⊗[R] ((i : n) → B i))
          x :
        ((i : n) → B i) ⊗[R] ((i : n) → B i))
⊢ Eq (α := WithConv (((i : n) → B i) →ₗ[R] ((i : n) → B i) ⊗[R] ((i : n) → B i))) (star (toConv comul))
    (toConv
      ((↑(TensorProduct.comm R ((i : n) → B i) ((i : n) → B i)) :
          ((i : n) → B i) ⊗[R] ((i : n) → B i) →ₗ[R] ((i : n) → B i) ⊗[R] ((i : n) → B i)) ∘ₗ
        comul))

Tactic:
ext i x
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : StarRing R
n : Type u_8
inst_2 : DecidableEq n
B : n → Type u_9
inst_3 : (i : n) → AddCommMonoid (B i)
inst_4 : (i : n) → Module.{u_5, u_9} R (B i)
inst_5 : (i : n) → StarAddMonoid (B i)
inst_6 : ∀ (i : n), StarModule.{u_5, u_9} R (B i)
inst_7 : Fintype n
inst_8 : (i : n) → CoalgebraStruct.{u_5, u_9} R (B i)
h :
  ∀ (i : n),
    Eq.{u_9 + 1} (α := WithConv (B i →ₗ[R] B i ⊗[R] B i)) (star (toConv comul))
      (toConv ((↑(TensorProduct.comm R (B i) (B i)) : B i ⊗[R] B i →ₗ[R] B i ⊗[R] B i) ∘ₗ comul))
i : n
x : B i
⊢ Eq (α := B i ⊗[R] B i) (star ((comul : (a : B i) → B i ⊗[R] B i) (star x)) : B i ⊗[R] B i)
    ((TensorProduct.comm R (B i) (B i) : (a : B i ⊗[R] B i) → B i ⊗[R] B i) ((comul : (a : B i) → B i ⊗[R] B i) x) :
      B i ⊗[R] B i)

Tactic:
simpa using congr($(h i) x)
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : StarRing R
n : Type u_8
inst_2 : DecidableEq n
B : n → Type u_9
inst_3 : (i : n) → AddCommMonoid (B i)
inst_4 : (i : n) → Module.{u_5, u_9} R (B i)
inst_5 : (i : n) → StarAddMonoid (B i)
inst_6 : ∀ (i : n), StarModule.{u_5, u_9} R (B i)
inst_7 : Fintype n
inst_8 : (i : n) → CoalgebraStruct.{u_5, u_9} R (B i)
h :
  ∀ (i : n),
    Eq.{u_9 + 1} (α := WithConv (B i →ₗ[R] B i ⊗[R] B i)) (star (toConv comul))
      (toConv ((↑(TensorProduct.comm R (B i) (B i)) : B i ⊗[R] B i →ₗ[R] B i ⊗[R] B i) ∘ₗ comul))
i : n
x : B i
⊢ Eq (α := B i ⊗[R] B i) (star ((comul : (a : B i) → B i ⊗[R] B i) (star x)) : B i ⊗[R] B i)
    ((TensorProduct.comm R (B i) (B i) : (a : B i ⊗[R] B i) → B i ⊗[R] B i) ((comul : (a : B i) → B i ⊗[R] B i) x) :
      B i ⊗[R] B i)

Tactic:
have := by simpa using congr($(h i) x)
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : StarRing R
n : Type u_8
inst_2 : DecidableEq n
B : n → Type u_9
inst_3 : (i : n) → AddCommMonoid (B i)
inst_4 : (i : n) → Module.{u_5, u_9} R (B i)
inst_5 : (i : n) → StarAddMonoid (B i)
inst_6 : ∀ (i : n), StarModule.{u_5, u_9} R (B i)
inst_7 : Fintype n
inst_8 : (i : n) → CoalgebraStruct.{u_5, u_9} R (B i)
h :
  ∀ (i : n),
    Eq.{u_9 + 1} (α := WithConv (B i →ₗ[R] B i ⊗[R] B i)) (star (toConv comul))
      (toConv ((↑(TensorProduct.comm R (B i) (B i)) : B i ⊗[R] B i →ₗ[R] B i ⊗[R] B i) ∘ₗ comul))
i : n
x : B i
this :
  Eq (α := B i ⊗[R] B i) (star ((comul : (a : B i) → B i ⊗[R] B i) (star x)) : B i ⊗[R] B i)
    ((TensorProduct.comm R (B i) (B i) : (a : B i ⊗[R] B i) → B i ⊗[R] B i) ((comul : (a : B i) → B i ⊗[R] B i) x) :
      B i ⊗[R] B i)
h₁ :
  Eq (α := ((i : n) → B i) ⊗[R] ((i : n) → B i))
    (star
        ((TensorProduct.map (single R B i) (single R B i) : (a : B i ⊗[R] B i) → ((i : n) → B i) ⊗[R] ((i : n) → B i))
          ((comul : (a : B i) → B i ⊗[R] B i) (star x))) :
      ((i : n) → B i) ⊗[R] ((i : n) → B i))
    ((TensorProduct.comm R ((i : n) → B i) ((i : n) → B i) :
          (a : ((i : n) → B i) ⊗[R] ((i : n) → B i)) → ((i : n) → B i) ⊗[R] ((i : n) → B i))
        ((TensorProduct.map (single R B i) (single R B i) : (a : B i ⊗[R] B i) → ((i : n) → B i) ⊗[R] ((i : n) → B i))
          ((comul : (a : B i) → B i ⊗[R] B i) x)) :
      ((i : n) → B i) ⊗[R] ((i : n) → B i))
⊢ Eq (α := ((i : n) → B i) ⊗[R] ((i : n) → B i))
    ((ofConv (star (toConv comul)) ∘ₗ single R B i : (a : B i) → ((i : n) → B i) ⊗[R] ((i : n) → B i)) x :
      ((i : n) → B i) ⊗[R] ((i : n) → B i))
    ((ofConv
              (toConv
                ((↑(TensorProduct.comm R ((i : n) → B i) ((i : n) → B i)) :
                    ((i : n) → B i) ⊗[R] ((i : n) → B i) →ₗ[R] ((i : n) → B i) ⊗[R] ((i : n) → B i)) ∘ₗ
                  comul)) ∘ₗ
            single R B i :
          (a : B i) → ((i : n) → B i) ⊗[R] ((i : n) → B i))
        x :
      ((i : n) → B i) ⊗[R] ((i : n) → B i))

Tactic:
simp only [coe_comp, coe_single, Function.comp_apply, intrinsicStar_apply, Pi.star_single,
    Pi.comul_single, LinearEquiv.coe_coe]

Premises used: Pi.star_single, LinearMap.coe_comp, LinearMap.coe_single, LinearMap.intrinsicStar_apply, Pi.comul_single, Function.comp_apply, LinearEquiv.coe_coe