-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SubcanonicalOver (hypothesis)
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
⊢ 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)))
have this : ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          (Functor.map (Functor.obj CategoryTheory.yoneda E.left) (Quiver.Hom.op (Functor.map (Over.forget X) (g i)))) :
        TypeCat.Fun (Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op Z.left))
          (Functor.obj (Functor.obj CategoryTheory.yoneda E.left) (Opposite.op (Functor.obj (Over.forget X) (T i))))) :
      (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 ((Over.forget X).obj (T i)))))
    a =
  hg.familyOfElements.sieveExtend (R := Presieve.ofArrows (fun (i : ι) ↦ (T i).left) fun (i : ι) ↦ Over.Hom.left (g i))
    (Functor.map (Over.forget X) (g i)) sorry
Tactic: have := ha _ (Sieve.ofArrows_mk _ _ i)