conesEquivInverse — Mathlib

Lean4
/-- (Impl) A preliminary definition to avoid timeouts. -/
@[simps]
def conesEquivInverse (B : C) {J : Type w} (F : Discrete J ⥤ Over B) :
    Cone F ⥤ Cone (widePullbackDiagramOfDiagramOver B F)
    where
  obj := conesEquivInverseObj B F
  map
    f :=
    { hom := f.hom.left
      w := fun j => by
        obtain - | j := j
        · simp
        · dsimp
          rw [← f.w ⟨j⟩]
          rfl }
      -- Porting note: this should help with the additional `naturality` proof we now have to give in
      -- `conesEquivFunctor`, but doesn't.
      -- attribute [local aesop safe cases (rule_sets := [CategoryTheory])] Discrete
Похожие утверждения