awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
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)
⊢ 𝟙 (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
have 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)
Tactic: rw [Category.id_comp, ← pullback.condition, app_hom, Over.coe_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
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)
⊢ 𝟙 (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
have rw₂ : (Over.mk (Y := pullback f q.hom) (pullback.fst f q.hom)).hom ≫ f = pullback.fst f q.hom ≫ f
Tactic: rw [Category.id_comp, ← pullback.condition, app_hom, Over.coe_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
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
⊢ 𝟙 (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
have rw₃ : Eq (α := pullback f q.hom ⟶ Q) (pullback.fst f q.hom ≫ f) (pullback.fst f q.hom ≫ f)
Tactic: rw [Category.id_comp, ← pullback.condition, app_hom, Over.coe_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
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)
⊢ Epi f
have have : ∀ (pbar : Pseudoelement.{v, u} P) (hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))), Epi f
Tactic: have ⟨pbar, hpbar⟩ := h (𝟙 Q)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
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))
⊢ Epi f
have have : ∀ (p : Over.{v, u} P) (hp : ⟦p⟧ = pbar), Epi f
Tactic: have ⟨p, hp⟩ := Quotient.exists_rep pbar
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (hypothesis)
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)⟧
have hpbar₁ : Eq (α := Pseudoelement.{v, u} Q) (pseudoApply f ⟦p⟧) (Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q)))
Tactic: rw [← hp] at hpbar
Cleared hypotheses: hpbar, hp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (hypothesis)
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
⊢ Epi f
have this : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
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)⟧
⊢ Epi f
have 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
Tactic: have ⟨R, x, y, _, ey, comm⟩ := Quotient.exact this
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
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))
⊢ Epi f
have apply : (x ≫ p.hom) ≫ f = y
Tactic: apply @epi_of_epi_fac _ _ _ _ _ (x ≫ p.hom) f y ey
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
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
⊢ (x ≫ p.hom) ≫ f = y
have rw : y ≫ 𝟙 Q = y
Tactic: rw [Category.assoc, comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (hypothesis)
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
⊢ ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = ⟦b⟧
have hb' : b.hom ≫ S.g = 0
Tactic: have hb' : b.hom ≫ S.g = 0 := (pseudoZero_iff _).1 hb
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
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
⊢ ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = ⟦b⟧
have obtain : ∀ (c : b.left ⟶ (KernelFork.ofι (image.ι S.f) sorry).pt) (hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) sorry) = b.hom),
  ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = ⟦b⟧
Tactic: obtain ⟨c, hc⟩ := KernelFork.IsLimit.lift' hS.isLimitImage _ hb'
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
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
⊢ ∃ (a : Pseudoelement.{v, u} S.X₁), pseudoApply S.f a = ⟦b⟧
have 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⟧
Tactic: use pullback.fst (Abelian.factorThruImage S.f) c
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
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 (α := 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⟧
have 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
Tactic: apply Quotient.sound
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
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
have 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
Tactic: refine ⟨pullback (Abelian.factorThruImage S.f) c, 𝟙 _,
              pullback.snd _ _, inferInstance, inferInstance, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
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)))
have 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)
Tactic: rw [Abelian.image.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
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 ≫
      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))
have 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))
Tactic: rw [← Category.assoc, pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
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))
⊢ 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))
have 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))
Tactic: rw [← Category.assoc, pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
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)
have 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)
Tactic: rw [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
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) ≫
      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
have _ : 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: 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
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)))
⊢ 𝟙 (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
have _₁ : 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: 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
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))
⊢ 𝟙 (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
have _₂ : 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: 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (hypothesis)
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 (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
have 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
Tactic: have : S.g (kernel.ι S.g) = 0 := apply_eq_zero_of_comp_eq_zero _ _ (kernel.condition _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
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
⊢ Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
have 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
Tactic: obtain ⟨a', ha⟩ := hS _ this
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (goal)
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))
⊢ Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
have obtain : ∀ (a : Over.{v, u} S.X₁) (ha' : ⟦a⟧ = a'), Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
Tactic: obtain ⟨a, ha'⟩ := Quotient.exists_rep a'
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Pseudoelements (hypothesis)
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 (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
have 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)))
Tactic: rw [← ha'] at ha
Cleared hypotheses: ha, ha'