mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝² x✝¹ x✝ : BialgCat R
⊢ ((AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (α_ x✝² x✝¹ x✝).hom)).comp
          Algebra.TensorProduct.includeLeft).comp
      Algebra.TensorProduct.includeLeft =
    ((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

Tactic:
ext

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
⊢ counit ∘ₗ ↑(_root_.TensorProduct.lid R P) = counit

Tactic:
ext

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
⊢ (AlgHom.restrictScalars R
          ((AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (α_ x✝² x✝¹ x✝).hom)).comp
            Algebra.TensorProduct.includeLeft)).comp
      Algebra.TensorProduct.includeRight =
    (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.includeLeft)).comp
      Algebra.TensorProduct.includeRight

Tactic:
ext

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.includeLeft)).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.includeLeft)).comp
        Algebra.TensorProduct.includeRight)
      x✝
Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝² x✝¹ x✝ : BialgCat R
⊢ (AlgHom.restrictScalars R (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (α_ x✝² x✝¹ x✝).hom))).comp
      Algebra.TensorProduct.includeRight =
    (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

Tactic:
ext

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
⊢ counit ∘ₗ ↑(AlgebraTensorModule.rid R S M) = counit

Tactic:
ext

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
⊢ (AlgHom.restrictScalars R (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (λ_ x✝).hom))).comp
      Algebra.TensorProduct.includeRight =
    (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

Tactic:
ext

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
⊢ (AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (ρ_ x✝).hom)).comp Algebra.TensorProduct.includeLeft =
    (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

Tactic:
ext

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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext

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.Algebra.Ring.BooleanRing

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

Tactic:
add_right_inj,

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ -b = b
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ⊔ (a ⊔ b ⊓ c) = a ⊔ b ⊓ c

Tactic:
by
  dsimp only [(· ⊔ ·), (· ⊓ ·)]
  rw [le_sup_inf_aux, add_self, mul_self, zero_add]

Goal state after:
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 : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
⊢ whiskerRight (adj1.rightAdjointUniq adj2).hom F ≫ adj2.counit = adj1.counit

Tactic:
ext

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 : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x✝ : D
⊢ (whiskerRight (adj1.rightAdjointUniq adj2).hom F ≫ adj2.counit).app x✝ = adj1.counit.app x✝
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: 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✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
⊢ (counitAlgHom R (B ⊗[R] A)).comp ↑(Algebra.TensorProduct.comm R A B) = counitAlgHom R (A ⊗[R] B)

Tactic:
ext

Goal state after:
case ha
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✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
x✝ : A
⊢ (((counitAlgHom R (B ⊗[R] A)).comp ↑(Algebra.TensorProduct.comm R A B)).comp Algebra.TensorProduct.includeLeft) x✝ =
    ((counitAlgHom R (A ⊗[R] B)).comp Algebra.TensorProduct.includeLeft) x✝

case hb
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✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
x✝ : B
⊢ ((AlgHom.restrictScalars R ((counitAlgHom R (B ⊗[R] A)).comp ↑(Algebra.TensorProduct.comm R A B))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R (counitAlgHom R (A ⊗[R] B))).comp Algebra.TensorProduct.includeRight) 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
⊢ (TensorProduct.comm R A A).toBialgHom.comp (comulBialgHom R A) = comulBialgHom R A

Tactic:
ext

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
⊢ counit ∘ₗ LinearMap.mul' R A = counit

Tactic:
ext

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
⊢ (AlgHom.restrictScalars R (counitAlgHom A (A ⊗[R] B))).comp Algebra.TensorProduct.includeRight =
    (Algebra.ofId R A).comp (counitAlgHom R B)

Tactic:
ext

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.Order.Category.Semilat

Goal state before:
pp: α β : SemilatSupCat
e : α.X ≃o β.X
⊢ { toFun := ⇑e, map_sup' := ⋯, map_bot' := ⋯ } ≫ { toFun := ⇑e.symm, map_sup' := ⋯, map_bot' := ⋯ } = 𝟙 α

Tactic:
ext

Goal state after:
α β : SemilatSupCat
e : α.X ≃o β.X
a✝ : α.X
⊢ (ConcreteCategory.hom
        ({ toFun := ⇑e, map_sup' := ⋯, map_bot' := ⋯ } ≫ { toFun := ⇑e.symm, map_sup' := ⋯, map_bot' := ⋯ }))
      a✝ =
    (ConcreteCategory.hom (𝟙 α)) a✝
Module: Mathlib.Order.Category.Semilat

Goal state before:
pp: α β : SemilatSupCat
e : α.X ≃o β.X
⊢ { toFun := ⇑e.symm, map_sup' := ⋯, map_bot' := ⋯ } ≫ { toFun := ⇑e, map_sup' := ⋯, map_bot' := ⋯ } = 𝟙 β

Tactic:
ext

Goal state after:
α β : SemilatSupCat
e : α.X ≃o β.X
a✝ : β.X
⊢ (ConcreteCategory.hom
        ({ toFun := ⇑e.symm, map_sup' := ⋯, map_bot' := ⋯ } ≫ { toFun := ⇑e, map_sup' := ⋯, map_bot' := ⋯ }))
      a✝ =
    (ConcreteCategory.hom (𝟙 β)) a✝
Module: Mathlib.Order.Category.Semilat

Goal state before:
pp: α β : SemilatInfCat
e : α.X ≃o β.X
⊢ { toFun := ⇑e, map_inf' := ⋯, map_top' := ⋯ } ≫ { toFun := ⇑e.symm, map_inf' := ⋯, map_top' := ⋯ } = 𝟙 α

Tactic:
ext

Goal state after:
α β : SemilatInfCat
e : α.X ≃o β.X
a✝ : α.X
⊢ (ConcreteCategory.hom
        ({ toFun := ⇑e, map_inf' := ⋯, map_top' := ⋯ } ≫ { toFun := ⇑e.symm, map_inf' := ⋯, map_top' := ⋯ }))
      a✝ =
    (ConcreteCategory.hom (𝟙 α)) a✝
Module: Mathlib.Order.Category.Semilat

Goal state before:
pp: α β : SemilatInfCat
e : α.X ≃o β.X
⊢ { toFun := ⇑e.symm, map_inf' := ⋯, map_top' := ⋯ } ≫ { toFun := ⇑e, map_inf' := ⋯, map_top' := ⋯ } = 𝟙 β

Tactic:
ext

Goal state after:
α β : SemilatInfCat
e : α.X ≃o β.X
a✝ : β.X
⊢ (ConcreteCategory.hom
        ({ toFun := ⇑e.symm, map_inf' := ⋯, map_top' := ⋯ } ≫ { toFun := ⇑e, map_inf' := ⋯, map_top' := ⋯ }))
      a✝ =
    (ConcreteCategory.hom (𝟙 β)) a✝
Module: Mathlib.Order.Category.BddOrd

Goal state before:
pp: α β : BddOrd
e : ↑α.toPartOrd ≃o ↑β.toPartOrd
⊢ ofHom ↑e ≫ ofHom ↑e.symm = 𝟙 α

Tactic:
ext

Goal state after:
α β : BddOrd
e : ↑α.toPartOrd ≃o ↑β.toPartOrd
a✝ : ↑α.toPartOrd
⊢ (Hom.hom (ofHom ↑e ≫ ofHom ↑e.symm)) a✝ = (Hom.hom (𝟙 α)) a✝
Module: Mathlib.Order.Category.BddOrd

Goal state before:
pp: α β : BddOrd
e : ↑α.toPartOrd ≃o ↑β.toPartOrd
⊢ ofHom ↑e.symm ≫ ofHom ↑e = 𝟙 β

Tactic:
ext

Goal state after:
α β : BddOrd
e : ↑α.toPartOrd ≃o ↑β.toPartOrd
a✝ : ↑β.toPartOrd
⊢ (Hom.hom (ofHom ↑e.symm ≫ ofHom ↑e)) a✝ = (Hom.hom (𝟙 β)) a✝
Module: Mathlib.Order.Category.BddLat

Goal state before:
pp: α β : BddLat
e : ↑α.toLat ≃o ↑β.toLat
⊢ ofHom
        (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫
      ofHom
        (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) =
    𝟙 α

Tactic:
ext

Goal state after:
α β : BddLat
e : ↑α.toLat ≃o ↑β.toLat
a✝ : ↑α.toLat
⊢ (Hom.hom
        (ofHom
            (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
            { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫
          ofHom
            (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
            { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })))
      a✝ =
    (Hom.hom (𝟙 α)) a✝