-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F₁_1 F₂_1 F₃ : Sheaf.{v, v', u, u'} J A
φ_1 : F₁_1 ⟶ F₂_1
ψ : F₂_1 ⟶ F₃
inst_4 : HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
F₁ F₂ : Sheaf J (Type w)
φ : F₁ ⟶ F₂
inst_5 : IsLocallySurjective (FA := TypeCat.Fun) φ
Z : Sheaf J (Type w)
f₁ f₂ : F₂ ⟶ Z
h : φ ≫ f₁ = φ ≫ f₂
X : Cᵒᵖ
x : F₂.obj (P := Presheaf.IsSheaf J).obj X
Y : C
f : Y ⟶ unop X
s : F₁.obj (P := Presheaf.IsSheaf J).obj (op Y)
hs :
  Eq (α := (fun (X : Type w) ↦ X) (F₂.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.hom.app (op Y)) :
          (a : (fun (X : Type w) ↦ X) (F₁.obj.obj (op Y))) → (fun (X : Type w) ↦ X) (F₂.obj.obj (op Y)))
        s :
      (fun (X : Type w) ↦ X) (F₂.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F₂.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : (fun (X : Type w) ↦ X) (F₂.obj.obj (op (unop X)))) → (fun (X : Type w) ↦ X) (F₂.obj.obj (op Y)))
        x :
      (fun (X : Type w) ↦ X) (F₂.obj (P := Presheaf.IsSheaf J).obj (op Y)))
h₁ :
  Eq (α := Z.obj (P := Presheaf.IsSheaf J).obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F₂.obj (P := Presheaf.IsSheaf J).map f.op ≫ f₁.hom.app (op Y)) :
          (a : F₂.obj.obj (op (unop X))) → Z.obj.obj (op Y))
        x :
      Z.obj (P := Presheaf.IsSheaf J).obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f₁.hom.app (op (unop X)) ≫ Z.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : F₂.obj.obj (op (unop X))) → Z.obj.obj (op Y))
        x :
      Z.obj (P := Presheaf.IsSheaf J).obj (op Y))
⊢ Eq (α := Z.obj (P := Presheaf.IsSheaf J).obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Z.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : Z.obj.obj X) → Z.obj.obj (op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f₁.hom.app X) : (a : F₂.obj.obj X) → Z.obj.obj X) x :
          Z.obj (P := Presheaf.IsSheaf J).obj X) :
      Z.obj (P := Presheaf.IsSheaf J).obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Z.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : Z.obj.obj X) → Z.obj.obj (op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f₂.hom.app X) : (a : F₂.obj.obj X) → Z.obj.obj X) x :
          Z.obj (P := Presheaf.IsSheaf J).obj X) :
      Z.obj (P := Presheaf.IsSheaf J).obj (op Y))
have h₂ : Eq (α := Z.obj (P := Presheaf.IsSheaf J).obj (op Y))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F₂.obj (P := Presheaf.IsSheaf J).map f.op ≫ f₂.hom.app (op Y)) :
        (a : F₂.obj.obj (op (unop X))) → Z.obj.obj (op Y))
      x :
    Z.obj (P := Presheaf.IsSheaf J).obj (op Y))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f₂.hom.app (op (unop X)) ≫ Z.obj (P := Presheaf.IsSheaf J).map f.op) :
        (a : F₂.obj.obj (op (unop X))) → Z.obj.obj (op Y))
      x :
    Z.obj (P := Presheaf.IsSheaf J).obj (op Y))
Tactic: have h₂ := ConcreteCategory.congr_hom (f₂.hom.naturality f.op) x