Lean4
/-- Provided that `R` preserves the appropriate limit, then the cone in `coneOfPreserves` is a
limit. -/
noncomputable def coneOfPreservesIsLimit [PreservesLimit (F ⋙ snd L R) R] {c₁ : Cone (F ⋙ fst L R)} (t₁ : IsLimit c₁)
{c₂ : Cone (F ⋙ snd L R)} (t₂ : IsLimit c₂) : IsLimit (coneOfPreserves F c₁ t₂)
where
lift
s :=
{ left := t₁.lift ((fst L R).mapCone s)
right := t₂.lift ((snd L R).mapCone s)
w :=
(isLimitOfPreserves R t₂).hom_ext fun j =>
by
rw [coneOfPreserves_pt_hom, assoc, assoc, (isLimitOfPreserves R t₂).fac, limitAuxiliaryCone_π_app, ←
L.map_comp_assoc, t₁.fac, R.mapCone_π_app, ← R.map_comp, t₂.fac]
exact (s.π.app j).w }
uniq s m
w := by
apply CommaMorphism.ext
· exact t₁.uniq ((fst L R).mapCone s) _ (fun j => by simp [← w])
· exact t₂.uniq ((snd L R).mapCone s) _ (fun j => by simp [← w])
