mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
A : Type u_3
B : Type u_4
inst✝²⁷ : CommSemiring R✝
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : AddCommMonoid A
inst✝²⁴ : AddCommMonoid B
inst✝²³ : Algebra R✝ S✝
inst✝²² : Module R✝ A
inst✝²¹ : Module S✝ A
inst✝²⁰ : Module R✝ B
inst✝¹⁹ : IsScalarTower R✝ S✝ A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
x✝² : M
x✝¹ : N
x✝ : P
⊢ (((AlgebraTensorModule.curry (AlgebraTensorModule.curry (counit ∘ₗ ↑(AlgebraTensorModule.assoc R S S M N P)))) x✝²)
        x✝¹)
      x✝ =
    (((AlgebraTensorModule.curry (AlgebraTensorModule.curry counit)) x✝²) x✝¹) x✝

Tactic:
;

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
A : Type u_3
B : Type u_4
inst✝²⁷ : CommSemiring R✝
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : AddCommMonoid A
inst✝²⁴ : AddCommMonoid B
inst✝²³ : Algebra R✝ S✝
inst✝²² : Module R✝ A
inst✝²¹ : Module S✝ A
inst✝²⁰ : Module R✝ B
inst✝¹⁹ : IsScalarTower R✝ S✝ A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
x✝² : M
x✝¹ : N
x✝ : P
⊢ (((AlgebraTensorModule.curry (AlgebraTensorModule.curry (counit ∘ₗ ↑(AlgebraTensorModule.assoc R S S M N P)))) x✝²)
        x✝¹)
      x✝ =
    (((AlgebraTensorModule.curry (AlgebraTensorModule.curry counit)) x✝²) x✝¹) x✝
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝⁴ x✝³ x✝² : BialgCat R
x✝¹ : x✝³ ⟶ x✝²
x✝ : ↑((forget₂ (BialgCat R) (AlgCat R)).obj (x✝⁴ ⊗ x✝³))
⊢ (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (x✝⁴ ◁ x✝¹))) x✝ =
    (AlgCat.Hom.hom
        ((Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝⁴ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝³)).inv ≫
          (forget₂ (BialgCat R) (AlgCat R)).obj x✝⁴ ◁ (forget₂ (BialgCat R) (AlgCat R)).map x✝¹ ≫
            (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝⁴ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝²)).hom))
      x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
x✝⁴ x✝³ x✝² : BialgCat R
x✝¹ : x✝³ ⟶ x✝²
x✝ : ↑((forget₂ (BialgCat R) (AlgCat R)).obj (x✝⁴ ⊗ x✝³))
⊢ (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (x✝⁴ ◁ x✝¹))) x✝ =
    (AlgCat.Hom.hom
        ((Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝⁴ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝³)).inv ≫
          (forget₂ (BialgCat R) (AlgCat R)).obj x✝⁴ ◁ (forget₂ (BialgCat R) (AlgCat R)).map x✝¹ ≫
            (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝⁴ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝²)).hom))
      x✝
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁✝ X₂✝ : BialgCat R
x✝² : X₁✝ ⟶ X₂✝
x✝¹ : BialgCat R
x✝ : ↑((forget₂ (BialgCat R) (AlgCat R)).obj (X₁✝ ⊗ x✝¹))
⊢ (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (x✝² ▷ x✝¹))) x✝ =
    (AlgCat.Hom.hom
        ((Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj X₁✝ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).inv ≫
          (forget₂ (BialgCat R) (AlgCat R)).map x✝² ▷ (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹ ≫
            (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj X₂✝ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).hom))
      x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
X₁✝ X₂✝ : BialgCat R
x✝² : X₁✝ ⟶ X₂✝
x✝¹ : BialgCat R
x✝ : ↑((forget₂ (BialgCat R) (AlgCat R)).obj (X₁✝ ⊗ x✝¹))
⊢ (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (x✝² ▷ x✝¹))) x✝ =
    (AlgCat.Hom.hom
        ((Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj X₁✝ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).inv ≫
          (forget₂ (BialgCat R) (AlgCat R)).map x✝² ▷ (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹ ≫
            (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj X₂✝ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).hom))
      x✝
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁✝ Y₁✝ X₂✝ Y₂✝ : BialgCat R
x✝² : X₁✝ ⟶ Y₁✝
x✝¹ : X₂✝ ⟶ Y₂✝
x✝ : ↑((forget₂ (BialgCat R) (AlgCat R)).obj (X₁✝ ⊗ X₂✝))
⊢ (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (x✝² ⊗ₘ x✝¹))) x✝ =
    (AlgCat.Hom.hom
        ((Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj X₁✝ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj X₂✝)).inv ≫
          ((forget₂ (BialgCat R) (AlgCat R)).map x✝² ⊗ₘ (forget₂ (BialgCat R) (AlgCat R)).map x✝¹) ≫
            (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj Y₁✝ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj Y₂✝)).hom))
      x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
X₁✝ Y₁✝ X₂✝ Y₂✝ : BialgCat R
x✝² : X₁✝ ⟶ Y₁✝
x✝¹ : X₂✝ ⟶ Y₂✝
x✝ : ↑((forget₂ (BialgCat R) (AlgCat R)).obj (X₁✝ ⊗ X₂✝))
⊢ (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (x✝² ⊗ₘ x✝¹))) x✝ =
    (AlgCat.Hom.hom
        ((Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj X₁✝ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj X₂✝)).inv ≫
          ((forget₂ (BialgCat R) (AlgCat R)).map x✝² ⊗ₘ (forget₂ (BialgCat R) (AlgCat R)).map x✝¹) ≫
            (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj Y₁✝ ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj Y₂✝)).hom))
      x✝
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝³ x✝² x✝¹ : BialgCat R
x✝ : x✝³.carrier
⊢ (((AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (α_ x✝³ x✝² x✝¹).hom)).comp
            Algebra.TensorProduct.includeLeft).comp
        Algebra.TensorProduct.includeLeft)
      x✝ =
    (((AlgCat.Hom.hom
                (((Iso.refl
                          ((forget₂ (BialgCat R) (AlgCat R)).obj (x✝³ ⊗ x✝²) ⊗
                            (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).symm ≪≫
                      ((Iso.refl
                            ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³ ⊗
                              (forget₂ (BialgCat R) (AlgCat R)).obj x✝²)).symm ⊗ᵢ
                        Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹))) ≪≫
                    α_ ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³) ((forget₂ (BialgCat R) (AlgCat R)).obj x✝²)
                        ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹) ≪≫
                      (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³) ⊗ᵢ
                          Iso.refl
                            ((forget₂ (BialgCat R) (AlgCat R)).obj x✝² ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)) ≪≫
                        Iso.refl
                          ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³ ⊗
                            (forget₂ (BialgCat R) (AlgCat R)).obj (x✝² ⊗ x✝¹))).hom).comp
            Algebra.TensorProduct.includeLeft).comp
        Algebra.TensorProduct.includeLeft)
      x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
x✝³ x✝² x✝¹ : BialgCat R
x✝ : x✝³.carrier
⊢ (((AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (α_ x✝³ x✝² x✝¹).hom)).comp
            Algebra.TensorProduct.includeLeft).comp
        Algebra.TensorProduct.includeLeft)
      x✝ =
    (((AlgCat.Hom.hom
                (((Iso.refl
                          ((forget₂ (BialgCat R) (AlgCat R)).obj (x✝³ ⊗ x✝²) ⊗
                            (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).symm ≪≫
                      ((Iso.refl
                            ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³ ⊗
                              (forget₂ (BialgCat R) (AlgCat R)).obj x✝²)).symm ⊗ᵢ
                        Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹))) ≪≫
                    α_ ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³) ((forget₂ (BialgCat R) (AlgCat R)).obj x✝²)
                        ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹) ≪≫
                      (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³) ⊗ᵢ
                          Iso.refl
                            ((forget₂ (BialgCat R) (AlgCat R)).obj x✝² ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)) ≪≫
                        Iso.refl
                          ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³ ⊗
                            (forget₂ (BialgCat R) (AlgCat R)).obj (x✝² ⊗ x✝¹))).hom).comp
            Algebra.TensorProduct.includeLeft).comp
        Algebra.TensorProduct.includeLeft)
      x✝
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
A : Type u_3
B : Type u_4
inst✝²⁷ : CommSemiring R✝
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : AddCommMonoid A
inst✝²⁴ : AddCommMonoid B
inst✝²³ : Algebra R✝ S✝
inst✝²² : Module R✝ A
inst✝²¹ : Module S✝ A
inst✝²⁰ : Module R✝ B
inst✝¹⁹ : IsScalarTower R✝ S✝ A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
x✝ : P
⊢ ((AlgebraTensorModule.curry (counit ∘ₗ ↑(_root_.TensorProduct.lid R P))) 1) x✝ =
    ((AlgebraTensorModule.curry counit) 1) x✝

Tactic:
;

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
A : Type u_3
B : Type u_4
inst✝²⁷ : CommSemiring R✝
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : AddCommMonoid A
inst✝²⁴ : AddCommMonoid B
inst✝²³ : Algebra R✝ S✝
inst✝²² : Module R✝ A
inst✝²¹ : Module S✝ A
inst✝²⁰ : Module R✝ B
inst✝¹⁹ : IsScalarTower R✝ S✝ A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
x✝ : P
⊢ ((AlgebraTensorModule.curry (counit ∘ₗ ↑(_root_.TensorProduct.lid R P))) 1) x✝ =
    ((AlgebraTensorModule.curry counit) 1) x✝
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝³ x✝² x✝¹ : BialgCat R
x✝ : x✝¹.carrier
⊢ ((AlgHom.restrictScalars R (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (α_ x✝³ x✝² x✝¹).hom))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            (AlgCat.Hom.hom
              (((Iso.refl
                        ((forget₂ (BialgCat R) (AlgCat R)).obj (x✝³ ⊗ x✝²) ⊗
                          (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).symm ≪≫
                    ((Iso.refl
                          ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³ ⊗
                            (forget₂ (BialgCat R) (AlgCat R)).obj x✝²)).symm ⊗ᵢ
                      Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹))) ≪≫
                  α_ ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³) ((forget₂ (BialgCat R) (AlgCat R)).obj x✝²)
                      ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹) ≪≫
                    (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³) ⊗ᵢ
                        Iso.refl
                          ((forget₂ (BialgCat R) (AlgCat R)).obj x✝² ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)) ≪≫
                      Iso.refl
                        ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³ ⊗
                          (forget₂ (BialgCat R) (AlgCat R)).obj (x✝² ⊗ x✝¹))).hom)).comp
        Algebra.TensorProduct.includeRight)
      x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
x✝³ x✝² x✝¹ : BialgCat R
x✝ : x✝¹.carrier
⊢ ((AlgHom.restrictScalars R (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (α_ x✝³ x✝² x✝¹).hom))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            (AlgCat.Hom.hom
              (((Iso.refl
                        ((forget₂ (BialgCat R) (AlgCat R)).obj (x✝³ ⊗ x✝²) ⊗
                          (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).symm ≪≫
                    ((Iso.refl
                          ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³ ⊗
                            (forget₂ (BialgCat R) (AlgCat R)).obj x✝²)).symm ⊗ᵢ
                      Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹))) ≪≫
                  α_ ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³) ((forget₂ (BialgCat R) (AlgCat R)).obj x✝²)
                      ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹) ≪≫
                    (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³) ⊗ᵢ
                        Iso.refl
                          ((forget₂ (BialgCat R) (AlgCat R)).obj x✝² ⊗ (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)) ≪≫
                      Iso.refl
                        ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³ ⊗
                          (forget₂ (BialgCat R) (AlgCat R)).obj (x✝² ⊗ x✝¹))).hom)).comp
        Algebra.TensorProduct.includeRight)
      x✝
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
A : Type u_3
B : Type u_4
inst✝²⁷ : CommSemiring R✝
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : AddCommMonoid A
inst✝²⁴ : AddCommMonoid B
inst✝²³ : Algebra R✝ S✝
inst✝²² : Module R✝ A
inst✝²¹ : Module S✝ A
inst✝²⁰ : Module R✝ B
inst✝¹⁹ : IsScalarTower R✝ S✝ A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
x✝ : M
⊢ ((AlgebraTensorModule.curry (counit ∘ₗ ↑(AlgebraTensorModule.rid R S M))) x✝) 1 =
    ((AlgebraTensorModule.curry counit) x✝) 1

Tactic:
;

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
A : Type u_3
B : Type u_4
inst✝²⁷ : CommSemiring R✝
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : AddCommMonoid A
inst✝²⁴ : AddCommMonoid B
inst✝²³ : Algebra R✝ S✝
inst✝²² : Module R✝ A
inst✝²¹ : Module S✝ A
inst✝²⁰ : Module R✝ B
inst✝¹⁹ : IsScalarTower R✝ S✝ A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
x✝ : M
⊢ ((AlgebraTensorModule.curry (counit ∘ₗ ↑(AlgebraTensorModule.rid R S M))) x✝) 1 =
    ((AlgebraTensorModule.curry counit) x✝) 1
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝¹ : BialgCat R
x✝ : x✝¹.carrier
⊢ ((AlgHom.restrictScalars R (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (λ_ x✝¹).hom))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            (AlgCat.Hom.hom
              (((Iso.refl
                        ((forget₂ (BialgCat R) (AlgCat R)).obj (𝟙_ (BialgCat R)) ⊗
                          (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).symm ≪≫
                    ((Iso.refl (𝟙_ (AlgCat R))).symm ⊗ᵢ Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹))) ≪≫
                  λ_ ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).hom)).comp
        Algebra.TensorProduct.includeRight)
      x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
x✝¹ : BialgCat R
x✝ : x✝¹.carrier
⊢ ((AlgHom.restrictScalars R (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (λ_ x✝¹).hom))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            (AlgCat.Hom.hom
              (((Iso.refl
                        ((forget₂ (BialgCat R) (AlgCat R)).obj (𝟙_ (BialgCat R)) ⊗
                          (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).symm ≪≫
                    ((Iso.refl (𝟙_ (AlgCat R))).symm ⊗ᵢ Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹))) ≪≫
                  λ_ ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).hom)).comp
        Algebra.TensorProduct.includeRight)
      x✝
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝¹ : BialgCat R
x✝ : x✝¹.carrier
⊢ ((AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (ρ_ x✝¹).hom)).comp Algebra.TensorProduct.includeLeft) x✝ =
    ((AlgCat.Hom.hom
            (((Iso.refl
                      ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹ ⊗
                        (forget₂ (BialgCat R) (AlgCat R)).obj (𝟙_ (BialgCat R)))).symm ≪≫
                  (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹) ⊗ᵢ (Iso.refl (𝟙_ (AlgCat R))).symm)) ≪≫
                ρ_ ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).hom).comp
        Algebra.TensorProduct.includeLeft)
      x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
x✝¹ : BialgCat R
x✝ : x✝¹.carrier
⊢ ((AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (ρ_ x✝¹).hom)).comp Algebra.TensorProduct.includeLeft) x✝ =
    ((AlgCat.Hom.hom
            (((Iso.refl
                      ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹ ⊗
                        (forget₂ (BialgCat R) (AlgCat R)).obj (𝟙_ (BialgCat R)))).symm ≪≫
                  (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹) ⊗ᵢ (Iso.refl (𝟙_ (AlgCat R))).symm)) ≪≫
                ρ_ ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).hom).comp
        Algebra.TensorProduct.includeLeft)
      x✝
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: R✝ : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹³ : CommSemiring R✝
inst✝¹² : CommSemiring S
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : AddCommMonoid B
inst✝⁹ : Algebra R✝ S
inst✝⁸ : Module R✝ A
inst✝⁷ : Module S A
inst✝⁶ : Module R✝ B
inst✝⁵ : IsScalarTower R✝ S A
R : Type u_5
C : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
inst✝ : IsCocomm R C
x✝ : C
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
;

Goal state after:
R✝ : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹³ : CommSemiring R✝
inst✝¹² : CommSemiring S
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : AddCommMonoid B
inst✝⁹ : Algebra R✝ S
inst✝⁸ : Module R✝ A
inst✝⁷ : Module S A
inst✝⁶ : Module R✝ B
inst✝⁵ : IsScalarTower R✝ S A
R : Type u_5
C : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
inst✝ : IsCocomm R C
x✝ : C
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Adjunction.Unique

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ adj1.unit.app x ≫ G.map ((adj1.leftAdjointUniq adj2).hom.app x) =
    (adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x

Tactic:
;

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ adj1.unit.app x ≫ G.map ((adj1.leftAdjointUniq adj2).hom.app x) =
    (adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a + a * b + a * (a * b) = a

Tactic:
rw [← mul_assoc, mul_self, add_assoc, add_self, add_zero]

Goal state after:
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a * (a + b + a * b) = a

Tactic:
rw [mul_add, mul_add, mul_self, ← mul_assoc, mul_self, add_assoc, add_self, add_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Category.Pointed

Goal state before:
pp: X✝ Y✝ Z✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ⇑(ConcreteCategory.hom (x✝¹ ≫ x✝)) = ⇑(ConcreteCategory.hom x✝) ∘ ⇑(ConcreteCategory.hom x✝¹)

Tactic:
;

Goal state after:
X✝ Y✝ Z✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ⇑(ConcreteCategory.hom (x✝¹ ≫ x✝)) = ⇑(ConcreteCategory.hom x✝) ∘ ⇑(ConcreteCategory.hom x✝¹)
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Bialgebra R A
inst✝ : IsCocomm R A
x✝ : A
⊢ ((TensorProduct.comm R A A).toBialgHom.comp (comulBialgHom R A)) x✝ = (comulBialgHom R A) x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Bialgebra R A
inst✝ : IsCocomm R A
x✝ : A
⊢ ((TensorProduct.comm R A A).toBialgHom.comp (comulBialgHom R A)) x✝ = (comulBialgHom R A) x✝
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Bialgebra R A
inst✝¹ : Semiring B
inst✝ : Bialgebra R B
a : A
b : B
x✝¹ x✝ : A
⊢ ((TensorProduct.AlgebraTensorModule.curry (counit ∘ₗ LinearMap.mul' R A)) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry counit) x✝¹) x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Bialgebra R A
inst✝¹ : Semiring B
inst✝ : Bialgebra R B
a : A
b : B
x✝¹ x✝ : A
⊢ ((TensorProduct.AlgebraTensorModule.curry (counit ∘ₗ LinearMap.mul' R A)) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry counit) x✝¹) x✝
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Bialgebra R B
x✝ : B
⊢ ((AlgHom.restrictScalars R (counitAlgHom A (A ⊗[R] B))).comp Algebra.TensorProduct.includeRight) x✝ =
    ((Algebra.ofId R A).comp (counitAlgHom R B)) x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Bialgebra R B
x✝ : B
⊢ ((AlgHom.restrictScalars R (counitAlgHom A (A ⊗[R] B))).comp Algebra.TensorProduct.includeRight) x✝ =
    ((Algebra.ofId R A).comp (counitAlgHom R B)) x✝
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Bialgebra R B
inst✝ : Algebra R A
x : B
⊢ ((↑(comulAlgHom A (A ⊗[R] B))).comp ↑Algebra.TensorProduct.includeRight) x =
    ((Algebra.TensorProduct.mapRingHom (algebraMap R A) ↑Algebra.TensorProduct.includeRight
            ↑Algebra.TensorProduct.includeRight ⋯ ⋯).comp
        ↑(comulAlgHom R B))
      x

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : CommSemiring B
inst✝¹ : Bialgebra R B
inst✝ : Algebra R A
x : B
⊢ ((↑(comulAlgHom A (A ⊗[R] B))).comp ↑Algebra.TensorProduct.includeRight) x =
    ((Algebra.TensorProduct.mapRingHom (algebraMap R A) ↑Algebra.TensorProduct.includeRight
            ↑Algebra.TensorProduct.includeRight ⋯ ⋯).comp
        ↑(comulAlgHom R B))
      x