-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst_3 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FC X Y) (CC X) (CC Y)
inst_4 : ConcreteCategory.{w', v', u', u_1} A FC (CC := CC)
P : Functor.{v, v', u, u'} Cᵒᵖ A
inst_5 : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A (FC := FC) (CC := CC))
inst_6 : LocallySmall.{w, v, u} C
X : C
x : Φ.fiber.obj X
z₁ z₂ : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (P.obj (op X))
Y : C
y : Φ.fiber.obj Y
f :
  (unop (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) Y y))).fst (β := fun (c : C) ↦ Φ.fiber.obj c) ⟶
    (unop (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x))).fst (β := fun (c : C) ↦ Φ.fiber.obj c)
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
        (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj (unop (op ⟨Y, y⟩)).fst)) →
          (fun (X : Type w) ↦ X) (Φ.fiber.obj (unop (op ⟨X, x⟩)).fst))
      ((unop (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) Y y))).snd (β := fun (c : C) ↦ Φ.fiber.obj c)) =
    (unop (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x))).snd (β := fun (c : C) ↦ Φ.fiber.obj c)
hf' :
  Eq (α := CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) Y y))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (((CategoryOfElements.π Φ.fiber).op ⋙ P).map
              (op
                (Subtype.mk (p :=
                  fun
                    (f :
                      (unop (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) Y y))).fst (β := fun (c : C) ↦
                          Φ.fiber.obj c) ⟶
                        (unop (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x))).fst (β := fun (c : C) ↦
                          Φ.fiber.obj c)) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
                        (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj (unop (op ⟨Y, y⟩)).fst)) →
                          (fun (X : Type w) ↦ X) (Φ.fiber.obj (unop (op ⟨X, x⟩)).fst))
                      ((unop (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) Y y))).snd (β := fun (c : C) ↦
                        Φ.fiber.obj c)) =
                    (unop (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x))).snd (β := fun (c : C) ↦
                      Φ.fiber.obj c))
                  f hf))) :
          (a : CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj (op ⟨X, x⟩))) →
            CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj (op ⟨Y, y⟩)))
        z₁ :
      CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) Y y))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (((CategoryOfElements.π Φ.fiber).op ⋙ P).map
              (op
                (Subtype.mk (p :=
                  fun
                    (f :
                      (unop (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) Y y))).fst (β := fun (c : C) ↦
                          Φ.fiber.obj c) ⟶
                        (unop (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x))).fst (β := fun (c : C) ↦
                          Φ.fiber.obj c)) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
                        (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj (unop (op ⟨Y, y⟩)).fst)) →
                          (fun (X : Type w) ↦ X) (Φ.fiber.obj (unop (op ⟨X, x⟩)).fst))
                      ((unop (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) Y y))).snd (β := fun (c : C) ↦
                        Φ.fiber.obj c)) =
                    (unop (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x))).snd (β := fun (c : C) ↦
                      Φ.fiber.obj c))
                  f hf))) :
          (a : CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj (op ⟨X, x⟩))) →
            CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj (op ⟨Y, y⟩)))
        z₂ :
      CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) Y y))))
⊢ ∃ (Y : C) (f : Y ⟶ X) (y : Φ.fiber.obj Y),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
            (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj X))
          y =
        x ∧
      Eq (α := CC (P.obj (op Y)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (P.map f.op) : (a : CC (P.obj (op X))) → CC (P.obj (op Y))) z₁ :
          CC (P.obj (op Y)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (P.map f.op) : (a : CC (P.obj (op X))) → CC (P.obj (op Y))) z₂ :
          CC (P.obj (op Y)))

Tactic:
⟨Y, f, y, hf, hf'⟩

Premises used: And.intro, Exists.intro