-- Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean
theorem eq_of_locally_eq (s t : ToType (F.1.obj (op (iSup U))))
    (h : ∀ i, F.1.map (Opens.leSupr U i).op s = F.1.map (Opens.leSupr U i).op t) : s = t

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
s t : ToType (F.val.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.val.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.val.map (leSupr U i).op)) t
sf : (i : ι) → ToType (F.val.obj (op (U i))) := fun i => (ConcreteCategory.hom (F.val.map (leSupr U i).op)) s
sf_compatible : IsCompatible F.val U sf
⊢ s = t

Tactic:
obtain ⟨gl, -, gl_uniq⟩ := F.existsUnique_gluing U sf sf_compatible

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
s t : ToType (F.val.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.val.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.val.map (leSupr U i).op)) t
sf : (i : ι) → ToType (F.val.obj (op (U i))) := fun i => (ConcreteCategory.hom (F.val.map (leSupr U i).op)) s
sf_compatible : IsCompatible F.val U sf
gl : ToType (F.val.obj (op (iSup U)))
gl_uniq : ∀ (y : ToType (F.val.obj (op (iSup U)))), (fun s => IsGluing F.val U sf s) y → y = gl
⊢ s = t

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
s t : ToType (F.val.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.val.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.val.map (leSupr U i).op)) t
sf : (i : ι) → ToType (F.val.obj (op (U i))) := fun i => (ConcreteCategory.hom (F.val.map (leSupr U i).op)) s
⊢ s = t

Tactic:
have sf_compatible : IsCompatible _ U sf := by
  intro i j
  simp_rw [sf, ← ConcreteCategory.comp_apply, ← F.1.map_comp]
  rfl

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
s t : ToType (F.val.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.val.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.val.map (leSupr U i).op)) t
sf : (i : ι) → ToType (F.val.obj (op (U i))) := fun i => (ConcreteCategory.hom (F.val.map (leSupr U i).op)) s
sf_compatible : IsCompatible F.val U sf
⊢ s = t

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
s t : ToType (F.val.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.val.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.val.map (leSupr U i).op)) t
sf : (i : ι) → ToType (F.val.obj (op (U i))) := fun i => (ConcreteCategory.hom (F.val.map (leSupr U i).op)) s
sf_compatible : IsCompatible F.val U sf
gl : ToType (F.val.obj (op (iSup U)))
gl_uniq : ∀ (y : ToType (F.val.obj (op (iSup U)))), (fun s => IsGluing F.val U sf s) y → y = gl
⊢ gl = t

Tactic:
symm

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
s t : ToType (F.val.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.val.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.val.map (leSupr U i).op)) t
sf : (i : ι) → ToType (F.val.obj (op (U i))) := fun i => (ConcreteCategory.hom (F.val.map (leSupr U i).op)) s
sf_compatible : IsCompatible F.val U sf
gl : ToType (F.val.obj (op (iSup U)))
gl_uniq : ∀ (y : ToType (F.val.obj (op (iSup U)))), (fun s => IsGluing F.val U sf s) y → y = gl
⊢ t = gl

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
s t : ToType (F.val.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.val.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.val.map (leSupr U i).op)) t
⊢ s = t

Tactic:
let sf : ∀ i : ι, ToType (F.1.obj (op (U i))) := fun i => F.1.map (Opens.leSupr U i).op s

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
s t : ToType (F.val.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.val.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.val.map (leSupr U i).op)) t
sf : (i : ι) → ToType (F.val.obj (op (U i))) := fun i => (ConcreteCategory.hom (F.val.map (leSupr U i).op)) s
⊢ s = t

Proof state:
case a
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
s t : ToType (F.val.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.val.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.val.map (leSupr U i).op)) t
sf : (i : ι) → ToType (F.val.obj (op (U i))) := fun i => (ConcreteCategory.hom (F.val.map (leSupr U i).op)) s
sf_compatible : IsCompatible F.val U sf
gl : ToType (F.val.obj (op (iSup U)))
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 (leSupr U i).op)) s = sf i

Tactic:
rfl

Result:
no goals