Module: Mathlib.CategoryTheory.Sites.Point.Over

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
inst✝⁴ : LocallySmall.{w, v, u} C
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y✝ : C
f : Y✝ ⟶ X
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y g_1,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm (Sieve.ofArrows Z g)).arrows g_1),
        ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g_1)) y = x
Φ : P.FullSubcategory
y : Φ.obj.fiber.obj (Over.mk f).left
T : Over X
a : T ⟶ Over.mk f
Y : C
i : ι
b : (Over.forget X).obj T ⟶ Z i
hb : b ≫ g i = (Over.forget X).map a
z : (Over.forget X ⋙ ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.fiber).obj T
hz₁ :
  z ∈
    (FunctorToTypes.fromOverSubfunctor ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.fiber
          ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.snd).obj
      T
hz₂ :
  (ConcreteCategory.hom
        ({
                  obj :=
                    ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.over
                      ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.snd,
                  property := ⋯ }.obj.fiber.map
          a))
      ⟨z, hz₁⟩ =
    ⟨y, ⋯⟩
⊢ ∃ i y_1, (ConcreteCategory.hom (Φ.obj.fiber.map (g i))) y_1 = y

Tactic:
rw [Subtype.ext_iff] at hz₂

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
inst✝⁴ : LocallySmall.{w, v, u} C
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y✝ : C
f : Y✝ ⟶ X
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y g_1,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm (Sieve.ofArrows Z g)).arrows g_1),
        ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g_1)) y = x
Φ : P.FullSubcategory
y : Φ.obj.fiber.obj (Over.mk f).left
T : Over X
a : T ⟶ Over.mk f
Y : C
i : ι
b : (Over.forget X).obj T ⟶ Z i
hb : b ≫ g i = (Over.forget X).map a
z : (Over.forget X ⋙ ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.fiber).obj T
hz₁ :
  z ∈
    (FunctorToTypes.fromOverSubfunctor ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.fiber
          ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.snd).obj
      T
hz₂ :
  ↑((ConcreteCategory.hom
          ({
                    obj :=
                      ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.over
                        ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.snd,
                    property := ⋯ }.obj.fiber.map
            a))
        ⟨z, hz₁⟩) =
    ↑⟨y, ⋯⟩
⊢ ∃ i y_1, (ConcreteCategory.hom (Φ.obj.fiber.map (g i))) y_1 = y