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))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S T : J.Cover X
x : Meq (FD := FD) (CD := CD) P S
y : Meq (FD := FD) (CD := CD) P T
h :
  Eq (α := ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))) (mk (FD := FD) (CD := CD) x)
    (mk (FD := FD) (CD := CD) y)
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
hh :
  Eq.{t + 1} (α := CD ((J.diagram P X).obj W))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map h1) :
          (a : CD ((J.diagram P X).obj (op S))) → CD ((J.diagram P X).obj W))
        ((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.diagram P X).obj W))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map h2) :
          (a : CD ((J.diagram P X).obj (op T))) → CD ((J.diagram P X).obj W))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P T) : (a : Meq P T) → ToType (multiequalizer (T.index P))) y :
          ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (T.index P))) :
      CD ((J.diagram P X).obj W))
h₁ :
  ∀ (I : (unop W).Arrow),
    (↑(x.refine (FD := FD) (CD := CD) h1.unop) : (I : (unop W).Arrow) → ToType (P.obj (op I.Y))) I =
      (↑(y.refine (FD := FD) (CD := CD) h2.unop) : (I : (unop W).Arrow) → ToType (P.obj (op I.Y))) I
⊢ x.refine (FD := FD) (CD := CD) h1.unop = y.refine (FD := FD) (CD := CD) h2.unop

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))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S T : J.Cover X
x : Meq (FD := FD) (CD := CD) P S
y : Meq (FD := FD) (CD := CD) P T
h :
  Eq (α := ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))) (mk (FD := FD) (CD := CD) x)
    (mk (FD := FD) (CD := CD) y)
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
Y : C
f : Y ⟶ X
hf : (↑(unop W) : Sieve X).arrows f
hh :
  Eq.{t + 1} (α := CD (((unop W).index P).left { Y := Y, f := f, hf := hf }))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (Multiequalizer.ι ((unop W).index P) { Y := Y, f := f, hf := hf : (unop W).Arrow }) :
          (a : CD (multiequalizer ((unop W).index P))) → CD (((unop W).index P).left { Y := Y, f := f, hf := hf }))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map h1) :
              (a : CD ((J.diagram P X).obj (op S))) → CD ((J.diagram P X).obj W))
            ((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.diagram P X).obj W)) :
      CD (((unop W).index P).left { Y := Y, f := f, hf := hf }))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (Multiequalizer.ι ((unop W).index P) { Y := Y, f := f, hf := hf : (unop W).Arrow }) :
          (a : CD (multiequalizer ((unop W).index P))) → CD (((unop W).index P).left { Y := Y, f := f, hf := hf }))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map h2) :
              (a : CD ((J.diagram P X).obj (op T))) → CD ((J.diagram P X).obj W))
            ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P T) : (a : Meq P T) → ToType (multiequalizer (T.index P)))
                y :
              ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (T.index P))) :
          CD ((J.diagram P X).obj W)) :
      CD (((unop W).index P).left { Y := Y, f := f, hf := hf }))
e_1 :
  ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op { Y := Y, f := f, hf := hf : (unop W).Arrow }.Y)) =
    CD (((unop W).index P).left { Y := Y, f := f, hf := hf })
⊢ (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y)))
      { Y := { Y := Y, f := f, hf := hf : (unop W).Arrow }.Y, f := { Y := Y, f := f, hf := hf : (unop W).Arrow }.f,
        hf := ⋯ : S.Arrow } =
    (↑x : (I : S.Arrow) → ToType (P.obj (op I.Y))) ({ Y := Y, f := f, hf := hf : (unop W).Arrow }.map h1.unop)

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)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S T : J.Cover X
x : Meq (FD := FD) (CD := CD) P S
y : Meq (FD := FD) (CD := CD) P T
h :
  Eq (α := ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))) (mk (FD := FD) (CD := CD) x)
    (mk (FD := FD) (CD := CD) y)
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
Y : C
f : Y ⟶ X
hf : (↑(unop W) : Sieve X).arrows f
hh :
  Eq.{t + 1} (α := CD (((unop W).index P).left { Y := Y, f := f, hf := hf }))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (Multiequalizer.ι ((unop W).index P) { Y := Y, f := f, hf := hf : (unop W).Arrow }) :
          (a : CD (multiequalizer ((unop W).index P))) → CD (((unop W).index P).left { Y := Y, f := f, hf := hf }))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map h1) :
              (a : CD ((J.diagram P X).obj (op S))) → CD ((J.diagram P X).obj W))
            ((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.diagram P X).obj W)) :
      CD (((unop W).index P).left { Y := Y, f := f, hf := hf }))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (Multiequalizer.ι ((unop W).index P) { Y := Y, f := f, hf := hf : (unop W).Arrow }) :
          (a : CD (multiequalizer ((unop W).index P))) → CD (((unop W).index P).left { Y := Y, f := f, hf := hf }))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map h2) :
              (a : CD ((J.diagram P X).obj (op T))) → CD ((J.diagram P X).obj W))
            ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P T) : (a : Meq P T) → ToType (multiequalizer (T.index P)))
                y :
              ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (T.index P))) :
          CD ((J.diagram P X).obj W)) :
      CD (((unop W).index P).left { Y := Y, f := f, hf := hf }))
e_1 :
  ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op { Y := Y, f := f, hf := hf : (unop W).Arrow }.Y)) =
    CD (((unop W).index P).left { Y := Y, f := f, hf := hf })
⊢ (↑y : (I : T.Arrow) → ToType (P.obj (op I.Y)))
      { Y := { Y := Y, f := f, hf := hf : (unop W).Arrow }.Y, f := { Y := Y, f := f, hf := hf : (unop W).Arrow }.f,
        hf := ⋯ : T.Arrow } =
    (↑y : (I : T.Arrow) → ToType (P.obj (op I.Y))) ({ Y := Y, f := f, hf := hf : (unop W).Arrow }.map h2.unop)

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)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S_1 T : J.Cover X
x : Meq (FD := FD) (CD := CD) P S_1
y : Meq (FD := FD) (CD := CD) P T
S : J.Cover X
h1 : S ⟶ S_1
h2 : S ⟶ T
e : x.refine (FD := FD) (CD := CD) h1 = y.refine (FD := FD) (CD := CD) h2
mpr :
  ∃ (k : (J.Cover X)ᵒᵖ) (f : op S_1 ⟶ k) (g : op T ⟶ k),
    Eq.{t + 1} (α := CD ((J.diagram P X).obj k))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map f) :
            (a : CD ((J.diagram P X).obj (op S_1))) → CD ((J.diagram P X).obj k))
          ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S_1) :
                (a : Meq P S_1) → ToType (multiequalizer (S_1.index P)))
              x :
            ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S_1.index P))) :
        CD ((J.diagram P X).obj k))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map g) :
            (a : CD ((J.diagram P X).obj (op T))) → CD ((J.diagram P X).obj k))
          ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P T) : (a : Meq P T) → ToType (multiequalizer (T.index P))) y :
            ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (T.index P))) :
        CD ((J.diagram P X).obj k))
⊢ Eq (α := ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))) (mk (FD := FD) (CD := CD) x)
    (mk (FD := FD) (CD := CD) y)

Tactic:
apply Concrete.colimit_rep_eq_of_exists (C := D)

Premises used: CategoryTheory.Limits.Concrete.colimit_rep_eq_of_exists
-- 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))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S_1 T : J.Cover X
x : Meq (FD := FD) (CD := CD) P S_1
y : Meq (FD := FD) (CD := CD) P T
S : J.Cover X
h1 : S ⟶ S_1
h2 : S ⟶ T
e : x.refine (FD := FD) (CD := CD) h1 = y.refine (FD := FD) (CD := CD) h2
h :
  Eq.{t + 1} (α := CD ((J.diagram P X).obj (op S)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map h1.op) :
          (a : CD ((J.diagram P X).obj (op S_1))) → CD ((J.diagram P X).obj (op S)))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S_1) : (a : Meq P S_1) → ToType (multiequalizer (S_1.index P)))
            x :
          ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S_1.index P))) :
      CD ((J.diagram P X).obj (op S)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map h2.op) :
          (a : CD ((J.diagram P X).obj (op T))) → CD ((J.diagram P X).obj (op S)))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P T) : (a : Meq P T) → ToType (multiequalizer (T.index P))) y :
          ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (T.index P))) :
      CD ((J.diagram P X).obj (op S)))
⊢ ∃ (k : (J.Cover X)ᵒᵖ) (f : op S_1 ⟶ k) (g : op T ⟶ k),
    Eq.{t + 1} (α := CD ((J.diagram P X).obj k))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map f) :
            (a : CD ((J.diagram P X).obj (op S_1))) → CD ((J.diagram P X).obj k))
          ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S_1) :
                (a : Meq P S_1) → ToType (multiequalizer (S_1.index P)))
              x :
            ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S_1.index P))) :
        CD ((J.diagram P X).obj k))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map g) :
            (a : CD ((J.diagram P X).obj (op T))) → CD ((J.diagram P X).obj k))
          ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P T) : (a : Meq P T) → ToType (multiequalizer (T.index P))) y :
            ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (T.index P))) :
        CD ((J.diagram P X).obj k))

Tactic:
use op S, h1.op, h2.op

Premises used: Quiver.Hom.op, Opposite.op
-- 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))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S_1 T : J.Cover X
x : Meq (FD := FD) (CD := CD) P S_1
y : Meq (FD := FD) (CD := CD) P T
S : J.Cover X
h1 : S ⟶ S_1
h2 : S ⟶ T
e : x.refine (FD := FD) (CD := CD) h1 = y.refine (FD := FD) (CD := CD) h2
i : (unop (op S)).shape.L
⊢ (↑(x.refine (FD := FD) (CD := CD) h1) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i =
    (↑(y.refine (FD := FD) (CD := CD) h2) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i

Tactic:
apply_fun fun ee => ee i at e
-- 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))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S_1 T : J.Cover X
x : Meq (FD := FD) (CD := CD) P S_1
y : Meq (FD := FD) (CD := CD) P T
S : J.Cover X
h1 : S ⟶ S_1
h2 : S ⟶ T
i : (unop (op S)).shape.L
e :
  (↑(x.refine (FD := FD) (CD := CD) h1) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i =
    (↑(y.refine (FD := FD) (CD := CD) h2) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i
⊢ (↑(x.refine (FD := FD) (CD := CD) h1) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i =
    (↑(y.refine (FD := FD) (CD := CD) h2) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i

Tactic:
e
-- 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))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S_1 T : J.Cover X
x : Meq (FD := FD) (CD := CD) P S_1
y : Meq (FD := FD) (CD := CD) P T
S : J.Cover X
h1 : S ⟶ S_1
h2 : S ⟶ T
i : (unop (op S)).shape.L
e :
  (↑(x.refine (FD := FD) (CD := CD) h1) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i =
    (↑(y.refine (FD := FD) (CD := CD) h2) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i
e_1 : CD (((unop (op S)).index P).left i) = ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op i.Y))
h :
  (ConcreteCategory.hom (FC := FD) (CC := CD) (Multiequalizer.ι (S.index P) i) :
        (a : CD (multiequalizer (S.index P))) → CD (P.obj (op i.Y)))
      ((ConcreteCategory.hom (FC := FD) (CC := CD)
              (Multiequalizer.lift (S.index P) (multiequalizer (S_1.index P))
                (fun (I : S.Arrow) ↦ Multiequalizer.ι (S_1.index P) (I.map h1)) ⋯) :
            (a : CD (multiequalizer (S_1.index P))) → CD (multiequalizer (S.index P)))
          ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S_1) :
                (a : Meq P S_1) → ToType (multiequalizer (S_1.index P)))
              x :
            ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S_1.index P))) :
        CD (multiequalizer (S.index P))) =
    (↑x : (I : S_1.Arrow) → ToType (P.obj (op I.Y))) { Y := i.Y, f := i.f, hf := ⋯ : S_1.Arrow }
⊢ (ConcreteCategory.hom (FC := FD) (CC := CD) (Multiequalizer.ι ((unop (op S)).index P) i) :
        (a : CD (multiequalizer ((unop (op S)).index P))) → CD (((unop (op S)).index P).left i))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map h1.op) :
            (a : CD ((J.diagram P X).obj (op S_1))) → CD ((J.diagram P X).obj (op S)))
          ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S_1) :
                (a : Meq P S_1) → ToType (multiequalizer (S_1.index P)))
              x :
            ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S_1.index P))) :
        CD ((J.diagram P X).obj (op S))) =
    (↑(x.refine (FD := FD) (CD := CD) h1) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i

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)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S_1 T : J.Cover X
x : Meq (FD := FD) (CD := CD) P S_1
y : Meq (FD := FD) (CD := CD) P T
S : J.Cover X
h1 : S ⟶ S_1
h2 : S ⟶ T
i : (unop (op S)).shape.L
e :
  (↑(x.refine (FD := FD) (CD := CD) h1) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i =
    (↑(y.refine (FD := FD) (CD := CD) h2) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i
e_1 : CD (((unop (op S)).index P).left i) = ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op i.Y))
h :
  ((@ConcreteCategory.hom.{t, w', w, u_1} _ inst_1 FD CD _ _ _ _
            (Multiequalizer.ι (S_1.index P) (Cover.Arrow.map i h1)) :
          FD (multiequalizer (S_1.index P)) (P.obj (op i.Y))) :
        (a : CD (multiequalizer (S_1.index P))) → CD (P.obj (op i.Y)))
      ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S_1) : (a : Meq P S_1) → ToType (multiequalizer (S_1.index P)))
          x :
        ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S_1.index P))) =
    (↑x : (I : S_1.Arrow) → ToType (P.obj (op I.Y))) { Y := i.Y, f := i.f, hf := ⋯ : S_1.Arrow }
⊢ (ConcreteCategory.hom (FC := FD) (CC := CD) (Multiequalizer.ι (S.index P) i) :
        (a : CD (multiequalizer (S.index P))) → CD (P.obj (op i.Y)))
      ((ConcreteCategory.hom (FC := FD) (CC := CD)
              (Multiequalizer.lift (S.index P) (multiequalizer (S_1.index P))
                (fun (I : S.Arrow) ↦ Multiequalizer.ι (S_1.index P) (I.map h1)) ⋯) :
            (a : CD (multiequalizer (S_1.index P))) → CD (multiequalizer (S.index P)))
          ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S_1) :
                (a : Meq P S_1) → ToType (multiequalizer (S_1.index P)))
              x :
            ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S_1.index P))) :
        CD (multiequalizer (S.index P))) =
    (↑x : (I : S_1.Arrow) → ToType (P.obj (op I.Y))) { Y := i.Y, f := i.f, hf := ⋯ : S_1.Arrow }

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

Premises used: CategoryTheory.ConcreteCategory.comp_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)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S_1 T : J.Cover X
x : Meq (FD := FD) (CD := CD) P S_1
y : Meq (FD := FD) (CD := CD) P T
S : J.Cover X
h1 : S ⟶ S_1
h2 : S ⟶ T
i : (unop (op S)).shape.L
e :
  (↑(x.refine (FD := FD) (CD := CD) h1) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i =
    (↑(y.refine (FD := FD) (CD := CD) h2) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i
e_1 : CD (((unop (op S)).index P).left i) = ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op i.Y))
h :
  (↑x : (I : S_1.Arrow) → ToType (P.obj (op I.Y))) (Cover.Arrow.map i h1) =
    (↑x : (I : S_1.Arrow) → ToType (P.obj (op I.Y))) { Y := i.Y, f := i.f, hf := ⋯ }
⊢ ((@ConcreteCategory.hom.{t, w', w, u_1} _ inst_1 FD CD _ _ _ _
            (Multiequalizer.ι (S_1.index P) (Cover.Arrow.map i h1)) :
          FD (multiequalizer (S_1.index P)) (P.obj (op i.Y))) :
        (a : CD (multiequalizer (S_1.index P))) → CD (P.obj (op i.Y)))
      ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P S_1) : (a : Meq P S_1) → ToType (multiequalizer (S_1.index P)))
          x :
        ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S_1.index P))) =
    (↑x : (I : S_1.Arrow) → ToType (P.obj (op I.Y))) { Y := i.Y, f := i.f, hf := ⋯ : S_1.Arrow }

Tactic:
erw [Meq.equiv_symm_eq_apply]

Premises used: CategoryTheory.Meq.equiv_symm_eq_apply