Module: Mathlib.Topology.Sheaves.Alexandrov

Goal state before:
pp: X✝ : Type v
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : Preorder X✝
inst✝⁴ : Topology.IsUpperSet X✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
F✝ : X✝ ⥤ C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
α : Type v
Us : α → Opens ↑X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
m : S.pt ⟶ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).pt
hm :
  ∀ (j : (ObjectProperty.FullSubcategory fun V ↦ ∃ i, V ≤ Us i)ᵒᵖ),
    m ≫ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).π.app j = S.π.app j
left✝ : Discrete PUnit.{1}
x : ↑X
f : (fromPUnit (Opposite.op (iSup Us))).obj left✝ ⟶ (principals ↑X).obj x
⊢ ∃ i, principalOpen x ≤ Us i

pp: X✝ : Type v
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : Preorder X✝
inst✝⁴ : Topology.IsUpperSet X✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
F✝ : X✝ ⥤ C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
α : Type v
Us : α → Opens ↑X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
m : S.pt ⟶ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).pt
hm✝ :
  ∀ (j : (ObjectProperty.FullSubcategory fun V ↦ ∃ i, V ≤ Us i)ᵒᵖ),
    m ≫ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).π.app j = S.π.app j
left✝ : Discrete PUnit.{1}
x : ↑X
f : (fromPUnit (Opposite.op (iSup Us))).obj left✝ ⟶ (principals ↑X).obj x
hm :
  m ≫
      ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).π.app
        (Opposite.op { obj := principalOpen x, property := ?m.255 }) =
    S.π.app (Opposite.op { obj := principalOpen x, property := ?m.255 })
⊢ S.π.app
        (Opposite.op
          { obj := principalOpen (StructuredArrow.right { left := left✝, right := x, hom := f }), property := ⋯ }) ≫
      limit.π (generator (principalOpen (StructuredArrow.right { left := left✝, right := x, hom := f })) ⋙ F)
        { left := { as := PUnit.unit }, right := StructuredArrow.right { left := left✝, right := x, hom := f },
          hom := 𝟙 (Opposite.op (principalOpen (StructuredArrow.right { left := left✝, right := x, hom := f }))) } =
    m ≫ limit.π (generator (iSup Us) ⋙ F) { left := left✝, right := x, hom := f }

Tactic:
· apply exists_le_of_le_sup
      exact f.unop.le

Goal state after:
X✝ : Type v
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : Preorder X✝
inst✝⁴ : Topology.IsUpperSet X✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
F✝ : X✝ ⥤ C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
α : Type v
Us : α → Opens ↑X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
m : S.pt ⟶ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).pt
hm✝ :
  ∀ (j : (ObjectProperty.FullSubcategory fun V ↦ ∃ i, V ≤ Us i)ᵒᵖ),
    m ≫ ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).π.app j = S.π.app j
left✝ : Discrete PUnit.{1}
x : ↑X
f : (fromPUnit (Opposite.op (iSup Us))).obj left✝ ⟶ (principals ↑X).obj x
hm :
  m ≫
      ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op).π.app
        (Opposite.op { obj := principalOpen x, property := ⋯ }) =
    S.π.app (Opposite.op { obj := principalOpen x, property := ⋯ })
⊢ S.π.app
        (Opposite.op
          { obj := principalOpen (StructuredArrow.right { left := left✝, right := x, hom := f }), property := ⋯ }) ≫
      limit.π (generator (principalOpen (StructuredArrow.right { left := left✝, right := x, hom := f })) ⋙ F)
        { left := { as := PUnit.unit }, right := StructuredArrow.right { left := left✝, right := x, hom := f },
          hom := 𝟙 (Opposite.op (principalOpen (StructuredArrow.right { left := left✝, right := x, hom := f }))) } =
    m ≫ limit.π (generator (iSup Us) ⋙ F) { left := left✝, right := x, hom := f }