-- 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:
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

Tactic:
obtain ⟨gl, gl_spec, gl_uniq⟩ := F.existsUnique_gluing U sf h

Result:
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

Proof state:
case intro.intro.refine_2.convert_3
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
i : ι
⊢ (ConcreteCategory.hom (F.val.map ((eqToHom ⋯).op ≫ (leSupr U i).op))) gl' = sf i

Tactic:
exact gl'_spec i

Result:
no goals

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
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

Tactic:
convert congr_arg _ (gl_uniq (F.1.map (eqToHom V_eq_supr_U.symm).op gl') fun i => _) <;>
  rw [← ConcreteCategory.comp_apply, ← F.1.map_comp]

Result:
case h.e'_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 ⋯).op ≫ (eqToHom V_eq_supr_U).op))) gl'

case intro.intro.refine_2.convert_3
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
i : ι
⊢ (ConcreteCategory.hom (F.val.map ((eqToHom ⋯).op ≫ (leSupr U i).op))) gl' = sf i

Proof state:
case h.e'_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 ⋯).op ≫ (eqToHom V_eq_supr_U).op))) gl'

Tactic:
rw [eqToHom_op, eqToHom_op, eqToHom_trans, eqToHom_refl, F.1.map_id,
  ConcreteCategory.id_apply]

Result:
no goals

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 ((eqToHom V_eq_supr_U).op ≫ (iUV i).op))) gl = sf i

Tactic:
exact gl_spec i

Result:
no goals