awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C_1 : Type u
F_1 : C_1 → Type v
C : Type u
F : C → Type v
c : Cofan F
i j : C
f : { as := i : Discrete C } ⟶ { as := j }
⊢ Eq (α := Functor.obj (Discrete.functor F) { as := i : Discrete C } → c.pt)
    (Function.comp (β := Functor.obj (Discrete.functor F) { as := j : Discrete C })
      (match (motive := (x : Discrete C) → Functor.obj (Discrete.functor F) x → c.pt) { as := j : Discrete C } with
      | { as := j } =>
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.inj (f := F) j)) :
          (a : (fun (X : Type v) ↦ X) (F j)) → (fun (X : Type v) ↦ X) c.pt))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Discrete.functor F) f)) :
        (a : (fun (X : Type v) ↦ X) ((Discrete.functor F).obj { as := i })) →
          (fun (X : Type v) ↦ X) ((Discrete.functor F).obj { as := j })))
    (match (motive := (x : Discrete C) → Functor.obj (Discrete.functor F) x → c.pt) { as := i : Discrete C } with
    | { as := j } =>
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.inj (f := F) j)) :
        (a : (fun (X : Type v) ↦ X) (F j)) → (fun (X : Type v) ↦ X) c.pt))
have obtain : ∀ (f : { as := i : Discrete C } ⟶ { as := i }),
  Eq (α := Functor.obj (Discrete.functor F) { as := i : Discrete C } → c.pt)
    (Function.comp (β := Functor.obj (Discrete.functor F) { as := i : Discrete C })
      (match (motive := (x : Discrete C) → Functor.obj (Discrete.functor F) x → c.pt) { as := i : Discrete C } with
      | { as := j } =>
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.inj (f := F) j)) :
          (a : (fun (X : Type v) ↦ X) (F j)) → (fun (X : Type v) ↦ X) c.pt))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Discrete.functor F) f)) :
        (a : (fun (X : Type v) ↦ X) ((Discrete.functor F).obj { as := i })) →
          (fun (X : Type v) ↦ X) ((Discrete.functor F).obj { as := i })))
    (match (motive := (x : Discrete C) → Functor.obj (Discrete.functor F) x → c.pt) { as := i : Discrete C } with
    | { as := j } =>
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.inj (f := F) j)) :
        (a : (fun (X : Type v) ↦ X) (F j)) → (fun (X : Type v) ↦ X) c.pt))
Tactic: obtain rfl : i = j := by simpa using Discrete.eq_of_hom f
Cleared hypotheses: j, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C : Type u
F : C → Type v
c : Cofan F
⊢ Nonempty (IsColimit c) ↔
    Function.Bijective (β := c.cofanTypes (F := F).pt) (CofanTypes.fromSigma F (c.cofanTypes (F := F)))
have rw : Functor.CoconeTypes.IsColimit (c.cofanTypes (F := F)) ↔
  Function.Bijective (β := c.cofanTypes (F := F).pt) (CofanTypes.fromSigma F (c.cofanTypes (F := F)))
Tactic: rw [← isColimit_cofanTypes_iff, CofanTypes.isColimit_iff_bijective_fromSigma]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C : Type u
F : C → Type v
c : Cofan F
rw :
  Functor.CoconeTypes.IsColimit (c.cofanTypes (F := F)) ↔
    Function.Bijective (β := c.cofanTypes (F := F).pt) (CofanTypes.fromSigma F (c.cofanTypes (F := F)))
⊢ Nonempty (IsColimit c) ↔
    Function.Bijective (β := c.cofanTypes (F := F).pt) (CofanTypes.fromSigma F (c.cofanTypes (F := F)))
have rw₁ : Function.Bijective (β := c.cofanTypes (F := F).pt) (CofanTypes.fromSigma F (c.cofanTypes (F := F))) ↔
  Function.Bijective (β := c.cofanTypes (F := F).pt) (CofanTypes.fromSigma F (c.cofanTypes (F := F)))
Tactic: rw [← isColimit_cofanTypes_iff, CofanTypes.isColimit_iff_bijective_fromSigma]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C_1 : Type u
F_1 : C_1 → Type v
C : Type u
F : C → Type v
c : Cofan F
hc : IsColimit c
i j : C
x : F i
y : F j
hij : i = j
⊢ F i = F j
have rw : F j = F j
Tactic: rw [hij]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C : Type u
F : C → Type v
x : Cocone.{u_1, u, u_1, u + 1} (Functor.empty (Type u))
x_1 :
  Cocone.pt.{u_1, u, u_1, u + 1}
      { pt := PEmpty.{u + 1},
        ι :=
          Iso.inv (Functor.uniqueFromEmpty (Functor.obj (Functor.const (Discrete PEmpty.{u_1 + 1})) PEmpty.{u + 1})) :
        Cocone.{u_1, u, u_1, u + 1} (Functor.empty (Type u)) } ⟶
    x.pt
h :
  ∀ (j : Discrete PEmpty.{u_1 + 1}),
    NatTrans.app
          (Cocone.ι
            { pt := PEmpty.{u + 1},
              ι :=
                Iso.inv
                  (Functor.uniqueFromEmpty (Functor.obj (Functor.const (Discrete PEmpty.{u_1 + 1})) PEmpty.{u + 1})) })
          j ≫
        x_1 =
      x.ι.app j
⊢ x_1 =
    ↾fun
        (x_2 :
          Cocone.pt.{u_1, u, u_1, u + 1}
            { pt := PEmpty.{u + 1},
              ι :=
                Iso.inv
                  (Functor.uniqueFromEmpty
                    (Functor.obj (Functor.const (Discrete PEmpty.{u_1 + 1})) PEmpty.{u + 1})) }) ↦
      PEmpty.elim x_2
have h : ∀
  (x_2 :
    Cocone.pt.{u_1, u, u_1, u + 1}
      { pt := PEmpty.{u + 1},
        ι :=
          Iso.inv (Functor.uniqueFromEmpty (Functor.obj (Functor.const (Discrete PEmpty.{u_1 + 1})) PEmpty.{u + 1})) }),
  (ConcreteCategory.hom (FC := TypeCat.Fun) x_1).toFun x_2 =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾fun
            (x_3 :
              Cocone.pt.{u_1, u, u_1, u + 1}
                { pt := PEmpty.{u + 1},
                  ι :=
                    Iso.inv
                      (Functor.uniqueFromEmpty
                        (Functor.obj (Functor.const (Discrete PEmpty.{u_1 + 1})) PEmpty.{u + 1})) :
                  Cocone.{u_1, u, u_1, u + 1} (Functor.empty (Type u)) }) ↦
          PEmpty.elim x_3))
      x_2
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
X : Type u
⊢ Nonempty.{u + 2} (IsInitial X) ↔ IsEmpty X
have mp : Nonempty.{u + 2} (IsInitial X) → IsEmpty X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
X : Type u
mp : Nonempty.{u + 2} (IsInitial X) → IsEmpty X
⊢ Nonempty.{u + 2} (IsInitial X) ↔ IsEmpty X
have mpr : IsEmpty X → Nonempty.{u + 2} (IsInitial X)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C : Type u
F : C → Type v
X Y : Type u
x : Cocone (pair X Y)
x_1 : (binaryCoproductCocone X Y).pt ⟶ x.pt
w : ∀ (j : Discrete WalkingPair), (binaryCoproductCocone X Y).ι.app j ≫ x_1 = x.ι.app j
⊢ x_1 =
    ↾Sum.elim
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inl x)) :
          (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
            (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := left }))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inr x)) :
          (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
            (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := right }))
have h : ∀ (val : X),
  (ConcreteCategory.hom (FC := TypeCat.Fun) x_1).toFun (Sum.inl val) =
    TypeCat.Fun.toFun (X := (binaryCoproductCocone X Y).pt)
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾Sum.elim
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inl x)) :
              (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
                (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := left }))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inr x)) :
              (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
                (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := right }))))
      (Sum.inl val)
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C : Type u
F : C → Type v
X Y : Type u
x : Cocone (pair X Y)
x_1 : (binaryCoproductCocone X Y).pt ⟶ x.pt
w : ∀ (j : Discrete WalkingPair), (binaryCoproductCocone X Y).ι.app j ≫ x_1 = x.ι.app j
h :
  ∀ (val : X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) x_1).toFun (Sum.inl val) =
      TypeCat.Fun.toFun (X := (binaryCoproductCocone X Y).pt)
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾Sum.elim
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inl x)) :
                (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
                  (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := left }))
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inr x)) :
                (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
                  (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := right }))))
        (Sum.inl val)
⊢ x_1 =
    ↾Sum.elim
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inl x)) :
          (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
            (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := left }))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inr x)) :
          (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
            (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := right }))
have h₁ : ∀ (val : Y),
  (ConcreteCategory.hom (FC := TypeCat.Fun) x_1).toFun (Sum.inr val) =
    TypeCat.Fun.toFun (X := (binaryCoproductCocone X Y).pt)
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾Sum.elim
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inl x)) :
              (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
                (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := left }))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inr x)) :
              (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
                (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := right }))))
      (Sum.inr val)
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ Injective (α := X) (β := c.pt)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾Sum.inl ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
        (a : X) → c.pt) ∧
    Injective (α := Y) (β := c.pt)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾Sum.inr ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
          (a : Y) → c.pt) ∧
      IsCompl (α := Set c.pt)
        (Set.range (ι := X)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                (↾Sum.inl ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
            (a : X) → c.pt))
        (Set.range (ι := Y)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                (↾Sum.inr ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
            (a : Y) → c.pt))
have mp : IsCompl (α := Set c.pt)
  (Set.range (ι := X)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾Sum.inl ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
      (a : X) → c.pt))
  (Set.range (ι := Y)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾Sum.inr ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
      (a : Y) → c.pt))
Tactic: refine
        ⟨(h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.injective.comp
            Sum.inl_injective,
          (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.injective.comp
            Sum.inr_injective, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ IsCompl (α := Set c.pt)
    (Set.range (ι := X)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾Sum.inl ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
        (a : X) → c.pt))
    (Set.range (ι := Y)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾Sum.inr ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
        (a : Y) → c.pt))
have mp : Eq (α := Set c.pt)
  (Set.image (α := (fun (X : Type u) ↦ X) (X ⊕ Y))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) :
      (a : (fun (X : Type u) ↦ X) (X ⊕ Y)) → (fun (X : Type u) ↦ X) c.pt)
    (Set.range (ι := X)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (↾Sum.inl)) :
        (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (X ⊕ Y))))
  (Set.range (ι := Y)
      (Function.comp (β := (fun (X : Type u) ↦ X) (X ⊕ Y))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) :
          (a : (fun (X : Type u) ↦ X) (X ⊕ Y)) → (fun (X : Type u) ↦ X) c.pt)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (↾Sum.inr)) :
          (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) (X ⊕ Y))))ᶜ
Tactic: rw [types_comp, Set.range_comp, ← eq_compl_iff_isCompl, types_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ Eq (α := Set c.pt)
    (Set.image (α := (fun (X : Type u) ↦ X) (X ⊕ Y))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) :
        (a : (fun (X : Type u) ↦ X) (X ⊕ Y)) → (fun (X : Type u) ↦ X) c.pt)
      (Set.range (ι := X)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (↾Sum.inl)) :
          (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (X ⊕ Y))))
    (Set.range (ι := Y)
        (Function.comp (β := (fun (X : Type u) ↦ X) (X ⊕ Y))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) :
            (a : (fun (X : Type u) ↦ X) (X ⊕ Y)) → (fun (X : Type u) ↦ X) c.pt)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (↾Sum.inr)) :
            (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) (X ⊕ Y))))ᶜ
have mp : Eq (α := Set c.pt)
  (Set.image (α := X ⊕ Y)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) :
      (a : X ⊕ Y) → c.pt)
    (Set.range Sum.inl))
  (Set.range (ι := Y)
      (Function.comp (β := X ⊕ Y)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) :
          (a : X ⊕ Y) → c.pt)
        Sum.inr))ᶜ
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ Eq (α := Set c.pt)
    (Set.image (α := X ⊕ Y)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) :
        (a : X ⊕ Y) → c.pt)
      (Set.range Sum.inl))
    (Set.range (ι := Y)
        (Function.comp (β := X ⊕ Y)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) :
            (a : X ⊕ Y) → c.pt)
          Sum.inr))ᶜ
have mp : Eq (α := Set c.pt)
  (Set.image (α := X ⊕ Y)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) :
      (a : X ⊕ Y) → c.pt)
    (Set.range Sum.inl))
  (Set.image (α := X ⊕ Y)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) :
      (a : X ⊕ Y) → c.pt)
    (Set.range Sum.inr)ᶜ)
Tactic: rw [Set.range_comp _ Sum.inr, ← dsimp% [Iso.toEquiv] Set.image_compl_eq
          (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.bijective]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
Goal:
C : Type u
F : C → Type v
X Y : Type u
f : X ⟶ Y
inst : Mono f
⊢ IsColimit (F :=
    pair X
      { x : (fun (X : Type u) ↦ X) Y //
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
          (Set.range (ι := (fun (X : Type u) ↦ X) X)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
          x })
    (BinaryCofan.mk f
      (↾Subtype.val (p := fun (x : (fun (X : Type u) ↦ X) Y) ↦
          Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
            (Set.range (ι := (fun (X : Type u) ↦ X) X)
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                  (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
            x)))
have h : Nonempty.{u + 2}
  (IsColimit (F :=
    pair X
      { x : (fun (X : Type u) ↦ X) Y //
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
          (Set.range (ι := (fun (X : Type u) ↦ X) X)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
          x })
    (BinaryCofan.mk f
      (↾Subtype.val (p := fun (x : (fun (X : Type u) ↦ X) Y) ↦
          Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
            (Set.range (ι := (fun (X : Type u) ↦ X) X)
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                  (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
            x))))
Tactic: apply Nonempty.some
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.End (goal)
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'
⊢ 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'
have 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'
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.End (goal)
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'
⊢ 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'
have 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')
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.End (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
j j' : J
f : j ⟶ j'
⊢ (F.map f.op).app j ≫ ι F j = (F.obj (op j')).map f ≫ ι F j'
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.End (goal)
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
⊢ (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
have 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))
Tactic: apply Quot.sound