awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
Y X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : Meq (FD := FD) (CD := CD) P S
f : Y ⟶ X
Y_1 : C
f_1 : Y_1 ⟶ Y
hf : (↑(S.pullback f) : Sieve Y).arrows f_1
⊢ (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := Y_1, f := f_1, hf := hf : (S.pullback f).Arrow }.base =
    (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y)))
      { Y := { Y := Y_1, f := f_1, hf := hf : (S.pullback f).Arrow }.Y,
        f := { Y := Y_1, f := f_1, hf := hf : (S.pullback f).Arrow }.f ≫ f, hf := ⋯ }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))
dsimp :
  Eq (α := CD ((J.plusObj P).obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (CategoryStruct.comp (Y :=
              multiequalizer (J := Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤) (Cover.index ⊤ P))
              (Cover.toMultiequalizer ⊤ P) (colimit.ι (J.diagram P X) (op ⊤))) :
          (a : CD (P.obj (op X))) → CD ((J.plusObj P).obj (op X)))
        x :
      CD ((J.plusObj P).obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P X) (op S)) :
          (a : CD (multiequalizer (S.index P))) → CD (colimit (J.diagram P X)))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
            (Meq.mk (FD := FD) (CD := CD) S x) :
          ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))) :
      CD (colimit (J.diagram P X)))
⊢ Eq (α := CD ((J.plusObj P).obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (NatTrans.app (J.toPlus P) (op X)) :
          (a : CD (P.obj (op X))) → CD ((J.plusObj P).obj (op X)))
        x :
      CD ((J.plusObj P).obj (op X)))
    (mk (FD := FD) (CD := CD) (Meq.mk (FD := FD) (CD := CD) S x) :
      ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X)))

Tactic:
dsimp [mk, toPlus]

Premises used: CategoryTheory.GrothendieckTopology.toPlus, CategoryTheory.GrothendieckTopology.Plus.mk
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
rw :
  Eq (α := CD ((J.plusObj P).obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (Cover.toMultiequalizer ⊤ P ≫ (J.diagram P X).map e.op ≫ colimit.ι (J.diagram P X) (op S)) :
          (a : CD (P.obj (op X))) → CD ((J.plusObj P).obj (op X)))
        x :
      CD ((J.plusObj P).obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P X) (op S)) :
          (a : CD (multiequalizer (S.index P))) → CD (colimit (J.diagram P X)))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
            (Meq.mk (FD := FD) (CD := CD) S x) :
          ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))) :
      CD (colimit (J.diagram P X)))
⊢ Eq (α := CD ((J.plusObj P).obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (CategoryStruct.comp (Y :=
              multiequalizer (J := Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤) (Cover.index ⊤ P))
              (Cover.toMultiequalizer ⊤ P) (colimit.ι (J.diagram P X) (op ⊤))) :
          (a : CD (P.obj (op X))) → CD ((J.plusObj P).obj (op X)))
        x :
      CD ((J.plusObj P).obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P X) (op S)) :
          (a : CD (multiequalizer (S.index P))) → CD (colimit (J.diagram P X)))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
            (Meq.mk (FD := FD) (CD := CD) S x) :
          ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))) :
      CD (colimit (J.diagram P X)))

Tactic:
rw [← colimit.w _ e.op]

Premises used: Quiver.Hom.op, CategoryTheory.Limits.colimit.w
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
delta :
  Eq (α := CD ((J.plusObj P).obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X))
                (fun (I : (Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯ ≫
              (J.diagram P X).map e.op ≫ colimit.ι (J.diagram P X) (op S)) :
          (a : CD (P.obj (op X))) → CD ((J.plusObj P).obj (op X)))
        x :
      CD ((J.plusObj P).obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P X) (op S)) :
          (a : CD (multiequalizer (S.index P))) → CD (colimit (J.diagram P X)))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
            (Meq.mk (FD := FD) (CD := CD) S x) :
          ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))) :
      CD (colimit (J.diagram P X)))
⊢ Eq (α := CD ((J.plusObj P).obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (Cover.toMultiequalizer ⊤ P ≫ (J.diagram P X).map e.op ≫ colimit.ι (J.diagram P X) (op S)) :
          (a : CD (P.obj (op X))) → CD ((J.plusObj P).obj (op X)))
        x :
      CD ((J.plusObj P).obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P X) (op S)) :
          (a : CD (multiequalizer (S.index P))) → CD (colimit (J.diagram P X)))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
            (Meq.mk (FD := FD) (CD := CD) S x) :
          ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))) :
      CD (colimit (J.diagram P X)))

Tactic:
delta Cover.toMultiequalizer

Premises used: CategoryTheory.GrothendieckTopology.Cover.toMultiequalizer
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
rw :
  Eq (α := CD ((J.plusObj P).obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P X) (op S)) :
          (a : CD ((J.diagram P X).obj (op S))) → CD ((J.plusObj P).obj (op X)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map e.op) :
              (a : CD (multiequalizer (⊤.index P))) → CD ((J.diagram P X).obj (op S)))
            ((ConcreteCategory.hom (FC := FD) (CC := CD)
                    (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X))
                      (fun (I : (Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯) :
                  (a : CD (P.obj (op X))) → CD (multiequalizer (⊤.index P)))
                x :
              CD (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤) (Cover.index ⊤ P))) :
          CD ((J.diagram P X).obj (op S))) :
      CD ((J.plusObj P).obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P X) (op S)) :
          (a : CD (multiequalizer (S.index P))) → CD (colimit (J.diagram P X)))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
            (Meq.mk (FD := FD) (CD := CD) S x) :
          ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))) :
      CD (colimit (J.diagram P X)))
⊢ Eq (α := CD ((J.plusObj P).obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X))
                (fun (I : (Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯ ≫
              (J.diagram P X).map e.op ≫ colimit.ι (J.diagram P X) (op S)) :
          (a : CD (P.obj (op X))) → CD ((J.plusObj P).obj (op X)))
        x :
      CD ((J.plusObj P).obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P X) (op S)) :
          (a : CD (multiequalizer (S.index P))) → CD (colimit (J.diagram P X)))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
            (Meq.mk (FD := FD) (CD := CD) S x) :
          ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))) :
      CD (colimit (J.diagram P X)))

Tactic:
rw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply]

Premises used: CategoryTheory.ConcreteCategory.comp_apply
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
h :
  Eq (α := CD ((J.diagram P X).obj (op S)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map e.op) :
          (a : CD (multiequalizer (⊤.index P))) → CD ((J.diagram P X).obj (op S)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD)
                (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X))
                  (fun (I : (Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯) :
              (a : CD (P.obj (op X))) → CD (multiequalizer (⊤.index P)))
            x :
          CD (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤) (Cover.index ⊤ P))) :
      CD ((J.diagram P X).obj (op S)))
    ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
        (Meq.mk (FD := FD) (CD := CD) S x) :
      ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P)))
⊢ Eq (α := CD ((J.plusObj P).obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P X) (op S)) :
          (a : CD ((J.diagram P X).obj (op S))) → CD ((J.plusObj P).obj (op X)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map e.op) :
              (a : CD (multiequalizer (⊤.index P))) → CD ((J.diagram P X).obj (op S)))
            ((ConcreteCategory.hom (FC := FD) (CC := CD)
                    (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X))
                      (fun (I : (Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯) :
                  (a : CD (P.obj (op X))) → CD (multiequalizer (⊤.index P)))
                x :
              CD (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤) (Cover.index ⊤ P))) :
          CD ((J.diagram P X).obj (op S))) :
      CD ((J.plusObj P).obj (op X)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P X) (op S)) :
          (a : CD (multiequalizer (S.index P))) → CD (colimit (J.diagram P X)))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
            (Meq.mk (FD := FD) (CD := CD) S x) :
          ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))) :
      CD (colimit (J.diagram P X)))

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
h :
  Eq (α := CD (multiequalizer (S.index P)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (Multiequalizer.lift (S.index P)
              (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤) (Cover.index ⊤ P))
              (fun (I : S.Arrow) ↦ Multiequalizer.ι (Cover.index ⊤ P) (I.map e)) ⋯) :
          (a : CD (multiequalizer (⊤.index P))) → CD (multiequalizer (S.index P)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD)
                (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X))
                  (fun (I : Cover.Arrow.{v, u} (C := C) (X := X) (J := J) ⊤) ↦ P.map I.f.op) ⋯) :
              (a : CD (P.obj (op X))) → CD (multiequalizer (⊤.index P)))
            x :
          CD (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤) (Cover.index ⊤ P))) :
      CD (multiequalizer (S.index P)))
    ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
        (Meq.mk (FD := FD) (CD := CD) S x) :
      ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P)))
⊢ Eq (α := CD ((J.diagram P X).obj (op S)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map e.op) :
          (a : CD (multiequalizer (⊤.index P))) → CD ((J.diagram P X).obj (op S)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD)
                (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X))
                  (fun (I : (Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤).L) ↦ P.map I.f.op) ⋯) :
              (a : CD (P.obj (op X))) → CD (multiequalizer (⊤.index P)))
            x :
          CD (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤) (Cover.index ⊤ P))) :
      CD ((J.diagram P X).obj (op S)))
    ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
        (Meq.mk (FD := FD) (CD := CD) S x) :
      ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P)))

Tactic:
dsimp [diagram]

Premises used: CategoryTheory.GrothendieckTopology.diagram
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
i : S.shape.L
h :
  (ConcreteCategory.hom (FC := FD) (CC := CD) (P.map (Cover.Arrow.map i e).f.op) :
        (a : CD (P.obj (op X))) → CD ((S.index P).left i))
      x =
    (↑(Meq.mk (FD := FD) (CD := CD) S x) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i
⊢ Eq (α := CD ((S.index P).left i))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (Multiequalizer.ι (S.index P) i) :
          (a : CD (multiequalizer (S.index P))) → CD ((S.index P).left i))
        ((ConcreteCategory.hom (FC := FD) (CC := CD)
                (Multiequalizer.lift (S.index P)
                  (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤) (Cover.index ⊤ P))
                  (fun (I : S.Arrow) ↦ Multiequalizer.ι (Cover.index ⊤ P) (I.map e)) ⋯) :
              (a : CD (multiequalizer (⊤.index P))) → CD (multiequalizer (S.index P)))
            ((ConcreteCategory.hom (FC := FD) (CC := CD)
                    (Multiequalizer.lift (Cover.index ⊤ P) (P.obj (op X))
                      (fun (I : Cover.Arrow.{v, u} (C := C) (X := X) (J := J) ⊤) ↦ P.map I.f.op) ⋯) :
                  (a : CD (P.obj (op X))) → CD (multiequalizer (⊤.index P)))
                x :
              CD (multiequalizer (J := Cover.shape.{v, u} (C := C) (X := X) (J := J) ⊤) (Cover.index ⊤ P))) :
          CD (multiequalizer (S.index P))) :
      CD ((S.index P).left i))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (Multiequalizer.ι (S.index P) i) :
          (a : CD (multiequalizer (S.index P))) → CD ((S.index P).left i))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
            (Meq.mk (FD := FD) (CD := CD) S x) :
          ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))) :
      CD ((S.index P).left i))

Tactic:
simp only [← ConcreteCategory.comp_apply, Category.assoc, Multiequalizer.lift_ι,
    Meq.equiv_symm_eq_apply]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.Meq.equiv_symm_eq_apply, CategoryTheory.Limits.Multiequalizer.lift_ι
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
i : S.shape.L
⊢ (ConcreteCategory.hom (FC := FD) (CC := CD) (P.map (Cover.Arrow.map i e).f.op) :
        (a : CD (P.obj (op X))) → CD ((S.index P).left i))
      x =
    (↑(Meq.mk (FD := FD) (CD := CD) S x) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x : Meq (FD := FD) (CD := CD) P S
I : S.Arrow
dsimp :
  Eq (α := CD (colimit (J := (J.Cover I.Y)ᵒᵖ) (J.diagram P I.Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (CategoryStruct.comp (Y :=
              multiequalizer (J := Cover.shape.{v, u} (C := C) (X := I.Y) (J := J) ⊤) (Cover.index ⊤ P))
              (Cover.toMultiequalizer ⊤ P) (colimit.ι (J.diagram P I.Y) (op ⊤))) :
          (a : CD (P.obj (op I.Y))) → CD (colimit (J.diagram P I.Y)))
        ((↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) I) :
      CD (colimit (J := (J.Cover I.Y)ᵒᵖ) (J.diagram P I.Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (CategoryStruct.comp (Y := colimit ((J.pullback I.f.op.unop).op ⋙ J.diagram P I.Y))
              (colimMap (J.diagramPullback P I.f.op.unop))
              (colimit.pre (J.diagram P I.Y) (J.pullback I.f.op.unop).op)) :
          (a : CD (colimit (J.diagram P X))) → CD (colimit (J.diagram P I.Y)))
        (mk (FD := FD) (CD := CD) x) :
      CD (colimit (J := (J.Cover I.Y)ᵒᵖ) (J.diagram P I.Y)))
⊢ Eq (α := CD ((J.plusObj P).obj (op I.Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (NatTrans.app (J.toPlus P) (op I.Y)) :
          (a : CD (P.obj (op I.Y))) → CD ((J.plusObj P).obj (op I.Y)))
        ((↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) I) :
      CD ((J.plusObj P).obj (op I.Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map I.f.op) :
          (a : CD ((J.plusObj P).obj (op X))) → CD ((J.plusObj P).obj (op I.Y)))
        (mk (FD := FD) (CD := CD) x) :
      CD ((J.plusObj P).obj (op I.Y)))

Tactic:
dsimp only [toPlus, plusObj]

Premises used: CategoryTheory.GrothendieckTopology.toPlus, CategoryTheory.GrothendieckTopology.plusObj