mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: case refine_2.refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s✝ : Cone F
⊢ ∀ (x y : ↑s✝.1),
    (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝)))
        (x * y) =
      (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝))) x *
        (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝))) y

Tactic:
intro x y

Goal state after:
case refine_2.refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s✝ : Cone F
x y : ↑s✝.1
⊢ (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝)))
      (x * y) =
    (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝))) x *
      (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝))) y
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: case refine_1
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
s : Cone F
⊢ ∀ (x y : ↑s.1),
    (ConcreteCategory.hom
          ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s)))
        (x + y) =
      (ConcreteCategory.hom
            ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s)))
          x +
        (ConcreteCategory.hom
            ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s)))
          y

Tactic:
intro x y

Goal state after:
case refine_1
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
s : Cone F
x y : ↑s.1
⊢ (ConcreteCategory.hom
        ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s)))
      (x + y) =
    (ConcreteCategory.hom
          ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s)))
        x +
      (ConcreteCategory.hom
          ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s)))
        y
Module: Mathlib.Algebra.Category.AlgCat.Limits

Goal state before:
pp: case refine_2
R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
s : Cone F
⊢ ∀ (x y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) (x * y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) x, ⋯⟩ *
        EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) y, ⋯⟩

Tactic:
intro x y

Goal state after:
case refine_2
R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
s : Cone F
x y : ↑s.1
⊢ EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
      ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) (x * y), ⋯⟩ =
    EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) x, ⋯⟩ *
      EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) y, ⋯⟩
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
s : Cocone (directLimitDiagram G f)
i : ι
x✝ : ↑((directLimitDiagram G f).obj i)
⊢ (Hom.hom ((directLimitCocone G f).ι.app i ≫ ↟(Module.DirectLimit.lift R ι G f (fun i ↦ Hom.hom (s.ι.app i)) ⋯))) x✝ =
    (Hom.hom (s.ι.app i)) x✝

Tactic:
dsimp only [hom_comp, directLimitCocone, hom_ofHom, LinearMap.comp_apply]

Goal state after:
R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
s : Cocone (directLimitDiagram G f)
i : ι
x✝ : ↑((directLimitDiagram G f).obj i)
⊢ (Module.DirectLimit.lift R ι G f (fun i ↦ Hom.hom (s.ι.app i)) ⋯) ((DirectLimit.of R ι G f i) x✝) =
    (Hom.hom (s.ι.app i)) x✝
Module: Mathlib.Algebra.Category.AlgCat.Limits

Goal state before:
pp: case refine_4
R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
s : Cone F
⊢ ∀ (x y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) (x + y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) x, ⋯⟩ +
        EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) y, ⋯⟩

Tactic:
intro x y

Goal state after:
case refine_4
R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
s : Cone F
x y : ↑s.1
⊢ EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
      ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) (x + y), ⋯⟩ =
    EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) x, ⋯⟩ +
      EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) y, ⋯⟩
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ GrpCat
a : (j : J) → ↑(F.obj j)
ah : ∀ {j j' : J} (f : j ⟶ j'), (ConcreteCategory.hom (F.map f)) (a j) = a j'
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (F.map f)) (a j)⁻¹ = (a j')⁻¹

Tactic:
(F.map f).hom.map_inv (a j),

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ GrpCat
a : (j : J) → ↑(F.obj j)
ah : ∀ {j j' : J} (f : j ⟶ j'), (ConcreteCategory.hom (F.map f)) (a j) = a j'
j j' : J
f : j ⟶ j'
⊢ ((Hom.hom (F.map f)) (a j))⁻¹ = (a j')⁻¹
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : D), IsSplitMono (h.counit.app X)
X Y : D
f : R.obj X ⟶ R.obj Y
⊢ R.map (retraction (h.counit.app X) ≫ (h.homEquiv (R.obj X) Y).symm f) = f

Tactic:
suffices R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X) by simp [this]

Goal state after:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : D), IsSplitMono (h.counit.app X)
X Y : D
f : R.obj X ⟶ R.obj Y
⊢ R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X)
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (λ_ X).hom ▷ Y = (α_ (𝟙_ C) X Y).hom ≫ (λ_ (X ⊗ Y)).hom

Tactic:
← whiskerLeft_iff,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ 𝟙_ C ◁ (λ_ X).hom ▷ Y = 𝟙_ C ◁ ((α_ (𝟙_ C) X Y).hom ≫ (λ_ (X ⊗ Y)).hom)
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: case refine_2
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
⊢ ∀ (x y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) (x * y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) x, ⋯⟩ *
        EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) y, ⋯⟩

Tactic:
intro x y

Goal state after:
case refine_2
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
x y : ↑s.1
⊢ EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
      ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) (x * y), ⋯⟩ =
    EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) x, ⋯⟩ *
      EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) y, ⋯⟩
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: case refine_4
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
⊢ ∀ (x y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) (x + y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) x, ⋯⟩ +
        EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) y, ⋯⟩

Tactic:
intro x y

Goal state after:
case refine_4
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
x y : ↑s.1
⊢ EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
      ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) (x + y), ⋯⟩ =
    EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) x, ⋯⟩ +
      EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) y, ⋯⟩
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ (biproduct.ι (fun j ↦ X ⊗ f j) j✝ ≫ biproduct.desc fun j ↦ X ◁ biproduct.ι f j) =
    biproduct.ι (fun j ↦ X ⊗ f j) j✝ ≫ ∑ j, biproduct.π (fun j ↦ X ⊗ f j) j ≫ X ◁ biproduct.ι f j

Tactic:
simp only [Preadditive.comp_sum, biproduct.ι_π_assoc, dite_comp, zero_comp,
    Finset.sum_dite_eq, Finset.mem_univ, ite_true, eqToHom_refl, Category.id_comp,
    biproduct.ι_desc]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.MonoidalComp

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ⊗≫ g = f ≫ g

Tactic:
simp [monoidalComp]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
⊢ ∀ (x : ↑M) (y : ↑(of R R)) (z : ↑N),
    (Hom.hom ((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom)) (x ⊗ₜ[R] y ⊗ₜ[R] z) =
      (Hom.hom (tensorHom (rightUnitor M).hom (𝟙 N))) (x ⊗ₜ[R] y ⊗ₜ[R] z)

Tactic:
intro x y

Goal state after:
R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
x : ↑M
y : ↑(of R R)
⊢ ∀ (z : ↑N),
    (Hom.hom ((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom)) (x ⊗ₜ[R] y ⊗ₜ[R] z) =
      (Hom.hom (tensorHom (rightUnitor M).hom (𝟙 N))) (x ⊗ₜ[R] y ⊗ₜ[R] z)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case η
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toOplaxMonoidal = b.toOplaxMonoidal
⊢ η F = η F

Tactic:
exact congr(($eq).η)

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X₁ X₂ Y₁ Y₂ : SemimoduleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ ∀ (x : ↑X₁) (y : ↑X₂),
    (Hom.hom ((f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom)) (x ⊗ₜ[R] y) = (Hom.hom ((X₁.braiding X₂).hom ≫ (g ⊗ₘ f))) (x ⊗ₜ[R] y)

Tactic:
intro x y

Goal state after:
R : Type u
inst✝ : CommSemiring R
X₁ X₂ Y₁ Y₂ : SemimoduleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
x : ↑X₁
y : ↑X₂
⊢ (Hom.hom ((f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom)) (x ⊗ₜ[R] y) = (Hom.hom ((X₁.braiding X₂).hom ≫ (g ⊗ₘ f))) (x ⊗ₜ[R] y)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y Z : D
⊢ F.map (adj.unit.app (G.obj X ⊗ G.obj Y) ▷ G.obj Z) ≫
      F.map (G.map (δ F (G.obj X) (G.obj Y)) ▷ G.obj Z) ≫
        F.map (G.map (adj.counit.app X ⊗ₘ adj.counit.app Y) ▷ G.obj Z) ≫
          δ F (G.obj (X ⊗ Y)) (G.obj Z) ≫ (adj.counit.app (X ⊗ Y) ⊗ₘ adj.counit.app Z) ≫ (α_ X Y Z).hom =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      F.map (G.obj X ◁ adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (Y ⊗ Z)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (Y ⊗ Z))

Tactic:
← δ_natural_left_assoc,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y Z : D
⊢ F.map (adj.unit.app (G.obj X ⊗ G.obj Y) ▷ G.obj Z) ≫
      F.map (G.map (δ F (G.obj X) (G.obj Y)) ▷ G.obj Z) ≫
        δ F (G.obj (F.obj (G.obj X) ⊗ F.obj (G.obj Y))) (G.obj Z) ≫
          F.map (G.map (adj.counit.app X ⊗ₘ adj.counit.app Y)) ▷ F.obj (G.obj Z) ≫
            (adj.counit.app (X ⊗ Y) ⊗ₘ adj.counit.app Z) ≫ (α_ X Y Z).hom =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      F.map (G.obj X ◁ adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (Y ⊗ Z)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (Y ⊗ Z))
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y Z : D
⊢ F.map (adj.unit.app (G.obj X ⊗ G.obj Y) ▷ G.obj Z) ≫
      F.map (G.map (δ F (G.obj X) (G.obj Y)) ▷ G.obj Z) ≫
        δ F (G.obj (F.obj (G.obj X) ⊗ F.obj (G.obj Y))) (G.obj Z) ≫
          F.map (G.map (adj.counit.app X ⊗ₘ adj.counit.app Y)) ▷ F.obj (G.obj Z) ≫
            (adj.counit.app (X ⊗ Y) ⊗ₘ adj.counit.app Z) ≫ (α_ X Y Z).hom =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      F.map (G.obj X ◁ adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (Y ⊗ Z)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (Y ⊗ Z))

Tactic:
← δ_natural_left_assoc,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y Z : D
⊢ F.map (adj.unit.app (G.obj X ⊗ G.obj Y) ▷ G.obj Z) ≫
      δ F (G.obj (F.obj (G.obj X ⊗ G.obj Y))) (G.obj Z) ≫
        F.map (G.map (δ F (G.obj X) (G.obj Y))) ▷ F.obj (G.obj Z) ≫
          F.map (G.map (adj.counit.app X ⊗ₘ adj.counit.app Y)) ▷ F.obj (G.obj Z) ≫
            (adj.counit.app (X ⊗ Y) ⊗ₘ adj.counit.app Z) ≫ (α_ X Y Z).hom =
    F.map (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      F.map (G.obj X ◁ adj.unit.app (G.obj Y ⊗ G.obj Z)) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (Y ⊗ Z)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (Y ⊗ Z))
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝² : HasPushout f g
inst✝¹ : HasPushout (G.map f) (G.map g)
inst✝ : PreservesColimit (span f g) G
⊢ IsIso (pushoutComparison G f g)

Tactic:
← PreservesPushout.iso_hom

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝² : HasPushout f g
inst✝¹ : HasPushout (G.map f) (G.map g)
inst✝ : PreservesColimit (span f g) G
⊢ IsIso (PreservesPushout.iso G f g).hom
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    F.map (adj.unit.app (𝟙_ C) ▷ G.obj X) ≫
      F.map (G.map (η F) ▷ G.obj X) ≫
        δ F (G.obj (𝟙_ D)) (G.obj X) ≫ (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X) ≫ (λ_ X).hom

Tactic:
← δ_natural_left_assoc,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    F.map (adj.unit.app (𝟙_ C) ▷ G.obj X) ≫
      δ F ((F ⋙ G).obj (𝟙_ C)) (G.obj X) ≫
        F.map (G.map (η F)) ▷ F.obj (G.obj X) ≫ (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X) ≫ (λ_ X).hom
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    F.map (adj.unit.app (𝟙_ C) ▷ G.obj X) ≫
      δ F ((F ⋙ G).obj (𝟙_ C)) (G.obj X) ≫
        F.map (G.map (η F)) ▷ F.obj (G.obj X) ≫ (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X) ≫ (λ_ X).hom

Tactic:
← δ_natural_left_assoc,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    δ F (𝟙_ C) (G.obj X) ≫
      F.map (adj.unit.app (𝟙_ C)) ▷ F.obj (G.obj X) ≫
        F.map (G.map (η F)) ▷ F.obj (G.obj X) ≫ (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X) ≫ (λ_ X).hom
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case comp_of
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsMultiplicative
X✝ Y✝ : C
f✝¹ : X✝ ⟶ Y✝
x✝ y✝ z✝ : C
f✝ : x✝ ⟶ y✝
g✝ : y✝ ⟶ z✝
hf✝ : W.multiplicativeClosure f✝
hg : W g✝
hf : W f✝
⊢ W (f✝ ≫ g✝)

Tactic:
exact W.comp_mem _ _ hf hg

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

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
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
Z✝ : C
⊢ μ F X✝ Z✝ ≫ F.map (f✝ ▷ Z✝) ≫ F.map (β Y✝ Z✝).hom = μ F X✝ Z✝ ≫ F.map ((β X✝ Z✝).hom ≫ Z✝ ◁ f✝)

Tactic:
← μ_natural_left_assoc,

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
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
Z✝ : C
⊢ F.map f✝ ▷ F.obj Z✝ ≫ μ F Y✝ Z✝ ≫ F.map (β Y✝ Z✝).hom = μ F X✝ Z✝ ≫ F.map ((β X✝ Z✝).hom ≫ Z✝ ◁ f✝)
Module: Mathlib.Algebra.Category.ModuleCat.EpiMono

Goal state before:
pp: R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f✝ : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
hf : Mono f
⊢ Mono ((forget (ModuleCat R)).map f)

Tactic:
CategoryTheory.ofHom_mono_iff_injective,

Goal state after:
R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f✝ : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
hf : Mono f
⊢ Function.Injective ⇑(ConcreteCategory.hom f)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| (adj.unit.app (X ⊗ Y) ⊗ₘ adj.unit.app Z) ≫
    μ G (F.obj (X ⊗ Y)) (F.obj Z) ≫
      G.map
        ((F.map ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y)) ≫ adj.counit.app (F.obj X ⊗ F.obj Y)) ▷
            F.obj Z ≫
          (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom)

Tactic:
map_comp_assoc,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| (adj.unit.app (X ⊗ Y) ⊗ₘ adj.unit.app Z) ≫
    μ G (F.obj (X ⊗ Y)) (F.obj Z) ≫
      G.map
        ((F.map (adj.unit.app X ⊗ₘ adj.unit.app Y) ≫
              F.map (μ G (F.obj X) (F.obj Y)) ≫ adj.counit.app (F.obj X ⊗ F.obj Y)) ▷
            F.obj Z ≫
          (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom)