constructLeftAdjoint — Mathlib

Lean4
/-- Construct the left adjoint to `R`, with object map `constructLeftAdjointObj`. -/
noncomputable def constructLeftAdjoint [∀ X : B, RegularEpi (adj₁.counit.app X)] : B ⥤ A :=
  by
  refine Adjunction.leftAdjointOfEquiv (fun X Y => constructLeftAdjointEquiv R _ adj₁ adj₂ Y X) ?_
  intro X Y Y' g h
  rw [constructLeftAdjointEquiv_apply, constructLeftAdjointEquiv_apply, Equiv.symm_apply_eq, Subtype.ext_iff]
  dsimp
    -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644

  erw [Cofork.IsColimit.homIso_natural, Cofork.IsColimit.homIso_natural]
  erw [adj₂.homEquiv_naturality_right]
  simp_rw [Functor.comp_map]
    -- This used to be `simp`, but we need `cat_disch` after https://github.com/leanprover/lean4/pull/2644

  cat_disch
Похожие утверждения