mathlib-initiative/mathlib-tactics huggingface dataset:
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)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
i : (unop (op ((J.pullback I.f).obj (unop (op S))))).shape.L
⊢ (ConcreteCategory.hom
        (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 ↦ P.map I_1.f.op) ⋯ ≫
          Multiequalizer.lift ((S.pullback I.f).index P) (multiequalizer (⊤.index P))
              (fun I_1 ↦ Multiequalizer.ι (⊤.index P) (I_1.map e)) ⋯ ≫
            Multiequalizer.ι ((S.pullback I.f).index P) i))
      (↑x I) =
    (ConcreteCategory.hom (Multiequalizer.ι ((S.pullback I.f).index P) i))
      ((ConcreteCategory.hom
          (Multiequalizer.lift ((S.pullback I.f).index P) (multiequalizer (S.index P))
            (fun I_1 ↦ Multiequalizer.ι (S.index P) I_1.base) ⋯))
        ((Meq.equiv P S).symm x))

Tactic:
← ConcreteCategory.comp_apply,

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)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
i : (unop (op ((J.pullback I.f).obj (unop (op S))))).shape.L
⊢ (ConcreteCategory.hom
        (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 ↦ P.map I_1.f.op) ⋯ ≫
          Multiequalizer.lift ((S.pullback I.f).index P) (multiequalizer (⊤.index P))
              (fun I_1 ↦ Multiequalizer.ι (⊤.index P) (I_1.map e)) ⋯ ≫
            Multiequalizer.ι ((S.pullback I.f).index P) i))
      (↑x I) =
    (ConcreteCategory.hom
        (Multiequalizer.lift ((S.pullback I.f).index P) (multiequalizer (S.index P))
            (fun I_1 ↦ Multiequalizer.ι (S.index P) I_1.base) ⋯ ≫
          Multiequalizer.ι ((S.pullback I.f).index P) i))
      ((Meq.equiv P S).symm x)
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
h : mk x = mk y
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
I : (unop W).Arrow
hh :
  (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y))
e_1✝ : ToType (P.obj (op I.Y)) = CD (((unop W).index P).left I)
⊢ ↑x { Y := I.Y, f := I.f, hf := ⋯ } =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom
          (Multiequalizer.lift ((unop W).index P) (multiequalizer (S.index P))
            (fun I ↦ Multiequalizer.ι (S.index P) (Cover.Arrow.map I h1.unop)) ⋯))
        ((Meq.equiv P S).symm x))

Tactic:
← ConcreteCategory.comp_apply,

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
h : mk x = mk y
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
I : (unop W).Arrow
hh :
  (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y))
e_1✝ : ToType (P.obj (op I.Y)) = CD (((unop W).index P).left I)
⊢ ↑x { Y := I.Y, f := I.f, hf := ⋯ } =
    (ConcreteCategory.hom
        (Multiequalizer.lift ((unop W).index P) (multiequalizer (S.index P))
            (fun I ↦ Multiequalizer.ι (S.index P) (Cover.Arrow.map I h1.unop)) ⋯ ≫
          Multiequalizer.ι ((unop W).index P) I))
      ((Meq.equiv P S).symm x)
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
h : mk x = mk y
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
I : (unop W).Arrow
hh :
  (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y))
e_1✝ : ToType (P.obj (op I.Y)) = CD (((unop W).index P).left I)
⊢ ↑y { Y := I.Y, f := I.f, hf := ⋯ } =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom
          (Multiequalizer.lift ((unop W).index P) (multiequalizer (T.index P))
            (fun I ↦ Multiequalizer.ι (T.index P) (Cover.Arrow.map I h2.unop)) ⋯))
        ((Meq.equiv P T).symm y))

Tactic:
← ConcreteCategory.comp_apply,

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
h : mk x = mk y
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
I : (unop W).Arrow
hh :
  (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y))
e_1✝ : ToType (P.obj (op I.Y)) = CD (((unop W).index P).left I)
⊢ ↑y { Y := I.Y, f := I.f, hf := ⋯ } =
    (ConcreteCategory.hom
        (Multiequalizer.lift ((unop W).index P) (multiequalizer (T.index P))
            (fun I ↦ Multiequalizer.ι (T.index P) (Cover.Arrow.map I h2.unop)) ⋯ ≫
          Multiequalizer.ι ((unop W).index P) I))
      ((Meq.equiv P T).symm y)
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))
⊢ (ConcreteCategory.hom (Multiequalizer.ι (S.index P) i))
      ((ConcreteCategory.hom
          (Multiequalizer.lift (S.index P) (multiequalizer (S✝.index P))
            (fun I ↦ Multiequalizer.ι (S✝.index P) (Cover.Arrow.map I h1)) ⋯))
        ((Meq.equiv P S✝).symm x)) =
    ↑x { Y := i.Y, f := i.f, hf := ⋯ }

Tactic:
← ConcreteCategory.comp_apply,

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))
⊢ (ConcreteCategory.hom
        (Multiequalizer.lift (S.index P) (multiequalizer (S✝.index P))
            (fun I ↦ Multiequalizer.ι (S✝.index P) (Cover.Arrow.map I h1)) ⋯ ≫
          Multiequalizer.ι (S.index P) i))
      ((Meq.equiv P S✝).symm x) =
    ↑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
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (ofArrows X π).HasPairwisePullbacks
⊢ IsSheafFor P (ofArrows X π) ↔
    ∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.PullbackCompatible P π x → ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i

Tactic:
simp_rw [← Arrows.pullbackCompatible_iff, isSheafFor_arrows_iff]

Goal state after:
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.ι (S.index P) i))
      ((ConcreteCategory.hom
          (Multiequalizer.lift (S.index P) (multiequalizer (T.index P))
            (fun I ↦ Multiequalizer.ι (T.index P) (Cover.Arrow.map I h2)) ⋯))
        ((Meq.equiv P T).symm y)) =
    ↑y { Y := i.Y, f := i.f, hf := ⋯ }

Tactic:
← ConcreteCategory.comp_apply,

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.lift (S.index P) (multiequalizer (T.index P))
            (fun I ↦ Multiequalizer.ι (T.index P) (Cover.Arrow.map I h2)) ⋯ ≫
          Multiequalizer.ι (S.index P) i))
      ((Meq.equiv P T).symm y) =
    ↑y { Y := i.Y, f := i.f, hf := ⋯ }
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)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
s : Meq (J.plusObj P) S
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
II : (S.bind T).Relation
⊢ (ConcreteCategory.hom ((J.toPlus P).app (op II.r.Z)))
      ((ConcreteCategory.hom (P.map II.r.g₁.op)) ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) II.fst)) =
    (ConcreteCategory.hom ((J.toPlus P).app (op II.r.Z)))
      ((ConcreteCategory.hom (P.map II.r.g₂.op)) ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) II.snd))

Tactic:
← ConcreteCategory.comp_apply,

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)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
s : Meq (J.plusObj P) S
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
II : (S.bind T).Relation
⊢ (ConcreteCategory.hom (P.map II.r.g₁.op ≫ (J.toPlus P).app (op II.r.Z)))
      ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) II.fst) =
    (ConcreteCategory.hom ((J.toPlus P).app (op II.r.Z)))
      ((ConcreteCategory.hom (P.map II.r.g₂.op)) ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) II.snd))
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)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
s : Meq (J.plusObj P) S
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
II : (S.bind T).Relation
⊢ (ConcreteCategory.hom (P.map II.r.g₁.op ≫ (J.toPlus P).app (op II.r.Z)))
      ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) II.fst) =
    (ConcreteCategory.hom ((J.toPlus P).app (op II.r.Z)))
      ((ConcreteCategory.hom (P.map II.r.g₂.op)) ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) II.snd))

Tactic:
← ConcreteCategory.comp_apply,

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)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
s : Meq (J.plusObj P) S
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
II : (S.bind T).Relation
⊢ (ConcreteCategory.hom (P.map II.r.g₁.op ≫ (J.toPlus P).app (op II.r.Z)))
      ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) II.fst) =
    (ConcreteCategory.hom (P.map II.r.g₂.op ≫ (J.toPlus P).app (op II.r.Z)))
      ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) II.snd)
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
E : Type u_2
inst✝³ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝² : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝¹ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
X : C
W : (J.Cover X)ᵒᵖ
⊢ (J.diagram P X ⋙ F).obj W ≅ (J.diagram (P ⋙ F) X).obj W

Tactic:
refine ?_ ≪≫ HasLimit.isoOfNatIso (W.unop.multicospanComp _ _).symm

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
E : Type u_2
inst✝³ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝² : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝¹ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
X : C
W : (J.Cover X)ᵒᵖ
⊢ (J.diagram P X ⋙ F).obj W ≅ limit (((unop W).index P).multicospan ⋙ F)
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)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
s : Meq (J.plusObj P) S
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
II : (S.bind T).Relation
⊢ (ConcreteCategory.hom ((J.plusObj P).map II.r.g₁.op))
      ((ConcreteCategory.hom ((J.plusObj P).map II.fst.toMiddle.f.op)) (↑s II.fst.fromMiddle)) =
    (ConcreteCategory.hom ((J.plusObj P).map II.r.g₂.op))
      ((ConcreteCategory.hom ((J.plusObj P).map II.snd.toMiddle.f.op)) (↑s II.snd.fromMiddle))

Tactic:
← ConcreteCategory.comp_apply,

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)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
s : Meq (J.plusObj P) S
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
II : (S.bind T).Relation
⊢ (ConcreteCategory.hom ((J.plusObj P).map II.fst.toMiddle.f.op ≫ (J.plusObj P).map II.r.g₁.op))
      (↑s II.fst.fromMiddle) =
    (ConcreteCategory.hom ((J.plusObj P).map II.r.g₂.op))
      ((ConcreteCategory.hom ((J.plusObj P).map II.snd.toMiddle.f.op)) (↑s II.snd.fromMiddle))
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case h
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)
inst✝ : (forget D).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
x : ToType (multiequalizer (S.index (J.plusObj P)))
t : ToType ((J.plusObj P).obj (op X))
ht : Meq.mk S t = (Meq.equiv (J.plusObj P) S) x
i : S.Arrow
⊢ (ConcreteCategory.hom (Multiequalizer.ι (S.index (J.plusObj P)) i))
      ((ConcreteCategory.hom (S.toMultiequalizer (J.plusObj P))) t) =
    ↑(Meq.mk S t) i

Tactic:
← ConcreteCategory.comp_apply,

Goal state after:
case h
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)
inst✝ : (forget D).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
x : ToType (multiequalizer (S.index (J.plusObj P)))
t : ToType ((J.plusObj P).obj (op X))
ht : Meq.mk S t = (Meq.equiv (J.plusObj P) S) x
i : S.Arrow
⊢ (ConcreteCategory.hom (S.toMultiequalizer (J.plusObj P) ≫ Multiequalizer.ι (S.index (J.plusObj P)) i)) t =
    ↑(Meq.mk S t) i