awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst_1 : (X Y : C) → FunLike.{u_1 + 1, t + 1, t + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{t, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{r, w} J
F : Functor.{r, v, w, u} J C
D : Cocone F
i j : J
x : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj i)
y : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)
E : Cocone (F ⋙ forget C (FC := FC) (CC := CC)) := Functor.mapCocone (forget C (FC := FC) (CC := CC)) D
k : J
f : i ⟶ k
g : j ⟶ k
hfg :
  Eq (α := (fun (X : Type t) ↦ X) ((F ⋙ forget C (FC := FC) (CC := CC)).obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget C (FC := FC) (CC := CC)).map f) :
          (a : (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj i)) → (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj k))
        x :
      (fun (X : Type t) ↦ X) ((F ⋙ forget C (FC := FC) (CC := CC)).obj k))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map g) : (a : CC (F.obj j)) → CC (F.obj k)) y : CC (F.obj k))
h1 : (F ⋙ forget C (FC := FC) (CC := CC)).map f ≫ E.ι.app k = E.ι.app i := ⋯
h2 : (F ⋙ forget C (FC := FC) (CC := CC)).map g ≫ E.ι.app k = E.ι.app j := ⋯
rw :
  Eq (α := (fun (X : Type t) ↦ X) (Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (E.ι.app k) :
          (a : (F ⋙ forget C).obj k) → ((Functor.const J).obj E.pt).obj i)
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map g) : (a : CC (F.obj j)) → CC (F.obj k)) y : CC (F.obj k)) :
      Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (E.ι.app j) :
          (a : (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj j)) →
            (fun (X : Type t) ↦ X) (((Functor.const J).obj E.pt).obj j))
        y :
      (fun (X : Type t) ↦ X) (Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) j))
⊢ Eq (α := (fun (X : Type t) ↦ X) (Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (E.ι.app i) :
          (a : (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj i)) →
            (fun (X : Type t) ↦ X) (((Functor.const J).obj E.pt).obj i))
        x :
      (fun (X : Type t) ↦ X) (Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (E.ι.app j) :
          (a : (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj j)) →
            (fun (X : Type t) ↦ X) (((Functor.const J).obj E.pt).obj j))
        y :
      (fun (X : Type t) ↦ X) (Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) j))

Tactic:
rw [← h1, comp_apply, hfg]

Premises used: CategoryTheory.comp_apply
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst_1 : (X Y : C) → FunLike.{u_1 + 1, t + 1, t + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{t, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{r, w} J
F : Functor.{r, v, w, u} J C
D : Cocone F
i j : J
x : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj i)
y : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)
E : Cocone (F ⋙ forget C (FC := FC) (CC := CC)) := Functor.mapCocone (forget C (FC := FC) (CC := CC)) D
k : J
f : i ⟶ k
g : j ⟶ k
hfg :
  Eq (α := (fun (X : Type t) ↦ X) ((F ⋙ forget C (FC := FC) (CC := CC)).obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget C (FC := FC) (CC := CC)).map f) :
          (a : (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj i)) → (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj k))
        x :
      (fun (X : Type t) ↦ X) ((F ⋙ forget C (FC := FC) (CC := CC)).obj k))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map g) : (a : CC (F.obj j)) → CC (F.obj k)) y : CC (F.obj k))
h1 : (F ⋙ forget C (FC := FC) (CC := CC)).map f ≫ E.ι.app k = E.ι.app i := ⋯
h2 : (F ⋙ forget C (FC := FC) (CC := CC)).map g ≫ E.ι.app k = E.ι.app j := ⋯
⊢ Eq (α := (fun (X : Type t) ↦ X) (Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (E.ι.app k) :
          (a : (F ⋙ forget C).obj k) → ((Functor.const J).obj E.pt).obj i)
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map g) : (a : CC (F.obj j)) → CC (F.obj k)) y : CC (F.obj k)) :
      Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (E.ι.app j) :
          (a : (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj j)) →
            (fun (X : Type t) ↦ X) (((Functor.const J).obj E.pt).obj j))
        y :
      (fun (X : Type t) ↦ X) (Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) j))

Tactic:
ConcreteCategory.congr_hom h2 y

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst_1 : (X Y : C) → FunLike.{u_1 + 1, t + 1, t + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{t, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{r, w} J
F : Functor.{r, v, w, u} J C
D : Cocone F
i j : J
x : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj i)
y : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)
E : Cocone (F ⋙ forget C (FC := FC) (CC := CC)) := Functor.mapCocone (forget C (FC := FC) (CC := CC)) D
k : J
f : i ⟶ k
g : j ⟶ k
hfg :
  Eq (α := (fun (X : Type t) ↦ X) ((F ⋙ forget C (FC := FC) (CC := CC)).obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget C (FC := FC) (CC := CC)).map f) :
          (a : (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj i)) → (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj k))
        x :
      (fun (X : Type t) ↦ X) ((F ⋙ forget C (FC := FC) (CC := CC)).obj k))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map g) : (a : CC (F.obj j)) → CC (F.obj k)) y : CC (F.obj k))
h1 : (F ⋙ forget C (FC := FC) (CC := CC)).map f ≫ E.ι.app k = E.ι.app i := ⋯
h2 : (F ⋙ forget C (FC := FC) (CC := CC)).map g ≫ E.ι.app k = E.ι.app j := ⋯
⊢ Eq (α := (fun (X : Type t) ↦ X) (Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (E.ι.app k) :
          (a : (F ⋙ forget C).obj k) → ((Functor.const J).obj E.pt).obj i)
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map g) : (a : CC (F.obj j)) → CC (F.obj k)) y : CC (F.obj k)) :
      Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (E.ι.app j) :
          (a : (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj j)) →
            (fun (X : Type t) ↦ X) (((Functor.const J).obj E.pt).obj j))
        y :
      (fun (X : Type t) ↦ X) (Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) j))

Tactic:
exact ConcreteCategory.congr_hom h2 y

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst_1 : (X Y : C) → FunLike.{u_1 + 1, t + 1, t + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{t, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{r, w} J
F : Functor.{r, v, w, u} J C
inst_4 : HasColimit F
i j : J
x : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj i)
y : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)
h :
  ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k),
    Eq (α := CC (F.obj k))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map f) : (a : CC (F.obj i)) → CC (F.obj k)) x : CC (F.obj k))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map g) : (a : CC (F.obj j)) → CC (F.obj k)) y : CC (F.obj k))
⊢ Eq (α := CC (colimit F))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (colimit.ι F i) : (a : CC (F.obj i)) → CC (colimit F)) x :
      CC (colimit F))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (colimit.ι F j) : (a : CC (F.obj j)) → CC (colimit F)) y :
      CC (colimit F))

Tactic:
Concrete.isColimit_rep_eq_of_exists F x y h

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.Limits.Concrete.isColimit_rep_eq_of_exists, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst_1 : (X Y : C) → FunLike.{u_1 + 1, s + 1, s + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{s, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{r, w} J
F : Functor.{r, v, w, u} J C
inst_4 : PreservesColimit F (forget C (FC := FC) (CC := CC))
inst_5 : IsFiltered.{r, w} J
D : Cocone F
i j : J
hD : IsColimit D
x : ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (F.obj i)
y : ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)
h :
  Eq (α := CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) i))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.ι.app i) :
          (a : CC (F.obj i)) → CC (((Functor.const J).obj D.pt).obj i))
        x :
      CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) i))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.ι.app j) :
          (a : CC (F.obj j)) → CC (((Functor.const J).obj D.pt).obj j))
        y :
      CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) j))
E : Cocone (F ⋙ forget C (FC := FC) (CC := CC)) := Functor.mapCocone (forget C (FC := FC) (CC := CC)) D
hE : IsColimit E := isColimitOfPreserves (forget C (FC := FC) (CC := CC)) hD
⊢ ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k),
    Eq (α := CC (F.obj k))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map f) : (a : CC (F.obj i)) → CC (F.obj k)) x : CC (F.obj k))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map g) : (a : CC (F.obj j)) → CC (F.obj k)) y : CC (F.obj k))

Tactic:
(Types.FilteredColimit.isColimit_eq_iff (F ⋙ forget C) hE).mp h

Premises used: CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff, CategoryTheory.Functor.comp, CategoryTheory.forget, Iff.mp
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst_1 : (X Y : C) → FunLike.{u_1 + 1, s + 1, s + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{s, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{r, w} J
F : Functor.{r, v, w, u} J C
inst_4 : PreservesColimit F (forget C (FC := FC) (CC := CC))
inst_5 : IsFiltered.{r, w} J
D : Cocone F
i j : J
hD : IsColimit D
x : ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (F.obj i)
y : ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)
h :
  Eq (α := CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) i))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.ι.app i) :
          (a : CC (F.obj i)) → CC (((Functor.const J).obj D.pt).obj i))
        x :
      CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) i))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.ι.app j) :
          (a : CC (F.obj j)) → CC (((Functor.const J).obj D.pt).obj j))
        y :
      CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) j))
E : Cocone (F ⋙ forget C (FC := FC) (CC := CC)) := Functor.mapCocone (forget C (FC := FC) (CC := CC)) D
hE : IsColimit E := isColimitOfPreserves (forget C (FC := FC) (CC := CC)) hD
⊢ ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k),
    Eq (α := CC (F.obj k))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map f) : (a : CC (F.obj i)) → CC (F.obj k)) x : CC (F.obj k))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map g) : (a : CC (F.obj j)) → CC (F.obj k)) y : CC (F.obj k))

Tactic:
exact (Types.FilteredColimit.isColimit_eq_iff (F ⋙ forget C) hE).mp h

Premises used: CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff, CategoryTheory.Functor.comp, CategoryTheory.forget, Iff.mp
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst_1 : (X Y : C) → FunLike.{u_1 + 1, s + 1, s + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{s, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{r, w} J
F : Functor.{r, v, w, u} J C
inst_4 : PreservesColimit F (forget C (FC := FC) (CC := CC))
inst_5 : IsFiltered.{r, w} J
D : Cocone F
i j : J
hD : IsColimit D
x : ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (F.obj i)
y : ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)
⊢ Eq (α := CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) i))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.ι.app i) :
            (a : CC (F.obj i)) → CC (((Functor.const J).obj D.pt).obj i))
          x :
        CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) i))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.ι.app j) :
            (a : CC (F.obj j)) → CC (((Functor.const J).obj D.pt).obj j))
          y :
        CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) j)) ↔
    ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k),
      Eq (α := CC (F.obj k))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map f) : (a : CC (F.obj i)) → CC (F.obj k)) x : CC (F.obj k))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map g) : (a : CC (F.obj j)) → CC (F.obj k)) y : CC (F.obj k))

Tactic:
⟨Concrete.isColimit_exists_of_rep_eq.{s} _ hD _ _,
   Concrete.isColimit_rep_eq_of_exists _ _ _⟩

Premises used: CategoryTheory.Limits.Concrete.isColimit_exists_of_rep_eq, Iff.intro, CategoryTheory.Limits.Concrete.isColimit_rep_eq_of_exists
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst_1 : (X Y : C) → FunLike.{u_1 + 1, s + 1, s + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{s, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{r, w} J
F : Functor.{r, v, w, u} J C
inst_4 : PreservesColimit F (forget C (FC := FC) (CC := CC))
inst_5 : IsFiltered.{r, w} J
inst_6 : HasColimit F
i j : J
x : ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (F.obj i)
y : ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)
h :
  Eq (α := CC (colimit F))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (colimit.ι F i) : (a : CC (F.obj i)) → CC (colimit F)) x :
      CC (colimit F))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (colimit.ι F j) : (a : CC (F.obj j)) → CC (colimit F)) y :
      CC (colimit F))
⊢ ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k),
    Eq (α := CC (F.obj k))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map f) : (a : CC (F.obj i)) → CC (F.obj k)) x : CC (F.obj k))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map g) : (a : CC (F.obj j)) → CC (F.obj k)) y : CC (F.obj k))

Tactic:
Concrete.isColimit_exists_of_rep_eq.{s} F (colimit.isColimit _) x y h

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.Concrete.isColimit_exists_of_rep_eq
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst_1 : (X Y : C) → FunLike.{u_1 + 1, s + 1, s + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{s, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{r, w} J
F : Functor.{r, v, w, u} J C
inst_4 : PreservesColimit F (forget C (FC := FC) (CC := CC))
inst_5 : IsFiltered.{r, w} J
inst_6 : HasColimit F
i j : J
x : ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (F.obj i)
y : ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)
⊢ Eq (α := CC (colimit F))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (colimit.ι F i) : (a : CC (F.obj i)) → CC (colimit F)) x :
        CC (colimit F))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (colimit.ι F j) : (a : CC (F.obj j)) → CC (colimit F)) y :
        CC (colimit F)) ↔
    ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k),
      Eq (α := CC (F.obj k))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map f) : (a : CC (F.obj i)) → CC (F.obj k)) x : CC (F.obj k))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map g) : (a : CC (F.obj j)) → CC (F.obj k)) y : CC (F.obj k))

Tactic:
⟨Concrete.colimit_exists_of_rep_eq.{s} _ _ _, Concrete.colimit_rep_eq_of_exists _ _ _⟩

Premises used: CategoryTheory.Limits.Concrete.colimit_rep_eq_of_exists, Iff.intro, CategoryTheory.Limits.Concrete.colimit_exists_of_rep_eq
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Filtered
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
FC : C → C → Type u_3
CC : C → Type u_4
inst_2 : (X Y : C) → FunLike.{u_3 + 1, u_4 + 1, u_4 + 1} (FC X Y) (CC X) (CC Y)
inst_3 : ConcreteCategory.{u_4, v_2, u_2, u_3} C FC (CC := CC)
inst_4 : PreservesColimitsOfShape.{v_1, u_1, v_2, u_4, u_2, u_4 + 1} J (forget C (FC := FC) (CC := CC))
F : Functor.{v_1, v_2, u_1, u_2} J C
inst_5 : IsFilteredOrEmpty.{v_1, u_1} J
t : Cocone F
ht : IsColimit t
i j : J
xi : ToType.{u_4, v_2, u_2, u_3} (FC := FC) (CC := CC) (F.obj i)
xj : ToType.{u_4, v_2, u_2, u_3} (FC := FC) (CC := CC) (F.obj j)
⊢ Eq (α := CC (Functor.obj.{v_1, v_2, u_1, u_2} (Functor.obj (Functor.const J) t.pt) i))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (t.ι.app i) :
            (a : CC (F.obj i)) → CC (((Functor.const J).obj t.pt).obj i))
          xi :
        CC (Functor.obj.{v_1, v_2, u_1, u_2} (Functor.obj (Functor.const J) t.pt) i))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (t.ι.app j) :
            (a : CC (F.obj j)) → CC (((Functor.const J).obj t.pt).obj j))
          xj :
        CC (Functor.obj.{v_1, v_2, u_1, u_2} (Functor.obj (Functor.const J) t.pt) j)) ↔
    ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k),
      Eq (α := CC (F.obj k))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map f) : (a : CC (F.obj i)) → CC (F.obj k)) xi : CC (F.obj k))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map g) : (a : CC (F.obj j)) → CC (F.obj k)) xj : CC (F.obj k))

Tactic:
Types.FilteredColimit.isColimit_eq_iff _ (isColimitOfPreserves (forget C) ht)

Premises used: CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff, CategoryTheory.forget, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Filtered
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
FC : C → C → Type u_3
CC : C → Type u_4
inst_2 : (X Y : C) → FunLike.{u_3 + 1, u_4 + 1, u_4 + 1} (FC X Y) (CC X) (CC Y)
inst_3 : ConcreteCategory.{u_4, v_2, u_2, u_3} C FC (CC := CC)
inst_4 : PreservesColimitsOfShape.{v_1, u_1, v_2, u_4, u_2, u_4 + 1} J (forget C (FC := FC) (CC := CC))
F : Functor.{v_1, v_2, u_1, u_2} J C
inst_5 : IsFilteredOrEmpty.{v_1, u_1} J
t : Cocone F
ht : IsColimit t
i : J
x y : ToType.{u_4, v_2, u_2, u_3} (FC := FC) (CC := CC) (F.obj i)
⊢ Eq (α := CC (Functor.obj.{v_1, v_2, u_1, u_2} (Functor.obj (Functor.const J) t.pt) i))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (t.ι.app i) :
            (a : CC (F.obj i)) → CC (((Functor.const J).obj t.pt).obj i))
          x :
        CC (Functor.obj.{v_1, v_2, u_1, u_2} (Functor.obj (Functor.const J) t.pt) i))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (t.ι.app i) :
            (a : CC (F.obj i)) → CC (((Functor.const J).obj t.pt).obj i))
          y :
        CC (Functor.obj.{v_1, v_2, u_1, u_2} (Functor.obj (Functor.const J) t.pt) i)) ↔
    ∃ (j : J) (f : i ⟶ j),
      Eq (α := CC (F.obj j))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map f) : (a : CC (F.obj i)) → CC (F.obj j)) x : CC (F.obj j))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map f) : (a : CC (F.obj i)) → CC (F.obj j)) y : CC (F.obj j))

Tactic:
Types.FilteredColimit.isColimit_eq_iff' (isColimitOfPreserves (forget C) ht) x y

Premises used: CategoryTheory.forget, CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff', CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Filtered
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
FC : C → C → Type u_3
CC : C → Type u_4
inst_2 : (X Y : C) → FunLike.{u_3 + 1, u_4 + 1, u_4 + 1} (FC X Y) (CC X) (CC Y)
inst_3 : ConcreteCategory.{u_4, v_2, u_2, u_3} C FC (CC := CC)
inst_4 : PreservesColimitsOfShape.{v_1, u_1, v_2, u_4, u_2, u_4 + 1} J (forget C (FC := FC) (CC := CC))
F : Functor.{v_1, v_2, u_1, u_2} J C
inst_5 : IsFilteredOrEmpty.{v_1, u_1} J
inst_6 : HasColimit F
i j : J
xi : ToType.{u_4, v_2, u_2, u_3} (FC := FC) (CC := CC) (F.obj i)
xj : ToType.{u_4, v_2, u_2, u_3} (FC := FC) (CC := CC) (F.obj j)
⊢ Eq (α := CC (colimit F))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (colimit.ι F i) : (a : CC (F.obj i)) → CC (colimit F)) xi :
        CC (colimit F))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (colimit.ι F j) : (a : CC (F.obj j)) → CC (colimit F)) xj :
        CC (colimit F)) ↔
    ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k),
      Eq (α := CC (F.obj k))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map f) : (a : CC (F.obj i)) → CC (F.obj k)) xi : CC (F.obj k))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map g) : (a : CC (F.obj j)) → CC (F.obj k)) xj : CC (F.obj k))

Tactic:
(colimit.isColimit F).eq_iff _

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Limits.IsColimit.eq_iff, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures
Goal:
R : Type u_1
inst : Ring R
J : Type w
inst_1 : Category.{r, w} J
F : J ⥤ ModuleCat R
inst_2 :
  PreservesColimit F
    (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier))
inst_3 : IsFiltered.{r, w} J
inst_4 : HasColimit F
j : J
x : (↑(F.obj j) : Type (max t w))
hx :
  Eq (α := (↑(colimit F) : Type (max t w)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
            (CC := ModuleCat.carrier) (Y := colimit F) (colimit.ι F j) :
          (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w)))
        x :
      (↑(colimit F) : Type (max t w)))
    (0 : (↑(colimit F) : Type (max t w)))
⊢ Eq (α := (↑(colimit F) : Type (max t w))) 0
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
          (CC := ModuleCat.carrier) (Y := colimit F) (colimit.ι F j) :
        (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w)))
      0)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures
Goal:
R : Type u_1
inst : Ring R
J : Type w
inst_1 : Category.{r, w} J
F : J ⥤ ModuleCat R
inst_2 :
  PreservesColimit F
    (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier))
inst_3 : IsFiltered.{r, w} J
inst_4 : HasColimit F
j : J
x : (↑(F.obj j) : Type (max t w))
hx :
  Eq (α := (↑(colimit F) : Type (max t w)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
            (CC := ModuleCat.carrier) (Y := colimit F) (colimit.ι F j) :
          (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w)))
        x :
      (↑(colimit F) : Type (max t w)))
    (0 : (↑(colimit F) : Type (max t w)))
⊢ ∃ (k : J) (f : j ⟶ k) (g : j ⟶ k),
    Eq (α := (↑(F.obj k) : Type (max t w)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
              (CC := ModuleCat.carrier) (F.map f) :
            (a : (↑(F.obj j) : Type (max t w))) → (↑(F.obj k) : Type (max t w)))
          x :
        (↑(F.obj k) : Type (max t w)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
              (CC := ModuleCat.carrier) (F.map g) :
            (a : (↑(F.obj j) : Type (max t w))) → (↑(F.obj k) : Type (max t w)))
          0 :
        (↑(F.obj k) : Type (max t w)))

Tactic:
rw [show 0 = colimit.ι F j 0 by simp, colimit_rep_eq_iff_exists] at hx

Premises used: CategoryTheory.Limits.Concrete.colimit_rep_eq_iff_exists