Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case uniq_F.intro
B : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
X : Profinite
π : X ⟶ B
πsurj : Function.Surjective ↑π
y : Equalizer.FirstObj F (Presieve.singleton π)
h : Equalizer.Presieve.firstMap F (Presieve.singleton π) y = Equalizer.Presieve.secondMap F (Presieve.singleton π) y
fork_comp : Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom = F.map π.op
fmap_comp :
  (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.fst π π).op =
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso F π).hom
smap_comp :
  (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.snd π π).op =
    Equalizer.Presieve.secondMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso F π).hom
iy_mem :
  F.map (pullback.fst π π).op ((EqualizerFirstObjIso F π).hom y) =
    F.map (pullback.snd π π).op ((EqualizerFirstObjIso F π).hom y)
x : F.obj B.op
hx :
  { val := F.map π.op x,
        property :=
          (_ : (F.map π.op ≫ F.map (pullback.fst π π).op) x = (F.map π.op ≫ F.map (pullback.snd π π).op) x) } =
      { val := (EqualizerFirstObjIso F π).hom y, property := iy_mem } ∧
    ∀ (y_1 : F.obj B.op),
      { val := F.map π.op y_1,
            property :=
              (_ : (F.map π.op ≫ F.map (pullback.fst π π).op) y_1 = (F.map π.op ≫ F.map (pullback.snd π π).op) y_1) } =
          { val := (EqualizerFirstObjIso F π).hom y, property := iy_mem } →
        y_1 = x
z : F.obj B.op
hz : F.map π.op z = (EqualizerFirstObjIso F π).hom y
⊢ z = x
Tactic:
apply hx.2
Proof state after:
case uniq_F.intro.a
B : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
X : Profinite
π : X ⟶ B
πsurj : Function.Surjective ↑π
y : Equalizer.FirstObj F (Presieve.singleton π)
h : Equalizer.Presieve.firstMap F (Presieve.singleton π) y = Equalizer.Presieve.secondMap F (Presieve.singleton π) y
fork_comp : Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom = F.map π.op
fmap_comp :
  (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.fst π π).op =
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso F π).hom
smap_comp :
  (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.snd π π).op =
    Equalizer.Presieve.secondMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso F π).hom
iy_mem :
  F.map (pullback.fst π π).op ((EqualizerFirstObjIso F π).hom y) =
    F.map (pullback.snd π π).op ((EqualizerFirstObjIso F π).hom y)
x : F.obj B.op
hx :
  { val := F.map π.op x,
        property :=
          (_ : (F.map π.op ≫ F.map (pullback.fst π π).op) x = (F.map π.op ≫ F.map (pullback.snd π π).op) x) } =
      { val := (EqualizerFirstObjIso F π).hom y, property := iy_mem } ∧
    ∀ (y_1 : F.obj B.op),
      { val := F.map π.op y_1,
            property :=
              (_ : (F.map π.op ≫ F.map (pullback.fst π π).op) y_1 = (F.map π.op ≫ F.map (pullback.snd π π).op) y_1) } =
          { val := (EqualizerFirstObjIso F π).hom y, property := iy_mem } →
        y_1 = x
z : F.obj B.op
hz : F.map π.op z = (EqualizerFirstObjIso F π).hom y
⊢ { val := F.map π.op z,
      property := (_ : (F.map π.op ≫ F.map (pullback.fst π π).op) z = (F.map π.op ≫ F.map (pullback.snd π π).op) z) } =
    { val := (EqualizerFirstObjIso F π).hom y, property := iy_mem }