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)
inst_3 : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
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))
I : S.Relation
⊢ Eq.{t + 1} (α := CD (P.obj (op I.r.Z)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.r.g₁.op) :
          (a : CD (P.obj (op I.fst.Y))) → CD (P.obj (op I.r.Z)))
        ((fun (I : S.Arrow) ↦
            ((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))))
          I.fst) :
      CD (P.obj (op I.r.Z)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.r.g₂.op) :
          (a : CD (P.obj (op I.snd.Y))) → CD (P.obj (op I.r.Z)))
        ((fun (I : S.Arrow) ↦
            ((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))))
          I.snd) :
      CD (P.obj (op I.r.Z)))

Tactic:
simp only [← ConcreteCategory.comp_apply, ← P.map_comp, ← op_comp, I.r.w]

Premises used: CategoryTheory.op_comp, CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.Functor.map_comp, CategoryTheory.GrothendieckTopology.Cover.Relation.r, CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.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)
inst_3 : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
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))
I : S.Arrow
⊢ (↑(mk (FD := FD) (CD := CD) S x) : (I : S.Arrow) → ToType (P.obj (op I.Y))) I =
    (ConcreteCategory.hom (FC := FD) (CC := CD) (P.map I.f.op) : (a : CD (P.obj (op X))) → CD (P.obj (op I.Y))) x

Tactic:
rfl

Premises used: 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)
inst_3 : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_4 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
inst_5 : HasMultiequalizer (S.index P)
x : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))
I : S.Arrow
⊢ Eq.{t + 1} (α := ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op I.Y)))
    ((↑((equiv (FD := FD) (CD := CD) P S : (a : ToType (multiequalizer (S.index P))) → Meq P S) x) :
          (I : S.Arrow) → ToType (P.obj (op I.Y)))
        I :
      ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op I.Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (Multiequalizer.ι (S.index P) I) :
          (a : CD (multiequalizer (S.index P))) → CD ((S.index P).left I))
        x :
      CD ((S.index P).left I))

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, 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)
inst_3 : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_4 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
inst_5 : HasMultiequalizer (S.index P)
x : Meq (FD := FD) (CD := CD) P S
I : S.Arrow
⊢ (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 (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))) I

Tactic:
simp [← GrothendieckTopology.Cover.index_left, ← equiv_apply]

Premises used: CategoryTheory.GrothendieckTopology.Cover.index_left, CategoryTheory.Meq.equiv_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)
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
dsimp :
  Eq.{t + 1} (α := CD (colimit (J.diagram P Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (CategoryStruct.comp (Y := colimit ((J.pullback f).op ⋙ J.diagram P Y)) (colimMap (J.diagramPullback P f))
              (colimit.pre (J.diagram P Y) (J.pullback f).op)) :
          (a : CD (colimit (J.diagram P X))) → CD (colimit (J.diagram P Y)))
        ((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)))
                x :
              ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (S.index P))) :
          CD (colimit (J.diagram P X))) :
      CD (colimit (J.diagram P Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P Y) (op (S.pullback f))) :
          (a : CD (multiequalizer ((S.pullback f).index P))) → CD (colimit (J.diagram P Y)))
        ((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))) :
      CD (colimit (J.diagram P Y)))
⊢ Eq (α := CD ((J.plusObj P).obj (op Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map f.op) :
          (a : CD ((J.plusObj P).obj (op X))) → CD ((J.plusObj P).obj (op Y)))
        (mk (FD := FD) (CD := CD) x) :
      CD ((J.plusObj P).obj (op Y)))
    (mk (FD := FD) (CD := CD) (x.pullback (FD := FD) (CD := CD) f) :
      ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op Y)))

Tactic:
dsimp [mk, plusObj]

Premises used: CategoryTheory.GrothendieckTopology.plusObj, 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)
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
h :
  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)))
⊢ Eq.{t + 1} (α := CD (colimit (J.diagram P Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P Y) ((J.pullback f).op.obj (op S))) :
          (a : CD (((J.pullback f).op ⋙ J.diagram P Y).obj (op S))) → CD (colimit (J.diagram P Y)))
        ((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))) :
      CD (colimit (J.diagram P Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD) (colimit.ι (J.diagram P Y) (op (S.pullback f))) :
          (a : CD (multiequalizer ((S.pullback f).index P))) → CD (colimit (J.diagram P Y)))
        ((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))) :
      CD (colimit (J.diagram P Y)))

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)
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
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))))
⊢ 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)))

Tactic:
apply (Meq.equiv P _).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)
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
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) ⋯) :
          (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
⊢ 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))

Tactic:
simp only [Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_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)
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
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) ⋯) :
                  (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
⊢ (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

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)
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
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 := ⋯ : S.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

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]

Premises used: CategoryTheory.GrothendieckTopology.Cover.index_left, CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.Limits.Multifork.ofι_pt, CategoryTheory.Limits.Multifork.ofι_π_app, CategoryTheory.Limits.limit.lift_π, CategoryTheory.GrothendieckTopology.pullback_obj, CategoryTheory.Meq.equiv_apply, CategoryTheory.Meq.pullback_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)
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
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 := ⋯ }
⊢ ((@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 }

Tactic:
rw [dsimp% Meq.equiv_symm_eq_apply x i.base]

Premises used: CategoryTheory.GrothendieckTopology.Cover.Arrow.base, CategoryTheory.Meq.equiv_symm_eq_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)
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
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 := ⋯ }
⊢ (↑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 := ⋯ }

Tactic:
cases i