awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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)
⊢ F.map (η.hom.app X) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
have rw : Eq.{v₂ + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X)) (𝟙 (F.obj X))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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
⊢ (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)
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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
        (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))
have 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))
Tactic: simp only [comp_id, id_comp, map_comp, fun_inv_map, comp_obj, id_obj, counitInv,
      functor_unit_comp_assoc, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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 (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))))
have a : f.functor.map (𝟙 (obj.{v₂, v₂, u₂, u₂} (𝟭 D) (f.inverse.obj (f.functor.obj (e.functor.obj X)))))
Tactic: rw [← Functor.map_comp, Iso.inv_hom_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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 (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))
have 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))
Tactic: slice_lhs 2 3 => rw [← Functor.map_comp, Iso.inv_hom_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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
⊢ (e.funInvIdAssoc F).hom.app X = F.map (e.unitInv.app X)
have 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)
Tactic: dsimp [funInvIdAssoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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
⊢ (e.invFunIdAssoc F).hom.app X = F.map (e.counit.app X)
have 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)
Tactic: dsimp [invFunIdAssoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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
⊢ 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)
have 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) sorry))
            F))
        (NatTrans.app (Iso.hom (ofComponents (fun (F : Functor.{v₂, v₃, u₂, u₃} D E) ↦ e.invFunIdAssoc F) sorry))
          (obj (obj (whiskeringLeft D C E) e.inverse) F)))
      X =
    NatTrans.app (𝟙 (obj (obj (whiskeringLeft D C E) e.inverse) F)) X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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
⊢ 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
have w : (e.funInvIdAssoc F).inv.app (e.inverse.obj X) ≫ (e.invFunIdAssoc (e.inverse ⋙ F)).hom.app X =
  𝟙 (F.obj (e.inverse.obj X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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
⊢ 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)
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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
⊢ 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)
have 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)
Tactic: rw [← map_comp_assoc, assoc, iso.hom_inv_id_app, comp_id, functor_unit_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← map_comp_assoc, assoc, iso.hom_inv_id_app, comp_id, functor_unit_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← map_comp_assoc, assoc, iso.hom_inv_id_app, comp_id, functor_unit_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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)
⊢ 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)
have rw₃ : e.functor.map (e.unitIso.hom.app 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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)
⊢ 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)
have rw₄ : Eq.{v₂ + 1} (α := e.functor.obj X ⟶ e.functor.obj X) (𝟙 (e.functor.obj X)) (𝟙 (e.functor.obj X))
Tactic: rw [← map_comp_assoc, assoc, iso.hom_inv_id_app, comp_id, functor_unit_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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.preimage (Iso.hom (F.objObjPreimageIso X) ≫ 𝟙 X ≫ Iso.inv (F.objObjPreimageIso X)) = 𝟙 (F.objPreimage X)
have a : F.map (F.preimage (Iso.hom (F.objObjPreimageIso X) ≫ 𝟙 X ≫ Iso.inv (F.objObjPreimageIso X))) =
  F.map (𝟙 (F.objPreimage X))
Tactic: apply F.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
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
⊢ 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))))
have 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)))))
Tactic: apply F.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v_1, u₂, u_1} D E
inst_3 : G.IsEquivalence
inst_4 : (F ⋙ G).IsEquivalence
⊢ F.IsEquivalence
have rw : (F ⋙ G.asEquivalence.functor ⋙ G.asEquivalence.inverse).IsEquivalence
Tactic: rw [isEquivalence_iff_of_iso (F.rightUnitor.symm ≪≫ isoWhiskerLeft F (G.asEquivalence.unitIso))]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v_1, u₂, u_1} D E
inst_3 : F.IsEquivalence
inst_4 : (F ⋙ G).IsEquivalence
⊢ G.IsEquivalence
have rw : ((F.asEquivalence.inverse ⋙ F.asEquivalence.functor) ⋙ G).IsEquivalence
Tactic: rw [isEquivalence_iff_of_iso (G.leftUnitor.symm ≪≫
    isoWhiskerRight F.asEquivalence.counitIso.symm G)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Equivalence (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G G' : Equivalence.{v₁, v₂, u₁, u₂} C D
i : G.functor ≅ G'.functor
⊢ i.isoInverseOfIsoFunctor.isoFunctorOfIsoInverse = i
have w : ∀ (X : C), i.isoInverseOfIsoFunctor.isoFunctorOfIsoInverse.hom.app X = i.hom.app X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentialImage (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
h : Function.Surjective F.obj
Y : D
⊢ F.essImage Y
have obtain : ∀ (X : C), F.essImage (F.obj X)
Tactic: obtain ⟨X, rfl⟩ := h Y
Cleared hypotheses: Y
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentialImage (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : ObjectProperty.{v₁, u₁} C
⊢ (P.ι ⋙ F).essImage = P.map F
have h : ∀ (Y : D), (P.ι ⋙ F).essImage Y ↔ P.map F Y
Tactic: ext Y
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentialImage (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : ObjectProperty.{v₁, u₁} C
Y : D
⊢ (P.ι ⋙ F).essImage Y ↔ P.map F Y
have h : (P.ι ⋙ F).essImage Y → P.map F Y
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentialImage (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : ObjectProperty.{v₁, u₁} C
Y : D
h : (P.ι ⋙ F).essImage Y → P.map F Y
⊢ (P.ι ⋙ F).essImage Y ↔ P.map F Y
have h₁ : P.map F Y → (P.ι ⋙ F).essImage Y
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentialImage (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₂, v₃, u₂, u₃} D E
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : L.EssSurj
h : ∀ ⦃X₁ X₂ : C⦄ (φ : F.obj (L.obj X₁) ⟶ F.obj (L.obj X₂)), ∃ (f : L.obj X₁ ⟶ L.obj X₂), F.map f = φ
X₁ X₂ : D
ψ : F.obj X₁ ⟶ F.obj X₂
⊢ ∃ (a : X₁ ⟶ X₂), F.map a = ψ
have obtain : ∀ (f : L.obj (L.objPreimage X₁) ⟶ L.obj (L.objPreimage X₂))
  (hf : F.map f = F.map (Iso.hom (L.objObjPreimageIso X₁)) ≫ ψ ≫ F.map (Iso.inv (L.objObjPreimageIso X₂))),
  ∃ (a : X₁ ⟶ X₂), F.map a = ψ
Tactic: obtain ⟨f, hf⟩ := h (F.map (L.objObjPreimageIso X₁).hom ≫ ψ ≫
    F.map (L.objObjPreimageIso X₂).inv)
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentialImage (goal)
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₂, v₃, u₂, u₃} D E
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : L.EssSurj
h : ∀ ⦃X₁ X₂ : C⦄ (f g : L.obj X₁ ⟶ L.obj X₂), F.map f = F.map g → f = g
X Y : D
a₁ a₂ : X ⟶ Y
hfg : F.map a₁ = F.map a₂
⊢ a₁ = a₂
have rw : Eq (α := L.obj (L.objPreimage X) ⟶ L.obj (L.objPreimage Y))
  (Iso.hom (L.objObjPreimageIso X) ≫ a₁ ≫ Iso.inv (L.objObjPreimageIso Y))
  (Iso.hom (L.objObjPreimageIso X) ≫ a₂ ≫ Iso.inv (L.objObjPreimageIso Y))
Tactic: rw [← cancel_mono (L.objObjPreimageIso _).inv, ← cancel_epi (L.objObjPreimageIso _).hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentiallySmall (goal)
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
⊢ EssentiallySmall.{w, v, u} C ↔ EssentiallySmall.{w, v', u'} D
have mp : EssentiallySmall.{w, v, u} C → EssentiallySmall.{w, v', u'} D
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentiallySmall (goal)
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
mp : EssentiallySmall.{w, v, u} C → EssentiallySmall.{w, v', u'} D
⊢ EssentiallySmall.{w, v, u} C ↔ EssentiallySmall.{w, v', u'} D
have mpr : EssentiallySmall.{w, v', u'} D → EssentiallySmall.{w, v, u} C
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentiallySmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ EssentiallySmall.{w, v, u} C ↔ Small.{w, u} (Skeleton.{v, u} C) ∧ LocallySmall.{w, v, u} C
have mp : EssentiallySmall.{w, v, u} C → Small.{w, u} (Skeleton.{v, u} C) ∧ LocallySmall.{w, v, u} C
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentiallySmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
mp : EssentiallySmall.{w, v, u} C → Small.{w, u} (Skeleton.{v, u} C) ∧ LocallySmall.{w, v, u} C
⊢ EssentiallySmall.{w, v, u} C ↔ Small.{w, u} (Skeleton.{v, u} C) ∧ LocallySmall.{w, v, u} C
have mpr : Small.{w, u} (Skeleton.{v, u} C) ∧ LocallySmall.{w, v, u} C → EssentiallySmall.{w, v, u} C
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentiallySmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : EssentiallySmall.{w, v, u} C
⊢ Small.{w, u} (Skeleton.{v, u} C) ∧ LocallySmall.{w, v, u} C
have mp : Small.{w, u} (Skeleton.{v, u} C)
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentiallySmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : EssentiallySmall.{w, v, u} C
mp : Small.{w, u} (Skeleton.{v, u} C)
⊢ Small.{w, u} (Skeleton.{v, u} C) ∧ LocallySmall.{w, v, u} C
have mp₁ : LocallySmall.{w, v, u} C
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentiallySmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : EssentiallySmall.{w, v, u} C
⊢ Small.{w, u} (Skeleton.{v, u} C)
have mp : ∀ (S : Type w) (𝒮 : SmallCategory S) (e : Equivalence.{v, w, u, w} C S), Small.{w, u} (Skeleton.{v, u} C)
Tactic: rcases h with ⟨S, 𝒮, ⟨e⟩⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentiallySmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
S : Type w
𝒮 : SmallCategory S
e : Equivalence.{v, w, u, w} C S
⊢ Small.{w, u} (Skeleton.{v, u} C)
have mp : Equiv.{u + 1, w + 1} (Skeleton.{v, u} C) (Skeleton S)
Tactic: refine ⟨⟨Skeleton S, ⟨?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.EssentiallySmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
inst_2 : LocallySmall.{w, v, u} C
φ : (f : Arrow.{v, u} C) → (s : C) × (t : C) × (s ⟶ t) :=
  fun (f : Arrow.{v, u} C) ↦
    Sigma.mk (β := fun (s : C) ↦ (t : C) × (s ⟶ t)) f.left (Sigma.mk (β := fun (t : C) ↦ f.left ⟶ t) f.right f.hom)
⊢ Small.{w, max u v} (Arrow.{v, u} C)
have refine : Function.Injective φ
Tactic: refine small_of_injective (f := φ) ?_