internlm/Lean-Github huggingface dataset:
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case inr
B : Profinite
S : Presieve B
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
hFecs : EqualizerCondition F
hSSingle : S ∈ RegularSieve B
⊢ ∀ (y : Equalizer.FirstObj F S),
    Equalizer.Presieve.firstMap F S y = Equalizer.Presieve.secondMap F S y → ∃! x, Equalizer.forkMap F S x = y
Tactic:
intro y h
Proof state after:
case inr
B : Profinite
S : Presieve B
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
hFecs : EqualizerCondition F
hSSingle : S ∈ RegularSieve B
y : Equalizer.FirstObj F S
h : Equalizer.Presieve.firstMap F S y = Equalizer.Presieve.secondMap F S y
⊢ ∃! x, Equalizer.forkMap F S x = y
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case inr
B : Profinite
S : Presieve B
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
hFecs : EqualizerCondition F
hSSingle : S ∈ RegularSieve B
y : Equalizer.FirstObj F S
h : Equalizer.Presieve.firstMap F S y = Equalizer.Presieve.secondMap F S y
⊢ ∃! x, Equalizer.forkMap F S x = y
Tactic:
dsimp [RegularSieve] at hSSingle
Proof state after:
case inr
B : Profinite
S : Presieve B
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
hFecs : EqualizerCondition F
hSSingle : ∃ X f, (S = ofArrows (fun x => X) fun x => f) ∧ Epi f
y : Equalizer.FirstObj F S
h : Equalizer.Presieve.firstMap F S y = Equalizer.Presieve.secondMap F S y
⊢ ∃! x, Equalizer.forkMap F S x = y
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case inr
B : Profinite
S : Presieve B
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
hFecs : EqualizerCondition F
hSSingle : ∃ X f, (S = ofArrows (fun x => X) fun x => f) ∧ Epi f
y : Equalizer.FirstObj F S
h : Equalizer.Presieve.firstMap F S y = Equalizer.Presieve.secondMap F S y
⊢ ∃! x, Equalizer.forkMap F S x = y
Tactic:
obtain ⟨X, π, ⟨hS, πsurj⟩⟩ := hSSingle
Proof state after:
case inr.intro.intro.intro
B : Profinite
S : Presieve B
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
hFecs : EqualizerCondition F
y : Equalizer.FirstObj F S
h : Equalizer.Presieve.firstMap F S y = Equalizer.Presieve.secondMap F S y
X : Profinite
π : X ⟶ B
hS : S = ofArrows (fun x => X) fun x => π
πsurj : Epi π
⊢ ∃! x, Equalizer.forkMap F S x = y
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case inr.intro.intro.intro
B : Profinite
S : Presieve B
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
hFecs : EqualizerCondition F
y : Equalizer.FirstObj F S
h : Equalizer.Presieve.firstMap F S y = Equalizer.Presieve.secondMap F S y
X : Profinite
π : X ⟶ B
hS : S = ofArrows (fun x => X) fun x => π
πsurj : Epi π
⊢ ∃! x, Equalizer.forkMap F S x = y
Tactic:
rw [Presieve.ofArrows_pUnit] at hS
Proof state after:
case inr.intro.intro.intro
B : Profinite
S : Presieve B
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
hFecs : EqualizerCondition F
y : Equalizer.FirstObj F S
h : Equalizer.Presieve.firstMap F S y = Equalizer.Presieve.secondMap F S y
X : Profinite
π : X ⟶ B
hS : S = Presieve.singleton π
πsurj : Epi π
⊢ ∃! x, Equalizer.forkMap F S x = y
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case inr.intro.intro.intro
B : Profinite
S : Presieve B
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
hFecs : EqualizerCondition F
y : Equalizer.FirstObj F S
h : Equalizer.Presieve.firstMap F S y = Equalizer.Presieve.secondMap F S y
X : Profinite
π : X ⟶ B
hS : S = Presieve.singleton π
πsurj : Epi π
⊢ ∃! x, Equalizer.forkMap F S x = y
Tactic:
subst hS
Proof state after:
case inr.intro.intro.intro
B : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
hFecs : EqualizerCondition F
X : Profinite
π : X ⟶ B
πsurj : Epi π
y : Equalizer.FirstObj F (Presieve.singleton π)
h : Equalizer.Presieve.firstMap F (Presieve.singleton π) y = Equalizer.Presieve.secondMap F (Presieve.singleton π) y
⊢ ∃! x, Equalizer.forkMap F (Presieve.singleton π) x = y
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case inr.intro.intro.intro
B : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
hFecs : EqualizerCondition F
X : Profinite
π : X ⟶ B
πsurj : Epi π
y : Equalizer.FirstObj F (Presieve.singleton π)
h : Equalizer.Presieve.firstMap F (Presieve.singleton π) y = Equalizer.Presieve.secondMap F (Presieve.singleton π) y
⊢ ∃! x, Equalizer.forkMap F (Presieve.singleton π) x = y
Tactic:
rw [Profinite.epi_iff_surjective] at πsurj
Proof state after:
case inr.intro.intro.intro
B : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
hFecs : EqualizerCondition 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
⊢ ∃! x, Equalizer.forkMap F (Presieve.singleton π) x = y
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case inr.intro.intro.intro
B : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hFpfp : PreservesFiniteProducts F
hFecs : EqualizerCondition 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
⊢ ∃! x, Equalizer.forkMap F (Presieve.singleton π) x = y
Tactic:
specialize hFecs X B π πsurj
Proof state after:
case inr.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 π π ≫ π))
⊢ ∃! x, Equalizer.forkMap F (Presieve.singleton π) x = y
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case inr.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 π π ≫ π))
⊢ ∃! x, Equalizer.forkMap F (Presieve.singleton π) x = y
Tactic:
have fork_comp : Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom = 
    F.map π.op
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 π π ≫ π))
⊢ Equalizer.forkMap F (Presieve.singleton π) ≫ (EqualizerFirstObjIso F π).hom = F.map π.op

case inr.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
⊢ ∃! x, Equalizer.forkMap F (Presieve.singleton π) x = y
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case inr.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
⊢ ∃! x, Equalizer.forkMap F (Presieve.singleton π) x = y
Tactic:
have fmap_comp : (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.fst π π).op = 
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso 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
⊢ (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.fst π π).op =
    Equalizer.Presieve.firstMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso F π).hom

case inr.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
⊢ ∃! x, Equalizer.forkMap F (Presieve.singleton π) x = y
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case inr.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
⊢ ∃! x, Equalizer.forkMap F (Presieve.singleton π) x = y
Tactic:
have smap_comp : (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.snd π π).op = 
    Equalizer.Presieve.secondMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso 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
⊢ (EqualizerFirstObjIso F π).hom ≫ F.map (pullback.snd π π).op =
    Equalizer.Presieve.secondMap F (Presieve.singleton π) ≫ (EqualizerSecondObjIso F π).hom

case inr.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
⊢ ∃! x, Equalizer.forkMap F (Presieve.singleton π) x = y
Theorem: Profinite.isSheafFor_of_Dagur
Proof state before:
case inr.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)
uniq_F : ∃! x, F.map π.op x = (EqualizerFirstObjIso F π).hom y
⊢ ∃! x, Equalizer.forkMap F (Presieve.singleton π) x = y
Tactic:
obtain ⟨x,hx⟩ := uniq_F
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 :
  (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
⊢ ∃! x, Equalizer.forkMap F (Presieve.singleton π) x = y
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 :
  (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
⊢ ∃! x, Equalizer.forkMap F (Presieve.singleton π) x = y
Tactic:
dsimp at hx
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 :
  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
⊢ ∃! x, Equalizer.forkMap F (Presieve.singleton π) x = y
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 :
  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
⊢ ∃! x, Equalizer.forkMap F (Presieve.singleton π) x = y
Tactic:
rw [← fork_comp] at hx
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
⊢ ∃! x, Equalizer.forkMap F (Presieve.singleton π) x = y
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
⊢ ∃! x, Equalizer.forkMap F (Presieve.singleton π) x = y
Tactic:
use x
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
⊢ (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