mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
⊢ Compatible P π x ↔ PullbackCompatible P π x

Tactic:
refine ⟨fun t i j ↦ ?_, fun t i j Z gi gj comm ↦ ?_⟩
  · apply t
    exact pullback.condition
  · rw [← pullback.lift_fst _ _ comm, op_comp, Functor.map_comp, comp_apply, t i j,
      ← comp_apply, ← Functor.map_comp, ← op_comp, pullback.lift_snd]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
B : Type u₃
inst✝¹ : Category.{v₃, u₃} B
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
s : A ⥤ B
inst✝ : ReflectsLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
h : ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (IsLimit ((P ⋙ s).mapCone S.arrows.cocone.op))
⊢ ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (IsLimit (P.mapCone S.arrows.cocone.op))

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
B : Type u₃
inst✝¹ : Category.{v₃, u₃} B
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
s : A ⥤ B
inst✝ : ReflectsLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
h : ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (IsLimit ((P ⋙ s).mapCone S.arrows.cocone.op))
⊢ ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (IsLimit (P.mapCone S.arrows.cocone.op))
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
B : Type u₃
inst✝¹ : Category.{v₃, u₃} B
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
s : A ⥤ B
inst✝ : PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
h : ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (IsLimit (P.mapCone S.arrows.cocone.op))
⊢ ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (IsLimit ((P ⋙ s).mapCone S.arrows.cocone.op))

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
B : Type u₃
inst✝¹ : Category.{v₃, u₃} B
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
s : A ⥤ B
inst✝ : PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
h : ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (IsLimit (P.mapCone S.arrows.cocone.op))
⊢ ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (IsLimit ((P ⋙ s).mapCone S.arrows.cocone.op))
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case e'_2
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : J.Cover X
x : Meq P S✝
y : Meq P T
S : J.Cover X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (unop (op S)).shape.L
e : ↑(x.refine h1) i = ↑(y.refine h2) i
e_1✝ : CD (((unop (op S)).index P).left i) = ToType (P.obj (op i.Y))
⊢ ↑x (Cover.Arrow.map i h1) = ↑x { Y := i.Y, f := i.f, hf := ⋯ }

Tactic:
]

Goal state after:
case e'_2
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : J.Cover X
x : Meq P S✝
y : Meq P T
S : J.Cover X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (unop (op S)).shape.L
e : ↑(x.refine h1) i = ↑(y.refine h2) i
e_1✝ : CD (((unop (op S)).index P).left i) = ToType (P.obj (op i.Y))
⊢ ↑x (Cover.Arrow.map i h1) = ↑x { Y := i.Y, f := i.f, hf := ⋯ }
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
f : X ⟶ Y
⊢ (∀ (b : P.obj (op X)) (t₁ t₂ : P.obj (op Y)),
      ((FamilyOfElements.singletonEquiv P f).symm b).IsAmalgamation t₁ →
        ((FamilyOfElements.singletonEquiv P f).symm b).IsAmalgamation t₂ → t₁ = t₂) ↔
    Function.Injective ⇑(ConcreteCategory.hom (P.map f.op))

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
f : X ⟶ Y
⊢ (∀ (b : P.obj (op X)) (t₁ t₂ : P.obj (op Y)),
      ((FamilyOfElements.singletonEquiv P f).symm b).IsAmalgamation t₁ →
        ((FamilyOfElements.singletonEquiv P f).symm b).IsAmalgamation t₂ → t₁ = t₂) ↔
    Function.Injective ⇑(ConcreteCategory.hom (P.map f.op))
Module: Mathlib.CategoryTheory.Sites.Whiskering

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁵ : Category.{v₂, u₂} A
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
inst✝³ : J.HasSheafCompose F
inst✝² : J.HasSheafCompose G
inst✝¹ : J.HasSheafCompose H
inst✝ : F.ReflectsIsomorphisms
G₁ G₂ : Sheaf J A
f : G₁ ⟶ G₂
x✝ : IsIso ((sheafCompose J F).map f)
⊢ IsIso (((whiskeringRight Cᵒᵖ A B).obj F).map ((sheafToPresheaf J A).map f))

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁵ : Category.{v₂, u₂} A
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
inst✝³ : J.HasSheafCompose F
inst✝² : J.HasSheafCompose G
inst✝¹ : J.HasSheafCompose H
inst✝ : F.ReflectsIsomorphisms
G₁ G₂ : Sheaf J A
f : G₁ ⟶ G₂
x✝ : IsIso ((sheafCompose J F).map f)
⊢ IsIso (((whiskeringRight Cᵒᵖ A B).obj F).map ((sheafToPresheaf J A).map f))
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
f : X ⟶ Y
⊢ (∀ (b : P.obj (op X)),
      ((FamilyOfElements.singletonEquiv P f).symm b).Compatible →
        ∃! t, ((FamilyOfElements.singletonEquiv P f).symm b).IsAmalgamation t) ↔
    ∀ (x : P.obj (op X)),
      (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
          p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (P.map p₁.op)) x = (ConcreteCategory.hom (P.map p₂.op)) x) →
        ∃! y, (ConcreteCategory.hom (P.map f.op)) y = x

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
f : X ⟶ Y
⊢ (∀ (b : P.obj (op X)),
      ((FamilyOfElements.singletonEquiv P f).symm b).Compatible →
        ∃! t, ((FamilyOfElements.singletonEquiv P f).symm b).IsAmalgamation t) ↔
    ∀ (x : P.obj (op X)),
      (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
          p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (P.map p₁.op)) x = (ConcreteCategory.hom (P.map p₂.op)) x) →
        ∃! y, (ConcreteCategory.hom (P.map f.op)) y = x
Module: Mathlib.CategoryTheory.Sites.Whiskering

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁵ : Category.{v₂, u₂} A
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F✝ G H : A ⥤ B
η : F✝ ⟶ G
γ : G ⟶ H
inst✝³ : J.HasSheafCompose F✝
inst✝² : J.HasSheafCompose G
inst✝¹ : J.HasSheafCompose H
F : A ⥤ B
inst✝ : ∀ (X : C) (S : J.Cover X) (P : Cᵒᵖ ⥤ A), PreservesLimit (S.index P).multicospan F
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
⊢ ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork (P ⋙ F)))

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁵ : Category.{v₂, u₂} A
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F✝ G H : A ⥤ B
η : F✝ ⟶ G
γ : G ⟶ H
inst✝³ : J.HasSheafCompose F✝
inst✝² : J.HasSheafCompose G
inst✝¹ : J.HasSheafCompose H
F : A ⥤ B
inst✝ : ∀ (X : C) (S : J.Cover X) (P : Cᵒᵖ ⥤ A), PreservesLimit (S.index P).multicospan F
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
⊢ ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork (P ⋙ F)))
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case e'_3
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : J.Cover X
x : Meq P S✝
y : Meq P T
S : J.Cover X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (unop (op S)).shape.L
e : ↑(x.refine h1) i = ↑(y.refine h2) i
e_1✝ : CD (((unop (op S)).index P).left i) = ToType (P.obj (op i.Y))
⊢ (ConcreteCategory.hom (Multiequalizer.ι (T.index P) (Cover.Arrow.map i h2))) ((Meq.equiv P T).symm y) =
    ↑y { Y := i.Y, f := i.f, hf := ⋯ }

Tactic:
]

Goal state after:
case e'_3
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : J.Cover X
x : Meq P S✝
y : Meq P T
S : J.Cover X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (unop (op S)).shape.L
e : ↑(x.refine h1) i = ↑(y.refine h2) i
e_1✝ : CD (((unop (op S)).index P).left i) = ToType (P.obj (op i.Y))
⊢ (ConcreteCategory.hom (Multiequalizer.ι (T.index P) (Cover.Arrow.map i h2))) ((Meq.equiv P T).symm y) =
    ↑y { Y := i.Y, f := i.f, hf := ⋯ }
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case e'_3
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : J.Cover X
x : Meq P S✝
y : Meq P T
S : J.Cover X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (unop (op S)).shape.L
e : ↑(x.refine h1) i = ↑(y.refine h2) i
e_1✝ : CD (((unop (op S)).index P).left i) = ToType (P.obj (op i.Y))
⊢ ↑y (Cover.Arrow.map i h2) = ↑y { Y := i.Y, f := i.f, hf := ⋯ }

Tactic:
]

Goal state after:
case e'_3
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : J.Cover X
x : Meq P S✝
y : Meq P T
S : J.Cover X
h1 : S ⟶ S✝
h2 : S ⟶ T
i : (unop (op S)).shape.L
e : ↑(x.refine h1) i = ↑(y.refine h2) i
e_1✝ : CD (((unop (op S)).index P).left i) = ToType (P.obj (op i.Y))
⊢ ↑y (Cover.Arrow.map i h2) = ↑y { Y := i.Y, f := i.f, hf := ⋯ }
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
s : (sheafify J G).toFunctor.obj (op U)
H : x''.IsAmalgamation ↑s
V : C
i : V ⟶ U
hi : S.arrows i
V' : C
i' : V' ⟶ unop (op V)
hi' : (G.sieveOfSection ↑(x i hi)).arrows i'
hi'' : S'.arrows (i' ≫ i)
this : (ConcreteCategory.hom (F.map i.op ≫ F.map i'.op)) ↑s = x'' (i' ≫ i) hi''
⊢ (ConcreteCategory.hom (F.map i'.op)) ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i.op)) s) =
    (ConcreteCategory.hom (F.map i'.op)) ↑(x i hi)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
s : (sheafify J G).toFunctor.obj (op U)
H : x''.IsAmalgamation ↑s
V : C
i : V ⟶ U
hi : S.arrows i
V' : C
i' : V' ⟶ unop (op V)
hi' : (G.sieveOfSection ↑(x i hi)).arrows i'
hi'' : S'.arrows (i' ≫ i)
this : (ConcreteCategory.hom (F.map i.op ≫ F.map i'.op)) ↑s = x'' (i' ≫ i) hi''
⊢ (ConcreteCategory.hom (F.map i'.op)) ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i.op)) s) =
    (ConcreteCategory.hom (F.map i'.op)) ↑(x i hi)
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S Sx : J.Cover X
x : Meq P Sx
Sy : J.Cover X
y : Meq P Sy
h : ∀ (I : S.Arrow), mk (x.pullback I.f) = mk (y.pullback I.f)
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
hh : ∀ (I : S.Arrow), (x.pullback I.f).refine (h1 I) = (y.pullback I.f).refine (h2 I)
⊢ ∃ W h1 h2, x.refine h1 = y.refine h2

Tactic:
]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S Sx : J.Cover X
x : Meq P Sx
Sy : J.Cover X
y : Meq P Sy
h : ∀ (I : S.Arrow), mk (x.pullback I.f) = mk (y.pullback I.f)
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
hh : ∀ (I : S.Arrow), (x.pullback I.f).refine (h1 I) = (y.pullback I.f).refine (h2 I)
⊢ ∃ W h1 h2, x.refine h1 = y.refine h2
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
H : ∀ (s : (sheafify J G).toFunctor.obj (op U)), x''.IsAmalgamation ↑s → x.IsAmalgamation s
V₁ V₂ V₃ : C
g₁ : V₃ ⟶ V₁
g₂ : V₃ ⟶ V₂
g₃ : V₁ ⟶ U
g₄ : V₂ ⟶ U
S₁ : S'.arrows g₃
S₂ : S'.arrows g₄
e : g₁ ≫ g₃ = g₂ ≫ g₄
⊢ (ConcreteCategory.hom (F.map (i₁ V₁ g₃ S₁).op ≫ F.map g₁.op)) ↑(x (i₂ V₁ g₃ S₁) ⋯) =
    (ConcreteCategory.hom (F.map (i₁ V₂ g₄ S₂).op ≫ F.map g₂.op)) ↑(x (i₂ V₂ g₄ S₂) ⋯)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
H : ∀ (s : (sheafify J G).toFunctor.obj (op U)), x''.IsAmalgamation ↑s → x.IsAmalgamation s
V₁ V₂ V₃ : C
g₁ : V₃ ⟶ V₁
g₂ : V₃ ⟶ V₂
g₃ : V₁ ⟶ U
g₄ : V₂ ⟶ U
S₁ : S'.arrows g₃
S₂ : S'.arrows g₄
e : g₁ ≫ g₃ = g₂ ≫ g₄
⊢ (ConcreteCategory.hom (F.map (i₁ V₁ g₃ S₁).op ≫ F.map g₁.op)) ↑(x (i₂ V₁ g₃ S₁) ⋯) =
    (ConcreteCategory.hom (F.map (i₁ V₂ g₄ S₂).op ≫ F.map g₂.op)) ↑(x (i₂ V₂ g₄ S₂) ⋯)
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S Sx : J.Cover X
x : Meq P Sx
Sy : J.Cover X
y : Meq P Sy
h : ∀ (I : S.Arrow), mk (x.pullback I.f) = mk (y.pullback I.f)
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
hh : ∀ (I : S.Arrow), (x.pullback I.f).refine (h1 I) = (y.pullback I.f).refine (h2 I)
B : J.Cover X := S.bind W
Y : C
f : Y ⟶ X
Z : C
e1 : Y ⟶ Z
e2 : Z ⟶ X
he2 : (↑S).arrows e2
he1 : ((fun Y f hf ↦ ↑(W { Y := Y, f := f, hf := hf })) Z e2 he2).arrows e1
hee : e1 ≫ e2 = f
⊢ (↑Sx).arrows (e1 ≫ e2)

Tactic:
]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S Sx : J.Cover X
x : Meq P Sx
Sy : J.Cover X
y : Meq P Sy
h : ∀ (I : S.Arrow), mk (x.pullback I.f) = mk (y.pullback I.f)
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
hh : ∀ (I : S.Arrow), (x.pullback I.f).refine (h1 I) = (y.pullback I.f).refine (h2 I)
B : J.Cover X := S.bind W
Y : C
f : Y ⟶ X
Z : C
e1 : Y ⟶ Z
e2 : Z ⟶ X
he2 : (↑S).arrows e2
he1 : ((fun Y f hf ↦ ↑(W { Y := Y, f := f, hf := hf })) Z e2 he2).arrows e1
hee : e1 ≫ e2 = f
⊢ (↑Sx).arrows (e1 ≫ e2)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg ↦ s (g ≫ f) ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible
t : FamilyOfElements P U.arrows := fun Y f hf ↦ ⋯.amalgamate (y hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (t f hf)
⊢ t.SieveCompatible

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg ↦ s (g ≫ f) ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible
t : FamilyOfElements P U.arrows := fun Y f hf ↦ ⋯.amalgamate (y hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (t f hf)
⊢ t.SieveCompatible