awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F_1 : C → Type v
J : Type v
F : J → Type (max v u)
s : Cocone (Discrete.functor F)
m :
  Cocone.pt (J := Discrete J) (F := Discrete.functor F)
      { pt := (j : J) × F j,
        ι :=
          Discrete.natTrans fun (x : Discrete J) ↦
            match (motive :=
              (x : Discrete J) →
                Functor.obj (Discrete.functor F) x ⟶
                  Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) × F j)) x)
              x with
            | { as := j } =>
              ↾fun (x : Functor.obj (Discrete.functor F) { as := j : Discrete J }) ↦
                Sigma.mk (β := fun (j : J) ↦ F j) j x :
        Cocone (Discrete.functor F) } ⟶
    s.pt
w :
  ∀ (j : Discrete J),
    NatTrans.app
          (Cocone.ι
            { pt := (j : J) × F j,
              ι :=
                Discrete.natTrans fun (x : Discrete J) ↦
                  match (motive :=
                    (x : Discrete J) →
                      Functor.obj (Discrete.functor F) x ⟶
                        Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) × F j)) x)
                    x with
                  | { as := j } =>
                    ↾fun (x : Functor.obj (Discrete.functor F) { as := j : Discrete J }) ↦
                      Sigma.mk (β := fun (j : J) ↦ F j) j x })
          j ≫
        m =
      s.ι.app j
j : J
x : F j
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun (Sigma.mk (β := fun (j : J) ↦ F j) j x) =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾fun
            (x :
              Cocone.pt (J := Discrete J) (F := Discrete.functor F)
                { pt := (j : J) × F j,
                  ι :=
                    Discrete.natTrans fun (x : Discrete J) ↦
                      match (motive :=
                        (x : Discrete J) →
                          Functor.obj (Discrete.functor F) x ⟶
                            Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) × F j)) x)
                        x with
                      | { as := j } =>
                        ↾fun (x : Functor.obj (Discrete.functor F) { as := j : Discrete J }) ↦
                          Sigma.mk (β := fun (j : J) ↦ F j) j x :
                  Cocone (Discrete.functor F) }) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app { as := x.fst (β := fun (j : J) ↦ F j) : Discrete J }) :
              (a : (fun (X : Type (max u v)) ↦ X) ((Discrete.functor F).obj { as := x.fst })) →
                (fun (X : Type (max u v)) ↦ X) (((Functor.const (Discrete J)).obj s.pt).obj { as := x.fst }))
            (x.snd (β := fun (j : J) ↦ F j))))
      (Sigma.mk (β := fun (j : J) ↦ F j) j x)

Tactic:
exact ConcreteCategory.congr_hom (w ⟨j⟩) x

Premises used: CategoryTheory.Discrete.mk, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
J : Type v
F : J → Type (max v u)
j : J
⊢ Sigma.ι F j ≫ (coproductIso.{v, u} F).hom = ↾fun (x : F j) ↦ Sigma.mk (β := fun (j : J) ↦ F j) j x

Tactic:
colimit.isoColimitCocone_ι_hom (coproductColimitCocone F) ⟨j⟩

Premises used: CategoryTheory.Discrete.mk, CategoryTheory.Limits.Types.coproductColimitCocone, CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
J : Type v
F : J → Type (max v u)
j : J
⊢ (↾fun (x : F j) ↦ Sigma.mk (β := fun (j : J) ↦ F j) j x) ≫ (coproductIso.{v, u} F).inv = Sigma.ι F j

Tactic:
rfl

Premises used: TypeCat.Fun.comp, CategoryTheory.Limits.colimit, rfl, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
j j' : J
x : (F.obj (op j)).obj j
x' : (F.obj (op j')).obj j'
mp :
  coendRel.{w, v, u} F (Sigma.mk (β := fun (j : J) ↦ (F.obj (op j)).obj j) j x)
      (Sigma.mk (β := fun (j : J) ↦ (F.obj (op j)).obj j) j' x') →
    ∃ (f : j ⟶ j') (y : (F.obj (op j')).obj j),
      (hom (FC := Fun) ((F.map f.op).app j) :
              (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j)) →
                (fun (X : Type (max u w)) ↦ X) ((F.obj (op j)).obj j))
            y =
          x ∧
        (hom (FC := Fun) ((F.obj (op j')).map f) :
              (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j)) →
                (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j'))
            y =
          x'
mpr :
  (∃ (f : j ⟶ j') (y : (F.obj (op j')).obj j),
      (hom (FC := Fun) ((F.map f.op).app j) :
              (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j)) →
                (fun (X : Type (max u w)) ↦ X) ((F.obj (op j)).obj j))
            y =
          x ∧
        (hom (FC := Fun) ((F.obj (op j')).map f) :
              (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j)) →
                (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j'))
            y =
          x') →
    coendRel.{w, v, u} F (Sigma.mk (β := fun (j : J) ↦ (F.obj (op j)).obj j) j x)
      (Sigma.mk (β := fun (j : J) ↦ (F.obj (op j)).obj j) j' x')
⊢ coendRel.{w, v, u} F (Sigma.mk (β := fun (j : J) ↦ (F.obj (op j)).obj j) j x)
      (Sigma.mk (β := fun (j : J) ↦ (F.obj (op j)).obj j) j' x') ↔
    ∃ (f : j ⟶ j') (y : (F.obj (op j')).obj j),
      (hom (FC := Fun) ((F.map f.op).app j) :
              (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j)) →
                (fun (X : Type (max u w)) ↦ X) ((F.obj (op j)).obj j))
            y =
          x ∧
        (hom (FC := Fun) ((F.obj (op j')).map f) :
              (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j)) →
                (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j'))
            y =
          x'

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

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

Tactic:
exact ⟨f, x, by simp⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
j j' : J
f : j ⟶ j'
y : (F.obj (op j')).obj j
⊢ coendRel.{w, v, u} F
    (Sigma.mk (β := fun (j : J) ↦ (F.obj (op j)).obj j) j
      ((hom (FC := Fun) ((F.map f.op).app j) :
          (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j)) →
            (fun (X : Type (max u w)) ↦ X) ((F.obj (op j)).obj j))
        y))
    (Sigma.mk (β := fun (j : J) ↦ (F.obj (op j)).obj j) j'
      ((hom (FC := Fun) ((F.obj (op j')).map f) :
          (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j)) →
            (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j'))
        y))

Tactic:
coendRel.mk f y

Premises used: CategoryTheory.Limits.Types.coendRel.mk
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
j j' : J
f : j ⟶ j'
y : (F.obj (op j')).obj j
⊢ coendRel.{w, v, u} F
    (Sigma.mk (β := fun (j : J) ↦ (F.obj (op j)).obj j) j
      ((hom (FC := Fun) ((F.map f.op).app j) :
          (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j)) →
            (fun (X : Type (max u w)) ↦ X) ((F.obj (op j)).obj j))
        y))
    (Sigma.mk (β := fun (j : J) ↦ (F.obj (op j)).obj j) j'
      ((hom (FC := Fun) ((F.obj (op j')).map f) :
          (a : (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j)) →
            (fun (X : Type (max u w)) ↦ X) ((F.obj (op j')).obj j'))
        y))

Tactic:
exact coendRel.mk f y

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

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
j j' : J
f : j ⟶ j'
x : (F.obj (op j')).obj j
h :
  coendRel.{w, v, u} F (Sigma.mk (β := fun (j : J) ↦ (F.obj (op j)).obj j) j (((F.map f.op).app j).hom'.toFun x))
    (Sigma.mk (β := fun (j : J) ↦ (F.obj (op j)).obj j) j' (((F.obj (op j')).map f).hom'.toFun x))
⊢ (hom (FC := Fun) ((F.map f.op).app j ≫ ι F j)).toFun x = (hom (FC := Fun) ((F.obj (op j')).map f ≫ ι F j')).toFun x

Tactic:
apply Quot.sound

Premises used: Quot.sound
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
j j' : J
f : j ⟶ j'
x : (F.obj (op j')).obj j
⊢ coendRel.{w, v, u} F (Sigma.mk (β := fun (j : J) ↦ (F.obj (op j)).obj j) j (((F.map f.op).app j).hom'.toFun x))
    (Sigma.mk (β := fun (j : J) ↦ (F.obj (op j)).obj j) j' (((F.obj (op j')).map f).hom'.toFun x))

Tactic:
apply coendRel.mk

Premises used: CategoryTheory.Limits.Types.coendRel.mk
-- 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
⊢ (F.map f.op).app i ≫ coend.ι F i = (F.obj (op j)).map f ≫ coend.ι F j

Tactic:
apply coend.condition

Premises used: CategoryTheory.Limits.Types.coend.condition
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cocone (multispanIndexCoend F).multispan
j j' : J
f : j ⟶ j'
x : (F.obj (op j')).obj j
⊢ Eq (α := s.pt)
    ((fun (x : (j : J) × (F.obj (op j)).obj j) ↦
        ((hom (FC := Fun) (Multicofork.π s (x.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))) :
              (a : (fun (X : Type (max u w)) ↦ X) ((multispanIndexCoend F).right x.fst)) →
                (fun (X : Type (max u w)) ↦ X) s.pt)
            (x.snd (β := fun (j : J) ↦ (F.obj (op j)).obj j)) :
          (fun (X : Type (max u w)) ↦ X) s.pt))
      (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 (x : (j : J) × (F.obj (op j)).obj j) ↦
        ((hom (FC := Fun) (Multicofork.π s (x.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))) :
              (a : (fun (X : Type (max u w)) ↦ X) ((multispanIndexCoend F).right x.fst)) →
                (fun (X : Type (max u w)) ↦ X) s.pt)
            (x.snd (β := fun (j : J) ↦ (F.obj (op j)).obj j)) :
          (fun (X : Type (max u w)) ↦ X) s.pt))
      (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:
ConcreteCategory.congr_hom (Cowedge.condition s f) _

Premises used: CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Limits.Cowedge.condition
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cocone (multispanIndexCoend F).multispan
j j' : J
f : j ⟶ j'
x : (F.obj (op j')).obj j
⊢ Eq (α := s.pt)
    ((fun (x : (j : J) × (F.obj (op j)).obj j) ↦
        ((hom (FC := Fun) (Multicofork.π s (x.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))) :
              (a : (fun (X : Type (max u w)) ↦ X) ((multispanIndexCoend F).right x.fst)) →
                (fun (X : Type (max u w)) ↦ X) s.pt)
            (x.snd (β := fun (j : J) ↦ (F.obj (op j)).obj j)) :
          (fun (X : Type (max u w)) ↦ X) s.pt))
      (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 (x : (j : J) × (F.obj (op j)).obj j) ↦
        ((hom (FC := Fun) (Multicofork.π s (x.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))) :
              (a : (fun (X : Type (max u w)) ↦ X) ((multispanIndexCoend F).right x.fst)) →
                (fun (X : Type (max u w)) ↦ X) s.pt)
            (x.snd (β := fun (j : J) ↦ (F.obj (op j)).obj j)) :
          (fun (X : Type (max u w)) ↦ X) s.pt))
      (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 (Cowedge.condition s f) _

Premises used: CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Limits.Cowedge.condition
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cocone (multispanIndexCoend F).multispan
x x_1 : (j : J) × (F.obj (op j)).obj j
h : coendRel.{w, v, u} F x x_1
mk :
  ∀ {j j' : J} (f : j ⟶ j') (x : (F.obj (op j')).obj j),
    Eq (α := s.pt)
      ((fun (x : (j : J) × (F.obj (op j)).obj j) ↦
          ((hom (FC := Fun) (Multicofork.π s (x.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))) :
                (a : (fun (X : Type (max u w)) ↦ X) ((multispanIndexCoend F).right x.fst)) →
                  (fun (X : Type (max u w)) ↦ X) s.pt)
              (x.snd (β := fun (j : J) ↦ (F.obj (op j)).obj j)) :
            (fun (X : Type (max u w)) ↦ X) s.pt))
        (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 (x : (j : J) × (F.obj (op j)).obj j) ↦
          ((hom (FC := Fun) (Multicofork.π s (x.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))) :
                (a : (fun (X : Type (max u w)) ↦ X) ((multispanIndexCoend F).right x.fst)) →
                  (fun (X : Type (max u w)) ↦ X) s.pt)
              (x.snd (β := fun (j : J) ↦ (F.obj (op j)).obj j)) :
            (fun (X : Type (max u w)) ↦ X) s.pt))
        (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)))
⊢ Eq (α := s.pt)
    ((fun (x : (j : J) × (F.obj (op j)).obj j) ↦
        ((hom (FC := Fun) (Multicofork.π s (x.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))) :
              (a : (fun (X : Type (max u w)) ↦ X) ((multispanIndexCoend F).right x.fst)) →
                (fun (X : Type (max u w)) ↦ X) s.pt)
            (x.snd (β := fun (j : J) ↦ (F.obj (op j)).obj j)) :
          (fun (X : Type (max u w)) ↦ X) s.pt))
      x)
    ((fun (x : (j : J) × (F.obj (op j)).obj j) ↦
        ((hom (FC := Fun) (Multicofork.π s (x.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))) :
              (a : (fun (X : Type (max u w)) ↦ X) ((multispanIndexCoend F).right x.fst)) →
                (fun (X : Type (max u w)) ↦ X) s.pt)
            (x.snd (β := fun (j : J) ↦ (F.obj (op j)).obj j)) :
          (fun (X : Type (max u w)) ↦ X) s.pt))
      x_1)

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

Premises used: CategoryTheory.ConcreteCategory.mk
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cocone (multispanIndexCoend F).multispan
a : (multispanShapeCoend.{v, u} J).R
right right₁ right₂ right₃ :
  Eq (α := (multispanIndexCoend F).multispan.obj (WalkingMultispan.right a) ⟶ s.pt)
    ((cowedge.{w, v, u} F).ι.app (WalkingMultispan.right a) ≫
      ↾Quot.lift (r := coendRel.{w, v, u} F)
          (fun (x : (j : J) × (F.obj (op j)).obj j) ↦
            (hom (FC := Fun) (Multicofork.π s (x.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))) :
                (a : (fun (X : Type (max u w)) ↦ X) ((multispanIndexCoend F).right x.fst)) →
                  (fun (X : Type (max u w)) ↦ X) s.pt)
              (x.snd (β := fun (j : J) ↦ (F.obj (op j)).obj j)))
          ⋯)
    (s.ι.app (WalkingMultispan.right a))
⊢ Eq (α := (multispanIndexCoend F).multispan.obj (WalkingMultispan.right a) ⟶ s.pt)
    ((cowedge.{w, v, u} F).ι.app (WalkingMultispan.right a) ≫
      ↾Quot.lift (r := coendRel.{w, v, u} F)
          (fun (x : (j : J) × (F.obj (op j)).obj j) ↦
            (hom (FC := Fun) (Multicofork.π s (x.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))) :
                (a : (fun (X : Type (max u w)) ↦ X) ((multispanIndexCoend F).right x.fst)) →
                  (fun (X : Type (max u w)) ↦ X) s.pt)
              (x.snd (β := fun (j : J) ↦ (F.obj (op j)).obj j)))
          ⋯)
    (s.ι.app (WalkingMultispan.right a))

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cocone (multispanIndexCoend F).multispan
m : (cowedge.{w, v, u} F).pt ⟶ s.pt
h : ∀ (j : WalkingMultispan (multispanShapeCoend.{v, u} J)), (cowedge.{w, v, u} F).ι.app j ≫ m = s.ι.app j
h₁ :
  ∀ (x : (cowedge.{w, v, u} F).pt) (j : (j : J) × (F.obj (op j)).obj j),
    (hom (FC := Fun) m).toFun (Quot.mk (coendRel.{w, v, u} F) j) =
      Fun.toFun
        (hom (FC := Fun)
          (↾Quot.lift (r := coendRel.{w, v, u} F)
              (fun (x : (j : J) × (F.obj (op j)).obj j) ↦
                (hom (FC := Fun) (Multicofork.π s (x.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))) :
                    (a : (fun (X : Type (max u w)) ↦ X) ((multispanIndexCoend F).right x.fst)) →
                      (fun (X : Type (max u w)) ↦ X) s.pt)
                  (x.snd (β := fun (j : J) ↦ (F.obj (op j)).obj j)))
              ⋯))
        (Quot.mk (coendRel.{w, v, u} F) j)
⊢ m =
    ↾Quot.lift (r := coendRel.{w, v, u} F)
        (fun (x : (j : J) × (F.obj (op j)).obj j) ↦
          (hom (FC := Fun) (Multicofork.π s (x.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))) :
              (a : (fun (X : Type (max u w)) ↦ X) ((multispanIndexCoend F).right x.fst)) →
                (fun (X : Type (max u w)) ↦ X) s.pt)
            (x.snd (β := fun (j : J) ↦ (F.obj (op j)).obj j)))
        ⋯

Tactic:
ext ⟨j⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.End
Goal:
J : Type u
inst : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cocone (multispanIndexCoend F).multispan
m : (cowedge.{w, v, u} F).pt ⟶ s.pt
h : ∀ (j : WalkingMultispan (multispanShapeCoend.{v, u} J)), (cowedge.{w, v, u} F).ι.app j ≫ m = s.ι.app j
x : (cowedge.{w, v, u} F).pt
j : (j : J) × (F.obj (op j)).obj j
⊢ (hom (FC := Fun) m).toFun (Quot.mk (coendRel.{w, v, u} F) j) =
    Fun.toFun
      (hom (FC := Fun)
        (↾Quot.lift (r := coendRel.{w, v, u} F)
            (fun (x : (j : J) × (F.obj (op j)).obj j) ↦
              (hom (FC := Fun) (Multicofork.π s (x.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))) :
                  (a : (fun (X : Type (max u w)) ↦ X) ((multispanIndexCoend F).right x.fst)) →
                    (fun (X : Type (max u w)) ↦ X) s.pt)
                (x.snd (β := fun (j : J) ↦ (F.obj (op j)).obj j)))
            ⋯))
      (Quot.mk (coendRel.{w, v, u} F) j)

Tactic:
ConcreteCategory.congr_hom (h (.right j.fst)) j.snd

Premises used: Sigma.fst, CategoryTheory.Limits.WalkingMultispan.right, 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)
s : Cocone (multispanIndexCoend F).multispan
m : (cowedge.{w, v, u} F).pt ⟶ s.pt
h : ∀ (j : WalkingMultispan (multispanShapeCoend.{v, u} J)), (cowedge.{w, v, u} F).ι.app j ≫ m = s.ι.app j
x : (cowedge.{w, v, u} F).pt
j : (j : J) × (F.obj (op j)).obj j
⊢ (hom (FC := Fun) m).toFun (Quot.mk (coendRel.{w, v, u} F) j) =
    Fun.toFun
      (hom (FC := Fun)
        (↾Quot.lift (r := coendRel.{w, v, u} F)
            (fun (x : (j : J) × (F.obj (op j)).obj j) ↦
              (hom (FC := Fun) (Multicofork.π s (x.fst (β := fun (j : J) ↦ (F.obj (op j)).obj j))) :
                  (a : (fun (X : Type (max u w)) ↦ X) ((multispanIndexCoend F).right x.fst)) →
                    (fun (X : Type (max u w)) ↦ X) s.pt)
                (x.snd (β := fun (j : J) ↦ (F.obj (op j)).obj j)))
            ⋯))
      (Quot.mk (coendRel.{w, v, u} F) j)

Tactic:
exact ConcreteCategory.congr_hom (h (.right j.fst)) j.snd

Premises used: Sigma.fst, CategoryTheory.Limits.WalkingMultispan.right, 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)
⊢ chosenCoend F = Quot (coendRel.{w, v, u} F)

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)
j : J
x : (F.obj (op j)).obj j
⊢ (hom (FC := Fun) (ι F j) : (a : (F.obj (op j)).obj j) → chosenCoend F) x =
    Quot.mk (Types.coendRel.{w, v, u} F) (Sigma.mk (β := fun (j : J) ↦ (F.obj (op j)).obj j) j x)

Tactic:
rfl

Premises used: rfl
-- 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:
ConcreteCategory.congr_hom (hf f) _

Premises used: CategoryTheory.ConcreteCategory.congr_hom