awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasColimit F
j j' : J
x : F.obj j
f : j ⟶ j'
⊢ Eq (α := (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (F.map f ≫ colimit.ι F j') : (a : (fun (X : Type u) ↦ X) (F.obj j)) → colimit F) x :
      colimit F)
    ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
        x :
      (fun (X : Type u) ↦ X) (colimit F))

Tactic:
exact congr_hom (colimit.w F f) x

Premises used: CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Limits.colimit.w
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasColimit F
s : Cocone F
j : J
x : F.obj j
⊢ Eq (α := (fun (X : Type u) ↦ X) s.pt)
    ((hom (FC := TypeCat.Fun) (colimit.desc F s) :
          (a : (fun (X : Type u) ↦ X) (colimit F)) → (fun (X : Type u) ↦ X) s.pt)
        ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
              (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
            x :
          (fun (X : Type u) ↦ X) (colimit F)) :
      (fun (X : Type u) ↦ X) s.pt)
    ((hom (FC := TypeCat.Fun) (s.ι.app j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj s.pt).obj j))
        x :
      (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) s.pt) j))

Tactic:
congr_hom (colimit.ι_desc s j) x

Premises used: CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F G : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasColimitsOfShape.{w, v, u, u + 1} J (Type u)
α : F ⟶ G
j : J
x : F.obj j
⊢ Eq (α := (fun (X : Type u) ↦ X) (Functor.obj colim G))
    ((hom (FC := TypeCat.Fun) (Functor.map colim α) :
          (a : (fun (X : Type u) ↦ X) (colim.obj F)) → (fun (X : Type u) ↦ X) (colim.obj G))
        ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
              (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
            x :
          (fun (X : Type u) ↦ X) (colimit F)) :
      (fun (X : Type u) ↦ X) (Functor.obj colim G))
    ((hom (FC := TypeCat.Fun) (colimit.ι G j) :
          (a : (fun (X : Type u) ↦ X) (G.obj j)) → (fun (X : Type u) ↦ X) (colimit G))
        ((hom (FC := TypeCat.Fun) (α.app j) : (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (G.obj j))
            x :
          (fun (X : Type u) ↦ X) (G.obj j)) :
      (fun (X : Type u) ↦ X) (colimit G))

Tactic:
congr_hom (colimit.ι_map α j) x

Premises used: CategoryTheory.Limits.colimit.ι_map, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasColimit F
j j' : J
x : F.obj j
x' : F.obj j'
f : j ⟶ j'
w :
  (hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj j')) x =
    x'
rw :
  Eq (α := (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
        x :
      (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j') :
          (a : (fun (X : Type u) ↦ X) (F.obj j')) → (fun (X : Type u) ↦ X) (colimit F))
        ((hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj j'))
            x :
          (fun (X : Type u) ↦ X) (F.obj j')) :
      (fun (X : Type u) ↦ X) (colimit F))
rw₁ rw₂ :
  Eq (α := (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
        x :
      (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j) : (a : F.obj j) → colimit F) x : colimit F)
⊢ Eq (α := (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
        x :
      (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j') :
          (a : (fun (X : Type u) ↦ X) (F.obj j')) → (fun (X : Type u) ↦ X) (colimit F))
        x' :
      (fun (X : Type u) ↦ X) (colimit F))

Tactic:
rw [← w, colimit.w_apply]

Premises used: CategoryTheory.Limits.colimit.w_apply
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasColimit F
j j' : J
x : F.obj j
x' : F.obj j'
j'' : J
f : j ⟶ j''
f' : j' ⟶ j''
w :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj j''))
    ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj j''))
        x :
      (fun (X : Type u) ↦ X) (F.obj j''))
    ((hom (FC := TypeCat.Fun) (F.map f') : (a : (fun (X : Type u) ↦ X) (F.obj j')) → (fun (X : Type u) ↦ X) (F.obj j''))
        x' :
      (fun (X : Type u) ↦ X) (F.obj j''))
rw :
  Eq (α := (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j'') : (a : F.obj j'') → colimit F)
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj j) → F.obj j'') x : F.obj j'') :
      colimit F)
    ((hom (FC := TypeCat.Fun) (colimit.ι F j') :
          (a : (fun (X : Type u) ↦ X) (F.obj j')) → (fun (X : Type u) ↦ X) (colimit F))
        x' :
      (fun (X : Type u) ↦ X) (colimit F))
rw₁ :
  Eq (α := (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j'') : (a : F.obj j'') → colimit F)
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj j) → F.obj j'') x : F.obj j'') :
      colimit F)
    ((hom (FC := TypeCat.Fun) (colimit.ι F j'') : (a : F.obj j'') → colimit F)
        ((hom (FC := TypeCat.Fun) (F.map f') : (a : F.obj j') → F.obj j'') x' : F.obj j'') :
      colimit F)
rw₂ rw₃ :
  Eq (α := (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j'') : (a : F.obj j'') → colimit F)
        ((hom (FC := TypeCat.Fun) (F.map f') :
              (a : (fun (X : Type u) ↦ X) (F.obj j')) → (fun (X : Type u) ↦ X) (F.obj j''))
            x' :
          (fun (X : Type u) ↦ X) (F.obj j'')) :
      colimit F)
    ((hom (FC := TypeCat.Fun) (colimit.ι F j'') : (a : F.obj j'') → colimit F)
        ((hom (FC := TypeCat.Fun) (F.map f') : (a : F.obj j') → F.obj j'') x' : F.obj j'') :
      colimit F)
⊢ Eq (α := (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
        x :
      (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j') :
          (a : (fun (X : Type u) ↦ X) (F.obj j')) → (fun (X : Type u) ↦ X) (colimit F))
        x' :
      (fun (X : Type u) ↦ X) (colimit F))

Tactic:
rw [← colimit.w_apply _ f, ← colimit.w_apply _ f', w]

Premises used: CategoryTheory.Limits.colimit.w_apply
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasColimit F
j j' : J
x : F.obj j
x' : F.obj j'
w :
  Eq (α := (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
        x :
      (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j') :
          (a : (fun (X : Type u) ↦ X) (F.obj j')) → (fun (X : Type u) ↦ X) (colimit F))
        x' :
      (fun (X : Type u) ↦ X) (colimit F))
apply :
  Quot.mk F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) j x) =
    Quot.mk F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) j' x')
⊢ Relation.EqvGen F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) j x)
    (Sigma.mk (β := fun (j : J) ↦ F.obj j) j' x')

Tactic:
apply Quot.eq.1

Premises used: Iff.mp, Quot.eq
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasColimit F
j j' : J
x : F.obj j
x' : F.obj j'
w :
  Eq (α := (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
        x :
      (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j') :
          (a : (fun (X : Type u) ↦ X) (F.obj j')) → (fun (X : Type u) ↦ X) (colimit F))
        x' :
      (fun (X : Type u) ↦ X) (colimit F))
⊢ Quot.mk F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) j x) =
    Quot.mk F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) j' x')

Tactic:
simpa using congr_arg (colimitEquivColimitType F) w

Premises used: congr_arg, CategoryTheory.Limits.Types.colimitEquivColimitType, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
t : Cocone F
h : IsColimit t
x : t.pt
by_contra :
  ∀
    (hx :
      ¬∃ (j : J) (y : (fun (X : Type u) ↦ X) (F.obj j)),
          (hom (FC := TypeCat.Fun) (t.ι.app j) :
                (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
              y =
            x),
    False
⊢ ∃ (j : J) (y : (fun (X : Type u) ↦ X) (F.obj j)),
    (hom (FC := TypeCat.Fun) (t.ι.app j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
        y =
      x

Tactic:
by_contra hx
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
t : Cocone F
h : IsColimit t
x : t.pt
hx :
  ¬∃ (j : J) (y : (fun (X : Type u) ↦ X) (F.obj j)),
      (hom (FC := TypeCat.Fun) (t.ι.app j) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
          y =
        x
⊢ ∀ (x_1 : J) (x_2 : F.obj x_1),
    ¬(hom (FC := TypeCat.Fun) (t.ι.app x_1) : (a : F.obj x_1) → ((Functor.const J).obj t.pt).obj x_1) x_2 = x

Tactic:
simp_rw [not_exists] at hx

Premises used: not_exists
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
t : Cocone F
h : IsColimit t
x : t.pt
hx :
  ∀ (x_1 : J) (x_2 : F.obj x_1),
    ¬(hom (FC := TypeCat.Fun) (t.ι.app x_1) : (a : F.obj x_1) → ((Functor.const J).obj t.pt).obj x_1) x_2 = x
apply :
  Eq.{u + 1} (α := t.pt ⟶ ULift.{u, 0} Prop) (↾fun (x : t.pt) ↦ { down := True }) (↾fun (y : t.pt) ↦ { down := y ≠ x })
apply₁ :
  Ne.{u + 1} (α := t.pt ⟶ ULift.{u, 0} Prop) (↾fun (x : t.pt) ↦ { down := True }) (↾fun (y : t.pt) ↦ { down := y ≠ x })
⊢ False

Tactic:
apply (_ : (↾fun _ ↦ ULift.up True :
      t.pt ⟶ (ULift.{u} Prop)) ≠
    (↾fun y ↦ ULift.up (y ≠ x)))
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
t : Cocone F
h : IsColimit t
x : t.pt
hx :
  ∀ (x_1 : J) (x_2 : F.obj x_1),
    ¬(hom (FC := TypeCat.Fun) (t.ι.app x_1) : (a : F.obj x_1) → ((Functor.const J).obj t.pt).obj x_1) x_2 = x
⊢ Eq.{u + 1} (α := t.pt ⟶ ULift.{u, 0} Prop) (↾fun (x : t.pt) ↦ { down := True }) (↾fun (y : t.pt) ↦ { down := y ≠ x })

Tactic:
h.hom_ext fun j ↦ ?_

Premises used: CategoryTheory.Limits.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
t : Cocone F
h : IsColimit t
x : t.pt
hx :
  ∀ (x_1 : J) (x_2 : F.obj x_1),
    ¬(hom (FC := TypeCat.Fun) (t.ι.app x_1) : (a : F.obj x_1) → ((Functor.const J).obj t.pt).obj x_1) x_2 = x
refine :
  ∀ (j : J),
    Eq (α := F.obj j ⟶ ULift.{u, 0} Prop) (t.ι.app j ≫ ↾fun (x : t.pt) ↦ { down := True })
      (t.ι.app j ≫ ↾fun (y : t.pt) ↦ { down := y ≠ x })
⊢ Eq.{u + 1} (α := t.pt ⟶ ULift.{u, 0} Prop) (↾fun (x : t.pt) ↦ { down := True }) (↾fun (y : t.pt) ↦ { down := y ≠ x })

Tactic:
refine h.hom_ext fun j ↦ ?_

Premises used: CategoryTheory.Limits.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
t : Cocone F
h : IsColimit t
x : t.pt
hx :
  ∀ (x_1 : J) (x_2 : F.obj x_1),
    ¬(hom (FC := TypeCat.Fun) (t.ι.app x_1) : (a : F.obj x_1) → ((Functor.const J).obj t.pt).obj x_1) x_2 = x
j : J
h₁ :
  ∀ (y : F.obj j),
    ULift.down.{u, 0}
        (TypeCat.Fun.toFun
          (hom (FC := TypeCat.Fun) (t.ι.app j ≫ ↾fun (x : t.pt) ↦ { down := True : ULift.{u, 0} Prop })) y) ↔
      ULift.down.{u, 0}
        (TypeCat.Fun.toFun
          (hom (FC := TypeCat.Fun) (t.ι.app j ≫ ↾fun (y : t.pt) ↦ { down := y ≠ x : ULift.{u, 0} Prop })) y)
⊢ Eq (α := F.obj j ⟶ ULift.{u, 0} Prop) (t.ι.app j ≫ ↾fun (x : t.pt) ↦ { down := True })
    (t.ι.app j ≫ ↾fun (y : t.pt) ↦ { down := y ≠ x })

Tactic:
ext y
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
t : Cocone F
h : IsColimit t
x : t.pt
hx :
  ∀ (x_1 : J) (x_2 : F.obj x_1),
    ¬(hom (FC := TypeCat.Fun) (t.ι.app x_1) : (a : F.obj x_1) → ((Functor.const J).obj t.pt).obj x_1) x_2 = x
j : J
y : F.obj j
h₁ : ¬(hom (FC := TypeCat.Fun) (t.ι.app j) : (a : F.obj j) → t.pt) y = x
⊢ ULift.down.{u, 0}
      (TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (t.ι.app j ≫ ↾fun (x : t.pt) ↦ { down := True : ULift.{u, 0} Prop }))
        y) ↔
    ULift.down.{u, 0}
      (TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (t.ι.app j ≫ ↾fun (y : t.pt) ↦ { down := y ≠ x : ULift.{u, 0} Prop }))
        y)

Tactic:
simp only [Functor.const_obj_obj, TypeCat.Fun.toFun_apply, comp_apply, hom_ofHom,
      TypeCat.Fun.coe_mk, ne_eq, true_iff]

Premises used: TypeCat.Fun.coe_mk, true_iff, TypeCat.Fun.toFun_apply, ne_eq, CategoryTheory.comp_apply, CategoryTheory.Functor.const_obj_obj, CategoryTheory.ConcreteCategory.hom_ofHom
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
t : Cocone F
h : IsColimit t
x : t.pt
hx :
  ∀ (x_1 : J) (x_2 : F.obj x_1),
    ¬(hom (FC := TypeCat.Fun) (t.ι.app x_1) : (a : F.obj x_1) → ((Functor.const J).obj t.pt).obj x_1) x_2 = x
j : J
y : F.obj j
⊢ ¬(hom (FC := TypeCat.Fun) (t.ι.app j) : (a : F.obj j) → t.pt) y = x

Tactic:
hx j y
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
t : Cocone F
h : IsColimit t
x : t.pt
hx :
  ∀ (x_1 : J) (x_2 : F.obj x_1),
    ¬(hom (FC := TypeCat.Fun) (t.ι.app x_1) : (a : F.obj x_1) → ((Functor.const J).obj t.pt).obj x_1) x_2 = x
j : J
y : F.obj j
⊢ ¬(hom (FC := TypeCat.Fun) (t.ι.app j) : (a : F.obj j) → t.pt) y = x

Tactic:
exact hx j y
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
t : Cocone F
h : IsColimit t
x : t.pt
hx :
  ∀ (x_1 : J) (x_2 : F.obj x_1),
    ¬(hom (FC := TypeCat.Fun) (t.ι.app x_1) : (a : F.obj x_1) → ((Functor.const J).obj t.pt).obj x_1) x_2 = x
he :
  Eq.{u + 1} (α := t.pt ⟶ ULift.{u, 0} Prop) (↾fun (x : t.pt) ↦ { down := True }) (↾fun (y : t.pt) ↦ { down := y ≠ x })
⊢ Eq (α := ULift.{u, 0} Prop)
    ((hom (FC := TypeCat.Fun) (↾fun (x : t.pt) ↦ { down := True : ULift.{u, 0} Prop }) : (a : t.pt) → ULift.{u, 0} Prop)
        x :
      ULift.{u, 0} Prop)
    ((hom (FC := TypeCat.Fun) (↾fun (y : t.pt) ↦ { down := y ≠ x : ULift.{u, 0} Prop }) :
          (a : t.pt) → ULift.{u, 0} Prop)
        x :
      ULift.{u, 0} Prop)

Tactic:
have := ConcreteCategory.congr_hom he x
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
t : Cocone F
h : IsColimit t
x : t.pt
hx :
  ∀ (x_1 : J) (x_2 : F.obj x_1),
    ¬(hom (FC := TypeCat.Fun) (t.ι.app x_1) : (a : F.obj x_1) → ((Functor.const J).obj t.pt).obj x_1) x_2 = x
he :
  Eq.{u + 1} (α := t.pt ⟶ ULift.{u, 0} Prop) (↾fun (x : t.pt) ↦ { down := True }) (↾fun (y : t.pt) ↦ { down := y ≠ x })
this : { down := True : ULift.{u, 0} Prop } = { down := ¬x = x }
⊢ False

Tactic:
of_eq_true (congrArg ULift.down this).symm rfl

Premises used: congrArg, of_eq_true, Eq.symm, ULift.down, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
t : Cocone F
h : IsColimit t
x : t.pt
hx :
  ∀ (x_1 : J) (x_2 : F.obj x_1),
    ¬(hom (FC := TypeCat.Fun) (t.ι.app x_1) : (a : F.obj x_1) → ((Functor.const J).obj t.pt).obj x_1) x_2 = x
he :
  Eq.{u + 1} (α := t.pt ⟶ ULift.{u, 0} Prop) (↾fun (x : t.pt) ↦ { down := True }) (↾fun (y : t.pt) ↦ { down := y ≠ x })
this : { down := True : ULift.{u, 0} Prop } = { down := ¬x = x }
⊢ False

Tactic:
exact of_eq_true (congrArg ULift.down this).symm rfl

Premises used: congrArg, of_eq_true, Eq.symm, ULift.down, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
t : Cocone F
h : IsColimit t
x : t.pt
⊢ ∃ (j : J) (y : F.obj j),
    (hom (FC := TypeCat.Fun) (t.ι.app j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
        y =
      x

Tactic:
jointly_surjective_of_isColimit h x

Premises used: CategoryTheory.Limits.Types.jointly_surjective_of_isColimit
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasColimit F
x : colimit F
⊢ ∃ (j : J) (y : F.obj j),
    (hom (FC := TypeCat.Fun) (colimit.ι F j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
        y =
      x

Tactic:
jointly_surjective F (colimit.isColimit F) x

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Limits.Types.jointly_surjective
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasColimit F
⊢ Nonempty.{u + 1} (colimit F) → Nonempty J

Tactic:
Nonempty.map <| Sigma.fst ∘ Quot.out ∘ (colimitEquivColimitType F).toFun

Premises used: Quot.out, Function.comp, Sigma.fst, Equiv.toFun, CategoryTheory.Limits.Types.colimitEquivColimitType, Nonempty.map
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
i j : C
f : { as := i : Discrete C } ⟶ { as := j }
⊢ i = j

Tactic:
simpa using Discrete.eq_of_hom f

Premises used: CategoryTheory.Discrete.eq_of_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
i j : C
f : { as := i : Discrete C } ⟶ { as := j }
obtain :
  ∀ (f : { as := i : Discrete C } ⟶ { as := i }),
    Eq (α := Functor.obj (Discrete.functor F) { as := i : Discrete C } → (i : C) × F i)
      ((fun (x : Functor.obj (Discrete.functor F) { as := i : Discrete C }) ↦
          match (motive := (x : Discrete C) → (x : Functor.obj (Discrete.functor F) x) → (i : C) × F i) { as := i },
            x with
          | { as := i }, x => Sigma.mk (β := fun (i : C) ↦ F i) i x) ∘
        (⇑(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 })))
      fun (x : Functor.obj (Discrete.functor F) { as := i : Discrete C }) ↦
      match (motive := (x : Discrete C) → (x : Functor.obj (Discrete.functor F) x) → (i : C) × F i) { as := i }, x with
      | { as := i }, x => Sigma.mk (β := fun (i : C) ↦ F i) i x
⊢ Eq (α := Functor.obj (Discrete.functor F) { as := i : Discrete C } → (i : C) × F i)
    ((fun (x : Functor.obj (Discrete.functor F) { as := j : Discrete C }) ↦
        match (motive := (x : Discrete C) → (x : Functor.obj (Discrete.functor F) x) → (i : C) × F i) { as := j },
          x with
        | { as := i }, x => Sigma.mk (β := fun (i : C) ↦ F i) i x) ∘
      (⇑(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 })))
    fun (x : Functor.obj (Discrete.functor F) { as := i : Discrete C }) ↦
    match (motive := (x : Discrete C) → (x : Functor.obj (Discrete.functor F) x) → (i : C) × F i) { as := i }, x with
    | { as := i }, x => Sigma.mk (β := fun (i : C) ↦ F i) i x

Tactic:
obtain rfl : i = j := by simpa using Discrete.eq_of_hom f

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
i : C
f : { as := i : Discrete C } ⟶ { as := i }
⊢ Eq (α := Functor.obj (Discrete.functor F) { as := i : Discrete C } → (i : C) × F i)
    ((fun (x : Functor.obj (Discrete.functor F) { as := i : Discrete C }) ↦
        match (motive := (x : Discrete C) → (x : Functor.obj (Discrete.functor F) x) → (i : C) × F i) { as := i },
          x with
        | { as := i }, x => Sigma.mk (β := fun (i : C) ↦ F i) i x) ∘
      (⇑(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 })))
    fun (x : Functor.obj (Discrete.functor F) { as := i : Discrete C }) ↦
    match (motive := (x : Discrete C) → (x : Functor.obj (Discrete.functor F) x) → (i : C) × F i) { as := i }, x with
    | { as := i }, x => Sigma.mk (β := fun (i : C) ↦ F i) i x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
i : C
x : F i
⊢ (sigma F).inj (F := F) i x = Sigma.mk (β := fun (i : C) ↦ F i) i x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
h₁ : ∀ (x : c.pt), ∃ (i : C) (y : F i), c.inj (F := F) i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj (F := F) i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj (F := F) i x = c.inj (F := F) j y → i = j
left : Function.Injective (Functor.descColimitType (Discrete.functor F) c)
right : Function.Surjective (Functor.descColimitType (Discrete.functor F) c)
⊢ Function.Bijective (Functor.descColimitType (Discrete.functor F) c)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
h₁ : ∀ (x : c.pt), ∃ (i : C) (y : F i), c.inj (F := F) i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj (F := F) i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj (F := F) i x = c.inj (F := F) j y → i = j
x y : Functor.ColimitType (Discrete.functor F)
h : Functor.descColimitType (Discrete.functor F) c x = Functor.descColimitType (Discrete.functor F) c y
left :
  ∀ (i : C) (x : Functor.obj (Discrete.functor F) { as := i : Discrete C })
    (h :
      Functor.descColimitType (Discrete.functor F) c
          (Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x) =
        Functor.descColimitType (Discrete.functor F) c y),
    Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x = y
⊢ x = y

Tactic:
obtain ⟨⟨i⟩, x, rfl⟩ := (Discrete.functor F).ιColimitType_jointly_surjective x

Premises used: CategoryTheory.Functor.ιColimitType_jointly_surjective, CategoryTheory.Discrete.functor, rfl