-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ Functor.obj coyoneda E) S.arrows
E : A
π : Functor.obj (Functor.const S.arrows.categoryᵒᵖ) E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃
  { x : FamilyOfElements (P ⋙ Functor.obj coyoneda (op E)) S.arrows // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
f₁ f₂ : { pt := E, π := eqv.invFun (eqv.toFun π) : Cone (S.arrows.diagram.op ⋙ P) } ⟶ P.mapCone S.arrows.cocone.op
eqv' : (SieveCompatible.cone (E := op E) (x :=
      (↑((eqv :
              (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
            π) :
        FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows))
      ⋯ ⟶
    P.mapCone S.arrows.cocone.op) ≃
  { t : (P ⋙ Functor.obj coyoneda (op E)).obj (op X) //
    IsAmalgamation (R := S.arrows)
      (↑((eqv :
              (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
            π) :
        FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows)
      t } :=
  homEquivAmalgamation ⋯
⊢ f₁ = f₂
have mpr : Eq (α :=
  { t : (P ⋙ Functor.obj coyoneda (op E)).obj (op X) //
    IsAmalgamation (R := S.arrows)
      (↑((eqv :
              (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
            π) :
        FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows)
      t })
  ((eqv' :
        (a : sorry.cone ⟶ P.mapCone S.arrows.cocone.op) →
          { t : (P ⋙ coyoneda.obj (op E)).obj (op X) //
            (↑((eqv :
                        (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                          { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
                      π) :
                  FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows).IsAmalgamation
              t })
      f₁ :
    { t : (P ⋙ Functor.obj coyoneda (op E)).obj (op X) //
      IsAmalgamation (R := S.arrows)
        (↑((eqv :
                (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                  { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
              π) :
          FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows)
        t })
  ((eqv' :
        (a : sorry.cone ⟶ P.mapCone S.arrows.cocone.op) →
          { t : (P ⋙ coyoneda.obj (op E)).obj (op X) //
            (↑((eqv :
                        (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                          { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
                      π) :
                  FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows).IsAmalgamation
              t })
      f₂ :
    { t : (P ⋙ Functor.obj coyoneda (op E)).obj (op X) //
      IsAmalgamation (R := S.arrows)
        (↑((eqv :
                (a : (S.arrows.diagram.op ⋙ P).cones.obj (op E)) →
                  { x : FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows // x.SieveCompatible })
              π) :
          FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows)
        t })
Tactic: apply eqv'.injective