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
inst_2 : F.IsEquivalence
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ 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:
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 : C
f : X ⟶ Y
⊢ Eq (α := F.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) ⟶ F.obj ((F ⋙ F.inv).obj Y))
    (F.map
      (map (𝟭 C) f ≫
        Iso.hom
          ((fun (X : C) ↦ (Iso.symm (F.preimageIso (F.objObjPreimageIso (F.obj X))) : X ≅ F.objPreimage (F.obj X))) Y)))
    (F.map
      (Iso.hom
          ((fun (X : C) ↦ (Iso.symm (F.preimageIso (F.objObjPreimageIso (F.obj X))) : X ≅ F.objPreimage (F.obj X))) X) ≫
        (F ⋙ F.inv).map f))

Tactic:
simp [inv]

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

Tactic:
simp [inv]

Premises used: CategoryTheory.Functor.inv
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
⊢ IsEquivalence.{v₁, v₁, u₁, u₁} (𝟭 C)

Tactic:
Equivalence.refl.isEquivalence_functor

Premises used: CategoryTheory.Equivalence.refl, CategoryTheory.Functor.id, CategoryTheory.Equivalence.isEquivalence_functor
-- 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
⊢ F.inv.IsEquivalence

Tactic:
F.asEquivalence.symm.isEquivalence_functor

Premises used: CategoryTheory.Functor.asEquivalence, CategoryTheory.Equivalence.isEquivalence_functor, CategoryTheory.Functor.inv, 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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.IsEquivalence
⊢ IsEquivalence (C := Functor.{v₂, v₃, u₂, u₃} D E) (obj (whiskeringLeft C D E) F)

Tactic:
inferInstanceAs <| IsEquivalence (Equivalence.congrLeft F.asEquivalence).inverse

Premises used: _private.0.CategoryTheory.Functor.instIsEquivalenceObjWhiskeringLeft._proof_1
-- 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
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.IsEquivalence
⊢ IsEquivalence (C := Functor.{v₃, v₁, u₃, u₁} E C) (obj (whiskeringRight E C D) F)

Tactic:
inferInstanceAs <| IsEquivalence (Equivalence.congrRight F.asEquivalence).functor

Premises used: _private.0.CategoryTheory.Functor.instIsEquivalenceObjWhiskeringRight._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 Y : D
f : X ⟶ Y
⊢ F.map (F.inv.map f) = F.asEquivalence.counit.app X ≫ f ≫ F.asEquivalence.counitInv.app Y

Tactic:
simpa using (NatIso.naturality_2 (α := F.asEquivalence.counitIso) (f := f)).symm

Premises used: CategoryTheory.Functor.asEquivalence, CategoryTheory.NatIso.naturality_2, Eq.symm, CategoryTheory.Equivalence.counitIso
-- 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 : C
f : X ⟶ Y
⊢ F.inv.map (F.map f) = F.asEquivalence.unitInv.app X ≫ f ≫ F.asEquivalence.unit.app Y

Tactic:
simpa using (NatIso.naturality_1 (α := F.asEquivalence.unitIso) (f := f)).symm

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.NatIso.naturality_1, CategoryTheory.Functor.asEquivalence, Eq.symm
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
e : F ≅ G
inst_2 : F.IsEquivalence
⊢ G.IsEquivalence

Tactic:
((asEquivalence F).changeFunctor e).isEquivalence_functor

Premises used: CategoryTheory.Functor.asEquivalence, CategoryTheory.Equivalence.isEquivalence_functor, CategoryTheory.Equivalence.changeFunctor
-- Module: Mathlib.CategoryTheory.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
e : F ≅ G
⊢ F.IsEquivalence ↔ G.IsEquivalence

Tactic:
⟨fun _ => isEquivalence_of_iso e, fun _ => isEquivalence_of_iso e.symm⟩

Premises used: CategoryTheory.Functor.isEquivalence_of_iso, Iff.intro, CategoryTheory.Iso.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_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
rw : (F ⋙ G.asEquivalence.functor ⋙ G.asEquivalence.inverse).IsEquivalence
⊢ F.IsEquivalence

Tactic:
rw [isEquivalence_iff_of_iso (F.rightUnitor.symm ≪≫ isoWhiskerLeft F (G.asEquivalence.unitIso))]

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Functor.rightUnitor, CategoryTheory.Functor.asEquivalence, CategoryTheory.Functor.isEquivalence_iff_of_iso, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Iso.trans, CategoryTheory.Iso.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_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 ⋙ G.asEquivalence.functor ⋙ G.asEquivalence.inverse).IsEquivalence

Tactic:
((F ⋙ G).asEquivalence.trans G.asEquivalence.symm).isEquivalence_functor

Premises used: CategoryTheory.Functor.preimage, CategoryTheory.Functor.comp, CategoryTheory.Functor.asEquivalence, CategoryTheory.Functor.objPreimage, CategoryTheory.Equivalence.isEquivalence_functor, Classical.choose, CategoryTheory.Equivalence.trans, CategoryTheory.Functor.essImage.witness, 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_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 ⋙ G.asEquivalence.functor ⋙ G.asEquivalence.inverse).IsEquivalence

Tactic:
exact ((F ⋙ G).asEquivalence.trans G.asEquivalence.symm).isEquivalence_functor

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.asEquivalence, CategoryTheory.Equivalence.isEquivalence_functor, CategoryTheory.Equivalence.trans, 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_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
rw : ((F.asEquivalence.inverse ⋙ F.asEquivalence.functor) ⋙ G).IsEquivalence
⊢ G.IsEquivalence

Tactic:
rw [isEquivalence_iff_of_iso (G.leftUnitor.symm ≪≫
    isoWhiskerRight F.asEquivalence.counitIso.symm G)]

Premises used: CategoryTheory.Functor.asEquivalence, CategoryTheory.Functor.isEquivalence_iff_of_iso, CategoryTheory.Functor.leftUnitor, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Functor.isoWhiskerRight, CategoryTheory.Equivalence.counitIso
-- 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_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
⊢ ((F.asEquivalence.inverse ⋙ F.asEquivalence.functor) ⋙ G).IsEquivalence

Tactic:
(F.asEquivalence.symm.trans (F ⋙ G).asEquivalence).isEquivalence_functor

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.asEquivalence, CategoryTheory.Equivalence.isEquivalence_functor, CategoryTheory.Equivalence.trans, 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_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
⊢ ((F.asEquivalence.inverse ⋙ F.asEquivalence.functor) ⋙ G).IsEquivalence

Tactic:
exact (F.asEquivalence.symm.trans (F ⋙ G).asEquivalence).isEquivalence_functor

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.asEquivalence, CategoryTheory.Equivalence.isEquivalence_functor, CategoryTheory.Equivalence.trans, 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
C' : Type u_1
e : C' ≃ D
Y : D
⊢ Nonempty.{v₂ + 1}
    (obj.{v₂, v₂, u_1, u₂} (C := InducedCategory (C := C') D (⇑e : (a : C') → D)) (inducedFunctor (⇑e : (a : C') → D))
        ((e.symm : (a : D) → C') Y) ≅
      Y)

Tactic:
simpa using ⟨default⟩
-- Module: Mathlib.CategoryTheory.Equivalence
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
w : ∀ (X : C), i.isoInverseOfIsoFunctor.isoFunctorOfIsoInverse.hom.app X = i.hom.app X
⊢ i.isoInverseOfIsoFunctor.isoFunctorOfIsoInverse = i

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
G G' : Equivalence.{v₁, v₂, u₁, u₂} C D
i : G.functor ≅ G'.functor
X : C
⊢ i.isoInverseOfIsoFunctor.isoFunctorOfIsoInverse.hom.app X = i.hom.app X

Tactic:
simp [← NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Equivalence
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.inverse ≅ G'.inverse
⊢ i.isoFunctorOfIsoInverse.isoInverseOfIsoFunctor = i

Tactic:
isoFunctorOfIsoInverse_isoInverseOfIsoFunctor (G := G.symm) (G' := G'.symm) i

Premises used: CategoryTheory.Iso.isoFunctorOfIsoInverse_isoInverseOfIsoFunctor, CategoryTheory.Iso.isoFunctorOfIsoInverse, CategoryTheory.Iso.symm, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.EssentialImage
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
Y Y' : D
h : Y ≅ Y'
hY : F.essImage Y
⊢ F.essImage Y'

Tactic:
hY.imp fun _ => Nonempty.map (· ≪≫ h)

Premises used: Exists.imp, CategoryTheory.Functor.essImage, CategoryTheory.Iso.trans, Nonempty.map
-- Module: Mathlib.CategoryTheory.EssentialImage
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F F' : Functor.{v₁, v₂, u₁, u₂} C D
h : F ≅ F'
Y : D
hY : F.essImage Y
⊢ F'.essImage Y

Tactic:
hY.imp fun X => Nonempty.map fun t => h.symm.app X ≪≫ t

Premises used: Exists.imp, CategoryTheory.Functor.essImage, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, Nonempty.map, CategoryTheory.Iso.app
-- Module: Mathlib.CategoryTheory.EssentialImage
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F F' : Functor.{v₁, v₂, u₁, u₂} C D
h : F ≅ F'
⊢ F.essImage = F'.essImage

Tactic:
funext fun _ => propext ⟨essImage.ofNatIso h, essImage.ofNatIso h.symm⟩

Premises used: CategoryTheory.Functor.essImage.ofNatIso, funext, Iff.intro, propext, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.EssentialImage
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
Y : D
⊢ F.essImage (F.obj Y)

Tactic:
⟨Y, ⟨Iso.refl _⟩⟩

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Functor.essImage, Nonempty.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.EssentialImage
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
X Y : F.EssImageSubcategory
f g : X ⟶ Y
h : F.essImage.ι.map f = F.essImage.ι.map g
⊢ f = g

Tactic:
F.essImage.ι.map_injective h

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.Functor.essImage, CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.EssentialImage
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
obtain : ∀ (X : C), F.essImage (F.obj X)
⊢ F.essImage Y

Tactic:
obtain ⟨X, rfl⟩ := h Y

Premises used: rfl
-- Module: Mathlib.CategoryTheory.EssentialImage
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
X : C
⊢ F.essImage (F.obj X)

Tactic:
apply obj_mem_essImage

Premises used: CategoryTheory.Functor.obj_mem_essImage
-- Module: Mathlib.CategoryTheory.EssentialImage
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_1 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F_1.EssSurj
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Faithful
⊢ (F.essImage.lift F ⋯).Faithful

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.EssentialImage
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_1 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F_1.EssSurj
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Full
⊢ (F.essImage.lift F ⋯).Full

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.EssentialImage
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₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.EssSurj
⊢ (F ⋙ G).essImage = G.essImage

Tactic:
funext fun _X ↦ propext essImage_comp_apply_of_essSurj

Premises used: CategoryTheory.Functor.essImage_comp_apply_of_essSurj, funext, propext
-- Module: Mathlib.CategoryTheory.EssentialImage
Goal:
C_1 : Type u₁
D_1 : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C_1
inst_1 : Category.{v₂, u₂} D_1
inst_2 : Category.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C_1 D_1
G_1 : Functor.{v₂, v₃, u₂, u₃} D_1 E
J : Type u_1
C : Type u_2
D : Type u_3
inst_3 : Category.{v_1, u_1} J
inst_4 : Category.{v_2, u_2} C
inst_5 : Category.{v_3, u_3} D
G : Functor.{v_1, v_3, u_1, u_3} J D
F : Functor.{v_2, v_3, u_2, u_3} C D
inst_6 : F.Full
inst_7 : F.Faithful
hG : ∀ (j : J), F.essImage (G.obj j)
x : J
⊢ F.map
      (F.preimage
        (InducedCategory.Hom.hom
            (Iso.hom
              (F.toEssImage.objObjPreimageIso (ObjectProperty.FullSubcategory.mk (P := F.essImage) (G.obj x) ⋯))) ≫
          G.map (𝟙 x) ≫
            InducedCategory.Hom.hom
              (Iso.inv
                (F.toEssImage.objObjPreimageIso (ObjectProperty.FullSubcategory.mk (P := F.essImage) (G.obj x) ⋯))))) =
    F.map (𝟙 (F.toEssImage.objPreimage (ObjectProperty.FullSubcategory.mk (P := F.essImage) (G.obj x) ⋯)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EssentialImage
Goal:
C_1 : Type u₁
D_1 : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C_1
inst_1 : Category.{v₂, u₂} D_1
inst_2 : Category.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C_1 D_1
G_1 : Functor.{v₂, v₃, u₂, u₃} D_1 E
J : Type u_1
C : Type u_2
D : Type u_3
inst_3 : Category.{v_1, u_1} J
inst_4 : Category.{v_2, u_2} C
inst_5 : Category.{v_3, u_3} D
G : Functor.{v_1, v_3, u_1, u_3} J D
F : Functor.{v_2, v_3, u_2, u_3} C D
inst_6 : F.Full
inst_7 : F.Faithful
hG : ∀ (j : J), F.essImage (G.obj j)
X Y Z : J
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ Eq (α :=
    F.obj (F.toEssImage.objPreimage (ObjectProperty.FullSubcategory.mk (P := F.essImage) (G.obj X) ⋯)) ⟶
      F.obj (F.toEssImage.objPreimage (ObjectProperty.FullSubcategory.mk (P := F.essImage) (G.obj Z) ⋯)))
    (F.map
      (F.preimage
        (InducedCategory.Hom.hom
            (Iso.hom
              (F.toEssImage.objObjPreimageIso (ObjectProperty.FullSubcategory.mk (P := F.essImage) (G.obj X) ⋯))) ≫
          G.map (x ≫ x_1) ≫
            InducedCategory.Hom.hom
              (Iso.inv
                (F.toEssImage.objObjPreimageIso (ObjectProperty.FullSubcategory.mk (P := F.essImage) (G.obj Z) ⋯))))))
    (F.map
      (CategoryStruct.comp (Y :=
        F.toEssImage.objPreimage (ObjectProperty.FullSubcategory.mk (P := F.essImage) (G.obj Y) ⋯))
        (F.preimage
          (InducedCategory.Hom.hom
              (Iso.hom
                (F.toEssImage.objObjPreimageIso (ObjectProperty.FullSubcategory.mk (P := F.essImage) (G.obj X) ⋯))) ≫
            G.map x ≫
              InducedCategory.Hom.hom
                (Iso.inv
                  (F.toEssImage.objObjPreimageIso (ObjectProperty.FullSubcategory.mk (P := F.essImage) (G.obj Y) ⋯)))))
        (F.preimage
          (InducedCategory.Hom.hom
              (Iso.hom
                (F.toEssImage.objObjPreimageIso (ObjectProperty.FullSubcategory.mk (P := F.essImage) (G.obj Y) ⋯))) ≫
            G.map x_1 ≫
              InducedCategory.Hom.hom
                (Iso.inv
                  (F.toEssImage.objObjPreimageIso
                    (ObjectProperty.FullSubcategory.mk (P := F.essImage) (G.obj Z) ⋯)))))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.EssentialImage
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
h : ∀ (Y : D), (P.ι ⋙ F).essImage Y ↔ P.map F Y
⊢ (P.ι ⋙ F).essImage = P.map F

Tactic:
ext Y
-- Module: Mathlib.CategoryTheory.EssentialImage
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
h₁ : P.map F Y → (P.ι ⋙ F).essImage Y
⊢ (P.ι ⋙ F).essImage Y ↔ P.map F Y

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.EssentialImage
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
X : P.FullSubcategory
e : (P.ι ⋙ F).obj X ≅ Y
⊢ P.map F Y

Tactic:
⟨X.1, X.2, ⟨e⟩⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.FullSubcategory.obj, Nonempty.intro, And.intro, Exists.intro, CategoryTheory.ObjectProperty.map
-- Module: Mathlib.CategoryTheory.EssentialImage
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
X : P.FullSubcategory
e : (P.ι ⋙ F).obj X ≅ Y
⊢ P.map F Y

Tactic:
exact ⟨X.1, X.2, ⟨e⟩⟩
-- Module: Mathlib.CategoryTheory.EssentialImage
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
X : C
hX : P X
e : F.obj X ≅ Y
⊢ (P.ι ⋙ F).essImage Y

Tactic:
⟨⟨X, hX⟩, ⟨e⟩⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Functor.essImage, Nonempty.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.EssentialImage
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
X : C
hX : P X
e : F.obj X ≅ Y
⊢ (P.ι ⋙ F).essImage Y

Tactic:
exact ⟨⟨X, hX⟩, ⟨e⟩⟩
-- Module: Mathlib.CategoryTheory.EssentialImage
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₂
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 = ψ
⊢ ∃ (a : X₁ ⟶ X₂), F.map a = ψ

Tactic:
obtain ⟨f, hf⟩ := h (F.map (L.objObjPreimageIso X₁).hom ≫ ψ ≫
    F.map (L.objObjPreimageIso X₂).inv)

Premises used: CategoryTheory.Functor.map, CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.EssentialImage
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₂
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₂))
⊢ F.map (Iso.inv (L.objObjPreimageIso X₁) ≫ f ≫ Iso.hom (L.objObjPreimageIso X₂)) = ψ

Tactic:
simp [hf]
-- Module: Mathlib.CategoryTheory.EssentialImage
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₂
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:
exact ⟨(L.objObjPreimageIso X₁).inv ≫ f ≫ (L.objObjPreimageIso X₂).hom, by simp [hf]⟩
-- Module: Mathlib.CategoryTheory.EssentialImage
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₂
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))
⊢ a₁ = a₂

Tactic:
rw [← cancel_mono (L.objObjPreimageIso _).inv, ← cancel_epi (L.objObjPreimageIso _).hom]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.EssentialImage
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₂
⊢ Eq (α := F.obj (L.obj (L.objPreimage X)) ⟶ F.obj (L.obj (L.objPreimage Y)))
    (F.map (Iso.hom (L.objObjPreimageIso X) ≫ a₁ ≫ Iso.inv (L.objObjPreimageIso Y)))
    (F.map (Iso.hom (L.objObjPreimageIso X) ≫ a₂ ≫ Iso.inv (L.objObjPreimageIso Y)))

Tactic:
simp [hfg]