awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.EpiMono
Goal:
X Y : TopCat
f : X ⟶ Y
suffices :
  Epi f ↔
    Epi (X :=
      Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) X)
      (CategoryTheory.Functor.map
        (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) f)
⊢ Epi f ↔
    Function.Surjective (α := (↑X : Type u)) (β := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑Y : Type u))

Tactic:
suffices Epi f ↔ Epi ((forget TopCat).map f) by
    rw [this, CategoryTheory.ofHom_epi_iff_surjective]
-- Module: Mathlib.Topology.Category.TopCat.EpiMono
Goal:
X Y : TopCat
f : X ⟶ Y
mp :
  Epi f →
    Epi (X :=
      Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) X)
      (CategoryTheory.Functor.map
        (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) f)
mpr :
  Epi (X :=
      Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) X)
      (CategoryTheory.Functor.map
        (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) f) →
    Epi f
⊢ Epi f ↔
    Epi (X :=
      Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) X)
      (CategoryTheory.Functor.map
        (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) f)

Tactic:
constructor
-- Module: Mathlib.Topology.Category.TopCat.EpiMono
Goal:
X Y : TopCat
f : X ⟶ Y
h : Epi f
⊢ Epi (X :=
    Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) X)
    (CategoryTheory.Functor.map
      (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) f)

Tactic:
apply Functor.map_epi

Premises used: CategoryTheory.Functor.map_epi
-- Module: Mathlib.Topology.Category.TopCat.EpiMono
Goal:
X Y : TopCat
f : X ⟶ Y
⊢ Epi (X :=
      Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) X)
      (CategoryTheory.Functor.map
        (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) f) →
    Epi f

Tactic:
apply Functor.epi_of_epi_map

Premises used: CategoryTheory.Functor.epi_of_epi_map
-- Module: Mathlib.Topology.Category.TopCat.EpiMono
Goal:
X Y : TopCat
f : X ⟶ Y
this :
  Mono f ↔
    Mono (X :=
      Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) X)
      (CategoryTheory.Functor.map
        (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) f)
rw :
  Function.Injective (α :=
      (fun (X : Type u) ↦ X)
        (Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
          X))
      (β :=
      (fun (X : Type u) ↦ X)
        (Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
          Y))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) f)) :
        (a : (fun (X : Type u) ↦ X) ((forget TopCat).obj X)) → (fun (X : Type u) ↦ X) ((forget TopCat).obj Y)) ↔
    Function.Injective (α := (↑X : Type u)) (β := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑Y : Type u))
⊢ Mono f ↔
    Function.Injective (α := (↑X : Type u)) (β := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑Y : Type u))

Tactic:
rw [this, CategoryTheory.mono_iff_injective]

Premises used: CategoryTheory.mono_iff_injective
-- Module: Mathlib.Topology.Category.TopCat.EpiMono
Goal:
X Y : TopCat
f : X ⟶ Y
this :
  Mono f ↔
    Mono (X :=
      Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) X)
      (CategoryTheory.Functor.map
        (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) f)
⊢ Function.Injective (α :=
      (fun (X : Type u) ↦ X)
        (Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
          X))
      (β :=
      (fun (X : Type u) ↦ X)
        (Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))
          Y))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) f)) :
        (a : (fun (X : Type u) ↦ X) ((forget TopCat).obj X)) → (fun (X : Type u) ↦ X) ((forget TopCat).obj Y)) ↔
    Function.Injective (α := (↑X : Type u)) (β := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑Y : Type u))

Tactic:
rfl
-- Module: Mathlib.Topology.Category.TopCat.EpiMono
Goal:
X Y : TopCat
f : X ⟶ Y
suffices :
  Mono f ↔
    Mono (X :=
      Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) X)
      (CategoryTheory.Functor.map
        (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) f)
⊢ Mono f ↔
    Function.Injective (α := (↑X : Type u)) (β := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑Y : Type u))

Tactic:
suffices Mono f ↔ Mono ((forget TopCat).map f) by
    rw [this, CategoryTheory.mono_iff_injective]
    rfl
-- Module: Mathlib.Topology.Category.TopCat.EpiMono
Goal:
X Y : TopCat
f : X ⟶ Y
mp :
  Mono f →
    Mono (X :=
      Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) X)
      (CategoryTheory.Functor.map
        (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) f)
mpr :
  Mono (X :=
      Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) X)
      (CategoryTheory.Functor.map
        (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) f) →
    Mono f
⊢ Mono f ↔
    Mono (X :=
      Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) X)
      (CategoryTheory.Functor.map
        (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) f)

Tactic:
constructor
-- Module: Mathlib.Topology.Category.TopCat.EpiMono
Goal:
X Y : TopCat
f : X ⟶ Y
h : Mono f
⊢ Mono (X :=
    Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) X)
    (CategoryTheory.Functor.map
      (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) f)

Tactic:
apply Functor.map_mono

Premises used: CategoryTheory.Functor.map_mono
-- Module: Mathlib.Topology.Category.TopCat.EpiMono
Goal:
X Y : TopCat
f : X ⟶ Y
⊢ Mono (X :=
      Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) X)
      (CategoryTheory.Functor.map
        (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) f) →
    Mono f

Tactic:
apply Functor.mono_of_mono_map

Premises used: CategoryTheory.Functor.mono_of_mono_map
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X Y : TopCat
f : X ⟶ Y
⊢ isOpenEmbedding f ↔
    Topology.IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑Y : Type u))

Tactic:
.rfl

Premises used: Iff.rfl, TopCat.isOpenEmbedding
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
⊢ isOpenEmbedding.RespectsIso

Tactic:
MorphismProperty.respectsIso_of_isStableUnderComposition fun _ _ f (_ : IsIso f) ↦
    (TopCat.homeoOfIso (asIso f)).isOpenEmbedding

Premises used: TopCat.homeoOfIso, CategoryTheory.MorphismProperty.respectsIso_of_isStableUnderComposition, Homeomorph.isOpenEmbedding, CategoryTheory.asIso
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
⊢ isOpenEmbedding.IsStableUnderBaseChange

Tactic:
.mk' fun _ _ _ _ _ _ hg ↦ fst_isOpenEmbedding_of_right _ hg

Premises used: CategoryTheory.MorphismProperty.IsStableUnderBaseChange.mk', TopCat.fst_isOpenEmbedding_of_right
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X : TopCat
E : Precoverage.ZeroHypercover.{u_1, u, u + 1} precoverage X
⊢ ∀ (x : (↑X : Type u)),
    ∃ (i : E.I₀),
      Membership.mem (γ := Set (↑X : Type u))
        (Set.range (ι := (↑(E.X i) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (E.f i)) :
            (a : (↑(E.X i) : Type u)) → (↑X : Type u)))
        x

Tactic:
simpa using E.mem₀.left

Premises used: And.left, CategoryTheory.Precoverage.ZeroHypercover.mem₀
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X : TopCat
E : Precoverage.ZeroHypercover.{u_1, u, u + 1} precoverage X
⊢ ∀ (i : E.I₀),
    Topology.IsOpenEmbedding (X := (↑(E.X i) : Type u)) (Y := (↑X : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (E.f i)) :
        (a : (↑(E.X i) : Type u)) → (↑X : Type u))

Tactic:
simpa using E.mem₀.right

Premises used: And.right, CategoryTheory.Precoverage.ZeroHypercover.mem₀
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
⊢ grothendieckTopology.Subcanonical

Tactic:
.of_isSheaf_yoneda_obj _ fun X ↦ ?_

Premises used: CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
refine : ∀ (X : TopCat.{u_1}), Presieve.IsSheaf grothendieckTopology (Functor.obj yoneda X)
⊢ grothendieckTopology.Subcanonical

Tactic:
refine .of_isSheaf_yoneda_obj _ fun X ↦ ?_
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X : TopCat
rw : ∀ ⦃X_1 : TopCat.{u_1}⦄ (E : precoverage.ZeroHypercover X_1), Presieve.IsSheafFor (Functor.obj yoneda X) E.presieve₀
⊢ Presieve.IsSheaf grothendieckTopology (Functor.obj yoneda X)

Tactic:
rw [Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small]

Premises used: CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
rw :
  ∀ (x : (i : 𝒰.I₀) → Functor.obj (Functor.obj yoneda X) (Opposite.op (𝒰.X i))),
    Presieve.Arrows.Compatible (Functor.obj yoneda X) 𝒰.f x →
      ∃! t : (fun (X : Type u_1) ↦ X) (Functor.obj (Functor.obj yoneda X) (Opposite.op Y)),
        ∀ (i : 𝒰.I₀),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (CategoryTheory.Functor.map (Functor.obj yoneda X) (𝒰.f i).op) :
                (a : (fun (X : Type u_1) ↦ X) ((yoneda.obj X).obj (Opposite.op Y))) →
                  (fun (X : Type u_1) ↦ X) ((yoneda.obj X).obj (Opposite.op (𝒰.X i))))
              t =
            x i
⊢ Presieve.IsSheafFor (Functor.obj yoneda X) 𝒰.presieve₀

Tactic:
rw [Presieve.isSheafFor_arrows_iff]

Premises used: CategoryTheory.Presieve.isSheafFor_arrows_iff
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
i : 𝒰.I₀
y : (↑(𝒰.X i) : Type u_1)
⊢ Membership.mem (α := (↑Y : Type u_1)) (γ := Set (↑Y : Type u_1))
    (Set.range (ι := (↑(𝒰.X i) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (𝒰.f i)) :
        (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (𝒰.f i) :
          (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1))
        y :
      (↑Y : Type u_1))

Tactic:
simp
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
⊢ ∀ (i : 𝒰.I₀) (y : (↑(𝒰.X i) : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (𝒰.f i) :
            (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1))
          y :
        (↑Y : Type u_1))
      ((↑(Subtype.mk (p := fun (x : (↑Y : Type u_1)) ↦
              Membership.mem (γ := Set (↑Y : Type u_1))
                (Set.range (ι := (↑(𝒰.X i) : Type u_1))
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                        carrier) (𝒰.f i)) :
                    (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1)))
                x)
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    carrier) (𝒰.f i) :
                  (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1))
                y)
              ⋯) :
          (↑Y : Type u_1)) :
        (↑Y : Type u_1))

Tactic:
have heq (i y) : 𝒰.f i y = (Subtype.val : Set.range (𝒰.f i) → Y) ⟨𝒰.f i y, by simp⟩ := rfl
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq :
  ∀ (i : 𝒰.I₀) (y : (↑(𝒰.X i) : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (𝒰.f i) :
            (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1))
          y :
        (↑Y : Type u_1))
      ((↑(Subtype.mk (p := fun (x : (↑Y : Type u_1)) ↦
              Membership.mem (γ := Set (↑Y : Type u_1))
                (Set.range (ι := (↑(𝒰.X i) : Type u_1))
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                        carrier) (𝒰.f i)) :
                    (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1)))
                x)
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    carrier) (𝒰.f i) :
                  (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1))
                y)
              ⋯) :
          (↑Y : Type u_1)) :
        (↑Y : Type u_1))
⊢ ∀ (x : (i : 𝒰.I₀) → Functor.obj (Functor.obj yoneda X) (Opposite.op (𝒰.X i))),
    Presieve.Arrows.Compatible (Functor.obj yoneda X) 𝒰.f x →
      ∃! t : (fun (X : Type u_1) ↦ X) (Functor.obj (Functor.obj yoneda X) (Opposite.op Y)),
        ∀ (i : 𝒰.I₀),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (CategoryTheory.Functor.map (Functor.obj yoneda X) (𝒰.f i).op) :
                (a : (fun (X : Type u_1) ↦ X) ((yoneda.obj X).obj (Opposite.op Y))) →
                  (fun (X : Type u_1) ↦ X) ((yoneda.obj X).obj (Opposite.op (𝒰.X i))))
              t =
            x i

Tactic:
fun x hx ↦ ⟨?_, fun i ↦ ?_, fun f hf ↦ ?_⟩

Premises used: ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq :
  ∀ (i : 𝒰.I₀) (y : (↑(𝒰.X i) : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (𝒰.f i) :
            (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1))
          y :
        (↑Y : Type u_1))
      ((↑(Subtype.mk (p := fun (x : (↑Y : Type u_1)) ↦
              Membership.mem (γ := Set (↑Y : Type u_1))
                (Set.range (ι := (↑(𝒰.X i) : Type u_1))
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                        carrier) (𝒰.f i)) :
                    (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1)))
                x)
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    carrier) (𝒰.f i) :
                  (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1))
                y)
              ⋯) :
          (↑Y : Type u_1)) :
        (↑Y : Type u_1))
x : (i : 𝒰.I₀) → Functor.obj (Functor.obj yoneda X) (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (Functor.obj yoneda X) 𝒰.f x
i : 𝒰.I₀
⊢ Continuous (X :=
    (↑((fun (i : 𝒰.I₀) ↦
            (Set.range (ι := (↑(𝒰.X i) : Type u_1))
                (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                      carrier) (𝒰.f i)) :
                  (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1)) :
              Set (↑Y : Type u_1)))
          i) :
      Type u_1))
    (Y := (↑X : Type u_1))
    (Function.comp (β := (↑(Opposite.unop (Opposite.op (𝒰.X i))) : Type u_1))
      (⇑(Hom.hom (x i)) : (a : (↑(Opposite.unop (Opposite.op (𝒰.X i))) : Type u_1)) → (↑X : Type u_1))
      (⇑⋯.toHomeomorph.symm :
        (a :
            (↑(Set.range (⇑(ConcreteCategory.hom (𝒰.f i)) : (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1))) :
              Type u_1)) →
          (↑(𝒰.X i) : Type u_1)))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq :
  ∀ (i : 𝒰.I₀) (y : (↑(𝒰.X i) : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (𝒰.f i) :
            (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1))
          y :
        (↑Y : Type u_1))
      ((↑(Subtype.mk (p := fun (x : (↑Y : Type u_1)) ↦
              Membership.mem (γ := Set (↑Y : Type u_1))
                (Set.range (ι := (↑(𝒰.X i) : Type u_1))
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                        carrier) (𝒰.f i)) :
                    (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1)))
                x)
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    carrier) (𝒰.f i) :
                  (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1))
                y)
              ⋯) :
          (↑Y : Type u_1)) :
        (↑Y : Type u_1))
x : (i : 𝒰.I₀) → Functor.obj (Functor.obj yoneda X) (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (Functor.obj yoneda X) 𝒰.f x
i : 𝒰.I₀
⊢ C((↑((fun (i : 𝒰.I₀) ↦
            (Set.range (ι := (↑(𝒰.X i) : Type u_1))
                (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                      carrier) (𝒰.f i)) :
                  (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1)) :
              Set (↑Y : Type u_1)))
          i) :
      Type u_1),
    (↑X : Type u_1))

Tactic:
exact ⟨(x i).hom ∘ (isOpenEmbedding_f_zeroHypercover 𝒰 i).toHomeomorph.symm, by fun_prop⟩
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq :
  ∀ (i : 𝒰.I₀) (y : (↑(𝒰.X i) : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (𝒰.f i) :
            (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1))
          y :
        (↑Y : Type u_1))
      ((↑(Subtype.mk (p := fun (x : (↑Y : Type u_1)) ↦
              Membership.mem (γ := Set (↑Y : Type u_1))
                (Set.range (ι := (↑(𝒰.X i) : Type u_1))
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                        carrier) (𝒰.f i)) :
                    (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1)))
                x)
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    carrier) (𝒰.f i) :
                  (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1))
                y)
              ⋯) :
          (↑Y : Type u_1)) :
        (↑Y : Type u_1))
x : (i : 𝒰.I₀) → Functor.obj (Functor.obj yoneda X) (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (Functor.obj yoneda X) 𝒰.f x
i j : 𝒰.I₀
y : (↑Y : Type u_1)
xi : (↑(𝒰.X i) : Type u_1)
hi :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier) (𝒰.f i) :
        (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1))
      xi =
    y
xj : (↑(𝒰.X j) : Type u_1)
hj :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier) (𝒰.f j) :
        (a : (↑(𝒰.X j) : Type u_1)) → (↑Y : Type u_1))
      xj =
    y
⊢ Eq (α :=
    (fun (X : Type u_1) ↦ X) (Functor.obj (Functor.obj yoneda X) (Opposite.op (pullbackCone (𝒰.f i) (𝒰.f j)).pt)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (Functor.obj yoneda X) (pullbackCone (𝒰.f i) (𝒰.f j)).fst.op) :
          (a : (fun (X : Type u_1) ↦ X) ((yoneda.obj X).obj (Opposite.op (𝒰.X i)))) →
            (fun (X : Type u_1) ↦ X) ((yoneda.obj X).obj (Opposite.op (pullbackCone (𝒰.f i) (𝒰.f j)).pt)))
        (x i) :
      (fun (X : Type u_1) ↦ X) (Functor.obj (Functor.obj yoneda X) (Opposite.op (pullbackCone (𝒰.f i) (𝒰.f j)).pt)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (Functor.obj yoneda X) (pullbackCone (𝒰.f i) (𝒰.f j)).snd.op) :
          (a : (fun (X : Type u_1) ↦ X) ((yoneda.obj X).obj (Opposite.op (𝒰.X j)))) →
            (fun (X : Type u_1) ↦ X) ((yoneda.obj X).obj (Opposite.op (pullbackCone (𝒰.f i) (𝒰.f j)).pt)))
        (x j) :
      (fun (X : Type u_1) ↦ X) (Functor.obj (Functor.obj yoneda X) (Opposite.op (pullbackCone (𝒰.f i) (𝒰.f j)).pt)))

Tactic:
have := hx i j _ (TopCat.pullbackCone (𝒰.f i) (𝒰.f j)).fst
        (TopCat.pullbackCone (𝒰.f i) (𝒰.f j)).snd (TopCat.pullbackCone (𝒰.f i) (𝒰.f j)).condition