-- Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean
theorem existsUnique_gluing' (V : Opens X) (iUV : ∀ i : ι, U i ⟶ V) (hcover : V ≤ iSup U)
    (sf : ∀ i : ι, ToType (F.1.obj (op (U i)))) (h : IsCompatible F.1 U sf) :
    ∃! s : ToType (F.1.obj (op V)), ∀ i : ι, F.1.map (iUV i).op s = sf i

Proof state:
case intro.intro.refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf : (i : ι) → ToType (F.val.obj (op (U i)))
h : IsCompatible F.val U sf
V_eq_supr_U : V = iSup U
gl : ToType (F.val.obj (op (iSup U)))
gl_spec : IsGluing F.val U sf gl
gl_uniq : ∀ (y : ToType (F.val.obj (op (iSup U)))), (fun s => IsGluing F.val U sf s) y → y = gl
i : ι
⊢ (ConcreteCategory.hom (F.val.map (iUV i).op)) ((ConcreteCategory.hom (F.val.map (eqToHom V_eq_supr_U).op)) gl) = sf i

Tactic:
rw [← ConcreteCategory.comp_apply, ← F.1.map_comp]

Result:
case intro.intro.refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf : (i : ι) → ToType (F.val.obj (op (U i)))
h : IsCompatible F.val U sf
V_eq_supr_U : V = iSup U
gl : ToType (F.val.obj (op (iSup U)))
gl_spec : IsGluing F.val U sf gl
gl_uniq : ∀ (y : ToType (F.val.obj (op (iSup U)))), (fun s => IsGluing F.val U sf s) y → y = gl
i : ι
⊢ (ConcreteCategory.hom (F.val.map ((eqToHom V_eq_supr_U).op ≫ (iUV i).op))) gl = sf i

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf : (i : ι) → ToType (F.val.obj (op (U i)))
h : IsCompatible F.val U sf
⊢ ∃! s, ∀ (i : ι), (ConcreteCategory.hom (F.val.map (iUV i).op)) s = sf i

Tactic:
have V_eq_supr_U : V = iSup U := le_antisymm hcover (iSup_le fun i => (iUV i).le)

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf : (i : ι) → ToType (F.val.obj (op (U i)))
h : IsCompatible F.val U sf
V_eq_supr_U : V = iSup U
⊢ ∃! s, ∀ (i : ι), (ConcreteCategory.hom (F.val.map (iUV i).op)) s = sf i

Proof state:
case intro.intro.refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf : (i : ι) → ToType (F.val.obj (op (U i)))
h : IsCompatible F.val U sf
V_eq_supr_U : V = iSup U
gl : ToType (F.val.obj (op (iSup U)))
gl_spec : IsGluing F.val U sf gl
gl_uniq : ∀ (y : ToType (F.val.obj (op (iSup U)))), (fun s => IsGluing F.val U sf s) y → y = gl
⊢ ∀ (y : ToType (F.val.obj (op V))),
    (fun s => ∀ (i : ι), (ConcreteCategory.hom (F.val.map (iUV i).op)) s = sf i) y →
      y = (ConcreteCategory.hom (F.val.map (eqToHom V_eq_supr_U).op)) gl

Tactic:
intro gl' gl'_spec

Result:
case intro.intro.refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf : (i : ι) → ToType (F.val.obj (op (U i)))
h : IsCompatible F.val U sf
V_eq_supr_U : V = iSup U
gl : ToType (F.val.obj (op (iSup U)))
gl_spec : IsGluing F.val U sf gl
gl_uniq : ∀ (y : ToType (F.val.obj (op (iSup U)))), (fun s => IsGluing F.val U sf s) y → y = gl
gl' : ToType (F.val.obj (op V))
gl'_spec : ∀ (i : ι), (ConcreteCategory.hom (F.val.map (iUV i).op)) gl' = sf i
⊢ gl' = (ConcreteCategory.hom (F.val.map (eqToHom V_eq_supr_U).op)) gl

Proof state:
case intro.intro
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf : (i : ι) → ToType (F.val.obj (op (U i)))
h : IsCompatible F.val U sf
V_eq_supr_U : V = iSup U
gl : ToType (F.val.obj (op (iSup U)))
gl_spec : IsGluing F.val U sf gl
gl_uniq : ∀ (y : ToType (F.val.obj (op (iSup U)))), (fun s => IsGluing F.val U sf s) y → y = gl
⊢ ∃! s, ∀ (i : ι), (ConcreteCategory.hom (F.val.map (iUV i).op)) s = sf i

Tactic:
refine ⟨F.1.map (eqToHom V_eq_supr_U).op gl, ?_, ?_⟩

Result:
case intro.intro.refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf : (i : ι) → ToType (F.val.obj (op (U i)))
h : IsCompatible F.val U sf
V_eq_supr_U : V = iSup U
gl : ToType (F.val.obj (op (iSup U)))
gl_spec : IsGluing F.val U sf gl
gl_uniq : ∀ (y : ToType (F.val.obj (op (iSup U)))), (fun s => IsGluing F.val U sf s) y → y = gl
⊢ (fun s => ∀ (i : ι), (ConcreteCategory.hom (F.val.map (iUV i).op)) s = sf i)
    ((ConcreteCategory.hom (F.val.map (eqToHom V_eq_supr_U).op)) gl)

case intro.intro.refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf : (i : ι) → ToType (F.val.obj (op (U i)))
h : IsCompatible F.val U sf
V_eq_supr_U : V = iSup U
gl : ToType (F.val.obj (op (iSup U)))
gl_spec : IsGluing F.val U sf gl
gl_uniq : ∀ (y : ToType (F.val.obj (op (iSup U)))), (fun s => IsGluing F.val U sf s) y → y = gl
⊢ ∀ (y : ToType (F.val.obj (op V))),
    (fun s => ∀ (i : ι), (ConcreteCategory.hom (F.val.map (iUV i).op)) s = sf i) y →
      y = (ConcreteCategory.hom (F.val.map (eqToHom V_eq_supr_U).op)) gl