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)
j : J
x₁ x₂ : c.pt.obj (X.obj j)
h : (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₁ = (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₂
this : IsFiltered J
y₁ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₁
y₂ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₂
hy₁ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₁ = x₁
hy₂ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₂ = x₂
H :
  ∀ (k : K),
    ∃ j_1 f, (ConcreteCategory.hom ((X ⋙ F.obj k).map f)) (↑y₁ k) = (ConcreteCategory.hom ((X ⋙ F.obj k).map f)) (↑y₂ k)
j₁ : K → J := fun k ↦ ⋯.choose
f : (k : K) → j ⟶ j₁ k := fun k ↦ ⋯.choose
hf :
  ∀ (k : K),
    (ConcreteCategory.hom ((F.obj k).map (X.map (f k)))) (↑y₁ k) =
      (ConcreteCategory.hom ((F.obj k).map (X.map (f k)))) (↑y₂ k)
hK' : HasCardinalLT K κ
ψ : K → (j ⟶ IsCardinalFiltered.max j₁ hK') := fun k ↦ f k ≫ IsCardinalFiltered.toMax j₁ hK' k
k : K
⊢ ↑((Types.isLimitEquivSections (hc (X.obj (IsCardinalFiltered.coeq ψ hK'))))
          ((ConcreteCategory.hom (c.pt.map (X.map (IsCardinalFiltered.toCoeq ψ hK')))) x₁))
      k =
    ↑((Types.isLimitEquivSections (hc (X.obj (IsCardinalFiltered.coeq ψ hK'))))
          ((ConcreteCategory.hom (c.pt.map (X.map (IsCardinalFiltered.toCoeq ψ hK')))) x₂))
      k

Tactic:
simp only [Types.isLimitEquivSections_apply, ← hy₁, ← hy₂]

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)
j : J
x₁ x₂ : c.pt.obj (X.obj j)
h : (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₁ = (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₂
this : IsFiltered J
y₁ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₁
y₂ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₂
hy₁ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₁ = x₁
hy₂ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₂ = x₂
H :
  ∀ (k : K),
    ∃ j_1 f, (ConcreteCategory.hom ((X ⋙ F.obj k).map f)) (↑y₁ k) = (ConcreteCategory.hom ((X ⋙ F.obj k).map f)) (↑y₂ k)
j₁ : K → J := fun k ↦ ⋯.choose
f : (k : K) → j ⟶ j₁ k := fun k ↦ ⋯.choose
hf :
  ∀ (k : K),
    (ConcreteCategory.hom ((F.obj k).map (X.map (f k)))) (↑y₁ k) =
      (ConcreteCategory.hom ((F.obj k).map (X.map (f k)))) (↑y₂ k)
hK' : HasCardinalLT K κ
ψ : K → (j ⟶ IsCardinalFiltered.max j₁ hK') := fun k ↦ f k ≫ IsCardinalFiltered.toMax j₁ hK' k
k : K
⊢ (ConcreteCategory.hom ((((evaluation C (Type w')).obj (X.obj (IsCardinalFiltered.coeq ψ hK'))).mapCone c).π.app k))
      ((ConcreteCategory.hom (c.pt.map (X.map (IsCardinalFiltered.toCoeq ψ hK'))))
        ((Types.isLimitEquivSections (hc (X.obj j))).symm y₁)) =
    (ConcreteCategory.hom ((((evaluation C (Type w')).obj (X.obj (IsCardinalFiltered.coeq ψ hK'))).mapCone c).π.app k))
      ((ConcreteCategory.hom (c.pt.map (X.map (IsCardinalFiltered.toCoeq ψ hK'))))
        ((Types.isLimitEquivSections (hc (X.obj j))).symm y₂))