Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case smap_comp
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
hFecs :
  Function.Bijective
    (MapToEqualizer F π (pullback.fst π π) (pullback.snd π π) (_ : pullback.fst π π ≫ π = pullback.snd π π ≫ π))
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
⊢ (EqualizerFirstObjIso F π).hom ≫ F.map Limits.pullback.snd.op ≫ F.map (fromExplicit π π).op =
    Equalizer.Presieve.secondMap F (Presieve.singleton π) ≫
      (EqualizerSecondObjIso_aux F π).hom ≫ F.map (fromExplicit π π).op
Tactic:
suffices : (EqualizerFirstObjIso F π).hom ≫ F.map Limits.pullback.snd.op = 
    Equalizer.Presieve.secondMap F (Presieve.singleton π) ≫
    (EqualizerSecondObjIso_aux F π).hom
Proof state after:
case smap_comp
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
hFecs :
  Function.Bijective
    (MapToEqualizer F π (pullback.fst π π) (pullback.snd π π) (_ : pullback.fst π π ≫ π = pullback.snd π π ≫ π))
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
this :
  (EqualizerFirstObjIso F π).hom ≫ F.map Limits.pullback.snd.op =
    Equalizer.Presieve.secondMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso_aux F π).hom
⊢ (EqualizerFirstObjIso F π).hom ≫ F.map Limits.pullback.snd.op ≫ F.map (fromExplicit π π).op =
    Equalizer.Presieve.secondMap F (Presieve.singleton π) ≫
      (EqualizerSecondObjIso_aux F π).hom ≫ F.map (fromExplicit π π).op

case this
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
hFecs :
  Function.Bijective
    (MapToEqualizer F π (pullback.fst π π) (pullback.snd π π) (_ : pullback.fst π π ≫ π = pullback.snd π π ≫ π))
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
⊢ (EqualizerFirstObjIso F π).hom ≫ F.map Limits.pullback.snd.op =
    Equalizer.Presieve.secondMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso_aux F π).hom