-- 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
y : Functor.obj (Functor.obj CategoryTheory.yoneda E) (Opposite.op Z)
hty :
  (fun (t_1 : Functor.obj (Functor.obj CategoryTheory.yoneda E) (Opposite.op Z)) ↦
      t.IsAmalgamation (R := (Sieve.ofArrows T g).arrows) t_1)
    y
W Y : C
i : ι
v : W ⟶ Functor.obj (Over.forget X) (T i)
this : Over.Hom.left (g i) ≫ Over.Hom.left y = Over.Hom.left (t (g i) ⋯)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Functor.map (Functor.obj CategoryTheory.yoneda E.left) (v ≫ Functor.map (Over.forget X) (g i)).op) :
        (a : (fun (X : Type v_1) ↦ X) ((CategoryTheory.yoneda.obj E.left).obj (Opposite.op Z.left))) →
          (fun (X : Type v_1) ↦ X) ((CategoryTheory.yoneda.obj E.left).obj (Opposite.op W)))
      (Over.Hom.left y) =
    hg.familyOfElements.sieveExtend (R :=
      Presieve.ofArrows (fun (i : ι) ↦ (T i).left) fun (i : ι) ↦ Over.Hom.left (g i))
      (v ≫ Functor.map (Over.forget X) (g i)) ⋯

Tactic:
simp [Presieve.FamilyOfElements.comp_of_compatible _
      hg.familyOfElements_compatible.sieveExtend (Sieve.ofArrows_mk _ _ i),
      Presieve.extend_agrees hg.familyOfElements_compatible (.mk i), this]

Premises used: CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Sieve.ofArrows_mk, CategoryTheory.Presieve.extend_agrees, CategoryTheory.Presieve.Arrows.Compatible.familyOfElements_compatible, CategoryTheory.Presieve.FamilyOfElements.comp_of_compatible, CategoryTheory.Presieve.FamilyOfElements.Compatible.sieveExtend