awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
y : Functor.ColimitType (Discrete.functor F)
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
left :
  ∀ (j : C) (y : Functor.obj (Discrete.functor F) { as := j : 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 (Functor.ιColimitType (Discrete.functor F) { as := j } y)),
    Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x =
      Functor.ιColimitType (Discrete.functor F) { as := j } y
⊢ Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x = y

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

Premises used: CategoryTheory.Functor.ιColimitType_jointly_surjective, CategoryTheory.Discrete.functor, 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
i : C
x : Functor.obj (Discrete.functor F) { as := i : Discrete C }
j : C
y : Functor.obj (Discrete.functor F) { as := j : 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 (Functor.ιColimitType (Discrete.functor F) { as := j } y)
left :
  ∀ (y : 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 (Functor.ιColimitType (Discrete.functor F) { as := i } y)),
    Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x =
      Functor.ιColimitType (Discrete.functor F) { as := i } y
⊢ Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x =
    Functor.ιColimitType (Discrete.functor F) { as := j } y

Tactic:
obtain rfl := h₃ _ _ _ _ h

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
i : C
x y : 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 (Functor.ιColimitType (Discrete.functor F) { as := i } y)
left :
  ∀
    (h :
      Functor.descColimitType (Discrete.functor F) c
          (Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x) =
        Functor.descColimitType (Discrete.functor F) c (Functor.ιColimitType (Discrete.functor F) { as := i } x)),
    Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x =
      Functor.ιColimitType (Discrete.functor F) { as := i } x
⊢ Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x =
    Functor.ιColimitType (Discrete.functor F) { as := i } y

Tactic:
obtain rfl := h₂ _ h

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
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 (Functor.ιColimitType (Discrete.functor F) { as := i } x)
⊢ Functor.ιColimitType (Discrete.functor F) { as := i : Discrete C } x =
    Functor.ιColimitType (Discrete.functor F) { as := i } x

Tactic:
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
x : c.pt
right :
  ∀ (i : C) (y : F i),
    ∃ (a : Functor.ColimitType (Discrete.functor F)),
      Functor.descColimitType (Discrete.functor F) c a = c.inj (F := F) i y
⊢ ∃ (a : Functor.ColimitType (Discrete.functor F)), Functor.descColimitType (Discrete.functor F) c a = x

Tactic:
obtain ⟨i, y, rfl⟩ := h₁ x

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
i : C
y : F i
⊢ ∃ (a : Functor.ColimitType (Discrete.functor F)),
    Functor.descColimitType (Discrete.functor F) c a = c.inj (F := F) i y

Tactic:
⟨(Discrete.functor F).ιColimitType ⟨i⟩ y, rfl⟩

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.Discrete.mk, Exists.intro, CategoryTheory.Functor.ιColimitType, 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
i : C
y : F i
⊢ ∃ (a : Functor.ColimitType (Discrete.functor F)),
    Functor.descColimitType (Discrete.functor F) c a = c.inj (F := F) i y

Tactic:
exact ⟨(Discrete.functor F).ιColimitType ⟨i⟩ y, rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
⊢ ∀ (x : (sigma F).pt), ∃ (i : C) (y : F i), (sigma F).inj (F := F) i y = x

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
x : C
x_1 x_2 : F x
h : (sigma F).inj (F := F) x x_1 = (sigma F).inj (F := F) x x_2
⊢ ((sigma F).inj (F := F) x x_1).fst (β := fun (i : C) ↦ F i) =
      ((sigma F).inj (F := F) x x_2).fst (β := fun (i : C) ↦ F i) ∧
    ((sigma F).inj (F := F) x x_1).snd (β := fun (i : C) ↦ F i) ≍
      ((sigma F).inj (F := F) x x_2).snd (β := fun (i : C) ↦ F i)

Tactic:
rw [Sigma.ext_iff] at h

Premises used: Sigma.ext_iff
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
x : C
x_1 x_2 : F x
h :
  ((sigma F).inj (F := F) x x_1).fst (β := fun (i : C) ↦ F i) =
      ((sigma F).inj (F := F) x x_2).fst (β := fun (i : C) ↦ F i) ∧
    ((sigma F).inj (F := F) x x_1).snd (β := fun (i : C) ↦ F i) ≍
      ((sigma F).inj (F := F) x x_2).snd (β := fun (i : C) ↦ F i)
⊢ x_1 = x_2

Tactic:
simpa using h
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
hf : ∀ (j : Discrete C) (x : Functor.obj (Discrete.functor F) j), c.ι j x = fromSigma F c ((sigma F).ι j x)
⊢ Functor.CoconeTypes.IsColimit c ↔ Function.Bijective (fromSigma F c)

Tactic:
rw [(isColimit_sigma F).iff_bijective]

Premises used: CategoryTheory.Limits.CofanTypes.isColimit_sigma, CategoryTheory.Functor.CoconeTypes.IsColimit.iff_bijective
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
⊢ ∀ (j : Discrete C) (x : Functor.obj (Discrete.functor F) j), c.ι j x = fromSigma F c ((sigma F).ι j x)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
hc rwa rwa₁ rwa₂ rwa₃ : Functor.CoconeTypes.IsColimit c
⊢ Function.Bijective (fromSigma F c)

Tactic:
rwa [← isColimit_iff_bijective_fromSigma]

Premises used: CategoryTheory.Limits.CofanTypes.isColimit_iff_bijective_fromSigma
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
hc : Functor.CoconeTypes.IsColimit c
i : C
x : F i
⊢ (equivOfIsColimit (F := F) hc : (a : (i : C) × F i) → c.pt) (Sigma.mk (β := fun (i : C) ↦ F i) i x) =
    c.inj (F := F) i x

Tactic:
rfl

Premises used: CategoryTheory.Limits.CofanTypes.fromSigma, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
hc : Functor.CoconeTypes.IsColimit c
i : C
x : F i
⊢ Eq.{w + 1} (α := c.pt)
    ((equivOfIsColimit (F := F) hc : (a : (i : C) × F i) → c.pt)
        (((equivOfIsColimit (F := F) hc).symm : (a : c.pt) → (i : C) × F i) (c.inj (F := F) i x)) :
      c.pt)
    ((equivOfIsColimit (F := F) hc : (a : (i : C) × F i) → c.pt) (Sigma.mk (β := fun (i : C) ↦ F i) i x) : c.pt)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
hc : Functor.CoconeTypes.IsColimit c
x : c.pt
obtain :
  ∀ (i : C) (y : Functor.obj (Discrete.functor F) { as := i : Discrete C }),
    ∃ (i_1 : C) (y_1 : F i_1), c.inj (F := F) i_1 y_1 = c.ι { as := i } y
⊢ ∃ (i : C) (y : F i), c.inj (F := F) i y = x

Tactic:
obtain ⟨⟨i⟩, y, rfl⟩ := hc.ι_jointly_surjective x

Premises used: CategoryTheory.Functor.CoconeTypes.IsColimit.ι_jointly_surjective, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
hc : Functor.CoconeTypes.IsColimit c
i : C
y : Functor.obj (Discrete.functor F) { as := i : Discrete C }
⊢ ∃ (i_1 : C) (y_1 : F i_1), c.inj (F := F) i_1 y_1 = c.ι { as := i } y

Tactic:
⟨i, y, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
hc : Functor.CoconeTypes.IsColimit c
i : C
y : Functor.obj (Discrete.functor F) { as := i : Discrete C }
⊢ ∃ (i_1 : C) (y_1 : F i_1), c.inj (F := F) i_1 y_1 = c.ι { as := i } y

Tactic:
exact ⟨i, y, rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
hc : Functor.CoconeTypes.IsColimit c
i : C
y₁ y₂ : F i
h : c.inj (F := F) i y₁ = c.inj (F := F) i y₂
⊢ y₁ = y₂

Tactic:
simpa using (equivOfIsColimit hc).injective (a₁ := ⟨i, y₁⟩) (a₂ := ⟨i, y₂⟩) h

Premises used: CategoryTheory.Limits.CofanTypes.equivOfIsColimit, Equiv.injective
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
hc : Functor.CoconeTypes.IsColimit c
i₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
h : c.inj (F := F) i₁ y₁ = c.inj (F := F) i₂ y₂
⊢ i₁ = i₂

Tactic:
congr_arg Sigma.fst ((equivOfIsColimit hc).injective (a₁ := ⟨i₁, y₁⟩) (a₂ := ⟨i₂, y₂⟩) h)

Premises used: Sigma.fst, CategoryTheory.Limits.CofanTypes.equivOfIsColimit, congr_arg, Equiv.injective
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
hc : Functor.CoconeTypes.IsColimit c
i₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
h : i₁ = i₂
rw rw₁ : F i₂ = F i₂
⊢ F i₁ = F i₂

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
hc : Functor.CoconeTypes.IsColimit c
i₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
h : ∃ (h : i₁ = i₂), y₂ = cast ⋯ y₁
h₁ : i₁ = i₂
h₂ : y₂ = cast ⋯ y₁
subst : ∀ (y₂ : F i₁), (∃ (h : i₁ = i₁), y₂ = cast ⋯ y₂) → c.inj (F := F) i₁ y₂ = c.inj (F := F) i₁ y₂
⊢ c.inj (F := F) i₁ y₁ = c.inj (F := F) i₂ y₂

Tactic:
subst h₁ h₂
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
hc : Functor.CoconeTypes.IsColimit c
i₁ : C
y₂ : F i₁
h : ∃ (h : i₁ = i₁), y₂ = cast ⋯ y₂
⊢ c.inj (F := F) i₁ y₂ = c.inj (F := F) i₁ y₂

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
hc : Functor.CoconeTypes.IsColimit c
i₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
refine : ∀ (h : c.inj (F := F) i₁ y₁ = c.inj (F := F) i₂ y₂), ∃ (h : i₁ = i₂), y₂ = cast ⋯ y₁
⊢ c.inj (F := F) i₁ y₁ = c.inj (F := F) i₂ y₂ ↔ ∃ (h : i₁ = i₂), y₂ = cast ⋯ y₁

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨h₁, h₂⟩ ↦ by subst h₁ h₂; rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
hc : Functor.CoconeTypes.IsColimit c
i₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
h : c.inj (F := F) i₁ y₁ = c.inj (F := F) i₂ y₂
obtain : ∀ (y₂ : F i₁) (h : c.inj (F := F) i₁ y₁ = c.inj (F := F) i₁ y₂), ∃ (h : i₁ = i₁), y₂ = cast ⋯ y₁
⊢ ∃ (h : i₁ = i₂), y₂ = cast ⋯ y₁

Tactic:
obtain rfl := eq_of_inj_apply_eq_of_isColimit hc _ _ h

Premises used: CategoryTheory.Limits.CofanTypes.eq_of_inj_apply_eq_of_isColimit, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
hc : Functor.CoconeTypes.IsColimit c
i₁ : C
y₁ y₂ : F i₁
h : c.inj (F := F) i₁ y₁ = c.inj (F := F) i₁ y₂
⊢ ∃ (h : i₁ = i₁), y₂ = cast ⋯ y₁

Tactic:
⟨rfl, (inj_injective_of_isColimit hc i₁ h).symm⟩

Premises used: CategoryTheory.Limits.CofanTypes.inj_injective_of_isColimit, Exists.intro, Eq.symm, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : CofanTypes.{w, v, u} F
hc : Functor.CoconeTypes.IsColimit c
i₁ : C
y₁ y₂ : F i₁
h : c.inj (F := F) i₁ y₁ = c.inj (F := F) i₁ y₂
⊢ ∃ (h : i₁ = i₁), y₂ = cast ⋯ y₁

Tactic:
exact ⟨rfl, (inj_injective_of_isColimit hc i₁ h).symm⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C_1 : Type u
F_1 : C_1 → Type v
C : Type u
F : C → Type v
c : Cofan F
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_1 : Type u
F_1 : C_1 → Type v
C : Type u
F : C → Type v
c : Cofan F
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 } → c.pt)
      (Function.comp (β := Functor.obj (Discrete.functor F) { as := i : Discrete C })
        (match (motive := (x : Discrete C) → Functor.obj (Discrete.functor F) x → c.pt) { as := i : Discrete C } with
        | { as := j } =>
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.inj (f := F) j)) :
            (a : (fun (X : Type v) ↦ X) (F j)) → (fun (X : Type v) ↦ X) c.pt))
        (⇑(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 })))
      (match (motive := (x : Discrete C) → Functor.obj (Discrete.functor F) x → c.pt) { as := i : Discrete C } with
      | { as := j } =>
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.inj (f := F) j)) :
          (a : (fun (X : Type v) ↦ X) (F j)) → (fun (X : Type v) ↦ X) c.pt))
⊢ Eq (α := Functor.obj (Discrete.functor F) { as := i : Discrete C } → c.pt)
    (Function.comp (β := Functor.obj (Discrete.functor F) { as := j : Discrete C })
      (match (motive := (x : Discrete C) → Functor.obj (Discrete.functor F) x → c.pt) { as := j : Discrete C } with
      | { as := j } =>
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.inj (f := F) j)) :
          (a : (fun (X : Type v) ↦ X) (F j)) → (fun (X : Type v) ↦ X) c.pt))
      (⇑(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 })))
    (match (motive := (x : Discrete C) → Functor.obj (Discrete.functor F) x → c.pt) { as := i : Discrete C } with
    | { as := j } =>
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.inj (f := F) j)) :
        (a : (fun (X : Type v) ↦ X) (F j)) → (fun (X : Type v) ↦ X) c.pt))

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

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C_1 : Type u
F_1 : C_1 → Type v
C : Type u
F : C → Type v
c : Cofan F
i : C
f : { as := i : Discrete C } ⟶ { as := i }
⊢ Eq (α := Functor.obj (Discrete.functor F) { as := i : Discrete C } → c.pt)
    (Function.comp (β := Functor.obj (Discrete.functor F) { as := i : Discrete C })
      (match (motive := (x : Discrete C) → Functor.obj (Discrete.functor F) x → c.pt) { as := i : Discrete C } with
      | { as := j } =>
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.inj (f := F) j)) :
          (a : (fun (X : Type v) ↦ X) (F j)) → (fun (X : Type v) ↦ X) c.pt))
      (⇑(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 })))
    (match (motive := (x : Discrete C) → Functor.obj (Discrete.functor F) x → c.pt) { as := i : Discrete C } with
    | { as := j } =>
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.inj (f := F) j)) :
        (a : (fun (X : Type v) ↦ X) (F j)) → (fun (X : Type v) ↦ X) c.pt))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : Cofan F
⊢ Functor.CoconeTypes.IsColimit (c.cofanTypes (F := F)) ↔ Nonempty (IsColimit c)

Tactic:
Functor.CoconeTypes.isColimit_iff _

Premises used: CategoryTheory.Functor.CoconeTypes.isColimit_iff
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : Cofan F
rw :
  Functor.CoconeTypes.IsColimit (c.cofanTypes (F := F)) ↔
    Function.Bijective (β := c.cofanTypes (F := F).pt) (CofanTypes.fromSigma F (c.cofanTypes (F := F)))
rw₁ rw₂ :
  Function.Bijective (β := c.cofanTypes (F := F).pt) (CofanTypes.fromSigma F (c.cofanTypes (F := F))) ↔
    Function.Bijective (β := c.cofanTypes (F := F).pt) (CofanTypes.fromSigma F (c.cofanTypes (F := F)))
⊢ Nonempty (IsColimit c) ↔
    Function.Bijective (β := c.cofanTypes (F := F).pt) (CofanTypes.fromSigma F (c.cofanTypes (F := F)))

Tactic:
rw [← isColimit_cofanTypes_iff, CofanTypes.isColimit_iff_bijective_fromSigma]

Premises used: CategoryTheory.Limits.CofanTypes.isColimit_iff_bijective_fromSigma, CategoryTheory.Limits.Cofan.isColimit_cofanTypes_iff
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : Cofan F
hc : IsColimit c
x : c.pt
⊢ ∃ (i : C) (y : F i),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (c.inj (f := F) i) :
          (a : (fun (X : Type v) ↦ X) (F i)) → (fun (X : Type v) ↦ X) c.pt)
        y =
      x

Tactic:
CofanTypes.inj_jointly_surjective_of_isColimit
    ((isColimit_cofanTypes_iff c).2 ⟨hc⟩) x

Premises used: Iff.mpr, CategoryTheory.Limits.CofanTypes.inj_jointly_surjective_of_isColimit, Nonempty.intro, CategoryTheory.Limits.Cofan.isColimit_cofanTypes_iff
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : Cofan F
hc : IsColimit c
i : C
⊢ Function.Injective (α := (fun (X : Type v) ↦ X) (F i)) (β := (fun (X : Type v) ↦ X) c.pt)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.inj (f := F) i)) :
      (a : (fun (X : Type v) ↦ X) (F i)) → (fun (X : Type v) ↦ X) c.pt)

Tactic:
CofanTypes.inj_injective_of_isColimit ((isColimit_cofanTypes_iff c).2 ⟨hc⟩) i

Premises used: Iff.mpr, CategoryTheory.Limits.CofanTypes.inj_injective_of_isColimit, Nonempty.intro, CategoryTheory.Limits.Cofan.isColimit_cofanTypes_iff
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : Cofan F
hc : IsColimit c
i₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
h :
  Eq (α := (fun (X : Type v) ↦ X) c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.inj (f := F) i₁) :
          (a : (fun (X : Type v) ↦ X) (F i₁)) → (fun (X : Type v) ↦ X) c.pt)
        y₁ :
      (fun (X : Type v) ↦ X) c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.inj (f := F) i₂) :
          (a : (fun (X : Type v) ↦ X) (F i₂)) → (fun (X : Type v) ↦ X) c.pt)
        y₂ :
      (fun (X : Type v) ↦ X) c.pt)
⊢ i₁ = i₂

Tactic:
CofanTypes.eq_of_inj_apply_eq_of_isColimit ((isColimit_cofanTypes_iff c).2 ⟨hc⟩) _ _ h

Premises used: Iff.mpr, CategoryTheory.Limits.CofanTypes.eq_of_inj_apply_eq_of_isColimit, Nonempty.intro, CategoryTheory.Limits.Cofan.isColimit_cofanTypes_iff
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C_1 : Type u
F_1 : C_1 → Type v
C : Type u
F : C → Type v
c : Cofan F
hc : IsColimit c
i j : C
x : F i
y : F j
hij : i = j
rw rw₁ : F j = F j
⊢ F i = F j

Tactic:
rw [hij]
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
c : Cofan F
hc : IsColimit c
i j : C
x : F i
y : F j
⊢ Eq (α := (fun (X : Type v) ↦ X) c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.inj (f := F) i) :
            (a : (fun (X : Type v) ↦ X) (F i)) → (fun (X : Type v) ↦ X) c.pt)
          x :
        (fun (X : Type v) ↦ X) c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.inj (f := F) j) :
            (a : (fun (X : Type v) ↦ X) (F j)) → (fun (X : Type v) ↦ X) c.pt)
          y :
        (fun (X : Type v) ↦ X) c.pt) ↔
    ∃ (hij : i = j), y = cast ⋯ x

Tactic:
CofanTypes.inj_apply_eq_iff_of_isColimit ((isColimit_cofanTypes_iff c).2 ⟨hc⟩) _ _

Premises used: Iff.mpr, CategoryTheory.Limits.CofanTypes.inj_apply_eq_iff_of_isColimit, Nonempty.intro, CategoryTheory.Limits.Cofan.isColimit_cofanTypes_iff
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
x : Cocone.{u_1, u, u_1, u + 1} (Functor.empty (Type u))
x_1 :
  Cocone.pt.{u_1, u, u_1, u + 1}
      { pt := PEmpty.{u + 1},
        ι :=
          Iso.inv (Functor.uniqueFromEmpty (Functor.obj (Functor.const (Discrete PEmpty.{u_1 + 1})) PEmpty.{u + 1})) :
        Cocone.{u_1, u, u_1, u + 1} (Functor.empty (Type u)) } ⟶
    x.pt
h_1 :
  ∀ (j : Discrete PEmpty.{u_1 + 1}),
    NatTrans.app
          (Cocone.ι
            { pt := PEmpty.{u + 1},
              ι :=
                Iso.inv
                  (Functor.uniqueFromEmpty (Functor.obj (Functor.const (Discrete PEmpty.{u_1 + 1})) PEmpty.{u + 1})) })
          j ≫
        x_1 =
      x.ι.app j
h :
  ∀
    (x_2 :
      Cocone.pt.{u_1, u, u_1, u + 1}
        { pt := PEmpty.{u + 1},
          ι :=
            Iso.inv
              (Functor.uniqueFromEmpty (Functor.obj (Functor.const (Discrete PEmpty.{u_1 + 1})) PEmpty.{u + 1})) }),
    (ConcreteCategory.hom (FC := TypeCat.Fun) x_1).toFun x_2 =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾fun
              (x_3 :
                Cocone.pt.{u_1, u, u_1, u + 1}
                  { pt := PEmpty.{u + 1},
                    ι :=
                      Iso.inv
                        (Functor.uniqueFromEmpty
                          (Functor.obj (Functor.const (Discrete PEmpty.{u_1 + 1})) PEmpty.{u + 1})) :
                    Cocone.{u_1, u, u_1, u + 1} (Functor.empty (Type u)) }) ↦
            PEmpty.elim x_3))
        x_2
⊢ x_1 =
    ↾fun
        (x_2 :
          Cocone.pt.{u_1, u, u_1, u + 1}
            { pt := PEmpty.{u + 1},
              ι :=
                Iso.inv
                  (Functor.uniqueFromEmpty
                    (Functor.obj (Functor.const (Discrete PEmpty.{u_1 + 1})) PEmpty.{u + 1})) }) ↦
      PEmpty.elim x_2

Tactic:
ext x