ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J₁ : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>J₁.close (J₁.close S) = J₁.close S
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J₁ : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>J₁.close S = ⊤ ↔ S ∈ J₁.sieves X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J₁ : CategoryTheory.GrothendieckTopology C<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.Functor.closedSieves J₁).obj X = { S // J₁.IsClosed S }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J₁ : CategoryTheory.GrothendieckTopology C<GOAL>∀ {X Y : Cᵒᵖ} (f : X ⟶ Y) (S : { S // J₁.IsClosed S }), ↑((CategoryTheory.Functor.closedSieves J₁).map f S) = CategoryTheory.Sieve.pullback f.unop ↑S
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J₁ : CategoryTheory.GrothendieckTopology C<GOAL>CategoryTheory.Presieve.IsSheaf J₁ (CategoryTheory.Functor.closedSieves J₁)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J₁ J₂ : CategoryTheory.GrothendieckTopology C<VAR>h : CategoryTheory.Presieve.IsSheaf J₁ (CategoryTheory.Functor.closedSieves J₂)<GOAL>J₁ ≤ J₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J₁ J₂ : CategoryTheory.GrothendieckTopology C<GOAL>J₁ = J₂ ↔ ∀ (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))), CategoryTheory.Presieve.IsSheaf J₁ P ↔ CategoryTheory.Presieve.IsSheaf J₂ P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>c : (X : C) → ClosureOperator (CategoryTheory.Sieve X)<VAR>hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : CategoryTheory.Sieve X), (c Y) (CategoryTheory.Sieve.pullback f S) = CategoryTheory.Sieve.pullback f ((c X) S)<VAR>X : C<GOAL>(CategoryTheory.topologyOfClosureOperator c hc).sieves X = {S | (c X) S = ⊤}
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J₁ : CategoryTheory.GrothendieckTopology C<GOAL>CategoryTheory.topologyOfClosureOperator J₁.closureOperator ⋯ = J₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>c : (X : C) → ClosureOperator (CategoryTheory.Sieve X)<VAR>pb : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : CategoryTheory.Sieve X), (c Y) (CategoryTheory.Sieve.pullback f S) = CategoryTheory.Sieve.pullback f ((c X) S)<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>(CategoryTheory.topologyOfClosureOperator c pb).close S = (c X) S
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.GrothendieckTopology C<VAR>X Y : C<VAR>S : CategoryTheory.Sieve X<VAR>f : Y ⟶ X<GOAL>S ∈ self.sieves X → CategoryTheory.Sieve.pullback f S ∈ self.sieves Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>S ∈ self.sieves X → ∀ (R : CategoryTheory.Sieve X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → CategoryTheory.Sieve.pullback f R ∈ self.sieves Y) → R ∈ self.sieves X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.GrothendieckTopology C<VAR>X : C<GOAL>⊤ ∈ self.sieves X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J₁ J₂ : CategoryTheory.GrothendieckTopology C<VAR>h : J₁.sieves = J₂.sieves<GOAL>J₁ = J₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : C<GOAL>⊤ ∈ J.sieves X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>S : CategoryTheory.Sieve X<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>f : Y ⟶ X<VAR>hS : S ∈ J.sieves X<GOAL>CategoryTheory.Sieve.pullback f S ∈ J.sieves Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>i : X ⟶ Y<VAR>CategoryTheory.IsIso i<VAR>S : CategoryTheory.Sieve Y<GOAL>CategoryTheory.Sieve.pullback i S ∈ J.sieves X ↔ S ∈ J.sieves Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>hS : S ∈ J.sieves X<VAR>R : CategoryTheory.Sieve X<VAR>h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → CategoryTheory.Sieve.pullback f R ∈ J.sieves Y<GOAL>R ∈ J.sieves X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>J : CategoryTheory.GrothendieckTopology C<GOAL>S = ⊤ → S ∈ J.sieves X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>S R : CategoryTheory.Sieve X<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>Hss : S ≤ R<VAR>sjx : S ∈ J.sieves X<GOAL>R ∈ J.sieves X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>S R : CategoryTheory.Sieve X<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>rj : R ∈ J.sieves X<VAR>sj : S ∈ J.sieves X<GOAL>R ⊓ S ∈ J.sieves X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>S R : CategoryTheory.Sieve X<VAR>J : CategoryTheory.GrothendieckTopology C<GOAL>R ⊓ S ∈ J.sieves X ↔ R ∈ J.sieves X ∧ S ∈ J.sieves X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S : CategoryTheory.Sieve X<VAR>R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S.arrows f → CategoryTheory.Sieve Y<VAR>hS : S ∈ J.sieves X<VAR>hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (H : S.arrows f), R H ∈ J.sieves Y<GOAL>CategoryTheory.Sieve.bind S.arrows R ∈ J.sieves X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S : CategoryTheory.Sieve X<VAR>f : Y ⟶ X<GOAL>J.Covers S f ↔ CategoryTheory.Sieve.pullback f S ∈ J.sieves Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S : CategoryTheory.Sieve X<GOAL>S ∈ J.sieves X ↔ J.Covers S (CategoryTheory.CategoryStruct.id X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>f : Y ⟶ X<VAR>S : CategoryTheory.Sieve X<VAR>hf : S.arrows f<GOAL>J.Covers S f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>f : Y ⟶ X<VAR>S : CategoryTheory.Sieve X<VAR>h : J.Covers S f<VAR>Z : C<VAR>g : Z ⟶ Y<GOAL>J.Covers S (CategoryTheory.CategoryStruct.comp g f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>f : Y ⟶ X<VAR>S R : CategoryTheory.Sieve X<VAR>h : J.Covers S f<GOAL>(∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g) → J.Covers R f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>f : Y ⟶ X<VAR>S R : CategoryTheory.Sieve X<VAR>hS : J.Covers S f<VAR>hR : J.Covers R f<GOAL>J.Covers (S ⊓ R) f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>S ∈ (CategoryTheory.GrothendieckTopology.trivial C).sieves X ↔ S = ⊤
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J₁ J₂ : CategoryTheory.GrothendieckTopology C<GOAL>J₁ ≤ J₂ ↔ J₁.sieves ≤ J₂.sieves
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>s : Set (CategoryTheory.GrothendieckTopology C)<GOAL>IsGLB s (sInf s)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.GrothendieckTopology.trivial C = ⊥
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.GrothendieckTopology.discrete C = ⊤
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>S ∈ ⊥.sieves X ↔ S = ⊤
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>S ∈ ⊤.sieves X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>S : CategoryTheory.Sieve X<VAR>f : Y ⟶ X<GOAL>⊥.Covers S f ↔ S.arrows f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>S : CategoryTheory.Sieve X<VAR>f : Y ⟶ X<GOAL>⊤.Covers S f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>S ∈ CategoryTheory.GrothendieckTopology.dense.sieves X ↔ ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (CategoryTheory.CategoryStruct.comp g f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPullbacks C<GOAL>CategoryTheory.GrothendieckTopology.RightOreCondition C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S : J.Cover X<GOAL>S.sieve ∈ J.sieves X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S T : J.Cover X<VAR>h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), S.sieve.arrows f ↔ T.sieve.arrows f<GOAL>S = T
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S : J.Cover X<VAR>self : S.Arrow<GOAL>S.sieve.arrows self.f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S : J.Cover X<VAR>I₁ I₂ : S.Arrow<VAR>self : I₁.Relation I₂<GOAL>CategoryTheory.CategoryStruct.comp self.g₁ I₁.f = CategoryTheory.CategoryStruct.comp self.g₂ I₂.f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S : J.Cover X<VAR>I : S.Arrow<VAR>Z : C<VAR>g : Z ⟶ I.Y<GOAL>(I.precomp g).f = CategoryTheory.CategoryStruct.comp g I.f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S : J.Cover X<VAR>I : S.Arrow<VAR>Z : C<VAR>g : Z ⟶ I.Y<GOAL>(I.precomp g).Y = Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S : J.Cover X<VAR>I : S.Arrow<VAR>Z : C<VAR>g : Z ⟶ I.Y<GOAL>(I.precompRelation g).g₁ = CategoryTheory.CategoryStruct.id (I.precomp g).Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S : J.Cover X<VAR>I : S.Arrow<VAR>Z : C<VAR>g : Z ⟶ I.Y<GOAL>(I.precompRelation g).g₂ = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S : J.Cover X<VAR>I : S.Arrow<VAR>Z : C<VAR>g : Z ⟶ I.Y<GOAL>(I.precompRelation g).Z = (I.precomp g).Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S T : J.Cover X<VAR>I : S.Arrow<VAR>f : S ⟶ T<GOAL>(I.map f).Y = I.Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S T : J.Cover X<VAR>I : S.Arrow<VAR>f : S ⟶ T<GOAL>(I.map f).f = I.f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S T : J.Cover X<VAR>I₁ I₂ : S.Arrow<VAR>r : I₁.Relation I₂<VAR>f : S ⟶ T<GOAL>(r.map f).g₂ = r.g₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S T : J.Cover X<VAR>I₁ I₂ : S.Arrow<VAR>r : I₁.Relation I₂<VAR>f : S ⟶ T<GOAL>(r.map f).g₁ = r.g₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S T : J.Cover X<VAR>I₁ I₂ : S.Arrow<VAR>r : I₁.Relation I₂<VAR>f : S ⟶ T<GOAL>(r.map f).Z = r.Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>f : Y ⟶ X<VAR>S : J.Cover X<VAR>I : (S.pullback f).Arrow<GOAL>I.base.Y = I.Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>f : Y ⟶ X<VAR>S : J.Cover X<VAR>I : (S.pullback f).Arrow<GOAL>I.base.f = CategoryTheory.CategoryStruct.comp I.f f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>Z : C<VAR>f : Y ⟶ X<VAR>g : Z ⟶ Y<VAR>S : J.Cover X<GOAL>(S.pullback f).sieve.arrows g ↔ S.sieve.arrows (CategoryTheory.CategoryStruct.comp g f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : J.Cover X<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>I : (S.bind T).Arrow<GOAL>S.sieve.arrows I.fromMiddleHom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : J.Cover X<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>I : (S.bind T).Arrow<GOAL>(T I.fromMiddle).sieve.arrows I.toMiddleHom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : J.Cover X<VAR>T : (I : S.Arrow) → J.Cover I.Y<VAR>I : (S.bind T).Arrow<GOAL>CategoryTheory.CategoryStruct.comp I.toMiddleHom I.fromMiddleHom = I.f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S : J.Cover X<VAR>fst snd : S.Arrow<VAR>r : fst.Relation snd<GOAL>(CategoryTheory.GrothendieckTopology.Cover.Relation.mk' r).r = r
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S : J.Cover X<VAR>fst snd : S.Arrow<VAR>r : fst.Relation snd<GOAL>(CategoryTheory.GrothendieckTopology.Cover.Relation.mk' r).fst = fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S : J.Cover X<VAR>fst snd : S.Arrow<VAR>r : fst.Relation snd<GOAL>(CategoryTheory.GrothendieckTopology.Cover.Relation.mk' r).snd = snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>S : J.Cover X<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>I : S.Relation<GOAL>(S.index P).sndTo I = I.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>S : J.Cover X<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>I : S.Relation<GOAL>(S.index P).snd I = P.map I.r.g₂.op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>S : J.Cover X<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>I : S.Relation<GOAL>(S.index P).fst I = P.map I.r.g₁.op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>S : J.Cover X<VAR>P : CategoryTheory.Functor Cᵒᵖ D<GOAL>(S.index P).R = S.Relation
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>S : J.Cover X<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>I : S.Relation<GOAL>(S.index P).fstTo I = I.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>S : J.Cover X<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>I : S.Relation<GOAL>(S.index P).right I = P.obj (Opposite.op I.r.Z)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>S : J.Cover X<VAR>P : CategoryTheory.Functor Cᵒᵖ D<GOAL>(S.index P).L = S.Arrow
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>S : J.Cover X<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>I : S.Arrow<GOAL>(S.index P).left I = P.obj (Opposite.op I.Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>f : Y ⟶ X<VAR>S : J.Cover X<GOAL>(J.pullback f).obj S = S.pullback f
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>self : C ≌ D<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (self.functor.map (self.unitIso.hom.app X)) (self.counitIso.hom.app (self.functor.obj X)) = CategoryTheory.CategoryStruct.id (self.functor.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>functor : CategoryTheory.Functor C D<VAR>inverse : CategoryTheory.Functor D C<VAR>unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse<VAR>counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D<VAR>f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)<GOAL>{ functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.unit = unit_iso.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>functor : CategoryTheory.Functor C D<VAR>inverse : CategoryTheory.Functor D C<VAR>unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse<VAR>counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D<VAR>f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)<GOAL>{ functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.counit = counit_iso.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>functor : CategoryTheory.Functor C D<VAR>inverse : CategoryTheory.Functor D C<VAR>unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse<VAR>counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D<VAR>f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)<GOAL>{ functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.unitInv = unit_iso.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>functor : CategoryTheory.Functor C D<VAR>inverse : CategoryTheory.Functor D C<VAR>unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse<VAR>counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D<VAR>f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)<GOAL>{ functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.counitInv = counit_iso.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (e.functor.map (e.unit.app X)) (e.counit.app (e.functor.obj X)) = CategoryTheory.CategoryStruct.id (e.functor.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (e.counitInv.app (e.functor.obj X)) (e.functor.map (e.unitInv.app X)) = CategoryTheory.CategoryStruct.id (e.functor.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X : C<GOAL>e.counitInv.app (e.functor.obj X) = e.functor.map (e.unit.app X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X : C<GOAL>e.counit.app (e.functor.obj X) = e.functor.map (e.unitInv.app X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>CategoryTheory.CategoryStruct.comp (e.unit.app (e.inverse.obj Y)) (e.inverse.map (e.counit.app Y)) = CategoryTheory.CategoryStruct.id (e.inverse.obj Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>CategoryTheory.CategoryStruct.comp (e.inverse.map (e.counitInv.app Y)) (e.unitInv.app (e.inverse.obj Y)) = CategoryTheory.CategoryStruct.id (e.inverse.obj Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counitInv.app Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>Y : D<GOAL>e.unitInv.app (e.inverse.obj Y) = e.inverse.map (e.counit.app Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>e.functor.map (e.inverse.map f) = CategoryTheory.CategoryStruct.comp (e.counit.app X) (CategoryTheory.CategoryStruct.comp f (e.counitInv.app Y))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>e.inverse.map (e.functor.map f) = CategoryTheory.CategoryStruct.comp (e.unitInv.app X) (CategoryTheory.CategoryStruct.comp f (e.unit.app Y))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D C<VAR>η : CategoryTheory.Functor.id C ≅ F.comp G<VAR>ε : G.comp F ≅ CategoryTheory.Functor.id D<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.Equivalence.adjointifyη η ε).hom.app X)) (ε.hom.app (F.obj X)) = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>CategoryTheory.Equivalence.refl.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>CategoryTheory.Equivalence.refl.inverse = CategoryTheory.Functor.id C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>CategoryTheory.Equivalence.refl.counitIso = CategoryTheory.Iso.refl ((CategoryTheory.Functor.id C).comp (CategoryTheory.Functor.id C))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>CategoryTheory.Equivalence.refl.functor = CategoryTheory.Functor.id C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>e.symm.unitIso = e.counitIso.symm
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>e.symm.counitIso = e.unitIso.symm
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>e.symm.functor = e.inverse
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>e.symm.inverse = e.functor
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>e : C ≌ D<VAR>f : D ≌ E<GOAL>(e.trans f).unitIso = e.unitIso ≪≫ CategoryTheory.isoWhiskerLeft e.functor (CategoryTheory.isoWhiskerRight f.unitIso e.inverse)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>e : C ≌ D<VAR>f : D ≌ E<GOAL>(e.trans f).inverse = f.inverse.comp e.inverse
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>e : C ≌ D<VAR>f : D ≌ E<GOAL>(e.trans f).functor = e.functor.comp f.functor
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>e : C ≌ D<VAR>f : D ≌ E<GOAL>(e.trans f).counitIso = CategoryTheory.isoWhiskerLeft f.inverse (CategoryTheory.isoWhiskerRight e.counitIso f.functor) ≪≫ f.counitIso
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>e : C ≌ D<VAR>F : CategoryTheory.Functor C E<VAR>X : C<GOAL>(e.funInvIdAssoc F).hom.app X = F.map (e.unitInv.app X)