lift — Mathlib

Lean4
/-- Auxiliary definition for `Enriched.FunctorCategory.isLimitConeFunctorEnrichedHom`. -/
noncomputable def lift : s.pt ⟶ enrichedHom V F₁ F₂ :=
  end_.lift (fun j ↦ s.π.app j ≫ enrichedHomπ V _ _ (Under.mk (𝟙 j)))
    (fun j j' f ↦ by
      dsimp
      rw [← s.w f, assoc, assoc, assoc]
        -- this was produced by `simp?`

      simp only [functorEnrichedHom_obj, functorEnrichedHom_map, end_.lift_π_assoc, diagram_obj_obj, Functor.comp_obj,
        Under.forget_obj, Under.mk_right, Under.map_obj_right, Iso.refl_inv, NatTrans.id_app, eHomWhiskerRight_id,
        Iso.refl_hom, eHomWhiskerLeft_id, comp_id]
      have :=
        enrichedHom_condition V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)
          (Under.homMk f : Under.mk (𝟙 j) ⟶ Under.mk f)
      dsimp at this
      rw [this]
      congr 3
      simp [Under.map, Comma.mapLeft]
      rfl)
Похожие утверждения