awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
Goal:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
h₁ :
  ∀
    (x :
      { x : Y //
        Eq (α := (fun (X : Type u) ↦ X) Z)
          ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
            (fun (X : Type u) ↦ X) Z)
          ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
            (fun (X : Type u) ↦ X) Z) }),
    TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          (↾Subtype.val (p := fun (x : Y) ↦
                Eq (α := (fun (X : Type u) ↦ X) Z)
                  ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                    (fun (X : Type u) ↦ X) Z)
                  ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                    (fun (X : Type u) ↦ X) Z)) ≫
            g))
        x =
      TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          (↾Subtype.val (p := fun (x : Y) ↦
                Eq (α := (fun (X : Type u) ↦ X) Z)
                  ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                    (fun (X : Type u) ↦ X) Z)
                  ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                    (fun (X : Type u) ↦ X) Z)) ≫
            h))
        x
⊢ Eq (α :=
    { x : Y //
        Eq (α := (fun (X : Type u) ↦ X) Z)
          ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
            (fun (X : Type u) ↦ X) Z)
          ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
            (fun (X : Type u) ↦ X) Z) } ⟶
      Z)
    (↾Subtype.val (p := fun (x : Y) ↦
          Eq (α := (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
              (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
              (fun (X : Type u) ↦ X) Z)) ≫
      g)
    (↾Subtype.val (p := fun (x : Y) ↦
          Eq (α := (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
              (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
              (fun (X : Type u) ↦ X) Z)) ≫
      h)

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
Goal:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
x :
  { x : Y //
    Eq (α := (fun (X : Type u) ↦ X) Z)
      ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
        (fun (X : Type u) ↦ X) Z)
      ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
        (fun (X : Type u) ↦ X) Z) }
⊢ TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (↾Subtype.val (p := fun (x : Y) ↦
              Eq (α := (fun (X : Type u) ↦ X) Z)
                ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                  (fun (X : Type u) ↦ X) Z)
                ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                  (fun (X : Type u) ↦ X) Z)) ≫
          g))
      x =
    TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (↾Subtype.val (p := fun (x : Y) ↦
              Eq (α := (fun (X : Type u) ↦ X) Z)
                ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                  (fun (X : Type u) ↦ X) Z)
                ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                  (fun (X : Type u) ↦ X) Z)) ≫
          h))
      x

Tactic:
x.prop

Premises used: Subtype.prop
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
Goal:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
x :
  { x : Y //
    Eq (α := (fun (X : Type u) ↦ X) Z)
      ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
        (fun (X : Type u) ↦ X) Z)
      ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
        (fun (X : Type u) ↦ X) Z) }
⊢ TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (↾Subtype.val (p := fun (x : Y) ↦
              Eq (α := (fun (X : Type u) ↦ X) Z)
                ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                  (fun (X : Type u) ↦ X) Z)
                ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                  (fun (X : Type u) ↦ X) Z)) ≫
          g))
      x =
    TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (↾Subtype.val (p := fun (x : Y) ↦
              Eq (α := (fun (X : Type u) ↦ X) Z)
                ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                  (fun (X : Type u) ↦ X) Z)
                ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                  (fun (X : Type u) ↦ X) Z)) ≫
          h))
      x

Tactic:
exact x.prop

Premises used: Subtype.prop
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
Goal:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
s : Fork g h
i : s.pt
⊢ Eq (α := (fun (X : Type u) ↦ X) Z)
    ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)
        ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) i :
          (fun (X : Type u) ↦ X) Y) :
      (fun (X : Type u) ↦ X) Z)
    ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)
        ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) i :
          (fun (X : Type u) ↦ X) Y) :
      (fun (X : Type u) ↦ X) Z)

Tactic:
apply congr_hom s.condition i

Premises used: CategoryTheory.Limits.Fork.condition, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
Goal:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
s : Fork g h
m :
  s.pt ⟶
    Cone.pt (F := parallelPair g h)
      (Fork.ofι
        (↾Subtype.val (p := fun (x : Y) ↦
            Eq (α := (fun (X : Type u) ↦ X) Z)
              ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                (fun (X : Type u) ↦ X) Z)
              ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                (fun (X : Type u) ↦ X) Z)))
        ⋯)
hm :
  m ≫
      Fork.ι
        (Fork.ofι
          (↾Subtype.val (p := fun (x : Y) ↦
              Eq (α := (fun (X : Type u) ↦ X) Z)
                ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                  (fun (X : Type u) ↦ X) Z)
                ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                  (fun (X : Type u) ↦ X) Z)))
          ⋯) =
    s.ι
h₁ :
  ∀ (x : s.pt),
    (hom (FC := TypeCat.Fun) m).toFun x =
      TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          (↾fun (i : s.pt) ↦
            Subtype.mk (p := fun (x : Y) ↦
              Eq (α := (fun (X : Type u) ↦ X) Z)
                ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                  (fun (X : Type u) ↦ X) Z)
                ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                  (fun (X : Type u) ↦ X) Z))
              ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) i) ⋯))
        x
⊢ m =
    ↾fun (i : s.pt) ↦
      Subtype.mk (p := fun (x : Y) ↦
        Eq (α := (fun (X : Type u) ↦ X) Z)
          ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
            (fun (X : Type u) ↦ X) Z)
          ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
            (fun (X : Type u) ↦ X) Z))
        ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) i) ⋯

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
Goal:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
s : Fork g h
m :
  s.pt ⟶
    Cone.pt (F := parallelPair g h)
      (Fork.ofι
        (↾Subtype.val (p := fun (x : Y) ↦
            Eq (α := (fun (X : Type u) ↦ X) Z)
              ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                (fun (X : Type u) ↦ X) Z)
              ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                (fun (X : Type u) ↦ X) Z)))
        ⋯)
hm :
  m ≫
      Fork.ι
        (Fork.ofι
          (↾Subtype.val (p := fun (x : Y) ↦
              Eq (α := (fun (X : Type u) ↦ X) Z)
                ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                  (fun (X : Type u) ↦ X) Z)
                ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                  (fun (X : Type u) ↦ X) Z)))
          ⋯) =
    s.ι
x : s.pt
⊢ (↑((hom (FC := TypeCat.Fun) m).toFun x) : Y) =
    (↑(TypeCat.Fun.toFun
          (hom (FC := TypeCat.Fun)
            (↾fun (i : s.pt) ↦
              Subtype.mk (p := fun (x : Y) ↦
                Eq (α := (fun (X : Type u) ↦ X) Z)
                  ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                    (fun (X : Type u) ↦ X) Z)
                  ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                    (fun (X : Type u) ↦ X) Z))
                ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) i) ⋯))
          x) :
      Y)

Tactic:
congr_hom hm x

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
Goal:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
s : Fork g h
m :
  s.pt ⟶
    Cone.pt (F := parallelPair g h)
      (Fork.ofι
        (↾Subtype.val (p := fun (x : Y) ↦
            Eq (α := (fun (X : Type u) ↦ X) Z)
              ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                (fun (X : Type u) ↦ X) Z)
              ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                (fun (X : Type u) ↦ X) Z)))
        ⋯)
hm :
  m ≫
      Fork.ι
        (Fork.ofι
          (↾Subtype.val (p := fun (x : Y) ↦
              Eq (α := (fun (X : Type u) ↦ X) Z)
                ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                  (fun (X : Type u) ↦ X) Z)
                ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                  (fun (X : Type u) ↦ X) Z)))
          ⋯) =
    s.ι
x : s.pt
⊢ (↑((hom (FC := TypeCat.Fun) m).toFun x) : Y) =
    (↑(TypeCat.Fun.toFun
          (hom (FC := TypeCat.Fun)
            (↾fun (i : s.pt) ↦
              Subtype.mk (p := fun (x : Y) ↦
                Eq (α := (fun (X : Type u) ↦ X) Z)
                  ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                    (fun (X : Type u) ↦ X) Z)
                  ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                    (fun (X : Type u) ↦ X) Z))
                ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) i) ⋯))
          x) :
      Y)

Tactic:
exact congr_hom hm x

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
Goal:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
s : Fork g h
m :
  s.pt ⟶
    Cone.pt (F := parallelPair g h)
      (Fork.ofι
        (↾Subtype.val (p := fun (x : Y) ↦
            Eq (α := (fun (X : Type u) ↦ X) Z)
              ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                (fun (X : Type u) ↦ X) Z)
              ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                (fun (X : Type u) ↦ X) Z)))
        ⋯)
hm :
  m ≫
      Fork.ι
        (Fork.ofι
          (↾Subtype.val (p := fun (x : Y) ↦
              Eq (α := (fun (X : Type u) ↦ X) Z)
                ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                  (fun (X : Type u) ↦ X) Z)
                ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                  (fun (X : Type u) ↦ X) Z)))
          ⋯) =
    s.ι
x : s.pt
⊢ (hom (FC := TypeCat.Fun) m).toFun x =
    TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (↾fun (i : s.pt) ↦
          Subtype.mk (p := fun (x : Y) ↦
            Eq (α := (fun (X : Type u) ↦ X) Z)
              ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                (fun (X : Type u) ↦ X) Z)
              ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
                (fun (X : Type u) ↦ X) Z))
            ((hom (FC := TypeCat.Fun) s.ι : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) i) ⋯))
      x

Tactic:
exact Subtype.ext (by exact congr_hom hm x)

Premises used: Subtype.ext
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
Goal:
Y Z : Type u
g h : Y ⟶ Z
⊢ (equalizerIso g h).hom ≫
      ↾Subtype.val (p := fun (x : Y) ↦
          Eq (α := (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
              (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
              (fun (X : Type u) ↦ X) Z)) =
    equalizer.ι g h

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Equalizers
Goal:
Y Z : Type u
g h : Y ⟶ Z
⊢ (equalizerIso g h).inv ≫ equalizer.ι g h =
    ↾Subtype.val (p := fun (x : Y) ↦
        Eq (α := (fun (X : Type u) ↦ X) Z)
          ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
            (fun (X : Type u) ↦ X) Z)
          ((hom (FC := TypeCat.Fun) h : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) x :
            (fun (X : Type u) ↦ X) Z))

Tactic:
limit.isoLimitCone_inv_π equalizerLimit WalkingParallelPair.zero

Premises used: CategoryTheory.Limits.Types.equalizerLimit, CategoryTheory.Limits.limit.isoLimitCone_inv_π, CategoryTheory.Limits.WalkingParallelPair.zero
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
x y : (j : J) × F.obj j
h_1 : F.ColimitTypeRel x y
f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ y.fst (β := fun (j : J) ↦ F.obj j)
h :
  y.snd (β := fun (j : J) ↦ F.obj j) =
    (hom (FC := TypeCat.Fun) (F.map f) :
        (a : (fun (X : Type u) ↦ X) (F.obj x.fst)) → (fun (X : Type u) ↦ X) (F.obj y.fst))
      (x.snd (β := fun (j : J) ↦ F.obj j))
rw :
  y.snd (β := fun (j : J) ↦ F.obj j) =
    (hom (FC := TypeCat.Fun) (F.map (𝟙 (y.fst (β := fun (j : J) ↦ F.obj j)))) :
        (a : (fun (X : Type u) ↦ X) (F.obj y.fst)) → (fun (X : Type u) ↦ X) (F.obj y.fst))
      (y.snd (β := fun (j : J) ↦ F.obj j))
rw₁ :
  y.snd (β := fun (j : J) ↦ F.obj j) =
    (hom (FC := TypeCat.Fun) (𝟙 (F.obj (y.fst (β := fun (j : J) ↦ F.obj j)))) :
        (a : (fun (X : Type u) ↦ X) (F.obj y.fst)) → (fun (X : Type u) ↦ X) (F.obj y.fst))
      (y.snd (β := fun (j : J) ↦ F.obj j))
rw₂ rw₃ : y.snd (β := fun (j : J) ↦ F.obj j) = y.snd (β := fun (j : J) ↦ F.obj j)
⊢ Eq (α := (fun (X : Type u) ↦ X) (F.obj (y.fst (β := fun (j : J) ↦ F.obj j))))
    ((hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type u) ↦ X) (F.obj x.fst)) → (fun (X : Type u) ↦ X) (F.obj y.fst))
        (x.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type u) ↦ X) (F.obj (y.fst (β := fun (j : J) ↦ F.obj j))))
    ((hom (FC := TypeCat.Fun) (F.map (𝟙 (y.fst (β := fun (j : J) ↦ F.obj j)))) :
          (a : (fun (X : Type u) ↦ X) (F.obj y.fst)) → (fun (X : Type u) ↦ X) (F.obj y.fst))
        (y.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type u) ↦ X) (F.obj (y.fst (β := fun (j : J) ↦ F.obj j))))

Tactic:
rw [← h, Functor.map_id, id_apply]

Premises used: CategoryTheory.id_apply, CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
x y : (j : J) × F.obj j
h_1 : FilteredColimit.Rel F x y
k : J
f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
g : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj x.fst)) → (fun (X : Type u) ↦ X) (F.obj k))
        (x.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj y.fst)) → (fun (X : Type u) ↦ X) (F.obj k))
        (y.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type u) ↦ X) (F.obj k))
⊢ Relation.EqvGen F.ColimitTypeRel x y

Tactic:
Relation.EqvGen.trans _ ⟨k, F.map f x.2⟩ _ ?_ ?_

Premises used: Relation.EqvGen.trans
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
x y : (j : J) × F.obj j
h_1 : FilteredColimit.Rel F x y
k : J
f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
g : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj x.fst)) → (fun (X : Type u) ↦ X) (F.obj k))
        (x.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj y.fst)) → (fun (X : Type u) ↦ X) (F.obj k))
        (y.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type u) ↦ X) (F.obj k))
refine_1 :
  Relation.EqvGen F.ColimitTypeRel x
    (Sigma.mk (β := fun (j : J) ↦ F.obj j) k
      ((hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type u) ↦ X) (F.obj x.fst)) → (fun (X : Type u) ↦ X) (F.obj k))
        (x.snd (β := fun (j : J) ↦ F.obj j))))
refine_2 :
  Relation.EqvGen F.ColimitTypeRel
    (Sigma.mk (β := fun (j : J) ↦ F.obj j) k
      ((hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type u) ↦ X) (F.obj x.fst)) → (fun (X : Type u) ↦ X) (F.obj k))
        (x.snd (β := fun (j : J) ↦ F.obj j))))
    y
⊢ Relation.EqvGen F.ColimitTypeRel x y

Tactic:
refine Relation.EqvGen.trans _ ⟨k, F.map f x.2⟩ _ ?_ ?_

Premises used: Relation.EqvGen.trans
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
x y : (j : J) × F.obj j
h_1 : FilteredColimit.Rel F x y
k : J
f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
g : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj x.fst)) → (fun (X : Type u) ↦ X) (F.obj k))
        (x.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj y.fst)) → (fun (X : Type u) ↦ X) (F.obj k))
        (y.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type u) ↦ X) (F.obj k))
⊢ Relation.EqvGen F.ColimitTypeRel x
    (Sigma.mk (β := fun (j : J) ↦ F.obj j) k
      ((hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type u) ↦ X) (F.obj x.fst)) → (fun (X : Type u) ↦ X) (F.obj k))
        (x.snd (β := fun (j : J) ↦ F.obj j))))

Tactic:
(Relation.EqvGen.rel _ _ ⟨f, rfl⟩)

Premises used: Exists.intro, Relation.EqvGen.rel, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
x y : (j : J) × F.obj j
h_1 : FilteredColimit.Rel F x y
k : J
f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
g : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj x.fst)) → (fun (X : Type u) ↦ X) (F.obj k))
        (x.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj y.fst)) → (fun (X : Type u) ↦ X) (F.obj k))
        (y.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type u) ↦ X) (F.obj k))
⊢ Relation.EqvGen F.ColimitTypeRel x
    (Sigma.mk (β := fun (j : J) ↦ F.obj j) k
      ((hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type u) ↦ X) (F.obj x.fst)) → (fun (X : Type u) ↦ X) (F.obj k))
        (x.snd (β := fun (j : J) ↦ F.obj j))))

Tactic:
exact (Relation.EqvGen.rel _ _ ⟨f, rfl⟩)

Premises used: Relation.EqvGen.rel
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
x y : (j : J) × F.obj j
h_1 : FilteredColimit.Rel F x y
k : J
f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
g : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj x.fst)) → (fun (X : Type u) ↦ X) (F.obj k))
        (x.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj y.fst)) → (fun (X : Type u) ↦ X) (F.obj k))
        (y.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type u) ↦ X) (F.obj k))
⊢ Relation.EqvGen F.ColimitTypeRel
    (Sigma.mk (β := fun (j : J) ↦ F.obj j) k
      ((hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type u) ↦ X) (F.obj x.fst)) → (fun (X : Type u) ↦ X) (F.obj k))
        (x.snd (β := fun (j : J) ↦ F.obj j))))
    y

Tactic:
(Relation.EqvGen.symm _ _ (Relation.EqvGen.rel _ _ ⟨g, h⟩))

Premises used: Exists.intro, Relation.EqvGen.rel, Relation.EqvGen.symm
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
x y : (j : J) × F.obj j
h_1 : FilteredColimit.Rel F x y
k : J
f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
g : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj x.fst)) → (fun (X : Type u) ↦ X) (F.obj k))
        (x.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj y.fst)) → (fun (X : Type u) ↦ X) (F.obj k))
        (y.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type u) ↦ X) (F.obj k))
⊢ Relation.EqvGen F.ColimitTypeRel
    (Sigma.mk (β := fun (j : J) ↦ F.obj j) k
      ((hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type u) ↦ X) (F.obj x.fst)) → (fun (X : Type u) ↦ X) (F.obj k))
        (x.snd (β := fun (j : J) ↦ F.obj j))))
    y

Tactic:
exact (Relation.EqvGen.symm _ _ (Relation.EqvGen.rel _ _ ⟨g, h⟩))

Premises used: Relation.EqvGen.rel, Relation.EqvGen.symm