openCoverOfBase' — Mathlib

Lean4
/-- (Implementation). Use `openCoverOfBase` instead. -/
@[simps! f]
def openCoverOfBase' (𝒰 : OpenCover Z) (f : X ⟶ Z) (g : Y ⟶ Z) : OpenCover (pullback f g) :=
  by
  apply (openCoverOfLeft (𝒰.pullback₁ f) f g).bind
  intro i
  haveI :=
    ((IsPullback.of_hasPullback (pullback.snd g (𝒰.f i)) (pullback.snd f (𝒰.f i))).paste_horiz
        (IsPullback.of_hasPullback _ _)).flip
  refine
    @coverOfIsIso _ _ _ _ _ (f :=
      (pullbackSymmetry (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i))).hom ≫
        (limit.isoLimitCone ⟨_, this.isLimit⟩).inv ≫ pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) ?_ ?_)
      inferInstance
  · simp [← pullback.condition]
  · simp only [Category.comp_id, Category.id_comp]
Похожие утверждения