-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over.{v, u} X
x_1 : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))) x_1
hx : x.Compatible (R := x_1)
Y₁ Y₂ : Over.{v, u} X
W : Over.{v, u} Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x_1 g₁
hg₂ : x_1 g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over.{v, u} X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
h₁ :
  Eq (α := (fun (X : Type u_1) ↦ X) (F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf (J.over Y)).map f₁.op) :
          (a : (fun (X : Type u_1) ↦ X) (F.obj.obj (Opposite.op ((Over.map f).obj Y₁)))) →
            (fun (X : Type u_1) ↦ X) (F.obj.obj (Opposite.op W)))
        (x g₁ hg₁) :
      (fun (X : Type u_1) ↦ X) (F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf (J.over Y)).map e.inv.op) :
          (a : (fun (X : Type u_1) ↦ X) (F.obj.obj (Opposite.op ((Over.map f).obj W')))) →
            (fun (X : Type u_1) ↦ X) (F.obj.obj (Opposite.op W)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))).map g₁'.op) :
              (a : (fun (X : Type u_1) ↦ X) (((Over.map f).op ⋙ F.obj).obj (Opposite.op Y₁))) →
                (fun (X : Type u_1) ↦ X) (((Over.map f).op ⋙ F.obj).obj (Opposite.op W')))
            (x g₁ hg₁) :
          (fun (X : Type u_1) ↦ X)
            (((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))).obj (Opposite.op W'))) :
      (fun (X : Type u_1) ↦ X) (F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W)))
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf (J.over Y)).map f₁.op) :
          (a : (fun (X : Type u_1) ↦ X) (F.obj.obj (Opposite.op ((Over.map f).obj Y₁)))) →
            (fun (X : Type u_1) ↦ X) (F.obj.obj (Opposite.op W)))
        (x g₁ hg₁) :
      (fun (X : Type u_1) ↦ X) (F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf (J.over Y)).map f₂.op) :
          (a : (fun (X : Type u_1) ↦ X) (F.obj.obj (Opposite.op ((Over.map f).obj Y₂)))) →
            (fun (X : Type u_1) ↦ X) (F.obj.obj (Opposite.op W)))
        (x g₂ hg₂) :
      (fun (X : Type u_1) ↦ X) (F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W)))
have h₂ : Eq (α := (fun (X : Type u_1) ↦ X) (F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf (J.over Y)).map f₂.op) :
        (a : (fun (X : Type u_1) ↦ X) (F.obj.obj (Opposite.op ((Over.map f).obj Y₂)))) →
          (fun (X : Type u_1) ↦ X) (F.obj.obj (Opposite.op W)))
      (x g₂ hg₂) :
    (fun (X : Type u_1) ↦ X) (F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf (J.over Y)).map e.inv.op) :
        (a : (fun (X : Type u_1) ↦ X) (F.obj.obj (Opposite.op ((Over.map f).obj W')))) →
          (fun (X : Type u_1) ↦ X) (F.obj.obj (Opposite.op W)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))).map g₂'.op) :
            (a : (fun (X : Type u_1) ↦ X) (((Over.map f).op ⋙ F.obj).obj (Opposite.op Y₂))) →
              (fun (X : Type u_1) ↦ X) (((Over.map f).op ⋙ F.obj).obj (Opposite.op W')))
          (x g₂ hg₂) :
        (fun (X : Type u_1) ↦ X) (((Over.map f).op ⋙ F.obj (P := Presheaf.IsSheaf (J.over Y))).obj (Opposite.op W'))) :
    (fun (X : Type u_1) ↦ X) (F.obj (P := Presheaf.IsSheaf (J.over Y)).obj (Opposite.op W)))
Tactic: convert!
      congr_arg (F.obj.map e.inv.op)
        (hx g₁' g₂' hg₁ hg₂ (by ext; exact (Over.forget _).congr_map h)) using 1