awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
X : Type (max w u)
f_1 : (j : J) → (F.obj (op j)).obj j ⟶ X
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f_1 i = (F.obj (op j)).map g ≫ f_1 j
x_1 : chosenCoend F
j j' : J
f : j ⟶ j'
x : (F.obj (op j')).obj j
⊢ Eq (α := (fun (X : Type (max u w)) ↦ X) X)
    ((fun (j : (j : J) × (F.obj (op j)).obj j) ↦
        ((hom (FC := Fun) (f_1 (j.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))) :
              (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j.fst)).obj j.fst)) → (fun (X : Type (max u w)) ↦ X) X)
            (j.snd (β := fun (j : J) ↦ (F.obj (op j)).obj j)) :
          (fun (X : Type (max u w)) ↦ X) X))
      (Sigma.mk (β := fun (j : J) ↦ (F.obj (op j)).obj j) j
        ((Hom.hom ((F.map f.op).app j) : (a : (F.obj (op j')).obj j) → (F.obj (op j)).obj j) x)))
    ((fun (j : (j : J) × (F.obj (op j)).obj j) ↦
        ((hom (FC := Fun) (f_1 (j.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))) :
              (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j.fst)).obj j.fst)) → (fun (X : Type (max u w)) ↦ X) X)
            (j.snd (β := fun (j : J) ↦ (F.obj (op j)).obj j)) :
          (fun (X : Type (max u w)) ↦ X) X))
      (Sigma.mk (β := fun (j : J) ↦ (F.obj (op j)).obj j) j'
        ((Hom.hom ((F.obj (op j')).map f) : (a : (F.obj (op j')).obj j) → (F.obj (op j')).obj j') x)))

Tactic:
exact ConcreteCategory.congr_hom (hf f) _

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
X : Type (max w u)
f : (j : J) → (F.obj (op j)).obj j ⟶ X
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f i = (F.obj (op j)).map g ≫ f j
x : chosenCoend F
x_1 x_2 : (j : J) × (F.obj (op j)).obj j
h : Types.coendRel.{w, v, u} F x_1 x_2
mk :
  ∀ {j j' : J} (f_1 : j ⟶ j') (x : (F.obj (op j')).obj j),
    Eq (α := (fun (X : Type (max u w)) ↦ X) X)
      ((fun (j : (j : J) × (F.obj (op j)).obj j) ↦
          ((hom (FC := Fun) (f (j.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))) :
                (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j.fst)).obj j.fst)) → (fun (X : Type (max u w)) ↦ X) X)
              (j.snd (β := fun (j : J) ↦ (F.obj (op j)).obj j)) :
            (fun (X : Type (max u w)) ↦ X) X))
        (Sigma.mk (β := fun (j : J) ↦ (F.obj (op j)).obj j) j
          ((Hom.hom ((F.map f_1.op).app j) : (a : (F.obj (op j')).obj j) → (F.obj (op j)).obj j) x)))
      ((fun (j : (j : J) × (F.obj (op j)).obj j) ↦
          ((hom (FC := Fun) (f (j.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))) :
                (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j.fst)).obj j.fst)) → (fun (X : Type (max u w)) ↦ X) X)
              (j.snd (β := fun (j : J) ↦ (F.obj (op j)).obj j)) :
            (fun (X : Type (max u w)) ↦ X) X))
        (Sigma.mk (β := fun (j : J) ↦ (F.obj (op j)).obj j) j'
          ((Hom.hom ((F.obj (op j')).map f_1) : (a : (F.obj (op j')).obj j) → (F.obj (op j')).obj j') x)))
⊢ Eq (α := (fun (X : Type (max u w)) ↦ X) X)
    ((fun (j : (j : J) × (F.obj (op j)).obj j) ↦
        ((hom (FC := Fun) (f (j.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))) :
              (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j.fst)).obj j.fst)) → (fun (X : Type (max u w)) ↦ X) X)
            (j.snd (β := fun (j : J) ↦ (F.obj (op j)).obj j)) :
          (fun (X : Type (max u w)) ↦ X) X))
      x_1)
    ((fun (j : (j : J) × (F.obj (op j)).obj j) ↦
        ((hom (FC := Fun) (f (j.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))) :
              (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j.fst)).obj j.fst)) → (fun (X : Type (max u w)) ↦ X) X)
            (j.snd (β := fun (j : J) ↦ (F.obj (op j)).obj j)) :
          (fun (X : Type (max u w)) ↦ X) X))
      x_2)

Tactic:
cases h with | mk f x => exact ConcreteCategory.congr_hom (hf f) _

Premises used: CategoryTheory.ConcreteCategory.mk, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
X : Type (max w u)
f : (j : J) → (F.obj (op j)).obj j ⟶ X
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f i = (F.obj (op j)).map g ≫ f j
x : chosenCoend F
⊢ Eq (α := X) ((hom (FC := Fun) (desc f hf) : (a : chosenCoend F) → X) x : X)
    (Quot.lift (r := Types.coendRel.{w, v, u} F)
        (fun (j : (j : J) × (F.obj (op j)).obj j) ↦
          (hom (FC := Fun) (f (j.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))) :
              (a : (F.obj (op j.fst)).obj j.fst) → X)
            (j.snd (β := fun (j : J) ↦ (F.obj (op j)).obj j)))
        ⋯ x :
      X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : chosenCoend F
j j' : J
g : j ⟶ j'
y : (F.obj (op j')).obj j
a :
  Types.coendRel.{w, v, u} G
    (Sigma.mk (β := fun (j : J) ↦ (G.obj (op j)).obj j) j
      ((hom (FC := Fun) (NatTrans.app (f.app (op j)) j) :
          (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j)).obj j)) →
            (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
        ((Hom.hom ((F.map g.op).app j) : (a : (F.obj (op j')).obj j) → (F.obj (op j)).obj j) y)))
    (Sigma.mk (β := fun (j : J) ↦ (G.obj (op j)).obj j) j'
      ((hom (FC := Fun) (NatTrans.app (f.app (op j')) j') :
          (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j')) →
            (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
        ((Hom.hom ((F.obj (op j')).map g) : (a : (F.obj (op j')).obj j) → (F.obj (op j')).obj j') y)))
⊢ Eq (α := (fun (X : Type (max u w)) ↦ X) (chosenCoend G))
    ((fun (x : (j : J) × (F.obj (op j)).obj j) ↦
        (match (motive := (j : J) × (F.obj (op j)).obj j → (fun (X : Type (max u w)) ↦ X) (chosenCoend G)) x with
          | ⟨j, y⟩ =>
            Quot.mk (Types.coendRel.{w, v, u} G)
              (Sigma.mk (β := fun (j : J) ↦ (G.obj (op j)).obj j) j
                ((hom (FC := Fun) (NatTrans.app (f.app (op j)) j) :
                    (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j)).obj j)) →
                      (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
                  y)) :
          (fun (X : Type (max u w)) ↦ X) (chosenCoend G)))
      (Sigma.mk (β := fun (j : J) ↦ (F.obj (op j)).obj j) j
        ((Hom.hom ((F.map g.op).app j) : (a : (F.obj (op j')).obj j) → (F.obj (op j)).obj j) y)))
    ((fun (x : (j : J) × (F.obj (op j)).obj j) ↦
        (match (motive := (j : J) × (F.obj (op j)).obj j → (fun (X : Type (max u w)) ↦ X) (chosenCoend G)) x with
          | ⟨j, y⟩ =>
            Quot.mk (Types.coendRel.{w, v, u} G)
              (Sigma.mk (β := fun (j : J) ↦ (G.obj (op j)).obj j) j
                ((hom (FC := Fun) (NatTrans.app (f.app (op j)) j) :
                    (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j)).obj j)) →
                      (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
                  y)) :
          (fun (X : Type (max u w)) ↦ X) (chosenCoend G)))
      (Sigma.mk (β := fun (j : J) ↦ (F.obj (op j)).obj j) j'
        ((Hom.hom ((F.obj (op j')).map g) : (a : (F.obj (op j')).obj j) → (F.obj (op j')).obj j') y)))

Tactic:
apply Quot.sound

Premises used: Quot.sound
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : chosenCoend F
j j' : J
g : j ⟶ j'
y : (F.obj (op j')).obj j
a :
  ∃ (f_1 : j ⟶ j') (y_1 : (G.obj (op j')).obj j),
    Eq (α := (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
        ((hom (FC := Fun) ((G.map f_1.op).app j) :
              (a : (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j)) →
                (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
            y_1 :
          (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
        ((hom (FC := Fun) (NatTrans.app (f.app (op j)) j) :
              (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j)).obj j)) →
                (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
            ((Hom.hom ((F.map g.op).app j) : (a : (F.obj (op j')).obj j) → (F.obj (op j)).obj j) y) :
          (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j)) ∧
      Eq (α := (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
        ((hom (FC := Fun) ((G.obj (op j')).map f_1) :
              (a : (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j)) →
                (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
            y_1 :
          (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
        ((hom (FC := Fun) (NatTrans.app (f.app (op j')) j') :
              (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j')) →
                (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
            ((Hom.hom ((F.obj (op j')).map g) : (a : (F.obj (op j')).obj j) → (F.obj (op j')).obj j') y) :
          (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
⊢ Types.coendRel.{w, v, u} G
    (Sigma.mk (β := fun (j : J) ↦ (G.obj (op j)).obj j) j
      ((hom (FC := Fun) (NatTrans.app (f.app (op j)) j) :
          (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j)).obj j)) →
            (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
        ((Hom.hom ((F.map g.op).app j) : (a : (F.obj (op j')).obj j) → (F.obj (op j)).obj j) y)))
    (Sigma.mk (β := fun (j : J) ↦ (G.obj (op j)).obj j) j'
      ((hom (FC := Fun) (NatTrans.app (f.app (op j')) j') :
          (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j')) →
            (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
        ((Hom.hom ((F.obj (op j')).map g) : (a : (F.obj (op j')).obj j) → (F.obj (op j')).obj j') y)))

Tactic:
rw [Types.coendRel_iff]

Premises used: CategoryTheory.Limits.Types.coendRel_iff
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : chosenCoend F
j j' : J
g : j ⟶ j'
y : (F.obj (op j')).obj j
⊢ ∃ (f_1 : j ⟶ j') (y_1 : (G.obj (op j')).obj j),
    Eq (α := (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
        ((hom (FC := Fun) ((G.map f_1.op).app j) :
              (a : (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j)) →
                (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
            y_1 :
          (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
        ((hom (FC := Fun) (NatTrans.app (f.app (op j)) j) :
              (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j)).obj j)) →
                (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
            ((Hom.hom ((F.map g.op).app j) : (a : (F.obj (op j')).obj j) → (F.obj (op j)).obj j) y) :
          (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j)) ∧
      Eq (α := (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
        ((hom (FC := Fun) ((G.obj (op j')).map f_1) :
              (a : (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j)) →
                (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
            y_1 :
          (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
        ((hom (FC := Fun) (NatTrans.app (f.app (op j')) j') :
              (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j')) →
                (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
            ((Hom.hom ((F.obj (op j')).map g) : (a : (F.obj (op j')).obj j) → (F.obj (op j')).obj j') y) :
          (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))

Tactic:
⟨g, (f.app _).app _ y, ?_, ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, And.intro, Exists.intro, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : chosenCoend F
j j' : J
g : j ⟶ j'
y : (F.obj (op j')).obj j
⊢ Eq (α := (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
    ((hom (FC := Fun) ((G.map g.op).app j) :
          (a : (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j)) →
            (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
        ((hom (FC := Fun) (NatTrans.app (f.app (op j')) j) :
            (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j)) →
              (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j))
          y) :
      (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
    ((hom (FC := Fun) (NatTrans.app (f.app (op j)) j) :
          (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j)).obj j)) →
            (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))
        ((Hom.hom ((F.map g.op).app j) : (a : (F.obj (op j')).obj j) → (F.obj (op j)).obj j) y) :
      (fun (X : Type (max u w)) ↦ X) ((G.obj (op j)).obj j))

Tactic:
simp only [← NatTrans.comp_app_apply, f.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.NatTrans.comp_app_apply
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : chosenCoend F
j j' : J
g : j ⟶ j'
y : (F.obj (op j')).obj j
⊢ Eq (α := (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
    ((hom (FC := Fun) ((G.obj (op j')).map g) :
          (a : (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j)) →
            (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
        ((hom (FC := Fun) (NatTrans.app (f.app (op j')) j) :
            (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j)) →
              (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j))
          y) :
      (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
    ((hom (FC := Fun) (NatTrans.app (f.app (op j')) j') :
          (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j')) →
            (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))
        ((Hom.hom ((F.obj (op j')).map g) : (a : (F.obj (op j')).obj j) → (F.obj (op j')).obj j') y) :
      (fun (X : Type (max u w)) ↦ X) ((G.obj (op j')).obj j'))

Tactic:
simp [← NatTrans.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : chosenCoend F
⊢ Eq (α := Quot (Types.coendRel.{w, v, u} G))
    ((hom (FC := Fun) (map f) : (a : Quot (Types.coendRel F)) → Quot (Types.coendRel G)) x :
      Quot (Types.coendRel.{w, v, u} G))
    (Quot.lift (r := Types.coendRel.{w, v, u} F)
        (fun (x : (j : J) × (F.obj (op j)).obj j) ↦
          Quot.mk (Types.coendRel.{w, v, u} G)
            (Sigma.mk (β := fun (j : J) ↦ (G.obj (op j)).obj j) (x.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))
              ((hom (FC := Fun)
                    (NatTrans.app (f.app (op (x.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))))
                      (x.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))) :
                  (a : (F.obj (op x.fst)).obj x.fst) → (G.obj (op x.fst)).obj x.fst)
                (x.snd (β := fun (j : J) ↦ (F.obj (op j)).obj j)))))
        ⋯ x :
      Quot (Types.coendRel.{w, v, u} G))

Tactic:
rfl

Premises used: CategoryTheory.Limits.chosenCoend, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
i j : J
f : i ⟶ j
h :
  ∀ (x : end_.{w, v, u} F),
    (hom (FC := Fun) (π F i ≫ (F.obj (op i)).map f)).toFun x = (hom (FC := Fun) (π F j ≫ (F.map f.op).app j)).toFun x
⊢ π F i ≫ (F.obj (op i)).map f = π F j ≫ (F.map f.op).app j

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
i j : J
f : i ⟶ j
x : end_.{w, v, u} F
⊢ (hom (FC := Fun) (π F i ≫ (F.obj (op i)).map f)).toFun x = (hom (FC := Fun) (π F j ≫ (F.map f.op).app j)).toFun x

Tactic:
x.2 f

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
i j : J
f : i ⟶ j
x : end_.{w, v, u} F
⊢ (hom (FC := Fun) (π F i ≫ (F.obj (op i)).map f)).toFun x = (hom (FC := Fun) (π F j ≫ (F.map f.op).app j)).toFun x

Tactic:
exact x.2 f

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J_1 : Type u
inst : Category.{v, u} J_1
F_1 : J_1ᵒᵖ ⥤ J_1 ⥤ Type (max w u)
J : Type u
inst_1 : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
i j : J
f : i ⟶ j
⊢ end_.π F i ≫ (F.obj (op i)).map f = end_.π F j ≫ (F.map f.op).app j

Tactic:
apply end_.condition

Premises used: CategoryTheory.Limits.Types.end_.condition
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J_1 : Type u
inst : Category.{v, u} J_1
F_1 : J_1ᵒᵖ ⥤ J_1 ⥤ Type (max w u)
J : Type u
inst_1 : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cone (multicospanIndexEnd F).multicospan
x : s.pt
x_1 x_2 : J
f : x_1 ⟶ x_2
⊢ Eq (α := (F.obj (op x_1)).obj x_2)
    ((Hom.hom ((F.obj (op x_1)).map f) : (a : (F.obj (op x_1)).obj x_1) → (F.obj (op x_1)).obj x_2)
      ((fun (j : J) ↦
          ((hom (FC := Fun) (Multifork.ι s j) :
                (a : (fun (X : Type (max u w)) ↦ X) s.pt) →
                  (fun (X : Type (max u w)) ↦ X) ((multicospanIndexEnd F).left j))
              x :
            (fun (X : Type (max u w)) ↦ X) ((multicospanIndexEnd F).left j)))
        x_1))
    ((Hom.hom ((F.map f.op).app x_2) : (a : (F.obj (op x_2)).obj x_2) → (F.obj (op x_1)).obj x_2)
      ((fun (j : J) ↦
          ((hom (FC := Fun) (Multifork.ι s j) :
                (a : (fun (X : Type (max u w)) ↦ X) s.pt) →
                  (fun (X : Type (max u w)) ↦ X) ((multicospanIndexEnd F).left j))
              x :
            (fun (X : Type (max u w)) ↦ X) ((multicospanIndexEnd F).left j)))
        x_2))

Tactic:
ConcreteCategory.congr_hom (Wedge.condition s f) x

Premises used: CategoryTheory.Limits.Wedge.condition, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J_1 : Type u
inst : Category.{v, u} J_1
F_1 : J_1ᵒᵖ ⥤ J_1 ⥤ Type (max w u)
J : Type u
inst_1 : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cone (multicospanIndexEnd F).multicospan
x : s.pt
x_1 x_2 : J
f : x_1 ⟶ x_2
⊢ Eq (α := (F.obj (op x_1)).obj x_2)
    ((Hom.hom ((F.obj (op x_1)).map f) : (a : (F.obj (op x_1)).obj x_1) → (F.obj (op x_1)).obj x_2)
      ((fun (j : J) ↦
          ((hom (FC := Fun) (Multifork.ι s j) :
                (a : (fun (X : Type (max u w)) ↦ X) s.pt) →
                  (fun (X : Type (max u w)) ↦ X) ((multicospanIndexEnd F).left j))
              x :
            (fun (X : Type (max u w)) ↦ X) ((multicospanIndexEnd F).left j)))
        x_1))
    ((Hom.hom ((F.map f.op).app x_2) : (a : (F.obj (op x_2)).obj x_2) → (F.obj (op x_1)).obj x_2)
      ((fun (j : J) ↦
          ((hom (FC := Fun) (Multifork.ι s j) :
                (a : (fun (X : Type (max u w)) ↦ X) s.pt) →
                  (fun (X : Type (max u w)) ↦ X) ((multicospanIndexEnd F).left j))
              x :
            (fun (X : Type (max u w)) ↦ X) ((multicospanIndexEnd F).left j)))
        x_2))

Tactic:
exact ConcreteCategory.congr_hom (Wedge.condition s f) x

Premises used: CategoryTheory.Limits.Wedge.condition, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J_1 : Type u
inst : Category.{v, u} J_1
F_1 : J_1ᵒᵖ ⥤ J_1 ⥤ Type (max w u)
J : Type u
inst_1 : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cone (multicospanIndexEnd F).multicospan
a : (multicospanShapeEnd.{v, u} J).L
left left₁ left₂ left₃ :
  Eq (α := s.pt ⟶ (multicospanIndexEnd F).multicospan.obj (WalkingMulticospan.left a))
    ((↾fun (x : s.pt) ↦
        Subtype.mk (p := fun (x : (j : J) → (F.obj (op j)).obj j) ↦
          ∀ ⦃i j : J⦄ (f : i ⟶ j),
            Eq (α := (F.obj (op i)).obj j)
              ((Hom.hom ((F.obj (op i)).map f) : (a : (F.obj (op i)).obj i) → (F.obj (op i)).obj j) (x i) :
                (F.obj (op i)).obj j)
              ((Hom.hom ((F.map f.op).app j) : (a : (F.obj (op j)).obj j) → (F.obj (op i)).obj j) (x j) :
                (F.obj (op i)).obj j))
          (fun (j : J) ↦
            (hom (FC := Fun) (Multifork.ι s j) :
                (a : (fun (X : Type (max u w)) ↦ X) s.pt) →
                  (fun (X : Type (max u w)) ↦ X) ((multicospanIndexEnd F).left j))
              x)
          ⋯) ≫
      (wedge.{w, v, u} F).π.app (WalkingMulticospan.left a))
    (s.π.app (WalkingMulticospan.left a))
⊢ Eq (α := s.pt ⟶ (multicospanIndexEnd F).multicospan.obj (WalkingMulticospan.left a))
    ((↾fun (x : s.pt) ↦
        Subtype.mk (p := fun (x : (j : J) → (F.obj (op j)).obj j) ↦
          ∀ ⦃i j : J⦄ (f : i ⟶ j),
            Eq (α := (F.obj (op i)).obj j)
              ((Hom.hom ((F.obj (op i)).map f) : (a : (F.obj (op i)).obj i) → (F.obj (op i)).obj j) (x i) :
                (F.obj (op i)).obj j)
              ((Hom.hom ((F.map f.op).app j) : (a : (F.obj (op j)).obj j) → (F.obj (op i)).obj j) (x j) :
                (F.obj (op i)).obj j))
          (fun (j : J) ↦
            (hom (FC := Fun) (Multifork.ι s j) :
                (a : (fun (X : Type (max u w)) ↦ X) s.pt) →
                  (fun (X : Type (max u w)) ↦ X) ((multicospanIndexEnd F).left j))
              x)
          ⋯) ≫
      (wedge.{w, v, u} F).π.app (WalkingMulticospan.left a))
    (s.π.app (WalkingMulticospan.left a))

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J_1 : Type u
inst : Category.{v, u} J_1
F_1 : J_1ᵒᵖ ⥤ J_1 ⥤ Type (max w u)
J : Type u
inst_1 : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cone (multicospanIndexEnd F).multicospan
m : s.pt ⟶ (wedge.{w, v, u} F).pt
h : ∀ (j : WalkingMulticospan (multicospanShapeEnd.{v, u} J)), m ≫ (wedge.{w, v, u} F).π.app j = s.π.app j
h₁ :
  ∀ (x : s.pt),
    (hom (FC := Fun) m).toFun x =
      Fun.toFun
        (hom (FC := Fun)
          (↾fun (x : s.pt) ↦
            Subtype.mk (p := fun (x : (j : J) → (F.obj (op j)).obj j) ↦
              ∀ ⦃i j : J⦄ (f : i ⟶ j),
                Eq (α := (F.obj (op i)).obj j)
                  ((Hom.hom ((F.obj (op i)).map f) : (a : (F.obj (op i)).obj i) → (F.obj (op i)).obj j) (x i) :
                    (F.obj (op i)).obj j)
                  ((Hom.hom ((F.map f.op).app j) : (a : (F.obj (op j)).obj j) → (F.obj (op i)).obj j) (x j) :
                    (F.obj (op i)).obj j))
              (fun (j : J) ↦
                (hom (FC := Fun) (Multifork.ι s j) :
                    (a : (fun (X : Type (max u w)) ↦ X) s.pt) →
                      (fun (X : Type (max u w)) ↦ X) ((multicospanIndexEnd F).left j))
                  x)
              ⋯))
        x
⊢ m =
    ↾fun (x : s.pt) ↦
      Subtype.mk (p := fun (x : (j : J) → (F.obj (op j)).obj j) ↦
        ∀ ⦃i j : J⦄ (f : i ⟶ j),
          Eq (α := (F.obj (op i)).obj j)
            ((Hom.hom ((F.obj (op i)).map f) : (a : (F.obj (op i)).obj i) → (F.obj (op i)).obj j) (x i) :
              (F.obj (op i)).obj j)
            ((Hom.hom ((F.map f.op).app j) : (a : (F.obj (op j)).obj j) → (F.obj (op i)).obj j) (x j) :
              (F.obj (op i)).obj j))
        (fun (j : J) ↦
          (hom (FC := Fun) (Multifork.ι s j) :
              (a : (fun (X : Type (max u w)) ↦ X) s.pt) →
                (fun (X : Type (max u w)) ↦ X) ((multicospanIndexEnd F).left j))
            x)
        ⋯

Tactic:
ext x