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

Tactic:
(ιColimitType_eq_iff ..).mpr (.trans _ _ _ (.rel _ ⟨k, F.map f x⟩ ⟨f, rfl⟩)
    (.symm _ _ (.rel _ _ ⟨f', H⟩)))

Premises used: Iff.mpr, Relation.EqvGen.trans, Exists.intro, Relation.EqvGen.rel, Relation.EqvGen.symm, CategoryTheory.Functor.ιColimitType_eq_iff
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
t : F.ColimitType
mk :
  ∀ (fst : J) (snd : F.obj fst),
    ∃ (j : J) (x : F.obj j),
      F.ιColimitType j x = Quot.mk F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) fst snd)
⊢ ∃ (j : J) (x : F.obj j), F.ιColimitType j x = t

Tactic:
obtain ⟨_, _⟩ := t
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
t : F.ColimitType
fst : J
snd : F.obj fst
⊢ ∃ (j : J) (x : F.obj j), F.ιColimitType j x = Quot.mk F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) fst snd)

Tactic:
⟨_, _, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
t : F.ColimitType
fst : J
snd : F.obj fst
⊢ ∃ (j : J) (x : F.obj j), F.ιColimitType j x = Quot.mk F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) fst snd)

Tactic:
exact ⟨_, _, rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
j j' : J
f : j ⟶ j'
x : F.obj j
⊢ F.ιColimitType j'
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j'))
        x) =
    F.ιColimitType j x

Tactic:
(Quot.sound ⟨f, rfl⟩).symm

Premises used: Quot.sound, CategoryTheory.Functor.ColimitType, Eq.symm, CategoryTheory.Functor.ιColimitType
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{u_1, w₀, v, u} F
a b : (j : J) × F.obj j
w : a.fst (β := fun (j : J) ↦ F.obj j) ⟶ b.fst (β := fun (j : J) ↦ F.obj j)
h :
  b.snd (β := fun (j : J) ↦ F.obj j) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map w) :
        (a : (fun (X : Type w₀) ↦ X) (F.obj a.fst)) → (fun (X : Type w₀) ↦ X) (F.obj b.fst))
      (a.snd (β := fun (j : J) ↦ F.obj j))
⊢ Eq.{u_1 + 1} (α := c.pt)
    ((fun (x : (j : J) × F.obj j) ↦
        (match (motive := (j : J) × F.obj j → c.pt) x with
          | ⟨j, x⟩ => c.ι j x :
          c.pt))
      a)
    ((fun (x : (j : J) × F.obj j) ↦
        (match (motive := (j : J) × F.obj j → c.pt) x with
          | ⟨j, x⟩ => c.ι j x :
          c.pt))
      b)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{u_1, w₀, v, u} F
j : J
⊢ F.descColimitType c ∘ F.ιColimitType j = c.ι j

Tactic:
rfl

Premises used: CategoryTheory.Functor.descColimitType, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{u_1, w₀, v, u} F
j : J
x : F.obj j
⊢ F.descColimitType c (F.ιColimitType j x) = c.ι j x

Tactic:
rfl

Premises used: CategoryTheory.Functor.descColimitType, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
mp : Function.Surjective (F.descColimitType c) → ∀ (z : c.pt), ∃ (i : J) (x : F.obj i), c.ι i x = z
mpr : (∀ (z : c.pt), ∃ (i : J) (x : F.obj i), c.ι i x = z) → Function.Surjective (F.descColimitType c)
⊢ Function.Surjective (F.descColimitType c) ↔ ∀ (z : c.pt), ∃ (i : J) (x : F.obj i), c.ι i x = z

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
h : Function.Surjective (F.descColimitType c)
z : c.pt
mp :
  ∀ (w : F.ColimitType) (i : J) (x : F.obj i),
    ∃ (i_1 : J) (x_1 : F.obj i_1),
      c.ι i_1 x_1 = F.descColimitType c (Quot.mk F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) i x))
⊢ ∃ (i : J) (x : F.obj i), c.ι i x = z

Tactic:
obtain ⟨⟨i, x⟩, rfl⟩ := h z

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
h : Function.Surjective (F.descColimitType c)
w : F.ColimitType
i : J
x : F.obj i
⊢ ∃ (i_1 : J) (x_1 : F.obj i_1),
    c.ι i_1 x_1 = F.descColimitType c (Quot.mk F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) i x))

Tactic:
⟨i, x, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
h : Function.Surjective (F.descColimitType c)
w : F.ColimitType
i : J
x : F.obj i
⊢ ∃ (i_1 : J) (x_1 : F.obj i_1),
    c.ι i_1 x_1 = F.descColimitType c (Quot.mk F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) i x))

Tactic:
exact ⟨i, x, rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
h : ∀ (z : c.pt), ∃ (i : J) (x : F.obj i), c.ι i x = z
z : c.pt
mpr : ∀ (i : J) (x : F.obj i), ∃ (a : F.ColimitType), F.descColimitType c a = c.ι i x
⊢ ∃ (a : F.ColimitType), F.descColimitType c a = z

Tactic:
obtain ⟨i, x, rfl⟩ := h z

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
h : ∀ (z : c.pt), ∃ (i : J) (x : F.obj i), c.ι i x = z
i : J
x : F.obj i
⊢ ∃ (a : F.ColimitType), F.descColimitType c a = c.ι i x

Tactic:
⟨F.ιColimitType i x, rfl⟩

Premises used: Exists.intro, CategoryTheory.Functor.ιColimitType, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
h : ∀ (z : c.pt), ∃ (i : J) (x : F.obj i), c.ι i x = z
i : J
x : F.obj i
⊢ ∃ (a : F.ColimitType), F.descColimitType c a = c.ι i x

Tactic:
exact ⟨F.ιColimitType i x, rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
j : J
x : F.obj j
⊢ Eq.{w₁ + 1} (α := c.pt)
    ((hc.equiv : (a : F.ColimitType) → c.pt) ((hc.equiv.symm : (a : c.pt) → F.ColimitType) (c.ι j x)) : c.pt)
    ((hc.equiv : (a : F.ColimitType) → c.pt) (F.ιColimitType j x) : c.pt)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
y : c.pt
obtain : ∀ (z : F.ColimitType), ∃ (j : J) (x : F.obj j), c.ι j x = (hc.equiv : (a : F.ColimitType) → c.pt) z
⊢ ∃ (j : J) (x : F.obj j), c.ι j x = y

Tactic:
obtain ⟨z, rfl⟩ := hc.equiv.surjective y

Premises used: CategoryTheory.Functor.CoconeTypes.IsColimit.equiv, Equiv.surjective, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
z : F.ColimitType
obtain :
  ∀ (j : J) (x : F.obj j),
    ∃ (j_1 : J) (x_1 : F.obj j_1), c.ι j_1 x_1 = (hc.equiv : (a : F.ColimitType) → c.pt) (F.ιColimitType j x)
⊢ ∃ (j : J) (x : F.obj j), c.ι j x = (hc.equiv : (a : F.ColimitType) → c.pt) z

Tactic:
obtain ⟨j, x, rfl⟩ := F.ιColimitType_jointly_surjective z

Premises used: CategoryTheory.Functor.ιColimitType_jointly_surjective, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
j : J
x : F.obj j
⊢ ∃ (j_1 : J) (x_1 : F.obj j_1), c.ι j_1 x_1 = (hc.equiv : (a : F.ColimitType) → c.pt) (F.ιColimitType j x)

Tactic:
⟨j, x, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
j : J
x : F.obj j
⊢ ∃ (j_1 : J) (x_1 : F.obj j_1), c.ι j_1 x_1 = (hc.equiv : (a : F.ColimitType) → c.pt) (F.ιColimitType j x)

Tactic:
exact ⟨j, x, rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
T : Type w₂
f g : c.pt → T
h : ∀ (j : J), f ∘ c.ι j = g ∘ c.ι j
h₁ : ∀ (y : c.pt), f y = g y
⊢ f = g

Tactic:
funext y
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
T : Type w₂
f g : c.pt → T
h : ∀ (j : J), f ∘ c.ι j = g ∘ c.ι j
y : c.pt
h₁ : ∀ (j : J) (x : F.obj j), f (c.ι j x) = g (c.ι j x)
⊢ f y = g y

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

Premises used: CategoryTheory.Functor.CoconeTypes.IsColimit.ι_jointly_surjective, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
T : Type w₂
f g : c.pt → T
h : ∀ (j : J), f ∘ c.ι j = g ∘ c.ι j
j : J
x : F.obj j
⊢ f (c.ι j x) = g (c.ι j x)

Tactic:
congr_fun (h j) x

Premises used: congr_fun
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
T : Type w₂
f g : c.pt → T
h : ∀ (j : J), f ∘ c.ι j = g ∘ c.ι j
j : J
x : F.obj j
⊢ f (c.ι j x) = g (c.ι j x)

Tactic:
exact congr_fun (h j) x

Premises used: congr_fun
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
⊢ ∀ (j : J), (F.descColimitType c' ∘ (⇑hc.equiv.symm : (a : c.pt) → F.ColimitType)) ∘ c.ι j = c'.ι j

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
j : J
⊢ hc.desc c' ∘ c.ι j = c'.ι j

Tactic:
(hc.exists_desc c').choose_spec j

Premises used: Exists.choose_spec, CategoryTheory.Functor.CoconeTypes.IsColimit.exists_desc, CategoryTheory.Functor.CoconeTypes.IsColimit.desc
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
j : J
x : F.obj j
⊢ hc.desc c' (c.ι j x) = c'.ι j x

Tactic:
congr_fun (hc.fac c' j) x

Premises used: Classical.choose, congr_fun, CategoryTheory.Functor.CoconeTypes.IsColimit.desc, CategoryTheory.Functor.CoconeTypes.IsColimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
e : Equiv.{w₁ + 1, w₂ + 1} c.pt c'.pt
he : ∀ (j : J) (x : F.obj j), c'.ι j x = (e : (a : c.pt) → c'.pt) (c.ι j x)
⊢ Function.Bijective (β := c'.pt) ((⇑e : (a : c.pt) → c'.pt) ∘ F.descColimitType c)

Tactic:
Function.Bijective.comp e.bijective hc.bijective

Premises used: CategoryTheory.Functor.CoconeTypes.IsColimit.bijective, Equiv.bijective, Function.Bijective.comp
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
e : Equiv.{w₁ + 1, w₂ + 1} c.pt c'.pt
he : ∀ (j : J) (x : F.obj j), c'.ι j x = (e : (a : c.pt) → c'.pt) (c.ι j x)
h : F.descColimitType c' = (⇑e : (a : c.pt) → c'.pt) ∘ F.descColimitType c
⊢ Function.Bijective (F.descColimitType c')

Tactic:
convert! Function.Bijective.comp e.bijective hc.bijective

Premises used: CategoryTheory.Functor.CoconeTypes.IsColimit.bijective, Equiv.bijective, Function.Bijective.comp
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
e : Equiv.{w₁ + 1, w₂ + 1} c.pt c'.pt
he : ∀ (j : J) (x : F.obj j), c'.ι j x = (e : (a : c.pt) → c'.pt) (c.ι j x)
h : ∀ (y : F.ColimitType), F.descColimitType c' y = ((⇑e : (a : c.pt) → c'.pt) ∘ F.descColimitType c) y
⊢ F.descColimitType c' = (⇑e : (a : c.pt) → c'.pt) ∘ F.descColimitType c

Tactic:
ext y
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
e : Equiv.{w₁ + 1, w₂ + 1} c.pt c'.pt
he : ∀ (j : J) (x : F.obj j), c'.ι j x = (e : (a : c.pt) → c'.pt) (c.ι j x)
y : F.ColimitType
h :
  ∀ (j : J) (x : F.obj j),
    F.descColimitType c' (F.ιColimitType j x) = ((⇑e : (a : c.pt) → c'.pt) ∘ F.descColimitType c) (F.ιColimitType j x)
⊢ F.descColimitType c' y = ((⇑e : (a : c.pt) → c'.pt) ∘ F.descColimitType c) y

Tactic:
obtain ⟨j, x, rfl⟩ := F.ιColimitType_jointly_surjective y

Premises used: CategoryTheory.Functor.ιColimitType_jointly_surjective, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
e : Equiv.{w₁ + 1, w₂ + 1} c.pt c'.pt
he : ∀ (j : J) (x : F.obj j), c'.ι j x = (e : (a : c.pt) → c'.pt) (c.ι j x)
j : J
x : F.obj j
⊢ F.descColimitType c' (F.ιColimitType j x) = ((⇑e : (a : c.pt) → c'.pt) ∘ F.descColimitType c) (F.ιColimitType j x)

Tactic:
simp_all
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
⊢ c'.IsColimit ↔ Function.Bijective f

Tactic:
⟨fun hc' ↦ ?_, fun h ↦ hc.of_equiv (Equiv.ofBijective _ h) hf⟩

Premises used: Equiv.ofBijective, Iff.intro, CategoryTheory.Functor.CoconeTypes.IsColimit.of_equiv
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
refine : ∀ (hc' : c'.IsColimit), Function.Bijective f
⊢ c'.IsColimit ↔ Function.Bijective f

Tactic:
refine ⟨fun hc' ↦ ?_, fun h ↦ hc.of_equiv (Equiv.ofBijective _ h) hf⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
hc' : c'.IsColimit
⊢ Function.Bijective (F.descColimitType c)

Tactic:
have h₁ := hc.bijective
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
hc' : c'.IsColimit
h₁ : Function.Bijective (F.descColimitType c)
rw : Function.Bijective (f ∘ F.descColimitType c)
⊢ Function.Bijective f

Tactic:
rw [← Function.Bijective.of_comp_iff _ hc.bijective]

Premises used: CategoryTheory.Functor.CoconeTypes.IsColimit.bijective, Function.Bijective.of_comp_iff
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
hc' : c'.IsColimit
h₁ : Function.Bijective (F.descColimitType c)
⊢ Function.Bijective (F.descColimitType c')

Tactic:
hc'.bijective

Premises used: CategoryTheory.Functor.CoconeTypes.IsColimit.bijective
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
hc' : c'.IsColimit
h₁ : Function.Bijective (F.descColimitType c)
h : f ∘ F.descColimitType c = F.descColimitType c'
⊢ Function.Bijective (f ∘ F.descColimitType c)

Tactic:
convert! hc'.bijective

Premises used: CategoryTheory.Functor.CoconeTypes.IsColimit.bijective
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
hc' : c'.IsColimit
h₁ : Function.Bijective (F.descColimitType c)
h : ∀ (x : F.ColimitType), (f ∘ F.descColimitType c) x = F.descColimitType c' x
⊢ f ∘ F.descColimitType c = F.descColimitType c'

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
hc' : c'.IsColimit
h₁ : Function.Bijective (F.descColimitType c)
x : F.ColimitType
h : ∀ (j : J) (x : F.obj j), (f ∘ F.descColimitType c) (F.ιColimitType j x) = F.descColimitType c' (F.ιColimitType j x)
⊢ (f ∘ F.descColimitType c) x = F.descColimitType c' x

Tactic:
obtain ⟨j, x, rfl⟩ := F.ιColimitType_jointly_surjective x

Premises used: CategoryTheory.Functor.ιColimitType_jointly_surjective, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
c' : CoconeTypes.{w₂, w₀, v, u} F
f : c.pt → c'.pt
hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)
hc' : c'.IsColimit
h₁ : Function.Bijective (F.descColimitType c)
j : J
x : F.obj j
⊢ (f ∘ F.descColimitType c) (F.ιColimitType j x) = F.descColimitType c' (F.ιColimitType j x)

Tactic:
simp [hf]
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : IsColimitCore.{w₂, w₁, w₀, v, u} c
c' : CoconeTypes.{w₂, w₀, v, u} F
j : J
x : F.obj j
⊢ hc.desc c' (c.ι j x) = c'.ι j x

Tactic:
congr_fun (hc.fac c' j) x

Premises used: CategoryTheory.Functor.CoconeTypes.IsColimitCore.fac, congr_fun
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
c' : CoconeTypes.{w₂, w₀, v, u} F
j : J
rw :
  Equiv.toFun Equiv.ulift ∘
      (c'.postcomp (T := ULift.{w₃, w₂} c'.pt) (⇑(Equiv.symm Equiv.ulift) : (a : c'.pt) → ULift.{w₃, w₂} c'.pt)).ι j =
    c'.ι j
⊢ (Equiv.toFun Equiv.ulift ∘
        hc.desc
          (c'.postcomp (T := ULift.{w₃, w₂} c'.pt) (⇑(Equiv.symm Equiv.ulift) : (a : c'.pt) → ULift.{w₃, w₂} c'.pt))) ∘
      c.ι j =
    c'.ι j

Tactic:
rw [Function.comp_assoc, hc.fac]

Premises used: CategoryTheory.Functor.CoconeTypes.IsColimitCore.fac, Function.comp_assoc
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
c' : CoconeTypes.{w₂, w₀, v, u} F
j : J
⊢ Equiv.toFun Equiv.ulift ∘
      (c'.postcomp (T := ULift.{w₃, w₂} c'.pt) (⇑(Equiv.symm Equiv.ulift) : (a : c'.pt) → ULift.{w₃, w₂} c'.pt)).ι j =
    c'.ι j

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
T : Type w₂
f g : c.pt → T
h : ∀ (j : J), f ∘ c.ι j = g ∘ c.ι j
this : Equiv.invFun Equiv.ulift ∘ f = Equiv.invFun Equiv.ulift ∘ g
h₁ : ∀ (x : c.pt), f x = g x
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
T : Type w₂
f g : c.pt → T
h : ∀ (j : J), f ∘ c.ι j = g ∘ c.ι j
this : Equiv.invFun Equiv.ulift ∘ f = Equiv.invFun Equiv.ulift ∘ g
x : c.pt
⊢ f x = g x

Tactic:
simpa using congr_fun this x

Premises used: congr_fun
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
T : Type w₂
f g : c.pt → T
h : ∀ (j : J), f ∘ c.ι j = g ∘ c.ι j
suffices : Equiv.invFun Equiv.ulift ∘ f = Equiv.invFun Equiv.ulift ∘ g
⊢ f = g

Tactic:
suffices Equiv.ulift.{w₃}.invFun.comp f =
        Equiv.ulift.invFun.comp g by
      ext x
      simpa using congr_fun this x
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
T : Type w₂
f g : c.pt → T
h : ∀ (j : J), f ∘ c.ι j = g ∘ c.ι j
j : J
⊢ (Equiv.invFun Equiv.ulift ∘ f) ∘ c.ι j = (Equiv.invFun Equiv.ulift ∘ g) ∘ c.ι j

Tactic:
simp [Function.comp_assoc, h]

Premises used: Function.comp_assoc
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
T : Type w₂
f g : c.pt → T
h : ∀ (j : J), f ∘ c.ι j = g ∘ c.ι j
⊢ Equiv.invFun Equiv.ulift ∘ f = Equiv.invFun Equiv.ulift ∘ g

Tactic:
exact hc.funext (fun j ↦ by simp [Function.comp_assoc, h])

Premises used: CategoryTheory.Functor.CoconeTypes.IsColimitCore.funext