-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover.{u_3, v_1, u_1} S
inst_1 : E.HasPullbacks
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
s : (E.toPreOneHypercover.multicospanIndex F).sections
i j : E.I₀
W : C
gi : W ⟶ E.X i
gj : W ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
⊢ Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map gi.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        (s.val i) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map gj.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op (E.X j)))) → (fun (X : Type u_2) ↦ X) (F.obj (op W)))
        (s.val j) :
      (fun (X : Type u_2) ↦ X) (F.obj (op W)))
have heq : Eq (α :=
  (fun (X : Type u_2) ↦ X)
    ((E.toPreOneHypercover.multicospanIndex F).right
      (Sigma.mk (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2)
        (i, j) PUnit.unit)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          ((E.toPreOneHypercover.multicospanIndex F).fst
            (Sigma.mk (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦
              E.toPreOneHypercover.I₁ i.1 i.2) (i, j) PUnit.unit)) :
        (a :
            (fun (X : Type u_2) ↦ X)
              ((E.toPreOneHypercover.multicospanIndex F).left
                (E.toPreOneHypercover.multicospanShape.fst ⟨(i, j), PUnit.unit⟩))) →
          (fun (X : Type u_2) ↦ X) ((E.toPreOneHypercover.multicospanIndex F).right ⟨(i, j), PUnit.unit⟩))
      (s.val
        (E.toPreOneHypercover.multicospanShape.fst
          (Sigma.mk (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2)
            (i, j) PUnit.unit))) :
    (fun (X : Type u_2) ↦ X)
      ((E.toPreOneHypercover.multicospanIndex F).right
        (Sigma.mk (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2)
          (i, j) PUnit.unit)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          ((E.toPreOneHypercover.multicospanIndex F).snd
            (Sigma.mk (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦
              E.toPreOneHypercover.I₁ i.1 i.2) (i, j) PUnit.unit)) :
        (a :
            (fun (X : Type u_2) ↦ X)
              ((E.toPreOneHypercover.multicospanIndex F).left
                (E.toPreOneHypercover.multicospanShape.snd ⟨(i, j), PUnit.unit⟩))) →
          (fun (X : Type u_2) ↦ X) ((E.toPreOneHypercover.multicospanIndex F).right ⟨(i, j), PUnit.unit⟩))
      (s.val
        (E.toPreOneHypercover.multicospanShape.snd
          (Sigma.mk (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2)
            (i, j) PUnit.unit))) :
    (fun (X : Type u_2) ↦ X)
      ((E.toPreOneHypercover.multicospanIndex F).right
        (Sigma.mk (β := fun (i : E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀) ↦ E.toPreOneHypercover.I₁ i.1 i.2)
          (i, j) PUnit.unit)))
Tactic: have heq := s.property ⟨(i, j), ⟨⟩⟩