Module: Mathlib.CategoryTheory.Presentable.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
H :
  ∀ {k k' : K} (φ : k ⟶ k'),
    ∃ j f,
      (ConcreteCategory.hom ((X ⋙ F.obj k').map f)) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
        (ConcreteCategory.hom ((X ⋙ F.obj k').map f)) (z k')
j : {k k' : K} → (k ⟶ k') → J := fun {k k'} φ ↦ ⋯.choose
g : {k k' : K} → (φ : k ⟶ k') → j₀ ⟶ j φ := fun {k k'} φ ↦ ⋯.choose
hg :
  ∀ {k k' : K} (φ : k ⟶ k'),
    (ConcreteCategory.hom ((F.obj k').map (X.map (g φ)))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
      (ConcreteCategory.hom ((F.obj k').map (X.map (g φ)))) (z k')
⊢ ∃ j₁ α,
    ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
      (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
        (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')

Tactic:
obtain ⟨j₁, α, β, hα⟩ : ∃ (j₁ : J) (α : j₀ ⟶ j₁)
        (β : ∀ ⦃k k' : K⦄ (φ : k ⟶ k'), j φ ⟶ j₁),
        ∀ ⦃k k' : K⦄ (φ : k ⟶ k'), α = g φ ≫ β φ := by
      let j'' (f : Arrow K) : J := j f.hom
      let ψ (f : Arrow K) : j₀ ⟶ IsCardinalFiltered.max j'' hK :=
        g f.hom ≫ IsCardinalFiltered.toMax j'' hK f
      refine ⟨IsCardinalFiltered.coeq ψ hK, IsCardinalFiltered.toCoeq ψ hK,
        fun k k' φ ↦ IsCardinalFiltered.toMax j'' hK φ ≫ IsCardinalFiltered.coeqHom ψ hK,
        fun k k' φ ↦ ?_⟩
      simpa [ψ] using! (IsCardinalFiltered.coeq_condition ψ hK (Arrow.mk φ)).symm

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
H :
  ∀ {k k' : K} (φ : k ⟶ k'),
    ∃ j f,
      (ConcreteCategory.hom ((X ⋙ F.obj k').map f)) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
        (ConcreteCategory.hom ((X ⋙ F.obj k').map f)) (z k')
j : {k k' : K} → (k ⟶ k') → J := fun {k k'} φ ↦ ⋯.choose
g : {k k' : K} → (φ : k ⟶ k') → j₀ ⟶ j φ := fun {k k'} φ ↦ ⋯.choose
hg :
  ∀ {k k' : K} (φ : k ⟶ k'),
    (ConcreteCategory.hom ((F.obj k').map (X.map (g φ)))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
      (ConcreteCategory.hom ((F.obj k').map (X.map (g φ)))) (z k')
j₁ : J
α : j₀ ⟶ j₁
β : ⦃k k' : K⦄ → (φ : k ⟶ k') → j φ ⟶ j₁
hα : ∀ ⦃k k' : K⦄ (φ : k ⟶ k'), α = g φ ≫ β φ
⊢ ∃ j₁ α,
    ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
      (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
        (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')