awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : ∀ (b : Pseudoelement.{v, u} S.X₂), pseudoApply S.g b = 0 → ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = b
this :
  Eq (α := Pseudoelement.{v, u} S.X₃)
    (pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))) 0
a' : Pseudoelement.{v, u} S.X₁
ha : pseudoApply S.f a' = Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g))
a : Over.{v, u} S.X₁
ha' : ⟦a⟧ = a'
⊢ Eq (α := Pseudoelement.{v, u} S.X₂) (pseudoApply S.f ⟦a⟧)
    (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))

Tactic:
rw [← ha'] at ha
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : ∀ (b : Pseudoelement.{v, u} S.X₂), pseudoApply S.g b = 0 → ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = b
this :
  Eq (α := Pseudoelement.{v, u} S.X₃)
    (pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))) 0
a' : Pseudoelement.{v, u} S.X₁
ha : pseudoApply S.f a' = Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g))
a : Over.{v, u} S.X₁
ha' : ⟦a⟧ = a'
ha₁ :
  Eq (α := Pseudoelement.{v, u} S.X₂) (pseudoApply S.f ⟦a⟧)
    (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))
⊢ ⟦a⟧ = a'

Tactic:
rw [← ha'] at ha
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : ∀ (b : Pseudoelement.{v, u} S.X₂), pseudoApply S.g b = 0 → ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = b
this :
  Eq (α := Pseudoelement.{v, u} S.X₃)
    (pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))) 0
a' : Pseudoelement.{v, u} S.X₁
a : Over.{v, u} S.X₁
ha :
  Eq (α := Pseudoelement.{v, u} S.X₂) (pseudoApply S.f ⟦a⟧)
    (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))
ha' : ⟦a⟧ = a'
obtain :
  ∀ (Z : C)
    (r :
      Z ⟶
        Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit S.X₂)
          ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a))
    (q : Z ⟶ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).left),
    Epi r →
      ∀ (eq : Epi q)
        (comm :
          r ≫ Over.hom ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a) =
            q ≫ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).hom),
        Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
⊢ Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0

Tactic:
obtain ⟨Z, r, q, _, eq, comm⟩ := Quotient.exact ha

Premises used: comm, Quotient.exact
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : ∀ (b : Pseudoelement.{v, u} S.X₂), pseudoApply S.g b = 0 → ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = b
this :
  Eq (α := Pseudoelement.{v, u} S.X₃)
    (pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))) 0
a' : Pseudoelement.{v, u} S.X₁
a : Over.{v, u} S.X₁
ha :
  Eq (α := Pseudoelement.{v, u} S.X₂) (pseudoApply S.f ⟦a⟧)
    (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))
ha' : ⟦a⟧ = a'
Z : C
r :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit S.X₂)
      ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a)
q : Z ⟶ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).left
w : Epi r
eq : Epi q
comm : r ≫ Over.hom ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a) = q ≫ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).hom
simp : r ≫ a.hom ≫ S.f = q ≫ kernel.ι S.g
⊢ CategoryStruct.comp (Y := kernel (Y := cokernel S.f) (cokernel.π S.f)) (r ≫ a.hom ≫ Abelian.factorThruImage S.f)
      (kernel.ι (cokernel.π S.f)) =
    q ≫ kernel.ι S.g

Tactic:
simp only [Category.assoc, Abelian.image.fac]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Abelian.image.fac
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : ∀ (b : Pseudoelement.{v, u} S.X₂), pseudoApply S.g b = 0 → ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = b
this :
  Eq (α := Pseudoelement.{v, u} S.X₃)
    (pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))) 0
a' : Pseudoelement.{v, u} S.X₁
a : Over.{v, u} S.X₁
ha :
  Eq (α := Pseudoelement.{v, u} S.X₂) (pseudoApply S.f ⟦a⟧)
    (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))
ha' : ⟦a⟧ = a'
Z : C
r :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit S.X₂)
      ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a)
q : Z ⟶ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).left
w : Epi r
eq : Epi q
comm : r ≫ Over.hom ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a) = q ≫ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).hom
⊢ r ≫ a.hom ≫ S.f = q ≫ kernel.ι S.g

Tactic:
comm

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Over, CategoryTheory.CostructuredArrow, CategoryTheory.Limits.limit
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : ∀ (b : Pseudoelement.{v, u} S.X₂), pseudoApply S.g b = 0 → ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = b
this :
  Eq (α := Pseudoelement.{v, u} S.X₃)
    (pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))) 0
a' : Pseudoelement.{v, u} S.X₁
a : Over.{v, u} S.X₁
ha :
  Eq (α := Pseudoelement.{v, u} S.X₂) (pseudoApply S.f ⟦a⟧)
    (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))
ha' : ⟦a⟧ = a'
Z : C
r :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit S.X₂)
      ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a)
q : Z ⟶ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).left
w : Epi r
eq : Epi q
comm : r ≫ Over.hom ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a) = q ≫ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).hom
⊢ r ≫ a.hom ≫ S.f = q ≫ kernel.ι S.g

Tactic:
exact comm
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : ∀ (b : Pseudoelement.{v, u} S.X₂), pseudoApply S.g b = 0 → ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = b
this :
  Eq (α := Pseudoelement.{v, u} S.X₃)
    (pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))) 0
a' : Pseudoelement.{v, u} S.X₁
a : Over.{v, u} S.X₁
ha :
  Eq (α := Pseudoelement.{v, u} S.X₂) (pseudoApply S.f ⟦a⟧)
    (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))
ha' : ⟦a⟧ = a'
Z : C
r :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit S.X₂)
      ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a)
q : Z ⟶ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).left
w : Epi r
eq : Epi q
comm : r ≫ Over.hom ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a) = q ≫ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).hom
obtain :
  ∀
    (z :
      Z ⟶
        pullback (X := kernel (Y := cokernel S.f) (cokernel.π S.f)) (Y := kernel S.g) (kernel.ι (cokernel.π S.f))
          (kernel.ι S.g)),
    z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f →
      ∀ (hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q),
        Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
⊢ Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0

Tactic:
obtain ⟨z, _, hz₂⟩ := @pullback.lift' _ _ _ _ _ _ (kernel.ι (cokernel.π S.f))
        (kernel.ι S.g) _ (r ≫ a.hom ≫ Abelian.factorThruImage S.f) q (by
          simp only [Category.assoc, Abelian.image.fac]
          exact comm)

Premises used: CategoryTheory.Abelian.factorThruImage, CategoryTheory.Limits.pullback.lift', CategoryTheory.CategoryStruct.comp, CategoryTheory.ShortComplex.f, CategoryTheory.Over.hom
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : ∀ (b : Pseudoelement.{v, u} S.X₂), pseudoApply S.g b = 0 → ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = b
this :
  Eq (α := Pseudoelement.{v, u} S.X₃)
    (pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))) 0
a' : Pseudoelement.{v, u} S.X₁
a : Over.{v, u} S.X₁
ha :
  Eq (α := Pseudoelement.{v, u} S.X₂) (pseudoApply S.f ⟦a⟧)
    (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))
ha' : ⟦a⟧ = a'
Z : C
r :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit S.X₂)
      ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a)
q : Z ⟶ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).left
w : Epi r
eq : Epi q
comm : r ≫ Over.hom ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a) = q ≫ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).hom
z :
  Z ⟶
    pullback (X := kernel (Y := cokernel S.f) (cokernel.π S.f)) (Y := kernel S.g) (kernel.ι (cokernel.π S.f))
      (kernel.ι S.g)
left : z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f
hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q
j : pullback (X := kernel (Y := cokernel S.f) (cokernel.π S.f)) (Y := kernel S.g) (kernel.ι (cokernel.π S.f))
    (kernel.ι S.g) ⟶
  kernel S.g :=
  pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
⊢ Epi j

Tactic:
haveI pe : Epi j := epi_of_epi_fac hz₂
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : ∀ (b : Pseudoelement.{v, u} S.X₂), pseudoApply S.g b = 0 → ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = b
this :
  Eq (α := Pseudoelement.{v, u} S.X₃)
    (pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))) 0
a' : Pseudoelement.{v, u} S.X₁
a : Over.{v, u} S.X₁
ha :
  Eq (α := Pseudoelement.{v, u} S.X₂) (pseudoApply S.f ⟦a⟧)
    (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))
ha' : ⟦a⟧ = a'
Z : C
r :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit S.X₂)
      ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a)
q : Z ⟶ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).left
w : Epi r
eq : Epi q
comm : r ≫ Over.hom ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a) = q ≫ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).hom
z :
  Z ⟶
    pullback (X := kernel (Y := cokernel S.f) (cokernel.π S.f)) (Y := kernel S.g) (kernel.ι (cokernel.π S.f))
      (kernel.ι S.g)
left : z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f
hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q
j : pullback (X := kernel (Y := cokernel S.f) (cokernel.π S.f)) (Y := kernel S.g) (kernel.ι (cokernel.π S.f))
    (kernel.ι S.g) ⟶
  kernel S.g :=
  pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
pe : Epi j
⊢ IsIso j

Tactic:
haveI : IsIso j := isIso_of_mono_of_epi _
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : ∀ (b : Pseudoelement.{v, u} S.X₂), pseudoApply S.g b = 0 → ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = b
this_1 :
  Eq (α := Pseudoelement.{v, u} S.X₃)
    (pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))) 0
a' : Pseudoelement.{v, u} S.X₁
a : Over.{v, u} S.X₁
ha :
  Eq (α := Pseudoelement.{v, u} S.X₂) (pseudoApply S.f ⟦a⟧)
    (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))
ha' : ⟦a⟧ = a'
Z : C
r :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit S.X₂)
      ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a)
q : Z ⟶ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).left
w : Epi r
eq : Epi q
comm : r ≫ Over.hom ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a) = q ≫ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).hom
z :
  Z ⟶
    pullback (X := kernel (Y := cokernel S.f) (cokernel.π S.f)) (Y := kernel S.g) (kernel.ι (cokernel.π S.f))
      (kernel.ι S.g)
left : z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f
hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q
j : pullback (X := kernel (Y := cokernel S.f) (cokernel.π S.f)) (Y := kernel S.g) (kernel.ι (cokernel.π S.f))
    (kernel.ι S.g) ⟶
  kernel S.g :=
  pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
pe : Epi j
this : IsIso j
rw :
  Eq (α := kernel S.g ⟶ cokernel S.f)
    (((asIso j).inv ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ≫ kernel.ι (cokernel.π S.f)) ≫
      cokernel.π S.f)
    0
⊢ Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0

Tactic:
rw [(Iso.eq_inv_comp (asIso j)).2 pullback.condition.symm]

Premises used: Iff.mpr, CategoryTheory.Limits.pullback.condition, CategoryTheory.Iso.eq_inv_comp, Eq.symm, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : ∀ (b : Pseudoelement.{v, u} S.X₂), pseudoApply S.g b = 0 → ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = b
this_1 :
  Eq (α := Pseudoelement.{v, u} S.X₃)
    (pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))) 0
a' : Pseudoelement.{v, u} S.X₁
a : Over.{v, u} S.X₁
ha :
  Eq (α := Pseudoelement.{v, u} S.X₂) (pseudoApply S.f ⟦a⟧)
    (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))
ha' : ⟦a⟧ = a'
Z : C
r :
  Z ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit S.X₂)
      ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a)
q : Z ⟶ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).left
w : Epi r
eq : Epi q
comm : r ≫ Over.hom ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g) a) = q ≫ (Over.mk (Y := kernel S.g) (kernel.ι S.g)).hom
z :
  Z ⟶
    pullback (X := kernel (Y := cokernel S.f) (cokernel.π S.f)) (Y := kernel S.g) (kernel.ι (cokernel.π S.f))
      (kernel.ι S.g)
left : z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f
hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q
j : pullback (X := kernel (Y := cokernel S.f) (cokernel.π S.f)) (Y := kernel S.g) (kernel.ι (cokernel.π S.f))
    (kernel.ι S.g) ⟶
  kernel S.g :=
  pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
pe : Epi j
this : IsIso j
⊢ Eq (α := kernel S.g ⟶ cokernel S.f)
    (((asIso j).inv ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ≫ kernel.ι (cokernel.π S.f)) ≫
      cokernel.π S.f)
    0

Tactic:
simp only [Category.assoc, kernel.condition, HasZeroMorphisms.comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.kernel.condition, CategoryTheory.Limits.HasZeroMorphisms.comp_zero
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
x y : Pseudoelement.{v, u} P
a a' : Over.{v, u} P
h : Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) (pseudoApply f ⟦a'⟧)
R : C
p :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a)
q :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a')
ep : Epi p
w : Epi q
comm : p ≫ a.hom ≫ f = q ≫ a'.hom ≫ f
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
⊢ Eq (α := Quotient (α := Over.{v, u} Q) (setoid Q)) ⟦Over.mk (a'' ≫ f)⟧ ⟦Over.mk (Y := Q) 0⟧

Tactic:
simp [a'', sub_eq_zero.2 comm]

Premises used: Iff.mpr, sub_eq_zero
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
x y : Pseudoelement.{v, u} P
a a' : Over.{v, u} P
h : Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) (pseudoApply f ⟦a'⟧)
R : C
p :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a)
q :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a')
ep : Epi p
w : Epi q
comm : p ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) a) = q ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) a')
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : Eq (α := Pseudoelement.{v, u} Z) (pseudoApply g ⟦a'⟧) 0
obtain :
  ∀ (X : C)
    (p' :
      X ⟶
        Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Z)
          ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a'))
    (q' : X ⟶ Comma.left.{v, 0, v, u, 0, u} (R := Functor.fromPUnit Z) (Over.mk (Y := Z) 0)) (ep' : Epi p'),
    Epi q' →
      ∀ (comm' : p' ≫ Over.hom ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a') = q' ≫ Over.hom (Over.mk (Y := Z) 0)),
        Eq (α := Pseudoelement.{v, u} Z) (pseudoApply g (Quot.mk (PseudoEqual P) (Over.mk a''))) (pseudoApply g ⟦a⟧)
⊢ Eq (α := Pseudoelement.{v, u} Z) (pseudoApply g (Quot.mk (PseudoEqual P) (Over.mk a''))) (pseudoApply g ⟦a⟧)

Tactic:
obtain ⟨X, p', q', ep', _, comm'⟩ := Quotient.exact hh

Premises used: Quotient.exact
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
x y : Pseudoelement.{v, u} P
a a' : Over.{v, u} P
h : Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) (pseudoApply f ⟦a'⟧)
R : C
p :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a)
q :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a')
ep : Epi p
w : Epi q
comm : p ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) a) = q ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) a')
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : Eq (α := Pseudoelement.{v, u} Z) (pseudoApply g ⟦a'⟧) 0
X : C
p' :
  X ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Z)
      ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a')
q' : X ⟶ Comma.left.{v, 0, v, u, 0, u} (R := Functor.fromPUnit Z) (Over.mk (Y := Z) 0)
ep' : Epi p'
w_1 : Epi q'
comm' : p' ≫ Over.hom ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a') = q' ≫ Over.hom (Over.mk (Y := Z) 0)
apply : p' ≫ a'.hom ≫ g = 0
⊢ a'.hom ≫ g = 0

Tactic:
apply (epi_iff_cancel_zero _).1 ep' _ (a'.hom ≫ g)

Premises used: CategoryTheory.Preadditive.epi_iff_cancel_zero, CategoryTheory.CategoryStruct.comp, Iff.mp, CategoryTheory.Over.hom
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
x y : Pseudoelement.{v, u} P
a a' : Over.{v, u} P
h : Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) (pseudoApply f ⟦a'⟧)
R : C
p :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a)
q :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a')
ep : Epi p
w : Epi q
comm : p ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) a) = q ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) a')
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : Eq (α := Pseudoelement.{v, u} Z) (pseudoApply g ⟦a'⟧) 0
X : C
p' :
  X ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Z)
      ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a')
q' : X ⟶ Comma.left.{v, 0, v, u, 0, u} (R := Functor.fromPUnit Z) (Over.mk (Y := Z) 0)
ep' : Epi p'
w_1 : Epi q'
comm' : p' ≫ Over.hom ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a') = q' ≫ Over.hom (Over.mk (Y := Z) 0)
⊢ p' ≫ a'.hom ≫ g = 0

Tactic:
simpa using comm'
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
x y : Pseudoelement.{v, u} P
a a' : Over.{v, u} P
h : Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) (pseudoApply f ⟦a'⟧)
R : C
p :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a)
q :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a')
ep : Epi p
w : Epi q
comm : p ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) a) = q ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) a')
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : Eq (α := Pseudoelement.{v, u} Z) (pseudoApply g ⟦a'⟧) 0
X : C
p' :
  X ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Z)
      ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a')
q' : X ⟶ Comma.left.{v, 0, v, u, 0, u} (R := Functor.fromPUnit Z) (Over.mk (Y := Z) 0)
ep' : Epi p'
w_1 : Epi q'
comm' : p' ≫ Over.hom ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a') = q' ≫ Over.hom (Over.mk (Y := Z) 0)
⊢ a'.hom ≫ g = 0

Tactic:
have : a'.hom ≫ g = 0 := by
            apply (epi_iff_cancel_zero _).1 ep' _ (a'.hom ≫ g)
            simpa using comm'
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q : C
f : P ⟶ Q
x y : Pseudoelement.{v, u} P
a a' : Over.{v, u} P
h : Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) (pseudoApply f ⟦a'⟧)
R : C
p :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a)
q :
  R ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Q)
      ((fun (g : Over.{v, u} P) ↦ app f g) a')
ep : Epi p
w : Epi q
comm : p ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) a) = q ≫ Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) a')
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : Eq (α := Pseudoelement.{v, u} Z) (pseudoApply g ⟦a'⟧) 0
X : C
p' :
  X ⟶
    Comma.left.{v, 0, v, u, 0, u} (B := Discrete PUnit.{1}) (T := C) (L := 𝟭 C) (R := Functor.fromPUnit Z)
      ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a')
q' : X ⟶ Comma.left.{v, 0, v, u, 0, u} (R := Functor.fromPUnit Z) (Over.mk (Y := Z) 0)
ep' : Epi p'
w_1 : Epi q'
comm' : p' ≫ Over.hom ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a') = q' ≫ Over.hom (Over.mk (Y := Z) 0)
this : a'.hom ≫ g = 0
a₁ :
  HasEquiv.Equiv (α := Over.{v, u} Z) ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) (Over.mk a''))
    ((fun (g_1 : Over.{v, u} P) ↦ app g g_1) a)
⊢ Eq (α := Pseudoelement.{v, u} Z) (pseudoApply g (Quot.mk (PseudoEqual P) (Over.mk a''))) (pseudoApply g ⟦a⟧)

Tactic:
apply Quotient.sound

Premises used: Quotient.sound