unitEqualises — Mathlib

Lean4
/-- To show that `η_X` is an equalizer for `(UFη_X, η_UFX)`, it suffices to assume it's always an
equalizer of something (i.e. a regular mono).
-/
def unitEqualises [∀ X : B, RegularMono (adj₁.unit.app X)] (X : B) :
    IsLimit (Fork.ofι (adj₁.unit.app X) (adj₁.unit_naturality _)) :=
  Fork.IsLimit.mk' _ fun s =>
    by
    refine ⟨(RegularMono.lift' (adj₁.unit.app X) s.ι ?_).1, ?_, ?_⟩
    · rw [← cancel_mono (adj₁.unit.app (RegularMono.Z (adj₁.unit.app X)))]
      rw [assoc, ← adj₁.unit_naturality RegularMono.left]
      dsimp only [Functor.comp_obj]
      erw [← assoc, ← s.condition, assoc, ← U.map_comp, ← F.map_comp, RegularMono.w, F.map_comp, U.map_comp,
        s.condition_assoc, assoc, ← adj₁.unit_naturality RegularMono.right]
      rfl
    · apply (RegularMono.lift' (adj₁.unit.app X) s.ι _).2
    · intro m hm
      rw [← cancel_mono (adj₁.unit.app X)]
      apply hm.trans (RegularMono.lift' (adj₁.unit.app X) s.ι _).2.symm
Похожие утверждения