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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
X : C
⊢ inv (e.inv.app X) = e.hom.app X

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: V : Type u_2
inst✝¹ : Quiver V
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
f : X ⟶ Y
⊢ (lift φ).map (reverse f) = reverse ((lift φ).map f)

Tactic:
by
  dsimp [Symmetrify.lift]; cases f
  · simp only
    rfl
  · simp only [reverse_reverse]
    rfl

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u₁
inst✝ : Quiver V
a b✝¹ b b✝ : V
q : Path a b✝
e : b✝ ⟶ b
⊢ ((𝟭q V).mapPath q).cons e = q.cons e

Tactic:
rw [mapPath_id q]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
h : P.isoClosure = P
⊢ P.IsClosedUnderIsomorphisms

Tactic:
rw [← h]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
h : P.isoClosure = P
⊢ P.isoClosure.IsClosedUnderIsomorphisms
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
h : X = Y
⊢ inv (eqToHom h) = eqToHom ⋯

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hz : F.obj Z = G.obj Z
hf : F.map f ≍ G.map f
hg : F.map g ≍ G.map g
⊢ F.map f ≫ F.map g ≍ G.map (f ≫ g)

Tactic:
G.map_comp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hz : F.obj Z = G.obj Z
hf : F.map f ≍ G.map f
hg : F.map g ≍ G.map g
⊢ F.map f ≫ F.map g ≍ G.map f ≫ G.map g
Module: Mathlib.CategoryTheory.Whiskering

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
F : C ⥤ D
G : D ⥤ E
⊢ isoWhiskerRight (Iso.refl F) G = Iso.refl (F ⋙ G)

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

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
B : Type u₄
inst✝ : Category.{v₄, u₄} B
F : B ⥤ C
G : C ⥤ D
H K : D ⥤ E
α : H ⟶ K
⊢ F.whiskerLeft (G.whiskerLeft α) = (F.associator G H).inv ≫ (F ⋙ G).whiskerLeft α ≫ (F.associator G K).hom

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

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
B : Type u₄
inst✝ : Category.{v₄, u₄} B
H K : B ⥤ C
F : C ⥤ D
G : D ⥤ E
α : H ⟶ K
⊢ whiskerRight (whiskerRight α F) G = (H.associator F G).hom ≫ whiskerRight α (F ⋙ G) ≫ (K.associator F G).inv

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

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
B : Type u₄
inst✝ : Category.{v₄, u₄} B
F : B ⥤ C
G H : C ⥤ D
α : G ⟶ H
K : D ⥤ E
⊢ whiskerRight (F.whiskerLeft α) K = (F.associator G K).hom ≫ F.whiskerLeft (whiskerRight α K) ≫ (F.associator H K).inv

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

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
B : Type u₄
inst✝ : Category.{v₄, u₄} B
F : B ⥤ C
G : C ⥤ D
H K : D ⥤ E
α : H ≅ K
⊢ F.isoWhiskerLeft (G.isoWhiskerLeft α) = (F.associator G H).symm ≪≫ (F ⋙ G).isoWhiskerLeft α ≪≫ F.associator G K

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

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
B : Type u₄
inst✝ : Category.{v₄, u₄} B
H K : B ⥤ C
F : C ⥤ D
G : D ⥤ E
α : H ≅ K
⊢ isoWhiskerRight (isoWhiskerRight α F) G = H.associator F G ≪≫ isoWhiskerRight α (F ⋙ G) ≪≫ (K.associator F G).symm

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

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
B : Type u₄
inst✝ : Category.{v₄, u₄} B
F : B ⥤ C
G H : C ⥤ D
α : G ≅ H
K : D ⥤ E
⊢ isoWhiskerRight (F.isoWhiskerLeft α) K =
    F.associator G K ≪≫ F.isoWhiskerLeft (isoWhiskerRight α K) ≪≫ (F.associator H K).symm

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

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
B : Type u₄
inst✝ : Category.{v₄, u₄} B
F : B ⥤ C
G H : C ⥤ D
α : G ≅ H
K : D ⥤ E
⊢ F.isoWhiskerLeft (isoWhiskerRight α K) =
    (F.associator G K).symm ≪≫ isoWhiskerRight (F.isoWhiskerLeft α) K ≪≫ F.associator H K

Tactic:
by
  cat_disch

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 { down := { down := ⋯ } } ≫ f { as := X } = f { as := X } ≫ G.map { down := { down := ⋯ } }

Tactic:
change F.map (𝟙 _) ≫ _ = _ ≫ G.map (𝟙 _)

Goal state after:
α : 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 })
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
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map ((adjointifyη η ε).hom.app X) ≫ ε.hom.app (F.obj X) = 𝟙 (F.obj X)

Tactic:
dsimp [adjointifyη, Trans.trans]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map
        ((((((η.hom.app X ≫ 𝟙 (G.obj (F.obj X))) ≫ G.map (ε.inv.app (F.obj X))) ≫ 𝟙 (G.obj (F.obj (G.obj (F.obj X))))) ≫
              𝟙 (G.obj (F.obj (G.obj (F.obj X))))) ≫
            G.map (F.map (η.inv.app X))) ≫
          𝟙 (G.obj (F.obj X))) ≫
      ε.hom.app (F.obj X) =
    𝟙 (F.obj X)
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
E : Type u_1
inst✝ : Category.{v_1, u_1} E
H : D ⥤ E
α : F ⟶ G
⊢ NatTrans.op (whiskerRight α H) = (G.opComp H).hom ≫ whiskerRight (NatTrans.op α) H.op ≫ (F.opComp H).inv

Tactic:
by
  cat_disch

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
E : Type u_1
inst✝ : Category.{v_1, u_1} E
H : E ⥤ C
α : F ⟶ G
⊢ NatTrans.op (H.whiskerLeft α) = (H.opComp G).hom ≫ H.op.whiskerLeft (NatTrans.op α) ≫ (H.opComp F).inv

Tactic:
by
  cat_disch

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 { down := { down := ⋯ } } ≫ (f { as := X✝ }).hom = (f { as := X✝ }).hom ≫ G.map { down := { down := ⋯ } }

Tactic:
change F.map (𝟙 _) ≫ _ = _ ≫ G.map (𝟙 _)

Goal state after:
α : 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✝ })
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ᵒᵖ
E : Type u_1
inst✝ : Category.{v_1, u_1} E
H : Dᵒᵖ ⥤ Eᵒᵖ
α : F ⟶ G
⊢ NatTrans.unop (whiskerRight α H) = (G.unopComp H).hom ≫ whiskerRight (NatTrans.unop α) H.unop ≫ (F.unopComp H).inv

Tactic:
by
  cat_disch

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ᵒᵖ
E : Type u_1
inst✝ : Category.{v_1, u_1} E
H : Eᵒᵖ ⥤ Cᵒᵖ
α : F ⟶ G
⊢ NatTrans.unop (H.whiskerLeft α) = (H.unopComp G).hom ≫ H.unop.whiskerLeft (NatTrans.unop α) ≫ (H.unopComp F).inv

Tactic:
by
  cat_disch

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ᵒᵖ
E : Type u_1
inst✝ : Category.{v_1, u_1} E
H : E ⥤ C
α : F ⟶ G
⊢ NatTrans.leftOp (H.whiskerLeft α) = (H.leftOpComp G).hom ≫ H.op.whiskerLeft (NatTrans.leftOp α) ≫ (H.leftOpComp F).inv

Tactic:
by
  cat_disch

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
E : Type u_1
inst✝ : Category.{v_1, u_1} E
H : D ⥤ E
α : F ⟶ G
⊢ NatTrans.rightOp (whiskerRight α H) =
    (G.rightOpComp H).hom ≫ whiskerRight (NatTrans.rightOp α) H.op ≫ (F.rightOpComp H).inv

Tactic:
by
  cat_disch

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
E : Type u_1
inst✝ : Category.{v_1, u_1} E
H : D ⥤ E
α : F ≅ G
⊢ NatIso.op (isoWhiskerRight α H) = G.opComp H ≪≫ isoWhiskerRight (NatIso.op α) H.op ≪≫ (F.opComp H).symm

Tactic:
by
  cat_disch

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
E : Type u_1
inst✝ : Category.{v_1, u_1} E
H : E ⥤ C
α : F ≅ G
⊢ NatIso.op (H.isoWhiskerLeft α) = H.opComp G ≪≫ H.op.isoWhiskerLeft (NatIso.op α) ≪≫ (H.opComp F).symm

Tactic:
by
  cat_disch

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ᵒᵖ
E : Type u_1
inst✝ : Category.{v_1, u_1} E
H : Dᵒᵖ ⥤ Eᵒᵖ
α : F ≅ G
⊢ NatIso.unop (isoWhiskerRight α H) = G.unopComp H ≪≫ isoWhiskerRight (NatIso.unop α) H.unop ≪≫ (F.unopComp H).symm

Tactic:
by
  cat_disch

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ᵒᵖ
E : Type u_1
inst✝ : Category.{v_1, u_1} E
H : Eᵒᵖ ⥤ Cᵒᵖ
α : F ≅ G
⊢ NatIso.unop (H.isoWhiskerLeft α) = H.unopComp G ≪≫ H.unop.isoWhiskerLeft (NatIso.unop α) ≪≫ (H.unopComp F).symm

Tactic:
by
  cat_disch

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
⊢ NatIso.op F.leftUnitor = F.op.leftUnitor.symm ≪≫ isoWhiskerRight (opId C).symm F.op ≪≫ ((𝟭 C).opComp F).symm

Tactic:
by
  cat_disch

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
⊢ NatIso.op F.rightUnitor = F.op.rightUnitor.symm ≪≫ F.op.isoWhiskerLeft (opId D).symm ≪≫ (F.opComp (𝟭 D)).symm

Tactic:
by
  cat_disch

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 : Type u_1
E' : Type u_2
inst✝¹ : Category.{v_1, u_1} E
inst✝ : Category.{v_2, u_2} E'
F : C ⥤ D
G : D ⥤ E
H : E ⥤ E'
⊢ NatIso.op (F.associator G H) =
    F.opComp (G ⋙ H) ≪≫
      F.op.isoWhiskerLeft (G.opComp H) ≪≫
        (F.op.associator G.op H.op).symm ≪≫ isoWhiskerRight (F.opComp G).symm H.op ≪≫ ((F ⋙ G).opComp H).symm

Tactic:
by
  cat_disch

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ᵒᵖ
⊢ NatIso.unop F.leftUnitor =
    F.unop.leftUnitor.symm ≪≫ isoWhiskerRight (unopId C).symm F.unop ≪≫ ((𝟭 Cᵒᵖ).unopComp F).symm

Tactic:
by
  cat_disch

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ᵒᵖ
⊢ NatIso.unop F.rightUnitor =
    F.unop.rightUnitor.symm ≪≫ F.unop.isoWhiskerLeft (unopId D).symm ≪≫ (F.unopComp (𝟭 Dᵒᵖ)).symm

Tactic:
by
  cat_disch

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 : Type u_1
E' : Type u_2
inst✝¹ : Category.{v_1, u_1} E
inst✝ : Category.{v_2, u_2} E'
F : Cᵒᵖ ⥤ Dᵒᵖ
G : Dᵒᵖ ⥤ Eᵒᵖ
H : Eᵒᵖ ⥤ E'ᵒᵖ
⊢ NatIso.unop (F.associator G H) =
    F.unopComp (G ⋙ H) ≪≫
      F.unop.isoWhiskerLeft (G.unopComp H) ≪≫
        (F.unop.associator G.unop H.unop).symm ≪≫
          isoWhiskerRight (F.unopComp G).symm H.unop ≪≫ ((F ⋙ G).unopComp H).symm

Tactic:
by
  cat_disch

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 ≫ (NatIso.ofComponents (fun x ↦ Iso.refl ((unop G).obj x)) ⋯).hom.op =
    (NatIso.ofComponents (fun x ↦ Iso.refl ((unop F).obj x)) ⋯).hom.op ≫
      Quiver.Hom.op { app := fun X ↦ f.unop.app X, naturality := ⋯ }

Tactic:
rw [show f = f.unop.op by simp, ← op_comp, ← op_comp]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (C ⥤ D)ᵒᵖ
f : F ⟶ G
⊢ ((NatIso.ofComponents (fun x ↦ Iso.refl ((unop G).obj x)) ⋯).hom ≫ f.unop).op =
    ({ app := fun X ↦ f.unop.op.unop.app X, naturality := ⋯ } ≫
        (NatIso.ofComponents (fun x ↦ Iso.refl ((unop F).obj x)) ⋯).hom).op
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✝ : C
f : X✝ ⟶ Y✝
⊢ F.map ((𝟭 C).map f ≫ (F.preimageIso (F.objObjPreimageIso (F.obj Y✝))).symm.hom) =
    F.map ((F.preimageIso (F.objObjPreimageIso (F.obj X✝))).symm.hom ≫ (F ⋙ F.inv).map f)

Tactic:
simp [inv]

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 : D} (f : X ⟶ Y), (F.inv ⋙ F).map f ≫ (F.objObjPreimageIso Y).hom = (F.objObjPreimageIso X).hom ≫ (𝟭 D).map f

Tactic:
simp [inv]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y Z : C
p : X = Y
q : Y = Z
x : F.obj X
⊢ (ConcreteCategory.hom (F.map (eqToHom q))) ((ConcreteCategory.hom (F.map (eqToHom p))) x) =
    (ConcreteCategory.hom (F.map (eqToHom ⋯))) x

Tactic:
by
  cat_disch

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
P : MorphismProperty C
⊢ ∀ {F G : C ⥤ D} (e : F ≅ G), P.map F = P.map G

Tactic:
suffices ∀ {F G : C ⥤ D} (_ : F ≅ G), P.map F ≤ P.map G from
    fun F G e => le_antisymm (this e) (this e.symm)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
P : MorphismProperty C
⊢ ∀ {F G : C ⥤ D} (x : F ≅ G), P.map F ≤ P.map G
Module: Mathlib.CategoryTheory.Adjunction.Basic

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
F : C ⥤ D
G : D ⥤ E
inst✝ : G.IsEquivalence
⊢ (F ⋙ G).IsLeftAdjoint ↔ F.IsLeftAdjoint

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ inferInstance⟩
  let iso : F ≅ (F ⋙ G) ⋙ G.asEquivalence.inverse :=
    (Functor.rightUnitor _).symm ≪≫ Functor.isoWhiskerLeft _ G.asEquivalence.unitIso ≪≫
      (Functor.associator _ _ _).symm
  exact isLeftAdjoint_of_iso iso.symm

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)} (f : X ⟶ Y),
    (yonedaPairing C).map f ≫ (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫ (yonedaEvaluation C).map f

Tactic:
intro (X, F) (Y, G) f

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
F : Cᵒᵖ ⥤ Type v₁
Y : Cᵒᵖ
G : Cᵒᵖ ⥤ Type v₁
f : (X, F) ⟶ (Y, G)
⊢ (yonedaPairing C).map f ≫ (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
    (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫ (yonedaEvaluation C).map f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : C × (C ⥤ Type v₁)} (f : X ⟶ Y),
    (coyonedaPairing C).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫ (coyonedaEvaluation C).map f

Tactic:
intro (X, F) (Y, G) f

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
Y : C
G : C ⥤ Type v₁
f : (X, F) ⟶ (Y, G)
⊢ (coyonedaPairing C).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
    (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫ (coyonedaEvaluation C).map f
Module: Mathlib.CategoryTheory.Limits.Cones

Goal state before:
pp: J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝⁵ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝⁴ : Category.{v₃, u₃} C
D : Type u₄
inst✝³ : Category.{v₄, u₄} D
E : Type u₅
inst✝² : Category.{v₅, u₅} E
F✝ : J ⥤ C
G F : C ⥤ D
inst✝¹ : F.ReflectsIsomorphisms
K : J ⥤ C
A B : Cone K
f : A ⟶ B
inst✝ : IsIso ((functoriality K F).map f)
this✝ : IsIso (F.map f.hom)
this : IsIso f.hom
⊢ IsIso f

Tactic:
apply cone_iso_of_hom_iso

Goal state after:
Module: Mathlib.CategoryTheory.Functor.EpiMono

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
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.PreservesMonomorphisms
inst✝ : G.PreservesMonomorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
h : Mono f
⊢ Mono ((F ⋙ G).map f)

Tactic:
rw [comp_map]
    exact inferInstance

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

Goal state before:
pp: J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasLimit F
E : K ⥤ J
inst✝¹ : HasLimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasLimit (D ⋙ E ⋙ F)
this : HasLimit ((D ⋙ E) ⋙ F)
j : L
⊢ π F (E.obj (D.obj j)) = pre F (D ⋙ E) ≫ π (D ⋙ E ⋙ F) j

Tactic:
limit.pre_π

Goal state after:
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasLimit F
E : K ⥤ J
inst✝¹ : HasLimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasLimit (D ⋙ E ⋙ F)
this : HasLimit ((D ⋙ E) ⋙ F)
j : L
⊢ π F (E.obj (D.obj j)) = π F ((D ⋙ E).obj j)
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasLimitsOfShape J C
F : J ⥤ C
⊢ pre F (𝟭 J) = lim.map F.leftUnitor.inv

Tactic:
by
  cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimit F
E : K ⥤ J
inst✝ : HasColimit (E ⋙ F)
s : ColimitCocone (E ⋙ F)
t : ColimitCocone F
⊢ pre F E = (isoColimitCocone s).hom ≫ s.isColimit.desc (Cocone.whisker E t.cocone) ≫ (isoColimitCocone t).inv

Tactic:
by
  cat_disch

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasColimitsOfSize.{v₁, u₁, v, u} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : Small.{u₁, u₂} J
inst✝ : LocallySmall.{v₁, v₂, u₂} J
⊢ HasColimitsOfShape J C

Tactic:
by
  have := HasColimitsOfSize.has_colimits_of_shape (C := C) (ShrinkHoms (Shrink.{u₁} J))
  exact hasColimitsOfShape_of_equivalence
    ((ShrinkHoms.equivalence _).symm.trans (Shrink.equivalence _).symm)

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

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
g : widePushout B objs arrows ⟶ X
⊢ g = desc (head arrows ≫ g) (fun j ↦ ι arrows j ≫ g) ⋯

Tactic:
by
  cat_disch

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

Goal state before:
pp: β : Type w
α : Type w₂
C : Type u
inst✝² : Category.{v, u} C
f : α → C
g : β → C
inst✝¹ : HasProduct f
inst✝ : HasProduct g
p p' : β → α
q : (b : β) → f (p b) ⟶ g b
q' : (b : β) → f (p' b) ⟶ g b
hp : p = p'
hq : ∀ (b : β), eqToHom ⋯ ≫ q b = q' b
⊢ map' p q = map' p' q'

Tactic:
by
  cat_disch

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

Goal state before:
pp: β : Type w
α : Type w₂
C : Type u
inst✝² : Category.{v, u} C
f : α → C
g : β → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct g
p p' : α → β
q : (a : α) → f a ⟶ g (p a)
q' : (a : α) → f a ⟶ g (p' a)
hp : p = p'
hq : ∀ (a : α), q a ≫ eqToHom ⋯ = q' a
⊢ map' p q = map' p' q'

Tactic:
by
  cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal X
c : BinaryFan X Y
⊢ Nonempty (IsLimit c) ↔ IsIso c.snd

Tactic:
refine Iff.trans ?_ (BinaryFan.isLimit_iff_isIso_fst h (BinaryFan.mk c.snd c.fst))

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal X
c : BinaryFan X Y
⊢ Nonempty (IsLimit c) ↔ Nonempty (IsLimit (mk c.snd c.fst))
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
inst✝¹ : HasBinaryProduct W Y
inst✝ : HasBinaryProduct X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift (fst ≫ g) (snd ≫ g') = map g g'

Tactic:
← prod.lift_map

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
inst✝¹ : HasBinaryProduct W Y
inst✝ : HasBinaryProduct X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift fst snd ≫ map g g' = map g g'
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProductsOfShape α C
a : α
⊢ (piEquivalenceFunctorDiscreteCompLim α).hom ≫ Pi.functorπ a =
    (piEquivalenceFunctorDiscrete α C).functor.whiskerLeft (lim.π { as := a }) ≫
      (piEquivalenceFunctorDiscreteCompEvaluationIso C a).hom

Tactic:
by
  cat_disch

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

Goal state before:
pp: α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasCoproductsOfShape α C
a : α
⊢ (piEquivalenceFunctorDiscrete α C).functor.whiskerLeft (colim.ι { as := a }) ≫
      (piEquivalenceFunctorDiscreteCompColim α).hom =
    (piEquivalenceFunctorDiscreteCompEvaluationIso C a).hom ≫ Sigma.functorι a

Tactic:
by
  cat_disch

Goal state after: