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 S A
inst_5 : Bialgebra R B
inst_6 : Algebra R A
inst_7 : Algebra R S
inst_8 : IsScalarTower R S A
hcounit :
  Eq (α := (a : A ⊗[R] B) → S) (⇑counit : (a : A ⊗[R] B) → S)
    (⇑(AlgHom.toLinearMap
            (AlgHom.comp (B := S ⊗[R] R) ((↑(Algebra.TensorProduct.rid R S S) : S ⊗[R] R →ₐ[S] S) : S ⊗[R] R →ₐ[S] S)
              (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B) : A ⊗[R] B →ₐ[S] S ⊗[R] R)) :
          A ⊗[R] B →ₗ[S] S) :
      (a : A ⊗[R] B) → S)
hcomul :
  Eq (α := (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B)) (⇑comul : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
    (⇑(AlgHom.toLinearMap
            (AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))
              ((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B) :
                  TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
                TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B))
              (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B) :
                A ⊗[R] B →ₐ[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))) :
          A ⊗[R] B →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
      (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
⊢ Eq.{u_2 + 1} (α := S)
    (((AlgHom.comp (B := S ⊗[R] R) ((↑(Algebra.TensorProduct.rid R S S) : S ⊗[R] R →ₐ[S] S) : S ⊗[R] R →ₐ[S] S)
              (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B) : A ⊗[R] B →ₐ[S] S ⊗[R] R) :
            A ⊗[R] B →ₐ[S] S) :
          (a : A ⊗[R] B) → S)
        1 :
      S)
    (1 : S)

Tactic:
simp only [map_one, map_mul]

Premises used: map_mul, map_one
-- 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 S A
inst_5 : Bialgebra R B
inst_6 : Algebra R A
inst_7 : Algebra R S
inst_8 : IsScalarTower R S A
hcounit :
  Eq (α := (a : A ⊗[R] B) → S) (⇑counit : (a : A ⊗[R] B) → S)
    (⇑(AlgHom.toLinearMap
            (AlgHom.comp (B := S ⊗[R] R) ((↑(Algebra.TensorProduct.rid R S S) : S ⊗[R] R →ₐ[S] S) : S ⊗[R] R →ₐ[S] S)
              (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B) : A ⊗[R] B →ₐ[S] S ⊗[R] R)) :
          A ⊗[R] B →ₗ[S] S) :
      (a : A ⊗[R] B) → S)
hcomul :
  Eq (α := (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B)) (⇑comul : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
    (⇑(AlgHom.toLinearMap
            (AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))
              ((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B) :
                  TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
                TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B))
              (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B) :
                A ⊗[R] B →ₐ[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))) :
          A ⊗[R] B →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
      (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
x y : A ⊗[R] B
⊢ ((AlgHom.comp (B := S ⊗[R] R) ((↑(Algebra.TensorProduct.rid R S S) : S ⊗[R] R →ₐ[S] S) : S ⊗[R] R →ₐ[S] S)
            (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B) : A ⊗[R] B →ₐ[S] S ⊗[R] R) :
          A ⊗[R] B →ₐ[S] S) :
        (a : A ⊗[R] B) → S)
      (x * y) =
    HMul.hMul (α := S) (β := S)
      (((AlgHom.comp (B := S ⊗[R] R) ((↑(Algebra.TensorProduct.rid R S S) : S ⊗[R] R →ₐ[S] S) : S ⊗[R] R →ₐ[S] S)
                (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B) : A ⊗[R] B →ₐ[S] S ⊗[R] R) :
              A ⊗[R] B →ₐ[S] S) :
            (a : A ⊗[R] B) → S)
          x :
        S)
      (((AlgHom.comp (B := S ⊗[R] R) ((↑(Algebra.TensorProduct.rid R S S) : S ⊗[R] R →ₐ[S] S) : S ⊗[R] R →ₐ[S] S)
                (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B) : A ⊗[R] B →ₐ[S] S ⊗[R] R) :
              A ⊗[R] B →ₐ[S] S) :
            (a : A ⊗[R] B) → S)
          y :
        S)

Tactic:
simp only [map_one, map_mul]

Premises used: map_mul, map_one
-- 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 S A
inst_5 : Bialgebra R B
inst_6 : Algebra R A
inst_7 : Algebra R S
inst_8 : IsScalarTower R S A
hcounit :
  Eq (α := (a : A ⊗[R] B) → S) (⇑counit : (a : A ⊗[R] B) → S)
    (⇑(AlgHom.toLinearMap
            (AlgHom.comp (B := S ⊗[R] R) ((↑(Algebra.TensorProduct.rid R S S) : S ⊗[R] R →ₐ[S] S) : S ⊗[R] R →ₐ[S] S)
              (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B) : A ⊗[R] B →ₐ[S] S ⊗[R] R)) :
          A ⊗[R] B →ₗ[S] S) :
      (a : A ⊗[R] B) → S)
hcomul :
  Eq (α := (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B)) (⇑comul : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
    (⇑(AlgHom.toLinearMap
            (AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))
              ((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B) :
                  TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
                TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B))
              (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B) :
                A ⊗[R] B →ₐ[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))) :
          A ⊗[R] B →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
      (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
⊢ Eq (α := A ⊗[R] B ⊗[S] (A ⊗[R] B))
    (((AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))
            ((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B) :
                TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
              TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B))
            (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B) :
              A ⊗[R] B →ₐ[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B)) :
          A ⊗[R] B →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
        (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
      1)
    1

Tactic:
simp only [map_one, map_mul]

Premises used: map_mul, map_one
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra S A
inst_5 : Bialgebra R B
inst_6 : Algebra R A
inst_7 : Algebra R S
inst_8 : IsScalarTower R S A
⊢ Eq (α := A ⊗[R] B →ₐ[S] S) (counitAlgHom S (A ⊗[R] B))
    (AlgHom.comp (B := S ⊗[R] R) ((↑(Algebra.TensorProduct.rid R S S) : S ⊗[R] R →ₐ[S] S) : S ⊗[R] R →ₐ[S] S)
      (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B) : A ⊗[R] B →ₐ[S] S ⊗[R] R))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, AlgHom.ofLinearMap, Bialgebra.counitAlgHom, AlgHom.comp, rfl
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra S A
inst_5 : Bialgebra R B
inst_6 : Algebra R A
inst_7 : Algebra R S
inst_8 : IsScalarTower R S A
⊢ Eq (α := A ⊗[R] B →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) (comulAlgHom S (A ⊗[R] B))
    (AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))
      ((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B) :
          TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
        TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B))
      (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B) :
        A ⊗[R] B →ₐ[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B)))

Tactic:
rfl

Premises used: Bialgebra.comulAlgHom, Quotient.liftOn', AddCon.liftOn, AlgHom.ofLinearMap, AlgHom.comp, rfl
-- 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 S A
inst_5 : Bialgebra R B
inst_6 : Algebra R A
inst_7 : Algebra R S
inst_8 : IsScalarTower R S A
inst_9 : Semiring C
inst_10 : Semiring D
inst_11 : Bialgebra S C
inst_12 : Bialgebra R D
inst_13 : Algebra R C
inst_14 : IsScalarTower R S C
f : A →ₐc[S] C
g : B →ₐc[R] D
x : A
y : B
⊢ Eq (α := C ⊗[R] D) ((map f g : (a : A ⊗[R] B) → C ⊗[R] D) (x ⊗ₜ[R] y) : C ⊗[R] D)
    ((f : (a : A) → C) x ⊗ₜ[R] (g : (a : B) → D) y : C ⊗[R] D)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- 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 S A
inst_5 : Bialgebra R B
inst_6 : Algebra R A
inst_7 : Algebra R S
inst_8 : IsScalarTower R S A
inst_9 : Semiring C
inst_10 : Semiring D
inst_11 : Bialgebra S C
inst_12 : Bialgebra R D
inst_13 : Algebra R C
inst_14 : IsScalarTower R S C
f : A →ₐc[S] C
g : B →ₐc[R] D
⊢ Eq (α := A ⊗[R] B →ₗc[S] C ⊗[R] D) (↑(map f g) : A ⊗[R] B →ₗc[S] C ⊗[R] D)
    (Coalgebra.TensorProduct.map (↑f : A →ₗc[S] C) (↑g : B →ₗc[R] D))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Coalgebra.TensorProduct.map, CoalgHomClass.toCoalgHom, TensorProduct, TensorProduct.AlgebraTensorModule.map, rfl, TensorProduct.AlgebraTensorModule.lift
-- 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 S A
inst_5 : Bialgebra R B
inst_6 : Algebra R A
inst_7 : Algebra R S
inst_8 : IsScalarTower R S A
inst_9 : Semiring C
inst_10 : Semiring D
inst_11 : Bialgebra S C
inst_12 : Bialgebra R D
inst_13 : Algebra R C
inst_14 : IsScalarTower R S C
f : A →ₐc[S] C
g : B →ₐc[R] D
⊢ Eq (α := A ⊗[R] B →ₐ[S] C ⊗[R] D) ((↑(map f g) : A ⊗[R] B →ₐ[S] C ⊗[R] D) : A ⊗[R] B →ₐ[S] C ⊗[R] D)
    (Algebra.TensorProduct.map (↑f : A →ₐ[S] C) (↑g : B →ₐ[R] D) : A ⊗[R] B →ₐ[S] C ⊗[R] D)

Tactic:
rfl

Premises used: Algebra.TensorProduct.algHomOfLinearMapTensorProduct, Algebra.TensorProduct.map, AlgHom.ofLinearMap, BialgHom.toAlgHom, rfl
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Bialgebra S A
inst_4 : Algebra R A
inst_5 : Algebra R S
inst_6 : IsScalarTower R S A
inst_7 : Semiring C
inst_8 : Semiring D
inst_9 : Bialgebra S C
inst_10 : Bialgebra R D
inst_11 : Algebra R C
inst_12 : IsScalarTower R S C
x : A
y : C
z : D
⊢ Eq (α := A ⊗[S] (C ⊗[R] D))
    (((TensorProduct.assoc R S A C D : A ⊗[S] C ⊗[R] D ≃ₐc[S] A ⊗[S] (C ⊗[R] D)) :
          (a : A ⊗[S] C ⊗[R] D) → A ⊗[S] (C ⊗[R] D))
        (x ⊗ₜ[S] y ⊗ₜ[R] z) :
      A ⊗[S] (C ⊗[R] D))
    (x ⊗ₜ[S] (y ⊗ₜ[R] z) : A ⊗[S] (C ⊗[R] D))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Bialgebra S A
inst_4 : Algebra R A
inst_5 : Algebra R S
inst_6 : IsScalarTower R S A
inst_7 : Semiring C
inst_8 : Semiring D
inst_9 : Bialgebra S C
inst_10 : Bialgebra R D
inst_11 : Algebra R C
inst_12 : IsScalarTower R S C
x : A
y : C
z : D
⊢ Eq (α := A ⊗[S] C ⊗[R] D)
    (((BialgEquiv.symm (TensorProduct.assoc R S A C D) : A ⊗[S] (C ⊗[R] D) ≃ₐc[S] A ⊗[S] C ⊗[R] D) :
          (a : A ⊗[S] (C ⊗[R] D)) → A ⊗[S] C ⊗[R] D)
        (x ⊗ₜ[S] (y ⊗ₜ[R] z)) :
      A ⊗[S] C ⊗[R] D)
    (x ⊗ₜ[S] y ⊗ₜ[R] z : A ⊗[S] C ⊗[R] D)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Bialgebra S A
inst_4 : Algebra R A
inst_5 : Algebra R S
inst_6 : IsScalarTower R S A
inst_7 : Semiring C
inst_8 : Semiring D
inst_9 : Bialgebra S C
inst_10 : Bialgebra R D
inst_11 : Algebra R C
inst_12 : IsScalarTower R S C
⊢ Eq (α := A ⊗[S] C ⊗[R] D ≃ₗc[S] A ⊗[S] (C ⊗[R] D))
    ((↑(TensorProduct.assoc R S A C D : A ⊗[S] C ⊗[R] D ≃ₐc[S] A ⊗[S] (C ⊗[R] D)) :
        A ⊗[S] C ⊗[R] D ≃ₗc[S] A ⊗[S] (C ⊗[R] D)) :
      A ⊗[S] C ⊗[R] D ≃ₗc[S] A ⊗[S] (C ⊗[R] D))
    (Coalgebra.TensorProduct.assoc R S A C D : A ⊗[S] C ⊗[R] D ≃ₗc[S] A ⊗[S] (C ⊗[R] D))

Tactic:
rfl

Premises used: CoalgEquivClass.toCoalgEquiv, Quotient.liftOn', AddCon.liftOn, Coalgebra.TensorProduct.assoc, CoalgHomClass.toCoalgHom, TensorProduct, rfl, TensorProduct.AlgebraTensorModule.lift
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Bialgebra S A
inst_4 : Algebra R A
inst_5 : Algebra R S
inst_6 : IsScalarTower R S A
inst_7 : Semiring C
inst_8 : Semiring D
inst_9 : Bialgebra S C
inst_10 : Bialgebra R D
inst_11 : Algebra R C
inst_12 : IsScalarTower R S C
⊢ Eq (α := A ⊗[S] C ⊗[R] D ≃ₐ[S] A ⊗[S] (C ⊗[R] D))
    (BialgEquiv.toAlgEquiv (TensorProduct.assoc R S A C D : A ⊗[S] C ⊗[R] D ≃ₐc[S] A ⊗[S] (C ⊗[R] D)) :
      A ⊗[S] C ⊗[R] D ≃ₐ[S] A ⊗[S] (C ⊗[R] D))
    (Algebra.TensorProduct.assoc R S S A C D : A ⊗[S] C ⊗[R] D ≃ₐ[S] A ⊗[S] (C ⊗[R] D))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Algebra.TensorProduct.assoc, TensorProduct, AlgEquiv.ofLinearEquiv, BialgEquiv.toAlgEquiv, rfl
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring B
inst_2 : Bialgebra R B
⊢ Eq (α := R ⊗[R] B ≃ₗc[R] B) (↑(TensorProduct.lid R B) : R ⊗[R] B ≃ₗc[R] B) (Coalgebra.TensorProduct.lid R B)

Tactic:
rfl

Premises used: CoalgEquivClass.toCoalgEquiv, Quotient.liftOn', AddCon.liftOn, Coalgebra.TensorProduct.lid, CoalgHomClass.toCoalgHom, TensorProduct, TensorProduct.tmul, TensorProduct.lift, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring B
inst_2 : Bialgebra R B
⊢ Eq (α := R ⊗[R] B ≃ₐ[R] B) (BialgEquiv.toAlgEquiv (TensorProduct.lid R B)) (Algebra.TensorProduct.lid R B)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Algebra.TensorProduct.lid, Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct, TensorProduct, BialgEquiv.toAlgEquiv, rfl
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring B
inst_2 : Bialgebra R B
r : R
a : B
⊢ (TensorProduct.lid R B : (a : R ⊗[R] B) → B) (r ⊗ₜ[R] a) = r • a

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring B
inst_2 : Bialgebra R B
a : B
⊢ Eq (α := R ⊗[R] B) ((BialgEquiv.symm (TensorProduct.lid R B) : (a : B) → R ⊗[R] B) a : R ⊗[R] B)
    (1 ⊗ₜ[R] a : R ⊗[R] B)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Bialgebra S A
inst_4 : Algebra R A
inst_5 : Algebra R S
inst_6 : IsScalarTower R S A
x : A ⊗[R] R
⊢ Eq.{u_3 + 1} (α := A) ((Coalgebra.TensorProduct.rid R S A : (a : A ⊗[R] R) → A) x : A)
    (((Algebra.TensorProduct.rid R R A : A ⊗[R] R ≃ₐ[R] A) : (a : A ⊗[R] R) → A) x : A)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- 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 S A
inst_5 : Bialgebra R B
inst_6 : Algebra R A
inst_7 : Algebra R S
inst_8 : IsScalarTower R S A
inst_9 : Semiring C
inst_10 : Semiring D
inst_11 : Bialgebra S C
inst_12 : Bialgebra R D
inst_13 : Algebra R C
inst_14 : IsScalarTower R S C
x y : A ⊗[R] R
⊢ AddHom.toFun
      (LinearMap.toAddHom
        (CoalgHom.toLinearMap (CoalgEquiv.toCoalgHom (Coalgebra.TensorProduct.rid R S A)) : A ⊗[R] R →ₗ[S] A))
      (x * y) =
    AddHom.toFun
        (LinearMap.toAddHom
          (CoalgHom.toLinearMap (CoalgEquiv.toCoalgHom (Coalgebra.TensorProduct.rid R S A)) : A ⊗[R] R →ₗ[S] A))
        x *
      AddHom.toFun
        (LinearMap.toAddHom
          (CoalgHom.toLinearMap (CoalgEquiv.toCoalgHom (Coalgebra.TensorProduct.rid R S A)) : A ⊗[R] R →ₗ[S] A))
        y

Tactic:
simp only [CoalgEquiv.toCoalgHom_eq_coe, CoalgHom.toLinearMap_eq_coe, AddHom.toFun_eq_coe,
      LinearMap.coe_toAddHom, CoalgHom.coe_toLinearMap, CoalgHom.coe_coe,
      coalgebra_rid_eq_algebra_rid_apply, map_mul]

Premises used: CoalgEquiv.toCoalgHom_eq_coe, AddHom.toFun_eq_coe, CoalgHom.coe_coe, map_mul, Bialgebra.TensorProduct.coalgebra_rid_eq_algebra_rid_apply, CoalgHom.coe_toLinearMap, LinearMap.coe_toAddHom, CoalgHom.toLinearMap_eq_coe
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Bialgebra S A
inst_4 : Algebra R A
inst_5 : Algebra R S
inst_6 : IsScalarTower R S A
⊢ Eq (α := A ⊗[R] R ≃ₗc[S] A) (↑(TensorProduct.rid R S A) : A ⊗[R] R ≃ₗc[S] A) (Coalgebra.TensorProduct.rid R S A)

Tactic:
rfl

Premises used: CoalgEquivClass.toCoalgEquiv, Coalgebra.TensorProduct.rid, Quotient.liftOn', AddCon.liftOn, CoalgHomClass.toCoalgHom, TensorProduct, TensorProduct.tmul, AddCon.toQuotient, rfl, TensorProduct.AlgebraTensorModule.lift
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Bialgebra S A
inst_4 : Algebra R A
inst_5 : Algebra R S
inst_6 : IsScalarTower R S A
h :
  ∀ (x : A ⊗[R] R),
    Eq.{u_3 + 1} (α := A)
      (((BialgEquiv.toAlgEquiv (TensorProduct.rid R S A) : A ⊗[R] R ≃ₐ[S] A) : (a : A ⊗[R] R) → A) x : A)
      (((Algebra.TensorProduct.rid R S A : A ⊗[R] R ≃ₐ[S] A) : (a : A ⊗[R] R) → A) x : A)
⊢ Eq (α := A ⊗[R] R ≃ₐ[S] A) (BialgEquiv.toAlgEquiv (TensorProduct.rid R S A) : A ⊗[R] R ≃ₐ[S] A)
    (Algebra.TensorProduct.rid R S A : A ⊗[R] R ≃ₐ[S] A)

Tactic:
ext x
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Bialgebra S A
inst_4 : Algebra R A
inst_5 : Algebra R S
inst_6 : IsScalarTower R S A
x : A ⊗[R] R
⊢ Eq.{u_3 + 1} (α := A)
    (((BialgEquiv.toAlgEquiv (TensorProduct.rid R S A) : A ⊗[R] R ≃ₐ[S] A) : (a : A ⊗[R] R) → A) x : A)
    (((Algebra.TensorProduct.rid R S A : A ⊗[R] R ≃ₐ[S] A) : (a : A ⊗[R] R) → A) x : A)

Tactic:
coalgebra_rid_eq_algebra_rid_apply x

Premises used: Quotient.liftOn', AddCon.liftOn, Bialgebra.TensorProduct.coalgebra_rid_eq_algebra_rid_apply
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Bialgebra S A
inst_4 : Algebra R A
inst_5 : Algebra R S
inst_6 : IsScalarTower R S A
x : A ⊗[R] R
⊢ Eq.{u_3 + 1} (α := A)
    (((BialgEquiv.toAlgEquiv (TensorProduct.rid R S A) : A ⊗[R] R ≃ₐ[S] A) : (a : A ⊗[R] R) → A) x : A)
    (((Algebra.TensorProduct.rid R S A : A ⊗[R] R ≃ₐ[S] A) : (a : A ⊗[R] R) → A) x : A)

Tactic:
exact coalgebra_rid_eq_algebra_rid_apply x

Premises used: Bialgebra.TensorProduct.coalgebra_rid_eq_algebra_rid_apply
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Bialgebra S A
inst_4 : Algebra R A
inst_5 : Algebra R S
inst_6 : IsScalarTower R S A
r : R
a : A
⊢ (TensorProduct.rid R S A : (a : A ⊗[R] R) → A) (a ⊗ₜ[R] r) = r • a

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Bialgebra S A
inst_4 : Algebra R A
inst_5 : Algebra R S
inst_6 : IsScalarTower R S A
a : A
⊢ Eq (α := A ⊗[R] R) ((BialgEquiv.symm (TensorProduct.rid R S A) : (a : A) → A ⊗[R] R) a : A ⊗[R] R)
    (a ⊗ₜ[R] 1 : A ⊗[R] R)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- 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 :
  ∀ (x : A),
    Eq.{u_1 + 1} (α := R)
      ((AlgHom.comp (B := A ⊗[R] B)
              (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.includeLeft :
            (a : A) → R)
          x :
        R)
      ((AlgHom.comp (B := A ⊗[R] B) (counitAlgHom R (A ⊗[R] B) : A ⊗[R] B →ₐ[R] R) Algebra.TensorProduct.includeLeft :
            (a : A) → R)
          x :
        R)
hb :
  ∀ (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)
⊢ Eq (α := A ⊗[R] B →ₐ[R] 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))
    (counitAlgHom R (A ⊗[R] B))

Tactic:
ext
-- 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 : A
⊢ Eq.{u_1 + 1} (α := R)
    ((AlgHom.comp (B := A ⊗[R] B)
            (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.includeLeft :
          (a : A) → R)
        x :
      R)
    ((AlgHom.comp (B := A ⊗[R] B) (counitAlgHom R (A ⊗[R] B) : A ⊗[R] B →ₐ[R] R) Algebra.TensorProduct.includeLeft :
          (a : A) → R)
        x :
      R)

Tactic:
simp