mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u₁
inst✝¹ : Category.{v₁, u₁} A
inst✝ : HasProducts A
J : Type w
f : J → FormalCoproduct C
F✝ F : Cᵒᵖ ⥤ A
x : Cᵒᵖ
⊢ (Pi.π (fun i ↦ F.obj (op ((unop ((incl C).op.obj x)).obj i))) PUnit.unit ≫
      Pi.lift fun x_1 ↦ 𝟙 (((𝟭 (Cᵒᵖ ⥤ A)).obj F).obj x)) =
    𝟙 (((evalOp C A ⋙ (whiskeringLeft Cᵒᵖ (FormalCoproduct C)ᵒᵖ A).obj (incl C).op).obj F).obj x)

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.PiProd

Goal state before:
pp: C : Type u_1
I : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i ↦ X ↑i
inst✝³ : HasProduct fun i ↦ X ↑i
inst✝² : HasProduct fun i ↦ Y ↑i
inst✝¹ : HasProduct fun i ↦ Y ↑i
inst✝ : (i : I) → Decidable (P i)
⊢ ∀ (s : BinaryFan (∏ᶜ fun i ↦ X ↑i) (∏ᶜ fun i ↦ X ↑i)),
    ((lift fun b ↦
          if h : P b then s.π.app { as := WalkingPair.left } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩
          else s.π.app { as := WalkingPair.right } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩) ≫
        map' Subtype.val fun x ↦ 𝟙 (X ↑x)) =
      s.fst

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.PiProd

Goal state before:
pp: C : Type u_1
I : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i ↦ X ↑i
inst✝³ : HasProduct fun i ↦ X ↑i
inst✝² : HasProduct fun i ↦ Y ↑i
inst✝¹ : HasProduct fun i ↦ Y ↑i
inst✝ : (i : I) → Decidable (P i)
⊢ ∀ (s : BinaryFan (∏ᶜ fun i ↦ X ↑i) (∏ᶜ fun i ↦ X ↑i)),
    ((lift fun b ↦
          if h : P b then s.π.app { as := WalkingPair.left } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩
          else s.π.app { as := WalkingPair.right } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩) ≫
        map' Subtype.val fun x ↦ 𝟙 (X ↑x)) =
      s.snd

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
a : C
z w : (F ⨯ G).obj a
h1 : (hom (Limits.prod.fst.app a)) z = (hom (Limits.prod.fst.app a)) w
h2 : (hom (Limits.prod.snd.app a)) z = (hom (Limits.prod.snd.app a)) w
⊢ (binaryProductEquiv F G a) z = (binaryProductEquiv F G a) w

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
⊢ Limits.coprod.inl ≫ (colimit.isoColimitCocone (binaryCoproductColimitCocone F G)).hom = coprod.inl

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
⊢ (binaryCoproductColimitCocone F G).cocone.ι.app { as := WalkingPair.right } = coprod.inr

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout b.fst b.snd 0 0

Tactic:
by
  refine IsPushout.of_left ?_ (by simp) (IsPushout.inl_snd' h)
  simp

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

Goal state before:
pp: case mk
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ : X ⟶ Y
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quot.map (fun f ↦ f.whiskerRight unit) ⋯ (Quot.mk (⇑(X.setoidHom Y)) f) ≫
      { hom := ⟦Hom.ρ_hom Y⟧, inv := ⟦Hom.ρ_inv Y⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom =
    { hom := ⟦Hom.ρ_hom X⟧, inv := ⟦Hom.ρ_inv X⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫ Quot.mk (⇑(X.setoidHom Y)) f

Tactic:
exact Quotient.sound (ρ_naturality _)

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

Goal state before:
pp: case f
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f : C → D
X✝ Y✝ x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (project f).map ⟦a✝⟧ ▷ (project f).obj x✝ ≫ (Iso.refl ((project f).obj Y✝ ⊗ (project f).obj x✝)).hom =
    (Iso.refl ((project f).obj X✝ ⊗ (project f).obj x✝)).hom ≫ (project f).map (⟦a✝⟧ ▷ x✝)

Tactic:
aesop

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

Goal state before:
pp: case h
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X✝ Y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X✝ ⟶ Y✝
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝ b✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
p✝ : a✝ ≈ b✝
⊢ ⋯ = ⋯

Tactic:
aesop

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

Goal state before:
pp: case f
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f : C → D
X✝ Y✝ x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (project f).obj x✝ ◁ (project f).map ⟦a✝⟧ ≫ (Iso.refl ((project f).obj x✝ ⊗ (project f).obj Y✝)).hom =
    (Iso.refl ((project f).obj x✝ ⊗ (project f).obj X✝)).hom ≫ (project f).map (x✝ ◁ ⟦a✝⟧)

Tactic:
aesop

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

Goal state before:
pp: case h
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X✝ Y✝ x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X✝ ⟶ Y✝
a✝ b✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
p✝ : a✝ ≈ b✝
⊢ ⋯ = ⋯

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
⊢ ∀ (X : adj.toMonad.Algebra) (Y Y' : D) (g : Y ⟶ Y') (h : comparisonLeftAdjointObj adj X ⟶ Y),
    (comparisonLeftAdjointHomEquiv adj X Y') (h ≫ g) =
      (comparisonLeftAdjointHomEquiv adj X Y) h ≫ (comparison adj).map g

Tactic:
· intro A B B' g h
    ext1
    simp [Cofork.IsColimit.homIso, Adjunction.homEquiv_unit]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: case inst
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝¹ : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst✝ : G.IsSplitPair f g
⊢ PreservesColimit (parallelPair f g ⋙ G) (monadicLeftAdjoint G ⋙ G)

Tactic:
apply @preservesColimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoParallelPair.{v₁} _).symm ?_

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝¹ : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst✝ : G.IsSplitPair f g
⊢ PreservesColimit
    (parallelPair ((parallelPair f g ⋙ G).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ G).map WalkingParallelPairHom.right))
    (monadicLeftAdjoint G ⋙ G)
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: case inst
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝¹ : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst✝ : G.IsSplitPair f g
⊢ PreservesColimit ((parallelPair f g ⋙ G) ⋙ monadicLeftAdjoint G ⋙ G) (monadicLeftAdjoint G ⋙ G)

Tactic:
apply @preservesColimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoParallelPair.{v₁} _).symm ?_

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝¹ : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst✝ : G.IsSplitPair f g
⊢ PreservesColimit
    (parallelPair (((parallelPair f g ⋙ G) ⋙ monadicLeftAdjoint G ⋙ G).map WalkingParallelPairHom.left)
      (((parallelPair f g ⋙ G) ⋙ monadicLeftAdjoint G ⋙ G).map WalkingParallelPairHom.right))
    (monadicLeftAdjoint G ⋙ G)
Module: Mathlib.CategoryTheory.Monoidal.Arrow

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y : Arrow C
f : X ⟶ Y
⊢ f ▷ 𝟙_ (Arrow C) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f

Tactic:
refine Arrow.hom_ext _ _ (pushout.hom_ext ?_ (by simp)) (by simp)

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y : Arrow C
f : X ⟶ Y
⊢ pushout.inl (((curriedTensor C).map X.hom).app (𝟙_ (Arrow C)).left)
        (((curriedTensor C).obj X.left).map (𝟙_ (Arrow C)).hom) ≫
      Arrow.Hom.left (f ▷ 𝟙_ (Arrow C) ≫ (ρ_ Y).hom) =
    pushout.inl (((curriedTensor C).map X.hom).app (𝟙_ (Arrow C)).left)
        (((curriedTensor C).obj X.left).map (𝟙_ (Arrow C)).hom) ≫
      Arrow.Hom.left ((ρ_ X).hom ≫ f)
Module: Mathlib.CategoryTheory.Monoidal.Arrow

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y Z : Arrow C
⊢ (α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv =
    X ◁ (braiding Y Z).hom ≫ (α_ X Z Y).inv ≫ (braiding X Z).hom ▷ Y

Tactic:
refine Arrow.hom_ext _ _ (pushout.hom_ext ?_ (by simp)) (by simp)

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y Z : Arrow C
⊢ pushout.inl (((curriedTensor C).map X.hom).app (Y ⊗ Z).left) (((curriedTensor C).obj X.left).map (Y ⊗ Z).hom) ≫
      Arrow.Hom.left ((α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv) =
    pushout.inl (((curriedTensor C).map X.hom).app (Y ⊗ Z).left) (((curriedTensor C).obj X.left).map (Y ⊗ Z).hom) ≫
      Arrow.Hom.left (X ◁ (braiding Y Z).hom ≫ (α_ X Z Y).inv ≫ (braiding X Z).hom ▷ Y)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
⊢ (∃ ψ, ψ ≫ φ = G ◁ φ ≫ conj G) → ∀ (X : C), (monoidHom φ X).range.Normal

pp: case refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
⊢ (∀ (X : C), (monoidHom φ X).range.Normal) → ∃ ψ, ψ ≫ φ = G ◁ φ ≫ conj G

Tactic:
· intro ⟨ψ, hψ⟩ X
    constructor
    rintro - ⟨x, rfl⟩ z
    exact ⟨lift z x ≫ ψ, by simp [hψ]⟩

Goal state after:
case refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
⊢ (∀ (X : C), (monoidHom φ X).range.Normal) → ∃ ψ, ψ ≫ φ = G ◁ φ ≫ conj G
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : MonoidalCategory D
inst✝⁵ : SymmetricCategory D
inst✝⁴ : MonoidalClosed D
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
c : C
⊢ R ⋙ tensorLeft (R.obj c) ⋙ L ≅ tensorLeft c ⋙ 𝟭 C

Tactic:
refine NatIso.ofComponents (fun _ ↦ (μIso L _ _).symm ≪≫
        asIso ((adj.counit.app _) ⊗ₘ (adj.counit.app _))) (fun _ ↦ ?_)
      dsimp
      rw [Category.assoc, ← δ_natural_right_assoc,
        tensorHom_def', ← MonoidalCategory.whiskerLeft_comp_assoc,
        Adjunction.counit_naturality, whisker_exchange,
        tensorHom_def_assoc, MonoidalCategory.whiskerLeft_comp]

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) ≫ TensorBimod.actLeft M N₁

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₂
| 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) ⋯ ⋯)

Tactic:
rw [TensorBimod.whiskerLeft_π_actLeft]

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 N₁.X).inv ≫
    M.actLeft ▷ N₁.X ≫ coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft)

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₂
| 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) ⋯ ⋯)
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 ◁
      colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)) WalkingParallelPair.one ≫
    TensorBimod.actLeft M N₂

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 ◁ M.X ◁ f.hom

Tactic:
rw [TensorBimod.whiskerLeft_π_actLeft]

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 N₂.X).inv ≫
    M.actLeft ▷ N₂.X ≫ coequalizer.π (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)

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
Module: Mathlib.CategoryTheory.Subterminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
inst✝ : HasTerminal C
⊢ ∀ {X Y : Subterminals C} (f : X ⟶ Y),
    (𝟭 (Subterminals C)).map f ≫ (Iso.refl Y).hom =
      (Iso.refl X).hom ≫
        ({ obj := fun X ↦ { obj := Over.mk (terminal.from X.obj), property := ⋯ },
                map := fun {X Y} f ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun X ↦ { obj := X.obj.left, property := ⋯ },
                map := fun {X Y} f ↦ ObjectProperty.homMk f.hom.left, map_id := ⋯, map_comp := ⋯ }).map
          f

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Subterminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
inst✝ : HasTerminal C
⊢ ∀ {X Y : MonoOver (⊤_ C)} (f : X ⟶ Y),
    ({ obj := fun X ↦ { obj := X.obj.left, property := ⋯ }, map := fun {X Y} f ↦ ObjectProperty.homMk f.hom.left,
                map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun X ↦ { obj := Over.mk (terminal.from X.obj), property := ⋯ },
                map := fun {X Y} f ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯, map_comp := ⋯ }).map
          f ≫
        (MonoOver.isoMk
            (Iso.refl
              (({ obj := fun X ↦ { obj := X.obj.left, property := ⋯ },
                          map := fun {X Y} f ↦ ObjectProperty.homMk f.hom.left, map_id := ⋯, map_comp := ⋯ } ⋙
                        { obj := fun X ↦ { obj := Over.mk (terminal.from X.obj), property := ⋯ },
                          map := fun {X Y} f ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯, map_comp := ⋯ }).obj
                    Y).obj.left)
            ⋯).hom =
      (MonoOver.isoMk
            (Iso.refl
              (({ obj := fun X ↦ { obj := X.obj.left, property := ⋯ },
                          map := fun {X Y} f ↦ ObjectProperty.homMk f.hom.left, map_id := ⋯, map_comp := ⋯ } ⋙
                        { obj := fun X ↦ { obj := Over.mk (terminal.from X.obj), property := ⋯ },
                          map := fun {X Y} f ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯, map_comp := ⋯ }).obj
                    X).obj.left)
            ⋯).hom ≫
        (𝟭 (MonoOver (⊤_ C))).map f

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Subterminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
inst✝ : HasTerminal C
⊢ ∀ (X : Subterminals C),
    { obj := fun X ↦ { obj := Over.mk (terminal.from X.obj), property := ⋯ },
              map := fun {X Y} f ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯, map_comp := ⋯ }.map
          ((NatIso.ofComponents (fun X ↦ Iso.refl X) ⋯).hom.app X) ≫
        (NatIso.ofComponents
                (fun X ↦
                  MonoOver.isoMk
                    (Iso.refl
                      (({ obj := fun X ↦ { obj := X.obj.left, property := ⋯ },
                                  map := fun {X Y} f ↦ ObjectProperty.homMk f.hom.left, map_id := ⋯, map_comp := ⋯ } ⋙
                                { obj := fun X ↦ { obj := Over.mk (terminal.from X.obj), property := ⋯ },
                                  map := fun {X Y} f ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯, map_comp := ⋯ }).obj
                            X).obj.left)
                    ⋯)
                ⋯).hom.app
          ({ obj := fun X ↦ { obj := Over.mk (terminal.from X.obj), property := ⋯ },
                map := fun {X Y} f ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯, map_comp := ⋯ }.obj
            X) =
      𝟙
        ({ obj := fun X ↦ { obj := Over.mk (terminal.from X.obj), property := ⋯ },
              map := fun {X Y} f ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯, map_comp := ⋯ }.obj
          X)

Tactic:
by subsingleton

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₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
| X.X ◁ coequalizer.π (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) ≫ TensorBimod.actLeft M₁ N

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₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
| 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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯)

Tactic:
rw [TensorBimod.whiskerLeft_π_actLeft]

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₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
| (α_ X.X M₁.X N.X).inv ≫
    M₁.actLeft ▷ N.X ≫ coequalizer.π (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft)

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₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
| 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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯)
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₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
| X.X ◁
      colimit.ι (parallelPair (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft)) WalkingParallelPair.one ≫
    TensorBimod.actLeft M₂ N

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₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
| X.X ◁ f.hom ▷ N.X

Tactic:
rw [TensorBimod.whiskerLeft_π_actLeft]

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₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
| (α_ X.X M₂.X N.X).inv ≫
    M₂.actLeft ▷ N.X ≫ coequalizer.π (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft)

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₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
| X.X ◁ f.hom ▷ N.X