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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
X✝ Y✝ : Cᵒᵖ
f : F.op.obj X✝ ⟶ F.op.obj Y✝
⊢ F.op.map (F.preimage f.unop).op = f

Tactic:
simp

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

Goal state before:
pp: I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
x✝ : K
⊢ ((fun i ↦ f' (g (f i))) ≫ fun b ↦ 𝟙 (Y (g (f b)))) x✝ =
    ((fun b ↦ 𝟙 (X (g (f b)))) ≫
        ({ obj := fun f i ↦ f (g i), map := fun {X Y} α i ↦ α (g i), map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun f_1 i ↦ f_1 (f i), map := fun {X Y} α i ↦ α (f i), map_id := ⋯, map_comp := ⋯ }).map
          f')
      x✝

Tactic:
simp

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

Goal state before:
pp: case h_map.refl
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
X Y : I
⊢ G.map { down := { down := ⋯ } } = eqToHom ⋯ ≫ F.map { down := { down := ⋯ } } ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ D
inst✝ : F.Full
X✝ Y✝ : C
f : F.rightOp.obj X✝ ⟶ F.rightOp.obj Y✝
⊢ F.rightOp.map (F.preimage f.unop).unop = f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ Dᵒᵖ
inst✝ : F.Full
X✝ Y✝ : Cᵒᵖ
f : F.leftOp.obj X✝ ⟶ F.leftOp.obj Y✝
⊢ F.leftOp.map (F.preimage f.op).op = f

Tactic:
simp

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

Goal state before:
pp: I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
h : J → I
j : J
⊢ ∀ {X Y : (i : I) → C i} (f : X ⟶ Y),
    (comap C h ⋙ eval (C ∘ h) j).map f ≫ (Iso.refl ((comap C h ⋙ eval (C ∘ h) j).obj Y)).hom =
      (Iso.refl ((comap C h ⋙ eval (C ∘ h) j).obj X)).hom ≫ (eval C (h j)).map f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫ e.inverse.map (𝟙 ((e.inverse ⋙ e.functor).obj Y)) ≫ e.unitInv.app (e.inverse.obj Y) =
    𝟙 (e.inverse.obj Y)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (G.op.map f ≫ (α.app (unop Y)).op).unop = ((α.app (unop X)).op ≫ F.op.map f).unop

Tactic:
simp

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

Goal state before:
pp: α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ⟶ G.obj i
X : I
x✝ : { as := X }.as = { as := X }.as
⊢ F.map (𝟙 { as := X }) ≫ f { as := X } = f { as := X } ≫ G.map (𝟙 { as := X })

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F ⟶ G
X Y : C
f : X ⟶ Y
⊢ (G.unop.map f ≫ (α.app (op Y)).unop).op = ((α.app (op X)).unop ≫ F.unop.map f).op

Tactic:
simp

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

Goal state before:
pp: α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ≅ G.obj i
X✝ : I
x✝ : { as := X✝ }.as = { as := X✝ }.as
⊢ F.map (𝟙 { as := X✝ }) ≫ (f { as := X✝ }).hom = (f { as := X✝ }).hom ≫ G.map (𝟙 { as := X✝ })

Tactic:
simp

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

Goal state before:
pp: α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
J : Type u₂
e : I ≃ J
i : Discrete I
⊢ (𝟭 (Discrete I)).obj i = (functor (mk ∘ ⇑e) ⋙ functor (mk ∘ ⇑e.symm)).obj i

Tactic:
simp

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

Goal state before:
pp: α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
J : Type u₂
e : I ≃ J
j : Discrete J
⊢ (functor (mk ∘ ⇑e.symm) ⋙ functor (mk ∘ ⇑e)).obj j = (𝟭 (Discrete J)).obj j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : C ⥤ Dᵒᵖ
α : F ⟶ G
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (G.leftOp.map f ≫ (α.app (unop Y)).unop).op = ((α.app (unop X)).unop ≫ F.leftOp.map f).op

Tactic:
simp

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

Goal state before:
pp: J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
h : f = 𝟙 j
⊢ F.map (𝟙 j) = 𝟙 (F.obj j)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : Cᵒᵖ ⥤ D
α : F ⟶ G
X Y : C
f : X ⟶ Y
⊢ (G.rightOp.map f ≫ (α.app (op Y)).op).unop = ((α.app (op X)).op ≫ F.rightOp.map f).unop

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ f.hom.unop ≫ f.inv.unop = 𝟙 (Opposite.unop Y)

Tactic:
by simp only [← unop_comp, f.inv_hom_id, unop_id]

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

Goal state before:
pp: J : Type u₂
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete J ⥤ C
x : J
⊢ (({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as, map_id := ⋯,
                  map_comp := ⋯ }).obj
            F).map
        (𝟙 { as := x }) ≫
      (Iso.refl
          ((({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯,
                      map_comp := ⋯ } ⋙
                    { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as,
                      map_id := ⋯, map_comp := ⋯ }).obj
                F).obj
            { as := x })).hom =
    (Iso.refl
          ((({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯,
                      map_comp := ⋯ } ⋙
                    { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as,
                      map_id := ⋯, map_comp := ⋯ }).obj
                F).obj
            { as := x })).hom ≫
      ((𝟭 (Discrete J ⥤ C)).obj F).map (𝟙 { as := x })

Tactic:
simp

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

Goal state before:
pp: I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
e : J ≃ I
i : I
⊢ e (e.symm i) = i

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
f : D ≌ E
X : C
⊢ f.functor.map (f.unitIso.hom.app (e.functor.obj X)) ≫
      f.functor.map (𝟙 ((𝟭 D).obj (f.inverse.obj (f.functor.obj (e.functor.obj X))))) ≫
        f.counitIso.hom.app (f.functor.obj (e.functor.obj X)) =
    𝟙 (f.functor.obj (e.functor.obj X))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : C ⥤ E
X : C
⊢ 𝟙 (F.obj (e.inverse.obj (e.functor.obj X))) ≫ F.map (e.unitIso.inv.app X) ≫ 𝟙 (F.obj X) = F.map (e.unitInv.app X)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : D ⥤ E
X : D
⊢ 𝟙 (F.obj (e.functor.obj (e.inverse.obj X))) ≫ F.map (e.counitIso.hom.app X) ≫ 𝟙 (F.obj X) = F.map (e.counit.app X)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : Cᵒᵖ
⊢ (e.functor.op.map ((NatIso.op e.unitIso).symm.hom.app X) ≫
        (NatIso.op e.counitIso).symm.hom.app (e.functor.op.obj X)).unop =
    (𝟙 (e.functor.op.obj X)).unop

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : Cᵒᵖ ≌ Dᵒᵖ
X : C
⊢ (e.functor.unop.map ((NatIso.unop e.unitIso).symm.hom.app X) ≫
        (NatIso.unop e.counitIso).symm.hom.app (e.functor.unop.obj X)).op =
    (𝟙 (e.functor.unop.obj X)).op

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (C ⥤ D)ᵒᵖ
f : F ⟶ G
⊢ f = f.unop.op

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (Cᵒᵖ ⥤ D)ᵒᵖ
η : F ⟶ G
⊢ η = η.unop.op

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.IsEquivalence
X : D
⊢ F.map (F.preimage ((F.objObjPreimageIso X).hom ≫ 𝟙 X ≫ (F.objObjPreimageIso X).inv)) = F.map (𝟙 (F.objPreimage X))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (F.preimage ((F.objObjPreimageIso X).hom ≫ (f ≫ g) ≫ (F.objObjPreimageIso Z).inv)) =
    F.map
      (F.preimage ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv) ≫
        F.preimage ((F.objObjPreimageIso Y).hom ≫ g ≫ (F.objObjPreimageIso Z).inv))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
X Y : C
f : X ⟶ Y
⊢ inv (inv f) = f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
X Y : C
f : Y ⟶ X
⊢ inv (inv f) = f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
X Y a✝ b✝ : C
f : a✝ ⟶ b✝
⊢ Groupoid.inv (Groupoid.inv f) = f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
X Y : C
D : Type u_1
inst✝ : Groupoid D
F : C ⥤ D
u✝ v✝ : C
f : u✝ ⟶ v✝
⊢ F.toPrefunctor.map (Quiver.reverse f) = Quiver.reverse (F.toPrefunctor.map f)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: C : Type u_1
𝒞 : Category.{?u.22, u_1} C
D : Type u
inst✝ : Groupoid D
F : C ⥤ D
h : F.FullyFaithful
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ F.map (h.preimage (inv (F.map f)) ≫ f) = F.map (𝟙 Y✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: C : Type u_1
𝒞 : Category.{?u.22, u_1} C
D : Type u
inst✝ : Groupoid D
F : C ⥤ D
h : F.FullyFaithful
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ F.map (f ≫ h.preimage (inv (F.map f))) = F.map (𝟙 X✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y Y' : T
f : X ⟶ Y
h : Y = Y'
⊢ (mk (f ≫ eqToHom h)).hom = eqToHom ⋯ ≫ (mk f).hom ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X' X Y : T
f : X ⟶ Y
h : X' = X
⊢ (mk (eqToHom h ≫ f)).hom = eqToHom h ≫ (mk f).hom ≫ eqToHom ⋯

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
ι : Type u_3
P : ι → MorphismProperty D
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ (⨆ i, P i).inverseImage F f✝ ↔ (⨆ i, (P i).inverseImage F) f✝

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
P : Set (MorphismProperty D)
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ (sSup P).inverseImage F f✝ ↔ (⨆ P' ∈ P, P'.inverseImage F) f✝

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
inst✝¹ : F.EssSurj
inst✝ : F.Full
X Y : D
f : X ⟶ Y
a✝ : ⊤ f
⊢ (F.objObjPreimageIso X).hom ≫ f =
    F.map (F.preimage ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv)) ≫ (F.objObjPreimageIso Y).hom

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ single f ≤ W ↔ W f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ Z✝ : C
e : X✝ ⟶ Y✝
he : IsIso e
f : Y✝ ⟶ Z✝
x✝ : P.isoClosure f
w✝¹ w✝ : C
f' : w✝¹ ⟶ w✝
hf' : P f'
iso : Arrow.mk f' ≅ Arrow.mk f
⊢ (asIso (Arrow.Hom.left iso.hom) ≪≫ asIso (inv e)).hom ≫ (Arrow.mk (e ≫ f)).hom =
    (Arrow.mk f').hom ≫ (asIso (Arrow.Hom.right iso.hom)).hom

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ Z✝ : C
e : Y✝ ⟶ Z✝
he : IsIso e
f : X✝ ⟶ Y✝
x✝ : P.isoClosure f
w✝¹ w✝ : C
f' : w✝¹ ⟶ w✝
hf' : P f'
iso : Arrow.mk f' ≅ Arrow.mk f
⊢ (asIso (Arrow.Hom.left iso.hom)).hom ≫ (Arrow.mk (f ≫ e)).hom =
    (Arrow.mk f').hom ≫ (asIso (Arrow.Hom.right iso.hom) ≪≫ asIso e).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y : T
i : X ≅ Y
p : Arrow T
sq : mk i.hom ⟶ p
⊢ i.inv ≫ Hom.left sq ≫ p.hom = Hom.right sq

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : IsSplitEpi f
⊢ section_ f ≫ f = 𝟙 Y

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : SplitEpi f
inst✝ : Epi hf.section_
⊢ hf.section_ ≫ f ≫ hf.section_ = hf.section_

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : SplitEpi f
inst✝ : Epi hf.section_
⊢ hf.section_ ≫ f = 𝟙 Y

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : SplitEpi f
⊢ (f.op ≫ h.section_.op).unop = (𝟙 (Opposite.op Y)).unop

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
hP : ∀ (f g : Arrow C) (x : f ≅ g), P f.hom → P g.hom
X Y Z : C
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : P f
⊢ (asIso (inv e)).hom ≫ (Arrow.mk (e ≫ f)).hom = (Arrow.mk f).hom ≫ (Iso.refl (Arrow.mk f).right).hom

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
hP : ∀ (f g : Arrow C) (x : f ≅ g), P f.hom → P g.hom
X Y Z : C
e : Y ⟶ Z
he : IsIso e
f : X ⟶ Y
hf : P f
⊢ (Iso.refl (Arrow.mk f).left).hom ≫ (Arrow.mk (f ≫ e)).hom = (Arrow.mk f).hom ≫ (asIso e).hom

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
W : MorphismProperty C
F : C ⥤ D
X✝ Y✝ : D
f✝ : X✝ ⟶ Y✝
x✝ : (W.strictMap F).isoClosure f✝
w✝¹ w✝ : D
f : w✝¹ ⟶ w✝
hf : W.strictMap F f
hf' : Nonempty (Arrow.mk f ≅ Arrow.mk f✝)
⊢ W.map F f✝

Tactic:
obtain ⟨hf⟩ := hf

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
W : MorphismProperty C
F : C ⥤ D
X✝¹ Y✝¹ : D
f✝¹ : X✝¹ ⟶ Y✝¹
x✝ : (W.strictMap F).isoClosure f✝¹
X Y : D
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
hf : W f✝
hf' : Nonempty (Arrow.mk (F.map f✝) ≅ Arrow.mk f✝¹)
⊢ W.map F f✝¹
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
E : Type u_2
inst✝ : Category.{v_2, u_2} E
G : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ P f → ((P.map F).map G).inverseImage (F ⋙ G) f

Tactic:
hf

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
E : Type u_2
inst✝ : Category.{v_2, u_2} E
G : D ⥤ E
X Y : C
f : X ⟶ Y
hf : P f
⊢ ((P.map F).map G).inverseImage (F ⋙ G) f
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: X Y : Type u
i : X ≅ Y
x : X
⊢ (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) x) = x

Tactic:
simp

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

Goal state before:
pp: X Y : Type u
i : X ≅ Y
y : Y
⊢ (ConcreteCategory.hom i.hom) ((ConcreteCategory.hom i.inv) y) = y

Tactic:
simp

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

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
X Y : C
f : X ⟶ Y
⊢ P.inverseImage E.functor f → P.map E.inverse f

Tactic:
hf

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
X Y : C
f : X ⟶ Y
hf : P.inverseImage E.functor f
⊢ P.map E.inverse f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
X Y : D
f : X ⟶ Y
⊢ P f → (P.inverseImage E.functor).inverseImage E.inverse f

Tactic:
hf

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
X Y : D
f : X ⟶ Y
hf : P f
⊢ (P.inverseImage E.functor).inverseImage E.inverse f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : C ⥤ D
α : F ⟶ G
X Y : C
e : X ≅ Y
⊢ (F.mapIso e).hom ≫ (Arrow.mk (α.app Y)).hom = (Arrow.mk (α.app X)).hom ≫ (G.mapIso e).hom

Tactic:
simp

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

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
e : X ⟶ Y
inst✝ : IsIso e
⊢ L.map e.left ≫ Y.hom ≫ R.map (inv e.right) = X.hom

Tactic:
simp

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

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
X Y : Comma L₁ R₁
l : X.left ≅ Y.left
r : X.right ≅ Y.right
h : L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom
⊢ X.hom = X.hom ≫ R₁.map (r.hom ≫ r.inv)

Tactic:
simp

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

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X : Comma L R
⊢ ((map α β).obj X).hom = (α.app X.left ≫ F.map X.hom) ≫ β.app X.right

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Endomorphism

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
f : End X
h : IsIso f
⊢ f * inv f = 1

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Endomorphism

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
f : End X
h : IsIso f
⊢ inv f * f = 1

Tactic:
simp

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

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
⊢ ∀ {X Y : Comma L R} (f : X ⟶ Y),
    (map α β ⋙ fst L' R').map f ≫ (Iso.refl ((map α β ⋙ fst L' R').obj Y)).hom =
      (Iso.refl ((map α β ⋙ fst L' R').obj X)).hom ≫ (fst L R ⋙ F₁).map f

Tactic:
simp

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

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
X✝ Y✝ : Comma L R
f : X✝ ⟶ Y✝
⊢ (R.op.map (op f.right) ≫ (unop (op { left := op X✝.right, right := op X✝.left, hom := op X✝.hom })).hom).unop =
    ((unop (op { left := op Y✝.right, right := op Y✝.left, hom := op Y✝.hom })).hom ≫ L.op.map (op f.left)).unop

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ (α.homCongr γ) (f ≫ g) = (α.homCongr β) f ≫ (β.homCongr γ) g

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ ((refl X).homCongr (refl Y)) f = f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ Y₁ X₂ Y₂ X₃ Y₃ : C
α₁ : X₁ ≅ X₂
β₁ : Y₁ ≅ Y₂
α₂ : X₂ ≅ X₃
β₂ : Y₂ ≅ Y₃
f : X₁ ⟶ Y₁
⊢ ((α₁ ≪≫ α₂).homCongr (β₁ ≪≫ β₂)) f = ((α₁.homCongr β₁).trans (α₂.homCongr β₂)) f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ⟶ Y
⊢ F.map ((α.homCongr β) f) = ((F.mapIso α).homCongr (F.mapIso β)) (F.map f)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ≅ Y
⊢ F.mapIso ((α.isoCongr β) f) = ((F.mapIso α).isoCongr (F.mapIso β)) (F.mapIso f)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: M : MonCat
x : ↑M
⊢ (ConcreteCategory.hom (𝟙 M)) x = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: M N T : MonCat
f : M ⟶ N
g : N ⟶ T
x : ↑M
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Goal state after: