-- Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
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
i j : E.I₀
Z : C
gi : Z ⟶ E.X i
gj : Z ⟶ E.X j
hgij : gi ≫ E.f i = gj ≫ E.f j
refine :
  ∀ (Y : C) (f : Y ⟶ Z),
    (E.sieve₁ gi gj).arrows f →
      ∀ (k : E.I₁ i j) (h : Y ⟶ E.Y k) (hf₁ : f ≫ gi = h ≫ E.p₁ k) (hf₂ : f ≫ gj = h ≫ E.p₂ k),
        Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op Y)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
                (a : (fun (X : Type u_2) ↦ X) (F.obj (op Z))) → (fun (X : Type u_2) ↦ X) (F.obj (op Y)))
              ((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 Z)))
                  (s i) :
                (fun (X : Type u_2) ↦ X) (F.obj (op Z))) :
            (fun (X : Type u_2) ↦ X) (F.obj (op Y)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
                (a : (fun (X : Type u_2) ↦ X) (F.obj (op Z))) → (fun (X : Type u_2) ↦ X) (F.obj (op Y)))
              ((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 Z)))
                  (s j) :
                (fun (X : Type u_2) ↦ X) (F.obj (op Z))) :
            (fun (X : Type u_2) ↦ X) (F.obj (op Y)))
⊢ Eq (α := (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
    ((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 Z)))
        (s i) :
      (fun (X : Type u_2) ↦ X) (F.obj (op Z)))
    ((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 Z)))
        (s j) :
      (fun (X : Type u_2) ↦ X) (F.obj (op Z)))

Tactic:
refine (h₁.isSeparatedFor_sieve₁ gi gj hgij).ext fun Y f ⟨k, h, hf₁, hf₂⟩ ↦ ?_

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, _private.0.CategoryTheory.PreOneHypercover.IsStronglySeparatedFor.arrowsCompatible.match_1, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Functor.map, CategoryTheory.PreOneHypercover.IsStronglySheafFor.isSeparatedFor_sieve₁, Eq, DFunLike.coe