awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing (goal)
Goal:
X : TopCat
F : Presheaf (Type u_4) X
ι : Type x
U : ι → Opens (↑X : Type x)
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → (Functor.op (Pairwise.diagram U) ⋙ F).obj j
hs : s ∈ (Functor.op (Pairwise.diagram U) ⋙ F).sections
h :
  ∃! s_1 : ToType (FC := TypeCat.Fun) (F.obj (op (iSup U))),
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      Eq (α := (Functor.op (Pairwise.diagram U) ⋙ F).obj i)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app i) :
              (a :
                  ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                    i) →
                ((Pairwise.diagram U).op ⋙ F).obj i)
            s_1 :
          (Functor.op (Pairwise.diagram U) ⋙ F).obj i)
        (objPairwiseOfFamily (fun (i : ι) ↦ s (op (Pairwise.single i))) i : (Functor.op (Pairwise.diagram U) ⋙ F).obj i)
e_1 : (Functor.mapCone F (Cocone.op (Pairwise.cocone U))).pt = ToType (FC := TypeCat.Fun) (F.obj (op (iSup U)))
x : (Functor.mapCone F (Cocone.op (Pairwise.cocone U))).pt
a : (CategoryTheory.Pairwise ι)ᵒᵖ
h₁ :
  ∀ (i : ι),
    s (op (Pairwise.single i)) = objPairwiseOfFamily (fun (i : ι) ↦ s (op (Pairwise.single i))) (op (Pairwise.single i))
⊢ s = objPairwiseOfFamily fun (i : ι) ↦ s (op (Pairwise.single i))
have h₂ : ∀ (i j : ι),
  s (op (Pairwise.pair i j)) = objPairwiseOfFamily (fun (i : ι) ↦ s (op (Pairwise.single i))) (op (Pairwise.pair i j))
Tactic: ext (i | ⟨i, j⟩)
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst_1 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
inst_3 : HasLimitsOfSize.{x, x, v_1, u_1} C
inst_4 : Functor.ReflectsIsomorphisms.{v_1, u_1, u_3, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
X : TopCat
F : Sheaf.{x, v_1, u_1} C X
ι : Type u_4
U : ι → Opens (↑X : Type x)
V : Opens (↑X : Type x)
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf :
  (i : ι) →
    ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i)))
h :
  IsCompatible (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf
⊢ ∃! s :
    ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op V)),
    ∀ (i : ι),
      (ConcreteCategory.hom (FC := FC) (CC := CC)
              (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map (iUV i).op) :
            (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op (U i))))
          s =
        sf i
have V_eq_supr_U : V = iSup U
Tactic: have V_eq_supr_U : V = iSup U := le_antisymm hcover (iSup_le fun i => (iUV i).le)
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst_1 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
inst_3 : HasLimitsOfSize.{x, x, v_1, u_1} C
inst_4 : Functor.ReflectsIsomorphisms.{v_1, u_1, u_3, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
X : TopCat
F : Sheaf.{x, v_1, u_1} C X
ι : Type u_4
U : ι → Opens (↑X : Type x)
V : Opens (↑X : Type x)
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf :
  (i : ι) →
    ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i)))
h :
  IsCompatible (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf
V_eq_supr_U : V = iSup U
⊢ ∃! s :
    ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op V)),
    ∀ (i : ι),
      (ConcreteCategory.hom (FC := FC) (CC := CC)
              (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map (iUV i).op) :
            (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op (U i))))
          s =
        sf i
have obtain : ∀
  (gl :
    ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U))))
  (gl_spec :
    IsGluing (FC := FC) (CC := CC)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf gl)
  (gl_uniq :
    ∀
      (y :
        ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U)))),
      (fun
              (s :
                ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
                  (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj
                    (op (iSup U)))) ↦
            IsGluing (FC := FC) (CC := CC)
              (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf s)
          y →
        y = gl),
  ∃! s :
    ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op V)),
    ∀ (i : ι),
      (ConcreteCategory.hom (FC := FC) (CC := CC)
              (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map (iUV i).op) :
            (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op (U i))))
          s =
        sf i
Tactic: obtain ⟨gl, gl_spec, gl_uniq⟩ := F.existsUnique_gluing U sf h
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst_1 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
inst_3 : HasLimitsOfSize.{x, x, v_1, u_1} C
inst_4 : Functor.ReflectsIsomorphisms.{v_1, u_1, u_3, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
X : TopCat
F : Sheaf.{x, v_1, u_1} C X
ι : Type u_4
U : ι → Opens (↑X : Type x)
V : Opens (↑X : Type x)
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf :
  (i : ι) →
    ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i)))
h :
  IsCompatible (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf
V_eq_supr_U : V = iSup U
gl :
  ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U)))
gl_spec :
  IsGluing (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf gl
gl_uniq :
  ∀
    (y :
      ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U)))),
    (fun
            (s :
              ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
                (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj
                  (op (iSup U)))) ↦
          IsGluing (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf s)
        y →
      y = gl
i : ι
⊢ (ConcreteCategory.hom (FC := FC) (CC := CC)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map (iUV i).op) :
        (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op (U i))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC)
              (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
                (Quiver.Hom.op (eqToHom V_eq_supr_U))) :
            (a : CC (F.obj.obj (op (iSup U)))) → CC (F.obj.obj (op V)))
          gl :
        CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op V))) =
    sf i
have refine_1 : (ConcreteCategory.hom (FC := FC) (CC := CC)
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
          (Quiver.Hom.op (eqToHom V_eq_supr_U) ≫ (iUV i).op)) :
      (a : CC (F.obj.obj (op (iSup U)))) → CC (F.obj.obj (op (U i))))
    gl =
  sf i
Tactic: rw [← ConcreteCategory.comp_apply, ← F.1.map_comp]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst_1 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
inst_3 : HasLimitsOfSize.{x, x, v_1, u_1} C
inst_4 : Functor.ReflectsIsomorphisms.{v_1, u_1, u_3, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
X : TopCat
F : Sheaf.{x, v_1, u_1} C X
ι : Type u_4
U : ι → Opens (↑X : Type x)
s t :
  ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U)))
h :
  ∀ (i : ι),
    Eq (α :=
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC)
              (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
                (leSupr U i).op) :
            (a : CC (F.obj.obj (op (iSup U)))) → CC (F.obj.obj (op (U i))))
          s :
        CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC)
              (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
                (leSupr U i).op) :
            (a : CC (F.obj.obj (op (iSup U)))) → CC (F.obj.obj (op (U i))))
          t :
        CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))))
sf : (i : ι) →
  ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))) :=
  fun (i : ι) ↦
    (ConcreteCategory.hom (FC := FC) (CC := CC)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
            (leSupr U i).op) :
        (a : CC (F.obj.obj (op (iSup U)))) → CC (F.obj.obj (op (U i))))
      s
⊢ s = t
have sf_compatible : IsCompatible (FC := FC) (CC := CC)
  (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf
Tactic: have sf_compatible : IsCompatible _ U sf := by
    intro i j
    simp_rw [sf, ← ConcreteCategory.comp_apply, ← F.1.map_comp]
    rfl
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst_1 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
inst_3 : HasLimitsOfSize.{x, x, v_1, u_1} C
inst_4 : Functor.ReflectsIsomorphisms.{v_1, u_1, u_3, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
X : TopCat
F : Sheaf.{x, v_1, u_1} C X
ι : Type u_4
U : ι → Opens (↑X : Type x)
V : Opens (↑X : Type x)
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t :
  ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op V))
h :
  ∀ (i : ι),
    Eq (α :=
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC)
              (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map (iUV i).op) :
            (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op (U i))))
          s :
        CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC)
              (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map (iUV i).op) :
            (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op (U i))))
          t :
        CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))))
⊢ s = t
have V_eq_supr_U : V = iSup U
Tactic: have V_eq_supr_U : V = iSup U := le_antisymm hcover (iSup_le fun i => (iUV i).le)
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst_1 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
inst_3 : HasLimitsOfSize.{x, x, v_1, u_1} C
inst_4 : Functor.ReflectsIsomorphisms.{v_1, u_1, u_3, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
X : TopCat
F : Sheaf.{x, v_1, u_1} C X
ι : Type u_4
U : ι → Opens (↑X : Type x)
V : Opens (↑X : Type x)
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t :
  ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op V))
h :
  ∀ (i : ι),
    Eq (α :=
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC)
              (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map (iUV i).op) :
            (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op (U i))))
          s :
        CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC)
              (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map (iUV i).op) :
            (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op (U i))))
          t :
        CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))))
V_eq_supr_U : V = iSup U
⊢ s = t
have suffices : Eq (α := CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U))))
  ((ConcreteCategory.hom (FC := FC) (CC := CC)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
            (Quiver.Hom.op (eqToHom sorry))) :
        (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op (iSup U))))
      s :
    CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U))))
  ((ConcreteCategory.hom (FC := FC) (CC := CC)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
            (Quiver.Hom.op (eqToHom sorry))) :
        (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op (iSup U))))
      t :
    CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U))))
Tactic: suffices F.1.map (eqToHom V_eq_supr_U.symm).op s = F.1.map (eqToHom V_eq_supr_U.symm).op t by
    convert! congr_arg (F.1.map (eqToHom V_eq_supr_U).op) this <;>
    rw [← ConcreteCategory.comp_apply, ← F.1.map_comp, eqToHom_op, eqToHom_op, eqToHom_trans,
      eqToHom_refl, F.1.map_id, ConcreteCategory.id_apply]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst_1 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
inst_3 : HasLimitsOfSize.{x, x, v_1, u_1} C
inst_4 : Functor.ReflectsIsomorphisms.{v_1, u_1, u_3, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
X : TopCat
F : Sheaf.{x, v_1, u_1} C X
U₁ U₂ V : Opens (↑X : Type x)
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t :
  ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op V))
h₁ :
  Eq (α := CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₁)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map i₁.op) :
          (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op U₁)))
        s :
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₁)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map i₁.op) :
          (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op U₁)))
        t :
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₁)))
h₂ :
  Eq (α := CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₂)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map i₂.op) :
          (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op U₂)))
        s :
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₂)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map i₂.op) :
          (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op U₂)))
        t :
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₂)))
⊢ s = t
have iUV : (i : Bool) → (if i = true then U₁ else U₂) ⟶ V
Tactic: fapply F.eq_of_locally_eq' fun t : Bool => if t then U₁ else U₂
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst_1 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
inst_3 : HasLimitsOfSize.{x, x, v_1, u_1} C
inst_4 : Functor.ReflectsIsomorphisms.{v_1, u_1, u_3, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
X : TopCat
F : Sheaf.{x, v_1, u_1} C X
U₁ U₂ V : Opens (↑X : Type x)
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t :
  ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op V))
h₁ :
  Eq (α := CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₁)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map i₁.op) :
          (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op U₁)))
        s :
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₁)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map i₁.op) :
          (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op U₁)))
        t :
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₁)))
h₂ :
  Eq (α := CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₂)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map i₂.op) :
          (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op U₂)))
        s :
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₂)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map i₂.op) :
          (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op U₂)))
        t :
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₂)))
iUV : (i : Bool) → (if i = true then U₁ else U₂) ⟶ V
⊢ s = t
have hcover₁ : V ≤ ⨆ (t : Bool), if t = true then U₁ else U₂
Tactic: fapply F.eq_of_locally_eq' fun t : Bool => if t then U₁ else U₂