awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ (F.mapIso (η.app X)).hom ≫ (F.mapIso (η.app X)).inv = 𝟙 (F.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X))

Tactic:
have := (F.mapIso <| η.app X).hom_inv_id
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this : F.map (η.hom.app X) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
rw rw₁ : Eq.{v₂ + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X)) (𝟙 (F.obj X))
⊢ F.map (η.hom.app X) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
⊢ mkHom (𝟙 e.inverse) = 𝟙 e.symm

Tactic:
rfl

Premises used: rfl, CategoryTheory.Equivalence.mkHom
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
⊢ e.symm.counit = e.unitInv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
⊢ e.symm.unit = e.counitInv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
e : Equivalence.{v₁, v₂, u₁, u₂} C D
f : Equivalence.{v₂, v₃, u₂, u₃} D E
X : C
dsimp :
  f.functor.map
        (e.functor.map
          (e.unitIso.hom.app X ≫
            e.inverse.map
                (𝟙 (e.functor.obj X) ≫
                  f.unitIso.hom.app (e.functor.obj X) ≫ 𝟙 (f.inverse.obj (f.functor.obj (e.functor.obj X)))) ≫
              𝟙 (e.inverse.obj (f.inverse.obj (f.functor.obj (e.functor.obj X)))))) ≫
      𝟙 (f.functor.obj (e.functor.obj (e.inverse.obj (f.inverse.obj (f.functor.obj (e.functor.obj X)))))) ≫
        f.functor.map
            (𝟙 (e.functor.obj (e.inverse.obj (f.inverse.obj (f.functor.obj (e.functor.obj X))))) ≫
              e.counitIso.hom.app (f.inverse.obj (f.functor.obj (e.functor.obj X))) ≫
                𝟙 (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))
⊢ (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:
dsimp
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
e : Equivalence.{v₁, v₂, u₁, u₂} C D
f : Equivalence.{v₂, v₃, u₂, u₃} D E
X : C
simp :
  f.functor.map (f.unitIso.hom.app (e.functor.obj X)) ≫
      f.functor.map (e.counitIso.inv.app (f.inverse.obj (f.functor.obj (e.functor.obj X)))) ≫
        f.functor.map (e.counitIso.hom.app (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))
⊢ f.functor.map
        (e.functor.map
          (e.unitIso.hom.app X ≫
            e.inverse.map
                (𝟙 (e.functor.obj X) ≫
                  f.unitIso.hom.app (e.functor.obj X) ≫ 𝟙 (f.inverse.obj (f.functor.obj (e.functor.obj X)))) ≫
              𝟙 (e.inverse.obj (f.inverse.obj (f.functor.obj (e.functor.obj X)))))) ≫
      𝟙 (f.functor.obj (e.functor.obj (e.inverse.obj (f.inverse.obj (f.functor.obj (e.functor.obj X)))))) ≫
        f.functor.map
            (𝟙 (e.functor.obj (e.inverse.obj (f.inverse.obj (f.functor.obj (e.functor.obj X))))) ≫
              e.counitIso.hom.app (f.inverse.obj (f.functor.obj (e.functor.obj X))) ≫
                𝟙 (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 only [comp_id, id_comp, map_comp, fun_inv_map, comp_obj, id_obj, counitInv,
      functor_unit_comp_assoc, assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Equivalence.counitInv, CategoryTheory.Category.comp_id, CategoryTheory.Equivalence.fun_inv_map, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp, CategoryTheory.Equivalence.functor_unit_comp_assoc
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
e : Equivalence.{v₁, v₂, u₁, u₂} C D
f : Equivalence.{v₂, v₃, u₂, u₃} D E
X : C
a : f.functor.map (𝟙 (obj.{v₂, v₂, u₂, u₂} (𝟭 D) (f.inverse.obj (f.functor.obj (e.functor.obj X)))))
| f.functor.map (e.counitIso.inv.app (f.inverse.obj (f.functor.obj (e.functor.obj X)))) ≫
    f.functor.map (e.counitIso.hom.app (f.inverse.obj (f.functor.obj (e.functor.obj X))))

Tactic:
rw [← Functor.map_comp, Iso.inv_hom_id_app]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
e : Equivalence.{v₁, v₂, u₁, u₂} C D
f : Equivalence.{v₂, v₃, u₂, u₃} D E
X : C
slice_lhs :
  f.functor.map (f.unitIso.hom.app (e.functor.obj X)) ≫
      f.functor.map (𝟙 (obj.{v₂, v₂, u₂, u₂} (𝟭 D) (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))
⊢ f.functor.map (f.unitIso.hom.app (e.functor.obj X)) ≫
      f.functor.map (e.counitIso.inv.app (f.inverse.obj (f.functor.obj (e.functor.obj X)))) ≫
        f.functor.map (e.counitIso.hom.app (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:
slice_lhs 2 3 => rw [← Functor.map_comp, Iso.inv_hom_id_app]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
e : Equivalence.{v₁, v₂, u₁, u₂} C D
f : Equivalence.{v₂, v₃, u₂, u₃} D E
X : C
⊢ f.functor.map (f.unitIso.hom.app (e.functor.obj X)) ≫
      f.functor.map (𝟙 (obj.{v₂, v₂, u₂, u₂} (𝟭 D) (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
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
e : Equivalence.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₁, v₃, u₁, u₃} C E
X : C
dsimp :
  𝟙 (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)
⊢ (e.funInvIdAssoc F).hom.app X = F.map (e.unitInv.app X)

Tactic:
dsimp [funInvIdAssoc]

Premises used: CategoryTheory.Equivalence.funInvIdAssoc
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
e : Equivalence.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₁, v₃, u₁, u₃} 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
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
e : Equivalence.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₃, u₂, u₃} D E
X : D
dsimp :
  𝟙 (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)
⊢ (e.invFunIdAssoc F).hom.app X = F.map (e.counit.app X)

Tactic:
dsimp [invFunIdAssoc]

Premises used: CategoryTheory.Equivalence.invFunIdAssoc
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
e : Equivalence.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₃, u₂, u₃} 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
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
e : Equivalence.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₁, v₃, u₁, u₃} C E
w :
  ∀ (X : D),
    NatTrans.app
        (CategoryStruct.comp (Y :=
          obj (obj (whiskeringLeft D C E) e.inverse)
            (obj (obj (whiskeringLeft C D E) e.functor) (obj (obj (whiskeringLeft D C E) e.inverse) F)))
          (map (obj (whiskeringLeft D C E) e.inverse)
            (NatTrans.app (Iso.hom (ofComponents (fun (F : Functor.{v₁, v₃, u₁, u₃} C E) ↦ (e.funInvIdAssoc F).symm) ⋯))
              F))
          (NatTrans.app (Iso.hom (ofComponents (fun (F : Functor.{v₂, v₃, u₂, u₃} D E) ↦ e.invFunIdAssoc F) ⋯))
            (obj (obj (whiskeringLeft D C E) e.inverse) F)))
        X =
      NatTrans.app (𝟙 (obj (obj (whiskeringLeft D C E) e.inverse) F)) X
⊢ Eq (α := obj (obj (whiskeringLeft D C E) e.inverse) F ⟶ obj (obj (whiskeringLeft D C E) e.inverse) F)
    (CategoryStruct.comp (Y :=
        obj (obj (whiskeringLeft D C E) e.inverse)
          (obj (obj (whiskeringLeft C D E) e.functor) (obj (obj (whiskeringLeft D C E) e.inverse) F)))
        (map (obj (whiskeringLeft D C E) e.inverse)
          (NatTrans.app (Iso.hom (ofComponents (fun (F : Functor.{v₁, v₃, u₁, u₃} C E) ↦ (e.funInvIdAssoc F).symm) ⋯))
            F))
        (NatTrans.app (Iso.hom (ofComponents (fun (F : Functor.{v₂, v₃, u₂, u₃} D E) ↦ e.invFunIdAssoc F) ⋯))
          (obj (obj (whiskeringLeft D C E) e.inverse) F)) :
      obj (obj (whiskeringLeft D C E) e.inverse) F ⟶ obj (obj (whiskeringLeft D C E) e.inverse) F)
    (𝟙 (obj (obj (whiskeringLeft D C E) e.inverse) F) :
      obj (obj (whiskeringLeft D C E) e.inverse) F ⟶ obj (obj (whiskeringLeft D C E) e.inverse) F)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
e : Equivalence.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₁, v₃, u₁, u₃} C E
X : D
w :
  (e.funInvIdAssoc F).inv.app (e.inverse.obj X) ≫ (e.invFunIdAssoc (e.inverse ⋙ F)).hom.app X =
    𝟙 (F.obj (e.inverse.obj X))
⊢ NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (obj (whiskeringLeft D C E) e.inverse)
          (obj (obj (whiskeringLeft C D E) e.functor) (obj (obj (whiskeringLeft D C E) e.inverse) F)))
        (map (obj (whiskeringLeft D C E) e.inverse)
          (NatTrans.app (Iso.hom (ofComponents (fun (F : Functor.{v₁, v₃, u₁, u₃} C E) ↦ (e.funInvIdAssoc F).symm) ⋯))
            F))
        (NatTrans.app (Iso.hom (ofComponents (fun (F : Functor.{v₂, v₃, u₂, u₃} D E) ↦ e.invFunIdAssoc F) ⋯))
          (obj (obj (whiskeringLeft D C E) e.inverse) F)))
      X =
    NatTrans.app (𝟙 (obj (obj (whiskeringLeft D C E) e.inverse) F)) X

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
e : Equivalence.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₁, v₃, u₁, u₃} C E
X : D
⊢ (e.funInvIdAssoc F).inv.app (e.inverse.obj X) ≫ (e.invFunIdAssoc (e.inverse ⋙ F)).hom.app X =
    𝟙 (F.obj (e.inverse.obj X))

Tactic:
simp only [funInvIdAssoc_inv_app, id_obj, comp_obj, invFunIdAssoc_hom_app,
      Functor.comp_map, ← F.map_comp, unit_inverse_comp, map_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Equivalence.invFunIdAssoc_hom_app, CategoryTheory.Functor.map_id, CategoryTheory.Functor.id_obj, CategoryTheory.Equivalence.unit_inverse_comp, CategoryTheory.Functor.map_comp, CategoryTheory.Equivalence.funInvIdAssoc_inv_app, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
X Y : C
f f' : X ⟶ Y
⊢ f ≫ e.unit.app Y = f' ≫ e.unit.app Y ↔ f = f'

Tactic:
simp only [cancel_mono]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} 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:
simp only [cancel_mono]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} 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:
simp only [cancel_mono]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
X Y : D
f f' : X ⟶ Y
⊢ f ≫ e.counitInv.app Y = f' ≫ e.counitInv.app Y ↔ f = f'

Tactic:
simp only [cancel_mono]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} 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:
simp only [← Category.assoc, cancel_mono]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} 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:
simp only [← Category.assoc, cancel_mono]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} 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:
simp only [← Category.assoc, cancel_mono]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} 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:
simp only [← Category.assoc, cancel_mono]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
e : Equivalence.{v₁, v₁, u₁, u₁} C C
⊢ HPow.hPow (β := ℤ) e 0 = refl

Tactic:
rfl

Premises used: CategoryTheory.Equivalence.refl, CategoryTheory.Equivalence.pow, CategoryTheory.Equivalence.powNat, rfl
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
e : Equivalence.{v₁, v₁, u₁, u₁} C C
⊢ HPow.hPow (β := ℤ) e 1 = e

Tactic:
rfl

Premises used: CategoryTheory.Equivalence.pow, CategoryTheory.Equivalence.powNat, rfl
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
e : Equivalence.{v₁, v₁, u₁, u₁} C C
⊢ HPow.hPow (β := ℤ) e (-1) = e.symm

Tactic:
rfl

Premises used: CategoryTheory.Equivalence.pow, CategoryTheory.Equivalence.powNat, CategoryTheory.Equivalence.symm, rfl
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
e : Equivalence.{v₁, v₃, u₁, u₃} C E
⊢ e.functor.EssSurj

Tactic:
⟨fun Y => ⟨e.inverse.obj Y, ⟨e.counitIso.app Y⟩⟩⟩

Premises used: CategoryTheory.Functor.EssSurj.mk, Nonempty.intro, Exists.intro, CategoryTheory.Iso.app, CategoryTheory.Functor.obj, CategoryTheory.Equivalence.counitIso, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
e : Equivalence.{v₁, v₃, u₁, u₃} C E
⊢ e.inverse.EssSurj

Tactic:
e.symm.essSurj_functor

Premises used: CategoryTheory.Equivalence.essSurj_functor, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
e : Equivalence.{v₁, v₃, u₁, u₃} C E
⊢ e.functor.Faithful

Tactic:
e.fullyFaithfulFunctor.faithful

Premises used: CategoryTheory.Equivalence.fullyFaithfulFunctor, CategoryTheory.Functor.FullyFaithful.faithful
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
e : Equivalence.{v₁, v₃, u₁, u₃} C E
⊢ e.inverse.Faithful

Tactic:
e.fullyFaithfulInverse.faithful

Premises used: CategoryTheory.Equivalence.fullyFaithfulInverse, CategoryTheory.Functor.FullyFaithful.faithful
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
e : Equivalence.{v₁, v₃, u₁, u₃} C E
⊢ e.functor.Full

Tactic:
e.fullyFaithfulFunctor.full

Premises used: CategoryTheory.Equivalence.fullyFaithfulFunctor, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
e : Equivalence.{v₁, v₃, u₁, u₃} C E
⊢ e.inverse.Full

Tactic:
e.fullyFaithfulInverse.full

Premises used: CategoryTheory.Equivalence.fullyFaithfulInverse, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
e : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
iso : e.inverse ≅ G
X : C
dsimp :
  e.functor.map (e.unitIso.hom.app X ≫ iso.hom.app (e.functor.obj X)) ≫
      e.functor.map (iso.inv.app (e.functor.obj X)) ≫ e.counitIso.hom.app (e.functor.obj X) =
    𝟙 (e.functor.obj X)
⊢ 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:
dsimp
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
e : Equivalence.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
iso : e.inverse ≅ G
X : C
rw :
  e.functor.map ((e.unitIso.hom.app X ≫ iso.hom.app (e.functor.obj X)) ≫ iso.inv.app (e.functor.obj X)) ≫
      e.counitIso.hom.app (e.functor.obj X) =
    𝟙 (e.functor.obj X)
rw₁ :
  e.functor.map (e.unitIso.hom.app X ≫ iso.hom.app (e.functor.obj X) ≫ iso.inv.app (e.functor.obj X)) ≫
      e.counitIso.hom.app (e.functor.obj X) =
    𝟙 (e.functor.obj X)
rw₂ :
  e.functor.map (e.unitIso.hom.app X ≫ 𝟙 (e.inverse.obj (e.functor.obj X))) ≫ e.counitIso.hom.app (e.functor.obj X) =
    𝟙 (e.functor.obj X)
rw₃ : e.functor.map (e.unitIso.hom.app X) ≫ e.counitIso.hom.app (e.functor.obj X) = 𝟙 (e.functor.obj X)
rw₄ rw₅ : Eq.{v₂ + 1} (α := e.functor.obj X ⟶ e.functor.obj X) (𝟙 (e.functor.obj X)) (𝟙 (e.functor.obj X))
⊢ e.functor.map (e.unitIso.hom.app X ≫ iso.hom.app (e.functor.obj X)) ≫
      e.functor.map (iso.inv.app (e.functor.obj X)) ≫ e.counitIso.hom.app (e.functor.obj X) =
    𝟙 (e.functor.obj X)

Tactic:
rw [← map_comp_assoc, assoc, iso.hom_inv_id_app, comp_id, functor_unit_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Equivalence.functor_unit_comp, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp_assoc
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Equivalence.{v₁, v₂, u₁, u₂} C D
⊢ F.inverse.IsEquivalence

Tactic:
F.symm.isEquivalence_functor

Premises used: CategoryTheory.Equivalence.isEquivalence_functor, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
⊢ F.IsEquivalence

Tactic:
inferInstanceAs (IsEquivalence (Equivalence.mk F G η ε).functor)

Premises used: _private.0.CategoryTheory.Functor.IsEquivalence.mk'._proof_1
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.IsEquivalence
X : D
a :
  F.map (F.preimage (Iso.hom (F.objObjPreimageIso X) ≫ 𝟙 X ≫ Iso.inv (F.objObjPreimageIso X))) =
    F.map (𝟙 (F.objPreimage X))
⊢ F.preimage (Iso.hom (F.objObjPreimageIso X) ≫ 𝟙 X ≫ Iso.inv (F.objObjPreimageIso X)) = 𝟙 (F.objPreimage X)

Tactic:
apply F.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.IsEquivalence
X : D
⊢ F.map (F.preimage (Iso.hom (F.objObjPreimageIso X) ≫ 𝟙 X ≫ Iso.inv (F.objObjPreimageIso X))) =
    F.map (𝟙 (F.objPreimage X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.IsEquivalence
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
a :
  Eq (α := F.obj (F.objPreimage X) ⟶ F.obj (F.objPreimage Z))
    (F.map (F.preimage (Iso.hom (F.objObjPreimageIso X) ≫ (f ≫ g) ≫ Iso.inv (F.objObjPreimageIso Z))))
    (F.map
      (CategoryStruct.comp (Y := F.objPreimage Y)
        (F.preimage (Iso.hom (F.objObjPreimageIso X) ≫ f ≫ Iso.inv (F.objObjPreimageIso Y)))
        (F.preimage (Iso.hom (F.objObjPreimageIso Y) ≫ g ≫ Iso.inv (F.objObjPreimageIso Z)))))
⊢ Eq (α := F.objPreimage X ⟶ F.objPreimage Z)
    (F.preimage (Iso.hom (F.objObjPreimageIso X) ≫ (f ≫ g) ≫ Iso.inv (F.objObjPreimageIso Z)))
    (CategoryStruct.comp (Y := F.objPreimage Y)
      (F.preimage (Iso.hom (F.objObjPreimageIso X) ≫ f ≫ Iso.inv (F.objObjPreimageIso Y)))
      (F.preimage (Iso.hom (F.objObjPreimageIso Y) ≫ g ≫ Iso.inv (F.objObjPreimageIso Z))))

Tactic:
apply F.map_injective

Premises used: CategoryTheory.Functor.map_injective