awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst_3 : HasWidePushout B X f
inst_4 : PreservesColimit (wideSpan B X f) (forget C (FC := FC) (CC := CC))
x : ToType (FC := FC) (CC := CC) (widePushout B X f)
none :
  ∀ (y : ToType (FC := FC) (CC := CC) ((wideSpan B X f).obj Option.none)),
    (∃ (y_1 : ToType (FC := FC) (CC := CC) B),
        Eq (α := CC (widePushout B X f))
          ((hom (FC := FC) (CC := CC) (head f) : (a : CC B) → CC (widePushout B X f)) y_1 : CC (widePushout B X f))
          ((hom (FC := FC) (CC := CC) (colimit.ι (wideSpan B X f) Option.none) :
                (a : CC ((wideSpan B X f).obj Option.none)) → CC (colimit (wideSpan B X f)))
              y :
            CC (colimit (wideSpan B X f)))) ∨
      ∃ (i : α) (y_1 : ToType (FC := FC) (CC := CC) (X i)),
        Eq (α := CC (widePushout B X f))
          ((hom (FC := FC) (CC := CC) (ι f i) : (a : CC (X i)) → CC (widePushout B X f)) y_1 : CC (widePushout B X f))
          ((hom (FC := FC) (CC := CC) (colimit.ι (wideSpan B X f) Option.none) :
                (a : CC ((wideSpan B X f).obj Option.none)) → CC (colimit (wideSpan B X f)))
              y :
            CC (colimit (wideSpan B X f)))
some :
  ∀ (j : α) (y : ToType (FC := FC) (CC := CC) ((wideSpan B X f).obj (Option.some j))),
    (∃ (y_1 : ToType (FC := FC) (CC := CC) B),
        Eq (α := CC (widePushout B X f))
          ((hom (FC := FC) (CC := CC) (head f) : (a : CC B) → CC (widePushout B X f)) y_1 : CC (widePushout B X f))
          ((hom (FC := FC) (CC := CC) (colimit.ι (wideSpan B X f) (Option.some j)) :
                (a : CC ((wideSpan B X f).obj (Option.some j))) → CC (colimit (wideSpan B X f)))
              y :
            CC (colimit (wideSpan B X f)))) ∨
      ∃ (i : α) (y_1 : ToType (FC := FC) (CC := CC) (X i)),
        Eq (α := CC (widePushout B X f))
          ((hom (FC := FC) (CC := CC) (ι f i) : (a : CC (X i)) → CC (widePushout B X f)) y_1 : CC (widePushout B X f))
          ((hom (FC := FC) (CC := CC) (colimit.ι (wideSpan B X f) (Option.some j)) :
                (a : CC ((wideSpan B X f).obj (Option.some j))) → CC (colimit (wideSpan B X f)))
              y :
            CC (colimit (wideSpan B X f)))
⊢ (∃ (y : ToType (FC := FC) (CC := CC) B),
      (hom (FC := FC) (CC := CC) (head f) : (a : CC B) → CC (widePushout B X f)) y = x) ∨
    ∃ (i : α) (y : ToType (FC := FC) (CC := CC) (X i)),
      (hom (FC := FC) (CC := CC) (ι f i) : (a : CC (X i)) → CC (widePushout B X f)) y = x

Tactic:
obtain ⟨_ | j, y, rfl⟩ := Concrete.colimit_exists_rep _ x

Premises used: CategoryTheory.Limits.Concrete.colimit_exists_rep, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst_3 : HasWidePushout B X f
inst_4 : PreservesColimit (wideSpan B X f) (forget C (FC := FC) (CC := CC))
y : ToType (FC := FC) (CC := CC) ((wideSpan B X f).obj Option.none)
none :
  ∃ (y_1 : ToType (FC := FC) (CC := CC) B),
    Eq (α := CC (widePushout B X f))
      ((hom (FC := FC) (CC := CC) (head f) : (a : CC B) → CC (widePushout B X f)) y_1 : CC (widePushout B X f))
      ((hom (FC := FC) (CC := CC) (colimit.ι (wideSpan B X f) Option.none) :
            (a : CC ((wideSpan B X f).obj Option.none)) → CC (colimit (wideSpan B X f)))
          y :
        CC (colimit (wideSpan B X f)))
⊢ (∃ (y_1 : ToType (FC := FC) (CC := CC) B),
      Eq (α := CC (widePushout B X f))
        ((hom (FC := FC) (CC := CC) (head f) : (a : CC B) → CC (widePushout B X f)) y_1 : CC (widePushout B X f))
        ((hom (FC := FC) (CC := CC) (colimit.ι (wideSpan B X f) Option.none) :
              (a : CC ((wideSpan B X f).obj Option.none)) → CC (colimit (wideSpan B X f)))
            y :
          CC (colimit (wideSpan B X f)))) ∨
    ∃ (i : α) (y_1 : ToType (FC := FC) (CC := CC) (X i)),
      Eq (α := CC (widePushout B X f))
        ((hom (FC := FC) (CC := CC) (ι f i) : (a : CC (X i)) → CC (widePushout B X f)) y_1 : CC (widePushout B X f))
        ((hom (FC := FC) (CC := CC) (colimit.ι (wideSpan B X f) Option.none) :
              (a : CC ((wideSpan B X f).obj Option.none)) → CC (colimit (wideSpan B X f)))
            y :
          CC (colimit (wideSpan B X f)))

Tactic:
left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst_3 : HasWidePushout B X f
inst_4 : PreservesColimit (wideSpan B X f) (forget C (FC := FC) (CC := CC))
y : ToType (FC := FC) (CC := CC) ((wideSpan B X f).obj none)
h :
  Eq (α := CC (widePushout B X f))
    ((hom (FC := FC) (CC := CC) (head f) : (a : CC B) → CC (widePushout B X f)) y : CC (widePushout B X f))
    ((hom (FC := FC) (CC := CC) (colimit.ι (wideSpan B X f) none) :
          (a : CC ((wideSpan B X f).obj none)) → CC (colimit (wideSpan B X f)))
        y :
      CC (colimit (wideSpan B X f)))
⊢ ∃ (y_1 : ToType (FC := FC) (CC := CC) B),
    Eq (α := CC (widePushout B X f))
      ((hom (FC := FC) (CC := CC) (head f) : (a : CC B) → CC (widePushout B X f)) y_1 : CC (widePushout B X f))
      ((hom (FC := FC) (CC := CC) (colimit.ι (wideSpan B X f) none) :
            (a : CC ((wideSpan B X f).obj none)) → CC (colimit (wideSpan B X f)))
          y :
        CC (colimit (wideSpan B X f)))

Tactic:
use y
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst_3 : HasWidePushout B X f
inst_4 : PreservesColimit (wideSpan B X f) (forget C (FC := FC) (CC := CC))
y : ToType (FC := FC) (CC := CC) ((wideSpan B X f).obj none)
⊢ Eq (α := CC (widePushout B X f))
    ((hom (FC := FC) (CC := CC) (head f) : (a : CC B) → CC (widePushout B X f)) y : CC (widePushout B X f))
    ((hom (FC := FC) (CC := CC) (colimit.ι (wideSpan B X f) none) :
          (a : CC ((wideSpan B X f).obj none)) → CC (colimit (wideSpan B X f)))
        y :
      CC (colimit (wideSpan B X f)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst_3 : HasWidePushout B X f
inst_4 : PreservesColimit (wideSpan B X f) (forget C (FC := FC) (CC := CC))
j : α
y : ToType (FC := FC) (CC := CC) ((wideSpan B X f).obj (Option.some j))
some :
  ∃ (i : α) (y_1 : ToType (FC := FC) (CC := CC) (X i)),
    Eq (α := CC (widePushout B X f))
      ((hom (FC := FC) (CC := CC) (ι f i) : (a : CC (X i)) → CC (widePushout B X f)) y_1 : CC (widePushout B X f))
      ((hom (FC := FC) (CC := CC) (colimit.ι (wideSpan B X f) (Option.some j)) :
            (a : CC ((wideSpan B X f).obj (Option.some j))) → CC (colimit (wideSpan B X f)))
          y :
        CC (colimit (wideSpan B X f)))
⊢ (∃ (y_1 : ToType (FC := FC) (CC := CC) B),
      Eq (α := CC (widePushout B X f))
        ((hom (FC := FC) (CC := CC) (head f) : (a : CC B) → CC (widePushout B X f)) y_1 : CC (widePushout B X f))
        ((hom (FC := FC) (CC := CC) (colimit.ι (wideSpan B X f) (Option.some j)) :
              (a : CC ((wideSpan B X f).obj (Option.some j))) → CC (colimit (wideSpan B X f)))
            y :
          CC (colimit (wideSpan B X f)))) ∨
    ∃ (i : α) (y_1 : ToType (FC := FC) (CC := CC) (X i)),
      Eq (α := CC (widePushout B X f))
        ((hom (FC := FC) (CC := CC) (ι f i) : (a : CC (X i)) → CC (widePushout B X f)) y_1 : CC (widePushout B X f))
        ((hom (FC := FC) (CC := CC) (colimit.ι (wideSpan B X f) (Option.some j)) :
              (a : CC ((wideSpan B X f).obj (Option.some j))) → CC (colimit (wideSpan B X f)))
            y :
          CC (colimit (wideSpan B X f)))

Tactic:
right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst_3 : HasWidePushout B X f
inst_4 : PreservesColimit (wideSpan B X f) (forget C (FC := FC) (CC := CC))
j : α
y : ToType (FC := FC) (CC := CC) ((wideSpan B X f).obj (some j))
h :
  Eq (α := CC (widePushout B X f))
    ((hom (FC := FC) (CC := CC) (ι f j) : (a : CC (X j)) → CC (widePushout B X f)) y : CC (widePushout B X f))
    ((hom (FC := FC) (CC := CC) (colimit.ι (wideSpan B X f) (some j)) :
          (a : CC ((wideSpan B X f).obj (some j))) → CC (colimit (wideSpan B X f)))
        y :
      CC (colimit (wideSpan B X f)))
⊢ ∃ (i : α) (y_1 : ToType (FC := FC) (CC := CC) (X i)),
    Eq (α := CC (widePushout B X f))
      ((hom (FC := FC) (CC := CC) (ι f i) : (a : CC (X i)) → CC (widePushout B X f)) y_1 : CC (widePushout B X f))
      ((hom (FC := FC) (CC := CC) (colimit.ι (wideSpan B X f) (some j)) :
            (a : CC ((wideSpan B X f).obj (some j))) → CC (colimit (wideSpan B X f)))
          y :
        CC (colimit (wideSpan B X f)))

Tactic:
use j, y
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst_3 : HasWidePushout B X f
inst_4 : PreservesColimit (wideSpan B X f) (forget C (FC := FC) (CC := CC))
j : α
y : ToType (FC := FC) (CC := CC) ((wideSpan B X f).obj (some j))
⊢ Eq (α := CC (widePushout B X f))
    ((hom (FC := FC) (CC := CC) (ι f j) : (a : CC (X j)) → CC (widePushout B X f)) y : CC (widePushout B X f))
    ((hom (FC := FC) (CC := CC) (colimit.ι (wideSpan B X f) (some j)) :
          (a : CC ((wideSpan B X f).obj (some j))) → CC (colimit (wideSpan B X f)))
        y :
      CC (colimit (wideSpan B X f)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
B : C
α : Type v
inst_3 : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst_4 : HasWidePushout B X f
inst_5 : PreservesColimit (wideSpan B X f) (forget C (FC := FC) (CC := CC))
x : ToType (FC := FC) (CC := CC) (widePushout B X f)
inl :
  ∀ (y : ToType (FC := FC) (CC := CC) B),
    ∃ (i : α) (y_1 : ToType (FC := FC) (CC := CC) (X i)),
      Eq (α := CC (widePushout B X f))
        ((hom (FC := FC) (CC := CC) (ι f i) : (a : CC (X i)) → CC (widePushout B X f)) y_1 : CC (widePushout B X f))
        ((hom (FC := FC) (CC := CC) (head f) : (a : CC B) → CC (widePushout B X f)) y : CC (widePushout B X f))
inr :
  ∀ (i : α) (y : ToType (FC := FC) (CC := CC) (X i)),
    ∃ (i_1 : α) (y_1 : ToType (FC := FC) (CC := CC) (X i_1)),
      Eq (α := CC (widePushout B X f))
        ((hom (FC := FC) (CC := CC) (ι f i_1) : (a : CC (X i_1)) → CC (widePushout B X f)) y_1 : CC (widePushout B X f))
        ((hom (FC := FC) (CC := CC) (ι f i) : (a : CC (X i)) → CC (widePushout B X f)) y : CC (widePushout B X f))
⊢ ∃ (i : α) (y : ToType (FC := FC) (CC := CC) (X i)),
    (hom (FC := FC) (CC := CC) (ι f i) : (a : CC (X i)) → CC (widePushout B X f)) y = x

Tactic:
rcases Concrete.widePushout_exists_rep f x with (⟨y, rfl⟩ | ⟨i, y, rfl⟩)

Premises used: CategoryTheory.Limits.Concrete.widePushout_exists_rep, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
B : C
α : Type v
inst_3 : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst_4 : HasWidePushout B X f
inst_5 : PreservesColimit (wideSpan B X f) (forget C (FC := FC) (CC := CC))
y : ToType (FC := FC) (CC := CC) B
inl :
  ∀ (inhabited_h : Inhabited α),
    ∃ (i : α) (y_1 : ToType (FC := FC) (CC := CC) (X i)),
      Eq (α := CC (widePushout B X f))
        ((hom (FC := FC) (CC := CC) (ι f i) : (a : CC (X i)) → CC (widePushout B X f)) y_1 : CC (widePushout B X f))
        ((hom (FC := FC) (CC := CC) (head f) : (a : CC B) → CC (widePushout B X f)) y : CC (widePushout B X f))
⊢ ∃ (i : α) (y_1 : ToType (FC := FC) (CC := CC) (X i)),
    Eq (α := CC (widePushout B X f))
      ((hom (FC := FC) (CC := CC) (ι f i) : (a : CC (X i)) → CC (widePushout B X f)) y_1 : CC (widePushout B X f))
      ((hom (FC := FC) (CC := CC) (head f) : (a : CC B) → CC (widePushout B X f)) y : CC (widePushout B X f))

Tactic:
inhabit α
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
B : C
α : Type v
inst_3 : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst_4 : HasWidePushout B X f
inst_5 : PreservesColimit (wideSpan B X f) (forget C (FC := FC) (CC := CC))
y : ToType (FC := FC) (CC := CC) B
inhabited_h : Inhabited α
h :
  Eq (α := CC (widePushout B X f))
    ((hom (FC := FC) (CC := CC) (ι f default) : (a : CC (X default)) → CC (widePushout B X f))
        ((hom (FC := FC) (CC := CC) (f default) : (a : CC B) → CC (X default)) y : CC (X default)) :
      CC (widePushout B X f))
    ((hom (FC := FC) (CC := CC) (head f) : (a : CC B) → CC (widePushout B X f)) y : CC (widePushout B X f))
⊢ ∃ (i : α) (y_1 : ToType (FC := FC) (CC := CC) (X i)),
    Eq (α := CC (widePushout B X f))
      ((hom (FC := FC) (CC := CC) (ι f i) : (a : CC (X i)) → CC (widePushout B X f)) y_1 : CC (widePushout B X f))
      ((hom (FC := FC) (CC := CC) (head f) : (a : CC B) → CC (widePushout B X f)) y : CC (widePushout B X f))

Tactic:
use default, f _ y

Premises used: Inhabited.default, CategoryTheory.ConcreteCategory.hom, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
B : C
α : Type v
inst_3 : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst_4 : HasWidePushout B X f
inst_5 : PreservesColimit (wideSpan B X f) (forget C (FC := FC) (CC := CC))
y : ToType (FC := FC) (CC := CC) B
inhabited_h : Inhabited α
⊢ Eq (α := CC (widePushout B X f))
    ((hom (FC := FC) (CC := CC) (ι f default) : (a : CC (X default)) → CC (widePushout B X f))
        ((hom (FC := FC) (CC := CC) (f default) : (a : CC B) → CC (X default)) y : CC (X default)) :
      CC (widePushout B X f))
    ((hom (FC := FC) (CC := CC) (head f) : (a : CC B) → CC (widePushout B X f)) y : CC (widePushout B X f))

Tactic:
simp only [← arrow_ι _ default, ConcreteCategory.comp_apply]

Premises used: Inhabited.default, CategoryTheory.Limits.WidePushout.arrow_ι, CategoryTheory.ConcreteCategory.comp_apply
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
B : C
α : Type v
inst_3 : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst_4 : HasWidePushout B X f
inst_5 : PreservesColimit (wideSpan B X f) (forget C (FC := FC) (CC := CC))
i : α
y : ToType (FC := FC) (CC := CC) (X i)
w : α
w₁ : ToType (FC := FC) (CC := CC) (X i)
h :
  Eq (α := CC (widePushout B X f))
    ((hom (FC := FC) (CC := CC) (ι f i) : (a : CC (X i)) → CC (widePushout B X f)) y : CC (widePushout B X f))
    ((hom (FC := FC) (CC := CC) (ι f i) : (a : CC (X i)) → CC (widePushout B X f)) y : CC (widePushout B X f))
⊢ ∃ (i_1 : α) (y_1 : ToType (FC := FC) (CC := CC) (X i_1)),
    Eq (α := CC (widePushout B X f))
      ((hom (FC := FC) (CC := CC) (ι f i_1) : (a : CC (X i_1)) → CC (widePushout B X f)) y_1 : CC (widePushout B X f))
      ((hom (FC := FC) (CC := CC) (ι f i) : (a : CC (X i)) → CC (widePushout B X f)) y : CC (widePushout B X f))

Tactic:
use i, y
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst_2 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_3 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
M N K : C
f : M ⟶ N
inst_4 : HasCokernel f
g h : cokernel f ⟶ K
w :
  ∀ (n : ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC) N),
    Eq (α := CC K)
      ((hom (FC := FC) (CC := CC) g : (a : CC (cokernel f)) → CC K)
          ((hom (FC := FC) (CC := CC) (cokernel.π f) : (a : CC N) → CC (cokernel f)) n : CC (cokernel f)) :
        CC K)
      ((hom (FC := FC) (CC := CC) h : (a : CC (cokernel f)) → CC K)
          ((hom (FC := FC) (CC := CC) (cokernel.π f) : (a : CC N) → CC (cokernel f)) n : CC (cokernel f)) :
        CC K)
h₁ :
  ∀ (x : CC N),
    Eq (α := CC K) ((hom (FC := FC) (CC := CC) (coequalizer.π f 0 ≫ g) : (a : CC N) → CC K) x : CC K)
      ((hom (FC := FC) (CC := CC) (coequalizer.π f 0 ≫ h) : (a : CC N) → CC K) x : CC K)
⊢ g = h

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst_2 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_3 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
M N K : C
f : M ⟶ N
inst_4 : HasCokernel f
g h : cokernel f ⟶ K
w :
  ∀ (n : ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC) N),
    Eq (α := CC K)
      ((hom (FC := FC) (CC := CC) g : (a : CC (cokernel f)) → CC K)
          ((hom (FC := FC) (CC := CC) (cokernel.π f) : (a : CC N) → CC (cokernel f)) n : CC (cokernel f)) :
        CC K)
      ((hom (FC := FC) (CC := CC) h : (a : CC (cokernel f)) → CC K)
          ((hom (FC := FC) (CC := CC) (cokernel.π f) : (a : CC N) → CC (cokernel f)) n : CC (cokernel f)) :
        CC K)
x : CC N
⊢ Eq (α := CC K) ((hom (FC := FC) (CC := CC) (coequalizer.π f 0 ≫ g) : (a : CC N) → CC K) x : CC K)
    ((hom (FC := FC) (CC := CC) (coequalizer.π f 0 ≫ h) : (a : CC N) → CC K) x : CC K)

Tactic:
simpa using w x
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Connected
Goal:
J : Type u_1
h :
  ∀ {α : Type u_1} (F : WidePullbackShape J → α),
    (∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : WidePullbackShape J), F j = F j'
⊢ IsConnected.{u_1, u_1} (WidePullbackShape J)

Tactic:
apply IsConnected.of_constant_of_preserves_morphisms

Premises used: CategoryTheory.IsConnected.of_constant_of_preserves_morphisms
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Connected
Goal:
J α : Type u_1
F : WidePullbackShape J → α
H : ∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
h : ∀ (i : WidePullbackShape J), F i = F none
⊢ ∀ (j j' : WidePullbackShape J), F j = F j'

Tactic:
suffices ∀ i, F i = F none from fun j j' ↦ (this j).trans (this j').symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Connected
Goal:
J α : Type u_1
F : WidePullbackShape J → α
H : ∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ F none = F none

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Connected
Goal:
J α : Type u_1
F : WidePullbackShape J → α
H : ∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
val : J
⊢ F (some val) = F none

Tactic:
H (.term _)

Premises used: CategoryTheory.Limits.WidePullbackShape.Hom.term
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Connected
Goal:
J α : Type u_1
F : WidePullbackShape J → α
H : ∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ F none = F none

Tactic:
exacts [rfl, H (.term _)]

Premises used: CategoryTheory.Limits.WidePullbackShape.Hom.term, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Connected
Goal:
J : Type u_1
h :
  ∀ {α : Type u_1} (F : WidePushoutShape J → α),
    (∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : WidePushoutShape J), F j = F j'
⊢ IsConnected.{u_1, u_1} (WidePushoutShape J)

Tactic:
apply IsConnected.of_constant_of_preserves_morphisms

Premises used: CategoryTheory.IsConnected.of_constant_of_preserves_morphisms
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Connected
Goal:
J α : Type u_1
F : WidePushoutShape J → α
H : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
h : ∀ (i : WidePushoutShape J), F i = F none
⊢ ∀ (j j' : WidePushoutShape J), F j = F j'

Tactic:
suffices ∀ i, F i = F none from fun j j' ↦ (this j).trans (this j').symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Connected
Goal:
J α : Type u_1
F : WidePushoutShape J → α
H : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ F none = F none

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Connected
Goal:
J α : Type u_1
F : WidePushoutShape J → α
H : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
val : J
⊢ F (some val) = F none

Tactic:
(H (.init _)).symm

Premises used: CategoryTheory.Limits.WidePushoutShape.Hom.init, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Connected
Goal:
J α : Type u_1
F : WidePushoutShape J → α
H : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ F none = F none

Tactic:
exacts [rfl, (H (.init _)).symm]

Premises used: CategoryTheory.Limits.WidePushoutShape.Hom.init, Eq.symm, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : HasCountableLimits.{v_1, u_1} C
inst_3 : Category.{v, u_2} J
inst_4 : CountableCategory.{v, u_2} J
⊢ HasLimitsOfShape.{v, u_2, v_1, u_1} J C

Tactic:
have : HasLimitsOfShape (HomAsType J) C := HasCountableLimits.out (HomAsType J)
  hasLimitsOfShape_of_equivalence (homAsTypeEquiv J)

Premises used: CategoryTheory.CountableCategory.HomAsType, CategoryTheory.Limits.hasLimitsOfShape_of_equivalence, CategoryTheory.Limits.HasCountableLimits.out, CategoryTheory.CountableCategory.homAsTypeEquiv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J_1 : Type u_2
inst_1 : Countable J_1
inst_2 : HasCountableProducts.{v_1, u_1} C
J : Type u_3
inst_3 : Countable J
⊢ HasProductsOfShape.{u_3, u_1, v_1} J C

Tactic:
have : Countable (Shrink.{0} J) := Countable.of_equiv _ (equivShrink.{0} J)
  have : HasLimitsOfShape (Discrete (Shrink.{0} J)) C := HasCountableProducts.out _
  hasLimitsOfShape_of_equivalence (Discrete.equivalence (equivShrink.{0} J)).symm

Premises used: Countable.of_equiv, CategoryTheory.Limits.HasCountableProducts.out, CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.hasLimitsOfShape_of_equivalence, Shrink, equivShrink, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J_1 : Type u_2
inst_1 : Countable J_1
inst_2 : HasCountableColimits.{v_1, u_1} C
J : Type u_3
inst_3 : Category.{v, u_3} J
inst_4 : CountableCategory.{v, u_3} J
⊢ HasColimitsOfShape.{v, u_3, v_1, u_1} J C

Tactic:
have : HasColimitsOfShape (HomAsType J) C := HasCountableColimits.out (HomAsType J)
  hasColimitsOfShape_of_equivalence (homAsTypeEquiv J)

Premises used: CategoryTheory.CountableCategory.HomAsType, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, CategoryTheory.Limits.HasCountableColimits.out, CategoryTheory.CountableCategory.homAsTypeEquiv