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

Tactic:
trans gl

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
⊢ s = gl

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

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
⊢ t = gl

Tactic:
apply gl_uniq

Result:
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
⊢ IsGluing F.val U sf 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
i j : ι
⊢ (ConcreteCategory.hom (F.val.map ((leSupr U i).op ≫ ((U i).infLELeft (U j)).op))) s =
    (ConcreteCategory.hom (F.val.map ((leSupr U j).op ≫ ((U i).infLERight (U j)).op))) s

Tactic:
rfl

Result:
no goals

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)) t = sf i

Tactic:
rw [← h]

Result:
no goals

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
⊢ IsCompatible F.val U sf

Tactic:
intro i j

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
i j : ι
⊢ (ConcreteCategory.hom (F.val.map ((U i).infLELeft (U j)).op)) (sf i) =
    (ConcreteCategory.hom (F.val.map ((U i).infLERight (U j)).op)) (sf j)