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

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
⊢ _root_.TensorProduct.map ↑(_root_.TensorProduct.lid R P) ↑(_root_.TensorProduct.lid R P) ∘ₗ comul =
    comul ∘ₗ ↑(_root_.TensorProduct.lid R P)

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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
⊢ _root_.TensorProduct.map ↑(AlgebraTensorModule.rid R S M) ↑(AlgebraTensorModule.rid R S M) ∘ₗ comul =
    comul ∘ₗ ↑(AlgebraTensorModule.rid R S M)

Tactic:
by

Goal state after:
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:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : BooleanRing α
a✝ b✝ a b : α
⊢ a * b = b * a

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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 F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ (adj1.homEquiv x (F'.obj x)) ((adj1.leftAdjointUniq adj2).hom.app x) = adj2.unit.app x

Tactic:
by

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 F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
⊢ adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G = adj2.unit

Tactic:
by

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 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) = adj2.unit.app x

Tactic:
by

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 F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
⊢ G.whiskerLeft (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit = adj1.counit

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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 F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ (adj1.leftAdjointUniq adj2).hom.app (G.obj x) ≫ adj2.counit.app x = adj1.counit.app x

Tactic:
by

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

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

Tactic:
by

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 F' F'' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
⊢ (adj1.leftAdjointUniq adj2).hom ≫ (adj2.leftAdjointUniq adj3).hom = (adj1.leftAdjointUniq adj3).hom

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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 F' F'' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
x : C
⊢ (adj1.leftAdjointUniq adj2).hom.app x ≫ (adj2.leftAdjointUniq adj3).hom.app x = (adj1.leftAdjointUniq adj3).hom.app x

Tactic:
by

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

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

Tactic:
by

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 : D ⥤ C
adj1 : F ⊣ G
⊢ (adj1.leftAdjointUniq adj1).hom = 𝟙 F

Tactic:
by

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'
x : D
⊢ (adj2.homEquiv (G.obj x) x).symm ((adj1.rightAdjointUniq adj2).hom.app x) = adj1.counit.app x

Tactic:
by

Goal state after:
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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a : α
⊢ 1 ≤ a ⊔ (1 + a)

Tactic:
by

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'
x : C
⊢ adj1.unit.app x ≫ (adj1.rightAdjointUniq adj2).hom.app (F.obj x) = adj2.unit.app x

Tactic:
by

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'
⊢ adj1.unit ≫ F.whiskerLeft (adj1.rightAdjointUniq adj2).hom = adj2.unit

Tactic:
by

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'
x : D
⊢ F.map ((adj1.rightAdjointUniq adj2).hom.app x) ≫ adj2.counit.app x = adj1.counit.app x

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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:
by

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

Tactic:
by

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

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

Tactic:
by

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' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x : D
⊢ (adj1.rightAdjointUniq adj2).hom.app x ≫ (adj2.rightAdjointUniq adj3).hom.app x =
    (adj1.rightAdjointUniq adj3).hom.app x

Tactic:
by

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 : D ⥤ C
adj1 : F ⊣ G
⊢ (adj1.rightAdjointUniq adj1).hom = 𝟙 G

Tactic:
by

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

Goal state before:
pp: X Y Z : Pointed
f : X.Hom Y
g : Y.Hom Z
⊢ (g.toFun ∘ f.toFun) X.point = Z.point

Tactic:
by

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

Goal state before:
pp: X✝ Y✝ Z✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { toFun := Option.map ⇑(ConcreteCategory.hom (x✝¹ ≫ x✝)), map_point := ⋯ }.toFun =
    ({ toFun := Option.map ⇑(ConcreteCategory.hom x✝¹), map_point := ⋯ } ≫
        { toFun := Option.map ⇑(ConcreteCategory.hom x✝), map_point := ⋯ }).toFun

Tactic:
by

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

Goal state before:
pp: X : Type ?u.36
Y : Pointed
f : typeToPointed.obj X ⟶ Y
⊢ (fun f ↦ { toFun := fun o ↦ Option.elim o Y.point ⇑(ConcreteCategory.hom f), map_point := ⋯ })
      ((fun f ↦ ↾(f.toFun ∘ some)) f) =
    f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
f : α →+* β
a b : AsBoolAlg α
⊢ (⇑toBoolAlg ∘ ⇑f ∘ ⇑ofBoolAlg) (a ⊔ b) = (⇑toBoolAlg ∘ ⇑f ∘ ⇑ofBoolAlg) a ⊔ (⇑toBoolAlg ∘ ⇑f ∘ ⇑ofBoolAlg) b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
a : Bool
⊢ a * 0 = 0

Tactic:
by

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

Goal state before:
pp: X'✝ X✝ : Type ?u.36
Y✝ : Pointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget Pointed).obj Y✝
⊢ { toFun := fun f ↦ ↾(f.toFun ∘ some),
          invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
          left_inv := ⋯, right_inv := ⋯ }.symm
      (f ≫ g) =
    typeToPointed.map f ≫
      { toFun := fun f ↦ ↾(f.toFun ∘ some),
            invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.point ⇑(ConcreteCategory.hom f), map_point := ⋯ },
            left_inv := ⋯, right_inv := ⋯ }.symm
        g

Tactic:
by

Goal state after:
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 S A
inst✝³ : Bialgebra R B
inst✝² : Algebra R A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
⊢ Bialgebra S (A ⊗[R] B)

Tactic:
by

Goal state after:
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 S A
inst✝⁹ : Bialgebra R B
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra R S
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Bialgebra S C
inst✝² : Bialgebra R D
inst✝¹ : Algebra R C
inst✝ : IsScalarTower R S C
x y : A ⊗[R] R
⊢ (Coalgebra.TensorProduct.rid R S A).toFun (x * y) =
    (Coalgebra.TensorProduct.rid R S A).toFun x * (Coalgebra.TensorProduct.rid R S A).toFun y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Bialgebra S A
inst✝² : Algebra R A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
⊢ (TensorProduct.rid R S A).toAlgEquiv = Algebra.TensorProduct.rid R S A

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: X Y Z : Bipointed
f : X.Hom Y
g : Y.Hom Z
⊢ (g.toFun ∘ f.toFun) X.toProd.1 = Z.toProd.1

Tactic:
by

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

Goal state before:
pp: X Y Z : Bipointed
f : X.Hom Y
g : Y.Hom Z
⊢ (g.toFun ∘ f.toFun) X.toProd.2 = Z.toProd.2

Tactic:
by

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

Goal state before:
pp: X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
⊢ (fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ })
      ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f) =
    f

Tactic:
by

Goal state after: