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
P Q : C
f : P ⟶ Q
inst_2 : Mono f
a a' : Over.{v, u} P
ha : _root_.Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦a⟧) (pseudoApply f ⟦a'⟧)
this : _root_.Eq (α := Quotient (α := Over.{v, u} Q) (setoid Q)) ⟦Over.mk (a.hom ≫ f)⟧ ⟦Over.mk (a'.hom ≫ f)⟧
R : C
p : R ⟶ (Over.mk (a.hom ≫ f)).left
q : R ⟶ (Over.mk (a'.hom ≫ f)).left
ep : Epi p
Eq : Epi q
comm : p ≫ (Over.mk (a.hom ≫ f)).hom = q ≫ (Over.mk (a'.hom ≫ f)).hom
⊢ a ≈ a'

Tactic:
exact ⟨R, p, q, ep, Eq, (cancel_mono f).1 <| by
    simp only [Category.assoc]
    exact 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
h : Function.Injective (α := Pseudoelement.{v, u} P) (pseudoApply f)
a : Pseudoelement.{v, u} P
ha : pseudoApply f a = 0
⊢ pseudoApply f a = pseudoApply f 0

Tactic:
rw [← apply_zero f] at ha

Premises used: CategoryTheory.Abelian.Pseudoelement.apply_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
h : Function.Injective (α := Pseudoelement.{v, u} P) (pseudoApply f)
a : Pseudoelement.{v, u} P
ha : pseudoApply f a = pseudoApply f 0
⊢ a = 0

Tactic:
h ha
-- 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
h : Function.Injective (α := Pseudoelement.{v, u} P) (pseudoApply f)
a : Pseudoelement.{v, u} P
ha : pseudoApply f a = pseudoApply f 0
⊢ a = 0

Tactic:
exact h ha
-- 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
⊢ (∀ (a : Pseudoelement.{v, u} P), pseudoApply f a = 0 → a = 0) → Mono f

Tactic:
fun h => (mono_iff_cancel_zero _).2 fun _ g hg =>
    (pseudoZero_iff (g : Over P)).1 <|
      h _ <| show f g = 0 from (pseudoZero_iff (g ≫ f : Over Q)).2 hg

Premises used: Iff.mpr, CategoryTheory.Abelian.Pseudoelement.pseudoZero_iff, CategoryTheory.Over.mk, CategoryTheory.Abelian.PseudoEqual, CategoryTheory.CategoryStruct.comp, Iff.mp, CategoryTheory.Preadditive.mono_iff_cancel_zero, Quot.mk
-- 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
inst_2 : Epi f
qbar : Pseudoelement.{v, u} Q
q : Over.{v, u} Q
rw :
  Eq.{v + 1} (α := pullback f q.hom ⟶ Q)
    (Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) (Over.mk (Y := pullback f q.hom) (pullback.fst f q.hom))) :
      Over.left.{v, u} (X := Q)
          ((fun (g : Over.{v, u} P) ↦ app f g) (Over.mk (Y := pullback f q.hom) (pullback.fst f q.hom))) ⟶
        Q)
    (pullback.snd f q.hom ≫ q.hom)
rw₁ :
  Eq.{v + 1} (α := pullback f q.hom ⟶ Q)
    (Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) (Over.mk (Y := pullback f q.hom) (pullback.fst f q.hom))) :
      Over.left.{v, u} (X := Q)
          ((fun (g : Over.{v, u} P) ↦ app f g) (Over.mk (Y := pullback f q.hom) (pullback.fst f q.hom))) ⟶
        Q)
    (pullback.fst f q.hom ≫ f)
rw₂ : (Over.mk (Y := pullback f q.hom) (pullback.fst f q.hom)).hom ≫ f = pullback.fst f q.hom ≫ f
rw₃ rw₄ : Eq (α := pullback f q.hom ⟶ Q) (pullback.fst f q.hom ≫ f) (pullback.fst f q.hom ≫ f)
⊢ 𝟙 (pullback f q.hom) ≫
      Over.hom ((fun (g : Over.{v, u} P) ↦ app f g) (Over.mk (Y := pullback f q.hom) (pullback.fst f q.hom))) =
    pullback.snd f q.hom ≫ q.hom

Tactic:
rw [Category.id_comp, ← pullback.condition, app_hom, Over.coe_hom]

Premises used: CategoryTheory.Over.coe_hom, CategoryTheory.Limits.pullback.condition, CategoryTheory.Abelian.app_hom, CategoryTheory.Category.id_comp
-- 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
h : Function.Surjective (α := Pseudoelement.{v, u} P) (pseudoApply f)
have : ∀ (pbar : Pseudoelement.{v, u} P) (hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))), Epi f
⊢ Epi f

Tactic:
have ⟨pbar, hpbar⟩ := h (𝟙 Q)
-- 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
h : Function.Surjective (α := Pseudoelement.{v, u} P) (pseudoApply f)
pbar : Pseudoelement.{v, u} P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
have : ∀ (p : Over.{v, u} P) (hp : ⟦p⟧ = pbar), Epi f
⊢ Epi f

Tactic:
have ⟨p, hp⟩ := Quotient.exists_rep pbar
-- 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
h : Function.Surjective (α := Pseudoelement.{v, u} P) (pseudoApply f)
pbar : Pseudoelement.{v, u} P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over.{v, u} P
hp : ⟦p⟧ = pbar
⊢ Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦p⟧) (Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q)))

Tactic:
rw [← hp] at hpbar
-- 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
h : Function.Surjective (α := Pseudoelement.{v, u} P) (pseudoApply f)
pbar : Pseudoelement.{v, u} P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over.{v, u} P
hp : ⟦p⟧ = pbar
hpbar₁ : Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦p⟧) (Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q)))
⊢ ⟦p⟧ = pbar

Tactic:
rw [← hp] at hpbar
-- 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
h : Function.Surjective (α := Pseudoelement.{v, u} P) (pseudoApply f)
pbar : Pseudoelement.{v, u} P
p : Over.{v, u} P
hpbar : Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦p⟧) (Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q)))
hp : ⟦p⟧ = pbar
⊢ Eq (α := Quotient (α := Over.{v, u} Q) (setoid Q)) ⟦Over.mk (p.hom ≫ f)⟧ ⟦Over.mk (𝟙 Q)⟧

Tactic:
hpbar

Premises used: Quotient.map, CategoryTheory.Abelian.Pseudoelement, CategoryTheory.Abelian.app, CategoryTheory.Abelian.Pseudoelement.pseudoApply
-- 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
h : Function.Surjective (α := Pseudoelement.{v, u} P) (pseudoApply f)
pbar : Pseudoelement.{v, u} P
p : Over.{v, u} P
hpbar : Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦p⟧) (Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q)))
hp : ⟦p⟧ = pbar
⊢ Eq (α := Quotient (α := Over.{v, u} Q) (setoid Q)) ⟦Over.mk (p.hom ≫ f)⟧ ⟦Over.mk (𝟙 Q)⟧

Tactic:
exact hpbar
-- 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
h : Function.Surjective (α := Pseudoelement.{v, u} P) (pseudoApply f)
pbar : Pseudoelement.{v, u} P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over.{v, u} P
hp : ⟦p⟧ = pbar
⊢ Eq (α := Quotient (α := Over.{v, u} Q) (setoid Q)) ⟦Over.mk (p.hom ≫ f)⟧ ⟦Over.mk (𝟙 Q)⟧

Tactic:
have : (⟦(p.hom ≫ f : Over Q)⟧ : Quotient (setoid Q)) = ⟦↑(𝟙 Q)⟧ := by
    rw [← hp] at hpbar
    exact hpbar
-- 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
h : Function.Surjective (α := Pseudoelement.{v, u} P) (pseudoApply f)
pbar : Pseudoelement.{v, u} P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over.{v, u} P
hp : ⟦p⟧ = pbar
this : Eq (α := Quotient (α := Over.{v, u} Q) (setoid Q)) ⟦Over.mk (p.hom ≫ f)⟧ ⟦Over.mk (𝟙 Q)⟧
have :
  ∀ (R : C) (x : R ⟶ (Over.mk (p.hom ≫ f)).left) (y : R ⟶ Comma.left.{v, 0, v, u, 0, u} (Over.mk (𝟙 Q))),
    Epi x → ∀ (ey : Epi y) (comm : x ≫ (Over.mk (p.hom ≫ f)).hom = y ≫ Over.hom (Over.mk (𝟙 Q))), Epi f
⊢ Epi f

Tactic:
have ⟨R, x, y, _, ey, comm⟩ := Quotient.exact this
-- 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
h : Function.Surjective (α := Pseudoelement.{v, u} P) (pseudoApply f)
pbar : Pseudoelement.{v, u} P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over.{v, u} P
hp : ⟦p⟧ = pbar
this : Eq (α := Quotient (α := Over.{v, u} Q) (setoid Q)) ⟦Over.mk (p.hom ≫ f)⟧ ⟦Over.mk (𝟙 Q)⟧
R : C
x : R ⟶ (Over.mk (p.hom ≫ f)).left
y : R ⟶ Comma.left.{v, 0, v, u, 0, u} (Over.mk (𝟙 Q))
w : Epi x
ey : Epi y
comm : x ≫ (Over.mk (p.hom ≫ f)).hom = y ≫ Over.hom (Over.mk (𝟙 Q))
apply : (x ≫ p.hom) ≫ f = y
⊢ Epi f

Tactic:
apply @epi_of_epi_fac _ _ _ _ _ (x ≫ p.hom) f y ey

Premises used: CategoryTheory.epi_of_epi_fac
-- 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
h : Function.Surjective (α := Pseudoelement.{v, u} P) (pseudoApply f)
pbar : Pseudoelement.{v, u} P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over.{v, u} P
hp : ⟦p⟧ = pbar
this : Eq (α := Quotient (α := Over.{v, u} Q) (setoid Q)) ⟦Over.mk (p.hom ≫ f)⟧ ⟦Over.mk (𝟙 Q)⟧
R : C
x : R ⟶ (Over.mk (p.hom ≫ f)).left
y : R ⟶ Comma.left.{v, 0, v, u, 0, u} (Over.mk (𝟙 Q))
w : Epi x
ey : Epi y
comm : x ≫ p.hom ≫ f = y ≫ 𝟙 Q
rw : y ≫ 𝟙 Q = y
⊢ (x ≫ p.hom) ≫ f = y

Tactic:
rw [Category.assoc, comm]

Premises used: CategoryTheory.Category.assoc
-- 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
h : Function.Surjective (α := Pseudoelement.{v, u} P) (pseudoApply f)
pbar : Pseudoelement.{v, u} P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over.{v, u} P
hp : ⟦p⟧ = pbar
this : Eq (α := Quotient (α := Over.{v, u} Q) (setoid Q)) ⟦Over.mk (p.hom ≫ f)⟧ ⟦Over.mk (𝟙 Q)⟧
R : C
x : R ⟶ (Over.mk (p.hom ≫ f)).left
y : R ⟶ Comma.left.{v, 0, v, u, 0, u} (Over.mk (𝟙 Q))
w : Epi x
ey : Epi y
comm : x ≫ p.hom ≫ f = y ≫ 𝟙 Q
⊢ y ≫ 𝟙 Q = y

Tactic:
apply Category.comp_id

Premises used: CategoryTheory.Category.comp_id
-- 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 : S.Exact
b' : Pseudoelement.{v, u} S.X₂
b : Over.{v, u} S.X₂
hb : Eq (α := Pseudoelement.{v, u} S.X₃) (pseudoApply S.g ⟦b⟧) 0
⊢ b.hom ≫ S.g = 0

Tactic:
have hb' : b.hom ≫ S.g = 0 := (pseudoZero_iff _).1 hb
-- 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 : S.Exact
b' : Pseudoelement.{v, u} S.X₂
b : Over.{v, u} S.X₂
hb : Eq (α := Pseudoelement.{v, u} S.X₃) (pseudoApply S.g ⟦b⟧) 0
hb' : b.hom ≫ S.g = 0
obtain :
  ∀ (c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt) (hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom),
    ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = ⟦b⟧
⊢ ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = ⟦b⟧

Tactic:
obtain ⟨c, hc⟩ := KernelFork.IsLimit.lift' hS.isLimitImage _ hb'

Premises used: CategoryTheory.ShortComplex.Exact.isLimitImage, CategoryTheory.Limits.KernelFork.IsLimit.lift'
-- 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 : S.Exact
b' : Pseudoelement.{v, u} S.X₂
b : Over.{v, u} S.X₂
hb : Eq (α := Pseudoelement.{v, u} S.X₃) (pseudoApply S.g ⟦b⟧) 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
h :
  Eq (α := Pseudoelement.{v, u} S.X₂)
    (pseudoApply S.f
      (Quot.mk (PseudoEqual S.X₁)
        (Over.mk (Y := pullback (Abelian.factorThruImage S.f) c) (pullback.fst (Abelian.factorThruImage S.f) c))))
    ⟦b⟧
⊢ ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = ⟦b⟧

Tactic:
use pullback.fst (Abelian.factorThruImage S.f) c

Premises used: CategoryTheory.Abelian.factorThruImage, CategoryTheory.Limits.pullback.fst, CategoryTheory.ShortComplex.f
-- 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 : S.Exact
b' : Pseudoelement.{v, u} S.X₂
b : Over.{v, u} S.X₂
hb : Eq (α := Pseudoelement.{v, u} S.X₃) (pseudoApply S.g ⟦b⟧) 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
h :
  (fun (g : Over.{v, u} S.X₁) ↦ app S.f g)
      (Over.mk (Y := pullback (Abelian.factorThruImage S.f) c) (pullback.fst (Abelian.factorThruImage S.f) c)) ≈
    b
⊢ Eq (α := Pseudoelement.{v, u} S.X₂)
    (pseudoApply S.f
      (Quot.mk (PseudoEqual S.X₁)
        (Over.mk (Y := pullback (Abelian.factorThruImage S.f) c) (pullback.fst (Abelian.factorThruImage S.f) c))))
    ⟦b⟧

Tactic:
apply Quotient.sound

Premises used: Quotient.sound
-- 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 : S.Exact
b' : Pseudoelement.{v, u} S.X₂
b : Over.{v, u} S.X₂
hb : Eq (α := Pseudoelement.{v, u} S.X₃) (pseudoApply S.g ⟦b⟧) 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ (fun (g : Over.{v, u} S.X₁) ↦ app S.f g)
      (Over.mk (Y := pullback (Abelian.factorThruImage S.f) c) (pullback.fst (Abelian.factorThruImage S.f) c)) ≈
    b

Tactic:
⟨pullback (Abelian.factorThruImage S.f) c, 𝟙 _,
              pullback.snd _ _, inferInstance, inferInstance, ?_⟩

Premises used: CategoryTheory.Limits.pullback, CategoryTheory.Abelian.factorThruImage, CategoryTheory.Limits.pullback.snd, CategoryTheory.CategoryStruct.id, inferInstance, CategoryTheory.Abelian.PseudoEqual, Exists.intro, CategoryTheory.ShortComplex.f
-- 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 : S.Exact
b' : Pseudoelement.{v, u} S.X₂
b : Over.{v, u} S.X₂
hb : Eq (α := Pseudoelement.{v, u} S.X₃) (pseudoApply S.g ⟦b⟧) 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
h :
  𝟙 (pullback (Abelian.factorThruImage S.f) c) ≫
      Over.hom
        ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g)
          (Over.mk (Y := pullback (Abelian.factorThruImage S.f) c) (pullback.fst (Abelian.factorThruImage S.f) c))) =
    pullback.snd (Abelian.factorThruImage S.f) c ≫ b.hom
⊢ (fun (g : Over.{v, u} S.X₁) ↦ app S.f g)
      (Over.mk (Y := pullback (Abelian.factorThruImage S.f) c) (pullback.fst (Abelian.factorThruImage S.f) c)) ≈
    b

Tactic:
refine ⟨pullback (Abelian.factorThruImage S.f) c, 𝟙 _,
              pullback.snd _ _, inferInstance, inferInstance, ?_⟩
-- 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 : S.Exact
b' : Pseudoelement.{v, u} S.X₂
b : Over.{v, u} S.X₂
hb : Eq (α := Pseudoelement.{v, u} S.X₃) (pseudoApply S.g ⟦b⟧) 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ 𝟙 (pullback (Abelian.factorThruImage S.f) c) ≫ pullback.fst (Abelian.factorThruImage S.f) c ≫ S.f =
    pullback.fst (Abelian.factorThruImage S.f) c ≫ S.f

Tactic:
Category.id_comp _

Premises used: CategoryTheory.Category.id_comp
-- 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 : S.Exact
b' : Pseudoelement.{v, u} S.X₂
b : Over.{v, u} S.X₂
hb : Eq (α := Pseudoelement.{v, u} S.X₃) (pseudoApply S.g ⟦b⟧) 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
rw rw₁ :
  Eq (α := pullback (Abelian.factorThruImage S.f) c ⟶ S.X₂) (pullback.fst (Abelian.factorThruImage S.f) c ≫ S.f)
    (pullback.fst (Abelian.factorThruImage S.f) c ≫ S.f)
⊢ Eq (α := pullback (Abelian.factorThruImage S.f) c ⟶ S.X₂) (pullback.fst (Abelian.factorThruImage S.f) c ≫ S.f)
    (pullback.fst (Abelian.factorThruImage S.f) c ≫
      CategoryStruct.comp (Y := Abelian.image S.f) (Abelian.factorThruImage S.f) (kernel.ι (cokernel.π S.f)))

Tactic:
rw [Abelian.image.fac]

Premises used: 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 : S.Exact
b' : Pseudoelement.{v, u} S.X₂
b : Over.{v, u} S.X₂
hb : Eq (α := Pseudoelement.{v, u} S.X₃) (pseudoApply S.g ⟦b⟧) 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
rw :
  Eq (α := pullback (Abelian.factorThruImage S.f) c ⟶ S.X₂)
    (CategoryStruct.comp (Y := Abelian.image S.f)
      (pullback.fst (Abelian.factorThruImage S.f) c ≫ Abelian.factorThruImage S.f) (kernel.ι (cokernel.π S.f)))
    ((pullback.snd (Abelian.factorThruImage S.f) c ≫ c) ≫ kernel.ι (cokernel.π S.f))
rw₁ rw₂ :
  Eq (α := pullback (Abelian.factorThruImage S.f) c ⟶ S.X₂)
    ((pullback.snd (Abelian.factorThruImage S.f) c ≫ c) ≫ kernel.ι (cokernel.π S.f))
    ((pullback.snd (Abelian.factorThruImage S.f) c ≫ c) ≫ kernel.ι (cokernel.π S.f))
⊢ Eq (α := pullback (Abelian.factorThruImage S.f) c ⟶ S.X₂)
    (pullback.fst (Abelian.factorThruImage S.f) c ≫
      CategoryStruct.comp (Y := Abelian.image S.f) (Abelian.factorThruImage S.f) (kernel.ι (cokernel.π S.f)))
    ((pullback.snd (Abelian.factorThruImage S.f) c ≫ c) ≫ kernel.ι (cokernel.π S.f))

Tactic:
rw [← Category.assoc, pullback.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.condition
-- 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 : S.Exact
b' : Pseudoelement.{v, u} S.X₂
b : Over.{v, u} S.X₂
hb : Eq (α := Pseudoelement.{v, u} S.X₃) (pseudoApply S.g ⟦b⟧) 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
rw :
  Eq (α := pullback (Abelian.factorThruImage S.f) c ⟶ S.X₂)
    (pullback.snd (Abelian.factorThruImage S.f) c ≫ c ≫ kernel.ι (cokernel.π S.f))
    (pullback.snd (Abelian.factorThruImage S.f) c ≫ b.hom)
⊢ Eq (α := pullback (Abelian.factorThruImage S.f) c ⟶ S.X₂)
    ((pullback.snd (Abelian.factorThruImage S.f) c ≫ c) ≫ kernel.ι (cokernel.π S.f))
    (pullback.snd (Abelian.factorThruImage S.f) c ≫ b.hom)

Tactic:
rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- 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 : S.Exact
b' : Pseudoelement.{v, u} S.X₂
b : Over.{v, u} S.X₂
hb : Eq (α := Pseudoelement.{v, u} S.X₃) (pseudoApply S.g ⟦b⟧) 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ Eq (α := pullback (Abelian.factorThruImage S.f) c ⟶ S.X₂)
    (pullback.snd (Abelian.factorThruImage S.f) c ≫ c ≫ kernel.ι (cokernel.π S.f))
    (pullback.snd (Abelian.factorThruImage S.f) c ≫ b.hom)

Tactic:
congr
-- 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 : S.Exact
b' : Pseudoelement.{v, u} S.X₂
b : Over.{v, u} S.X₂
hb : Eq (α := Pseudoelement.{v, u} S.X₃) (pseudoApply S.g ⟦b⟧) 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
_ :
  Eq (α := pullback (Abelian.factorThruImage S.f) c ⟶ S.X₂) (pullback.fst (Abelian.factorThruImage S.f) c ≫ S.f)
    (pullback.fst (Abelian.factorThruImage S.f) c ≫
      CategoryStruct.comp (Y := Abelian.image S.f) (Abelian.factorThruImage S.f) (kernel.ι (cokernel.π S.f)))
_₁ :
  Eq (α := pullback (Abelian.factorThruImage S.f) c ⟶ S.X₂)
    (pullback.fst (Abelian.factorThruImage S.f) c ≫
      CategoryStruct.comp (Y := Abelian.image S.f) (Abelian.factorThruImage S.f) (kernel.ι (cokernel.π S.f)))
    ((pullback.snd (Abelian.factorThruImage S.f) c ≫ c) ≫ kernel.ι (cokernel.π S.f))
_₂ :
  Eq (α := pullback (Abelian.factorThruImage S.f) c ⟶ S.X₂)
    ((pullback.snd (Abelian.factorThruImage S.f) c ≫ c) ≫ kernel.ι (cokernel.π S.f))
    (pullback.snd (Abelian.factorThruImage S.f) c ≫ b.hom)
⊢ 𝟙 (pullback (Abelian.factorThruImage S.f) c) ≫
      Over.hom
        ((fun (g : Over.{v, u} S.X₁) ↦ app S.f g)
          (Over.mk (Y := pullback (Abelian.factorThruImage S.f) c) (pullback.fst (Abelian.factorThruImage S.f) c))) =
    pullback.snd (Abelian.factorThruImage S.f) c ≫ b.hom

Tactic:
calc
        𝟙 (pullback (Abelian.factorThruImage S.f) c) ≫ pullback.fst _ _ ≫ S.f =
          pullback.fst _ _ ≫ S.f :=
          Category.id_comp _
        _ = pullback.fst _ _ ≫ Abelian.factorThruImage S.f ≫ kernel.ι (cokernel.π S.f) := by
          rw [Abelian.image.fac]
        _ = (pullback.snd _ _ ≫ c) ≫ kernel.ι (cokernel.π S.f) := by
          rw [← Category.assoc, pullback.condition]
        _ = pullback.snd _ _ ≫ b.hom := by
          rw [Category.assoc]
          congr

Premises used: CategoryTheory.Limits.pullback, CategoryTheory.Abelian.factorThruImage, CategoryTheory.Limits.pullback.snd, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.pullback.fst, CategoryTheory.CategoryStruct.comp, CategoryTheory.ShortComplex.f, CategoryTheory.Limits.cokernel.π, CategoryTheory.Over.hom, CategoryTheory.Limits.kernel.ι, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P Q R : C
f : Q ⟶ R
a : P ⟶ Q
h : a ≫ f = 0
⊢ Eq (α := Pseudoelement.{v, u} R) (pseudoApply f (Quot.mk (PseudoEqual Q) (Over.mk a))) 0

Tactic:
simp [over_coe_def, pseudoApply_mk', h]

Premises used: CategoryTheory.Abelian.Pseudoelement.pseudoApply_mk', CategoryTheory.Abelian.Pseudoelement.over_coe_def
-- 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
⊢ Eq (α := Pseudoelement.{v, u} S.X₃)
    (pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (Y := kernel S.g) (kernel.ι S.g)))) 0

Tactic:
have : S.g (kernel.ι S.g) = 0 := apply_eq_zero_of_comp_eq_zero _ _ (kernel.condition _)
-- 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
obtain :
  ∀ (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))),
    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 ⟨a', ha⟩ := hS _ this
-- 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))
obtain :
  ∀ (a : Over.{v, u} S.X₁) (ha' : ⟦a⟧ = a'), 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 ⟨a, ha'⟩ := Quotient.exists_rep a'

Premises used: Quotient.exists_rep