awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
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
⊢ Eq.{t + 1} (α := CD (((J.pullback f).op ⋙ J.diagram P Y).obj (op S)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (NatTrans.app (J.diagramPullback P f) (op S)) :
          (a : CD (multiequalizer (S.index P))) → CD (((J.pullback f).op ⋙ J.diagram P Y).obj (op S)))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P))) x :
          ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))) :
      CD (((J.pullback f).op ⋙ J.diagram P Y).obj (op S)))
    ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P (S.pullback f)) :
          (a : Meq P (S.pullback f)) → ToType (multiequalizer ((S.pullback f).index P)))
        (x.pullback (FD := FD) (CD := CD) f) :
      ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer ((S.pullback f).index P)))
have h : Eq (α := Meq (FD := FD) (CD := CD) P (unop ((J.pullback f).op.obj (op S))))
  ((Meq.equiv (FD := FD) (CD := CD) P (unop ((J.pullback f).op.obj (op S))) :
        (a : ToType (multiequalizer ((unop ((J.pullback f).op.obj (op S))).index P))) →
          Meq P (unop ((J.pullback f).op.obj (op S))))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) (NatTrans.app (J.diagramPullback P f) (op S)) :
          (a : CD (multiequalizer (S.index P))) → CD (((J.pullback f).op ⋙ J.diagram P Y).obj (op S)))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P))) x :
          ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P)))) :
    Meq (FD := FD) (CD := CD) P (unop ((J.pullback f).op.obj (op S))))
  ((Meq.equiv (FD := FD) (CD := CD) P (unop ((J.pullback f).op.obj (op S))) :
        (a : ToType (multiequalizer ((unop ((J.pullback f).op.obj (op S))).index P))) →
          Meq P (unop ((J.pullback f).op.obj (op S))))
      ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P (S.pullback f)) :
          (a : Meq P (S.pullback f)) → ToType (multiequalizer ((S.pullback f).index P)))
        (x.pullback (FD := FD) (CD := CD) f)) :
    Meq (FD := FD) (CD := CD) P (unop ((J.pullback f).op.obj (op S))))
Tactic: apply (Meq.equiv P _).injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
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
⊢ Eq (α := Meq (FD := FD) (CD := CD) P (S.pullback f))
    ((Meq.equiv (FD := FD) (CD := CD) P (S.pullback f) :
          (a : ToType (multiequalizer ((S.pullback f).index P))) → Meq P (S.pullback f))
        ((ConcreteCategory.hom (FC := FD) (CC := CD)
              (Multiequalizer.lift ((S.pullback f).index P) (multiequalizer (S.index P))
                (fun (I : (S.pullback f).Arrow) ↦ Multiequalizer.ι (S.index P) I.base) ⋯) :
            (a : CD (multiequalizer (S.index P))) → CD (multiequalizer ((S.pullback f).index P)))
          ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P))) x :
            ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P)))) :
      Meq (FD := FD) (CD := CD) P (S.pullback f))
    ((Meq.equiv (FD := FD) (CD := CD) P (S.pullback f) :
          (a : ToType (multiequalizer ((S.pullback f).index P))) → Meq P (S.pullback f))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P (S.pullback f)) :
            (a : Meq P (S.pullback f)) → ToType (multiequalizer ((S.pullback f).index P)))
          (x.pullback (FD := FD) (CD := CD) f)) :
      Meq (FD := FD) (CD := CD) P (S.pullback f))
have h : (Meq.equiv (FD := FD) (CD := CD) P (S.pullback f) :
      (a : ToType (multiequalizer ((S.pullback f).index P))) → Meq P (S.pullback f))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
          (Multiequalizer.lift ((S.pullback f).index P) (multiequalizer (S.index P))
            (fun (I : (S.pullback f).Arrow) ↦ Multiequalizer.ι (S.index P) I.base) sorry) :
        (a : CD (multiequalizer (S.index P))) → CD (multiequalizer ((S.pullback f).index P)))
      ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P))) x :
        ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P)))) =
  x.pullback (FD := FD) (CD := CD) f
Tactic: simp only [Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
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
⊢ (Meq.equiv (FD := FD) (CD := CD) P (S.pullback f) :
        (a : ToType (multiequalizer ((S.pullback f).index P))) → Meq P (S.pullback f))
      ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (Multiequalizer.lift ((S.pullback f).index P) (multiequalizer (S.index P))
              (fun (I : (S.pullback f).Arrow) ↦ Multiequalizer.ι (S.index P) I.base) ⋯) :
          (a : CD (multiequalizer (S.index P))) → CD (multiequalizer ((S.pullback f).index P)))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P))) x :
          ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P)))) =
    x.pullback (FD := FD) (CD := CD) f
have h : ∀ (i : (S.pullback f).Arrow),
  (↑((Meq.equiv (FD := FD) (CD := CD) P (S.pullback f) :
              (a : ToType (multiequalizer ((S.pullback f).index P))) → Meq P (S.pullback f))
            ((ConcreteCategory.hom (FC := FD) (CC := CD)
                  (Multiequalizer.lift ((S.pullback f).index P) (multiequalizer (S.index P))
                    (fun (I : (S.pullback f).Arrow) ↦ Multiequalizer.ι (S.index P) I.base) sorry) :
                (a : CD (multiequalizer (S.index P))) → CD (multiequalizer ((S.pullback f).index P)))
              ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
                  x :
                ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))))) :
        (I : (S.pullback f).Arrow) → ToType (P.obj (op I.Y)))
      i =
    (↑(x.pullback (FD := FD) (CD := CD) f) : (I : (S.pullback f).Arrow) → ToType (P.obj (op I.Y))) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
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
i : (S.pullback f).Arrow
⊢ (↑((Meq.equiv (FD := FD) (CD := CD) P (S.pullback f) :
              (a : ToType (multiequalizer ((S.pullback f).index P))) → Meq P (S.pullback f))
            ((ConcreteCategory.hom (FC := FD) (CC := CD)
                  (Multiequalizer.lift ((S.pullback f).index P) (multiequalizer (S.index P))
                    (fun (I : (S.pullback f).Arrow) ↦ Multiequalizer.ι (S.index P) I.base) ⋯) :
                (a : CD (multiequalizer (S.index P))) → CD (multiequalizer ((S.pullback f).index P)))
              ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P)))
                  x :
                ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))))) :
        (I : (S.pullback f).Arrow) → ToType (P.obj (op I.Y)))
      i =
    (↑(x.pullback (FD := FD) (CD := CD) f) : (I : (S.pullback f).Arrow) → ToType (P.obj (op I.Y))) i
have h : ((@ConcreteCategory.hom.{t, w', w, u_1} _ inst_1 FD CD _ _ _ _ (Multiequalizer.ι (S.index P) i.base) :
        FD (multiequalizer (S.index P)) (P.obj (op i.Y))) :
      (a : CD (multiequalizer (S.index P))) → CD (P.obj (op i.Y)))
    ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P))) x :
      ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))) =
  (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := i.Y, f := i.f ≫ f, hf := sorry : S.Arrow }
Tactic: simp only [Meq.equiv_apply, Cover.index_left, ← ConcreteCategory.comp_apply, limit.lift_π,
    Multifork.ofι_pt, Multifork.ofι_π_app, Meq.pullback_apply, pullback_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
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
i : (S.pullback f).Arrow
⊢ ((@ConcreteCategory.hom.{t, w', w, u_1} _ inst_1 FD CD _ _ _ _ (Multiequalizer.ι (S.index P) i.base) :
          FD (multiequalizer (S.index P)) (P.obj (op i.Y))) :
        (a : CD (multiequalizer (S.index P))) → CD (P.obj (op i.Y)))
      ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S) : (a : Meq P S) → ToType (multiequalizer (S.index P))) x :
        ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))) =
    (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := i.Y, f := i.f ≫ f, hf := ⋯ : S.Arrow }
have h : (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) i.base =
  (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := i.Y, f := i.f ≫ f, hf := sorry }
Tactic: rw [dsimp% Meq.equiv_symm_eq_apply x i.base]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
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
i : (S.pullback f).Arrow
⊢ (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) i.base =
    (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := i.Y, f := i.f ≫ f, hf := ⋯ }
have h : ∀ (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 := sorry }
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
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))
⊢ 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)))
have 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)))
Tactic: dsimp [mk, toPlus]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
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 ⋯
⊢ 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)))
have 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)))
Tactic: rw [← colimit.w _ e.op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
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 ⋯
⊢ 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)))
have 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) sorry ≫
            (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
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
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 ⋯
⊢ 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)))
have 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) sorry) :
                (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: rw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply]