mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (ρ_ X₁).hom ⊗ₘ (ρ_ X₂).hom =
    (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫ X₁ ◁ (ρ_ (𝟙_ C ⊗ X₂)).hom ≫ X₁ ◁ (λ_ X₂).hom
⊢ (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫ X₁ ◁ (ρ_ (𝟙_ C ⊗ X₂)).hom ≫ X₁ ◁ (λ_ X₂).hom =
    ((α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫
        X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫
          X₁ ◁ (β_ (𝟙_ C) X₂).hom ▷ 𝟙_ C ≫ X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).hom ≫ (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).inv) ≫
      (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).hom ≫ (ρ_ (X₁ ⊗ X₂)).hom

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (ρ_ X₁).hom ⊗ₘ (ρ_ X₂).hom =
    (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫ X₁ ◁ (ρ_ (𝟙_ C ⊗ X₂)).hom ≫ X₁ ◁ (λ_ X₂).hom
⊢ (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫ X₁ ◁ (ρ_ (𝟙_ C ⊗ X₂)).hom ≫ X₁ ◁ (λ_ X₂).hom =
    ((α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫
        X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫
          X₁ ◁ (β_ (𝟙_ C) X₂).hom ▷ 𝟙_ C ≫ X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).hom ≫ (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).inv) ≫
      (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).hom ≫ (ρ_ (X₁ ⊗ X₂)).hom
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
⊢ ((α_ (X₁ ⊗ X₂) X₃ ((Y₁ ⊗ Y₂) ⊗ Y₃)).hom ≫
        (X₁ ⊗ X₂) ◁ (α_ X₃ (Y₁ ⊗ Y₂) Y₃).inv ≫
          (X₁ ⊗ X₂) ◁
              ((α_ X₃ Y₁ Y₂).inv ≫ (β_ X₃ Y₁).hom ▷ Y₂ ≫ (α_ Y₁ X₃ Y₂).hom ≫ Y₁ ◁ (β_ X₃ Y₂).hom ≫ (α_ Y₁ Y₂ X₃).inv) ▷
                Y₃ ≫
            (X₁ ⊗ X₂) ◁ (α_ (Y₁ ⊗ Y₂) X₃ Y₃).hom ≫ (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (X₃ ⊗ Y₃)).inv) ≫
      ((α_ X₁ X₂ (Y₁ ⊗ Y₂)).hom ≫
            X₁ ◁ (α_ X₂ Y₁ Y₂).inv ≫ X₁ ◁ (β_ X₂ Y₁).hom ▷ Y₂ ≫ X₁ ◁ (α_ Y₁ X₂ Y₂).hom ≫ (α_ X₁ Y₁ (X₂ ⊗ Y₂)).inv) ▷
          (X₃ ⊗ Y₃) ≫
        (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom =
    𝟙 (((X₁ ⊗ X₂) ⊗ X₃) ⊗ (Y₁ ⊗ Y₂) ⊗ Y₃) ⊗≫
      X₁ ◁ X₂ ◁ (β_ X₃ Y₁).hom ▷ Y₂ ▷ Y₃ ⊗≫
        X₁ ◁ ((X₂ ⊗ Y₁) ◁ (β_ X₃ Y₂).hom ≫ (β_ X₂ Y₁).hom ▷ (Y₂ ⊗ X₃)) ▷ Y₃ ⊗≫ 𝟙 ((X₁ ⊗ Y₁) ⊗ (X₂ ⊗ Y₂) ⊗ X₃ ⊗ Y₃)

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
⊢ ((α_ (X₁ ⊗ X₂) X₃ ((Y₁ ⊗ Y₂) ⊗ Y₃)).hom ≫
        (X₁ ⊗ X₂) ◁ (α_ X₃ (Y₁ ⊗ Y₂) Y₃).inv ≫
          (X₁ ⊗ X₂) ◁
              ((α_ X₃ Y₁ Y₂).inv ≫ (β_ X₃ Y₁).hom ▷ Y₂ ≫ (α_ Y₁ X₃ Y₂).hom ≫ Y₁ ◁ (β_ X₃ Y₂).hom ≫ (α_ Y₁ Y₂ X₃).inv) ▷
                Y₃ ≫
            (X₁ ⊗ X₂) ◁ (α_ (Y₁ ⊗ Y₂) X₃ Y₃).hom ≫ (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (X₃ ⊗ Y₃)).inv) ≫
      ((α_ X₁ X₂ (Y₁ ⊗ Y₂)).hom ≫
            X₁ ◁ (α_ X₂ Y₁ Y₂).inv ≫ X₁ ◁ (β_ X₂ Y₁).hom ▷ Y₂ ≫ X₁ ◁ (α_ Y₁ X₂ Y₂).hom ≫ (α_ X₁ Y₁ (X₂ ⊗ Y₂)).inv) ▷
          (X₃ ⊗ Y₃) ≫
        (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom =
    𝟙 (((X₁ ⊗ X₂) ⊗ X₃) ⊗ (Y₁ ⊗ Y₂) ⊗ Y₃) ⊗≫
      X₁ ◁ X₂ ◁ (β_ X₃ Y₁).hom ▷ Y₂ ▷ Y₃ ⊗≫
        X₁ ◁ ((X₂ ⊗ Y₁) ◁ (β_ X₃ Y₂).hom ≫ (β_ X₂ Y₁).hom ▷ (Y₂ ⊗ X₃)) ▷ Y₃ ⊗≫ 𝟙 ((X₁ ⊗ Y₁) ⊗ (X₂ ⊗ Y₂) ⊗ X₃ ⊗ Y₃)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
⊢ 𝟙 (((X₁ ⊗ X₂) ⊗ X₃) ⊗ (Y₁ ⊗ Y₂) ⊗ Y₃) ⊗≫
      X₁ ◁ X₂ ◁ (β_ X₃ Y₁).hom ▷ Y₂ ▷ Y₃ ⊗≫
        X₁ ◁ ((β_ X₂ Y₁).hom ▷ (X₃ ⊗ Y₂) ≫ (Y₁ ⊗ X₂) ◁ (β_ X₃ Y₂).hom) ▷ Y₃ ⊗≫ 𝟙 ((X₁ ⊗ Y₁) ⊗ (X₂ ⊗ Y₂) ⊗ X₃ ⊗ Y₃) =
    ((α_ X₁ X₂ X₃).hom ⊗ₘ (α_ Y₁ Y₂ Y₃).hom) ≫
      ((α_ X₁ (X₂ ⊗ X₃) (Y₁ ⊗ Y₂ ⊗ Y₃)).hom ≫
          X₁ ◁ (α_ (X₂ ⊗ X₃) Y₁ (Y₂ ⊗ Y₃)).inv ≫
            X₁ ◁
                ((α_ X₂ X₃ Y₁).hom ≫
                    X₂ ◁ (β_ X₃ Y₁).hom ≫ (α_ X₂ Y₁ X₃).inv ≫ (β_ X₂ Y₁).hom ▷ X₃ ≫ (α_ Y₁ X₂ X₃).hom) ▷
                  (Y₂ ⊗ Y₃) ≫
              X₁ ◁ (α_ Y₁ (X₂ ⊗ X₃) (Y₂ ⊗ Y₃)).hom ≫ (α_ X₁ Y₁ ((X₂ ⊗ X₃) ⊗ Y₂ ⊗ Y₃)).inv) ≫
        (X₁ ⊗ Y₁) ◁
          ((α_ X₂ X₃ (Y₂ ⊗ Y₃)).hom ≫
            X₂ ◁ (α_ X₃ Y₂ Y₃).inv ≫ X₂ ◁ (β_ X₃ Y₂).hom ▷ Y₃ ≫ X₂ ◁ (α_ Y₂ X₃ Y₃).hom ≫ (α_ X₂ Y₂ (X₃ ⊗ Y₃)).inv)

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
⊢ 𝟙 (((X₁ ⊗ X₂) ⊗ X₃) ⊗ (Y₁ ⊗ Y₂) ⊗ Y₃) ⊗≫
      X₁ ◁ X₂ ◁ (β_ X₃ Y₁).hom ▷ Y₂ ▷ Y₃ ⊗≫
        X₁ ◁ ((β_ X₂ Y₁).hom ▷ (X₃ ⊗ Y₂) ≫ (Y₁ ⊗ X₂) ◁ (β_ X₃ Y₂).hom) ▷ Y₃ ⊗≫ 𝟙 ((X₁ ⊗ Y₁) ⊗ (X₂ ⊗ Y₂) ⊗ X₃ ⊗ Y₃) =
    ((α_ X₁ X₂ X₃).hom ⊗ₘ (α_ Y₁ Y₂ Y₃).hom) ≫
      ((α_ X₁ (X₂ ⊗ X₃) (Y₁ ⊗ Y₂ ⊗ Y₃)).hom ≫
          X₁ ◁ (α_ (X₂ ⊗ X₃) Y₁ (Y₂ ⊗ Y₃)).inv ≫
            X₁ ◁
                ((α_ X₂ X₃ Y₁).hom ≫
                    X₂ ◁ (β_ X₃ Y₁).hom ≫ (α_ X₂ Y₁ X₃).inv ≫ (β_ X₂ Y₁).hom ▷ X₃ ≫ (α_ Y₁ X₂ X₃).hom) ▷
                  (Y₂ ⊗ Y₃) ≫
              X₁ ◁ (α_ Y₁ (X₂ ⊗ X₃) (Y₂ ⊗ Y₃)).hom ≫ (α_ X₁ Y₁ ((X₂ ⊗ X₃) ⊗ Y₂ ⊗ Y₃)).inv) ≫
        (X₁ ⊗ Y₁) ◁
          ((α_ X₂ X₃ (Y₂ ⊗ Y₃)).hom ≫
            X₂ ◁ (α_ X₃ Y₂ Y₃).inv ≫ X₂ ◁ (β_ X₃ Y₂).hom ▷ Y₃ ≫ X₂ ◁ (α_ Y₂ X₃ Y₃).hom ≫ (α_ X₂ Y₂ (X₃ ⊗ Y₃)).inv)
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: case mk.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d✝ c : RingCon M
d : RingCon N
e : M ≃+* N
h : c = d.comap e
x✝ : c.Quotient
x : M
y✝ : c.Quotient
y : M
⊢ (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) x * Quot.mk (⇑c.toSetoid) y) =
    (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) x) * (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) y)

Tactic:
;

Goal state after:
case mk.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d✝ c : RingCon M
d : RingCon N
e : M ≃+* N
h : c = d.comap e
x✝ : c.Quotient
x : M
y✝ : c.Quotient
y : M
⊢ (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) x * Quot.mk (⇑c.toSetoid) y) =
    (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) x) * (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) y)
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: case mk.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d✝ c : RingCon M
d : RingCon N
e : M ≃+* N
h : c = d.comap e
x✝ : c.Quotient
x : M
y✝ : c.Quotient
y : M
⊢ (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) x + Quot.mk (⇑c.toSetoid) y) =
    (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) x) + (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) y)

Tactic:
;

Goal state after:
case mk.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d✝ c : RingCon M
d : RingCon N
e : M ≃+* N
h : c = d.comap e
x✝ : c.Quotient
x : M
y✝ : c.Quotient
y : M
⊢ (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) x + Quot.mk (⇑c.toSetoid) y) =
    (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) x) + (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) y)
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
P : Type u_3
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring P
c : RingCon M
f : c.Quotient →+* P
x : c.Quotient
⊢ (c.lift (f.comp c.mk') ⋯) x = f x

Tactic:
;

Goal state after:
M : Type u_1
P : Type u_3
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring P
c : RingCon M
f : c.Quotient →+* P
x : c.Quotient
⊢ (c.lift (f.comp c.mk') ⋯) x = f x
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: case mk
M : Type u_1
P : Type u_3
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring P
c : RingCon M
f : c.Quotient →+* P
x : c.Quotient
a✝ : M
⊢ (c.lift (f.comp c.mk') ⋯) (Quot.mk (⇑c.toSetoid) a✝) = f (Quot.mk (⇑c.toSetoid) a✝)

Tactic:
;

Goal state after:
case mk
M : Type u_1
P : Type u_3
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring P
c : RingCon M
f : c.Quotient →+* P
x : c.Quotient
a✝ : M
⊢ (c.lift (f.comp c.mk') ⋯) (Quot.mk (⇑c.toSetoid) a✝) = f (Quot.mk (⇑c.toSetoid) a✝)
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ : RingCon M
f : M →+* P
c d : RingCon M
h : c ≤ d
x y : (ker (c.map d h)).Quotient
w z : c.Quotient
a b : M
⊢ (c.quotientQuotientEquivQuotient d.toSetoid h).toFun (↑↑a * ↑↑b) = d.mk' (a * b)

Tactic:
;

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ : RingCon M
f : M →+* P
c d : RingCon M
h : c ≤ d
x y : (ker (c.map d h)).Quotient
w z : c.Quotient
a b : M
⊢ (c.quotientQuotientEquivQuotient d.toSetoid h).toFun (↑↑a * ↑↑b) = d.mk' (a * b)
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ : RingCon M
f : M →+* P
c d : RingCon M
h : c ≤ d
x y : (ker (c.map d h)).Quotient
w z : c.Quotient
a b : M
⊢ (c.quotientQuotientEquivQuotient d.toSetoid h).toFun (↑↑a + ↑↑b) = d.mk' (a + b)

Tactic:
;

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ : RingCon M
f : M →+* P
c d : RingCon M
h : c ≤ d
x y : (ker (c.map d h)).Quotient
w z : c.Quotient
a b : M
⊢ (c.quotientQuotientEquivQuotient d.toSetoid h).toFun (↑↑a + ↑↑b) = d.mk' (a + b)
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : TensorAlgebra R M
hx : x ∈ ⊤
⊢ x ∈ Algebra.adjoin R (Set.range ⇑(ι R))

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : TensorAlgebra R M
hx : x ∈ ⊤
⊢ x ∈ Algebra.adjoin R (Set.range ⇑(ι R))
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
r : R
x : tsze R M
⊢ r •> x.snd + 0 <• x.fst = r •> x.snd

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
r : R
x : tsze R M
⊢ r •> x.snd + 0 <• x.fst = r •> x.snd
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
x : tsze R M
r : R
⊢ x.fst •> 0 + x.snd <• r = x.snd <• r

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
x : tsze R M
r : R
⊢ x.fst •> 0 + x.snd <• r = x.snd <• r
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
c : C
⊢ adj₁.unit.app c ≫ ((conjugateEquiv adj₁ adj₂) α).app (L₁.obj c) = adj₂.unit.app c ≫ R₂.map (α.app c)

Tactic:
dsimp [conjugateEquiv]

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
c : C
⊢ adj₁.unit.app c ≫
      𝟙 (R₁.obj (L₁.obj c)) ≫
        (𝟙 (R₁.obj (L₁.obj c)) ≫
            adj₂.unit.app (R₁.obj (L₁.obj c)) ≫
              𝟙 (R₂.obj (L₂.obj (R₁.obj (L₁.obj c)))) ≫
                𝟙 (R₂.obj (L₂.obj (R₁.obj (L₁.obj c)))) ≫
                  R₂.map (𝟙 (L₂.obj (R₁.obj (L₁.obj c))) ≫ α.app (R₁.obj (L₁.obj c)) ≫ 𝟙 (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                    𝟙 (R₂.obj (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                      𝟙 (R₂.obj (L₁.obj (R₁.obj (L₁.obj c)))) ≫
                        R₂.map (adj₁.counit.app (L₁.obj c)) ≫ 𝟙 (R₂.obj (L₁.obj c))) ≫
          𝟙 (R₂.obj (L₁.obj c)) =
    adj₂.unit.app c ≫ R₂.map (α.app c)
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x y z : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (x.1 * y.1) •> z.2 + (x.1 •> y.2 <• z.1 + x.2 <• y.1 <• z.1) =
    x.1 •> y.1 •> z.2 + x.1 •> (y.2 <• z.1) + x.2 <• (y.1 * z.1)

Tactic:
← mul_smul,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x y z : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (x.1 * y.1) •> z.2 + (x.1 •> y.2 <• z.1 + (op z.1 * op y.1) •> x.2) =
    (x.1 * y.1) •> z.2 + x.1 •> (y.2 <• z.1) + x.2 <• (y.1 * z.1)
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ (LinearMap.rTensor R LinearMap.id ∘ₗ (TensorProduct.mk R R R) 1) 1 = ((TensorProduct.mk R R R) 1) 1

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ (LinearMap.rTensor R LinearMap.id ∘ₗ (TensorProduct.mk R R R) 1) 1 = ((TensorProduct.mk R R R) 1) 1
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ (LinearMap.lTensor R LinearMap.id ∘ₗ (TensorProduct.mk R R R) 1) 1 = ((TensorProduct.mk R R R).flip 1) 1

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ (LinearMap.lTensor R LinearMap.id ∘ₗ (TensorProduct.mk R R R) 1) 1 = ((TensorProduct.mk R R R).flip 1) 1
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ (↑(TensorProduct.comm R R R) ∘ₗ comul) 1 = comul 1

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ (↑(TensorProduct.comm R R R) ∘ₗ comul) 1 = comul 1
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
F₁ : A ⥤ C
U₁ : C ⥤ A
F₂ : B ⥤ D
U₂ : D ⥤ B
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : F₁ ⊣ U₁
adj₄ : F₂ ⊣ U₂
α : TwoSquare F₁ L₁ L₂ F₂
⊢ ((mateEquiv adj₄ adj₃) ((mateEquiv adj₁ adj₂) α)).natTrans = (conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)) α

Tactic:
ext d
  simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : A
⊢ (comul ∘ₗ inl R A B) x✝ = (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul) x✝

Tactic:
;

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : A
⊢ (comul ∘ₗ inl R A B) x✝ = (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul) x✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : B
⊢ (comul ∘ₗ inr R A B) x✝ = (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul) x✝

Tactic:
;

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : B
⊢ (comul ∘ₗ inr R A B) x✝ = (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul) x✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : B
⊢ (counit ∘ₗ inr R A B) x✝ = counit x✝

Tactic:
;

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : B
⊢ (counit ∘ₗ inr R A B) x✝ = counit x✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : A
⊢ (counit ∘ₗ inl R A B) x✝ = counit x✝

Tactic:
;

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : A
⊢ (counit ∘ₗ inl R A B) x✝ = counit x✝
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : CoalgebraStruct R A
f g : R →ₗc[R] A
h : f 1 = g 1
⊢ ((fun x ↦ ↑x) f) 1 = ((fun x ↦ ↑x) g) 1

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : CoalgebraStruct R A
f g : R →ₗc[R] A
h : f 1 = g 1
⊢ ((fun x ↦ ↑x) f) 1 = ((fun x ↦ ↑x) g) 1
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
f : A →ₗc[R] B
f' : A → B
h : f' = ⇑f
x✝ : A
⊢ (counit ∘ₗ (↑f).copy f' h) x✝ = counit x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
f : A →ₗc[R] B
f' : A → B
h : f' = ⇑f
x✝ : A
⊢ (counit ∘ₗ (↑f).copy f' h) x✝ = counit x✝
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
x✝ : A
⊢ (counit ∘ₗ LinearMap.id) x✝ = counit x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
x✝ : A
⊢ (counit ∘ₗ LinearMap.id) x✝ = counit x✝
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
φ₁ : B →ₗc[R] C
φ₂ : A →ₗc[R] B
x✝ : A
⊢ (counit ∘ₗ ↑φ₁ ∘ₗ ↑φ₂) x✝ = counit x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
φ₁ : B →ₗc[R] C
φ₂ : A →ₗc[R] B
x✝ : A
⊢ (counit ∘ₗ ↑φ₁ ∘ₗ ↑φ₂) x✝ = counit x✝
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
φ₁ : B →ₗc[R] C
φ₂ : A →ₗc[R] B
x✝ : A
⊢ (map (↑φ₁ ∘ₗ ↑φ₂) (↑φ₁ ∘ₗ ↑φ₂) ∘ₗ comul) x✝ = (comul ∘ₗ ↑φ₁ ∘ₗ ↑φ₂) x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
φ₁ : B →ₗc[R] C
φ₂ : A →ₗc[R] B
x✝ : A
⊢ (map (↑φ₁ ∘ₗ ↑φ₂) (↑φ₁ ∘ₗ ↑φ₂) ∘ₗ comul) x✝ = (comul ∘ₗ ↑φ₁ ∘ₗ ↑φ₂) x✝
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u
A : Type v
B : Type w
ι : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : A
⊢ (counit ∘ₗ counit) x✝ = counit x✝

Tactic:
;

Goal state after:
R : Type u
A : Type v
B : Type w
ι : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : A
⊢ (counit ∘ₗ counit) x✝ = counit x✝
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u
A : Type v
B : Type w
ι : Type u_1
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Coalgebra R A
inst✝² : Coalgebra R B
a : A
repr : Repr R a ι
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
φ : F
⊢ (map ↑φ ↑φ) (comul a) = ∑ i ∈ repr.index, (⇑φ ∘ repr.left) i ⊗ₜ[R] (⇑φ ∘ repr.right) i

Tactic:
← repr.eq,

Goal state after:
R : Type u
A : Type v
B : Type w
ι : Type u_1
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Coalgebra R A
inst✝² : Coalgebra R B
a : A
repr : Repr R a ι
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
φ : F
⊢ (map ↑φ ↑φ) (∑ i ∈ repr.index, repr.left i ⊗ₜ[R] repr.right i) =
    ∑ i ∈ repr.index, (⇑φ ∘ repr.left) i ⊗ₜ[R] (⇑φ ∘ repr.right) i
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u
A : Type v
B : Type w
ι : Type u_1
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Coalgebra R A
inst✝² : Coalgebra R B
a : A
repr : Repr R a ι
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
φ : F
⊢ ∑ x ∈ repr.index, (map ↑φ ↑φ) (repr.left x ⊗ₜ[R] repr.right x) =
    ∑ i ∈ repr.index, (⇑φ ∘ repr.left) i ⊗ₜ[R] (⇑φ ∘ repr.right) i

Tactic:
;

Goal state after:
R : Type u
A : Type v
B : Type w
ι : Type u_1
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Coalgebra R A
inst✝² : Coalgebra R B
a : A
repr : Repr R a ι
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
φ : F
⊢ ∑ x ∈ repr.index, (map ↑φ ↑φ) (repr.left x ⊗ₜ[R] repr.right x) =
    ∑ i ∈ repr.index, (⇑φ ∘ repr.left) i ⊗ₜ[R] (⇑φ ∘ repr.right) i