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

Goal state before:
pp: case w
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
a : G
this : X.ρ (f a) = ((res V f).obj X).ρ a
⊢ X.ρ (f a) ≫ g.hom = g.hom ≫ Y.ρ (f a)

Tactic:
this,

Goal state after:
case w
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
a : G
this : X.ρ (f a) = ((res V f).obj X).ρ a
⊢ ((res V f).obj X).ρ a ≫ g.hom = g.hom ≫ Y.ρ (f a)
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
this✝¹ : Abelian D := abelian L P
this✝ : PreservesFiniteLimits L
x✝ : PreservesFiniteLimits (L ⋙ G)
this : G.Additive
⊢ PreservesFiniteLimits G

Tactic:
refine ((Functor.preservesFiniteLimits_tfae G).out 2 3).mp (fun _ _ f ↦ ?_)

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
this✝¹ : Abelian D := abelian L P
this✝ : PreservesFiniteLimits L
x✝² : PreservesFiniteLimits (L ⋙ G)
this : G.Additive
x✝¹ x✝ : D
f : x✝¹ ⟶ x✝
⊢ PreservesLimit (parallelPair f 0) G
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: case zero
G : Type u
inst✝ : Group G
f : Fin (0 + 1) → G
⊢ (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G 0).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)

Tactic:
exact Prod.ext rfl (funext fun x => Fin.elim0 x)

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
⊢ { g // U.map (F.map g ≫ adj₁.counit.app (R.obj Y)) = U.map (adj₁.counit.app X) ≫ g } ≃
    { z // F.map (U.map (adj₁.counit.app X)) ≫ z = adj₁.counit.app ((U ⋙ F).obj X) ≫ z }

Tactic:
apply (adj₁.homEquiv _ _).symm.subtypeEquiv
      intro g
      rw [← (adj₁.homEquiv _ _).symm.injective.eq_iff, adj₁.homEquiv_counit,
        adj₁.homEquiv_counit, adj₁.homEquiv_counit, F.map_comp, assoc, U.map_comp, F.map_comp,
        assoc, adj₁.counit_naturality, adj₁.counit_naturality_assoc]
      apply eq_comm

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Quadruple

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ (∀ (X : C), Epi (q.leftTriple.rightToLeft.app X)) ↔ ∀ (X : D), Mono (q.rightTriple.leftToRight.app X)

Tactic:
simp_rw [mono_leftToRight_app_iff_mono_adj₂_unit_app, rightToLeft_eq_counits]

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ (∀ (X : C),
      Epi
        ((G.rightUnitor.inv ≫
              inv (G.whiskerLeft q.leftTriple.adj₁.counit) ≫
                (G.associator F L).inv ≫ whiskerRight q.leftTriple.adj₂.counit L ≫ L.leftUnitor.hom).app
          X)) ↔
    ∀ (X : D), Mono (q.rightTriple.adj₂.unit.app (F.obj X))
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := ⋯
⊢ R'.IsRightAdjoint

Tactic:
let : (R' ⋙ Monad.forget (monadicAdjunction U).toMonad).IsRightAdjoint := by
    refine ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight ?_).isRightAdjoint
    exact Functor.isoWhiskerLeft R (Monad.comparisonForget (monadicAdjunction U)).symm

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
this : (R' ⋙ (monadicAdjunction U).toMonad.forget).IsRightAdjoint :=
  Adjunction.isRightAdjoint
    ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight
      (R.isoWhiskerLeft (Monad.comparisonForget (monadicAdjunction U)).symm))
⊢ R'.IsRightAdjoint
Module: Mathlib.CategoryTheory.Bicategory.Extension

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
i : s ≅ t
x : B
h : c ⟶ x
⊢ StructuredArrow.Hom.right (i.hom ≫ i.inv) ▷ h = 𝟙 (StructuredArrow.right s ≫ h)

Tactic:
simp [Iso.hom_inv_id]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Extension

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
i : s ≅ t
x : B
h : x ⟶ c
⊢ h ◁ StructuredArrow.Hom.right (i.hom ≫ i.inv) = 𝟙 (h ≫ StructuredArrow.right s)

Tactic:
simp [Iso.hom_inv_id]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Extension

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : RightLift f g
i : s ≅ t
x : B
h : x ⟶ c
⊢ h ◁ (i.hom ≫ i.inv).left = 𝟙 (h ≫ s.left)

Tactic:
simp [Iso.hom_inv_id]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) ⊗≫
      η.app a ◁ (θ.naturality (f ≫ g) ≫ G.mapComp f g ▷ θ.app c) ⊗≫
        (η.naturality f ▷ G.map g ⊗≫ F.map f ◁ η.naturality g) ▷ θ.app c ⊗≫ 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) ⊗≫
      η.app a ◁ (θ.app a ◁ H.mapComp f g ⊗≫ θ.naturality f ▷ H.map g) ⊗≫
        ((η.app a ≫ G.map f) ◁ θ.naturality g ≫ η.naturality f ▷ (G.map g ≫ θ.app c)) ⊗≫
          F.map f ◁ η.naturality g ▷ θ.app c ⊗≫ 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c)

Tactic:
by
      rw [θ.naturality_comp]
      bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
      (F.map f ◁ η.naturality g ⊗≫ η.naturality f ▷ G.map g) ▷ θ.app c ⊗≫
        η.app a ◁ (G.mapComp f g ▷ θ.app c ≫ θ.naturality (f ≫ g)) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g)) =
    𝟙 ((F.map f ≫ F.map g) ≫ η.vCompApp θ c) ⊗≫
      F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
        (η.naturality f ▷ (G.map g ≫ θ.app c) ≫ (η.app a ≫ G.map f) ◁ θ.naturality g) ⊗≫
          η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ θ.app a ◁ H.mapComp f g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (f ≫ g))

Tactic:
by
      rw [θ.naturality_comp]
      bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ F.mapComp f g ▷ η.vCompApp θ c ≫ η.vCompNaturality θ (f ≫ g) =
    (α_ (F.map f) (F.map g) (η.vCompApp θ c)).hom ≫
      F.map f ◁ η.vCompNaturality θ g ≫
        (α_ (F.map f) (η.vCompApp θ b) (H.map g)).inv ≫
          η.vCompNaturality θ f ▷ H.map g ≫
            (α_ (η.vCompApp θ a) (H.map f) (H.map g)).hom ≫ η.vCompApp θ a ◁ H.mapComp f g

Tactic:
by
  calc
    _ = 𝟙 _ ⊗≫ (F.mapComp f g ▷ η.app c ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫
          η.app a ◁ θ.naturality (f ≫ g) ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ (F.map f ◁ η.naturality g ⊗≫ η.naturality f ▷ G.map g) ▷ θ.app c ⊗≫
          η.app a ◁ (G.mapComp f g ▷ θ.app c ≫ θ.naturality (f ≫ g)) ⊗≫ 𝟙 _ := by
      rw [η.naturality_comp]
      bicategory
    _ = 𝟙 _ ⊗≫ F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
          (η.naturality f ▷ (G.map g ≫ θ.app c) ≫ (η.app a ≫ G.map f) ◁ θ.naturality g) ⊗≫
            η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ θ.app a ◁ H.mapComp f g) ⊗≫ 𝟙 _ := by
      rw [θ.naturality_comp]
      bicategory
    _ = _ := by
      rw [← whisker_exchange]
      bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:

Tactic:
_
        _ = 𝟙 _ ⊗≫ t.unit ⊗≫ leftZigzag t.unit ε ▷ u ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ (_ ◁ t.unit ≫ t.unit ▷ _) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 _ := by
          rw [leftZigzag]; bicategory
        _ = 𝟙 _ ⊗≫ t.unit ⊗≫ t.lift ◁ (u ◁ t.unit ⊗≫ ε ▷ u) ⊗≫ 𝟙 _ := by
          rw [whisker_exchange]; bicategory
        _ = _ := by
          rw [← rightZigzag, Hε]; bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
j j' : J
h : j ⟶ j'
this : (s.π.app j).toFunctor ⋙ (F.map h).toFunctor = (s.π.app j').toFunctor
⊢ eqToHom ⋯ ≫ ((s.π.app j).toFunctor ⋙ (F.map h).toFunctor).map f ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯

Tactic:
rw [Functor.congr_hom this f]

Goal state after:
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
j j' : J
h : j ⟶ j'
this : (s.π.app j).toFunctor ⋙ (F.map h).toFunctor = (s.π.app j').toFunctor
⊢ eqToHom ⋯ ≫ (eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯) ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case refine_2
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
X Y : ↑s.pt
f : X ⟶ Y
this : ∀ (j : J), (s.π.app j).toFunctor.map f = eqToHom ⋯ ≫ (m ≫ (limitCone F).π.app j).toFunctor.map f ≫ eqToHom ⋯
⊢ (limitConeLift F s).toFunctor.map f = eqToHom ⋯ ≫ m.toFunctor.map f ≫ eqToHom ⋯

Tactic:
simp [this, -homDiagram_obj, limit_π_homDiagram_eqToHom]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Prod

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ (W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₁).flip).flip = (W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₂).flip).flip

Tactic:
apply Functor.uncurry_obj_injective

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ uncurry.obj (W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₁).flip).flip = uncurry.obj (W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₂).flip).flip
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝¹ : ChosenPullbacksAlong g
Y' Z' X' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
inst✝ : ChosenPullbacksAlong g'
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
comm₁ : f' ≫ γ₃ = γ₁ ≫ f
comm₂ : g' ≫ γ₃ = γ₂ ≫ g
⊢ fst f' g' ≫ γ₁ ≫ f = (snd f' g' ≫ γ₂) ≫ g

Tactic:
← comm₁,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝¹ : ChosenPullbacksAlong g
Y' Z' X' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
inst✝ : ChosenPullbacksAlong g'
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
comm₁ : f' ≫ γ₃ = γ₁ ≫ f
comm₂ : g' ≫ γ₃ = γ₂ ≫ g
⊢ fst f' g' ≫ f' ≫ γ₃ = (snd f' g' ≫ γ₂) ≫ g
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝¹ : ChosenPullbacksAlong g
Y' Z' X' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
inst✝ : ChosenPullbacksAlong g'
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
comm₁ : f' ≫ γ₃ = γ₁ ≫ f
comm₂ : g' ≫ γ₃ = γ₂ ≫ g
⊢ pullbackMap f g f' g' γ₁ γ₂ γ₃ comm₁ comm₂ ≫ fst f g = fst f' g' ≫ γ₁

Tactic:
simp only [pullbackMap, lift_fst]

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
K : Type u₄
inst✝² : Category.{v₄, u₄} K
inst✝¹ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝ : HasEnrichedHom V F₁ F₂
τ : F₁ ⟶ F₂
i j : J
f : i ⟶ j
⊢ (eHomEquiv V) (τ.app i) ≫ eHomWhiskerLeft V (F₁.obj i) (F₂.map f) = (eHomEquiv V) (τ.app i ≫ F₂.map f)

Tactic:
simp only [eHomEquiv_comp, tensorHom_def_assoc, MonoidalCategory.whiskerRight_id,
        ← unitors_equal, assoc, Iso.inv_hom_id_assoc, eHomWhiskerLeft]

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: case fst
X : Type w
φ : X → X → Prop
Y : Type w
f g : Y ⟶ ROfRel φ
h₁ : f ≫ p₁OfRel φ = g ≫ p₁OfRel φ
h₂ : f ≫ p₂OfRel φ = g ≫ p₂OfRel φ
y : Y
⊢ (↑((ConcreteCategory.hom f).toFun y)).1 = (↑((ConcreteCategory.hom g).toFun y)).1

pp: case snd
X : Type w
φ : X → X → Prop
Y : Type w
f g : Y ⟶ ROfRel φ
h₁ : f ≫ p₁OfRel φ = g ≫ p₁OfRel φ
h₂ : f ≫ p₂OfRel φ = g ≫ p₂OfRel φ
y : Y
⊢ (↑((ConcreteCategory.hom f).toFun y)).2 = (↑((ConcreteCategory.hom g).toFun y)).2

Tactic:
· exact congr($h₁ y)

Goal state after:
case snd
X : Type w
φ : X → X → Prop
Y : Type w
f g : Y ⟶ ROfRel φ
h₁ : f ≫ p₁OfRel φ = g ≫ p₁OfRel φ
h₂ : f ≫ p₂OfRel φ = g ≫ p₂OfRel φ
y : Y
⊢ (↑((ConcreteCategory.hom f).toFun y)).2 = (↑((ConcreteCategory.hom g).toFun y)).2
Module: Mathlib.CategoryTheory.Enriched.Opposite

Goal state before:
pp: V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : ForgetEnrichment V Cᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : f ≫ g = homTo V (f ≫ g)
⊢ (f ≫ g).op = f.op ≫ g.op

Tactic:
this,

Goal state after:
V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : ForgetEnrichment V Cᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : f ≫ g = homTo V (f ≫ g)
⊢ (homTo V (f ≫ g)).op = f.op ≫ g.op
Module: Mathlib.CategoryTheory.Enriched.Opposite

Goal state before:
pp: V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : (ForgetEnrichment V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
⊢ g.unop ≫ f.unop = f.unop ≫ g.unop

Tactic:
this,

Goal state after:
V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : (ForgetEnrichment V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
⊢ homTo V (g.unop ≫ f.unop) = f.unop ≫ g.unop
Module: Mathlib.CategoryTheory.Enriched.Opposite

Goal state before:
pp: V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : (ForgetEnrichment V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this✝ : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
this :
  (β_ (𝟙_ V) (𝟙_ V)).hom ≫
      (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
        eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    (homTo V f.unop ⊗ₘ homTo V g.unop) ≫ eComp V x y z
⊢ (λ_ (𝟙_ V)).inv ≫
      (β_ (𝟙_ V) (𝟙_ V)).hom ≫
        (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
          eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    f.unop ≫ g.unop

Tactic:
this,

Goal state after:
V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x y z : (ForgetEnrichment V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
this✝ : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop)
this :
  (β_ (𝟙_ V) (𝟙_ V)).hom ≫
      (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
        eComp V («to» V (Opposite.unop z)) («to» V (Opposite.unop y)) («to» V (Opposite.unop x)) =
    (homTo V f.unop ⊗ₘ homTo V g.unop) ≫ eComp V x y z
⊢ (λ_ (𝟙_ V)).inv ≫ (homTo V f.unop ⊗ₘ homTo V g.unop) ≫ eComp V x y z = f.unop ≫ g.unop
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁸ : Category.{v₁, u₁} V
inst✝⁷ : MonoidalCategory V
C : Type u₂
inst✝⁶ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
K : Type u₄
inst✝⁴ : Category.{v₄, u₄} K
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₁ F₂) i ≫
      (ρ_ (F₁.obj i ⟶[V] F₂.obj i)).inv ≫
        (F₁.obj i ⟶[V] F₂.obj i) ◁ (eHomEquiv V) (F₂.map f) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j ≫
      (λ_ (F₁.obj j ⟶[V] F₂.obj j)).inv ≫
        ((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₂.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)
| enrichedHom V F₁ F₂ ◁ end_.π (diagram V F₂ F₃) j ≫
    ((end_.π (diagram V F₁ F₂) i ≫
          (ρ_ (F₁.obj i ⟶[V] F₂.obj i)).inv ≫
            (F₁.obj i ⟶[V] F₂.obj i) ◁ (eHomEquiv V) (F₂.map f) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j)) ▷
        F₂.obj j ⟶[V] F₃.obj j) ≫
      eComp V (F₁.obj i) (F₂.obj j) (F₃.obj j)

Tactic:
this,

Goal state after:
V : Type u₁
inst✝⁸ : Category.{v₁, u₁} V
inst✝⁷ : MonoidalCategory V
C : Type u₂
inst✝⁶ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
K : Type u₄
inst✝⁴ : Category.{v₄, u₄} K
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₁ F₂) i ≫
      (ρ_ (F₁.obj i ⟶[V] F₂.obj i)).inv ≫
        (F₁.obj i ⟶[V] F₂.obj i) ◁ (eHomEquiv V) (F₂.map f) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j ≫
      (λ_ (F₁.obj j ⟶[V] F₂.obj j)).inv ≫
        ((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₂.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)
| enrichedHom V F₁ F₂ ◁ end_.π (diagram V F₂ F₃) j ≫
    ((end_.π (diagram V F₁ F₂) j ≫
          (λ_ (F₁.obj j ⟶[V] F₂.obj j)).inv ≫
            ((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₂.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)) ▷
        F₂.obj j ⟶[V] F₃.obj j) ≫
      eComp V (F₁.obj i) (F₂.obj j) (F₃.obj j)
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCartesian f φ
R' R'' : 𝒮
a' a'' : 𝒳
f' : R' ⟶ S
f'' : R'' ⟶ S
g : R' ⟶ R
g' : R'' ⟶ R'
H : f' = g ≫ f
H' : f'' = g' ≫ f'
φ' : a' ⟶ b
φ'' : a'' ⟶ b
inst✝¹ : p.IsStronglyCartesian f' φ'
inst✝ : p.IsHomLift f'' φ''
⊢ (map p f' φ' H' φ'' ≫ map p f φ H φ') ≫ φ = φ''

Tactic:
simp only [assoc, fac]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: case h.refine_1
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsStronglyCocartesian f φ
inst✝ : p.IsStronglyCocartesian g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : a ⟶ c'
hτ : p.IsHomLift ((f ≫ g) ≫ h) τ
⊢ (φ ≫ ψ) ≫ map p g ψ ⋯ (map p f φ ⋯ τ) = τ

Tactic:
simp only [assoc, fac]

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
K : Type u₄
inst✝³ : Category.{v₄, u₄} K
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
G : K ⥤ J
inst✝¹ : HasEnrichedHom V F₁ F₂
F₁' F₂' : K ⥤ C
inst✝ : HasEnrichedHom V F₁' F₂'
e₁ : G ⋙ F₁ ≅ F₁'
e₂ : G ⋙ F₂ ≅ F₂'
i j : K
f : i ⟶ j
⊢ enrichedHomπ V F₁ F₂ (G.obj i) ≫
      eHomWhiskerRight V (e₁.inv.app i) (F₂.obj (G.obj i)) ≫ eHomWhiskerLeft V (F₁'.obj i) (e₂.hom.app i ≫ F₂'.map f) =
    enrichedHomπ V F₁ F₂ (G.obj j) ≫
      eHomWhiskerRight V (e₁.inv.app j) (F₂.obj (G.obj j)) ≫
        eHomWhiskerLeft V (F₁'.obj j) (e₂.hom.app j) ≫ eHomWhiskerRight V (F₁'.map f) (F₂'.obj j)

Tactic:
← eHom_whisker_exchange,

Goal state after:
V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
K : Type u₄
inst✝³ : Category.{v₄, u₄} K
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
G : K ⥤ J
inst✝¹ : HasEnrichedHom V F₁ F₂
F₁' F₂' : K ⥤ C
inst✝ : HasEnrichedHom V F₁' F₂'
e₁ : G ⋙ F₁ ≅ F₁'
e₂ : G ⋙ F₂ ≅ F₂'
i j : K
f : i ⟶ j
⊢ enrichedHomπ V F₁ F₂ (G.obj i) ≫
      eHomWhiskerLeft V (F₁.obj (G.obj i)) (e₂.hom.app i ≫ F₂'.map f) ≫ eHomWhiskerRight V (e₁.inv.app i) (F₂'.obj j) =
    enrichedHomπ V F₁ F₂ (G.obj j) ≫
      eHomWhiskerRight V (e₁.inv.app j) (F₂.obj (G.obj j)) ≫
        eHomWhiskerLeft V (F₁'.obj j) (e₂.hom.app j) ≫ eHomWhiskerRight V (F₁'.map f) (F₂'.obj j)
Module: Mathlib.CategoryTheory.Filtered.Grothendieck

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
⊢ ∀ (X Y : Grothendieck F), ∃ Z x x, True

Tactic:
rintro ⟨c, f⟩ ⟨d, g⟩
    exact ⟨⟨max c d, max ((F.map (leftToMax c d)).toFunctor.obj f)
      ((F.map (rightToMax c d)).toFunctor.obj g)⟩,
      ⟨leftToMax c d, leftToMax _ _⟩, ⟨rightToMax c d, rightToMax _ _⟩, trivial⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Grothendieck

Goal state before:
pp: case e'_5
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
H : Type u₂
inst✝⁶ : Category.{v₂, u₂} H
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
F : C ⥤ Cat
inst✝⁴ : HasColimitsOfShape C H
inst✝³ : HasLimitsOfShape J H
inst✝² : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
inst✝¹ : PreservesLimitsOfShape J colim
inst✝ : ∀ (c : C), PreservesLimitsOfShape J colim
K : J ⥤ Grothendieck F ⥤ H
i₂ : colimit (limit K) ≅ limit (K ⋙ colim) :=
  Trans.trans
    (Trans.trans
      (Trans.trans (Trans.trans ⋯ (colimitFiberwiseColimitIso (limit K)).symm)
        (HasColimit.isoOfNatIso (fiberwiseColimitLimitIso K)))
      (preservesLimitIso colim (K ⋙ fiberwiseColim F H)))
    (HasLimit.isoOfNatIso (K.associator (fiberwiseColim F H) colim ≪≫ K.isoWhiskerLeft fiberwiseColimCompColimIso))
e_3✝ : colim.obj (limit K) = colimit (limit K)
j✝¹ : J
j✝ : Grothendieck F
⊢ (limit.π K j✝¹).app j✝ ≫ colimit.ι (K.obj j✝¹) j✝ =
    (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F j✝.base)).inv.app j✝.fiber ≫
      (limit.π (K ⋙ (whiskeringLeft (↑(F.obj j✝.base)) (Grothendieck F) H).obj (Grothendieck.ι F j✝.base)) j✝¹).app
          j✝.fiber ≫
        colimit.ι (K.obj j✝¹) { base := j✝.base, fiber := j✝.fiber }

Tactic:
simp [← Category.assoc, ← NatTrans.comp_app]

Goal state after: