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

Goal state before:
pp: J : Type u₂
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : Discrete J ⥤ C} (f : X ⟶ Y),
    ({ 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 := ⋯ }).map
          f ≫
        (NatIso.ofComponents
            (fun 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
                      Y).obj
                  x))
            ⋯).hom =
      (NatIso.ofComponents
            (fun 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
                      X).obj
                  x))
            ⋯).hom ≫
        (𝟭 (Discrete J ⥤ C)).map f

Tactic:
by

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)
f : J → I
i' j' : J
h : i' = j'
⊢ (eqToEquivalence C ⋯).functor = (eqToEquivalence (fun i' ↦ C (f i')) h).functor

Tactic:
by

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:
by

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

Goal state before:
pp: C : Type u_1
⊢ ∀ {X Y : Discrete C} (f : X ⟶ Y), X = Y

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : IsDiscrete C
X Y : C
f : X ⟶ Y
⊢ f ≫ eqToHom ⋯ = 𝟙 X ∧ eqToHom ⋯ ≫ f = 𝟙 Y

Tactic:
by

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)
C' : Option J → Type u₁
inst✝ : (i : Option J) → Category.{v₁, u₁} (C' i)
⊢ (pi' fun i ↦
        match i with
        | none => Prod.fst (C' none) ((j : J) → C' (some j))
        | some i => Prod.snd (C' none) ((j : J) → C' (some j)) ⋙ eval (fun j ↦ C' (some j)) i) ⋙
      (eval C' none).prod' (pi' fun i ↦ eval C' (some i)) ≅
    𝟭 (C' none × ((j : J) → C' (some j)))

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : IsDiscrete C
⊢ ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), X = Y

Tactic:
by

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
⊢ NatTrans.op α.inv ≫ NatTrans.op α.hom = 𝟙 F.op

Tactic:
by

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

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

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

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

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

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

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
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:
by

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

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

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

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
⊢ (e.functor ⋙ f.functor).map
        ((e.unitIso ≪≫
                isoWhiskerRight
                    (e.functor.rightUnitor.symm ≪≫
                      e.functor.isoWhiskerLeft f.unitIso ≪≫ (e.functor.associator f.functor f.inverse).symm)
                    e.inverse ≪≫
                  (e.functor ⋙ f.functor).associator f.inverse e.inverse).hom.app
          X) ≫
      (((f.inverse ⋙ e.inverse).associator e.functor f.functor).symm ≪≫
              isoWhiskerRight
                  (f.inverse.associator e.inverse e.functor ≪≫
                    f.inverse.isoWhiskerLeft e.counitIso ≪≫ f.inverse.rightUnitor)
                  f.functor ≪≫
                f.counitIso).hom.app
        ((e.functor ⋙ f.functor).obj X) =
    𝟙 ((e.functor ⋙ f.functor).obj X)

Tactic:
by

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

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
⊢ (e.funInvIdAssoc F).hom.app X = F.map (e.unitInv.app X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

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
inst✝ : IsIso α
⊢ NatTrans.op α ≫ NatTrans.op (inv α) = 𝟙 G.op

Tactic:
by

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
⊢ (e.invFunIdAssoc F).hom.app X = F.map (e.counit.app X)

Tactic:
by

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) =
    𝟙 (e.functor.op.obj X)

Tactic:
by

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) =
    𝟙 (e.functor.unop.obj X)

Tactic:
by

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
⊢ ((whiskeringLeft D C E).obj e.inverse).map ((ofComponents (fun F ↦ (e.funInvIdAssoc F).symm) ⋯).hom.app F) ≫
      (ofComponents (fun F ↦ e.invFunIdAssoc F) ⋯).hom.app (((whiskeringLeft D C E).obj e.inverse).obj F) =
    𝟙 (((whiskeringLeft D C E).obj e.inverse).obj F)

Tactic:
by

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
X Y : C
f f' : X ⟶ Y
⊢ f ≫ e.unit.app Y = f' ≫ e.unit.app Y ↔ f = f'

Tactic:
by

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
X Y : C
f f' : X ⟶ e.inverse.obj (e.functor.obj Y)
⊢ f ≫ e.unitInv.app Y = f' ≫ e.unitInv.app Y ↔ f = f'

Tactic:
by

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
X Y : D
f f' : X ⟶ e.functor.obj (e.inverse.obj Y)
⊢ f ≫ e.counit.app Y = f' ≫ e.counit.app Y ↔ f = f'

Tactic:
by

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
X Y : D
f f' : X ⟶ Y
⊢ f ≫ e.counitInv.app Y = f' ≫ e.counitInv.app Y ↔ f = f'

Tactic:
by

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
W X X' Y : C
f : W ⟶ X
g : X ⟶ Y
f' : W ⟶ X'
g' : X' ⟶ Y
⊢ f ≫ g ≫ e.unit.app Y = f' ≫ g' ≫ e.unit.app Y ↔ f ≫ g = f' ≫ g'

Tactic:
by

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
W X X' Y : D
f : W ⟶ X
g : X ⟶ Y
f' : W ⟶ X'
g' : X' ⟶ Y
⊢ f ≫ g ≫ e.counitInv.app Y = f' ≫ g' ≫ e.counitInv.app Y ↔ f ≫ g = f' ≫ g'

Tactic:
by

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
W X X' Y Y' Z : C
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
f' : W ⟶ X'
g' : X' ⟶ Y'
h' : Y' ⟶ Z
⊢ f ≫ g ≫ h ≫ e.unit.app Z = f' ≫ g' ≫ h' ≫ e.unit.app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h'

Tactic:
by

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
⊢ ∀ {X Y : (C ⥤ D)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (C ⥤ D)ᵒᵖ).map f ≫ (unop Y).opUnopIso.op.hom = (unop X).opUnopIso.op.hom ≫ (opHom C D ⋙ opInv C D).map f

Tactic:
by

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
W X X' Y Y' Z : D
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
f' : W ⟶ X'
g' : X' ⟶ Y'
h' : Y' ⟶ Z
⊢ f ≫ g ≫ h ≫ e.counitInv.app Z = f' ≫ g' ≫ h' ≫ e.counitInv.app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h'

Tactic:
by

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
⊢ e.changeFunctor (Iso.refl e.functor) = e

Tactic:
by

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
G G' : C ⥤ D
iso₁ : e.functor ≅ G
iso₂ : G ≅ G'
⊢ (e.changeFunctor iso₁).changeFunctor iso₂ = e.changeFunctor (iso₁ ≪≫ iso₂)

Tactic:
by

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
G : D ⥤ C
iso : e.inverse ≅ G
X : C
⊢ e.functor.map ((e.unitIso ≪≫ e.functor.isoWhiskerLeft iso).hom.app X) ≫
      (isoWhiskerRight iso.symm e.functor ≪≫ e.counitIso).hom.app (e.functor.obj X) =
    𝟙 (e.functor.obj X)

Tactic:
by

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.preimage ((F.objObjPreimageIso X).hom ≫ 𝟙 X ≫ (F.objObjPreimageIso X).inv) = 𝟙 (F.objPreimage X)

Tactic:
by

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.preimage ((F.objObjPreimageIso X).hom ≫ (f ≫ g) ≫ (F.objObjPreimageIso Z).inv) =
    F.preimage ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv) ≫
      F.preimage ((F.objObjPreimageIso Y).hom ≫ g ≫ (F.objObjPreimageIso Z).inv)

Tactic:
by

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
⊢ ∀ {X Y : (Cᵒᵖ ⥤ D)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (Cᵒᵖ ⥤ D)ᵒᵖ).map f ≫ (unop Y).rightOpLeftOpIso.op.hom =
      (unop X).rightOpLeftOpIso.op.hom ≫
        ({ obj := fun F ↦ (unop F).rightOp, map := fun {X Y} η ↦ NatTrans.rightOp η.unop, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun F ↦ op F.leftOp, map := fun {X Y} η ↦ (NatTrans.leftOp η).op, map_id := ⋯,
                map_comp := ⋯ }).map
          f

Tactic:
by

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✝ : 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:
by

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:
by

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_1
inst✝² : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : G.IsEquivalence
inst✝ : (F ⋙ G).IsEquivalence
⊢ F.IsEquivalence

Tactic:
by

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_1
inst✝² : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsEquivalence
inst✝ : (F ⋙ G).IsEquivalence
⊢ G.IsEquivalence

Tactic:
by

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
C' : Type u_1
e : C' ≃ D
Y : D
⊢ Nonempty ((inducedFunctor ⇑e).obj (e.symm Y) ≅ Y)

Tactic:
by

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
G G' : C ≌ D
i : G.functor ≅ G'.functor
⊢ i.isoInverseOfIsoFunctor.isoFunctorOfIsoInverse = i

Tactic:
by

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:
by

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:
by

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

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f : Arrow T
⊢ mk f.hom = f

Tactic:
by

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✝
⊢ Quiver.reverse (Quiver.reverse f) = f

Tactic:
by

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

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
A B : T
f g : A ⟶ B
h : mk f = mk g
⊢ f = g

Tactic:
by

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

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
φ₁ φ₂ : f ⟶ g
h : φ₁ = φ₂
⊢ Hom.left φ₁ = Hom.left φ₂

Tactic:
by

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

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ g.hom = Hom.left e.inv ≫ f.hom ≫ Hom.right e.hom

Tactic:
by

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:
by

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

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y : Arrow T
h : X = Y
⊢ X.left = Y.left

Tactic:
by

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

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y : Arrow T
h : X = Y
⊢ Hom.left (eqToHom h) = eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y : Arrow T
h : X = Y
⊢ X.right = Y.right

Tactic:
by

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✝
⊢ h.preimage (inv (F.map f)) ≫ f = 𝟙 Y✝

Tactic:
by

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

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y : Arrow T
h : X = Y
⊢ Hom.right (eqToHom h) = eqToHom ⋯

Tactic:
by

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 ≫ h.preimage (inv (F.map f)) = 𝟙 X✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: I : Type u
J : I → Type u₂
inst✝ : (i : I) → Groupoid (J i)
X✝ Y✝ : (i : I) → J i
f : X✝ ⟶ Y✝
⊢ (fun i ↦ Groupoid.inv (f i)) ≫ f = 𝟙 Y✝

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
W W' : MorphismProperty C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f
⊢ W = W'

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y : C
f : X ⟶ Y
⊢ ⊤ f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
P : MorphismProperty C
h : P = ⊤
X Y : C
f : X ⟶ Y
⊢ P f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
S : Set (MorphismProperty C)
X Y : C
f : X ⟶ Y
⊢ sSup S f ↔ ∃ W ∈ S, W f

Tactic:
by

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

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
⊢ mk f = mk f' ↔ ∃ hX hY, f = eqToHom hX ≫ f' ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: I : Type u
J : I → Type u₂
inst✝ : (i : I) → Groupoid (J i)
X✝ Y✝ : (i : I) → J i
f : X✝ ⟶ Y✝
⊢ (f ≫ fun i ↦ Groupoid.inv (f i)) = 𝟙 X✝

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Sort u_1
W : ι → MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ iSup W f ↔ ∃ i, W i f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
S : Set (MorphismProperty C)
X Y : C
f : X ⟶ Y
⊢ sInf S f ↔ ∀ W ∈ S, W f

Tactic:
by

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

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
h₁ : f.left = g.left
h₂ : f.right = g.right
h₃ : f.hom = eqToHom h₁ ≫ g.hom ≫ eqToHom ⋯
⊢ ∃ hX hY, f.hom = eqToHom hX ≫ g.hom ≫ eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ iInf W f ↔ ∀ (i : ι), W i f

Tactic:
by

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:
by

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 D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ P.inverseImage F f ↔ P (F.map f)

Tactic:
by

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:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.strictMap (𝟭 C) = P

Tactic:
by

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

Goal state before:
pp: T : Type u
inst✝² : Category.{v, u} T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso (Hom.left ff)
inst✝ : IsIso (Hom.right ff)
⊢ ff ≫ homMk (inv (Hom.left ff)) (inv (Hom.right ff)) ⋯ = 𝟙 f ∧
    homMk (inv (Hom.left ff)) (inv (Hom.right ff)) ⋯ ≫ ff = 𝟙 g

Tactic:
by

Goal state after: