awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf.{w, v, u} C Y
U : Opens (↑X : Type w)
cofiltered : IsCofilteredOrEmpty.{w, w} (StructuredArrow U (Opens.map f))
⊢ IsCofiltered.{w, w} (StructuredArrow U (Opens.map f))
have cofiltered₁ : Nonempty.{w + 1} (StructuredArrow U (Opens.map f))
Tactic: refine @IsCofiltered.mk _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf.{w, v, u} C Y
U : Opens (↑X : Type w)
⊢ IsCofilteredOrEmpty.{w, w} (StructuredArrow U (Opens.map f))
have cofiltered : ∀ (X_1 Y_1 : StructuredArrow U (Opens.map f)), ∃ (W : StructuredArrow U (Opens.map f)) (x : W ⟶ X_1) (x : W ⟶ Y_1), True
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf.{w, v, u} C Y
U : Opens (↑X : Type w)
cofiltered :
  ∀ (X_1 Y_1 : StructuredArrow U (Opens.map f)),
    ∃ (W : StructuredArrow U (Opens.map f)) (x : W ⟶ X_1) (x : W ⟶ Y_1), True
⊢ IsCofilteredOrEmpty.{w, w} (StructuredArrow U (Opens.map f))
have cofiltered₁ : ∀ ⦃X_1 Y_1 : StructuredArrow U (Opens.map f)⦄ (f_1 g : X_1 ⟶ Y_1),
  ∃ (W : StructuredArrow U (Opens.map f)) (h : W ⟶ X_1), h ≫ f_1 = h ≫ g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
Goal:
X Y : TopCat
f : X ⟶ Y
⊢ CoverPreserving (Opens.grothendieckTopology (↑Y : Type w)) (Opens.grothendieckTopology (↑X : Type w)) (Opens.map f)
have cover_preserve : ∀ {U : Opens (↑Y : Type w)} {S : Sieve U},
  S ∈ (Opens.grothendieckTopology (↑Y : Type w) : (a : Opens (↑Y : Type w)) → Set (Sieve a)) U →
    Membership.mem (γ := Set (Sieve ((Opens.map f).obj U)))
      ((Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) ((Opens.map f).obj U))
      (Sieve.functorPushforward (Opens.map f) S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
Goal:
X Y : TopCat
f : X ⟶ Y
U : Opens (↑Y : Type w)
S : Sieve U
hS : S ∈ (Opens.grothendieckTopology (↑Y : Type w) : (a : Opens (↑Y : Type w)) → Set (Sieve a)) U
x : (↑X : Type w)
hx : x ∈ (Opens.map f).obj U
⊢ ∃ (U_1 : Opens (↑X : Type w)) (f_1 : U_1 ⟶ (Opens.map f).obj U),
    (Sieve.functorPushforward (Opens.map f) S).arrows f_1 ∧ x ∈ U_1
have cover_preserve : ∀ (V : Opens (↑Y : Type w)) (i : V ⟶ U) (hi : S.arrows i)
  (hxV :
    Membership.mem (α := (↑Y : Type w)) V
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier) f :
            (a : (↑X : Type w)) → (↑Y : Type w))
          x :
        (↑Y : Type w))),
  ∃ (U_1 : Opens (↑X : Type w)) (f_1 : U_1 ⟶ (Opens.map f).obj U),
    (Sieve.functorPushforward (Opens.map f) S).arrows f_1 ∧ x ∈ U_1
Tactic: obtain ⟨V, i, hi, hxV⟩ := hS (f x) hx
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf.{w, v, u} C Y
⊢ (Opens.map f).IsContinuous (Opens.grothendieckTopology (↑Y : Type w)) (Opens.grothendieckTopology (↑X : Type w))
have hF₁ : CompatiblePreserving (Opens.grothendieckTopology (↑X : Type w)) (Opens.map f)
Tactic: apply Functor.isContinuous_of_coverPreserving
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf.{w, v, u} C Y
hF₁ : CompatiblePreserving (Opens.grothendieckTopology (↑X : Type w)) (Opens.map f)
⊢ (Opens.map f).IsContinuous (Opens.grothendieckTopology (↑Y : Type w)) (Opens.grothendieckTopology (↑X : Type w))
have hF₂ : CoverPreserving (Opens.grothendieckTopology (↑Y : Type w)) (Opens.grothendieckTopology (↑X : Type w)) (Opens.map f)
Tactic: apply Functor.isContinuous_of_coverPreserving
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens (↑X : Type w)
F : Presheaf.{w, v, u} C X
F' : Sheaf.{w, v, u} C X
h : Opens.IsBasis (Set.range B)
α :
  Functor.op (inducedFunctor B) ⋙ F ⟶
    Functor.op (inducedFunctor B) ⋙
      F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w)))
i : ι
⊢ NatTrans.app
      ((restrictHomEquivHom F F' h : (a : (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj) → F ⟶ F'.obj) α)
      (op (B i)) =
    α.app (op i)
have nth_rw : NatTrans.app
    ((restrictHomEquivHom F F' h : (a : (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj) → F ⟶ F'.obj) α)
    (op (B i)) =
  ((restrictHomEquivHom F F' h).invFun ((restrictHomEquivHom F F' h).toFun α)).app (op i)
Tactic: nth_rw 2 [← (restrictHomEquivHom F F' h).left_inv α]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens (↑X : Type w)
F : Presheaf.{w, v, u} C X
F' : Sheaf.{w, v, u} C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w)))
he :
  ∀ (i : ι),
    Eq (α :=
      F.obj (op (B i)) ⟶
        F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (B i)))
      (α.app (op (B i))) (β.app (op (B i)))
⊢ α = β
have a : Eq (α :=
  Functor.op (inducedFunctor B) ⋙ F ⟶
    Functor.op (inducedFunctor B) ⋙
      F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))))
  (((restrictHomEquivHom F F' h).symm : (a : F ⟶ F'.obj) → (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj)
      α :
    Functor.op (inducedFunctor B) ⋙ F ⟶
      Functor.op (inducedFunctor B) ⋙
        F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))))
  (((restrictHomEquivHom F F' h).symm : (a : F ⟶ F'.obj) → (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj)
      β :
    Functor.op (inducedFunctor B) ⋙ F ⟶
      Functor.op (inducedFunctor B) ⋙
        F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))))
Tactic: apply (restrictHomEquivHom F F' h).symm.injective
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.Sites (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens (↑X : Type w)
F : Presheaf.{w, v, u} C X
F' : Sheaf.{w, v, u} C X
h : Opens.IsBasis (Set.range B)
α β : F ⟶ F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w)))
he :
  ∀ (i : ι),
    Eq (α :=
      F.obj (op (B i)) ⟶
        F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (B i)))
      (α.app (op (B i))) (β.app (op (B i)))
⊢ Eq (α :=
    Functor.op (inducedFunctor B) ⋙ F ⟶
      Functor.op (inducedFunctor B) ⋙
        F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))))
    (((restrictHomEquivHom F F' h).symm : (a : F ⟶ F'.obj) → (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj)
        α :
      Functor.op (inducedFunctor B) ⋙ F ⟶
        Functor.op (inducedFunctor B) ⋙
          F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))))
    (((restrictHomEquivHom F F' h).symm : (a : F ⟶ F'.obj) → (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj)
        β :
      Functor.op (inducedFunctor B) ⋙ F ⟶
        Functor.op (inducedFunctor B) ⋙
          F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))))
have a : ∀ (i : (InducedCategory (Opens (↑X : Type w)) B)ᵒᵖ),
  Eq.{v + 1} (α :=
    (Functor.op (inducedFunctor B) ⋙ F).obj i ⟶
      (Functor.op (inducedFunctor B) ⋙
            F'.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w)))).obj
        i)
    (NatTrans.app
      (((restrictHomEquivHom F F' h).symm :
          (a : F ⟶ F'.obj) → (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj)
        α)
      i)
    (NatTrans.app
      (((restrictHomEquivHom F F' h).symm :
          (a : F ⟶ F'.obj) → (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj)
        β)
      i)
Tactic: ext i
-- 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)
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens (↑X : Type x)
sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))
h : F.IsCompatible (FC := TypeCat.Fun) U sf
⊢ (↑(Functor.op (Pairwise.diagram U) ⋙ F).sections : Type (max u_4 u_5))
have refine : objPairwiseOfFamily sf ∈ (Functor.op (Pairwise.diagram U) ⋙ F).sections
Tactic: refine ⟨objPairwiseOfFamily sf, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing (goal)
Goal:
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens (↑X : Type x)
sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))
s : ToType (FC := TypeCat.Fun) (F.obj (op (iSup U)))
⊢ F.IsGluing (FC := TypeCat.Fun) U sf s ↔
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app i) :
            (a :
                (fun (X : Type u_4) ↦ X)
                  (((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                    i)) →
              (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj i))
          s =
        objPairwiseOfFamily sf i
have refine : ∀ (h : F.IsGluing (FC := TypeCat.Fun) U sf s) (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app i) :
        (a :
            (fun (X : Type u_4) ↦ X)
              (((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                i)) →
          (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj i))
      s =
    objPairwiseOfFamily sf i
Tactic: refine ⟨fun h ↦ ?_, fun h i ↦ h (op <| Pairwise.single i)⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing (goal)
Goal:
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens (↑X : Type x)
sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))
s : ToType (FC := TypeCat.Fun) (F.obj (op (iSup U)))
h : F.IsGluing (FC := TypeCat.Fun) U sf s
i j : ι
⊢ Eq (α := (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app (op (Pairwise.pair i j))) :
          (a :
              (fun (X : Type u_4) ↦ X)
                (((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                  (op (Pairwise.pair i j)))) →
            (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj (op (Pairwise.pair i j))))
        s :
      (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j))))
    (objPairwiseOfFamily sf (op (Pairwise.pair i j)) :
      (Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j)))
have pair : Eq (α := (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app (op (Pairwise.single i)) ≫
            (Functor.op (Pairwise.diagram U) ⋙ F).map (op (Pairwise.Hom.left i j))) :
        (a :
            (fun (X : Type u_4) ↦ X)
              (((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                (op (Pairwise.pair i j)))) →
          (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj (op (Pairwise.pair i j))))
      s :
    (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j))))
  (objPairwiseOfFamily sf (op (Pairwise.pair i j)) : (Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j)))
Tactic: rw [← (F.mapCone (Pairwise.cocone U).op).w (op <| Pairwise.Hom.left i j)]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing (goal)
Goal:
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens (↑X : Type x)
h : F.IsSheaf
sf : (i : ι) → F.obj (op (U i))
cpt : F.IsCompatible (FC := TypeCat.Fun) U sf
⊢ ∃! s : F.obj (op (iSup U)), F.IsGluing (FC := TypeCat.Fun) U sf s
have simp_rw : ∃! s : F.obj (op (iSup U)),
  ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
    (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 =
      objPairwiseOfFamily sf i
Tactic: simp_rw [isGluing_iff_pairwise]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing (goal)
Goal:
X : TopCat
F : Presheaf (Type u_4) X
⊢ F.IsSheaf ↔ F.IsSheafUniqueGluing (FC := TypeCat.Fun)
have simp_rw : (∀ ⦃ι : Type x⦄ (U : ι → Opens (↑X : Type x)),
    ∀ s ∈ (Functor.op (Pairwise.diagram U) ⋙ F).sections,
      ∃! x : (Functor.mapCone F (Cocone.op (Pairwise.cocone U))).pt,
        ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
          (ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app j) :
                (a :
                    ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj
                          (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                      j) →
                  ((Pairwise.diagram U).op ⋙ F).obj j)
              x =
            s j) ↔
  ∀ ⦃ι : Type x⦄ (U : ι → Opens (↑X : Type x)) (sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))),
    F.IsCompatible (FC := TypeCat.Fun) U sf →
      ∃! s : ToType (FC := TypeCat.Fun) (F.obj (op (iSup U))),
        ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
          (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 =
            objPairwiseOfFamily sf i
Tactic: simp_rw [isSheaf_iff_isSheafPairwiseIntersections, IsSheafPairwiseIntersections,
    Types.isLimit_iff, IsSheafUniqueGluing, isGluing_iff_pairwise]
-- 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 ∈ (Functor.op (Pairwise.diagram U) ⋙ F).sections,
        ∃! x : (Functor.mapCone F (Cocone.op (Pairwise.cocone U))).pt,
          ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
            (ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app j) :
                  (a :
                      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj
                            (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                        j) →
                    ((Pairwise.diagram U).op ⋙ F).obj j)
                x =
              s j) ↔
    ∀ ⦃ι : Type x⦄ (U : ι → Opens (↑X : Type x)) (sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))),
      F.IsCompatible (FC := TypeCat.Fun) U sf →
        ∃! s : ToType (FC := TypeCat.Fun) (F.obj (op (iSup U))),
          ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
            (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 =
              objPairwiseOfFamily sf i
have refine_1 : ∀ (ι : Type x) (U : ι → Opens (↑X : Type x))
  (h :
    ∀ s ∈ (Functor.op (Pairwise.diagram U) ⋙ F).sections,
      ∃! x : (Functor.mapCone F (Cocone.op (Pairwise.cocone U))).pt,
        ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
          (ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app j) :
                (a :
                    ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj
                          (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                      j) →
                  ((Pairwise.diagram U).op ⋙ F).obj j)
              x =
            s j)
  (sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))) (cpt : F.IsCompatible (FC := TypeCat.Fun) U sf),
  ∃! s : ToType (FC := TypeCat.Fun) (F.obj (op (iSup U))),
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (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 =
        objPairwiseOfFamily sf i
Tactic: refine forall₂_congr fun ι U ↦ ⟨fun h sf cpt ↦ ?_, fun h s hs ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing (hypothesis)
Goal:
X : TopCat
F : Presheaf (Type u_4) X
ι : Type x
U : ι → Opens (↑X : Type x)
h :
  ∀ (sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))),
    F.IsCompatible (FC := TypeCat.Fun) U sf →
      ∃! s : ToType (FC := TypeCat.Fun) (F.obj (op (iSup U))),
        ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
          (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 =
            objPairwiseOfFamily sf i
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → (Functor.op (Pairwise.diagram U) ⋙ F).obj j
hs : s ∈ (Functor.op (Pairwise.diagram U) ⋙ F).sections
⊢ ∃! x : (Functor.mapCone F (Cocone.op (Pairwise.cocone U))).pt,
    ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app j) :
            (a :
                ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                  j) →
              ((Pairwise.diagram U).op ⋙ F).obj j)
          x =
        s j
have 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)
Tactic: specialize h (fun i ↦ s <| op <| Pairwise.single i) fun i j ↦
      (hs <| op <| Pairwise.Hom.left i j).trans (hs <| op <| Pairwise.Hom.right i j).symm
Cleared hypotheses: h
-- 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)
⊢ ∃! x : (Functor.mapCone F (Cocone.op (Pairwise.cocone U))).pt,
    ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app j) :
            (a :
                ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                  j) →
              ((Pairwise.diagram U).op ⋙ F).obj j)
          x =
        s j
have h₁ : (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 ι)ᵒᵖ),
    s = objPairwiseOfFamily fun (i : ι) ↦ s (op (Pairwise.single i))
Tactic: convert! h
-- 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 ι)ᵒᵖ
⊢ s = objPairwiseOfFamily fun (i : ι) ↦ s (op (Pairwise.single i))
have h₁ : ∀ (i : ι),
  s (op (Pairwise.single i)) = objPairwiseOfFamily (fun (i : ι) ↦ s (op (Pairwise.single i))) (op (Pairwise.single i))
Tactic: ext (i | ⟨i, j⟩)