internlm/Lean-Github huggingface dataset:
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
⊢ (fun x => Equalizer.forkMap F (Presieve.singleton π) x = y) x ∧
    ∀ (y_1 : F.obj B.op), (fun x => Equalizer.forkMap F (Presieve.singleton π) x = y) y_1 → y_1 = x
Tactic:
dsimp
Proof state after:
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
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case fork_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 π π ≫ π))
⊢ Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom = F.map π.op
Tactic:
dsimp [EqualizerFirstObjIso, Equalizer.forkMap]
Proof state after:
case fork_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 π π ≫ π))
⊢ ((Pi.lift fun f => F.map (↑f.snd).op) ≫
      (Equalizer.firstObjEqFamily F (Presieve.singleton π)).hom ≫ fun e => e π (_ : Presieve.singleton π π)) =
    F.map π.op
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case fork_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 π π ≫ π))
⊢ ((Pi.lift fun f => F.map (↑f.snd).op) ≫
      (Equalizer.firstObjEqFamily F (Presieve.singleton π)).hom ≫ fun e => e π (_ : Presieve.singleton π π)) =
    F.map π.op
Tactic:
ext b
Proof state after:
case fork_comp.h
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 π π ≫ π))
b : F.obj B.op
⊢ ((Pi.lift fun f => F.map (↑f.snd).op) ≫
        (Equalizer.firstObjEqFamily F (Presieve.singleton π)).hom ≫ fun e => e π (_ : Presieve.singleton π π))
      b =
    F.map π.op b
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case fork_comp.h
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 π π ≫ π))
b : F.obj B.op
⊢ ((Pi.lift fun f => F.map (↑f.snd).op) ≫
        (Equalizer.firstObjEqFamily F (Presieve.singleton π)).hom ≫ fun e => e π (_ : Presieve.singleton π π))
      b =
    F.map π.op b
Tactic:
simp only [types_comp_apply, Equalizer.firstObjEqFamily_hom, Types.pi_lift_π_apply]
Proof state after:
no goals
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case fmap_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
⊢ (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.fst π π).op =
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso F π).hom
Tactic:
dsimp [EqualizerSecondObjIso]
Proof state after:
case fmap_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
⊢ (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.fst π π).op =
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫
      (EqualizerSecondObjIso_aux F π).hom ≫ F.map (fromExplicit π π).op
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case fmap_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
⊢ (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.fst π π).op =
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫
      (EqualizerSecondObjIso_aux F π).hom ≫ F.map (fromExplicit π π).op
Tactic:
rw [Profinite.fst_comp_fromExplicit, op_comp, Functor.map_comp]
Proof state after:
case fmap_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
⊢ (EqualizerFirstObjIso F π).hom ≫ F.map Limits.pullback.fst.op ≫ F.map (fromExplicit π π).op =
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫
      (EqualizerSecondObjIso_aux F π).hom ≫ F.map (fromExplicit π π).op
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case fmap_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
⊢ (EqualizerFirstObjIso F π).hom ≫ F.map Limits.pullback.fst.op ≫ F.map (fromExplicit π π).op =
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫
      (EqualizerSecondObjIso_aux F π).hom ≫ F.map (fromExplicit π π).op
Tactic:
suffices : (EqualizerFirstObjIso F π).hom ≫ F.map Limits.pullback.fst.op = 
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫
    (EqualizerSecondObjIso_aux F π).hom
Proof state after:
case fmap_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
this :
  (EqualizerFirstObjIso F π).hom ≫ F.map Limits.pullback.fst.op =
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso_aux F π).hom
⊢ (EqualizerFirstObjIso F π).hom ≫ F.map Limits.pullback.fst.op ≫ F.map (fromExplicit π π).op =
    Equalizer.Presieve.firstMap 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
⊢ (EqualizerFirstObjIso F π).hom ≫ F.map Limits.pullback.fst.op =
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso_aux F π).hom
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
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
⊢ (EqualizerFirstObjIso F π).hom ≫ F.map Limits.pullback.fst.op =
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso_aux F π).hom
Tactic:
dsimp [EqualizerFirstObjIso, Equalizer.Presieve.firstMap, EqualizerSecondObjIso_aux]
Proof state after:
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
⊢ ((Equalizer.firstObjEqFamily F (Presieve.singleton π)).hom ≫ fun e => e π (_ : Presieve.singleton π π)) ≫
      F.map Limits.pullback.fst.op =
    (Pi.lift fun x => Pi.π (fun f => F.obj f.fst.op) x.fst ≫ F.map Limits.pullback.fst.op) ≫
      Pi.π (fun fg => F.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
        ({ fst := X, snd := { val := π, property := (_ : Presieve.singleton π π) } },
          { fst := X, snd := { val := π, property := (_ : Presieve.singleton π π) } })
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
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
⊢ ((Equalizer.firstObjEqFamily F (Presieve.singleton π)).hom ≫ fun e => e π (_ : Presieve.singleton π π)) ≫
      F.map Limits.pullback.fst.op =
    (Pi.lift fun x => Pi.π (fun f => F.obj f.fst.op) x.fst ≫ F.map Limits.pullback.fst.op) ≫
      Pi.π (fun fg => F.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
        ({ fst := X, snd := { val := π, property := (_ : Presieve.singleton π π) } },
          { fst := X, snd := { val := π, property := (_ : Presieve.singleton π π) } })
Tactic:
ext b
Proof state after:
case this.h
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
b : Equalizer.FirstObj F (Presieve.singleton π)
⊢ (((Equalizer.firstObjEqFamily F (Presieve.singleton π)).hom ≫ fun e => e π (_ : Presieve.singleton π π)) ≫
        F.map Limits.pullback.fst.op)
      b =
    ((Pi.lift fun x => Pi.π (fun f => F.obj f.fst.op) x.fst ≫ F.map Limits.pullback.fst.op) ≫
        Pi.π (fun fg => F.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
          ({ fst := X, snd := { val := π, property := (_ : Presieve.singleton π π) } },
            { fst := X, snd := { val := π, property := (_ : Presieve.singleton π π) } }))
      b
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case this.h
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
b : Equalizer.FirstObj F (Presieve.singleton π)
⊢ (((Equalizer.firstObjEqFamily F (Presieve.singleton π)).hom ≫ fun e => e π (_ : Presieve.singleton π π)) ≫
        F.map Limits.pullback.fst.op)
      b =
    ((Pi.lift fun x => Pi.π (fun f => F.obj f.fst.op) x.fst ≫ F.map Limits.pullback.fst.op) ≫
        Pi.π (fun fg => F.obj (Limits.pullback ↑fg.fst.snd ↑fg.snd.snd).op)
          ({ fst := X, snd := { val := π, property := (_ : Presieve.singleton π π) } },
            { fst := X, snd := { val := π, property := (_ : Presieve.singleton π π) } }))
      b
Tactic:
simp only [types_comp_apply, Equalizer.firstObjEqFamily_hom, Types.pi_lift_π_apply]
Proof state after:
no goals
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case fmap_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
this :
  (EqualizerFirstObjIso F π).hom ≫ F.map Limits.pullback.fst.op =
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso_aux F π).hom
⊢ (EqualizerFirstObjIso F π).hom ≫ F.map Limits.pullback.fst.op ≫ F.map (fromExplicit π π).op =
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫
      (EqualizerSecondObjIso_aux F π).hom ≫ F.map (fromExplicit π π).op
Tactic:
simp only [← Category.assoc]
Proof state after:
case fmap_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
this :
  (EqualizerFirstObjIso F π).hom ≫ F.map Limits.pullback.fst.op =
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso_aux F π).hom
⊢ ((EqualizerFirstObjIso F π).hom ≫ F.map Limits.pullback.fst.op) ≫ F.map (fromExplicit π π).op =
    (Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso_aux F π).hom) ≫
      F.map (fromExplicit π π).op
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case fmap_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
this :
  (EqualizerFirstObjIso F π).hom ≫ F.map Limits.pullback.fst.op =
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso_aux F π).hom
⊢ ((EqualizerFirstObjIso F π).hom ≫ F.map Limits.pullback.fst.op) ≫ F.map (fromExplicit π π).op =
    (Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso_aux F π).hom) ≫
      F.map (fromExplicit π π).op
Tactic:
rw [this]
Proof state after:
no goals
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 (pullback.snd π π).op =
    Equalizer.Presieve.secondMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso F π).hom
Tactic:
dsimp [EqualizerSecondObjIso]
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
⊢ (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.snd π π).op =
    Equalizer.Presieve.secondMap F (Presieve.singleton π) ≫
      (EqualizerSecondObjIso_aux F π).hom ≫ F.map (fromExplicit π π).op