-- Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
theorem pseudo_exact_of_exact {S : ShortComplex C} (hS : S.Exact) :
    ∀ b, S.g b = 0 → ∃ a, S.f a = b :=
  fun b' =>
    Quotient.inductionOn b' fun b hb => by
      have hb' : b.hom ≫ S.g = 0 := (pseudoZero_iff _).1 hb
      -- By exactness, `b` factors through `im f = ker g` via some `c`.
      obtain ⟨c, hc⟩ := KernelFork.IsLimit.lift' hS.isLimitImage _ hb'
      -- We compute the pullback of the map into the image and `c`.
      -- The pseudoelement induced by the first pullback map will be our preimage.
      use pullback.fst (Abelian.factorThruImage S.f) c
      -- It remains to show that the image of this element under `f` is pseudo-equal to `b`.
      apply Quotient.sound
      refine ⟨pullback (Abelian.factorThruImage S.f) c, 𝟙 _,
              pullback.snd _ _, inferInstance, inferInstance, ?_⟩
      -- Now we can verify that the diagram commutes.
      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)

Proof state:
case h.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ (fun g => app S.f g) (Over.mk (pullback.fst (Abelian.factorThruImage S.f) c)) ≈ b

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

Result:
case h.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ 𝟙 (pullback (Abelian.factorThruImage S.f) c) ≫
      ((fun g => app S.f g) (Over.mk (pullback.fst (Abelian.factorThruImage S.f) c))).hom =
    pullback.snd (Abelian.factorThruImage S.f) c ≫ b.hom

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ pseudoApply S.f (Quot.mk (PseudoEqual S.X₁) (Over.mk (pullback.fst (Abelian.factorThruImage S.f) c))) = ⟦b⟧

Tactic:
apply Quotient.sound

Result:
case h.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ (fun g => app S.f g) (Over.mk (pullback.fst (Abelian.factorThruImage S.f) c)) ≈ b

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
⊢ ∃ a, pseudoApply S.f a = ⟦b⟧

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

Result:
case mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ ∃ a, pseudoApply S.f a = ⟦b⟧

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ (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]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ pullback.snd (Abelian.factorThruImage S.f) c ≫ c ≫ kernel.ι (cokernel.π S.f) =
    pullback.snd (Abelian.factorThruImage S.f) c ≫ b.hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ 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]

Result:
no goals

Proof state:
case h.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ 𝟙 (pullback (Abelian.factorThruImage S.f) c) ≫
      ((fun g => app S.f g) (Over.mk (pullback.fst (Abelian.factorThruImage S.f) c))).hom =
    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

Result:
no goals

Proof state:
case mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ ∃ a, pseudoApply S.f a = ⟦b⟧

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

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ pseudoApply S.f (Quot.mk (PseudoEqual S.X₁) (Over.mk (pullback.fst (Abelian.factorThruImage S.f) c))) = ⟦b⟧

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
⊢ ∃ a, pseudoApply S.f a = ⟦b⟧

Tactic:
have hb' : b.hom ≫ S.g = 0 := (pseudoZero_iff _).1 hb

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
⊢ ∃ a, pseudoApply S.f a = ⟦b⟧

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ pullback.fst (Abelian.factorThruImage S.f) c ≫ S.f =
    pullback.fst (Abelian.factorThruImage S.f) c ≫ Abelian.factorThruImage S.f ≫ kernel.ι (cokernel.π S.f)

Tactic:
rw [Abelian.image.fac]

Result:
no goals