-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
E : PreOneHypercover.{w, v_1, u_1} X
F : Functor.{v_1, u_2, u_1, u_2 + 1} Cᵒᵖ (Type u_2)
h₁ : E.IsStronglySheafFor F
h₂ :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X),
    Presieve.IsSeparatedFor F (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v_1, u_1} E.toPreZeroHypercover)).arrows
S : Sieve.{v_1, u_1} X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows
H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) S).arrows
t : Presieve.FamilyOfElements F S.arrows
ht : t.Compatible (R := S.arrows)
s : (i : E.I₀) → F.obj (op (E.X i))
hs :
  ∀ (i : E.I₀),
    (fun (t_1 : F.obj (op (E.X i))) ↦
        (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation (R := (Sieve.pullback (E.f i) S).arrows) t_1)
      (s i)
huniq :
  ∀ (i : E.I₀) (y : F.obj (op (E.X i))),
    (fun (t_1 : F.obj (op (E.X i))) ↦
          (Presieve.FamilyOfElements.pullback (E.f i) t).IsAmalgamation (R := (Sieve.pullback (E.f i) S).arrows) t_1)
        y →
      y = s i
hr : Presieve.Arrows.Compatible F E.f s
s' : Presieve.FamilyOfElements F (Presieve.ofArrows E.X E.f)
hs' : ∀ (i : E.I₀), s' (E.f i) ⋯ = s i
t' : F.obj (op X)
ht' :
  ∀ (i : E.I₀),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.f i).op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op X))) → (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i))))
        t' =
      s i
hunique :
  ∀ (y : (fun (X : Type u_2) ↦ X) (F.obj (op X))),
    (fun (t : (fun (X : Type u_2) ↦ X) (F.obj (op X))) ↦
          ∀ (i : E.I₀),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (E.f i).op) :
                  (a : (fun (X : Type u_2) ↦ X) (F.obj (op X))) → (fun (X : Type u_2) ↦ X) (F.obj (op (E.X i))))
                t =
              s i)
        y →
      y = t'
T : C
f : T ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ T
hg : (Sieve.pullback f (PreZeroHypercover.sieve₀.{w, v_1, u_1} E.toPreZeroHypercover)).arrows g
⊢ Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op T))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj (op X))) → (fun (X : Type u_2) ↦ X) (F.obj (op T)))
            t' :
          (fun (X : Type u_2) ↦ X) (F.obj (op T))) :
      (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op T))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
        (t f hf) :
      (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
have refine_1 : ∀ ⦃Y : C⦄ (i : E.I₀) (w : Z ⟶ E.X i) (heq : w ≫ E.f i = g ≫ f),
  Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op T))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
              (a : (fun (X : Type u_2) ↦ X) (F.obj (op X))) → (fun (X : Type u_2) ↦ X) (F.obj (op T)))
            t' :
          (fun (X : Type u_2) ↦ X) (F.obj (op T))) :
      (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g.op) :
          (a : (fun (X : Type u_2) ↦ X) (F.obj (op T))) → (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
        (t f hf) :
      (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
Tactic: obtain ⟨W, w, u, ⟨i⟩, heq⟩ := hg
Cleared hypotheses: hg