-- 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))
mp :
  (∃ (j : Φ.fiber.Elementsᵒᵖ) (f : op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x) ⟶ j),
      Eq (α := CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f) :
              (a : CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj (op ⟨X, x⟩))) →
                CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))
            z₁ :
          CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f) :
              (a : CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj (op ⟨X, x⟩))) →
                CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))
            z₂ :
          CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))) →
    ∃ (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)))
mpr :
  (∃ (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)))) →
    ∃ (j : Φ.fiber.Elementsᵒᵖ) (f : op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x) ⟶ j),
      Eq (α := CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f) :
              (a : CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj (op ⟨X, x⟩))) →
                CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))
            z₁ :
          CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f) :
              (a : CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj (op ⟨X, x⟩))) →
                CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))
            z₂ :
          CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))
⊢ (∃ (j : Φ.fiber.Elementsᵒᵖ) (f : op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x) ⟶ j),
      Eq (α := CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f) :
              (a : CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj (op ⟨X, x⟩))) →
                CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))
            z₁ :
          CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (((CategoryOfElements.π Φ.fiber).op ⋙ P).map f) :
              (a : CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj (op ⟨X, x⟩))) →
                CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))
            z₂ :
          CC (((CategoryOfElements.π Φ.fiber).op ⋙ P).obj j))) ↔
    ∃ (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:
constructor