awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C (Type u)
X Y S : Type u_2
f : X ⟶ S
g : Y ⟶ S
H :
  ∀ [inst : HasPullback f g],
    Function.Surjective (α := (fun (X : Type u_2) ↦ X) (Functor.obj (𝟭 (Type u_2)) (pullback f g))) (β :=
      (fun (X : Type u_2) ↦ X)
        (pullback (X := Functor.obj (𝟭 (Type u_2)) X) (Functor.map (𝟭 (Type u_2)) f) (Functor.map (𝟭 (Type u_2)) g)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison (𝟭 (Type u_2)) f g)) :
        (a : (fun (X : Type u_2) ↦ X) ((𝟭 (Type u_2)).obj (pullback f g))) →
          (fun (X : Type u_2) ↦ X) (pullback ((𝟭 (Type u_2)).map f) ((𝟭 (Type u_2)).map g)))
⊢ ∀ [inst : HasPullback f g],
    Function.Surjective (α := (fun (X : Type u_2) ↦ X) (Functor.obj (𝟭 (Type u_2)) (pullback f g))) (β :=
      (fun (X : Type u_2) ↦ X)
        (pullback (X := Functor.obj (𝟭 (Type u_2)) X) (Functor.map (𝟭 (Type u_2)) f) (Functor.map (𝟭 (Type u_2)) g)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison (𝟭 (Type u_2)) f g)) :
        (a : (fun (X : Type u_2) ↦ X) ((𝟭 (Type u_2)).obj (pullback f g))) →
          (fun (X : Type u_2) ↦ X) (pullback ((𝟭 (Type u_2)).map f) ((𝟭 (Type u_2)).map g)))

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C (Type u)
X Y S : Type u_2
f : X ⟶ S
g : Y ⟶ S
inst_1 : HasPullback f g
⊢ Function.Surjective (α := (fun (X : Type u_2) ↦ X) (Functor.obj (𝟭 (Type u_2)) (pullback f g))) (β :=
    (fun (X : Type u_2) ↦ X)
      (pullback (X := Functor.obj (𝟭 (Type u_2)) X) (Functor.map (𝟭 (Type u_2)) f) (Functor.map (𝟭 (Type u_2)) g)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison (𝟭 (Type u_2)) f g)) :
      (a : (fun (X : Type u_2) ↦ X) ((𝟭 (Type u_2)).obj (pullback f g))) →
        (fun (X : Type u_2) ↦ X) (pullback ((𝟭 (Type u_2)).map f) ((𝟭 (Type u_2)).map g)))

Tactic:
surjective_of_epi _

Premises used: CategoryTheory.surjective_of_epi
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C (Type u)
X Y S : Type u_2
f : X ⟶ S
g : Y ⟶ S
inst_1 : HasPullback f g
⊢ Function.Surjective (α := (fun (X : Type u_2) ↦ X) (Functor.obj (𝟭 (Type u_2)) (pullback f g))) (β :=
    (fun (X : Type u_2) ↦ X)
      (pullback (X := Functor.obj (𝟭 (Type u_2)) X) (Functor.map (𝟭 (Type u_2)) f) (Functor.map (𝟭 (Type u_2)) g)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (pullbackComparison (𝟭 (Type u_2)) f g)) :
      (a : (fun (X : Type u_2) ↦ X) ((𝟭 (Type u_2)).obj (pullback f g))) →
        (fun (X : Type u_2) ↦ X) (pullback ((𝟭 (Type u_2)).map f) ((𝟭 (Type u_2)).map g)))

Tactic:
exact surjective_of_epi _

Premises used: CategoryTheory.surjective_of_epi
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
W : J.Cover X
i : W.Arrow
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) (op W))
a b : K
f : a ⟶ b
dsimp :
  𝟙 E.pt ≫ E.π.app b ≫ Multiequalizer.ι (W.index (F.obj b)) i =
    (E.π.app a ≫ Multiequalizer.ι (W.index (F.obj a)) i) ≫ (F.map f).app (op i.Y)
⊢ Functor.map (Functor.obj (Functor.const K) E.pt) f ≫ E.π.app b ≫ Multiequalizer.ι (W.index (F.obj b)) i =
    (E.π.app a ≫ Multiequalizer.ι (W.index (F.obj a)) i) ≫ (F ⋙ Functor.obj (evaluation Cᵒᵖ D) (op i.Y)).map f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
W : J.Cover X
i : W.Arrow
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) (op W))
a b : K
f : a ⟶ b
rw :
  (E.π.app a ≫ (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) (op W)).map f) ≫
      Multiequalizer.ι (W.index (F.obj b)) i =
    E.π.app a ≫ Multiequalizer.ι (W.index (F.obj a)) i ≫ (F.map f).app (op i.Y)
⊢ 𝟙 E.pt ≫ E.π.app b ≫ Multiequalizer.ι (W.index (F.obj b)) i =
    (E.π.app a ≫ Multiequalizer.ι (W.index (F.obj a)) i) ≫ (F.map f).app (op i.Y)

Tactic:
rw [Category.id_comp, Category.assoc, ← E.w f]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cone.w, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
W : J.Cover X
i : W.Arrow
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) (op W))
a b : K
f : a ⟶ b
dsimp :
  CategoryStruct.comp (Y := multiequalizer (W.index (F.obj b)))
      (E.π.app a ≫
        Multiequalizer.lift (W.index (F.obj b)) (multiequalizer (W.index (F.obj a)))
          (fun (x : W.Arrow) ↦ Multiequalizer.ι (W.index (F.obj a)) x ≫ (F.map f).app (op x.Y)) ⋯)
      (Multiequalizer.ι (W.index (F.obj b)) i) =
    E.π.app a ≫ Multiequalizer.ι (W.index (F.obj a)) i ≫ (F.map f).app (op i.Y)
⊢ (E.π.app a ≫ (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) (op W)).map f) ≫
      Multiequalizer.ι (W.index (F.obj b)) i =
    E.π.app a ≫ Multiequalizer.ι (W.index (F.obj a)) i ≫ (F.map f).app (op i.Y)

Tactic:
dsimp [diagramNatTrans]

Premises used: CategoryTheory.GrothendieckTopology.diagramNatTrans
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
W : J.Cover X
i : W.Arrow
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) (op W))
a b : K
f : a ⟶ b
⊢ CategoryStruct.comp (Y := multiequalizer (W.index (F.obj b)))
      (E.π.app a ≫
        Multiequalizer.lift (W.index (F.obj b)) (multiequalizer (W.index (F.obj a)))
          (fun (x : W.Arrow) ↦ Multiequalizer.ι (W.index (F.obj a)) x ≫ (F.map f).app (op x.Y)) ⋯)
      (Multiequalizer.ι (W.index (F.obj b)) i) =
    E.π.app a ≫ Multiequalizer.ι (W.index (F.obj a)) i ≫ (F.map f).app (op i.Y)

Tactic:
simp only [Multiequalizer.lift_ι, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Multiequalizer.lift_ι
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
inst_4 : HasLimitsOfShape.{s, s, t, w} K D
W : (J.Cover X)ᵒᵖ
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
i : (unop W).Arrow
k : K
⊢ CategoryStruct.comp (Y := (limit F).obj (op i.Y)) (liftToDiagramLimitObjAux F E i : E.pt ⟶ (limit F).obj (op i.Y))
      (NatTrans.app (limit.π F k) (op i.Y) : (limit F).obj (op i.Y) ⟶ (F.obj k).obj (op i.Y)) =
    E.π.app k ≫ Multiequalizer.ι ((unop W).index (F.obj k)) i

Tactic:
IsLimit.fac _ _ _

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.limit, CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
inst_4 : HasLimitsOfShape.{s, s, t, w} K D
W : (J.Cover X)ᵒᵖ
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
i : (unop W).shape.R
dsimp :
  liftToDiagramLimitObjAux F E i.fst ≫ (limit F).map i.r.g₁.op =
    liftToDiagramLimitObjAux F E i.snd ≫ (limit F).map i.r.g₂.op
⊢ liftToDiagramLimitObjAux F E ((unop W).shape.fst i) ≫ ((unop W).index (limit F)).fst i =
    liftToDiagramLimitObjAux F E ((unop W).shape.snd i) ≫ ((unop W).index (limit F)).snd i

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
inst_4 : HasLimitsOfShape.{s, s, t, w} K D
W : (J.Cover X)ᵒᵖ
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
i : (unop W).shape.R
w :
  ∀ (k : K),
    (liftToDiagramLimitObjAux F E i.fst ≫ (limit F).map i.r.g₁.op) ≫ NatTrans.app (limit.π F k) (op i.r.Z) =
      (liftToDiagramLimitObjAux F E i.snd ≫ (limit F).map i.r.g₂.op) ≫ NatTrans.app (limit.π F k) (op i.r.Z)
⊢ liftToDiagramLimitObjAux F E i.fst ≫ (limit F).map i.r.g₁.op =
    liftToDiagramLimitObjAux F E i.snd ≫ (limit F).map i.r.g₂.op

Tactic:
ext k
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
inst_4 : HasLimitsOfShape.{s, s, t, w} K D
W : (J.Cover X)ᵒᵖ
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
i : (unop W).shape.R
k : K
w :
  E.π.app k ≫ Multiequalizer.ι ((unop W).index (F.obj k)) i.fst ≫ (F.obj k).map i.r.g₁.op =
    E.π.app k ≫ Multiequalizer.ι ((unop W).index (F.obj k)) i.snd ≫ (F.obj k).map i.r.g₂.op
⊢ (liftToDiagramLimitObjAux F E i.fst ≫ (limit F).map i.r.g₁.op) ≫ NatTrans.app (limit.π F k) (op i.r.Z) =
    (liftToDiagramLimitObjAux F E i.snd ≫ (limit F).map i.r.g₂.op) ≫ NatTrans.app (limit.π F k) (op i.r.Z)

Tactic:
simp only [Category.assoc, NatTrans.naturality, liftToDiagramLimitObjAux_fac_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux_fac_assoc, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
inst_4 : HasLimitsOfShape.{s, s, t, w} K D
W : (J.Cover X)ᵒᵖ
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
i : (unop W).shape.R
k : K
w :
  E.π.app k ≫ Multiequalizer.ι ((unop W).index (F.obj k)) ((unop W).shape.snd i) ≫ ((unop W).index (F.obj k)).snd i =
    E.π.app k ≫ Multiequalizer.ι ((unop W).index (F.obj k)) i.snd ≫ (F.obj k).map i.r.g₂.op
⊢ E.π.app k ≫ Multiequalizer.ι ((unop W).index (F.obj k)) i.fst ≫ (F.obj k).map i.r.g₁.op =
    E.π.app k ≫ Multiequalizer.ι ((unop W).index (F.obj k)) i.snd ≫ (F.obj k).map i.r.g₂.op

Tactic:
erw [Multiequalizer.condition]

Premises used: CategoryTheory.Limits.Multiequalizer.condition
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
inst_4 : HasLimitsOfShape.{s, s, t, w} K D
W : (J.Cover X)ᵒᵖ
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
i : (unop W).shape.R
k : K
⊢ E.π.app k ≫ Multiequalizer.ι ((unop W).index (F.obj k)) ((unop W).shape.snd i) ≫ ((unop W).index (F.obj k)).snd i =
    E.π.app k ≫ Multiequalizer.ι ((unop W).index (F.obj k)) i.snd ≫ (F.obj k).map i.r.g₂.op

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
inst_4 : HasLimitsOfShape.{s, s, t, w} K D
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
W : (J.Cover X)ᵒᵖ
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
k : K
dsimp :
  CategoryStruct.comp (Y := multiequalizer ((unop W).index (limit F)))
      (liftToDiagramLimitObj F E : E.pt ⟶ (J.diagram (limit F) X).obj W)
      (Multiequalizer.lift ((unop W).index (F.obj k)) (multiequalizer ((unop W).index (limit F)))
          (fun (x : (unop W).Arrow) ↦
            Multiequalizer.ι ((unop W).index (limit F)) x ≫ NatTrans.app (limit.π F k) (op x.Y))
          ⋯ :
        multiequalizer ((unop W).index (limit F)) ⟶ multiequalizer ((unop W).index (F.obj k))) =
    E.π.app k
⊢ CategoryStruct.comp (Y :=
      Cone.pt (F := F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
        (Functor.mapCone (J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W) (limit.cone F)))
      (liftToDiagramLimitObj F E : E.pt ⟶ (J.diagram (limit F) X).obj W)
      (NatTrans.app
          (Cone.π (Functor.mapCone (J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W) (limit.cone F)))
          k :
        Functor.obj.{s, t, s, w}
            (Functor.obj (Functor.const K)
              (Cone.pt (F := F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
                (Functor.mapCone (J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W) (limit.cone F))))
            k ⟶
          (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W).obj k) =
    E.π.app k

Tactic:
dsimp [diagramNatTrans]

Premises used: CategoryTheory.GrothendieckTopology.diagramNatTrans
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
inst_4 : HasLimitsOfShape.{s, s, t, w} K D
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
W : (J.Cover X)ᵒᵖ
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
k : K
⊢ CategoryStruct.comp (Y := multiequalizer ((unop W).index (limit F)))
      (liftToDiagramLimitObj F E : E.pt ⟶ (J.diagram (limit F) X).obj W)
      (Multiequalizer.lift ((unop W).index (F.obj k)) (multiequalizer ((unop W).index (limit F)))
          (fun (x : (unop W).Arrow) ↦
            Multiequalizer.ι ((unop W).index (limit F)) x ≫ NatTrans.app (limit.π F k) (op x.Y))
          ⋯ :
        multiequalizer ((unop W).index (limit F)) ⟶ multiequalizer ((unop W).index (F.obj k))) =
    E.π.app k

Tactic:
Multiequalizer.hom_ext _ _ _ (fun a => ?_)

Premises used: CategoryTheory.Limits.Multiequalizer.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
inst_4 : HasLimitsOfShape.{s, s, t, w} K D
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
W : (J.Cover X)ᵒᵖ
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
k : K
refine :
  ∀ (a : (unop W).shape.L),
    CategoryStruct.comp (Y := multiequalizer ((unop W).index (F.obj k)))
        (CategoryStruct.comp (Y := multiequalizer ((unop W).index (limit F)))
          (liftToDiagramLimitObj F E : E.pt ⟶ (J.diagram (limit F) X).obj W)
          (Multiequalizer.lift ((unop W).index (F.obj k)) (multiequalizer ((unop W).index (limit F)))
              (fun (x : (unop W).Arrow) ↦
                Multiequalizer.ι ((unop W).index (limit F)) x ≫ NatTrans.app (limit.π F k) (op x.Y))
              ⋯ :
            multiequalizer ((unop W).index (limit F)) ⟶ multiequalizer ((unop W).index (F.obj k))))
        (Multiequalizer.ι ((unop W).index (F.obj k)) a) =
      E.π.app k ≫ Multiequalizer.ι ((unop W).index (F.obj k)) a
⊢ CategoryStruct.comp (Y := multiequalizer ((unop W).index (limit F)))
      (liftToDiagramLimitObj F E : E.pt ⟶ (J.diagram (limit F) X).obj W)
      (Multiequalizer.lift ((unop W).index (F.obj k)) (multiequalizer ((unop W).index (limit F)))
          (fun (x : (unop W).Arrow) ↦
            Multiequalizer.ι ((unop W).index (limit F)) x ≫ NatTrans.app (limit.π F k) (op x.Y))
          ⋯ :
        multiequalizer ((unop W).index (limit F)) ⟶ multiequalizer ((unop W).index (F.obj k))) =
    E.π.app k

Tactic:
refine Multiequalizer.hom_ext _ _ _ (fun a => ?_)

Premises used: CategoryTheory.Limits.Multiequalizer.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
inst_4 : HasLimitsOfShape.{s, s, t, w} K D
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
W : (J.Cover X)ᵒᵖ
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
k : K
a : (unop W).shape.L
⊢ CategoryStruct.comp (Y := multiequalizer ((unop W).index (F.obj k)))
      (CategoryStruct.comp (Y := multiequalizer ((unop W).index (limit F)))
        (liftToDiagramLimitObj F E : E.pt ⟶ (J.diagram (limit F) X).obj W)
        (Multiequalizer.lift ((unop W).index (F.obj k)) (multiequalizer ((unop W).index (limit F)))
            (fun (x : (unop W).Arrow) ↦
              Multiequalizer.ι ((unop W).index (limit F)) x ≫ NatTrans.app (limit.π F k) (op x.Y))
            ⋯ :
          multiequalizer ((unop W).index (limit F)) ⟶ multiequalizer ((unop W).index (F.obj k))))
      (Multiequalizer.ι ((unop W).index (F.obj k)) a) =
    E.π.app k ≫ Multiequalizer.ι ((unop W).index (F.obj k)) a

Tactic:
simp only [Multiequalizer.lift_ι, Multiequalizer.lift_ι_assoc, Category.assoc,
            liftToDiagramLimitObjAux_fac]

Premises used: CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux_fac, CategoryTheory.Category.assoc, CategoryTheory.Limits.Multiequalizer.lift_ι_assoc, CategoryTheory.Limits.Multiequalizer.lift_ι
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
inst_4 : HasLimitsOfShape.{s, s, t, w} K D
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
W : (J.Cover X)ᵒᵖ
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
m :
  E.pt ⟶
    Cone.pt (F := F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
      (Functor.mapCone (J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W) (limit.cone F))
hm :
  ∀ (j : K),
    m ≫
        NatTrans.app
          (Cone.π (Functor.mapCone (J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W) (limit.cone F)))
          j =
      E.π.app j
⊢ m = liftToDiagramLimitObj F E

Tactic:
Multiequalizer.hom_ext _ _ _ (fun a => limit_obj_ext (fun j => ?_))

Premises used: CategoryTheory.Limits.limit_obj_ext, CategoryTheory.Functor.comp, CategoryTheory.Limits.limit, CategoryTheory.Limits.MulticospanIndex.multicospan, CategoryTheory.Limits.Multiequalizer.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
inst_4 : HasLimitsOfShape.{s, s, t, w} K D
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
W : (J.Cover X)ᵒᵖ
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
m :
  E.pt ⟶
    Cone.pt (F := F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
      (Functor.mapCone (J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W) (limit.cone F))
hm :
  ∀ (j : K),
    m ≫
        NatTrans.app
          (Cone.π (Functor.mapCone (J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W) (limit.cone F)))
          j =
      E.π.app j
refine :
  ∀ (a : (unop W).shape.L) (j : K),
    (m ≫ Multiequalizer.ι ((unop W).index (limit.cone F).pt) a) ≫ NatTrans.app (limit.π F j) (op a.Y) =
      CategoryStruct.comp (Y := multiequalizer ((unop W).index (limit.cone F).pt))
          (liftToDiagramLimitObj F E : E.pt ⟶ (J.diagram (limit F) X).obj W)
          (Multiequalizer.ι ((unop W).index (limit.cone F).pt) a :
            multiequalizer ((unop W).index (limit.cone F).pt) ⟶ ((unop W).index (limit.cone F).pt).left a) ≫
        NatTrans.app (limit.π F j) (op a.Y)
⊢ m = liftToDiagramLimitObj F E

Tactic:
refine Multiequalizer.hom_ext _ _ _ (fun a => limit_obj_ext (fun j => ?_))

Premises used: CategoryTheory.Limits.Multiequalizer.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.LeftExact
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{t, w} D
inst_2 : ∀ (P : Functor.{v, t, u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
K : Type s
inst_3 : SmallCategory K
inst_4 : HasLimitsOfShape.{s, s, t, w} K D
F : K ⥤ Functor.{v, t, u, w} Cᵒᵖ D
W : (J.Cover X)ᵒᵖ
E : Cone (F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
m :
  E.pt ⟶
    Cone.pt (F := F ⋙ J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W)
      (Functor.mapCone (J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W) (limit.cone F))
hm :
  ∀ (j : K),
    m ≫
        NatTrans.app
          (Cone.π (Functor.mapCone (J.diagramFunctor D X ⋙ Functor.obj (evaluation (J.Cover X)ᵒᵖ D) W) (limit.cone F)))
          j =
      E.π.app j
a : (unop W).shape.L
j : K
dsimp :
  (m ≫ Multiequalizer.ι ((unop W).index (limit F)) a) ≫ NatTrans.app (limit.π F j) (op a.Y) =
    CategoryStruct.comp (Y := multiequalizer ((unop W).index (limit F)))
        (Multiequalizer.lift ((unop W).index (limit F)) E.pt (liftToDiagramLimitObjAux F E) ⋯)
        (Multiequalizer.ι ((unop W).index (limit F)) a) ≫
      NatTrans.app (limit.π F j) (op a.Y)
⊢ (m ≫ Multiequalizer.ι ((unop W).index (limit.cone F).pt) a) ≫ NatTrans.app (limit.π F j) (op a.Y) =
    CategoryStruct.comp (Y := multiequalizer ((unop W).index (limit.cone F).pt))
        (liftToDiagramLimitObj F E : E.pt ⟶ (J.diagram (limit F) X).obj W)
        (Multiequalizer.ι ((unop W).index (limit.cone F).pt) a :
          multiequalizer ((unop W).index (limit.cone F).pt) ⟶ ((unop W).index (limit.cone F).pt).left a) ≫
      NatTrans.app (limit.π F j) (op a.Y)

Tactic:
dsimp [liftToDiagramLimitObj]

Premises used: CategoryTheory.GrothendieckTopology.liftToDiagramLimitObj