awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra R A
inst_5 : Bialgebra R B
x : B
⊢ Eq.{u_1 + 1} (α := R)
    ((AlgHom.comp (B := A ⊗[R] B)
            (AlgHom.restrictScalars R
              (AlgHom.comp (B := B ⊗[R] A) (counitAlgHom R (B ⊗[R] A))
                (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)))
            Algebra.TensorProduct.includeRight :
          (a : B) → R)
        x :
      R)
    ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.restrictScalars R (counitAlgHom R (A ⊗[R] B) : A ⊗[R] B →ₐ[R] R))
            Algebra.TensorProduct.includeRight :
          (a : B) → R)
        x :
      R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra R A
inst_5 : Bialgebra R B
ha :
  ∀ (a : A),
    Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
      (((AlgHom.comp (B := A ⊗[R] B)
                (AlgHom.comp (B := A ⊗[R] B ⊗[R] (A ⊗[R] B))
                  (Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
                      (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
                    A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A))
                  (comulAlgHom R (A ⊗[R] B) : A ⊗[R] B →ₐ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)))
                Algebra.TensorProduct.includeLeft :
              A →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
            (a : A) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
          a :
        B ⊗[R] A ⊗[R] (B ⊗[R] A))
      ((AlgHom.comp (B := A ⊗[R] B)
              (AlgHom.comp (comulAlgHom R (B ⊗[R] A)) (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A))
              Algebra.TensorProduct.includeLeft :
            (a : A) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
          a :
        B ⊗[R] A ⊗[R] (B ⊗[R] A))
hb :
  ∀ (a : B),
    Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
      ((AlgHom.comp (B := A ⊗[R] B)
              (AlgHom.restrictScalars R
                (AlgHom.comp (B := A ⊗[R] B ⊗[R] (A ⊗[R] B))
                    (Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
                        (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
                      A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A))
                    (comulAlgHom R (A ⊗[R] B) : A ⊗[R] B →ₐ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
                  A ⊗[R] B →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)))
              Algebra.TensorProduct.includeRight :
            (a : B) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
          a :
        B ⊗[R] A ⊗[R] (B ⊗[R] A))
      ((AlgHom.comp (B := A ⊗[R] B)
              (AlgHom.restrictScalars R
                (AlgHom.comp (comulAlgHom R (B ⊗[R] A))
                  (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)))
              Algebra.TensorProduct.includeRight :
            (a : B) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
          a :
        B ⊗[R] A ⊗[R] (B ⊗[R] A))
⊢ Eq (α := A ⊗[R] B →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (AlgHom.comp (B := A ⊗[R] B ⊗[R] (A ⊗[R] B))
        (Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
            (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
          A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A))
        (comulAlgHom R (A ⊗[R] B) : A ⊗[R] B →ₐ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
      A ⊗[R] B →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (AlgHom.comp (comulAlgHom R (B ⊗[R] A)) (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
      A ⊗[R] B →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A))

Tactic:
ext a
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra R A
inst_5 : Bialgebra R B
a : A
ha :
  Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
              (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
            A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : A ⊗[R] B ⊗[R] (A ⊗[R] B)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B :
              TensorProduct.{u_1, u_3, u_4} R (A ⊗[R] A) (B ⊗[R] B) ≃ₗ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
            (a : A ⊗[R] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[R] (A ⊗[R] B))
          ((comul : (a : A) → A ⊗[R] A) a ⊗ₜ[R] (comul : (a : B) → B ⊗[R] B) 1)) :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A :
            TensorProduct.{u_1, u_4, u_3} R (B ⊗[R] B) (A ⊗[R] A) ≃ₗ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : B ⊗[R] B ⊗[R] (A ⊗[R] A)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        ((comul : (a : B) → B ⊗[R] B) 1 ⊗ₜ[R] (comul : (a : A) → A ⊗[R] A) a) :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
⊢ Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((AlgHom.comp (B := A ⊗[R] B)
              (AlgHom.comp (B := A ⊗[R] B ⊗[R] (A ⊗[R] B))
                (Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
                    (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
                  A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A))
                (comulAlgHom R (A ⊗[R] B) : A ⊗[R] B →ₐ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)))
              Algebra.TensorProduct.includeLeft :
            A →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : A) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        a :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
    ((AlgHom.comp (B := A ⊗[R] B)
            (AlgHom.comp (comulAlgHom R (B ⊗[R] A)) (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A))
            Algebra.TensorProduct.includeLeft :
          (a : A) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        a :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra R A
inst_5 : Bialgebra R B
a : A
ha :
  Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
              (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
            A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : A ⊗[R] B ⊗[R] (A ⊗[R] B)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B :
              TensorProduct.{u_1, u_3, u_4} R (A ⊗[R] A) (B ⊗[R] B) ≃ₗ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
            (a : A ⊗[R] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[R] (A ⊗[R] B))
          ((∑ i ∈ Repr.index (ℛ R a), Repr.left (ℛ R a) i ⊗ₜ[R] Repr.right (ℛ R a) i) ⊗ₜ[R]
            (comul : (a : B) → B ⊗[R] B) 1)) :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A :
            TensorProduct.{u_1, u_4, u_3} R (B ⊗[R] B) (A ⊗[R] A) ≃ₗ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : B ⊗[R] B ⊗[R] (A ⊗[R] A)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        ((comul : (a : B) → B ⊗[R] B) 1 ⊗ₜ[R]
          ∑ i ∈ Repr.index (ℛ R a), Repr.left (ℛ R a) i ⊗ₜ[R] Repr.right (ℛ R a) i) :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
⊢ Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
              (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
            A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : A ⊗[R] B ⊗[R] (A ⊗[R] B)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B :
              TensorProduct.{u_1, u_3, u_4} R (A ⊗[R] A) (B ⊗[R] B) ≃ₗ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
            (a : A ⊗[R] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[R] (A ⊗[R] B))
          ((comul : (a : A) → A ⊗[R] A) a ⊗ₜ[R] (comul : (a : B) → B ⊗[R] B) 1)) :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A :
            TensorProduct.{u_1, u_4, u_3} R (B ⊗[R] B) (A ⊗[R] A) ≃ₗ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : B ⊗[R] B ⊗[R] (A ⊗[R] A)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        ((comul : (a : B) → B ⊗[R] B) 1 ⊗ₜ[R] (comul : (a : A) → A ⊗[R] A) a) :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))

Tactic:
rw [← (ℛ R a).eq]

Premises used: Coalgebra.Repr.eq, Coalgebra.Repr.arbitrary
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra R A
inst_5 : Bialgebra R B
a : A
⊢ Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
              (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
            A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : A ⊗[R] B ⊗[R] (A ⊗[R] B)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B :
              TensorProduct.{u_1, u_3, u_4} R (A ⊗[R] A) (B ⊗[R] B) ≃ₗ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
            (a : A ⊗[R] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[R] (A ⊗[R] B))
          ((∑ i ∈ Repr.index (ℛ R a), Repr.left (ℛ R a) i ⊗ₜ[R] Repr.right (ℛ R a) i) ⊗ₜ[R]
            (comul : (a : B) → B ⊗[R] B) 1)) :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A :
            TensorProduct.{u_1, u_4, u_3} R (B ⊗[R] B) (A ⊗[R] A) ≃ₗ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : B ⊗[R] B ⊗[R] (A ⊗[R] A)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        ((comul : (a : B) → B ⊗[R] B) 1 ⊗ₜ[R]
          ∑ i ∈ Repr.index (ℛ R a), Repr.left (ℛ R a) i ⊗ₜ[R] Repr.right (ℛ R a) i) :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))

Tactic:
simp [TensorProduct.tmul_sum, TensorProduct.sum_tmul, Algebra.TensorProduct.one_def]

Premises used: TensorProduct.sum_tmul, TensorProduct.tmul_sum, Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra R A
inst_5 : Bialgebra R B
a : B
hb :
  Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
              (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
            A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : A ⊗[R] B ⊗[R] (A ⊗[R] B)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B :
              TensorProduct.{u_1, u_3, u_4} R (A ⊗[R] A) (B ⊗[R] B) ≃ₗ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
            (a : A ⊗[R] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[R] (A ⊗[R] B))
          ((comul : (a : A) → A ⊗[R] A) 1 ⊗ₜ[R] (comul : (a : B) → B ⊗[R] B) a)) :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A :
            TensorProduct.{u_1, u_4, u_3} R (B ⊗[R] B) (A ⊗[R] A) ≃ₗ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : B ⊗[R] B ⊗[R] (A ⊗[R] A)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        ((comul : (a : B) → B ⊗[R] B) a ⊗ₜ[R] (comul : (a : A) → A ⊗[R] A) 1) :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
⊢ Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
    ((AlgHom.comp (B := A ⊗[R] B)
            (AlgHom.restrictScalars R
              (AlgHom.comp (B := A ⊗[R] B ⊗[R] (A ⊗[R] B))
                  (Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
                      (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
                    A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A))
                  (comulAlgHom R (A ⊗[R] B) : A ⊗[R] B →ₐ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
                A ⊗[R] B →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)))
            Algebra.TensorProduct.includeRight :
          (a : B) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        a :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
    ((AlgHom.comp (B := A ⊗[R] B)
            (AlgHom.restrictScalars R
              (AlgHom.comp (comulAlgHom R (B ⊗[R] A)) (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)))
            Algebra.TensorProduct.includeRight :
          (a : B) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        a :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra R A
inst_5 : Bialgebra R B
a : B
hb :
  Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
              (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
            A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : A ⊗[R] B ⊗[R] (A ⊗[R] B)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B :
              TensorProduct.{u_1, u_3, u_4} R (A ⊗[R] A) (B ⊗[R] B) ≃ₗ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
            (a : A ⊗[R] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[R] (A ⊗[R] B))
          ((comul : (a : A) → A ⊗[R] A) 1 ⊗ₜ[R]
            ∑ i ∈ Repr.index (ℛ R a), Repr.left (ℛ R a) i ⊗ₜ[R] Repr.right (ℛ R a) i)) :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A :
            TensorProduct.{u_1, u_4, u_3} R (B ⊗[R] B) (A ⊗[R] A) ≃ₗ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : B ⊗[R] B ⊗[R] (A ⊗[R] A)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        ((∑ i ∈ Repr.index (ℛ R a), Repr.left (ℛ R a) i ⊗ₜ[R] Repr.right (ℛ R a) i) ⊗ₜ[R]
          (comul : (a : A) → A ⊗[R] A) 1) :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
⊢ Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
              (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
            A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : A ⊗[R] B ⊗[R] (A ⊗[R] B)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B :
              TensorProduct.{u_1, u_3, u_4} R (A ⊗[R] A) (B ⊗[R] B) ≃ₗ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
            (a : A ⊗[R] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[R] (A ⊗[R] B))
          ((comul : (a : A) → A ⊗[R] A) 1 ⊗ₜ[R] (comul : (a : B) → B ⊗[R] B) a)) :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A :
            TensorProduct.{u_1, u_4, u_3} R (B ⊗[R] B) (A ⊗[R] A) ≃ₗ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : B ⊗[R] B ⊗[R] (A ⊗[R] A)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        ((comul : (a : B) → B ⊗[R] B) a ⊗ₜ[R] (comul : (a : A) → A ⊗[R] A) 1) :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))

Tactic:
rw [← (ℛ R a).eq]

Premises used: Coalgebra.Repr.eq, Coalgebra.Repr.arbitrary
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra R A
inst_5 : Bialgebra R B
a : B
⊢ Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
              (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
            A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : A ⊗[R] B ⊗[R] (A ⊗[R] B)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B :
              TensorProduct.{u_1, u_3, u_4} R (A ⊗[R] A) (B ⊗[R] B) ≃ₗ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
            (a : A ⊗[R] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[R] (A ⊗[R] B))
          ((comul : (a : A) → A ⊗[R] A) 1 ⊗ₜ[R]
            ∑ i ∈ Repr.index (ℛ R a), Repr.left (ℛ R a) i ⊗ₜ[R] Repr.right (ℛ R a) i)) :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A :
            TensorProduct.{u_1, u_4, u_3} R (B ⊗[R] B) (A ⊗[R] A) ≃ₗ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : B ⊗[R] B ⊗[R] (A ⊗[R] A)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        ((∑ i ∈ Repr.index (ℛ R a), Repr.left (ℛ R a) i ⊗ₜ[R] Repr.right (ℛ R a) i) ⊗ₜ[R]
          (comul : (a : A) → A ⊗[R] A) 1) :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))

Tactic:
simp [TensorProduct.tmul_sum, TensorProduct.sum_tmul, Algebra.TensorProduct.one_def]

Premises used: TensorProduct.sum_tmul, TensorProduct.tmul_sum, Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
inst_3 : IsCocomm R A
H :
  ∀ (x : A),
    Eq (α := A ⊗[R] A)
      ((BialgHom.comp (BialgEquiv.toBialgHom (TensorProduct.comm R A A)) (comulBialgHom R A) : (a : A) → A ⊗[R] A) x :
        A ⊗[R] A)
      ((comulBialgHom R A : (a : A) → A ⊗[R] A) x : A ⊗[R] A)
⊢ Eq (α := A →ₐc[R] A ⊗[R] A) (BialgHom.comp (BialgEquiv.toBialgHom (TensorProduct.comm R A A)) (comulBialgHom R A))
    (comulBialgHom R A)

Tactic:
ext
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
inst_3 : IsCocomm R A
x : A
⊢ Eq (α := A ⊗[R] A)
    ((BialgHom.comp (BialgEquiv.toBialgHom (TensorProduct.comm R A A)) (comulBialgHom R A) : (a : A) → A ⊗[R] A) x :
      A ⊗[R] A)
    ((comulBialgHom R A : (a : A) → A ⊗[R] A) x : A ⊗[R] A)

Tactic:
comm_comul _ _

Premises used: Quotient.liftOn', AddCon.liftOn, Coalgebra.comm_comul
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
inst_3 : IsCocomm R A
x : A
⊢ Eq (α := A ⊗[R] A)
    ((BialgHom.comp (BialgEquiv.toBialgHom (TensorProduct.comm R A A)) (comulBialgHom R A) : (a : A) → A ⊗[R] A) x :
      A ⊗[R] A)
    ((comulBialgHom R A : (a : A) → A ⊗[R] A) x : A ⊗[R] A)

Tactic:
exact comm_comul _ _

Premises used: Coalgebra.comm_comul
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
a :
  ∀ (x x_1 : A),
    Eq.{u_1 + 1} (α := R)
      (((((TensorProduct.AlgebraTensorModule.curry (counit ∘ₗ LinearMap.mul' R A) : A →ₗ[R] A →ₗ[R] R) :
                  (a : A) → A →ₗ[R] R)
                x :
              A →ₗ[R] R) :
            (a : A) → R)
          x_1 :
        R)
      (((((TensorProduct.AlgebraTensorModule.curry counit : A →ₗ[R] A →ₗ[R] R) : (a : A) → A →ₗ[R] R) x : A →ₗ[R] R) :
            (a : A) → R)
          x_1 :
        R)
⊢ Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (A ⊗[R] A) R) (counit ∘ₗ LinearMap.mul' R A) counit

Tactic:
ext
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
x x_1 : A
⊢ Eq.{u_1 + 1} (α := R)
    (((((TensorProduct.AlgebraTensorModule.curry (counit ∘ₗ LinearMap.mul' R A) : A →ₗ[R] A →ₗ[R] R) :
                (a : A) → A →ₗ[R] R)
              x :
            A →ₗ[R] R) :
          (a : A) → R)
        x_1 :
      R)
    (((((TensorProduct.AlgebraTensorModule.curry counit : A →ₗ[R] A →ₗ[R] R) : (a : A) → A →ₗ[R] R) x : A →ₗ[R] R) :
          (a : A) → R)
        x_1 :
      R)

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
a :
  ∀ (a b : A),
    Eq (α := A ⊗[R] A)
      (((((TensorProduct.AlgebraTensorModule.curry
                      (_root_.TensorProduct.map (LinearMap.mul' R A) (LinearMap.mul' R A) ∘ₗ comul) :
                    A →ₗ[R] A →ₗ[R] A ⊗[R] A) :
                  (a : A) → A →ₗ[R] A ⊗[R] A)
                a :
              A →ₗ[R] A ⊗[R] A) :
            (a : A) → A ⊗[R] A)
          b :
        A ⊗[R] A)
      (((((TensorProduct.AlgebraTensorModule.curry (comul ∘ₗ LinearMap.mul' R A) : A →ₗ[R] A →ₗ[R] A ⊗[R] A) :
                  (a : A) → A →ₗ[R] A ⊗[R] A)
                a :
              A →ₗ[R] A ⊗[R] A) :
            (a : A) → A ⊗[R] A)
          b :
        A ⊗[R] A)
⊢ Eq (α := A ⊗[R] A →ₗ[R] A ⊗[R] A) (_root_.TensorProduct.map (LinearMap.mul' R A) (LinearMap.mul' R A) ∘ₗ comul)
    (comul ∘ₗ LinearMap.mul' R A)

Tactic:
ext a b
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
a b : A
a₁ :
  ∑ x ∈ Repr.index (ℛ R a),
      (_root_.TensorProduct.map (LinearMap.mul' R A) (LinearMap.mul' R A) : (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A)
        (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A A A :
              A ⊗[R] A ⊗[R] (A ⊗[R] A) ≃ₗ[R] A ⊗[R] A ⊗[R] (A ⊗[R] A)) :
            (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A ⊗[R] (A ⊗[R] A))
          (Repr.left (ℛ R a) x ⊗ₜ[R] Repr.right (ℛ R a) x ⊗ₜ[R]
            ∑ i ∈ Repr.index (ℛ R b), Repr.left (ℛ R b) i ⊗ₜ[R] Repr.right (ℛ R b) i)) =
    HMul.hMul (α := A ⊗[R] A) (∑ i ∈ Repr.index (ℛ R a), Repr.left (ℛ R a) i ⊗ₜ[R] Repr.right (ℛ R a) i)
      (∑ i ∈ Repr.index (ℛ R b), Repr.left (ℛ R b) i ⊗ₜ[R] Repr.right (ℛ R b) i)
⊢ Eq (α := A ⊗[R] A)
    (((((TensorProduct.AlgebraTensorModule.curry
                    (_root_.TensorProduct.map (LinearMap.mul' R A) (LinearMap.mul' R A) ∘ₗ comul) :
                  A →ₗ[R] A →ₗ[R] A ⊗[R] A) :
                (a : A) → A →ₗ[R] A ⊗[R] A)
              a :
            A →ₗ[R] A ⊗[R] A) :
          (a : A) → A ⊗[R] A)
        b :
      A ⊗[R] A)
    (((((TensorProduct.AlgebraTensorModule.curry (comul ∘ₗ LinearMap.mul' R A) : A →ₗ[R] A →ₗ[R] A ⊗[R] A) :
                (a : A) → A →ₗ[R] A ⊗[R] A)
              a :
            A →ₗ[R] A ⊗[R] A) :
          (a : A) → A ⊗[R] A)
        b :
      A ⊗[R] A)

Tactic:
simp [← (ℛ R a).eq, ← (ℛ R b).eq, TensorProduct.sum_tmul]

Premises used: TensorProduct.sum_tmul, Coalgebra.Repr.eq, Coalgebra.Repr.arbitrary
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
a b : A
⊢ ∑ x ∈ Repr.index (ℛ R a),
      (_root_.TensorProduct.map (LinearMap.mul' R A) (LinearMap.mul' R A) : (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A)
        (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A A A :
              A ⊗[R] A ⊗[R] (A ⊗[R] A) ≃ₗ[R] A ⊗[R] A ⊗[R] (A ⊗[R] A)) :
            (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A ⊗[R] (A ⊗[R] A))
          (Repr.left (ℛ R a) x ⊗ₜ[R] Repr.right (ℛ R a) x ⊗ₜ[R]
            ∑ i ∈ Repr.index (ℛ R b), Repr.left (ℛ R b) i ⊗ₜ[R] Repr.right (ℛ R b) i)) =
    HMul.hMul (α := A ⊗[R] A) (∑ i ∈ Repr.index (ℛ R a), Repr.left (ℛ R a) i ⊗ₜ[R] Repr.right (ℛ R a) i)
      (∑ i ∈ Repr.index (ℛ R b), Repr.left (ℛ R b) i ⊗ₜ[R] Repr.right (ℛ R b) i)

Tactic:
simp [TensorProduct.tmul_sum, Finset.sum_mul_sum]

Premises used: TensorProduct.tmul_sum, Finset.sum_mul_sum
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
⊢ (↑(mulCoalgHom R A) :
      [inst_3 : FunLike (A ⊗[R] A →ₗc[R] A) (A ⊗[R] A) A] →
        [SemilinearMapClass (A ⊗[R] A →ₗc[R] A) (RingHom.id R) (A ⊗[R] A) A] → A ⊗[R] A →ₗ[R] A) =
    LinearMap.mul' R A

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, SemilinearMapClass.semilinearMap, TensorProduct, LinearMap.mul', TensorProduct.lift, rfl