awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Preserves
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
⊢ F.PreservesInjectiveObjects

Tactic:
preservesInjectiveObjects_of_adjunction_of_preservesMonomorphisms
    F.asEquivalence.symm.toAdjunction

Premises used: CategoryTheory.Functor.preservesInjectiveObjects_of_adjunction_of_preservesMonomorphisms, CategoryTheory.Functor.asEquivalence, CategoryTheory.Equivalence.toAdjunction, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Preserves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : EnoughInjectives.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_3 : G.PreservesInjectiveObjects
X Y : C
f : X ⟶ Y
h : Mono f
suffices : ∃ (h : F.obj Y ⟶ Injective.under.{v₂, u₂} (F.obj X)), F.map f ≫ h = Injective.ι (F.obj X)
⊢ Mono (F.map f)

Tactic:
suffices ∃ h, F.map f ≫ h = Injective.ι (F.obj X) from mono_of_mono_fac this.choose_spec
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Preserves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : EnoughInjectives.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_3 : G.PreservesInjectiveObjects
X Y : C
f : X ⟶ Y
h : Mono f
⊢ Eq (α := F.obj X ⟶ Injective.under.{v₂, u₂} (F.obj X))
    (F.map f ≫
        CategoryStruct.comp (Y := F.obj (G.obj (Injective.under.{v₂, u₂} (F.obj X))))
          (F.map (Injective.factorThru (adj.unit.app X ≫ G.map (Injective.ι (F.obj X))) f))
          (adj.counit.app (Injective.under.{v₂, u₂} (F.obj X))) :
      F.obj X ⟶ Injective.under.{v₂, u₂} (F.obj X))
    (Injective.ι (F.obj X) : F.obj X ⟶ Injective.under.{v₂, u₂} (F.obj X))

Tactic:
simp [← Functor.map_comp_assoc]

Premises used: CategoryTheory.Functor.map_comp_assoc
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Preserves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : EnoughInjectives.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_3 : G.PreservesInjectiveObjects
X Y : C
f : X ⟶ Y
h : Mono f
⊢ ∃ (h : F.obj Y ⟶ Injective.under.{v₂, u₂} (F.obj X)), F.map f ≫ h = Injective.ι (F.obj X)

Tactic:
exact ⟨F.map (Injective.factorThru (adj.unit.app X ≫ G.map (Injective.ι _)) f) ≫
      adj.counit.app (Injective.under (F.obj X)), by simp [← Functor.map_comp_assoc]⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
n : ℕ
rw : QuasiIsoAt I.ι (n + 1)
⊢ ExactAt I.cocomplex (n + 1)

Tactic:
rw [← quasiIsoAt_iff_exactAt I.ι (n + 1) (exactAt_succ_single_obj _ _)]

Premises used: quasiIsoAt_iff_exactAt, CategoryTheory.InjectiveResolution.ι, CochainComplex.exactAt_succ_single_obj, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
n : ℕ
⊢ QuasiIsoAt I.ι (n + 1)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
n : ℕ
⊢ (ComplexShape.up ℕ).prev (n + 1) = n

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
n : ℕ
simp : n + 1 + 1 = n + 2
⊢ (ComplexShape.up ℕ).next (n + 1) = n + 2

Tactic:
simp only [CochainComplex.next]

Premises used: CochainComplex.next
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
n : ℕ
⊢ n + 1 + 1 = n + 2

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
n : ℕ
⊢ n + 1 ≠ 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
⊢ Eq (α := X.{v, u, 0} (Functor.obj (single₀ C) Z) 0 ⟶ I.cocomplex.X 1) (I.ι.f 0 ≫ I.cocomplex.d 0 1) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
n : ℕ
⊢ Eq (α := I.cocomplex.X n ⟶ I.cocomplex.X (n + 2))
    (CategoryStruct.comp (Y := I.cocomplex.X (n + 1)) (I.cocomplex.d n (n + 1)) (I.cocomplex.d (n + 1) (n + 2))) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
⊢ (ComplexShape.up ℕ).next 0 = 1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
refine : I.kernelFork ≅ KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯
⊢ IsLimit I.kernelFork

Tactic:
refine IsLimit.ofIsoLimit (I.cocomplex.cyclesIsKernel 0 1 (by simp)) (Iso.symm ?_)

Premises used: HomologicalComplex.cyclesIsKernel, CategoryTheory.Iso.symm, OfNat.ofNat, CategoryTheory.Limits.IsLimit.ofIsoLimit, CategoryTheory.InjectiveResolution.cocomplex
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
refine :
  CategoryStruct.comp (Y :=
      Cone.pt (F := parallelPair (X := I.cocomplex.X 0) (Y := I.cocomplex.X 1) (I.cocomplex.d 0 1) 0)
        (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯))
      (Iso.hom
          (Iso.symm (singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt) ≪≫
            Iso.trans (Y := homology I.cocomplex 0) (isoOfQuasiIsoAt I.ι 0) (Iso.symm I.cocomplex.isoHomologyπ₀)) :
        I.kernelFork.pt ⟶
          Cone.pt (F := parallelPair (X := I.cocomplex.X 0) (Y := I.cocomplex.X 1) (I.cocomplex.d 0 1) 0)
            (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯))
      (Fork.ι (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯) :
        Cone.pt (F := parallelPair (X := I.cocomplex.X 0) (Y := I.cocomplex.X 1) (I.cocomplex.d 0 1) 0)
            (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯) ⟶
          I.cocomplex.X 0) =
    Fork.ι I.kernelFork
⊢ I.kernelFork ≅ KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯

Tactic:
refine Fork.ext ((singleObjHomologySelfIso _ _ _).symm ≪≫
    isoOfQuasiIsoAt I.ι 0 ≪≫ I.cocomplex.isoHomologyπ₀.symm) ?_

Premises used: HomologicalComplex.singleObjHomologySelfIso, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Limits.Fork.ext
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
⊢ CategoryStruct.comp (Y := cycles.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℕ) 0) I.kernelFork.pt) 0)
      (Iso.inv (singleObjCyclesSelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt))
      (Iso.hom (isoHomologyπ₀ (Functor.obj (single C (ComplexShape.up ℕ) 0) I.kernelFork.pt)) ≫
        Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt) ≫
          CategoryStruct.comp (Y :=
            Cone.pt (F := parallelPair (X := I.cocomplex.X 0) (Y := I.cocomplex.X 1) (I.cocomplex.d 0 1) 0)
              (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯))
            (Iso.hom
                (Iso.symm (singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt) ≪≫
                  Iso.trans (Y := homology I.cocomplex 0) (isoOfQuasiIsoAt I.ι 0)
                    (Iso.symm I.cocomplex.isoHomologyπ₀)) :
              I.kernelFork.pt ⟶
                Cone.pt (F := parallelPair (X := I.cocomplex.X 0) (Y := I.cocomplex.X 1) (I.cocomplex.d 0 1) 0)
                  (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯))
            (Fork.ι (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯) :
              Cone.pt (F := parallelPair (X := I.cocomplex.X 0) (Y := I.cocomplex.X 1) (I.cocomplex.d 0 1) 0)
                  (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯) ⟶
                I.cocomplex.X 0)) =
    CategoryStruct.comp (Y := cycles.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℕ) 0) I.kernelFork.pt) 0)
      (Iso.inv (singleObjCyclesSelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt))
      (Iso.hom (isoHomologyπ₀ (Functor.obj (single C (ComplexShape.up ℕ) 0) I.kernelFork.pt)) ≫
        Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt) ≫ Fork.ι I.kernelFork)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
n : ℕ
zero : Mono (X := X.{v, u, 0} (Functor.obj (single₀ C) Z) 0) (I.ι.f 0)
succ : ∀ (n : ℕ), Mono (X := X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1)) (I.ι.f (n + 1))
⊢ Mono (I.ι.f n)

Tactic:
cases n
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
⊢ Mono (X := X.{v, u, 0} (Functor.obj (single₀ C) Z) 0) (I.ι.f 0)

Tactic:
mono_of_isLimit_fork I.isLimitKernelFork

Premises used: CategoryTheory.InjectiveResolution.isLimitKernelFork, CategoryTheory.Limits.mono_of_isLimit_fork, CategoryTheory.Limits.Fork.ι, ite
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
⊢ Mono (X := X.{v, u, 0} (Functor.obj (single₀ C) Z) 0) (I.ι.f 0)

Tactic:
exact mono_of_isLimit_fork I.isLimitKernelFork

Premises used: CategoryTheory.InjectiveResolution.isLimitKernelFork, CategoryTheory.Limits.mono_of_isLimit_fork
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
n : ℕ
succ : Mono.{v, u} (C := C) (X := X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1)) (Y := I.cocomplex.X (n + 1)) 0
⊢ Mono (X := X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1)) (I.ι.f (n + 1))

Tactic:
rw [ι_f_succ]

Premises used: CategoryTheory.InjectiveResolution.ι_f_succ
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
n : ℕ
⊢ Mono.{v, u} (C := C) (X := X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1)) (Y := I.cocomplex.X (n + 1)) 0

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
inst_3 : Injective.{v, u} Z
n : ℕ
zero : Injective.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) 0)
succ : ∀ (n : ℕ), Injective.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1))
⊢ Injective.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) n)

Tactic:
cases n
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
inst_3 : Injective.{v, u} Z
⊢ Injective.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) 0)

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
inst_3 : Injective.{v, u} Z
n : ℕ
succ : IsZero.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1))
⊢ Injective.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1))

Tactic:
apply IsZero.injective

Premises used: CategoryTheory.Limits.IsZero.injective
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
inst_3 : Injective.{v, u} Z
n : ℕ
succ : n + 1 ≠ 0
⊢ IsZero.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1))

Tactic:
apply HomologicalComplex.isZero_single_obj_X

Premises used: HomologicalComplex.isZero_single_obj_X
-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
inst_3 : Injective.{v, u} Z
n : ℕ
⊢ n + 1 ≠ 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y Z : C
π₁ : Z ⟶ X
π₂ : Z ⟶ Y
inst_5 : PreservesLimit (parallelPair π₂ 0) F
i : IsLimit (BinaryFan.mk π₁ π₂)
bc : BinaryBicone.{v₁, u₁} X Y := BinaryBicone.ofLimitCone i
⊢ PreservesLimit (parallelPair bc.snd 0) F

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y Z : C
π₁ : Z ⟶ X
π₂ : Z ⟶ Y
inst_5 : PreservesLimit (parallelPair π₂ 0) F
i : IsLimit (BinaryFan.mk π₁ π₂)
bc : BinaryBicone.{v₁, u₁} X Y := BinaryBicone.ofLimitCone i
presf : PreservesLimit (parallelPair bc.snd 0) F := inst_5
hf : IsLimit bc.sndKernelFork := BinaryBicone.isLimitSndKernelFork i
⊢ IsLimit (F.mapCone (BinaryFan.mk π₁ π₂))

Tactic:
exact (isLimitMapConeBinaryFanEquiv F π₁ π₂).invFun
    (BinaryBicone.isBilimitOfKernelInl (F.mapBinaryBicone bc)
    (isLimitMapConeForkEquiv' F bc.inl_snd (isLimitOfPreserves F hf))).isLimit

Premises used: CategoryTheory.Limits.isLimitMapConeForkEquiv', CategoryTheory.Functor.mapBinaryBicone, CategoryTheory.Limits.isLimitMapConeBinaryFanEquiv, CategoryTheory.Limits.BinaryBicone.isBilimitOfKernelInl, CategoryTheory.Limits.BinaryBicone.IsBilimit.isLimit, CategoryTheory.Limits.BinaryBicone.inl_snd, DFunLike.coe, CategoryTheory.Limits.isLimitOfPreserves, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : HasBinaryBiproducts.{v₁, u₁} C
inst_6 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this : PreservesBinaryBiproducts F := ⋯
⊢ F.Additive

Tactic:
haveI := additive_of_preservesBinaryBiproducts F
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : HasBinaryBiproducts.{v₁, u₁} C
inst_6 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this_1 : PreservesBinaryBiproducts F := ⋯
this : F.Additive
preserves : ∀ {c : Cone (parallelPair f g)} (hc : IsLimit c), Nonempty (IsLimit (F.mapCone c))
⊢ PreservesLimit (parallelPair f g) F

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : HasBinaryBiproducts.{v₁, u₁} C
inst_6 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this_1 : PreservesBinaryBiproducts F := ⋯
this : F.Additive
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (F := parallelPair (f - g) 0) (KernelFork.ofι (Fork.ι c) ⋯) :=
  isLimitKernelForkOfFork (i.ofIsoLimit (Fork.isoForkOfι c))
iFc : IsLimit (F := parallelPair (F.map (f - g)) 0) (KernelFork.ofι (F.map (Fork.ι c)) ⋯) :=
  isLimitForkMapOfIsLimit' F ⋯ c'
preserves : IsLimit (F.mapCone c)
⊢ Nonempty (IsLimit (F.mapCone c))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : HasBinaryBiproducts.{v₁, u₁} C
inst_6 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this_1 : PreservesBinaryBiproducts F := ⋯
this : F.Additive
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (F := parallelPair (f - g) 0) (KernelFork.ofι (Fork.ι c) ⋯) :=
  isLimitKernelForkOfFork (i.ofIsoLimit (Fork.isoForkOfι c))
iFc : IsLimit (F := parallelPair (F.map (f - g)) 0) (KernelFork.ofι (F.map (Fork.ι c)) ⋯) :=
  isLimitForkMapOfIsLimit' F ⋯ c'
apply : IsLimit ((Cone.functoriality (parallelPair f g) F).obj (Fork.ofι (Fork.ι c) ⋯))
⊢ IsLimit (F.mapCone c)

Tactic:
apply IsLimit.ofIsoLimit _ ((Cone.functoriality _ F).mapIso (Fork.isoForkOfι c).symm)

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Limits.Cone.functoriality, CategoryTheory.Limits.IsLimit.ofIsoLimit, CategoryTheory.Functor.mapIso, CategoryTheory.Limits.Fork.isoForkOfι
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : HasBinaryBiproducts.{v₁, u₁} C
inst_6 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this_1 : PreservesBinaryBiproducts F := ⋯
this : F.Additive
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (F := parallelPair (f - g) 0) (KernelFork.ofι (Fork.ι c) ⋯) :=
  isLimitKernelForkOfFork (i.ofIsoLimit (Fork.isoForkOfι c))
iFc : IsLimit (F := parallelPair (F.map (f - g)) 0) (KernelFork.ofι (F.map (Fork.ι c)) ⋯) :=
  isLimitForkMapOfIsLimit' F ⋯ c'
apply : IsLimit (Fork.ofι (F.map (Fork.ι c)) ⋯)
⊢ IsLimit ((Cone.functoriality (parallelPair f g) F).obj (Fork.ofι (Fork.ι c) ⋯))

Tactic:
apply (isLimitMapConeForkEquiv F (Fork.condition c)).invFun

Premises used: CategoryTheory.Limits.isLimitMapConeForkEquiv, CategoryTheory.Limits.Fork.condition, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : HasBinaryBiproducts.{v₁, u₁} C
inst_6 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this_1 : PreservesBinaryBiproducts F := ⋯
this : F.Additive
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (F := parallelPair (f - g) 0) (KernelFork.ofι (Fork.ι c) ⋯) :=
  isLimitKernelForkOfFork (i.ofIsoLimit (Fork.isoForkOfι c))
iFc : IsLimit (F := parallelPair (F.map (f - g)) 0) (KernelFork.ofι (F.map (Fork.ι c)) ⋯) :=
  isLimitForkMapOfIsLimit' F ⋯ c'
p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 := parallelPair.eqOfHomEq ⋯ ⋯
⊢ Iso.hom (Iso.refl (forkOfKernelFork ((Cone.postcompose p.hom).obj (KernelFork.ofι (F.map (Fork.ι c)) ⋯))).pt) ≫
      (Fork.ofι (F.map (Fork.ι c)) ⋯).ι =
    (forkOfKernelFork ((Cone.postcompose p.hom).obj (KernelFork.ofι (F.map (Fork.ι c)) ⋯))).ι

Tactic:
simp [p]
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : HasBinaryBiproducts.{v₁, u₁} C
inst_6 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this_1 : PreservesBinaryBiproducts F := ⋯
this : F.Additive
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (F := parallelPair (f - g) 0) (KernelFork.ofι (Fork.ι c) ⋯) :=
  isLimitKernelForkOfFork (i.ofIsoLimit (Fork.isoForkOfι c))
iFc : IsLimit (F := parallelPair (F.map (f - g)) 0) (KernelFork.ofι (F.map (Fork.ι c)) ⋯) :=
  isLimitForkMapOfIsLimit' F ⋯ c'
p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 := parallelPair.eqOfHomEq ⋯ ⋯
⊢ IsLimit (Fork.ofι (F.map (Fork.ι c)) ⋯)

Tactic:
exact
    IsLimit.ofIsoLimit
      (isLimitForkOfKernelFork ((IsLimit.postcomposeHomEquiv p _).symm iFc))
      (Fork.ext (Iso.refl _) (by simp [p]))

Premises used: CategoryTheory.Preadditive.isLimitForkOfKernelFork, CategoryTheory.Limits.IsLimit.postcomposeHomEquiv, CategoryTheory.Iso.refl, CategoryTheory.Limits.Fork.ext, Equiv.symm, CategoryTheory.Limits.IsLimit.ofIsoLimit, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : HasBinaryBiproducts.{v₁, u₁} C
inst_6 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
K : Functor.{0, v₁, 0, u₁} WalkingParallelPair C
this : PreservesLimit (parallelPair (K.map WalkingParallelPairHom.left) (K.map WalkingParallelPairHom.right)) F := ⋯
⊢ PreservesLimit K F

Tactic:
apply preservesLimit_of_iso_diagram F (diagramIsoParallelPair K).symm

Premises used: CategoryTheory.Limits.preservesLimit_of_iso_diagram, CategoryTheory.Limits.diagramIsoParallelPair, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : HasBinaryBiproducts.{v₁, u₁} C
inst_6 : HasFiniteProducts.{v₁, u₁} C
inst_7 : HasEqualizers.{v₁, u₁} C
inst_8 : HasZeroObject.{v₁, u₁} C
inst_9 : HasZeroObject.{v₂, u₂} D
inst_10 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
⊢ PreservesFiniteLimits F

Tactic:
have := preservesEqualizers_of_preservesKernels F
  have := preservesTerminalObject_of_preservesZeroMorphisms F
  have := preservesLimitsOfShape_pempty_of_preservesTerminal F
  have : PreservesFiniteProducts F := .of_preserves_binary_and_terminal F
  preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts F

Premises used: CategoryTheory.Limits.PreservesFiniteProducts.of_preserves_binary_and_terminal, CategoryTheory.Limits.preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts, CategoryTheory.Functor.preservesEqualizers_of_preservesKernels, CategoryTheory.Functor.preservesTerminalObject_of_preservesZeroMorphisms, CategoryTheory.Limits.preservesLimitsOfShape_pempty_of_preservesTerminal