-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.SheafOfTypes (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt) f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z) ⋯
F₁ : Over.mk (g₁ ≫ f₁) ⟶ Over.mk f₁ := Over.homMk g₁ ⋯
F₂ : Over.mk (g₂ ≫ f₂) ⟶ Over.mk f₂ := Over.homMk g₂ ⋯
hF :
  Eq (α :=
    S.arrows.diagram.obj
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₁ ≫ f₁)) hgf₁) ⟶
      Functor.obj (C := S.arrows.category) (Functor.obj (Functor.const S.arrows.category) s.pt)
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₂ ≫ f₂)) hgf₂))
    (S.arrows.diagram.map (ObjectProperty.homMk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) F) ≫
      s.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₂ ≫ f₂)) hgf₂))
    (s.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₁ ≫ f₁)) hgf₁) ≫
      Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt)
        (ObjectProperty.homMk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) F))
hF₁ :
  Eq (α :=
    S.arrows.diagram.obj
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₁ ≫ f₁)) hgf₁) ⟶
      Functor.obj (C := S.arrows.category) (Functor.obj (Functor.const S.arrows.category) s.pt)
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk f₁) hf₁))
    (S.arrows.diagram.map (ObjectProperty.homMk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) F₁) ≫
      s.ι.app (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk f₁) hf₁))
    (s.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₁ ≫ f₁)) hgf₁) ≫
      Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt)
        (ObjectProperty.homMk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) F₁))
⊢ Eq (α := Z ⟶ s.pt)
    (g₁ ≫ s.ι.app (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk f₁) hf₁))
    (g₂ ≫ s.ι.app (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk f₂) hf₂))
have hF₂ : Eq (α :=
  S.arrows.diagram.obj
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₂ ≫ f₂)) hgf₂) ⟶
    Functor.obj (C := S.arrows.category) (Functor.obj (Functor.const S.arrows.category) s.pt)
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk f₂) hf₂))
  (S.arrows.diagram.map (ObjectProperty.homMk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) F₂) ≫
    s.ι.app (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk f₂) hf₂))
  (s.ι.app
      (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₂ ≫ f₂)) hgf₂) ≫
    Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt)
      (ObjectProperty.homMk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) F₂))
Tactic: have hF₂ := @Hs ⟨Over.mk (g₂ ≫ f₂), hgf₂⟩ ⟨Over.mk f₂, hf₂⟩ (ObjectProperty.homMk F₂)