C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι : Type v
U : ι → Opens ↑X
Fsh : IsSheafUniqueGluing F
⊢ IsSheafEqualizerProducts F
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι : Type v
U : ι → Opens ↑X
Fsh : IsSheafUniqueGluing F
⊢ IsSheaf F
rw [isSheaf_iff_isSheafEqualizerProducts]
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
⊢ Nonempty (IsLimit (fork F U))
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι : Type v
U : ι → Opens ↑X
Fsh : IsSheafUniqueGluing F
⊢ IsSheafEqualizerProducts F
intro ι U
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
⊢ (s : Fork (leftRes F U) (rightRes F U)) →
    { l //
      l ≫ Fork.ι (fork F U) = Fork.ι s ∧
        ∀
          {m :
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
              ((Functor.const WalkingParallelPair).obj (fork F U).pt).obj WalkingParallelPair.zero},
          m ≫ Fork.ι (fork F U) = Fork.ι s → m = l }
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
⊢ Nonempty (IsLimit (fork F U))
refine' ⟨Fork.IsLimit.mk' _ _⟩
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
⊢ { l //
    l ≫ Fork.ι (fork F U) = Fork.ι s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
            ((Functor.const WalkingParallelPair).obj (fork F U).pt).obj WalkingParallelPair.zero},
        m ≫ Fork.ι (fork F U) = Fork.ι s → m = l }
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
⊢ (s : Fork (leftRes F U) (rightRes F U)) →
    { l //
      l ≫ Fork.ι (fork F U) = Fork.ι s ∧
        ∀
          {m :
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
              ((Functor.const WalkingParallelPair).obj (fork F U).pt).obj WalkingParallelPair.zero},
          m ≫ Fork.ι (fork F U) = Fork.ι s → m = l }
intro s
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
h_compatible : ∀ (x : s.pt), IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
⊢ { l //
    l ≫ Fork.ι (fork F U) = Fork.ι s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
            ((Functor.const WalkingParallelPair).obj (fork F U).pt).obj WalkingParallelPair.zero},
        m ≫ Fork.ι (fork F U) = Fork.ι s → m = l }
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
⊢ { l //
    l ≫ Fork.ι (fork F U) = Fork.ι s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
            ((Functor.const WalkingParallelPair).obj (fork F U).pt).obj WalkingParallelPair.zero},
        m ≫ Fork.ι (fork F U) = Fork.ι s → m = l }
have h_compatible :
  ∀ x : s.pt, F.IsCompatible U ((F.piOpensIsoSectionsFamily U).hom (s.ι x)) := by
  intro x
  rw [compatible_iff_leftRes_eq_rightRes]
  convert congr_fun s.condition x
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
h_compatible : ∀ (x : s.pt), IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
m : s.pt → (forget (Type v)).obj (F.obj (iSup U).op)
m_spec : ∀ (x : s.pt), (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) (m x)
m_uniq :
  ∀ (x : s.pt) (y : (forget (Type v)).obj (F.obj (iSup U).op)),
    (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) y → y = m x
⊢ { l //
    l ≫ Fork.ι (fork F U) = Fork.ι s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
            ((Functor.const WalkingParallelPair).obj (fork F U).pt).obj WalkingParallelPair.zero},
        m ≫ Fork.ι (fork F U) = Fork.ι s → m = l }
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
h_compatible : ∀ (x : s.pt), IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
⊢ { l //
    l ≫ Fork.ι (fork F U) = Fork.ι s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
            ((Functor.const WalkingParallelPair).obj (fork F U).pt).obj WalkingParallelPair.zero},
        m ≫ Fork.ι (fork F U) = Fork.ι s → m = l }
choose m m_spec m_uniq using fun x : s.pt =>
  Fsh U ((piOpensIsoSectionsFamily F U).hom (s.ι x)) (h_compatible x)
case refine'_1
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
h_compatible : ∀ (x : s.pt), IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
m : s.pt → (forget (Type v)).obj (F.obj (iSup U).op)
m_spec : ∀ (x : s.pt), (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) (m x)
m_uniq :
  ∀ (x : s.pt) (y : (forget (Type v)).obj (F.obj (iSup U).op)),
    (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) y → y = m x
⊢ m ≫ Fork.ι (fork F U) = Fork.ι s

case refine'_2
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
h_compatible : ∀ (x : s.pt), IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
m : s.pt → (forget (Type v)).obj (F.obj (iSup U).op)
m_spec : ∀ (x : s.pt), (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) (m x)
m_uniq :
  ∀ (x : s.pt) (y : (forget (Type v)).obj (F.obj (iSup U).op)),
    (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) y → y = m x
⊢ ∀
    {m_1 :
      ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
        ((Functor.const WalkingParallelPair).obj (fork F U).pt).obj WalkingParallelPair.zero},
    m_1 ≫ Fork.ι (fork F U) = Fork.ι s → m_1 = m
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
h_compatible : ∀ (x : s.pt), IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
m : s.pt → (forget (Type v)).obj (F.obj (iSup U).op)
m_spec : ∀ (x : s.pt), (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) (m x)
m_uniq :
  ∀ (x : s.pt) (y : (forget (Type v)).obj (F.obj (iSup U).op)),
    (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) y → y = m x
⊢ { l //
    l ≫ Fork.ι (fork F U) = Fork.ι s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
            ((Functor.const WalkingParallelPair).obj (fork F U).pt).obj WalkingParallelPair.zero},
        m ≫ Fork.ι (fork F U) = Fork.ι s → m = l }
refine' ⟨m, _, _⟩
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
x : s.pt
⊢ IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
⊢ ∀ (x : s.pt), IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
intro x
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
x : s.pt
⊢ leftRes F U (Fork.ι s x) = rightRes F U (Fork.ι s x)
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
x : s.pt
⊢ IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
rw [compatible_iff_leftRes_eq_rightRes]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
x : s.pt
⊢ leftRes F U (Fork.ι s x) = rightRes F U (Fork.ι s x)
convert congr_fun s.condition x
case refine'_1
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
h_compatible : ∀ (x : s.pt), IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
m : s.pt → (forget (Type v)).obj (F.obj (iSup U).op)
m_spec : ∀ (x : s.pt), (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) (m x)
m_uniq :
  ∀ (x : s.pt) (y : (forget (Type v)).obj (F.obj (iSup U).op)),
    (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) y → y = m x
x✝ : Discrete ι
i : ι
x : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero
⊢ ((m ≫ Fork.ι (fork F U)) ≫ limit.π (Discrete.functor fun i => F.obj (U i).op) { as := i }) x =
    (Fork.ι s ≫ limit.π (Discrete.functor fun i => F.obj (U i).op) { as := i }) x
case refine'_1
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
h_compatible : ∀ (x : s.pt), IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
m : s.pt → (forget (Type v)).obj (F.obj (iSup U).op)
m_spec : ∀ (x : s.pt), (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) (m x)
m_uniq :
  ∀ (x : s.pt) (y : (forget (Type v)).obj (F.obj (iSup U).op)),
    (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) y → y = m x
⊢ m ≫ Fork.ι (fork F U) = Fork.ι s
refine limit.hom_ext fun ⟨i⟩ => funext fun x => ?_
case refine'_1
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
h_compatible : ∀ (x : s.pt), IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
m : s.pt → (forget (Type v)).obj (F.obj (iSup U).op)
m_spec : ∀ (x : s.pt), (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) (m x)
m_uniq :
  ∀ (x : s.pt) (y : (forget (Type v)).obj (F.obj (iSup U).op)),
    (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) y → y = m x
x✝ : Discrete ι
i : ι
x : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero
⊢ F.map (leSupr U i).op (m x) = limit.π (Discrete.functor fun i => F.obj (U i).op) { as := i } (Fork.ι s x)
case refine'_1
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
h_compatible : ∀ (x : s.pt), IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
m : s.pt → (forget (Type v)).obj (F.obj (iSup U).op)
m_spec : ∀ (x : s.pt), (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) (m x)
m_uniq :
  ∀ (x : s.pt) (y : (forget (Type v)).obj (F.obj (iSup U).op)),
    (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) y → y = m x
x✝ : Discrete ι
i : ι
x : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero
⊢ ((m ≫ Fork.ι (fork F U)) ≫ limit.π (Discrete.functor fun i => F.obj (U i).op) { as := i }) x =
    (Fork.ι s ≫ limit.π (Discrete.functor fun i => F.obj (U i).op) { as := i }) x
simp [res]
no goals
case refine'_1
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
h_compatible : ∀ (x : s.pt), IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
m : s.pt → (forget (Type v)).obj (F.obj (iSup U).op)
m_spec : ∀ (x : s.pt), (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) (m x)
m_uniq :
  ∀ (x : s.pt) (y : (forget (Type v)).obj (F.obj (iSup U).op)),
    (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) y → y = m x
x✝ : Discrete ι
i : ι
x : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero
⊢ F.map (leSupr U i).op (m x) = limit.π (Discrete.functor fun i => F.obj (U i).op) { as := i } (Fork.ι s x)
exact m_spec x i
case refine'_2
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
h_compatible : ∀ (x : s.pt), IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
m : s.pt → (forget (Type v)).obj (F.obj (iSup U).op)
m_spec : ∀ (x : s.pt), (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) (m x)
m_uniq :
  ∀ (x : s.pt) (y : (forget (Type v)).obj (F.obj (iSup U).op)),
    (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) y → y = m x
l :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (fork F U).pt).obj WalkingParallelPair.zero
hl : l ≫ Fork.ι (fork F U) = Fork.ι s
⊢ l = m
case refine'_2
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
h_compatible : ∀ (x : s.pt), IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
m : s.pt → (forget (Type v)).obj (F.obj (iSup U).op)
m_spec : ∀ (x : s.pt), (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) (m x)
m_uniq :
  ∀ (x : s.pt) (y : (forget (Type v)).obj (F.obj (iSup U).op)),
    (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) y → y = m x
⊢ ∀
    {m_1 :
      ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
        ((Functor.const WalkingParallelPair).obj (fork F U).pt).obj WalkingParallelPair.zero},
    m_1 ≫ Fork.ι (fork F U) = Fork.ι s → m_1 = m
intro l hl
case refine'_2.h
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
h_compatible : ∀ (x : s.pt), IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
m : s.pt → (forget (Type v)).obj (F.obj (iSup U).op)
m_spec : ∀ (x : s.pt), (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) (m x)
m_uniq :
  ∀ (x : s.pt) (y : (forget (Type v)).obj (F.obj (iSup U).op)),
    (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) y → y = m x
l :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (fork F U).pt).obj WalkingParallelPair.zero
hl : l ≫ Fork.ι (fork F U) = Fork.ι s
x : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero
⊢ l x = m x
case refine'_2
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
h_compatible : ∀ (x : s.pt), IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
m : s.pt → (forget (Type v)).obj (F.obj (iSup U).op)
m_spec : ∀ (x : s.pt), (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) (m x)
m_uniq :
  ∀ (x : s.pt) (y : (forget (Type v)).obj (F.obj (iSup U).op)),
    (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) y → y = m x
l :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (fork F U).pt).obj WalkingParallelPair.zero
hl : l ≫ Fork.ι (fork F U) = Fork.ι s
⊢ l = m
ext x
case refine'_2.h.a
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
h_compatible : ∀ (x : s.pt), IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
m : s.pt → (forget (Type v)).obj (F.obj (iSup U).op)
m_spec : ∀ (x : s.pt), (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) (m x)
m_uniq :
  ∀ (x : s.pt) (y : (forget (Type v)).obj (F.obj (iSup U).op)),
    (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) y → y = m x
l :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (fork F U).pt).obj WalkingParallelPair.zero
hl : l ≫ Fork.ι (fork F U) = Fork.ι s
x : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero
⊢ IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) (l x)
case refine'_2.h
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
h_compatible : ∀ (x : s.pt), IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
m : s.pt → (forget (Type v)).obj (F.obj (iSup U).op)
m_spec : ∀ (x : s.pt), (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) (m x)
m_uniq :
  ∀ (x : s.pt) (y : (forget (Type v)).obj (F.obj (iSup U).op)),
    (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) y → y = m x
l :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (fork F U).pt).obj WalkingParallelPair.zero
hl : l ≫ Fork.ι (fork F U) = Fork.ι s
x : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero
⊢ l x = m x
apply m_uniq
case refine'_2.h.a
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
h_compatible : ∀ (x : s.pt), IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
m : s.pt → (forget (Type v)).obj (F.obj (iSup U).op)
m_spec : ∀ (x : s.pt), (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) (m x)
m_uniq :
  ∀ (x : s.pt) (y : (forget (Type v)).obj (F.obj (iSup U).op)),
    (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) y → y = m x
l :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (fork F U).pt).obj WalkingParallelPair.zero
hl : l ≫ Fork.ι (fork F U) = Fork.ι s
x : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero
⊢ res F U (l x) = Fork.ι s x
case refine'_2.h.a
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
h_compatible : ∀ (x : s.pt), IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
m : s.pt → (forget (Type v)).obj (F.obj (iSup U).op)
m_spec : ∀ (x : s.pt), (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) (m x)
m_uniq :
  ∀ (x : s.pt) (y : (forget (Type v)).obj (F.obj (iSup U).op)),
    (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) y → y = m x
l :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (fork F U).pt).obj WalkingParallelPair.zero
hl : l ≫ Fork.ι (fork F U) = Fork.ι s
x : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero
⊢ IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) (l x)
rw [isGluing_iff_eq_res]
no goals
case refine'_2.h.a
C : Type u
inst✝¹ : Category C
inst✝ : ConcreteCategory C
X : TopCat
F : Presheaf (Type v) X
ι✝ : Type v
U✝ : ι✝ → Opens ↑X
Fsh : IsSheafUniqueGluing F
ι : Type v
U : ι → Opens ↑X
s : Fork (leftRes F U) (rightRes F U)
h_compatible : ∀ (x : s.pt), IsCompatible F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x))
m : s.pt → (forget (Type v)).obj (F.obj (iSup U).op)
m_spec : ∀ (x : s.pt), (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) (m x)
m_uniq :
  ∀ (x : s.pt) (y : (forget (Type v)).obj (F.obj (iSup U).op)),
    (fun s_1 => IsGluing F U ((piOpensIsoSectionsFamily F U).hom (Fork.ι s x)) s_1) y → y = m x
l :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (fork F U).pt).obj WalkingParallelPair.zero
hl : l ≫ Fork.ι (fork F U) = Fork.ι s
x : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero
⊢ res F U (l x) = Fork.ι s x
exact congr_fun hl x