-- Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
inst_1 : J.Subcanonical
X : C
E Z : Over.{v_1, u_1} X
ι : Type (max u_1 v_1)
T : ι → Over.{v_1, u_1} X
g : (i : ι) → T i ⟶ Z
hR :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} Z.left)) ((J : (a : C) → Set (Sieve a)) Z.left)
    (Sieve.generate
      (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
        Functor.map (Over.forget X) (g i)))
t : Presieve.FamilyOfElements (Functor.obj CategoryTheory.yoneda E) (Sieve.ofArrows T g).arrows
ht : t.Compatible (R := (Sieve.ofArrows T g).arrows)
hg : Presieve.Arrows.Compatible (Functor.obj CategoryTheory.yoneda E.left) (B := Z.left) (X := fun (i : ι) ↦ (T i).left)
  (fun (i : ι) ↦ Over.Hom.left (g i)) fun (i : ι) ↦ Over.Hom.left (t (g i) ⋯) :=
  ⋯
a : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)
ha :
  hg.familyOfElements.sieveExtend (R :=
        Presieve.ofArrows (fun (i : ι) ↦ (T i).left) fun (i : ι) ↦ Over.Hom.left (g i)).IsAmalgamation
    (R :=
    Sieve.arrows
      (Sieve.generate
        (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
          Functor.map (Over.forget X) (g i))))
    a
huniq :
  ∀ (y : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)),
    (fun (t_1 : Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left)) ↦
          hg.familyOfElements.sieveExtend (R :=
                Presieve.ofArrows (fun (i : ι) ↦ (T i).left) fun (i : ι) ↦ Over.Hom.left (g i)).IsAmalgamation
            (R :=
            Sieve.arrows
              (Sieve.generate
                (Presieve.ofArrows (fun (i : ι) ↦ Functor.obj (Over.forget X) (T i)) fun (i : ι) ↦
                  Functor.map (Over.forget X) (g i))))
            t_1)
        y →
      y = a
refine_1 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ Z.left⦄,
    Sieve.arrows (Sieve.ofArrows (fun (i : ι) ↦ (T i).left) fun (i : ι) ↦ Over.Hom.left (g i)) f →
      Eq (α := (fun (X : Type v_1) ↦ X) (Functor.obj (Functor.obj CategoryTheory.yoneda X) (Opposite.op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj CategoryTheory.yoneda X) f.op) :
              (a : (fun (X : Type v_1) ↦ X) ((CategoryTheory.yoneda.obj X).obj (Opposite.op Z.left))) →
                (fun (X : Type v_1) ↦ X) ((CategoryTheory.yoneda.obj X).obj (Opposite.op Y)))
            (a ≫ E.hom) :
          (fun (X : Type v_1) ↦ X) (Functor.obj (Functor.obj CategoryTheory.yoneda X) (Opposite.op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj CategoryTheory.yoneda X) f.op) :
              (a : (fun (X : Type v_1) ↦ X) ((CategoryTheory.yoneda.obj X).obj (Opposite.op Z.left))) →
                (fun (X : Type v_1) ↦ X) ((CategoryTheory.yoneda.obj X).obj (Opposite.op Y)))
            (Opposite.unop (Opposite.op Z)).hom :
          (fun (X : Type v_1) ↦ X) (Functor.obj (Functor.obj CategoryTheory.yoneda X) (Opposite.op Y)))
⊢ a ≫ E.hom = (Opposite.unop (Opposite.op Z)).hom

Tactic:
refine (Subcanonical.isSheaf_of_isRepresentable <| CategoryTheory.yoneda.obj X)
      (.ofArrows _ <| fun i ↦ (g i).left) hR |>.isSeparatedFor.ext ?_

Premises used: CategoryTheory.Over.Hom.left, CategoryTheory.yoneda, CategoryTheory.Sieve.ofArrows, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable, CategoryTheory.Functor.obj