awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.EffectiveEpi (goal)
Goal:
B X : TopCat
π : X ⟶ B
hπ :
  IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
      (a : (↑X : Type u)) → (↑B : Type u))
W : TopCat
e : X ⟶ W
h : ∀ {Z : TopCat.{u}} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W
hm : π ≫ g = e
⊢ Hom.hom g =
    Hom.hom
      (ofHom
        ((hπ.liftEquiv :
            (a :
                { g : C((↑X : Type u), (↑W : Type u)) //
                  Function.FactorsThrough (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
                    (⇑(ConcreteCategory.hom π) : (a : (↑X : Type u)) → (↑B : Type u)) }) →
              C((↑B : Type u), (↑W : Type u)))
          (Subtype.mk (p := fun (g : C((↑X : Type u), (↑W : Type u))) ↦
            Function.FactorsThrough (α := (↑X : Type u)) (β := (↑B : Type u)) (γ := (↑W : Type u))
              (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    π) :
                (a : (↑X : Type u)) → (↑B : Type u)))
            (Hom.hom e) ⋯)))
have hf : Eq (α :=
  { g : C((↑X : Type u), (↑W : Type u)) //
    Function.FactorsThrough (α := (↑X : Type u)) (β := (↑B : Type u)) (γ := (↑W : Type u))
      (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
        (a : (↑X : Type u)) → (↑B : Type u)) })
  ((Equiv.symm hπ.liftEquiv :
        (a : C((↑B : Type u), (↑W : Type u))) →
          { g : C((↑X : Type u), (↑W : Type u)) //
            Function.FactorsThrough (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
              (⇑(ConcreteCategory.hom π) : (a : (↑X : Type u)) → (↑B : Type u)) })
      (Hom.hom g) :
    { g : C((↑X : Type u), (↑W : Type u)) //
      Function.FactorsThrough (α := (↑X : Type u)) (β := (↑B : Type u)) (γ := (↑W : Type u))
        (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
          (a : (↑X : Type u)) → (↑B : Type u)) })
  (Subtype.mk (p := fun (g : C((↑X : Type u), (↑W : Type u))) ↦
      Function.FactorsThrough (α := (↑X : Type u)) (β := (↑B : Type u)) (γ := (↑W : Type u))
        (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
          (a : (↑X : Type u)) → (↑B : Type u)))
      (Hom.hom e) sorry :
    { g : C((↑X : Type u), (↑W : Type u)) //
      Function.FactorsThrough (α := (↑X : Type u)) (β := (↑B : Type u)) (γ := (↑W : Type u))
        (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
          (a : (↑X : Type u)) → (↑B : Type u)) })
Tactic: rw [hom_ofHom, ← Equiv.symm_apply_eq hπ.liftEquiv]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.EffectiveEpi (goal)
Goal:
B X : TopCat
π : X ⟶ B
hπ :
  IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
      (a : (↑X : Type u)) → (↑B : Type u))
W : TopCat
e : X ⟶ W
h : ∀ {Z : TopCat.{u}} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W
hm : π ≫ g = e
a : (↑X : Type u)
⊢ Eq (α := (↑W : Type u))
    (((↑((Equiv.symm hπ.liftEquiv :
                  (a : C((↑B : Type u), (↑W : Type u))) →
                    { g : C((↑X : Type u), (↑W : Type u)) //
                      Function.FactorsThrough (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
                        (⇑(ConcreteCategory.hom π) : (a : (↑X : Type u)) → (↑B : Type u)) })
                (Hom.hom g)) :
            C((↑X : Type u), (↑W : Type u))) :
          (a : (↑X : Type u)) → (↑W : Type u))
        a :
      (↑W : Type u))
    (((↑(Subtype.mk (p := fun (g : C((↑X : Type u), (↑W : Type u))) ↦
                Function.FactorsThrough (α := (↑X : Type u)) (β := (↑B : Type u)) (γ := (↑W : Type u))
                  (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        carrier) π) :
                    (a : (↑X : Type u)) → (↑B : Type u)))
                (Hom.hom e) ⋯) :
            C((↑X : Type u), (↑W : Type u))) :
          (a : (↑X : Type u)) → (↑W : Type u))
        a :
      (↑W : Type u))
have hf : Eq (α := (↑W : Type u))
  ((Hom.hom g : (a : (↑B : Type u)) → (↑W : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π :
            (a : (↑X : Type u)) → (↑B : Type u))
          a :
        (↑B : Type u)) :
    (↑W : Type u))
  ((Hom.hom (π ≫ g) : (a : (↑X : Type u)) → (↑W : Type u)) a : (↑W : Type u))
Tactic: simp only [IsQuotientMap.liftEquiv_symm_apply_coe, ContinuousMap.comp_apply, ← hm]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.EffectiveEpi (goal)
Goal:
B X : TopCat
π : X ⟶ B
⊢ EffectiveEpi π ↔
    IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
        (a : (↑X : Type u)) → (↑B : Type u))
have refine : EffectiveEpi π →
  IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
      (a : (↑X : Type u)) → (↑B : Type u))
Tactic: refine ⟨fun _ ↦ ?_, fun hπ ↦ ⟨⟨effectiveEpiStructOfQuotientMap π hπ⟩⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.EpiMono (goal)
Goal:
X Y : TopCat
f : X ⟶ Y
this :
  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))
have rw : 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) ↔
  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: rw [this, CategoryTheory.ofHom_epi_iff_surjective]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.EpiMono (goal)
Goal:
X Y : TopCat
f : X ⟶ Y
this :
  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)
rw :
  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) ↔
    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))
⊢ 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))
have rw₁ : Function.Surjective (α :=
    Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) X)
    (β :=
    Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) Y)
    (⇑(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)) ↔
  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: rw [this, CategoryTheory.ofHom_epi_iff_surjective]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.EpiMono (goal)
Goal:
X Y : TopCat
f : X ⟶ Y
⊢ 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))
have 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)
Tactic: suffices Epi f ↔ Epi ((forget TopCat).map f) by
    rw [this, CategoryTheory.ofHom_epi_iff_surjective]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.EpiMono (goal)
Goal:
X Y : TopCat
f : X ⟶ Y
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.EpiMono (goal)
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)
⊢ 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)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.EpiMono (goal)
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)
⊢ 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))
have 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))
Tactic: rw [this, CategoryTheory.mono_iff_injective]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.EpiMono (goal)
Goal:
X Y : TopCat
f : X ⟶ Y
⊢ 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))
have 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)
Tactic: suffices Mono f ↔ Mono ((forget TopCat).map f) by
    rw [this, CategoryTheory.mono_iff_injective]
    rfl
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.EpiMono (goal)
Goal:
X Y : TopCat
f : X ⟶ Y
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.EpiMono (goal)
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)
⊢ 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)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.GrothendieckTopology (goal)
Goal:
⊢ grothendieckTopology.Subcanonical
have refine : ∀ (X : TopCat.{u_1}), Presieve.IsSheaf grothendieckTopology (Functor.obj yoneda X)
Tactic: refine .of_isSheaf_yoneda_obj _ fun X ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.GrothendieckTopology (goal)
Goal:
X : TopCat
⊢ Presieve.IsSheaf grothendieckTopology (Functor.obj yoneda X)
have rw : ∀ ⦃X_1 : TopCat.{u_1}⦄ (E : precoverage.ZeroHypercover X_1), Presieve.IsSheafFor (Functor.obj yoneda X) E.presieve₀
Tactic: rw [Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.GrothendieckTopology (goal)
Goal:
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
⊢ Presieve.IsSheafFor (Functor.obj yoneda X) 𝒰.presieve₀
have 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
Tactic: rw [Presieve.isSheafFor_arrows_iff]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.GrothendieckTopology (hypothesis)
Goal:
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
⊢ ∀ (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
have 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)
            sorry) :
        (↑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
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.GrothendieckTopology (goal)
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
have refine_1 : (x : (i : 𝒰.I₀) → Functor.obj (Functor.obj yoneda X) (Opposite.op (𝒰.X i))) →
  (hx : Presieve.Arrows.Compatible (Functor.obj yoneda X) 𝒰.f x) →
    (fun (X : Type u_1) ↦ X) (Functor.obj (Functor.obj yoneda X) (Opposite.op Y))
Tactic: refine fun x hx ↦ ⟨?_, fun i ↦ ?_, fun f hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.GrothendieckTopology (goal)
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
⊢ (fun (X : Type u_1) ↦ X) (Functor.obj (Functor.obj yoneda X) (Opposite.op Y))
have refine_1 : (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: refine ofHom <| ContinuousMap.liftCover (fun i ↦ Set.range (𝒰.f i)) ?_ ?_ ?_