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)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms.{w', w, t, t + 1} (forget D (FC := FD) (CC := CD))
P : Functor.{v, w', u, w} Cᵒᵖ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))),
    (∀ (I : S.Arrow),
        Eq (α := CD (P.obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y)))
              x :
            CD (P.obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y)))
              y :
            CD (P.obj (op I.Y)))) →
      x = y
X : C
S : J.Cover X
x y : Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)) ((J.plusObj P).obj (op X))
h :
  Eq (α :=
    (fun (X : Type t) ↦ X)
      (Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)) (multiequalizer (S.index (J.plusObj P)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Functor.map (forget D (FC := FD) (CC := CD)) (S.toMultiequalizer (J.plusObj P))) :
          (a : (fun (X : Type t) ↦ X) ((forget D).obj ((J.plusObj P).obj (op X)))) →
            (fun (X : Type t) ↦ X) ((forget D).obj (multiequalizer (S.index (J.plusObj P)))))
        x :
      (fun (X : Type t) ↦ X)
        (Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)) (multiequalizer (S.index (J.plusObj P)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Functor.map (forget D (FC := FD) (CC := CD)) (S.toMultiequalizer (J.plusObj P))) :
          (a : (fun (X : Type t) ↦ X) ((forget D).obj ((J.plusObj P).obj (op X)))) →
            (fun (X : Type t) ↦ X) ((forget D).obj (multiequalizer (S.index (J.plusObj P)))))
        y :
      (fun (X : Type t) ↦ X)
        (Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)) (multiequalizer (S.index (J.plusObj P)))))
left :
  ∀ (I : S.Arrow),
    Eq (α := 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)))
          x :
        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)))
          y :
        CD ((J.plusObj P).obj (op I.Y)))
⊢ x = y

Tactic:
apply sep P S _ _

Premises used: CategoryTheory.GrothendieckTopology.Plus.sep
-- 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)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms.{w', w, t, t + 1} (forget D (FC := FD) (CC := CD))
P : Functor.{v, w', u, w} Cᵒᵖ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))),
    (∀ (I : S.Arrow),
        Eq (α := CD (P.obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y)))
              x :
            CD (P.obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y)))
              y :
            CD (P.obj (op I.Y)))) →
      x = y
X : C
S : J.Cover X
x :
  ToType.{t, w', w, u_1} (FC := FD) (CC := Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)))
    (multiequalizer (S.index (J.plusObj P)))
right :
  ∀ (t : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X)))
    (ht :
      Meq.mk (FD := FD) (CD := CD) S t =
        (Meq.equiv (FD := FD) (CD := CD) (J.plusObj P) S :
            (a : ToType (multiequalizer (S.index (J.plusObj P)))) → Meq (J.plusObj P) S)
          x),
    ∃ (a :
      (fun (X : Type t) ↦ X)
        (Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)) ((J.plusObj P).obj (op X)))),
      (ConcreteCategory.hom (FC := TypeCat.Fun)
              (Functor.map (forget D (FC := FD) (CC := CD)) (S.toMultiequalizer (J.plusObj P))) :
            (a : (fun (X : Type t) ↦ X) ((forget D).obj ((J.plusObj P).obj (op X)))) →
              (fun (X : Type t) ↦ X) ((forget D).obj (multiequalizer (S.index (J.plusObj P)))))
          a =
        x
⊢ ∃ (a :
    (fun (X : Type t) ↦ X) (Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)) ((J.plusObj P).obj (op X)))),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (Functor.map (forget D (FC := FD) (CC := CD)) (S.toMultiequalizer (J.plusObj P))) :
          (a : (fun (X : Type t) ↦ X) ((forget D).obj ((J.plusObj P).obj (op X)))) →
            (fun (X : Type t) ↦ X) ((forget D).obj (multiequalizer (S.index (J.plusObj P)))))
        a =
      x

Tactic:
obtain ⟨t, ht⟩ := exists_of_sep P hsep X S (Meq.equiv _ _ x)

Premises used: CategoryTheory.Meq.equiv, CategoryTheory.GrothendieckTopology.Plus.exists_of_sep, DFunLike.coe
-- 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)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms.{w', w, t, t + 1} (forget D (FC := FD) (CC := CD))
P : Functor.{v, w', u, w} Cᵒᵖ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))),
    (∀ (I : S.Arrow),
        Eq (α := CD (P.obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y)))
              x :
            CD (P.obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y)))
              y :
            CD (P.obj (op I.Y)))) →
      x = y
X : C
S : J.Cover X
x :
  ToType.{t, w', w, u_1} (FC := FD) (CC := Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)))
    (multiequalizer (S.index (J.plusObj P)))
t : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))
ht :
  Meq.mk (FD := FD) (CD := CD) S t =
    (Meq.equiv (FD := FD) (CD := CD) (J.plusObj P) S :
        (a : ToType (multiequalizer (S.index (J.plusObj P)))) → Meq (J.plusObj P) S)
      x
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Functor.map (forget D (FC := FD) (CC := CD)) (S.toMultiequalizer (J.plusObj P))) :
        (a : (fun (X : Type t) ↦ X) ((forget D).obj ((J.plusObj P).obj (op X)))) →
          (fun (X : Type t) ↦ X) ((forget D).obj (multiequalizer (S.index (J.plusObj P)))))
      t =
    x
⊢ ∃ (a :
    (fun (X : Type t) ↦ X) (Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)) ((J.plusObj P).obj (op X)))),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (Functor.map (forget D (FC := FD) (CC := CD)) (S.toMultiequalizer (J.plusObj P))) :
          (a : (fun (X : Type t) ↦ X) ((forget D).obj ((J.plusObj P).obj (op X)))) →
            (fun (X : Type t) ↦ X) ((forget D).obj (multiequalizer (S.index (J.plusObj P)))))
        a =
      x

Tactic:
use t
-- 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)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms.{w', w, t, t + 1} (forget D (FC := FD) (CC := CD))
P : Functor.{v, w', u, w} Cᵒᵖ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))),
    (∀ (I : S.Arrow),
        Eq (α := CD (P.obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y)))
              x :
            CD (P.obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y)))
              y :
            CD (P.obj (op I.Y)))) →
      x = y
X : C
S : J.Cover X
x :
  ToType.{t, w', w, u_1} (FC := FD) (CC := Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)))
    (multiequalizer (S.index (J.plusObj P)))
t : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))
ht :
  Meq.mk (FD := FD) (CD := CD) S t =
    (Meq.equiv (FD := FD) (CD := CD) (J.plusObj P) S :
        (a : ToType (multiequalizer (S.index (J.plusObj P)))) → Meq (J.plusObj P) S)
      x
h :
  Eq (α := Meq (FD := FD) (CD := CD) (J.plusObj P) S)
    ((Meq.equiv (FD := FD) (CD := CD) (J.plusObj P) S :
          (a : ToType (multiequalizer (S.index (J.plusObj P)))) → Meq (J.plusObj P) S)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (Functor.map (forget D (FC := FD) (CC := CD)) (S.toMultiequalizer (J.plusObj P))) :
            (a : (fun (X : Type t) ↦ X) ((forget D).obj ((J.plusObj P).obj (op X)))) →
              (fun (X : Type t) ↦ X) ((forget D).obj (multiequalizer (S.index (J.plusObj P)))))
          t) :
      Meq (FD := FD) (CD := CD) (J.plusObj P) S)
    ((Meq.equiv (FD := FD) (CD := CD) (J.plusObj P) S :
          (a : ToType (multiequalizer (S.index (J.plusObj P)))) → Meq (J.plusObj P) S)
        x :
      Meq (FD := FD) (CD := CD) (J.plusObj P) S)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Functor.map (forget D (FC := FD) (CC := CD)) (S.toMultiequalizer (J.plusObj P))) :
        (a : (fun (X : Type t) ↦ X) ((forget D).obj ((J.plusObj P).obj (op X)))) →
          (fun (X : Type t) ↦ X) ((forget D).obj (multiequalizer (S.index (J.plusObj P)))))
      t =
    x

Tactic:
apply (Meq.equiv (D := D) _ _).injective

Premises used: CategoryTheory.Meq.equiv, Equiv.injective
-- 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)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms.{w', w, t, t + 1} (forget D (FC := FD) (CC := CD))
P : Functor.{v, w', u, w} Cᵒᵖ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))),
    (∀ (I : S.Arrow),
        Eq (α := CD (P.obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y)))
              x :
            CD (P.obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y)))
              y :
            CD (P.obj (op I.Y)))) →
      x = y
X : C
S : J.Cover X
x :
  ToType.{t, w', w, u_1} (FC := FD) (CC := Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)))
    (multiequalizer (S.index (J.plusObj P)))
t : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))
ht :
  Meq.mk (FD := FD) (CD := CD) S t =
    (Meq.equiv (FD := FD) (CD := CD) (J.plusObj P) S :
        (a : ToType (multiequalizer (S.index (J.plusObj P)))) → Meq (J.plusObj P) S)
      x
h :
  (Meq.equiv (FD := FD) (CD := CD) (J.plusObj P) S :
        (a : ToType (multiequalizer (S.index (J.plusObj P)))) → Meq (J.plusObj P) S)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Functor.map (forget D (FC := FD) (CC := CD)) (S.toMultiequalizer (J.plusObj P))) :
          (a : (fun (X : Type t) ↦ X) ((forget D).obj ((J.plusObj P).obj (op X)))) →
            (fun (X : Type t) ↦ X) ((forget D).obj (multiequalizer (S.index (J.plusObj P)))))
        t) =
    Meq.mk (FD := FD) (CD := CD) S t
⊢ Eq (α := Meq (FD := FD) (CD := CD) (J.plusObj P) S)
    ((Meq.equiv (FD := FD) (CD := CD) (J.plusObj P) S :
          (a : ToType (multiequalizer (S.index (J.plusObj P)))) → Meq (J.plusObj P) S)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (Functor.map (forget D (FC := FD) (CC := CD)) (S.toMultiequalizer (J.plusObj P))) :
            (a : (fun (X : Type t) ↦ X) ((forget D).obj ((J.plusObj P).obj (op X)))) →
              (fun (X : Type t) ↦ X) ((forget D).obj (multiequalizer (S.index (J.plusObj P)))))
          t) :
      Meq (FD := FD) (CD := CD) (J.plusObj P) S)
    ((Meq.equiv (FD := FD) (CD := CD) (J.plusObj P) S :
          (a : ToType (multiequalizer (S.index (J.plusObj P)))) → Meq (J.plusObj P) S)
        x :
      Meq (FD := FD) (CD := CD) (J.plusObj P) S)

Tactic:
rw [← ht]
-- 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)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms.{w', w, t, t + 1} (forget D (FC := FD) (CC := CD))
P : Functor.{v, w', u, w} Cᵒᵖ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))),
    (∀ (I : S.Arrow),
        Eq (α := CD (P.obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y)))
              x :
            CD (P.obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y)))
              y :
            CD (P.obj (op I.Y)))) →
      x = y
X : C
S : J.Cover X
x :
  ToType.{t, w', w, u_1} (FC := FD) (CC := Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)))
    (multiequalizer (S.index (J.plusObj P)))
t : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))
ht :
  Meq.mk (FD := FD) (CD := CD) S t =
    (Meq.equiv (FD := FD) (CD := CD) (J.plusObj P) S :
        (a : ToType (multiequalizer (S.index (J.plusObj P)))) → Meq (J.plusObj P) S)
      x
h :
  ∀ (i : S.Arrow),
    (↑((Meq.equiv (FD := FD) (CD := CD) (J.plusObj P) S :
                (a : ToType (multiequalizer (S.index (J.plusObj P)))) → Meq (J.plusObj P) S)
              ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (Functor.map (forget D (FC := FD) (CC := CD)) (S.toMultiequalizer (J.plusObj P))) :
                  (a : (fun (X : Type t) ↦ X) ((forget D).obj ((J.plusObj P).obj (op X)))) →
                    (fun (X : Type t) ↦ X) ((forget D).obj (multiequalizer (S.index (J.plusObj P)))))
                t)) :
          (I : S.Arrow) → ToType ((J.plusObj P).obj (op I.Y)))
        i =
      (↑(Meq.mk (FD := FD) (CD := CD) S t) : (I : S.Arrow) → ToType ((J.plusObj P).obj (op I.Y))) i
⊢ (Meq.equiv (FD := FD) (CD := CD) (J.plusObj P) S :
        (a : ToType (multiequalizer (S.index (J.plusObj P)))) → Meq (J.plusObj P) S)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Functor.map (forget D (FC := FD) (CC := CD)) (S.toMultiequalizer (J.plusObj P))) :
          (a : (fun (X : Type t) ↦ X) ((forget D).obj ((J.plusObj P).obj (op X)))) →
            (fun (X : Type t) ↦ X) ((forget D).obj (multiequalizer (S.index (J.plusObj P)))))
        t) =
    Meq.mk (FD := FD) (CD := CD) S t

Tactic:
ext i
-- 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)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms.{w', w, t, t + 1} (forget D (FC := FD) (CC := CD))
P : Functor.{v, w', u, w} Cᵒᵖ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))),
    (∀ (I : S.Arrow),
        Eq (α := CD (P.obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y)))
              x :
            CD (P.obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y)))
              y :
            CD (P.obj (op I.Y)))) →
      x = y
X : C
S : J.Cover X
x :
  ToType.{t, w', w, u_1} (FC := FD) (CC := Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)))
    (multiequalizer (S.index (J.plusObj P)))
t : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))
ht :
  Meq.mk (FD := FD) (CD := CD) S t =
    (Meq.equiv (FD := FD) (CD := CD) (J.plusObj P) S :
        (a : ToType (multiequalizer (S.index (J.plusObj P)))) → Meq (J.plusObj P) S)
      x
i : S.Arrow
h :
  (ConcreteCategory.hom (FC := FD) (CC := CD) (Multiequalizer.ι (S.index (J.plusObj P)) i) :
        (a : CD (multiequalizer (S.index (J.plusObj P)))) → CD ((J.plusObj P).obj (op i.Y)))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (S.toMultiequalizer (J.plusObj P)) :
            (a : CD ((J.plusObj P).obj (op X))) → CD (multiequalizer (S.index (J.plusObj P))))
          t :
        CD (multiequalizer (S.index (J.plusObj P)))) =
    (↑(Meq.mk (FD := FD) (CD := CD) S t) : (I : S.Arrow) → ToType ((J.plusObj P).obj (op I.Y))) i
⊢ (↑((Meq.equiv (FD := FD) (CD := CD) (J.plusObj P) S :
              (a : ToType (multiequalizer (S.index (J.plusObj P)))) → Meq (J.plusObj P) S)
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (Functor.map (forget D (FC := FD) (CC := CD)) (S.toMultiequalizer (J.plusObj P))) :
                (a : (fun (X : Type t) ↦ X) ((forget D).obj ((J.plusObj P).obj (op X)))) →
                  (fun (X : Type t) ↦ X) ((forget D).obj (multiequalizer (S.index (J.plusObj P)))))
              t)) :
        (I : S.Arrow) → ToType ((J.plusObj P).obj (op I.Y)))
      i =
    (↑(Meq.mk (FD := FD) (CD := CD) S t) : (I : S.Arrow) → ToType ((J.plusObj P).obj (op I.Y))) i

Tactic:
dsimp
-- 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)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
inst_7 : Functor.ReflectsIsomorphisms.{w', w, t, t + 1} (forget D (FC := FD) (CC := CD))
P : Functor.{v, w', u, w} Cᵒᵖ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op X))),
    (∀ (I : S.Arrow),
        Eq (α := CD (P.obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y)))
              x :
            CD (P.obj (op I.Y)))
          ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y)))
              y :
            CD (P.obj (op I.Y)))) →
      x = y
X : C
S : J.Cover X
x :
  ToType.{t, w', w, u_1} (FC := FD) (CC := Functor.obj.{w', t, w, t + 1} (forget D (FC := FD) (CC := CD)))
    (multiequalizer (S.index (J.plusObj P)))
t : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))
ht :
  Meq.mk (FD := FD) (CD := CD) S t =
    (Meq.equiv (FD := FD) (CD := CD) (J.plusObj P) S :
        (a : ToType (multiequalizer (S.index (J.plusObj P)))) → Meq (J.plusObj P) S)
      x
i : S.Arrow
h :
  (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)))
      t =
    (↑(Meq.mk (FD := FD) (CD := CD) S t) : (I : S.Arrow) → ToType ((J.plusObj P).obj (op I.Y))) i
⊢ (ConcreteCategory.hom (FC := FD) (CC := CD) (Multiequalizer.ι (S.index (J.plusObj P)) i) :
        (a : CD (multiequalizer (S.index (J.plusObj P)))) → CD ((J.plusObj P).obj (op i.Y)))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (S.toMultiequalizer (J.plusObj P)) :
            (a : CD ((J.plusObj P).obj (op X))) → CD (multiequalizer (S.index (J.plusObj P))))
          t :
        CD (multiequalizer (S.index (J.plusObj P)))) =
    (↑(Meq.mk (FD := FD) (CD := CD) S t) : (I : S.Arrow) → ToType ((J.plusObj P).obj (op I.Y))) i

Tactic:
rw [← ConcreteCategory.comp_apply, Multiequalizer.lift_ι]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.Limits.Multiequalizer.lift_ι