Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: case refine_1
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
⊢ (fun X ↦ X) ((yoneda.obj X).obj (Opposite.op Y))

pp: case refine_2
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
i : 𝒰.I₀
⊢ (ConcreteCategory.hom ((yoneda.obj X).map (𝒰.f i).op)) ?refine_1 = x i

pp: case refine_3
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
f : (fun X ↦ X) ((yoneda.obj X).obj (Opposite.op Y))
hf : (fun t ↦ ∀ (i : 𝒰.I₀), (ConcreteCategory.hom ((yoneda.obj X).map (𝒰.f i).op)) t = x i) f
⊢ f = ?refine_1

Tactic:
· refine ofHom <| ContinuousMap.liftCover (fun i ↦ Set.range (𝒰.f i)) ?_ ?_ ?_
    · intro i
      exact ⟨(x i).hom ∘ (isOpenEmbedding_f_zeroHypercover 𝒰 i).toHomeomorph.symm, by fun_prop⟩
    · intro i j y
      simp only [Set.mem_range, ContinuousMap.coe_mk, Function.comp_apply, forall_exists_index]
      intro xi hi xj hj
      conv_lhs => simp only [← hi]
      conv_rhs => simp only [← hj]
      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
      dsimp at this
      simpa using! congr($(this) ⟨(xi, xj), hi ▸ hj.symm⟩)
    · intro x
      obtain ⟨i, hi⟩ := exists_mem_zeroHypercover_range 𝒰 x
      exact ⟨i, (isOpenEmbedding_f_zeroHypercover 𝒰 i).isOpen_range.mem_nhds hi⟩

Goal state after:
case refine_2
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
i : 𝒰.I₀
⊢ (ConcreteCategory.hom ((yoneda.obj X).map (𝒰.f i).op))
      (ofHom
        (ContinuousMap.liftCover (fun i ↦ Set.range ⇑(ConcreteCategory.hom (𝒰.f i)))
          (fun i ↦ { toFun := ⇑(Hom.hom (x i)) ∘ ⇑⋯.toHomeomorph.symm, continuous_toFun := ⋯ }) ⋯ ⋯)) =
    x i

case refine_3
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
f : (fun X ↦ X) ((yoneda.obj X).obj (Opposite.op Y))
hf : (fun t ↦ ∀ (i : 𝒰.I₀), (ConcreteCategory.hom ((yoneda.obj X).map (𝒰.f i).op)) t = x i) f
⊢ f =
    ofHom
      (ContinuousMap.liftCover (fun i ↦ Set.range ⇑(ConcreteCategory.hom (𝒰.f i)))
        (fun i ↦ { toFun := ⇑(Hom.hom (x i)) ∘ ⇑⋯.toHomeomorph.symm, continuous_toFun := ⋯ }) ⋯ ⋯)