-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Basic (hypothesis)
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 Q : 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
f : P ⟶ Q
inst_7 : Presheaf.IsLocallyInjective (FD := FC) (CD := CC) J f
this :
  ∀ (X : C) (x : Φ.fiber.obj X) (p₁ p₂ : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (P.obj (op X)))
    (hp :
      Eq (α := CC (Q.obj (op X)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op X)) : (a : CC (P.obj (op X))) → CC (Q.obj (op X))) p₁ :
          CC (Q.obj (op X)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op X)) : (a : CC (P.obj (op X))) → CC (Q.obj (op X))) p₂ :
          CC (Q.obj (op X)))),
    Eq (α := CC (Functor.obj Φ.presheafFiber P))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber X x P) :
            (a : CC (P.obj (op X))) → CC (Φ.presheafFiber.obj P))
          p₁ :
        CC (Functor.obj Φ.presheafFiber P))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber X x P) :
            (a : CC (P.obj (op X))) → CC (Φ.presheafFiber.obj P))
          p₂ :
        CC (Functor.obj Φ.presheafFiber P))
X : C
x : Φ.fiber.obj X
p₁ p₂ : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (P.obj (op X))
h :
  Eq (α := CC (Functor.obj Φ.presheafFiber Q))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (Functor.map Φ.presheafFiber f) :
          (a : CC (Φ.presheafFiber.obj P)) → CC (Φ.presheafFiber.obj Q))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber X x P) :
              (a : CC (P.obj (op X))) → CC (Φ.presheafFiber.obj P))
            p₁ :
          CC (Functor.obj Φ.presheafFiber P)) :
      CC (Functor.obj Φ.presheafFiber Q))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (Functor.map Φ.presheafFiber f) :
          (a : CC (Φ.presheafFiber.obj P)) → CC (Φ.presheafFiber.obj Q))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber X x P) :
              (a : CC (P.obj (op X))) → CC (Φ.presheafFiber.obj P))
            p₂ :
          CC (Functor.obj Φ.presheafFiber P)) :
      CC (Functor.obj Φ.presheafFiber Q))
⊢ Eq (α := CC (Functor.obj Φ.presheafFiber P))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber X x P) :
          (a : CC (P.obj (op X))) → CC (Φ.presheafFiber.obj P))
        p₁ :
      CC (Functor.obj Φ.presheafFiber P))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber X x P) :
          (a : CC (P.obj (op X))) → CC (Φ.presheafFiber.obj P))
        p₂ :
      CC (Functor.obj Φ.presheafFiber P))
have h₁ : ∃ (Y : C) (f_1 : Y ⟶ X) (y : Φ.fiber.obj Y),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f_1) : (a : Φ.fiber.obj Y) → Φ.fiber.obj X) y = x ∧
    Eq (α := CC (Q.obj (op Y)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (Q.map f_1.op) : (a : CC (Q.obj (op X))) → CC (Q.obj (op Y)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op X)) : (a : CC (P.obj (op X))) → CC (Q.obj (op X)))
              p₁ :
            CC (Q.obj (op X))) :
        CC (Q.obj (op Y)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (Q.map f_1.op) : (a : CC (Q.obj (op X))) → CC (Q.obj (op Y)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op X)) : (a : CC (P.obj (op X))) → CC (Q.obj (op X)))
              p₂ :
            CC (Q.obj (op X))) :
        CC (Q.obj (op Y)))
Tactic: simp only [toPresheafFiber_naturality_apply, toPresheafFiber_eq_iff'] at h
Cleared hypotheses: h