Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case inr.intro.intro.intro.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
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
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 :
  (Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom) x = (EqualizerFirstObjIso F π).hom y ∧
    ∀ (y_1 : F.obj B.op),
      (Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom) y_1 =
          (EqualizerFirstObjIso F π).hom y →
        y_1 = x
⊢ Equalizer.forkMap F (Presieve.singleton π) x = y ∧
    ∀ (y_1 : F.obj B.op), Equalizer.forkMap F (Presieve.singleton π) y_1 = y → y_1 = x
Tactic:
constructor
Proof state after:
case inr.intro.intro.intro.intro.left
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
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 :
  (Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom) x = (EqualizerFirstObjIso F π).hom y ∧
    ∀ (y_1 : F.obj B.op),
      (Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom) y_1 =
          (EqualizerFirstObjIso F π).hom y →
        y_1 = x
⊢ Equalizer.forkMap F (Presieve.singleton π) x = y

case inr.intro.intro.intro.intro.right
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
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 :
  (Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom) x = (EqualizerFirstObjIso F π).hom y ∧
    ∀ (y_1 : F.obj B.op),
      (Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom) y_1 =
          (EqualizerFirstObjIso F π).hom y →
        y_1 = x
⊢ ∀ (y_1 : F.obj B.op), Equalizer.forkMap F (Presieve.singleton π) y_1 = y → y_1 = x