internlm/Lean-Github huggingface dataset:
Theorem: ExtrDisc.Sheaf.isSheafOfIsColimit
Proof state before:
A : Type (u + 2)
inst✝³ : Category A
inst✝² : HasZeroMorphisms A
inst✝¹ : HasFiniteBiproducts A
J : Type (u + 1)
inst✝ : SmallCategory J
F✝ : J ⥤ ExtrDiscᵒᵖ ⥤ A
F : J ⥤ Sheaf (coherentTopology ExtrDisc) A
S : Cocone (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
hS : IsColimit S
this : HasColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
e : S.pt ≅ colimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A) :=
  IsColimit.coconePointUniqueUpToIso hS (colimit.isColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A))
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) S.pt
Tactic:
rw [Presheaf.isSheaf_of_iso_iff e]
Proof state after:
A : Type (u + 2)
inst✝³ : Category A
inst✝² : HasZeroMorphisms A
inst✝¹ : HasFiniteBiproducts A
J : Type (u + 1)
inst✝ : SmallCategory J
F✝ : J ⥤ ExtrDiscᵒᵖ ⥤ A
F : J ⥤ Sheaf (coherentTopology ExtrDisc) A
S : Cocone (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
hS : IsColimit S
this : HasColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
e : S.pt ≅ colimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A) :=
  IsColimit.coconePointUniqueUpToIso hS (colimit.isColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A))
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) (colimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A))
Theorem: ExtrDisc.Sheaf.isSheafOfIsColimit
Proof state before:
A : Type (u + 2)
inst✝³ : Category A
inst✝² : HasZeroMorphisms A
inst✝¹ : HasFiniteBiproducts A
J : Type (u + 1)
inst✝ : SmallCategory J
F✝ : J ⥤ ExtrDiscᵒᵖ ⥤ A
F : J ⥤ Sheaf (coherentTopology ExtrDisc) A
S : Cocone (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
hS : IsColimit S
this : HasColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A)
e : S.pt ≅ colimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A) :=
  IsColimit.coconePointUniqueUpToIso hS (colimit.isColimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A))
⊢ Presheaf.IsSheaf (coherentTopology ExtrDisc) (colimit (F ⋙ sheafToPresheaf (coherentTopology ExtrDisc) A))
Tactic:
apply isSheafColimit
Proof state after:
no goals
Theorem: ExtrDisc.toFiniteCoproductCompFromFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
⊢ toFiniteCoproduct Z ≫ fromFiniteCoproduct Z = 𝟙 (∐ Z)
Tactic:
ext
Proof state after:
case h.w
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
b✝ : α
x✝ : (forget ExtrDisc).obj (Z b✝)
⊢ ↑(Sigma.ι Z b✝ ≫ toFiniteCoproduct Z ≫ fromFiniteCoproduct Z) x✝ = ↑(Sigma.ι Z b✝ ≫ 𝟙 (∐ Z)) x✝
Theorem: ExtrDisc.toFiniteCoproductCompFromFiniteCoproduct
Proof state before:
case h.w
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
b✝ : α
x✝ : (forget ExtrDisc).obj (Z b✝)
⊢ ↑(Sigma.ι Z b✝ ≫ toFiniteCoproduct Z ≫ fromFiniteCoproduct Z) x✝ = ↑(Sigma.ι Z b✝ ≫ 𝟙 (∐ Z)) x✝
Tactic:
simp [toFiniteCoproduct, fromFiniteCoproduct]
Proof state after:
no goals
Theorem: ExtrDisc.FromFiniteCoproductComptToFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
⊢ fromFiniteCoproduct Z ≫ toFiniteCoproduct Z = 𝟙 (finiteCoproduct Z)
Tactic:
refine' finiteCoproduct.hom_ext _ _ _ (fun a => _)
Proof state after:
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
⊢ finiteCoproduct.ι Z a ≫ fromFiniteCoproduct Z ≫ toFiniteCoproduct Z = finiteCoproduct.ι Z a ≫ 𝟙 (finiteCoproduct Z)
Theorem: ExtrDisc.FromFiniteCoproductComptToFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
⊢ finiteCoproduct.ι Z a ≫ fromFiniteCoproduct Z ≫ toFiniteCoproduct Z = finiteCoproduct.ι Z a ≫ 𝟙 (finiteCoproduct Z)
Tactic:
simp [toFiniteCoproduct, fromFiniteCoproduct]
Proof state after:
no goals
Theorem: ExtrDisc.IsIsotoFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
⊢ toFiniteCoproduct Z ≫ fromFiniteCoproduct Z = 𝟙 (∐ Z)
Tactic:
simp
Proof state after:
no goals
Theorem: ExtrDisc.IsIsotoFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
⊢ fromFiniteCoproduct Z ≫ toFiniteCoproduct Z = 𝟙 (finiteCoproduct Z)
Tactic:
simp
Proof state after:
no goals
Theorem: ExtrDisc.IsIsofromFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
⊢ fromFiniteCoproduct Z ≫ toFiniteCoproduct Z = 𝟙 (finiteCoproduct Z)
Tactic:
simp
Proof state after:
no goals
Theorem: ExtrDisc.IsIsofromFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
⊢ toFiniteCoproduct Z ≫ fromFiniteCoproduct Z = 𝟙 (∐ Z)
Tactic:
simp
Proof state after:
no goals
Theorem: ExtrDisc.Sigma.ιCompToFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
⊢ Sigma.ι Z a ≫ toFiniteCoproduct Z = finiteCoproduct.ι Z a
Tactic:
simp [toFiniteCoproduct]
Proof state after:
no goals
Theorem: ExtrDisc.finiteCoproduct.ιCompFromFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
⊢ ι Z a ≫ fromFiniteCoproduct Z = Sigma.ι Z a
Tactic:
simp [fromFiniteCoproduct]
Proof state after:
no goals
Theorem: ExtrDisc.finiteCoproduct.ιOpenEmbedding
Proof state before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
⊢ OpenEmbedding ↑(ι Z a)
Tactic:
exact openEmbedding_sigmaMk (σ := fun a => (Z a))
Proof state after:
no goals
Theorem: ExtrDisc.openEmbedding_ι
Proof state before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
⊢ OpenEmbedding ↑(Sigma.ι Z a)
Tactic:
refine' OpenEmbedding.of_comp _ (toFiniteCoproduct.OpenEmbedding Z) _
Proof state after:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
⊢ OpenEmbedding (↑(toFiniteCoproductHomeo Z) ∘ ↑(Sigma.ι Z a))
Theorem: ExtrDisc.openEmbedding_ι
Proof state before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
⊢ OpenEmbedding (↑(toFiniteCoproductHomeo Z) ∘ ↑(Sigma.ι Z a))
Tactic:
convert finiteCoproduct.ιOpenEmbedding Z a
Proof state after:
case h.e'_5
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
⊢ ↑(toFiniteCoproductHomeo Z) ∘ ↑(Sigma.ι Z a) = ↑(finiteCoproduct.ι Z a)
Theorem: ExtrDisc.openEmbedding_ι
Proof state before:
case h.e'_5
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
⊢ ↑(toFiniteCoproductHomeo Z) ∘ ↑(Sigma.ι Z a) = ↑(finiteCoproduct.ι Z a)
Tactic:
ext x
Proof state after:
case h.e'_5.h
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
x : CoeSort.coe (Z a)
⊢ (↑(toFiniteCoproductHomeo Z) ∘ ↑(Sigma.ι Z a)) x = ↑(finiteCoproduct.ι Z a) x
Theorem: ExtrDisc.openEmbedding_ι
Proof state before:
case h.e'_5.h
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
x : CoeSort.coe (Z a)
⊢ (↑(toFiniteCoproductHomeo Z) ∘ ↑(Sigma.ι Z a)) x = ↑(finiteCoproduct.ι Z a) x
Tactic:
change ((Sigma.ι Z a) ≫ toFiniteCoproduct Z) x = _
Proof state after:
case h.e'_5.h
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
x : CoeSort.coe (Z a)
⊢ ↑(Sigma.ι Z a ≫ toFiniteCoproduct Z) x = ↑(finiteCoproduct.ι Z a) x
Theorem: ExtrDisc.openEmbedding_ι
Proof state before:
case h.e'_5.h
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
x : CoeSort.coe (Z a)
⊢ ↑(Sigma.ι Z a ≫ toFiniteCoproduct Z) x = ↑(finiteCoproduct.ι Z a) x
Tactic:
simp
Proof state after:
no goals
Theorem: CategoryTheory.isPullbackSieve_ExtensiveSieve
Proof state before:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
⊢ isPullbackPresieve S
Tactic:
rcases hS with ⟨α, _, Z, π, hS, HIso⟩
Proof state after:
case intro.intro.intro.intro.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
⊢ isPullbackPresieve S
Theorem: CategoryTheory.isPullbackSieve_ExtensiveSieve
Proof state before:
case intro.intro.intro.intro.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
⊢ isPullbackPresieve S
Tactic:
intro Y₁ Y₂ f hf g hg
Proof state after:
case intro.intro.intro.intro.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
Y₁ Y₂ : C
f : Y₁ ⟶ X
hf : S f
g : Y₂ ⟶ X
hg : S g
⊢ HasPullback f g
Theorem: CategoryTheory.isPullbackSieve_ExtensiveSieve
Proof state before:
case intro.intro.intro.intro.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
Y₁ Y₂ : C
f : Y₁ ⟶ X
hf : S f
g : Y₂ ⟶ X
hg : S g
⊢ HasPullback f g
Tactic:
rw [hS] at hf hg
Proof state after:
case intro.intro.intro.intro.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
Y₁ Y₂ : C
f : Y₁ ⟶ X
hf : Presieve.ofArrows Z π f
g : Y₂ ⟶ X
hg : Presieve.ofArrows Z π g
⊢ HasPullback f g
Theorem: CategoryTheory.isPullbackSieve_ExtensiveSieve
Proof state before:
case intro.intro.intro.intro.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
Y₁ Y₂ : C
f : Y₁ ⟶ X
hf : Presieve.ofArrows Z π f
g : Y₂ ⟶ X
hg : Presieve.ofArrows Z π g
⊢ HasPullback f g
Tactic:
cases' hg with b
Proof state after:
case intro.intro.intro.intro.intro.mk
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
Y₁ : C
f : Y₁ ⟶ X
hf : Presieve.ofArrows Z π f
b : α
⊢ HasPullback f (π b)
Theorem: CategoryTheory.isPullbackSieve_ExtensiveSieve
Proof state before:
case intro.intro.intro.intro.intro.mk
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
Y₁ : C
f : Y₁ ⟶ X
hf : Presieve.ofArrows Z π f
b : α
⊢ HasPullback f (π b)
Tactic:
apply HasPullbackOfIsIsodesc.HasPullback f
Proof state after:
no goals
Theorem: CategoryTheory.vsurj
Proof state before:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
α : Type
Z : α → C
X : C
π : (a : α) → Z a ⟶ X
S : Presieve X
hS : S = Presieve.ofArrows Z π
x✝ : (Y : C) × { f // S f }
Y : C
f : Y ⟶ X
hf : S f
⊢ ∃ a, v hS a = { fst := Y, snd := { val := f, property := hf } }
Tactic:
cases' (hS ▸ hf) with a h
Proof state after:
case mk
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
α : Type
Z : α → C
X : C
π : (a : α) → Z a ⟶ X
S : Presieve X
hS : S = Presieve.ofArrows Z π
x✝ : (Y : C) × { f // S f }
a : α
hf : S (π a)
⊢ ∃ a_1, v hS a_1 = { fst := Z a, snd := { val := π a, property := hf } }
Theorem: CategoryTheory.vsurj
Proof state before:
case mk
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
α : Type
Z : α → C
X : C
π : (a : α) → Z a ⟶ X
S : Presieve X
hS : S = Presieve.ofArrows Z π
x✝ : (Y : C) × { f // S f }
a : α
hf : S (π a)
⊢ ∃ a_1, v hS a_1 = { fst := Z a, snd := { val := π a, property := hf } }
Tactic:
exact ⟨a, rfl⟩
Proof state after:
no goals
Theorem: CategoryTheory.HasProductT
Proof state before:
C : Type u
inst✝³ : Category C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasPullbackOfIsIsodesc C
α : Type
inst✝ : Fintype α
Z : α → C
X : C
π : (a : α) → Z a ⟶ X
S : Presieve X
hS : S = Presieve.ofArrows Z π
⊢ Finite ((Y : C) × { f // S f })
Tactic:
exact Fintype.finite <| FintypeT hS
Proof state after:
no goals
Theorem: CategoryTheory.HasProductT
Proof state before:
C : Type u
inst✝³ : Category C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasPullbackOfIsIsodesc C
α : Type
inst✝ : Fintype α
Z : α → C
X : C
π : (a : α) → Z a ⟶ X
S : Presieve X
hS : S = Presieve.ofArrows Z π
this : Finite ((Y : C) × { f // S f })
⊢ HasProduct fun f => f.fst.op
Tactic:
infer_instance
Proof state after:
no goals
Theorem: CategoryTheory.piCompInvdesc
Proof state before:
C : Type u
inst✝³ : Category C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasPullbackOfIsIsodesc C
α : Type
inst✝ : Fintype α
Z : α → C
X : C
π : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc π)
a : α
⊢ π a ≫ inv (Sigma.desc π) = Sigma.ι Z a
Tactic:
simp
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
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
⊢ IsIso (Equalizer.forkMap F S)
Tactic:
rcases hS with ⟨α, _, Z, π, hS, HIso⟩
Proof state after:
case intro.intro.intro.intro.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 π)
⊢ IsIso (Equalizer.forkMap F S)
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
case intro.intro.intro.intro.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 π)
⊢ IsIso (Equalizer.forkMap F S)
Tactic:
haveI : PreservesLimit (Discrete.functor fun a => op (Z a)) F := by
    haveI := (hF.preserves α); infer_instance
Proof state after:
case intro.intro.intro.intro.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
⊢ IsIso (Equalizer.forkMap F S)
Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork
Proof state before:
case intro.intro.intro.intro.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
⊢ IsIso (Equalizer.forkMap F S)
Tactic:
refine' ⟨fromFirst hS hF HIso, _, _⟩
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
⊢ Equalizer.forkMap F S ≫ fromFirst hS hF HIso = 𝟙 (F.obj X.op)

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)
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 π)
⊢ PreservesLimit (Discrete.functor fun a => (Z a).op) F
Tactic:
haveI := (hF.preserves α)
Proof state after:
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 : PreservesLimitsOfShape (Discrete α) F
⊢ PreservesLimit (Discrete.functor fun a => (Z a).op) F
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 : PreservesLimitsOfShape (Discrete α) F
⊢ PreservesLimit (Discrete.functor fun a => (Z a).op) F
Tactic:
infer_instance
Proof state after:
no goals
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
⊢ Equalizer.forkMap F S ≫ fromFirst hS hF HIso = 𝟙 (F.obj X.op)
Tactic:
unfold fromFirst
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
⊢ Equalizer.forkMap F S ≫
      comparisoninv hS F ≫
        (PreservesProduct.iso F fun a => (Z a).op).inv ≫ F.map (CoprodToProd Z).inv ≫ F.map (inv (Sigma.desc π).op) =
    𝟙 (F.obj X.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
⊢ Equalizer.forkMap F S ≫
      comparisoninv hS F ≫
        (PreservesProduct.iso F fun a => (Z a).op).inv ≫ F.map (CoprodToProd Z).inv ≫ F.map (inv (Sigma.desc π).op) =
    𝟙 (F.obj X.op)
Tactic:
simp only [← Category.assoc]
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
⊢ (((Equalizer.forkMap F S ≫ comparisoninv hS F) ≫ (PreservesProduct.iso F fun a => (Z a).op).inv) ≫
        F.map (CoprodToProd Z).inv) ≫
      F.map (inv (Sigma.desc π).op) =
    𝟙 (F.obj X.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
⊢ (((Equalizer.forkMap F S ≫ comparisoninv hS F) ≫ (PreservesProduct.iso F fun a => (Z a).op).inv) ≫
        F.map (CoprodToProd Z).inv) ≫
      F.map (inv (Sigma.desc π).op) =
    𝟙 (F.obj X.op)
Tactic:
rw [Functor.map_inv, IsIso.comp_inv_eq, Category.id_comp, ← Functor.mapIso_inv,
  Iso.comp_inv_eq, Functor.mapIso_hom, Iso.comp_inv_eq, ← Functor.map_comp, descOpCompCoprodToProd]
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
⊢ Equalizer.forkMap F S ≫ comparisoninv hS F =
    F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom
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
⊢ 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:
have : F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => op (Z a)).hom =
  Pi.lift (fun a => F.map ((Sigma.ι Z a ≫ (Sigma.desc π)).op)) := by simp
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 =
    F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom