awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
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 : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
x :
  { x : (i : J.L) → ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (I.left i) //
    ∀ (i : J.R),
      Eq.{s + 1} (α := CC (I.right i))
        ((hom (FC := FC) (CC := CC) (I.fst i) : (a : CC (I.left (J.fst i))) → CC (I.right i)) (x (J.fst i)) :
          CC (I.right i))
        ((hom (FC := FC) (CC := CC) (I.snd i) : (a : CC (I.left (J.snd i))) → CC (I.right i)) (x (J.snd i)) :
          CC (I.right i)) }
b' : J.R
⊢ Eq (α := (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right b')))
    ((hom (FC := TypeCat.Fun) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).map (WalkingMulticospan.Hom.snd b')) :
          (a : (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.left (J.snd b')))) →
            (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C).obj (WalkingMulticospan.right b')))
        ((fun (j : WalkingMulticospan J) ↦
            (match (motive := (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j)
                j with
              | WalkingMulticospan.left a => (↑x : (i : J.L) → ToType (I.left i)) a
              | WalkingMulticospan.right b =>
                (hom (FC := FC) (CC := CC) (I.fst b) : (a : CC (I.left (J.fst b))) → CC (I.right b))
                  ((↑x : (i : J.L) → ToType (I.left i)) (J.fst b)) :
              (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j))
          (WalkingMulticospan.left (J.snd b'))) :
      (fun (X : Type s) ↦ X) ((I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right b')))
    ((fun (j : WalkingMulticospan J) ↦
          (match (motive := (j : WalkingMulticospan J) → (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j) j with
            | WalkingMulticospan.left a => (↑x : (i : J.L) → ToType (I.left i)) a
            | WalkingMulticospan.right b =>
              (hom (FC := FC) (CC := CC) (I.fst b) : (a : CC (I.left (J.fst b))) → CC (I.right b))
                ((↑x : (i : J.L) → ToType (I.left i)) (J.fst b)) :
            (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj j))
        (WalkingMulticospan.right b') :
      (I.multicospan ⋙ forget C (FC := FC) (CC := CC)).obj (WalkingMulticospan.right b'))
have left : Eq (α := ToType.{s, v, u, u_1} (FC := FC) (CC := CC) (I.right b'))
  ((hom (FC := FC) (CC := CC) (I.snd b') : (a : CC (I.left (J.snd b'))) → CC (I.right b'))
      ((↑x : (i : J.L) → ToType (I.left i)) (J.snd b')) :
    CC (I.right b'))
  ((hom (FC := FC) (CC := CC) (I.fst b') : (a : CC (I.left (J.fst b'))) → CC (I.right b'))
      ((↑x : (i : J.L) → ToType (I.left i)) (J.fst b')) :
    CC (I.right b'))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
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)
⊢ (∃ (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
have none : ∀ (y : ToType (FC := FC) (CC := CC) ((wideSpan B X f).obj 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) none) :
              (a : CC ((wideSpan B X f).obj 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) none) :
              (a : CC ((wideSpan B X f).obj none)) → CC (colimit (wideSpan B X f)))
            y :
          CC (colimit (wideSpan B X f)))
Tactic: obtain ⟨_ | j, y, rfl⟩ := Concrete.colimit_exists_rep _ x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
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)))
⊢ (∃ (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
have some : ∀ (j : α) (y : ToType (FC := FC) (CC := CC) ((wideSpan B X f).obj (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) (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: obtain ⟨_ | j, y, rfl⟩ := Concrete.colimit_exists_rep _ x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
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)
⊢ (∃ (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)))) ∨
    ∃ (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) none) :
              (a : CC ((wideSpan B X f).obj none)) → CC (colimit (wideSpan B X f)))
            y :
          CC (colimit (wideSpan B X f)))
have 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) none) :
          (a : CC ((wideSpan B X f).obj none)) → CC (colimit (wideSpan B X f)))
        y :
      CC (colimit (wideSpan B X f)))
Tactic: left
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
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)
⊢ ∃ (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)))
have 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)))
Tactic: use y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
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))
⊢ (∃ (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) (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)))
have 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) (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: right
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
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))
⊢ ∃ (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)))
have 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)))
Tactic: use j, y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
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)
⊢ ∃ (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
have 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))
Tactic: rcases Concrete.widePushout_exists_rep f x with (⟨y, rfl⟩ | ⟨i, y, rfl⟩)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
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))
⊢ ∃ (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
have 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))
Tactic: rcases Concrete.widePushout_exists_rep f x with (⟨y, rfl⟩ | ⟨i, y, rfl⟩)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
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
⊢ ∃ (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))
have 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))
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
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 α
⊢ ∃ (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))
have 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))
Tactic: use default, f _ y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
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)
⊢ ∃ (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))
have 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))
Tactic: use i, y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory (goal)
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)
⊢ g = h
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Connected (goal)
Goal:
J : Type u_1
⊢ IsConnected.{u_1, u_1} (WidePullbackShape J)
have 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'
Tactic: apply IsConnected.of_constant_of_preserves_morphisms
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Connected (goal)
Goal:
J α : Type u_1
F : WidePullbackShape J → α
H : ∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ ∀ (j j' : WidePullbackShape J), F j = F j'
have h : ∀ (i : WidePullbackShape J), F i = F none
Tactic: suffices ∀ i, F i = F none from fun j j' ↦ (this j).trans (this j').symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Connected (goal)
Goal:
J : Type u_1
⊢ IsConnected.{u_1, u_1} (WidePushoutShape J)
have 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'
Tactic: apply IsConnected.of_constant_of_preserves_morphisms
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Connected (goal)
Goal:
J α : Type u_1
F : WidePushoutShape J → α
H : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ ∀ (j j' : WidePushoutShape J), F j = F j'
have h : ∀ (i : WidePushoutShape J), F i = F none
Tactic: suffices ∀ i, F i = F none from fun j j' ↦ (this j).trans (this j').symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Countable (goal)
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsFiltered J
j : J
⊢ ∃ (n : ℕ), j ≤ sequentialFunctor_obj J n
have obtain : ∀ (m : ℕ) (h : sorry.choose (p := Function.Surjective) m = j), ∃ (n : ℕ), j ≤ sequentialFunctor_obj J n
Tactic: obtain ⟨m, h⟩ := (exists_surjective_nat _).choose_spec j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Countable (goal)
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsFiltered J
j : J
m : ℕ
h : ⋯.choose (p := Function.Surjective) m = j
⊢ ∃ (n : ℕ), j ≤ sequentialFunctor_obj J n
have refine : j ≤ sequentialFunctor_obj J (m + 1)
Tactic: refine ⟨m + 1, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Countable (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : Preorder J
inst_3 : IsFiltered J
d : J
⊢ IsConnected.{0, u_2} (StructuredArrow d (sequentialFunctor J))
have obtain : ∀ (n : ℕ) (g : d ≤ Functor.obj (sequentialFunctor J) n), IsConnected.{0, u_2} (StructuredArrow d (sequentialFunctor J))
Tactic: obtain ⟨n, (g : d ≤ (sequentialFunctor J).obj n)⟩ := sequentialFunctor_final_aux J d
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Countable (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : Preorder J
inst_3 : IsFiltered J
d : J
n : ℕ
g : d ≤ Functor.obj (sequentialFunctor J) n
⊢ IsConnected.{0, u_2} (StructuredArrow d (sequentialFunctor J))
have this : Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J))
Tactic: have : Nonempty (StructuredArrow d (sequentialFunctor J)) :=
      ⟨StructuredArrow.mk (homOfLE g)⟩