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 :
  (fun a =>
        MapToEqualizer F π (pullback.fst π π) (pullback.snd π π) (_ : pullback.fst π π ≫ π = pullback.snd π π ≫ π) a =
          { val := (EqualizerFirstObjIso F π).hom y, property := iy_mem })
      x ∧
    ∀ (y_1 : F.obj B.op),
      (fun a =>
            MapToEqualizer F π (pullback.fst π π) (pullback.snd π π) (_ : pullback.fst π π ≫ π = pullback.snd π π ≫ π)
                a =
              { val := (EqualizerFirstObjIso F π).hom y, property := iy_mem })
          y_1 →
        y_1 = x
⊢ (fun x => F.map π.op x = (EqualizerFirstObjIso F π).hom y) x ∧
    ∀ (y_1 : F.obj B.op), (fun x => F.map π.op x = (EqualizerFirstObjIso F π).hom y) y_1 → y_1 = x
Tactic:
dsimp [MapToEqualizer] at *
Proof state after:
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
⊢ F.map π.op x = (EqualizerFirstObjIso F π).hom y ∧
    ∀ (y_1 : F.obj B.op), F.map π.op y_1 = (EqualizerFirstObjIso F π).hom y → y_1 = x