awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyFiber
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)
i : α
⊢ HasBinaryBiproduct.{v_1, u_1} (op (K.X i)) (op (K.X i))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomotopyFiber
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.X j) ((K ⊞ K).X i)

Tactic:
have := HasHomotopyFiber.hasBinaryBiproduct (biprod.desc (𝟙 K) (-𝟙 K)) j i hij
-- Module: Mathlib.Algebra.Homology.HomotopyFiber
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
this : HasBinaryBiproduct.{v_1, u_1} (K.X j) ((K ⊞ K).X i)
⊢ HasBinaryBiproduct.{v_1, u_1} (K.op.X j) ((K.op ⊞ K.op).X i)

Tactic:
hasBinaryBiproduct_of_iso (Iso.refl _ : op (K.X j) ≅ K.op.X j)
      (show op ((K ⊞ K).X i) ≅ (K.op ⊞ K.op).X i from
        ((eval _ _ i).mapBiprod K K).op.symm ≪≫ biprod.opIso _ _ ≪≫
          ((eval _ _ i).mapBiprod K.op K.op).symm)

Premises used: Opposite, HomologicalComplex.op, CategoryTheory.Iso.op, CategoryTheory.Limits.biprod.opIso, HomologicalComplex.eval, CategoryTheory.Limits.hasBinaryBiproduct_of_iso, CategoryTheory.Iso.refl, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, ComplexShape.symm, CategoryTheory.Functor.mapBiprod, CategoryTheory.Functor.obj
-- Module: Mathlib.Algebra.Homology.HomotopyFiber
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
this : HasBinaryBiproduct.{v_1, u_1} (K.X j) ((K ⊞ K).X i)
⊢ HasBinaryBiproduct.{v_1, u_1} (K.op.X j) ((K.op ⊞ K.op).X i)

Tactic:
exact hasBinaryBiproduct_of_iso (Iso.refl _ : op (K.X j) ≅ K.op.X j)
      (show op ((K ⊞ K).X i) ≅ (K.op ⊞ K.op).X i from
        ((eval _ _ i).mapBiprod K K).op.symm ≪≫ biprod.opIso _ _ ≪≫
          ((eval _ _ i).mapBiprod K.op K.op).symm)

Premises used: Opposite, HomologicalComplex.op, CategoryTheory.Iso.op, CategoryTheory.Limits.biprod.opIso, HomologicalComplex.eval, CategoryTheory.Limits.hasBinaryBiproduct_of_iso, CategoryTheory.Iso.refl, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, ComplexShape.symm, CategoryTheory.Functor.mapBiprod, CategoryTheory.Functor.obj
-- Module: Mathlib.Algebra.Homology.HomotopyFiber
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)
h : IsZero.{v_1, u_1} (C := Cᵒᵖ) (op (K.pathObject.1 i))
⊢ IsZero.{v_1, u_1} (K.pathObject.X i)

Tactic:
apply IsZero.unop

Premises used: CategoryTheory.Limits.IsZero.unop
-- Module: Mathlib.Algebra.Homology.HomotopyFiber
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)
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)
⊢ IsZero.{v_1, u_1} (C := Cᵒᵖ) (op (K.pathObject.1 i))

Tactic:
dsimp [pathObject]

Premises used: HomologicalComplex.pathObject
-- Module: Mathlib.Algebra.Homology.HomotopyFiber
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)

Tactic:
homotopyCofiber.isZero_X _ _ ?_ (fun j hj ↦ IsZero.op (h₂ _ hj))

Premises used: CategoryTheory.Limits.IsZero.op, HomologicalComplex.homotopyCofiber.isZero_X
-- Module: Mathlib.Algebra.Homology.HomotopyFiber
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)
h : IsZero.{v_1, u_1} ((K.op ⊞ K.op).X i)
⊢ 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:
refine homotopyCofiber.isZero_X _ _ ?_ (fun j hj ↦ IsZero.op (h₂ _ hj))

Premises used: CategoryTheory.Limits.IsZero.op, HomologicalComplex.homotopyCofiber.isZero_X
-- Module: Mathlib.Algebra.Homology.HomotopyFiber
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} (biprod.{v_1, u_1} (Functor.obj (eval Cᵒᵖ c.symm i) K.op) (Functor.obj (eval Cᵒᵖ c.symm i) K.op))

Tactic:
simpa using h₁.op

Premises used: CategoryTheory.Limits.IsZero.op
-- Module: Mathlib.Algebra.Homology.HomotopyFiber
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.op ⊞ K.op).X i)

Tactic:
exact IsZero.of_iso (by simpa using h₁.op)
    ((eval Cᵒᵖ c.symm i).mapBiprod K.op K.op)

Premises used: Opposite, HomologicalComplex.op, HomologicalComplex.eval, CategoryTheory.Limits.IsZero.of_iso, ComplexShape.symm, CategoryTheory.Functor.mapBiprod
-- Module: Mathlib.Algebra.Homology.HomotopyFiber
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
⊢ CategoryStruct.comp (Y := K.pathObject) (ι K) (π₀ K) = 𝟙 K

Tactic:
Quiver.Hom.op_inj ((opFunctor C c).map_injective (cylinder.ι₀_π K.op))

Premises used: HomologicalComplex.op, Quiver.Hom.op_inj, HomologicalComplex.cylinder.ι₀_π, HomologicalComplex.opFunctor, CategoryTheory.Functor.map_injective
-- Module: Mathlib.Algebra.Homology.HomotopyFiber
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
⊢ CategoryStruct.comp (Y := K.pathObject) (ι K) (π₁ K) = 𝟙 K

Tactic:
Quiver.Hom.op_inj ((opFunctor C c).map_injective (cylinder.ι₁_π K.op))

Premises used: HomologicalComplex.op, Quiver.Hom.op_inj, HomologicalComplex.cylinder.ι₁_π, HomologicalComplex.opFunctor, CategoryTheory.Functor.map_injective
-- Module: Mathlib.Algebra.Homology.HomotopyFiber
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
hc : ∀ (i : α), ∃ (j : α), c.Rel i j
⊢ CategoryStruct.comp (Y := K.pathObject) (ι K) (π₀ K) = 𝟙 K

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyFiber
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 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
φ₀ φ₁ : F ⟶ K
h : Homotopy φ₀ φ₁
⊢ CategoryStruct.comp (Y := K.pathObject) (lift φ₀ φ₁ h) (π₀ K) = φ₀

Tactic:
Quiver.Hom.op_inj ((opFunctor C c).map_injective (cylinder.ι₀_desc _ _ _))

Premises used: Quiver.Hom.op_inj, HomologicalComplex.cylinder.ι₀_desc, HomologicalComplex.opFunctor, CategoryTheory.Functor.map_injective
-- Module: Mathlib.Algebra.Homology.HomotopyFiber
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 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
φ₀ φ₁ : F ⟶ K
h : Homotopy φ₀ φ₁
⊢ CategoryStruct.comp (Y := K.pathObject) (lift φ₀ φ₁ h) (π₁ K) = φ₁

Tactic:
Quiver.Hom.op_inj ((opFunctor C c).map_injective (cylinder.ι₁_desc _ _ _))

Premises used: Quiver.Hom.op_inj, HomologicalComplex.opFunctor, CategoryTheory.Functor.map_injective, HomologicalComplex.cylinder.ι₁_desc
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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
⊢ CategoryStruct.comp (Y := kernel g) (kernel.lift g f w) (kernel.ι g) = f

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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
inst_2 : HasImage f
g : B ⟶ C
inst_3 : HasKernel g
w : f ≫ g = 0
⊢ Mono (Y := Functor.obj Subobject.underlying (kernelSubobject g)) ((imageSubobject f).ofLE (kernelSubobject g) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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
h : imageSubobject f ≤ kernelSubobject g
⊢ (imageSubobject f).ofLE (kernelSubobject g) h = imageToKernel f g w

Tactic:
rfl

Premises used: imageToKernel, rfl
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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
⊢ imageToKernel f g w ≫ (kernelSubobject g).arrow = (imageSubobject f).arrow

Tactic:
simp [imageToKernel]

Premises used: imageToKernel
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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
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
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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
⊢ 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:
simp
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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
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)
⊢ 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

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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) ⟶ B)
    (imageToKernel 0 g w ≫ (kernelSubobject g).arrow) (0 ≫ (kernelSubobject g).arrow)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ImageToKernel
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
inst_2 : HasImages.{v, u} V
w : Eq (α := A ⟶ C) (f ≫ 0) 0
⊢ Eq (α :=
    Functor.obj Subobject.underlying (imageSubobject f) ⟶
      Functor.obj (C := Subobject.{v, u} B) Subobject.underlying (kernelSubobject (Y := C) 0))
    (imageToKernel f 0 w) ((imageSubobject f).arrow ≫ inv (Subobject.arrow (kernelSubobject (Y := C) 0)))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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 : HasKernels.{v, u} V
inst_3 : HasImages.{v, u} V
D : V
h : C ⟶ D
w : f ≫ g = 0
⊢ f ≫ g ≫ h = 0

Tactic:
simp [reassoc_of% w]
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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
h₁ :
  Eq (α := Functor.obj Subobject.underlying (imageSubobject f) ⟶ B)
    (imageToKernel f (g ≫ h) ⋯ ≫ (kernelSubobject (g ≫ h)).arrow)
    ((imageToKernel f g w ≫ (kernelSubobject g).ofLE (kernelSubobject (g ≫ h)) ⋯) ≫ (kernelSubobject (g ≫ h)).arrow)
⊢ 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)) ⋯)

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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) ⟶ B)
    (imageToKernel f (g ≫ h) ⋯ ≫ (kernelSubobject (g ≫ h)).arrow)
    ((imageToKernel f g w ≫ (kernelSubobject g).ofLE (kernelSubobject (g ≫ h)) ⋯) ≫ (kernelSubobject (g ≫ h)).arrow)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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 : HasKernels.{v, u} V
inst_3 : HasImages.{v, u} V
Z : V
h : Z ⟶ A
w : f ≫ g = 0
⊢ (h ≫ f) ≫ g = 0

Tactic:
simp [w]
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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
h₁ :
  imageToKernel (h ≫ f) g ⋯ ≫ (kernelSubobject g).arrow =
    CategoryStruct.comp (Y := Functor.obj Subobject.underlying (imageSubobject f))
        ((imageSubobject (h ≫ f)).ofLE (imageSubobject f) ⋯) (imageToKernel f g w) ≫
      (kernelSubobject g).arrow
⊢ 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))

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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
⊢ imageToKernel (h ≫ f) g ⋯ ≫ (kernelSubobject g).arrow =
    CategoryStruct.comp (Y := Functor.obj Subobject.underlying (imageSubobject f))
        ((imageSubobject (h ≫ f)).ofLE (imageSubobject f) ⋯) (imageToKernel f g w) ≫
      (kernelSubobject g).arrow

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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 : HasKernels.{v, u} V
inst_3 : HasImages.{v, u} V
D : V
h : C ⟶ D
inst_4 : Mono h
w : f ≫ g ≫ h = 0
⊢ (f ≫ g) ≫ h = 0 ≫ h

Tactic:
simpa using w
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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
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 ⋯)
        (Iso.inv ((kernelSubobject (g ≫ h)).isoOfEq (kernelSubobject g) ⋯)) ≫
      (kernelSubobject (g ≫ h)).arrow)
⊢ 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) ⋯)))

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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) ⟶ B)
    (imageToKernel f (g ≫ h) w ≫ (kernelSubobject (g ≫ h)).arrow)
    (CategoryStruct.comp (Y := Functor.obj Subobject.underlying (kernelSubobject g)) (imageToKernel f g ⋯)
        (Iso.inv ((kernelSubobject (g ≫ h)).isoOfEq (kernelSubobject g) ⋯)) ≫
      (kernelSubobject (g ≫ h)).arrow)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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 : HasKernels.{v, u} V
inst_3 : HasImages.{v, u} V
Z : V
h : Z ⟶ A
inst_4 : Epi h
w : (h ≫ f) ≫ g = 0
⊢ h ≫ f ≫ g = h ≫ 0

Tactic:
simpa using w
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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
h₁ :
  imageToKernel (h ≫ f) g w ≫ (kernelSubobject g).arrow =
    CategoryStruct.comp (Y := Functor.obj Subobject.underlying (imageSubobject f))
        ((imageSubobject (h ≫ f)).ofLE (imageSubobject f) ⋯) (imageToKernel f g ⋯) ≫
      (kernelSubobject g).arrow
⊢ 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 ⋯))

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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
⊢ imageToKernel (h ≫ f) g w ≫ (kernelSubobject g).arrow =
    CategoryStruct.comp (Y := Functor.obj Subobject.underlying (imageSubobject f))
        ((imageSubobject (h ≫ f)).ofLE (imageSubobject f) ⋯) (imageToKernel f g ⋯) ≫
      (kernelSubobject g).arrow

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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 : HasEqualizers.{v, u} V
inst_3 : HasImages.{v, u} V
Z : V
i : B ≅ Z
w : (f ≫ i.hom) ≫ i.inv ≫ g = 0
⊢ f ≫ g = 0

Tactic:
simpa using w
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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
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 ⋯)
            (Iso.inv (kernelSubobjectIsoComp i.inv g))) ≫
        (kernelSubobject (i.inv ≫ g)).arrow :
      Functor.obj Subobject.underlying (imageSubobject (f ≫ i.hom)) ⟶ Z)
⊢ 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)))

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ImageToKernel
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)) ⟶ 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 ⋯)
            (Iso.inv (kernelSubobjectIsoComp i.inv g))) ≫
        (kernelSubobject (i.inv ≫ g)).arrow :
      Functor.obj Subobject.underlying (imageSubobject (f ≫ i.hom)) ⟶ Z)

Tactic:
simp