C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
⊢ s = t
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
⊢ s = t
let sf : ∀ i : ι, F.1.obj (op (U i)) := fun i => F.1.map (Opens.leSupr U i).op s
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
sf_compatible : IsCompatible F.val U sf
⊢ s = t
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
⊢ s = t
have sf_compatible : IsCompatible _ U sf := by
  intro i j
  simp_rw [← comp_apply, ← F.1.map_comp]
  rfl
case intro.intro
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
sf_compatible : IsCompatible F.val U sf
gl : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
gl_uniq : ∀ (y : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)), (fun s => IsGluing F.val U sf s) y → y = gl
⊢ s = t
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
sf_compatible : IsCompatible F.val U sf
⊢ s = t
obtain ⟨gl, -, gl_uniq⟩ := F.existsUnique_gluing U sf sf_compatible
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
sf_compatible : IsCompatible F.val U sf
gl : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
gl_uniq : ∀ (y : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)), (fun s => IsGluing F.val U sf s) y → y = gl
⊢ s = gl

C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
sf_compatible : IsCompatible F.val U sf
gl : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
gl_uniq : ∀ (y : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)), (fun s => IsGluing F.val U sf s) y → y = gl
⊢ gl = t
case intro.intro
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
sf_compatible : IsCompatible F.val U sf
gl : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
gl_uniq : ∀ (y : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)), (fun s => IsGluing F.val U sf s) y → y = gl
⊢ s = t
trans gl
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
i j : ι
⊢ (CategoryTheory.forget C).map (F.val.map (infLELeft (U i) (U j)).op) (sf i) =
    (CategoryTheory.forget C).map (F.val.map (infLERight (U i) (U j)).op) (sf j)
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
⊢ IsCompatible F.val U sf
intro i j
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
i j : ι
⊢ (CategoryTheory.forget C).map (F.val.map ((leSupr U i).op ≫ (infLELeft (U i) (U j)).op)) s =
    (CategoryTheory.forget C).map (F.val.map ((leSupr U j).op ≫ (infLERight (U i) (U j)).op)) s
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
i j : ι
⊢ (CategoryTheory.forget C).map (F.val.map (infLELeft (U i) (U j)).op) (sf i) =
    (CategoryTheory.forget C).map (F.val.map (infLERight (U i) (U j)).op) (sf j)
simp_rw [← comp_apply, ← F.1.map_comp]
no goals
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
i j : ι
⊢ (CategoryTheory.forget C).map (F.val.map ((leSupr U i).op ≫ (infLELeft (U i) (U j)).op)) s =
    (CategoryTheory.forget C).map (F.val.map ((leSupr U j).op ≫ (infLERight (U i) (U j)).op)) s
rfl
case a
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
sf_compatible : IsCompatible F.val U sf
gl : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
gl_uniq : ∀ (y : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)), (fun s => IsGluing F.val U sf s) y → y = gl
⊢ IsGluing F.val U sf s
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
sf_compatible : IsCompatible F.val U sf
gl : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
gl_uniq : ∀ (y : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)), (fun s => IsGluing F.val U sf s) y → y = gl
⊢ s = gl
apply gl_uniq
case a
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
sf_compatible : IsCompatible F.val U sf
gl : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
gl_uniq : ∀ (y : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)), (fun s => IsGluing F.val U sf s) y → y = gl
i : ι
⊢ (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s = sf i
case a
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
sf_compatible : IsCompatible F.val U sf
gl : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
gl_uniq : ∀ (y : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)), (fun s => IsGluing F.val U sf s) y → y = gl
⊢ IsGluing F.val U sf s
intro i
no goals
case a
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
sf_compatible : IsCompatible F.val U sf
gl : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
gl_uniq : ∀ (y : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)), (fun s => IsGluing F.val U sf s) y → y = gl
i : ι
⊢ (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s = sf i
rfl
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
sf_compatible : IsCompatible F.val U sf
gl : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
gl_uniq : ∀ (y : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)), (fun s => IsGluing F.val U sf s) y → y = gl
⊢ t = gl
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
sf_compatible : IsCompatible F.val U sf
gl : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
gl_uniq : ∀ (y : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)), (fun s => IsGluing F.val U sf s) y → y = gl
⊢ gl = t
symm
case a
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
sf_compatible : IsCompatible F.val U sf
gl : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
gl_uniq : ∀ (y : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)), (fun s => IsGluing F.val U sf s) y → y = gl
⊢ IsGluing F.val U sf t
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
sf_compatible : IsCompatible F.val U sf
gl : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
gl_uniq : ∀ (y : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)), (fun s => IsGluing F.val U sf s) y → y = gl
⊢ t = gl
apply gl_uniq
case a
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
sf_compatible : IsCompatible F.val U sf
gl : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
gl_uniq : ∀ (y : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)), (fun s => IsGluing F.val U sf s) y → y = gl
i : ι
⊢ (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t = sf i
case a
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
sf_compatible : IsCompatible F.val U sf
gl : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
gl_uniq : ∀ (y : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)), (fun s => IsGluing F.val U sf s) y → y = gl
⊢ IsGluing F.val U sf t
intro i
no goals
case a
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
s t : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
h :
  ∀ (i : ι),
    (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s =
      (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t
sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (U i).op) :=
  fun i => (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) s
sf_compatible : IsCompatible F.val U sf
gl : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)
gl_uniq : ∀ (y : (CategoryTheory.forget C).obj (F.val.obj (iSup U).op)), (fun s => IsGluing F.val U sf s) y → y = gl
i : ι
⊢ (CategoryTheory.forget C).map (F.val.map (leSupr U i).op) t = sf i
rw [← h]