awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasTerminal.{v₁, u₁} C
inst_3 : HasTerminal.{v₂, u₂} D
i : IsIso (X := G.obj (terminal.{v₁, u₁} C)) (Y := terminal.{v₂, u₂} D) (terminalComparison G)
apply : IsLimit (G.mapCone (asEmptyCone (terminal.{v₁, u₁} C)))
⊢ PreservesLimit (Functor.empty C) G

Tactic:
apply preservesLimit_of_preserves_limit_cone terminalIsTerminal

Premises used: CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasTerminal.{v₁, u₁} C
inst_3 : HasTerminal.{v₂, u₂} D
i : IsIso (X := G.obj (terminal.{v₁, u₁} C)) (Y := terminal.{v₂, u₂} D) (terminalComparison G)
apply : IsTerminal.{v₂, u₂} (G.obj (terminal.{v₁, u₁} C))
⊢ IsLimit (G.mapCone (asEmptyCone (terminal.{v₁, u₁} C)))

Tactic:
apply (isLimitMapConeEmptyConeEquiv _ _).symm _

Premises used: CategoryTheory.Limits.isLimitMapConeEmptyConeEquiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasTerminal.{v₁, u₁} C
inst_3 : HasTerminal.{v₂, u₂} D
i : IsIso (X := G.obj (terminal.{v₁, u₁} C)) (Y := terminal.{v₂, u₂} D) (terminalComparison G)
⊢ IsTerminal.{v₂, u₂} (G.obj (terminal.{v₁, u₁} C))

Tactic:
exact @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (Functor.empty.{0} D)) i

Premises used: CategoryTheory.Limits.limit.isLimit, CategoryTheory.Functor.empty, CategoryTheory.Limits.IsLimit.ofPointIso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasTerminal.{v₁, u₁} C
inst_3 : HasTerminal.{v₂, u₂} D
f : G.obj (terminal.{v₁, u₁} C) ⟶ terminal.{v₂, u₂} D
i : IsIso f
⊢ IsIso (X := G.obj (terminal.{v₁, u₁} C)) (Y := terminal.{v₂, u₂} D) (terminalComparison G)

Tactic:
rw [Subsingleton.elim f (terminalComparison G)] at i

Premises used: CategoryTheory.Limits.terminalComparison, Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasTerminal.{v₁, u₁} C
inst_3 : HasTerminal.{v₂, u₂} D
f : G.obj (terminal.{v₁, u₁} C) ⟶ terminal.{v₂, u₂} D
i : IsIso (X := G.obj (terminal.{v₁, u₁} C)) (Y := terminal.{v₂, u₂} D) (terminalComparison G)
⊢ PreservesLimit (Functor.empty C) G

Tactic:
PreservesTerminal.of_iso_comparison G

Premises used: CategoryTheory.Limits.PreservesTerminal.of_iso_comparison
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasTerminal.{v₁, u₁} C
inst_3 : HasTerminal.{v₂, u₂} D
f : G.obj (terminal.{v₁, u₁} C) ⟶ terminal.{v₂, u₂} D
i : IsIso (X := G.obj (terminal.{v₁, u₁} C)) (Y := terminal.{v₂, u₂} D) (terminalComparison G)
⊢ PreservesLimit (Functor.empty C) G

Tactic:
exact PreservesTerminal.of_iso_comparison G

Premises used: CategoryTheory.Limits.PreservesTerminal.of_iso_comparison
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasTerminal.{v₁, u₁} C
inst_3 : HasTerminal.{v₂, u₂} D
f : G.obj (terminal.{v₁, u₁} C) ≅ terminal.{v₂, u₂} D
⊢ PreservesLimit (Functor.empty C) G

Tactic:
preservesTerminal_of_isIso G f.hom

Premises used: CategoryTheory.Limits.preservesTerminal_of_isIso, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasTerminal.{v₁, u₁} C
inst_3 : HasTerminal.{v₂, u₂} D
inst_4 : PreservesLimit (Functor.empty C) G
⊢ Eq (α := G.obj (terminal.{v₁, u₁} C) ⟶ terminal.{v₂, u₂} D) (Iso.hom (iso G)) (terminalComparison G)

Tactic:
rfl

Premises used: CategoryTheory.Limits.terminalComparison, CategoryTheory.Limits.limit.lift, rfl
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X : C
inst_2 : HasTerminal.{v₁, u₁} C
inst_3 : HasTerminal.{v₂, u₂} D
inst_4 : PreservesLimit (Functor.empty C) G
⊢ IsIso (X := G.obj (terminal.{v₁, u₁} C)) (Y := terminal.{v₂, u₂} D) (Iso.hom (PreservesTerminal.iso G))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasInitial.{v₁, u₁} C
inst_3 : PreservesColimit (Functor.empty C) G
F : Functor.{0, v₂, 0, u₂} (Discrete PEmpty.{1}) D
⊢ HasColimit.{0, 0, v₂, u₂} (Functor.empty D)

Tactic:
haveI := HasColimit.mk ⟨_, isColimitOfHasInitialOfPreservesColimit G⟩
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasInitial.{v₁, u₁} C
inst_3 : PreservesColimit (Functor.empty C) G
F : Functor.{0, v₂, 0, u₂} (Discrete PEmpty.{1}) D
this : HasColimit.{0, 0, v₂, u₂} (Functor.empty D)
⊢ HasColimit F

Tactic:
apply hasColimit_of_iso F.uniqueFromEmpty

Premises used: CategoryTheory.Limits.hasColimit_of_iso, CategoryTheory.Functor.uniqueFromEmpty
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasInitial.{v₁, u₁} C
inst_3 : HasInitial.{v₂, u₂} D
i : IsIso (X := initial.{v₂, u₂} D) (Y := G.obj (initial.{v₁, u₁} C)) (initialComparison G)
apply : IsColimit (G.mapCocone (asEmptyCocone (initial.{v₁, u₁} C)))
⊢ PreservesColimit (Functor.empty C) G

Tactic:
apply preservesColimit_of_preserves_colimit_cocone initialIsInitial

Premises used: CategoryTheory.Limits.initialIsInitial, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasInitial.{v₁, u₁} C
inst_3 : HasInitial.{v₂, u₂} D
i : IsIso (X := initial.{v₂, u₂} D) (Y := G.obj (initial.{v₁, u₁} C)) (initialComparison G)
apply : IsInitial.{v₂, u₂} (G.obj (initial.{v₁, u₁} C))
⊢ IsColimit (G.mapCocone (asEmptyCocone (initial.{v₁, u₁} C)))

Tactic:
apply (isColimitMapCoconeEmptyCoconeEquiv _ _).symm _

Premises used: CategoryTheory.Limits.isColimitMapCoconeEmptyCoconeEquiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasInitial.{v₁, u₁} C
inst_3 : HasInitial.{v₂, u₂} D
i : IsIso (X := initial.{v₂, u₂} D) (Y := G.obj (initial.{v₁, u₁} C)) (initialComparison G)
⊢ IsInitial.{v₂, u₂} (G.obj (initial.{v₁, u₁} C))

Tactic:
exact @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (Functor.empty.{0} D)) i

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.IsColimit.ofPointIso, CategoryTheory.Functor.empty
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasInitial.{v₁, u₁} C
inst_3 : HasInitial.{v₂, u₂} D
f : initial.{v₂, u₂} D ⟶ G.obj (initial.{v₁, u₁} C)
i : IsIso f
⊢ IsIso (X := initial.{v₂, u₂} D) (Y := G.obj (initial.{v₁, u₁} C)) (initialComparison G)

Tactic:
rw [Subsingleton.elim f (initialComparison G)] at i

Premises used: CategoryTheory.Limits.initialComparison, Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasInitial.{v₁, u₁} C
inst_3 : HasInitial.{v₂, u₂} D
f : initial.{v₂, u₂} D ⟶ G.obj (initial.{v₁, u₁} C)
i : IsIso (X := initial.{v₂, u₂} D) (Y := G.obj (initial.{v₁, u₁} C)) (initialComparison G)
⊢ PreservesColimit (Functor.empty C) G

Tactic:
PreservesInitial.of_iso_comparison G

Premises used: CategoryTheory.Limits.PreservesInitial.of_iso_comparison
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasInitial.{v₁, u₁} C
inst_3 : HasInitial.{v₂, u₂} D
f : initial.{v₂, u₂} D ⟶ G.obj (initial.{v₁, u₁} C)
i : IsIso (X := initial.{v₂, u₂} D) (Y := G.obj (initial.{v₁, u₁} C)) (initialComparison G)
⊢ PreservesColimit (Functor.empty C) G

Tactic:
exact PreservesInitial.of_iso_comparison G

Premises used: CategoryTheory.Limits.PreservesInitial.of_iso_comparison
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasInitial.{v₁, u₁} C
inst_3 : HasInitial.{v₂, u₂} D
f : initial.{v₂, u₂} D ≅ G.obj (initial.{v₁, u₁} C)
⊢ PreservesColimit (Functor.empty C) G

Tactic:
preservesInitial_of_isIso G f.hom

Premises used: CategoryTheory.Limits.preservesInitial_of_isIso, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasInitial.{v₁, u₁} C
inst_3 : HasInitial.{v₂, u₂} D
inst_4 : PreservesColimit (Functor.empty C) G
⊢ Eq (α := initial.{v₂, u₂} D ⟶ G.obj (initial.{v₁, u₁} C)) (Iso.inv (iso G)) (initialComparison G)

Tactic:
rfl

Premises used: CategoryTheory.Limits.initialComparison, CategoryTheory.Limits.colimit.desc, rfl
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
X : C
inst_2 : HasInitial.{v₁, u₁} C
inst_3 : HasInitial.{v₂, u₂} D
inst_4 : PreservesColimit (Functor.empty C) G
⊢ IsIso (X := initial.{v₂, u₂} D) (Y := G.obj (initial.{v₁, u₁} C)) (Iso.inv (PreservesInitial.iso G))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) 0

Tactic:
PreservesZeroMorphisms.map_zero _ _

Premises used: CategoryTheory.Functor.PreservesZeroMorphisms.map_zero
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X : C
hX : IsZero.{v₁, u₁} X
simp : ∀ (hX : Eq.{v₁ + 1} (α := X ⟶ X) (𝟙 X) 0), Eq.{v₂ + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X)) 0
⊢ IsZero.{v₂, u₂} (F.obj X)

Tactic:
simp only [IsZero.iff_id_eq_zero] at hX ⊢

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X : C
hX : Eq.{v₁ + 1} (α := X ⟶ X) (𝟙 X) 0
rw : F.map (𝟙 X) = 0
rw₁ : Eq (α := F.obj X ⟶ F.obj X) (F.map 0) 0
rw₂ rw₃ : Eq.{v₂ + 1} (α := F.obj X ⟶ F.obj X) 0 0
⊢ Eq.{v₂ + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X)) 0

Tactic:
rw [← F.map_id, hX, F.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.Faithful
X Y : C
f : X ⟶ Y
h : F.map f = 0
⊢ f = 0

Tactic:
F.map_injective <| h.trans <| Eq.symm <| F.map_zero _ _

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map_injective, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.Faithful
X Y : C
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) 0

Tactic:
F.map_zero _ _

Premises used: CategoryTheory.Functor.map_zero
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.Faithful
X Y : C
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) 0

Tactic:
exact F.map_zero _ _

Premises used: CategoryTheory.Functor.map_zero
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.IsLeftAdjoint
X Y : C
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y))

Tactic:
?_
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.IsLeftAdjoint
X Y : C
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (F.rightAdjoint.obj (F.obj X))) (F.map 0)
      (F.map (F.rightAdjoint.map 0) ≫ adj.counit.app (F.obj Y)))

Tactic:
?_
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.IsLeftAdjoint
X Y : C
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
⊢ Eq (α := F.obj X ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (F.rightAdjoint.obj (F.obj X))) (F.map 0)
      (F.map (F.rightAdjoint.map 0) ≫ adj.counit.app (F.obj Y)))
    0

Tactic:
?_
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.IsLeftAdjoint
X Y : C
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
calc_1 : Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y))
calc_2 :
  Eq (α := F.obj X ⟶ F.obj Y) (F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (F.rightAdjoint.obj (F.obj X))) (F.map 0)
      (F.map (F.rightAdjoint.map 0) ≫ adj.counit.app (F.obj Y)))
calc_3 :
  Eq (α := F.obj X ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (F.rightAdjoint.obj (F.obj X))) (F.map 0)
      (F.map (F.rightAdjoint.map 0) ≫ adj.counit.app (F.obj Y)))
    0
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) 0

Tactic:
calc
      dsimp% F.map (0 : X ⟶ Y) = F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y) := ?_
      _ = F.map 0 ≫ F.map ((rightAdjoint F).map (0 : F.obj X ⟶ _)) ≫ adj.counit.app (F.obj Y) := ?_
      _ = 0 := ?_

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.Functor.map, CategoryTheory.Adjunction.counit, CategoryTheory.Functor.rightAdjoint, OfNat.ofNat, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.IsLeftAdjoint
X Y : C
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
calc_1 : Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (F.map 0 ≫ 𝟙 (F.obj Y))
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y))

Tactic:
rw [Adjunction.left_triangle_components]

Premises used: CategoryTheory.Adjunction.left_triangle_components
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.IsLeftAdjoint
X Y : C
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (F.map 0 ≫ 𝟙 (F.obj Y))

Tactic:
(Category.comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.IsLeftAdjoint
X Y : C
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (F.map 0 ≫ 𝟙 (F.obj Y))

Tactic:
exact (Category.comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.IsLeftAdjoint
X Y : C
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (F.rightAdjoint.obj (F.obj X))) (F.map 0)
      (F.map (F.rightAdjoint.map 0) ≫ adj.counit.app (F.obj Y)))

Tactic:
simp only [← Category.assoc, ← F.map_comp, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.IsLeftAdjoint
X Y : C
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
⊢ Eq (α := F.obj X ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (F.rightAdjoint.obj (F.obj X))) (F.map 0)
      (F.map (F.rightAdjoint.map 0) ≫ adj.counit.app (F.obj Y)))
    0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : G.IsRightAdjoint
X Y : C
adj : G.leftAdjoint ⊣ G := Adjunction.ofIsRightAdjoint G
⊢ Eq (α := G.obj X ⟶ G.obj Y) (G.map 0) (adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0)

Tactic:
?_
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : G.IsRightAdjoint
X Y : C
adj : G.leftAdjoint ⊣ G := Adjunction.ofIsRightAdjoint G
⊢ Eq (α := obj.{v₂, v₂, u₂, u₂} (𝟭 D) (G.obj X) ⟶ G.obj Y) (adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0)
    (adj.unit.app (G.obj X) ≫
      CategoryStruct.comp (Y := G.obj (G.leftAdjoint.obj (G.obj X))) (G.map (G.leftAdjoint.map 0)) (G.map 0))

Tactic:
?_
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : G.IsRightAdjoint
X Y : C
adj : G.leftAdjoint ⊣ G := Adjunction.ofIsRightAdjoint G
⊢ Eq (α := obj.{v₂, v₂, u₂, u₂} (𝟭 D) (G.obj X) ⟶ G.obj Y)
    (adj.unit.app (G.obj X) ≫
      CategoryStruct.comp (Y := G.obj (G.leftAdjoint.obj (G.obj X))) (G.map (G.leftAdjoint.map 0)) (G.map 0))
    0

Tactic:
?_
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : G.IsRightAdjoint
X Y : C
adj : G.leftAdjoint ⊣ G := Adjunction.ofIsRightAdjoint G
calc_1 : Eq (α := G.obj X ⟶ G.obj Y) (G.map 0) (adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0)
calc_2 :
  Eq (α := obj.{v₂, v₂, u₂, u₂} (𝟭 D) (G.obj X) ⟶ G.obj Y) (adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0)
    (adj.unit.app (G.obj X) ≫
      CategoryStruct.comp (Y := G.obj (G.leftAdjoint.obj (G.obj X))) (G.map (G.leftAdjoint.map 0)) (G.map 0))
calc_3 :
  Eq (α := obj.{v₂, v₂, u₂, u₂} (𝟭 D) (G.obj X) ⟶ G.obj Y)
    (adj.unit.app (G.obj X) ≫
      CategoryStruct.comp (Y := G.obj (G.leftAdjoint.obj (G.obj X))) (G.map (G.leftAdjoint.map 0)) (G.map 0))
    0
⊢ Eq (α := G.obj X ⟶ G.obj Y) (G.map 0) 0

Tactic:
calc
      G.map (0 : X ⟶ Y) = adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0 := ?_
      _ = adj.unit.app (G.obj X) ≫ G.map ((leftAdjoint G).map (0 : _ ⟶ G.obj X)) ≫ G.map 0 := ?_
      _ = 0 := ?_

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.Functor.map, CategoryTheory.Adjunction.counit, CategoryTheory.Functor.leftAdjoint, OfNat.ofNat, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app