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

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
A : Action V G
⊢ A.ρ 1 = 𝟙 A.V

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M ≅ N
⊢ f.hom.hom ≫ f.inv.hom = 𝟙 M.V ∧ f.inv.hom ≫ f.hom.hom = 𝟙 N.V

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M ≅ N
⊢ f.inv.hom ≫ f.hom.hom = 𝟙 N.V ∧ f.hom.hom ≫ f.inv.hom = 𝟙 M.V

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : HasZeroMorphisms V
X Y : Action V G
⊢ ∀ (g : G), X.ρ g ≫ 0 = 0 ≫ Y.ρ g

Tactic:
by simp

Goal state after:
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
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝¹ : L.PreservesEpimorphisms
this✝ : L.EssSurj
W : D
w : L.obj Y ⟶ W
hw : L.map f ≫ w = 0
this :
  ∀ (W : D) (w : L.obj Y ⟶ W),
    L.map f ≫ w = 0 → (∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ) → ∃ l, L.map (cokernel.π f) ≫ l = w
hw' : ¬∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : w ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s = L.map φ.f
⊢ ∃ z, L.map φ.f = L.map z ≫ eqToHom ⋯

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
X✝ Y✝ : V
f : X✝ ⟶ Y✝
x✝ : PUnit.{?u.12 + 1}
⊢ { V := X✝, ρ := 1 }.ρ PUnit.unit ≫ f = f ≫ { V := Y✝, ρ := 1 }.ρ PUnit.unit

Tactic:
by simp

Goal state after:
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
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X✝ Y✝ : D
f : X✝ ⟶ Y✝
g : Arrow C
e : L.mapArrow.obj g ≅ Arrow.mk f
this : PreservesColimit (parallelPair g.hom 0) L
⊢ HasCokernel f

Tactic:
have : HasColimit (parallelPair (L.map g.hom) 0) :=
      ⟨_, (CokernelCofork.isColimitMapCoconeEquiv _ L).1
        (isColimitOfPreserves L (cokernelIsCokernel g.hom))⟩

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
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X✝ Y✝ : D
f : X✝ ⟶ Y✝
g : Arrow C
e : L.mapArrow.obj g ≅ Arrow.mk f
this✝ : PreservesColimit (parallelPair g.hom 0) L
this : HasColimit (parallelPair (L.map g.hom) 0)
⊢ HasCokernel f
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
G : Type u_3
inst✝ : Monoid G
M : Action V G
⊢ F.map (M.ρ 1) = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence

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.Full
inst✝¹ : F.Faithful
X Y : C
inst✝ : ExactPairing (F.obj X) (F.obj Y)
⊢ F.map (F.preimage (δ F Y X ≫ ε_ (F.obj X) (F.obj Y) ≫ ε F)) = δ F Y X ≫ ε_ (F.obj X) (F.obj Y) ≫ ε F

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence

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.Full
inst✝¹ : F.Faithful
X Y : C
inst✝ : ExactPairing (F.obj X) (F.obj Y)
⊢ F.map (F.preimage (η F ≫ η_ (F.obj X) (F.obj Y) ≫ μ F X Y)) = η F ≫ η_ (F.obj X) (F.obj Y) ≫ μ F X Y

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Action.Continuous

Goal state before:
pp: V : Type u_1
inst✝⁷ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁶ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝⁵ : ConcreteCategory V FV
inst✝⁴ : HasForget₂ V TopCat
G : Type u_4
inst✝³ : Monoid G
inst✝² : TopologicalSpace G
H : Type u_5
inst✝¹ : Monoid H
inst✝ : TopologicalSpace H
f✝ f' : G →ₜ* H
h : f✝ = f'
X✝ Y✝ : ContAction V H
f : X✝ ⟶ Y✝
⊢ ((res V f✝).map f ≫ (ObjectProperty.isoMk IsContinuous (mkIso (Iso.refl ((res V f✝).obj Y✝).obj.V) ⋯)).hom).hom.hom =
    ((ObjectProperty.isoMk IsContinuous (mkIso (Iso.refl ((res V f✝).obj X✝).obj.V) ⋯)).hom ≫ (res V f').map f).hom.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Action.Continuous

Goal state before:
pp: V✝ : Type u_1
inst✝¹⁵ : Category.{v_1, u_1} V✝
FV✝ : V✝ → V✝ → Type u_2
CV✝ : V✝ → Type u_3
inst✝¹⁴ : (X Y : V✝) → FunLike (FV✝ X Y) (CV✝ X) (CV✝ Y)
inst✝¹³ : ConcreteCategory V✝ FV✝
inst✝¹² : HasForget₂ V✝ TopCat
G✝ : Type u_4
inst✝¹¹ : Monoid G✝
inst✝¹⁰ : TopologicalSpace G✝
V : Type u_5
W : Type u_6
inst✝⁹ : Category.{v_2, u_5} V
FV : V → V → Type u_7
CV : V → Type u_8
inst✝⁸ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝⁷ : ConcreteCategory V FV
inst✝⁶ : HasForget₂ V TopCat
inst✝⁵ : Category.{v_3, u_6} W
FW : W → W → Type u_9
CW : W → Type u_10
inst✝⁴ : (X Y : W) → FunLike (FW X Y) (CW X) (CW Y)
inst✝³ : ConcreteCategory W FW
inst✝² : HasForget₂ W TopCat
G : Type u_11
inst✝¹ : Monoid G
inst✝ : TopologicalSpace G
F F' : V ⥤ W
e : F ≅ F'
H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous
H' : ∀ (X : ContAction V G), ((F'.mapAction G).obj X.obj).IsContinuous
X : ContAction V G
⊢ ∀ (g : G),
    ((mapContAction G F H).obj X).obj.ρ g ≫ (e.app X.obj.V).hom =
      (e.app X.obj.V).hom ≫ ((mapContAction G F' H').obj X).obj.ρ g

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
inst✝¹ : MonoidalCategory V
inst✝ : BraidedCategory V
X Y : Action V G
g : G
⊢ (X ⊗ Y).ρ g ≫ (β_ X.V Y.V).hom = (β_ X.V Y.V).hom ≫ (Y ⊗ X).ρ g

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G✝ : Type u_2
inst✝¹ : Monoid G✝
G : Type u
inst✝ : Group G
X : Action (Type u) G
x✝ : (leftRegular G ⊗ X).V
⊢ ((fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1)) g.2))
        ((fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1⁻¹)) g.2)) x✝)).2 =
    x✝.2

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G✝ : Type u_2
inst✝¹ : Monoid G✝
G : Type u
inst✝ : Group G
X : Action (Type u) G
x✝ : (leftRegular G ⊗ trivial G X.V).V
⊢ ((fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1⁻¹)) g.2))
        ((fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1)) g.2)) x✝)).2 =
    x✝.2

Tactic:
by simp

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

Goal state before:
pp: case refine_1
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 : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this✝ : ∀ (Y : B), Mono (adj₁.unit.app Y)
this : s.ι ≫ U.map (F.map (adj₁.unit.app X)) = s.ι ≫ adj₁.unit.app (U.obj (F.obj X))
⊢ s.ι ≫ adj₁.unit.app (U.obj (F.obj X)) ≫ U.map (F.map (h X).left) = (s.ι ≫ (h X).right) ≫ adj₁.unit.app (h X).Z

Tactic:
rw [← assoc, ← this, assoc, ← U.map_comp, ← F.map_comp, RegularMono.w, F.map_comp,
        U.map_comp, s.condition_assoc, assoc, ← adj₁.unit_naturality (h _).right]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : d ⟶ ((evaluation C D).obj c).obj F
⊢ (fun f ↦ Sigma.ι (fun x ↦ d) (𝟙 c) ≫ f.app c)
      ((fun f ↦ { app := fun x ↦ Sigma.desc fun h ↦ f ≫ F.map h, naturality := ⋯ }) f) =
    f

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : ((evaluation C D).obj c).obj F ⟶ d
⊢ (fun f ↦ f.app c ≫ Pi.π (fun x ↦ d) (𝟙 c))
      ((fun f ↦ { app := fun x ↦ Pi.lift fun g ↦ F.map g ≫ f, naturality := ⋯ }) f) =
    f

Tactic:
by simp

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

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
F : B ⥤ A
inst✝² : ComonadicLeftAdjoint F
L : C ⥤ B
inst✝¹ : HasCoreflexiveEqualizers C
inst✝ : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (comonadicAdjunction F).toComonad.Coalgebra := L ⋙ Comonad.comparison (comonadicAdjunction F)
this : (L' ⋙ (comonadicAdjunction F).toComonad.forget).IsLeftAdjoint :=
  Adjunction.isLeftAdjoint
    ((Adjunction.ofIsLeftAdjoint (L ⋙ F)).ofNatIsoLeft
      (L.isoWhiskerLeft (Comonad.comparisonForget (comonadicAdjunction F)).symm))
X : (comonadicAdjunction F).toComonad.Coalgebra
⊢ RegularMono { f := X.a, h := ⋯ }

Tactic:
exact ⟨_, _, _, _, Comonad.beckCoalgebraEqualizer X⟩

Goal state after:
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
⊢ t.unit ▷ h = StructuredArrow.hom (t.whisker h) ≫ (α_ f t.extension h).inv

Tactic:
by simp

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 ◁ t.unit = StructuredArrow.hom (t.whisker h) ≫ (α_ h t.lift f).hom

Tactic:
by simp

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 ◁ s.counit = (α_ h s.lift f).inv ≫ CostructuredArrow.hom (s.whisker h)

Tactic:
by simp

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
⊢ (postcomp x f).map (h ◁ i.left) ≫ CostructuredArrow.hom (t.whisker h) = CostructuredArrow.hom (s.whisker h)

Tactic:
by
    rw [← cancel_epi (α_ h _ _).inv]
    calc
      _ = h ◁ (i.left ▷ f ≫ t.counit) := by simp [-RightLift.w]
      _ = h ◁ s.counit := congrArg (h ◁ ·) (RightLift.w i)
      _ = _ := by simp

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
η : OplaxTrans F G
θ : OplaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ (F.map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
      F.mapComp f g ▷ η.app c ▷ θ.app c ≫
        (α_ (F.map f) (F.map g) (η.app c)).hom ▷ θ.app c ≫
          (α_ (F.map f) (F.map g ≫ η.app c) (θ.app c)).hom ≫
            F.map f ◁ η.naturality g ▷ θ.app c ≫
              F.map f ◁ (α_ (η.app b) (G.map g) (θ.app c)).hom ≫
                (α_ (F.map f) (η.app b) (G.map g ≫ θ.app c)).inv ≫
                  (F.map f ≫ η.app b) ◁ θ.naturality g ≫
                    η.naturality f ▷ (θ.app b ≫ H.map g) ≫
                      (α_ (η.app a) (G.map f) (θ.app b ≫ H.map g)).hom ≫
                        η.app a ◁ (α_ (G.map f) (θ.app b) (H.map g)).inv ≫
                          η.app a ◁ θ.naturality f ▷ H.map g ≫
                            η.app a ◁ (α_ (θ.app a) (H.map f) (H.map g)).hom ≫
                              (α_ (η.app a) (θ.app a) (H.map f ≫ H.map g)).inv =
    F.mapComp f g ▷ (η.app c ≫ θ.app c) ≫
      (α_ (F.map f) (F.map g) (η.app c ≫ θ.app c)).hom ≫
        F.map f ◁
            ((α_ (F.map g) (η.app c) (θ.app c)).inv ≫
              η.naturality g ▷ θ.app c ≫
                (α_ (η.app b) (G.map g) (θ.app c)).hom ≫
                  η.app b ◁ θ.naturality g ≫ (α_ (η.app b) (θ.app b) (H.map g)).inv) ≫
          (α_ (F.map f) (η.app b ≫ θ.app b) (H.map g)).inv ≫
            ((α_ (F.map f) (η.app b) (θ.app b)).inv ≫
                  η.naturality f ▷ θ.app b ≫
                    (α_ (η.app a) (G.map f) (θ.app b)).hom ≫
                      η.app a ◁ θ.naturality f ≫ (α_ (η.app a) (θ.app a) (H.map f)).inv) ▷
                H.map g ≫
              (α_ (η.app a ≫ θ.app a) (H.map f) (H.map g)).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a : B
F : LocallyDiscrete (Discrete Unit) ⥤ᵒᵖᴸ B
⊢ (F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫ F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } })) ≫
      MonoidalCategoryStruct.whiskerLeft (F.map (𝟙 { as := { as := () } }))
        (F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫ F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } })) =
    (F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫ F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } })) ≫
      MonoidalCategoryStruct.whiskerRight
          (F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫ F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } }))
          (F.map (𝟙 { as := { as := () } })) ≫
        (MonoidalCategoryStruct.associator (F.map (𝟙 { as := { as := () } })) (F.map (𝟙 { as := { as := () } }))
            (F.map (𝟙 { as := { as := () } }))).hom

Tactic:
simp only [tensorObj_def, MonoidalCategory.whiskerLeft_comp, whiskerLeft_def, Category.assoc,
      MonoidalCategory.comp_whiskerRight, whiskerRight_def, associator_def]
    rw [← F.mapComp_naturality_left_assoc, ← F.mapComp_naturality_right_assoc]
    simp only [whiskerLeft_rightUnitor_inv, PrelaxFunctor.map₂_comp, Category.assoc,
      OplaxFunctor.map₂_associator, whiskerRight_id, Iso.hom_inv_id_assoc]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
τ₀ : (LeftExtension.mk u adj.unit).whisker h ⟶ s
τ : u ≫ h ⟶ s.extension := StructuredArrow.Hom.right τ₀
hτ : adj.unit ▷ h ⊗≫ f ◁ τ = s.unit
⊢ τ = 𝟙 (u ≫ h) ⊗≫ rightZigzag adj.unit adj.counit ▷ h ⊗≫ τ ⊗≫ 𝟙 s.extension

Tactic:
by
        rw [adj.right_triangle]; bicategory

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a✝ b✝ c✝ d✝ : Bᵒᵖ
f : a✝ ⟶ b✝
g g' : b✝ ⟶ c✝
η : g ⟶ g'
i : c✝ ⟶ d✝
⊢ i.unop ◁ (op2 (η.unop2 ▷ f.unop)).unop2 =
    (α_ i.unop g.unop f.unop).op2_unop.symm.hom.unop2 ≫
      (op2 ((op2 (i.unop ◁ η.unop2)).unop2 ▷ f.unop) ≫ (α_ i.unop g'.unop f.unop).op2_unop.symm.inv).unop2

Tactic:
by simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a✝ b✝ c✝ d✝ e✝ : Bᵒᵖ
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
i : d✝ ⟶ e✝
⊢ (op2 (i.unop ◁ (α_ h.unop g.unop f.unop).op2_unop.symm.hom.unop2)).unop2 ≫
      ((α_ i.unop (g ≫ h).unop f.unop).op2_unop.symm.hom ≫
          op2 ((α_ i.unop h.unop g.unop).op2_unop.symm.hom.unop2 ▷ f.unop)).unop2 =
    (α_ i.unop h.unop (f ≫ g).unop).op2_unop.symm.hom.unop2 ≫ (α_ (h ≫ i).unop g.unop f.unop).op2_unop.symm.hom.unop2

Tactic:
by simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a✝ b✝ c✝ : Bᵒᵖ
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
⊢ (α_ g.unop (𝟙 b✝).unop f.unop).op2_unop.symm.hom.unop2 ≫ (op2 ((ρ_ g.unop).op2_unop.hom.unop2 ▷ f.unop)).unop2 =
    g.unop ◁ (λ_ f.unop).op2_unop.hom.unop2

Tactic:
by simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
⊢ s.unit ⊗≫ s.lift ◁ rightZigzag adj.unit adj.counit ⊗≫ 𝟙 (s.lift ≫ u) = s.unit

Tactic:
by
        rw [adj.right_triangle]; bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : B
f : X₁ ⟶ X₂
⊢ 𝟙 X₁ ≫ f = f ≫ 𝟙 X₂

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ : B
f : X₁ ⟶ X₂
⊢ 𝟙 X₁ ≫ f = f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : B
f : X₁ ⟶ X₂
⊢ f ≫ 𝟙 X₂ = 𝟙 X₁ ≫ f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ : B
f : X₁ ⟶ X₂
⊢ f ≫ 𝟙 X₂ = f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: case some
X : PartialFun
x : X
⊢ ↑(ConcreteCategory.hom
          (partialFunToPointed.map
              ((NatIso.ofComponents
                      (fun X ↦
                        PartialFun.Iso.mk
                          { toFun := fun a ↦ ⟨some a, ⋯⟩, invFun := fun a ↦ Option.get ↑a ⋯, left_inv := ⋯,
                            right_inv := ⋯ })
                      ⋯).hom.app
                X) ≫
            (NatIso.ofComponents (fun X ↦ Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯) ⋯).hom.app
              (partialFunToPointed.obj X)))
      (some x) =
    ↑(ConcreteCategory.hom (𝟙 (partialFunToPointed.obj X))) (some x)

Tactic:
simp
      rfl

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
x✝¹ : α
x✝ : β
⊢ x✝ ∈ (PFun.id β).comp f x✝¹ ↔ x✝ ∈ f x✝¹

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
x✝¹ : α
x✝ : β
⊢ x✝ ∈ f.comp (PFun.id α) x✝¹ ↔ x✝ ∈ f x✝¹

Tactic:
by simp

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X : limit (F ⋙ objects)
j j' : J
f : j ⟶ j'
⊢ (hom ((homDiagram X X).map f)) (𝟙 ((hom (limit.π (F ⋙ objects) j)) X)) = 𝟙 ((hom (limit.π (F ⋙ objects) j')) X)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final

Goal state before:
pp: A : Type u₁
inst✝⁴ : SmallCategory A
B : Type u₁
inst✝³ : SmallCategory B
T : Type u₁
inst✝² : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝¹ : R.Final
inst✝ : ∀ (b : B), (CostructuredArrow.toOver L (R.obj b)).Final
G : T ⥤ Type u₁
this : ∀ (b : B), ((R.whiskerLeft (preFunctor L (𝟭 T))).app b).toFunctor.Final
i : colimit (L ⋙ G) ≅ colimit G :=
  Trans.trans
    (Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans
            (Trans.trans (L.colimitIsoColimitGrothendieck (L ⋙ G))
              (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ L ⋙ G)).symm)
            (HasColimit.isoOfNatIso
              (NatIso.ofComponents
                (fun x ↦ Iso.refl ((Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G).obj x)) ⋯)))
          (Final.colimitIso (Grothendieck.map (R.whiskerLeft (preFunctor L (𝟭 T))))
            (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G)))
        (HasColimit.isoOfNatIso (Iso.refl (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G))))
      (Final.colimitIso (Grothendieck.pre (functor (𝟭 T)) R) (grothendieckProj (𝟭 T) ⋙ G)))
    ((𝟭 T).colimitIsoColimitGrothendieck G).symm
x✝ : Grothendieck (R ⋙ functor L)
⊢ colimit.ι (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G) x✝ ≫
      (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ L ⋙ G)).hom ≫
        (L.colimitIsoColimitGrothendieck (L ⋙ G)).inv ≫ colimit.pre G L =
    colimit.ι (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G) x✝ ≫
      (HasColimit.isoOfNatIso (NatIso.ofComponents (fun x ↦ Iso.refl (G.obj (L.obj (left x.fiber)))) ⋯)).hom ≫
        (Final.colimitIso (Grothendieck.map (R.whiskerLeft (preFunctor L (𝟭 T))))
              (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G)).hom ≫
          (HasColimit.isoOfNatIso (Iso.refl (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G))).hom ≫
            (Final.colimitIso (Grothendieck.pre (functor (𝟭 T)) R) (grothendieckProj (𝟭 T) ⋙ G)).hom ≫
              ((𝟭 T).colimitIsoColimitGrothendieck G).inv

Tactic:
by simp

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
E : Type u_5
E' : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D₁
inst✝⁸ : Category.{v_4, u_4} D₂
inst✝⁷ : Category.{v_5, u_5} E
inst✝⁶ : Category.{v_6, u_6} E'
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
inst✝³ : W₁.ContainsIdentities
inst✝² : W₂.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ E
inst✝¹ : Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'
inst✝ : Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'
e : F₁ ≅ F₂
⊢ ∀ (X₁ : C₁) (X₂ : C₂),
    ((lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' e.hom ≫ lift₂NatTrans L₁ L₂ W₁ W₂ F₂ F₁ F₂' F₁' e.inv).app
            (L₁.obj X₁)).app
        (L₂.obj X₂) =
      ((𝟙 F₁').app (L₁.obj X₁)).app (L₂.obj X₂)

Tactic:
by simp

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
E : Type u_5
E' : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D₁
inst✝⁸ : Category.{v_4, u_4} D₂
inst✝⁷ : Category.{v_5, u_5} E
inst✝⁶ : Category.{v_6, u_6} E'
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
inst✝³ : W₁.ContainsIdentities
inst✝² : W₂.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ E
inst✝¹ : Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'
inst✝ : Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'
e : F₁ ≅ F₂
⊢ ∀ (X₁ : C₁) (X₂ : C₂),
    ((lift₂NatTrans L₁ L₂ W₁ W₂ F₂ F₁ F₂' F₁' e.inv ≫ lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' e.hom).app
            (L₁.obj X₁)).app
        (L₂.obj X₂) =
      ((𝟙 F₂').app (L₁.obj X₁)).app (L₂.obj X₂)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X : Dial C
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalLeftDistrib C
X Y Z : C
⊢ X ◁ coprod.inr ≫ (∂L X Y Z).inv = coprod.inr

Tactic:
apply (cancel_iso_hom_right _ _ (∂L X Y Z)).mp
  rw [assoc, Iso.inv_hom_id, comp_id, coprod_inr_leftDistrib_hom]

Goal state after: