internlm/Lean-Github huggingface dataset:
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
⊢ Equalizer.forkMap F S ≫ comparisoninv hS F =
    F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom
Tactic:
erw [this]
Proof state after:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
⊢ Equalizer.forkMap F S ≫ comparisoninv hS F = Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
⊢ Equalizer.forkMap F S ≫ comparisoninv hS F = Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
Tactic:
refine' funext (fun s => _)
Proof state after:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
⊢ (Equalizer.forkMap F S ≫ comparisoninv hS F) s = Pi.lift (fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op) s
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
⊢ (Equalizer.forkMap F S ≫ comparisoninv hS F) s = Pi.lift (fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op) s
Tactic:
simp only [types_comp_apply, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]
Proof state after:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
⊢ comparisoninv hS F (Equalizer.forkMap F S s) = Pi.lift (fun a => F.map (π a).op) s
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
⊢ comparisoninv hS F (Equalizer.forkMap F S s) = Pi.lift (fun a => F.map (π a).op) s
Tactic:
ext a
Proof state after:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ limit.π (Discrete.functor fun a => F.obj (Z a).op) a (comparisoninv hS F (Equalizer.forkMap F S s)) =
    limit.π (Discrete.functor fun a => F.obj (Z a).op) a (Pi.lift (fun a => F.map (π a).op) s)
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ limit.π (Discrete.functor fun a => F.obj (Z a).op) a (comparisoninv hS F (Equalizer.forkMap F S s)) =
    limit.π (Discrete.functor fun a => F.obj (Z a).op) a (Pi.lift (fun a => F.map (π a).op) s)
Tactic:
rw [Types.Limit.lift_π_apply]
Proof state after:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ limit.π (Discrete.functor fun a => F.obj (Z a).op) a (comparisoninv hS F (Equalizer.forkMap F S s)) =
    (Fan.mk (F.obj X.op) fun a => F.map (π a).op).π.app a s
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ limit.π (Discrete.functor fun a => F.obj (Z a).op) a (comparisoninv hS F (Equalizer.forkMap F S s)) =
    (Fan.mk (F.obj X.op) fun a => F.map (π a).op).π.app a s
Tactic:
dsimp [comparisoninv]
Proof state after:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ limit.π (Discrete.functor fun a => F.obj (Z a).op) a
      (Pi.lift (fun a => Pi.π (fun f => F.obj f.fst.op) (v hS a) ≫ F.map (𝟙 (v hS a).fst.op))
        (Equalizer.forkMap F S s)) =
    F.map (π a.as).op s
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ limit.π (Discrete.functor fun a => F.obj (Z a).op) a
      (Pi.lift (fun a => Pi.π (fun f => F.obj f.fst.op) (v hS a) ≫ F.map (𝟙 (v hS a).fst.op))
        (Equalizer.forkMap F S s)) =
    F.map (π a.as).op s
Tactic:
simp_rw [v.fst]
Proof state after:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ limit.π (Discrete.functor fun a => F.obj (Z a).op) a
      (Pi.lift (fun a => Pi.π (fun f => F.obj f.fst.op) (v hS a) ≫ F.map (𝟙 (Z a).op)) (Equalizer.forkMap F S s)) =
    F.map (π a.as).op s
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ limit.π (Discrete.functor fun a => F.obj (Z a).op) a
      (Pi.lift (fun a => Pi.π (fun f => F.obj f.fst.op) (v hS a) ≫ F.map (𝟙 (Z a).op)) (Equalizer.forkMap F S s)) =
    F.map (π a.as).op s
Tactic:
simp only [Functor.map_id, Category.comp_id]
Proof state after:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ limit.π (Discrete.functor fun a => F.obj (Z a).op) a
      (Pi.lift (fun a => Pi.π (fun f => F.obj f.fst.op) (v hS a)) (Equalizer.forkMap F S s)) =
    F.map (π a.as).op s
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ limit.π (Discrete.functor fun a => F.obj (Z a).op) a
      (Pi.lift (fun a => Pi.π (fun f => F.obj f.fst.op) (v hS a)) (Equalizer.forkMap F S s)) =
    F.map (π a.as).op s
Tactic:
rw [Types.Limit.lift_π_apply]
Proof state after:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ (Fan.mk (∏ fun f => F.obj f.fst.op) fun a => Pi.π (fun f => F.obj f.fst.op) (v hS a)).π.app a
      (Equalizer.forkMap F S s) =
    F.map (π a.as).op s
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ (Fan.mk (∏ fun f => F.obj f.fst.op) fun a => Pi.π (fun f => F.obj f.fst.op) (v hS a)).π.app a
      (Equalizer.forkMap F S s) =
    F.map (π a.as).op s
Tactic:
simp only [Fan.mk_pt, Equalizer.forkMap, Fan.mk_π_app, Types.pi_lift_π_apply, v.snd]
Proof state after:
no goals
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
⊢ F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
Tactic:
simp
Proof state after:
no goals
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
case intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
⊢ fromFirst hS hF HIso ≫ Equalizer.forkMap F S = 𝟙 (Equalizer.FirstObj F S)
Tactic:
refine' Limits.Pi.hom_ext _ _ (fun f => _)
Proof state after:
case intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
⊢ (fromFirst hS hF HIso ≫ Equalizer.forkMap F S) ≫ Pi.π (fun f => F.obj f.fst.op) f =
    𝟙 (Equalizer.FirstObj F S) ≫ Pi.π (fun f => F.obj f.fst.op) f
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
case intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
⊢ (fromFirst hS hF HIso ≫ Equalizer.forkMap F S) ≫ Pi.π (fun f => F.obj f.fst.op) f =
    𝟙 (Equalizer.FirstObj F S) ≫ Pi.π (fun f => F.obj f.fst.op) f
Tactic:
dsimp [Equalizer.forkMap]
Proof state after:
case intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
⊢ (fromFirst hS hF HIso ≫ Pi.lift fun f => F.map (↑f.snd).op) ≫ Pi.π (fun f => F.obj f.fst.op) f =
    𝟙 (Equalizer.FirstObj F S) ≫ Pi.π (fun f => F.obj f.fst.op) f
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
case intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
⊢ (fromFirst hS hF HIso ≫ Pi.lift fun f => F.map (↑f.snd).op) ≫ Pi.π (fun f => F.obj f.fst.op) f =
    𝟙 (Equalizer.FirstObj F S) ≫ Pi.π (fun f => F.obj f.fst.op) f
Tactic:
rw [Category.id_comp, Category.assoc, limit.lift_π, Limits.Fan.mk_π_app]
Proof state after:
case intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
⊢ fromFirst hS hF HIso ≫ F.map (↑{ as := f }.as.snd).op = Pi.π (fun f => F.obj f.fst.op) f
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
case intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
⊢ fromFirst hS hF HIso ≫ F.map (↑{ as := f }.as.snd).op = Pi.π (fun f => F.obj f.fst.op) f
Tactic:
simp only
Proof state after:
case intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
⊢ fromFirst hS hF HIso ≫ F.map (↑f.snd).op = Pi.π (fun f => F.obj f.fst.op) f
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
case intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
⊢ fromFirst hS hF HIso ≫ F.map (↑f.snd).op = Pi.π (fun f => F.obj f.fst.op) f
Tactic:
obtain ⟨a, ha⟩ := vsurj hS f
Proof state after:
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
a : α
ha : v hS a = f
⊢ fromFirst hS hF HIso ≫ F.map (↑f.snd).op = Pi.π (fun f => F.obj f.fst.op) f
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
a : α
ha : v hS a = f
⊢ fromFirst hS hF HIso ≫ F.map (↑f.snd).op = Pi.π (fun f => F.obj f.fst.op) f
Tactic:
unfold fromFirst
Proof state after:
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
a : α
ha : v hS a = f
⊢ (comparisoninv hS F ≫
        (PreservesProduct.iso F fun a => (Z a).op).inv ≫ F.map (CoprodToProd Z).inv ≫ F.map (inv (Sigma.desc π).op)) ≫
      F.map (↑f.snd).op =
    Pi.π (fun f => F.obj f.fst.op) f
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
a : α
ha : v hS a = f
⊢ (comparisoninv hS F ≫
        (PreservesProduct.iso F fun a => (Z a).op).inv ≫ F.map (CoprodToProd Z).inv ≫ F.map (inv (Sigma.desc π).op)) ≫
      F.map (↑f.snd).op =
    Pi.π (fun f => F.obj f.fst.op) f
Tactic:
simp only [Category.assoc]
Proof state after:
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
a : α
ha : v hS a = f
⊢ comparisoninv hS F ≫
      (PreservesProduct.iso F fun a => (Z a).op).inv ≫
        F.map (CoprodToProd Z).inv ≫ F.map (inv (Sigma.desc π).op) ≫ F.map (↑f.snd).op =
    Pi.π (fun f => F.obj f.fst.op) f