mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
L : D ⥤ C
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)))
        ((mateEquiv h h)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A))))).natTrans =
    (conjugateEquiv (h.comp (ihom.adjunction A)) ((ihom.adjunction (F.obj A)).comp h))
      (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A)))
B : C
⊢ h.unit.app (F.obj A ⊗ F.obj B) ≫
      F.map (prodComparison L (F.obj A) (F.obj B)) ≫ F.map (h.counit.app A ▷ L.obj (F.obj B) ≫ A ◁ h.counit.app B) =
    inv (prodComparison F A B)

Tactic:
← F.map_comp

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
L : D ⥤ C
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)))
        ((mateEquiv h h)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A))))).natTrans =
    (conjugateEquiv (h.comp (ihom.adjunction A)) ((ihom.adjunction (F.obj A)).comp h))
      (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A)))
B : C
⊢ h.unit.app (F.obj A ⊗ F.obj B) ≫
      F.map (prodComparison L (F.obj A) (F.obj B) ≫ h.counit.app A ▷ L.obj (F.obj B) ≫ A ◁ h.counit.app B) =
    inv (prodComparison F A B)
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j j' : J
φ : j ⟶ j'
⊢ uncurry
      (g.app j ≫
        precompEnrichedHom' C (Under.map φ) (Iso.refl (Under.map φ ⋙ Under.forget j ⋙ F₁))
            (Iso.refl (Under.map φ ⋙ Under.forget j ⋙ F₃)) ≫
          enrichedHomπ C (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃) (Under.mk (𝟙 j')) ≫
            (pre (F₁.map φ)).app (F₃.obj j')) =
    uncurry
      (g.app j ≫
        enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)) ≫ (ihom (F₁.obj j)).map (F₃.map φ))

Tactic:
end_.lift_π_assoc,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j j' : J
φ : j ⟶ j'
⊢ uncurry
      (g.app j ≫
        (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) ≫
            eHomWhiskerRight C ((Iso.refl (Under.map φ ⋙ Under.forget j ⋙ F₁)).inv.app (Under.mk (𝟙 j')))
                ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))) ≫
              eHomWhiskerLeft C ((Under.forget j' ⋙ F₁).obj (Under.mk (𝟙 j')))
                ((Iso.refl (Under.map φ ⋙ Under.forget j ⋙ F₃)).hom.app (Under.mk (𝟙 j')))) ≫
          (pre (F₁.map φ)).app (F₃.obj j')) =
    uncurry
      (g.app j ≫
        enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)) ≫ (ihom (F₁.obj j)).map (F₃.map φ))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
L : D ⥤ C
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
i :
  IsIso
    ((conjugateEquiv (h.comp (ihom.adjunction A)) ((ihom.adjunction (F.obj A)).comp h))
      (frobeniusMorphism F h A).natTrans)
⊢ IsIso (frobeniusMorphism F h A).natTrans

Tactic:
exact @conjugateEquiv_of_iso _ _ _ _ _ _ _ _ _ _ _ i

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
| X.X ◁ coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) ≫
    X.X ◁
      colimMap
        (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
          ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯)

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
| TensorBimod.actLeft M N₂

Tactic:
rw [← whiskerLeft_comp, ι_colimMap, parallelPairHom_app_one,
      whiskerLeft_comp]

Goal state after:
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
| X.X ◁ M.X ◁ f.hom ≫
    X.X ◁
      colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)) WalkingParallelPair.one

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
| TensorBimod.actLeft M N₂
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalClosed C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under j
⊢ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right) =
    end_.lift (fun k ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯ ≫
      end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k ≫
        (ρ_ (((diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)).obj (Opposite.op k)).obj k)).inv ≫
          ((diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)).obj (Opposite.op k)).obj k ◁
              ((Enriched.FunctorCategory.homEquiv C) f₃ ≫ precompEnrichedHom C F₃ F₃' (Under.forget j)) ≫
            ((diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)).obj (Opposite.op k)).obj k ◁
                end_.π (diagram C (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')) k ≫
              eComp C (Opposite.unop ((Under.forget j ⋙ F₁).op.obj (Opposite.op k))) ((Under.forget j ⋙ F₃).obj k)
                ((Under.forget j ⋙ F₃').obj k)

Tactic:
end_.lift_π_assoc,

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalClosed C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under j
⊢ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right) =
    (F₂.map k.hom ≫ curry (f.app k.right)) ≫
      (ρ_ (((diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)).obj (Opposite.op k)).obj k)).inv ≫
        ((diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)).obj (Opposite.op k)).obj k ◁
            ((Enriched.FunctorCategory.homEquiv C) f₃ ≫ precompEnrichedHom C F₃ F₃' (Under.forget j)) ≫
          ((diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)).obj (Opposite.op k)).obj k ◁
              end_.π (diagram C (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')) k ≫
            eComp C (Opposite.unop ((Under.forget j ⋙ F₁).op.obj (Opposite.op k))) ((Under.forget j ⋙ F₃).obj k)
              ((Under.forget j ⋙ F₃').obj k)
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: case h_snd
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ ((reflectorAdjunction i).unit.app A ⊗ₘ (reflectorAdjunction i).unit.app B) ≫
      snd (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)) =
    ((reflectorAdjunction i).unit.app (A ⊗ B) ≫
        i.map (prodComparison (reflector i) A B) ≫ prodComparison i ((reflector i).obj A) ((reflector i).obj B)) ≫
      snd (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))

Tactic:
tensorHom_snd,

Goal state after:
case h_snd
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ snd A B ≫ (reflectorAdjunction i).unit.app B =
    ((reflectorAdjunction i).unit.app (A ⊗ B) ≫
        i.map (prodComparison (reflector i) A B) ≫ prodComparison i ((reflector i).obj A) ((reflector i).obj B)) ≫
      snd (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory V
hasDayConvolution : ∀ (F G : C ⥤ V), (tensor C).HasPointwiseLeftKanExtension (F ⊠ G)
hasDayConvolutionUnit : (Functor.fromPUnit (𝟙_ C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (𝟙_ V))
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
F G : C ⊛⥤ V
x y : C
⊢ (F.η G).app (x, y) ≫ (F.isoPointwiseLeftKanExtension G).hom.app (x ⊗ y) =
    Limits.colimit.ι (CostructuredArrow.proj (tensor C) (x ⊗ y) ⋙ F.functor ⊠ G.functor)
      (CostructuredArrow.mk (𝟙 (x ⊗ y)))

Tactic:
by
  simpa [η, isoPointwiseLeftKanExtension] using!
    Functor.descOfIsLeftKanExtension_fac_app
      (F ⊗ G).functor (η F G) _
      ((tensor C).pointwiseLeftKanExtensionUnit (F.functor ⊠ G.functor)) (x, y)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hba
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
A B : C
inst✝² : HopfObj A
inst✝¹ : HopfObj B
f : A ⟶ B
inst✝ : IsBimonHom f
⊢ f ≫ ε ≫ η = ε ≫ η

Tactic:
slice_lhs 1 2 =>
      rw [IsComonHom.hom_counit]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasInitial C
inst✝ : HasBinaryCoproducts C
X Y Z : C
⊢ (α_ X Y Z).inv ≫ (coprod.braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv =
    X ◁ (coprod.braiding Y Z).hom ≫ (α_ X Z Y).inv ≫ (coprod.braiding X Z).hom ▷ Y

Tactic:
dsimp [monoidalOfHasFiniteCoproducts.associator_inv]; simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁶ : Category.{v₂, u₂} V
inst✝⁵ : MonoidalCategory C
inst✝⁴ : MonoidalCategory V
U : C ⥤ V
inst✝³ : DayConvolutionUnit U
F : C ⥤ V
inst✝² : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝¹ : DayConvolution F U
G : C ⥤ V
inst✝ : DayConvolution G U
f : F ⟶ G
⊢ DayConvolution.map f (𝟙 U) ≫ (rightUnitor U G).hom = (rightUnitor U F).hom ≫ f

Tactic:
apply Functor.hom_ext_of_isLeftKanExtension _ (DayConvolution.unit _ _) _
  apply Functor.hom_ext_of_isLeftKanExtension _ (extensionUnitRight U (φ U) F) _
  ext
  simp [whisker_exchange_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v : Arrow V
f g : u ⟶ v
x✝ : Nonempty (RightHomotopy f g)
h : RightHomotopy f g
⊢ (quotient V).map f = (quotient V).map g

Tactic:
simpa using eq_of_rightHomotopy _ _ h

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v : Arrow V
f : u ⟶ v
x✝ : Nonempty (RightHomotopy f 0)
h : RightHomotopy f 0
⊢ (quotient V).map f = 0

Tactic:
simpa using eq_of_rightHomotopy _ _ h

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)

Tactic:
have hd₁ : biprod.inl ≫ diag = biprod.lift f h := by ext <;> simp [diag]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon C
M : Bimod W X
N N' : Bimod X Y
f : N ⟶ N'
P : Bimod Y Z
⊢ (M.X ◁ f.hom ≫
          colimit.ι (parallelPair (M.actRight ▷ N'.X) ((α_ M.X X.X N'.X).hom ≫ M.X ◁ N'.actLeft))
            WalkingParallelPair.one) ▷
        P.X ≫
      colimit.ι
        (parallelPair (TensorBimod.actRight M N' ▷ P.X)
          ((α_ (TensorBimod.X M N') Y.X P.X).hom ≫ TensorBimod.X M N' ◁ P.actLeft))
        WalkingParallelPair.one =
    (α_ M.X N.X P.X).hom ≫
      M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫
        (M.X ◁
              colimMap
                (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N'.actRight ▷ P.X)
                  ((α_ N'.X Y.X P.X).hom ≫ N'.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯) ≫
            colimit.ι
              (parallelPair (M.actRight ▷ TensorBimod.X N' P)
                ((α_ M.X X.X (TensorBimod.X N' P)).hom ≫ M.X ◁ TensorBimod.actLeft N' P))
              WalkingParallelPair.one) ≫
          AssociatorBimod.inv M N' P

Tactic:
slice_rhs 2 3 => rw [← whiskerLeft_comp, ι_colimMap, parallelPairHom_app_one]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon C
M : Bimod W X
N N' : Bimod X Y
f : N ⟶ N'
P : Bimod Y Z
⊢ (M.X ◁ f.hom ≫
          colimit.ι (parallelPair (M.actRight ▷ N'.X) ((α_ M.X X.X N'.X).hom ≫ M.X ◁ N'.actLeft))
            WalkingParallelPair.one) ▷
        P.X ≫
      colimit.ι
        (parallelPair (TensorBimod.actRight M N' ▷ P.X)
          ((α_ (TensorBimod.X M N') Y.X P.X).hom ≫ TensorBimod.X M N' ◁ P.actLeft))
        WalkingParallelPair.one =
    (α_ M.X N.X P.X).hom ≫
      (M.X ◁
            (f.hom ▷ P.X ≫
              colimit.ι (parallelPair (N'.actRight ▷ P.X) ((α_ N'.X Y.X P.X).hom ≫ N'.X ◁ P.actLeft))
                WalkingParallelPair.one) ≫
          colimit.ι
            (parallelPair (M.actRight ▷ TensorBimod.X N' P)
              ((α_ M.X X.X (TensorBimod.X N' P)).hom ≫ M.X ◁ TensorBimod.actLeft N' P))
            WalkingParallelPair.one) ≫
        AssociatorBimod.inv M N' P
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
j : J
x y : ↑(F.1 j)
h : (ConcreteCategory.hom (c.ι.app j)) x = (ConcreteCategory.hom (c.ι.app j)) y
⊢ x = y

Tactic:
obtain ⟨k, a, ha⟩ := (Types.FilteredColimit.isColimit_eq_iff' hc x y).1 h

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
j : J
x y : ↑(F.1 j)
h : (ConcreteCategory.hom (c.ι.app j)) x = (ConcreteCategory.hom (c.ι.app j)) y
k : J
a : j ⟶ k
ha : (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map a)) x = (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map a)) y
⊢ x = y
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : Preadditive D
F : Mat_ C ⥤ D
inst✝ : F.Additive
M : Mat_ C
i : M.ι
⊢ F.map (biproduct.lift fun i j x ↦ if h : j = i then eqToHom ⋯ else 0) ≫
      (F.mapBicone (biproduct.bicone fun i ↦ (embedding C).obj (M.X i))).π i =
    F.map fun j x ↦ if h : j = i then eqToHom ⋯ else 0

Tactic:
← F.map_comp

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : Preadditive D
F : Mat_ C ⥤ D
inst✝ : F.Additive
M : Mat_ C
i : M.ι
⊢ F.map
      ((biproduct.lift fun i j x ↦ if h : j = i then eqToHom ⋯ else 0) ≫
        (biproduct.bicone fun i ↦ (embedding C).obj (M.X i)).π i) =
    F.map fun j x ↦ if h : j = i then eqToHom ⋯ else 0
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
⊢ IsCardinalPresentable J κ' ↔ HasCardinalLT (↑J.obj) κ'

Tactic:
refine ⟨fun _ ↦ ?_, fun hJ ↦ isCardinalPresentable_of_hasCardinalLT_of_le _ hJ h⟩
  obtain ⟨X, f, hf⟩ :=
    IsCardinalPresentable.exists_hom_of_isColimit κ' (isColimitCoconeWithTop J κ')
      (ObjectProperty.homMk (PartOrdEmb.ofHom WithTop.coeOrderHom))
  replace hf : OrderEmbedding.subtype (· ∈ X.1) ∘ f = WithTop.coeOrderHom := by
    ext x
    exact ConcreteCategory.congr_hom hf x
  refine X.2.1.of_injective f (Function.Injective.of_comp
    (f := OrderEmbedding.subtype (· ∈ X.1)) ?_)
  dsimp at hf ⊢
  rw [hf]
  exact WithTop.coe_injective

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m₀ : ι → J
t₀ : (i : ι) → (D i).top ⟶ m₀ i
hm₀ : ∀ (i : ι), IsEmpty (m₀ i ⟶ (D i).top)
⊢ ∃ m u,
    (∀ (i : ι), IsEmpty (m ⟶ (D i).top)) ∧
      ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
        (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂

Tactic:
let m₁ := IsCardinalFiltered.max m₀ hι

Goal state after:
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m₀ : ι → J
t₀ : (i : ι) → (D i).top ⟶ m₀ i
hm₀ : ∀ (i : ι), IsEmpty (m₀ i ⟶ (D i).top)
m₁ : J := max m₀ hι
⊢ ∃ m u,
    (∀ (i : ι), IsEmpty (m ⟶ (D i).top)) ∧
      ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
        (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison

Goal state before:
pp: case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : Preregular C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
x✝¹ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w✝ : EffectiveEpi g
g' : Y ⟶ ∐ X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : α → C := fun a ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun a ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun a ↦ pullback.fst g' (Sigma.ι X₁ a)
x✝ : IsIso (Sigma.desc fun x ↦ pullback.fst g' (Sigma.ι X₁ x))
⊢ ∃ i ι, ∀ (b : α), ι b ≫ π₁ (i b) = π₂ b ≫ f

Tactic:
refine ⟨id, fun b ↦ pullback.snd _ _, fun b ↦ ?_⟩

Goal state after:
case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : Preregular C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
x✝¹ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w✝ : EffectiveEpi g
g' : Y ⟶ ∐ X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : α → C := fun a ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun a ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun a ↦ pullback.fst g' (Sigma.ι X₁ a)
x✝ : IsIso (Sigma.desc fun x ↦ pullback.fst g' (Sigma.ι X₁ x))
b : α
⊢ (fun b ↦ pullback.snd g' (Sigma.ι X₁ b)) b ≫ π₁ (id b) = π₂ b ≫ f
Module: Mathlib.CategoryTheory.Sites.EpiMono

Goal state before:
pp: case mpr
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁷ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasFunctorialSurjectiveInjectiveFactorization A
inst✝³ : J.WEqualsLocallyBijective A
inst✝² : HasSheafify J A
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : Balanced (Sheaf J A)
F G : Sheaf J A
φ : F ⟶ G
⊢ Epi φ → IsLocallySurjective φ

Tactic:
intro
    let data := (locallySurjective J A).factorizationData (locallyInjective J A) φ
    have : IsLocallySurjective data.i := data.hi
    have : IsLocallyInjective data.p := data.hp
    have : Epi data.p := epi_of_epi_fac data.fac
    have := mono_of_isLocallyInjective data.p
    have := isIso_of_mono_of_epi data.p
    rw [← data.fac]
    infer_instance

Goal state after: