-- Module: Mathlib.CategoryTheory.Sites.LocallyBijective
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ :
  ∀ (X : Cᵒᵖ),
    Function.Injective (α := F.obj (P := Presheaf.IsSheaf J).obj X) (β := G.obj (P := Presheaf.IsSheaf J).obj X)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app X)) : (a : F.obj.obj X) → G.obj.obj X)
right : IsLocallySurjective (FA := TypeCat.Fun) f
X : Cᵒᵖ
s : G.obj (P := Presheaf.IsSheaf J).obj X
H : Presieve.IsSheafFor (F.obj (P := Presheaf.IsSheaf J)) (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows
t : Presieve.FamilyOfElements (F.obj (P := Presheaf.IsSheaf J))
  (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows :=
  fun (Y : C) (g : Y ⟶ Opposite.unop X) (hg : (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows g) ↦
    Presheaf.localPreimage (FA := TypeCat.Fun) f.hom s g hg
Y₁ Y₂ W : C
g₁ : W ⟶ Y₁
g₂ : W ⟶ Y₂
f₁ : Y₁ ⟶ Opposite.unop X
f₂ : Y₂ ⟶ Opposite.unop X
hf₁ : (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows f₁
hf₂ : (Presheaf.imageSieve (FA := TypeCat.Fun) f.hom s).arrows f₂
w : g₁ ≫ f₁ = g₂ ≫ f₂
eq₁ :
  Eq (α := G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op W)) :
          (a : F.obj.obj (Opposite.op W)) → G.obj.obj (Opposite.op W))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map g₁.op) :
              (a : F.obj.obj (Opposite.op Y₁)) → F.obj.obj (Opposite.op W))
            (t f₁ hf₁) :
          F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W)) :
      G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.obj (P := Presheaf.IsSheaf J).map g₁.op) :
          (a : G.obj.obj (Opposite.op Y₁)) → G.obj.obj (Opposite.op W))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op Y₁)) :
              (a : F.obj.obj (Opposite.op Y₁)) → G.obj.obj (Opposite.op Y₁))
            (t f₁ hf₁) :
          G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y₁)) :
      G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W))
eq₂ :
  Eq (α := G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op W)) :
          (a : F.obj.obj (Opposite.op W)) → G.obj.obj (Opposite.op W))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map g₂.op) :
              (a : F.obj.obj (Opposite.op Y₂)) → F.obj.obj (Opposite.op W))
            (t f₂ hf₂) :
          F.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W)) :
      G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.obj (P := Presheaf.IsSheaf J).map g₂.op) :
          (a : G.obj.obj (Opposite.op Y₂)) → G.obj.obj (Opposite.op W))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op Y₂)) :
              (a : F.obj.obj (Opposite.op Y₂)) → G.obj.obj (Opposite.op Y₂))
            (t f₂ hf₂) :
          G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y₂)) :
      G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W))
⊢ Eq (α := (fun (X : Type w) ↦ X) (G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.obj (P := Presheaf.IsSheaf J).map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (G.obj.obj (Opposite.op Y₁))) →
            (fun (X : Type w) ↦ X) (G.obj.obj (Opposite.op W)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op Y₁)) :
              (a : F.obj.obj (Opposite.op Y₁)) → G.obj.obj (Opposite.op Y₁))
            (Presheaf.localPreimage (FA := TypeCat.Fun) f.hom s f₁ hf₁) :
          G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y₁)) :
      (fun (X : Type w) ↦ X) (G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.obj (P := Presheaf.IsSheaf J).map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (G.obj.obj (Opposite.op Y₁))) →
            (fun (X : Type w) ↦ X) (G.obj.obj (Opposite.op W)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.obj (P := Presheaf.IsSheaf J).map f₁.op) :
              (a : G.obj.obj (Opposite.op (Opposite.unop X))) → G.obj.obj (Opposite.op Y₁))
            s :
          G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op Y₁)) :
      (fun (X : Type w) ↦ X) (G.obj (P := Presheaf.IsSheaf J).obj (Opposite.op W)))

Tactic:
have eq₃ := congr_arg (G.obj.map g₁.op) (Presheaf.app_localPreimage f.hom s _ hf₁)