awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
neg :
  CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inl
      (Iso.inv (K.biprodXIso K j) ≫
        Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j) =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inl
      (Iso.inv (K.biprodXIso K j) ≫
        HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
          (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f biprod.inl j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j :
            (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))
⊢ Eq (α := biprod.{v_1, u_1} (K.X j) (K.X j) ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
    (Iso.inv (K.biprodXIso K j) ≫
      Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j)
    (Iso.inv (K.biprodXIso K j) ≫
      HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
        (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f biprod.inl j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j :
          (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))
have neg₁ : CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inr
    (Iso.inv (K.biprodXIso K j) ≫
      Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j) =
  CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inr
    (Iso.inv (K.biprodXIso K j) ≫
      HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
        (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f biprod.inl j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j :
          (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
⊢ nullHomotopicMap K = π K ≫ ι₀ K - 𝟙 K.cylinder
have h : ∀ (i : ι), Hom.f (nullHomotopicMap K) i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
i : ι
⊢ Hom.f (nullHomotopicMap K) i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i
have pos : ∀ (hi : c.Rel i (c.next i)), Hom.f (nullHomotopicMap K) i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i
Tactic: by_cases hi : c.Rel i (c.next i)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
i : ι
pos : ∀ (hi : c.Rel i (c.next i)), Hom.f (nullHomotopicMap K) i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i
⊢ Hom.f (nullHomotopicMap K) i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i
have neg : ∀ (hi : ¬c.Rel i (c.next i)), Hom.f (nullHomotopicMap K) i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i
Tactic: by_cases hi : c.Rel i (c.next i)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
D : Type u_3
inst_5 : Category.{v_2, u_3} D
H : HomologicalComplex.{v_1, u_1, u_2} C c ⥤ D
hH : MorphismProperty.IsInvertedBy (homotopyEquivalences C c) H
⊢ Eq (α := H.obj K ⟶ H.obj K.cylinder) (H.map (ι₀ K)) (H.map (ι₁ K))
have this : IsIso (X := H.obj K.cylinder) (H.map (π K))
Tactic: have : IsIso (H.map (cylinder.π K)) := hH _ ⟨homotopyEquiv K hc, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyFiber (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
α : Type u_2
c : ComplexShape α
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : DecidableRel c.Rel
inst_3 : HasHomotopyFiber φ
inst_4 : DecidableRel c.Rel
i j : α
hij : c.symm.Rel i j
⊢ HasBinaryBiproduct.{v_1, u_1} ((Functor.obj (opFunctor C c) (op G)).X j) ((Functor.obj (opFunctor C c) (op F)).X i)
have this : HasBinaryBiproduct.{v_1, u_1} (G.X j) (F.X i)
Tactic: have := HasHomotopyFiber.hasBinaryBiproduct φ j i hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyFiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
α : Type u_2
c : ComplexShape α
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : DecidableRel c.Rel
inst_3 : HasHomotopyFiber φ
inst_4 : DecidableRel c.Rel
i j : α
hij : c.symm.Rel i j
this : HasBinaryBiproduct.{v_1, u_1} (G.X j) (F.X i)
⊢ HasBinaryBiproduct.{v_1, u_1} ((Functor.obj (opFunctor C c) (op G)).X j) ((Functor.obj (opFunctor C c) (op F)).X i)
have dsimp : HasBinaryBiproduct.{v_1, u_1} (op (G.X j)) (op (F.X i))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyFiber (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
α : Type u_2
c : ComplexShape α
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : α), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasPathObject
i j : α
hij : c.symm.Rel i j
⊢ HasBinaryBiproduct.{v_1, u_1} (K.op.X j) ((K.op ⊞ K.op).X i)
have this : HasBinaryBiproduct.{v_1, u_1} (K.X j) ((K ⊞ K).X i)
Tactic: have := HasHomotopyFiber.hasBinaryBiproduct (biprod.desc (𝟙 K) (-𝟙 K)) j i hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyFiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
α : Type u_2
c : ComplexShape α
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : α), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasPathObject
i : α
h₁ : IsZero.{v_1, u_1} (K.X i)
h₂ : ∀ (j : α), c.Rel j i → IsZero.{v_1, u_1} (K.X j)
⊢ IsZero.{v_1, u_1} (K.pathObject.X i)
have h : IsZero.{v_1, u_1} (C := Cᵒᵖ) (op (K.pathObject.1 i))
Tactic: apply IsZero.unop
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyFiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
α : Type u_2
c : ComplexShape α
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : α), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasPathObject
i : α
h₁ : IsZero.{v_1, u_1} (K.X i)
h₂ : ∀ (j : α), c.Rel j i → IsZero.{v_1, u_1} (K.X j)
⊢ IsZero.{v_1, u_1} (C := Cᵒᵖ) (op (K.pathObject.1 i))
have h : IsZero.{v_1, u_1} (C := Cᵒᵖ)
  (homotopyCofiber.X.{v_1, u_1, u_2} (c := c.symm) (F := K.op) (G := K.op ⊞ K.op) (biprod.lift (𝟙 K.op) (-𝟙 K.op)) i)
Tactic: dsimp [pathObject]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyFiber (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
α : Type u_2
c : ComplexShape α
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : α), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasPathObject
i : α
h₁ : IsZero.{v_1, u_1} (K.X i)
h₂ : ∀ (j : α), c.Rel j i → IsZero.{v_1, u_1} (K.X j)
⊢ IsZero.{v_1, u_1} (C := Cᵒᵖ)
    (homotopyCofiber.X.{v_1, u_1, u_2} (c := c.symm) (F := K.op) (G := K.op ⊞ K.op) (biprod.lift (𝟙 K.op) (-𝟙 K.op)) i)
have h : IsZero.{v_1, u_1} ((K.op ⊞ K.op).X i)
Tactic: refine homotopyCofiber.isZero_X _ _ ?_ (fun j hj ↦ IsZero.op (h₂ _ hj))
-- Lean 4 proof step from Mathlib.Algebra.Homology.ImageToKernel (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
inst_2 : HasImage f
g : B ⟶ C
inst_3 : HasKernel g
w : f ≫ g = 0
⊢ Eq (α := A ⟶ Functor.obj Subobject.underlying (kernelSubobject g))
    (CategoryStruct.comp (Y := Functor.obj Subobject.underlying (imageSubobject f)) (factorThruImageSubobject f)
      (imageToKernel f g w))
    (factorThruKernelSubobject g f w)
have h : CategoryStruct.comp (Y := Functor.obj Subobject.underlying (imageSubobject f)) (factorThruImageSubobject f)
      (imageToKernel f g w) ≫
    (kernelSubobject g).arrow =
  factorThruKernelSubobject g f w ≫ (kernelSubobject g).arrow
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ImageToKernel (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
g : B ⟶ C
inst_2 : HasKernels.{v, u} V
inst_3 : HasZeroObject.{v, u} V
w : Eq (α := A ⟶ C) (0 ≫ g) 0
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v, u} B) Subobject.underlying (imageSubobject (X := A) 0) ⟶
      Functor.obj Subobject.underlying (kernelSubobject g))
    (imageToKernel 0 g w) 0
have h : Eq (α := Functor.obj (C := Subobject.{v, u} B) Subobject.underlying (imageSubobject (X := A) 0) ⟶ B)
  (imageToKernel 0 g w ≫ (kernelSubobject g).arrow) (0 ≫ (kernelSubobject g).arrow)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ImageToKernel (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst_2 : HasKernels.{v, u} V
inst_3 : HasImages.{v, u} V
D : V
h : C ⟶ D
w : f ≫ g = 0
⊢ Eq (α :=
    Functor.obj Subobject.underlying (imageSubobject f) ⟶ Functor.obj Subobject.underlying (kernelSubobject (g ≫ h)))
    (imageToKernel f (g ≫ h) ⋯) (imageToKernel f g w ≫ (kernelSubobject g).ofLE (kernelSubobject (g ≫ h)) ⋯)
have h₁ : Eq (α := Functor.obj Subobject.underlying (imageSubobject f) ⟶ B)
  (imageToKernel f (g ≫ h) sorry ≫ (kernelSubobject (g ≫ h)).arrow)
  ((imageToKernel f g w ≫ (kernelSubobject g).ofLE (kernelSubobject (g ≫ h)) sorry) ≫ (kernelSubobject (g ≫ h)).arrow)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ImageToKernel (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst_2 : HasKernels.{v, u} V
inst_3 : HasImages.{v, u} V
Z : V
h : Z ⟶ A
w : f ≫ g = 0
⊢ Eq (α :=
    Functor.obj Subobject.underlying (imageSubobject (h ≫ f)) ⟶ Functor.obj Subobject.underlying (kernelSubobject g))
    (imageToKernel (h ≫ f) g ⋯)
    (CategoryStruct.comp (Y := Functor.obj Subobject.underlying (imageSubobject f))
      ((imageSubobject (h ≫ f)).ofLE (imageSubobject f) ⋯) (imageToKernel f g w))
have h₁ : imageToKernel (h ≫ f) g sorry ≫ (kernelSubobject g).arrow =
  CategoryStruct.comp (Y := Functor.obj Subobject.underlying (imageSubobject f))
      ((imageSubobject (h ≫ f)).ofLE (imageSubobject f) sorry) (imageToKernel f g w) ≫
    (kernelSubobject g).arrow
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ImageToKernel (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst_2 : HasKernels.{v, u} V
inst_3 : HasImages.{v, u} V
D : V
h : C ⟶ D
inst_4 : Mono h
w : f ≫ g ≫ h = 0
⊢ Eq (α :=
    Functor.obj Subobject.underlying (imageSubobject f) ⟶ Functor.obj Subobject.underlying (kernelSubobject (g ≫ h)))
    (imageToKernel f (g ≫ h) w)
    (CategoryStruct.comp (Y := Functor.obj Subobject.underlying (kernelSubobject g)) (imageToKernel f g ⋯)
      (Iso.inv ((kernelSubobject (g ≫ h)).isoOfEq (kernelSubobject g) ⋯)))
have h₁ : Eq (α := Functor.obj Subobject.underlying (imageSubobject f) ⟶ B)
  (imageToKernel f (g ≫ h) w ≫ (kernelSubobject (g ≫ h)).arrow)
  (CategoryStruct.comp (Y := Functor.obj Subobject.underlying (kernelSubobject g)) (imageToKernel f g sorry)
      (Iso.inv ((kernelSubobject (g ≫ h)).isoOfEq (kernelSubobject g) sorry)) ≫
    (kernelSubobject (g ≫ h)).arrow)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ImageToKernel (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst_2 : HasKernels.{v, u} V
inst_3 : HasImages.{v, u} V
Z : V
h : Z ⟶ A
inst_4 : Epi h
w : (h ≫ f) ≫ g = 0
⊢ Eq (α :=
    Functor.obj Subobject.underlying (imageSubobject (h ≫ f)) ⟶ Functor.obj Subobject.underlying (kernelSubobject g))
    (imageToKernel (h ≫ f) g w)
    (CategoryStruct.comp (Y := Functor.obj Subobject.underlying (imageSubobject f))
      ((imageSubobject (h ≫ f)).ofLE (imageSubobject f) ⋯) (imageToKernel f g ⋯))
have h₁ : imageToKernel (h ≫ f) g w ≫ (kernelSubobject g).arrow =
  CategoryStruct.comp (Y := Functor.obj Subobject.underlying (imageSubobject f))
      ((imageSubobject (h ≫ f)).ofLE (imageSubobject f) sorry) (imageToKernel f g sorry) ≫
    (kernelSubobject g).arrow
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ImageToKernel (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst_2 : HasEqualizers.{v, u} V
inst_3 : HasImages.{v, u} V
Z : V
i : B ≅ Z
w : (f ≫ i.hom) ≫ i.inv ≫ g = 0
⊢ Eq (α :=
    Functor.obj Subobject.underlying (imageSubobject (f ≫ i.hom)) ⟶
      Functor.obj Subobject.underlying (kernelSubobject (i.inv ≫ g)))
    (imageToKernel (f ≫ i.hom) (i.inv ≫ g) w :
      Functor.obj Subobject.underlying (imageSubobject (f ≫ i.hom)) ⟶
        Functor.obj Subobject.underlying (kernelSubobject (i.inv ≫ g)))
    (CategoryStruct.comp (Y := Functor.obj Subobject.underlying (imageSubobject f))
        (Iso.hom (imageSubobjectCompIso f i.hom))
        (CategoryStruct.comp (Y := Functor.obj Subobject.underlying (kernelSubobject g)) (imageToKernel f g ⋯)
          (Iso.inv (kernelSubobjectIsoComp i.inv g))) :
      Functor.obj Subobject.underlying (imageSubobject (f ≫ i.hom)) ⟶
        Functor.obj Subobject.underlying (kernelSubobject (i.inv ≫ g)))
have h : Eq (α := Functor.obj Subobject.underlying (imageSubobject (f ≫ i.hom)) ⟶ Z)
  (imageToKernel (f ≫ i.hom) (i.inv ≫ g) w ≫ (kernelSubobject (i.inv ≫ g)).arrow :
    Functor.obj Subobject.underlying (imageSubobject (f ≫ i.hom)) ⟶ Z)
  (CategoryStruct.comp (Y := Functor.obj Subobject.underlying (imageSubobject f))
        (Iso.hom (imageSubobjectCompIso f i.hom))
        (CategoryStruct.comp (Y := Functor.obj Subobject.underlying (kernelSubobject g)) (imageToKernel f g sorry)
          (Iso.inv (kernelSubobjectIsoComp i.inv g))) ≫
      (kernelSubobject (i.inv ≫ g)).arrow :
    Functor.obj Subobject.underlying (imageSubobject (f ≫ i.hom)) ⟶ Z)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ImageToKernel (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst_2 : HasImages.{v, u} V
inst_3 : Epi f
⊢ Epi (X := Functor.obj Subobject.underlying (imageSubobject f)) (Y :=
    Functor.obj (C := Subobject.{v, u} B) Subobject.underlying (kernelSubobject (Y := C) 0)) (imageToKernel f 0 ⋯)
have simp : Epi (Y := Functor.obj (C := Subobject.{v, u} B) Subobject.underlying (kernelSubobject (Y := C) 0))
  ((imageSubobject f).arrow ≫ inv (Subobject.arrow (kernelSubobject (Y := C) 0)))
Tactic: simp only [imageToKernel_zero_right]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ImageToKernel (hypothesis)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst_2 : HasImages.{v, u} V
inst_3 : Epi f
⊢ Epi (Y := Functor.obj (C := Subobject.{v, u} B) Subobject.underlying (kernelSubobject (Y := C) 0))
    ((imageSubobject f).arrow ≫ inv (Subobject.arrow (kernelSubobject (Y := C) 0)))
have this : Epi (X := image f) (image.ι f)
Tactic: haveI := epi_image_of_epi f
-- Lean 4 proof step from Mathlib.Algebra.Homology.ImageToKernel (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst_2 : HasImages.{v, u} V
inst_3 : Epi f
this : Epi (X := image f) (image.ι f)
⊢ Epi (Y := Functor.obj (C := Subobject.{v, u} B) Subobject.underlying (kernelSubobject (Y := C) 0))
    ((imageSubobject f).arrow ≫ inv (Subobject.arrow (kernelSubobject (Y := C) 0)))
have rw : Epi (X := Functor.obj Subobject.underlying (imageSubobject f)) (Y :=
  Functor.obj (C := Subobject.{v, u} B) Subobject.underlying (kernelSubobject (Y := C) 0))
  ((Iso.hom (imageSubobjectIso f) ≫ image.ι f) ≫ inv (Subobject.arrow (kernelSubobject (Y := C) 0)))
Tactic: rw [← imageSubobject_arrow]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ImageToKernel (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
w_1 : f ≫ g = 0
inst_2 : HasKernels.{v, u} V
inst_3 : HasImages.{v, u} V
w : f ≫ g = 0
⊢ Eq (α := image f ⟶ C) (image.ι f ≫ g) 0
have w₁ : CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f ≫ g) =
  CategoryStruct.comp (Y := image f) (factorThruImage f) 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ImageToKernel (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst_2 : HasKernels.{v, u} V
inst_3 : HasImages.{v, u} V
w : f ≫ g = 0
⊢ Eq (α := Functor.obj Subobject.underlying (imageSubobject f) ⟶ kernel g)
    (Iso.hom (imageSubobjectIso f) ≫ imageToKernel' f g w :
      Functor.obj Subobject.underlying (imageSubobject f) ⟶ kernel g)
    (imageToKernel f g w ≫ Iso.hom (kernelSubobjectIso g) :
      Functor.obj Subobject.underlying (imageSubobject f) ⟶ kernel g)
have h : Eq (α := Functor.obj Subobject.underlying (imageSubobject f) ⟶ B)
  (CategoryStruct.comp (Y := equalizer g 0)
      (Iso.hom (imageSubobjectIso f) ≫ imageToKernel' f g w :
        Functor.obj Subobject.underlying (imageSubobject f) ⟶ kernel g)
      (equalizer.ι g 0 : equalizer g 0 ⟶ B) :
    Functor.obj Subobject.underlying (imageSubobject f) ⟶ B)
  (CategoryStruct.comp (Y := equalizer g 0) (imageToKernel f g w ≫ Iso.hom (kernelSubobjectIso g)) (equalizer.ι g 0) :
    Functor.obj Subobject.underlying (imageSubobject f) ⟶ B)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ImageToKernel (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst_2 : HasKernels.{v, u} V
inst_3 : HasImages.{v, u} V
w : f ≫ g = 0
⊢ Eq (α := image f ⟶ Functor.obj Subobject.underlying (kernelSubobject g))
    (CategoryStruct.comp (Y := kernel g) (imageToKernel' f g w : image f ⟶ kernel g)
        (Iso.inv (kernelSubobjectIso g) : kernel g ⟶ Functor.obj Subobject.underlying (kernelSubobject g)) :
      image f ⟶ Functor.obj Subobject.underlying (kernelSubobject g))
    (Iso.inv (imageSubobjectIso f) ≫ imageToKernel f g w :
      image f ⟶ Functor.obj Subobject.underlying (kernelSubobject g))
have h : Eq (α := image f ⟶ B)
  (CategoryStruct.comp (Y := kernel g) (imageToKernel' f g w : image f ⟶ kernel g)
        (Iso.inv (kernelSubobjectIso g) : kernel g ⟶ Functor.obj Subobject.underlying (kernelSubobject g)) ≫
      (kernelSubobject g).arrow :
    image f ⟶ B)
  ((Iso.inv (imageSubobjectIso f) ≫ imageToKernel f g w) ≫ (kernelSubobject g).arrow : image f ⟶ B)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Basic (hypothesis)
Goal:
A : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} A
ι : Functor.{v_1, v_2, u_2, u_1} C A
Λ : LeftResolution ι
X : A
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
n : ℕ
⊢ Eq (α :=
    ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 2)) ⟶ ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
    (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 2) (n + 1)))
    (ι.map (Iso.hom (Λ.chainComplexXIso X n)) ≫
      Λ.π.app
          (kernel (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
            (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n))) ≫
        kernel.ι (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)))
have this : Eq (α :=
  ι.obj
      (Λ.F.obj
        (limit.cone
            (parallelPair (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
              (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)) 0)).1) ⟶
    ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
  (ι.map
    (ι.preimage
      (Λ.π.app
          (limit.cone
              (parallelPair (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
                (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)) 0)).1 ≫
        kernel.ι (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)))))
  (Λ.π.app
      (limit.cone
          (parallelPair (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
            (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)) 0)).1 ≫
    kernel.ι (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)))
Tactic: have := ι.map_preimage (Λ.π.app _ ≫ kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n)))