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

Tactic:
simp [reassoc_of% this, Presieve.extend_agrees hg.familyOfElements_compatible (.mk i)]

Premises used: CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Presieve.extend_agrees, CategoryTheory.Presieve.Arrows.Compatible.familyOfElements_compatible