-- Mathlib/CategoryTheory/Limits/Types.lean
theorem isColimit_iff_bijective_desc : Nonempty (IsColimit c) ↔ (Quot.desc c).Bijective

Proof state:
case refine_1.refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
x : c.pt
f₁ : c.pt ⟶ ULift.{u, 0} Bool := fun x => { down := true }
f₂ : c.pt ⟶ ULift.{u, 0} Bool := fun x => { down := decide (∃ a, Quot.desc c a = x) }
⊢ ∃ a, Quot.desc c a = x

Tactic:
suffices f₁ = f₂ by simpa [f₁, f₂] using congrFun this x

Result:
case refine_1.refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
x : c.pt
f₁ : c.pt ⟶ ULift.{u, 0} Bool := fun x => { down := true }
f₂ : c.pt ⟶ ULift.{u, 0} Bool := fun x => { down := decide (∃ a, Quot.desc c a = x) }
⊢ f₁ = f₂

Proof state:
case refine_1.refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
x : c.pt
f₁ : c.pt ⟶ ULift.{u, 0} Bool := fun x => { down := true }
⊢ ∃ a, Quot.desc c a = x

Tactic:
let f₂ : c.pt ⟶ ULift.{u} Bool := fun x => ULift.up (∃ a, Quot.desc c a = x)

Result:
case refine_1.refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
x : c.pt
f₁ : c.pt ⟶ ULift.{u, 0} Bool := fun x => { down := true }
f₂ : c.pt ⟶ ULift.{u, 0} Bool := fun x => { down := decide (∃ a, Quot.desc c a = x) }
⊢ ∃ a, Quot.desc c a = x

Proof state:
case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
h✝ : Function.Bijective (Quot.desc c)
e : Quot F ≃ c.pt := Equiv.ofBijective (Quot.desc c) h✝
h : ∀ (j : J) (x : F.obj j), e.symm (c.ι.app j x) = Quot.ι F j x
⊢ IsColimit c

Tactic:
exact
  { desc := fun s => Quot.desc s ∘ e.symm
    fac := fun s j => by
      ext x
      simp [h]
    uniq := fun s m hm => by
      ext x
      obtain ⟨x, rfl⟩ := e.surjective x
      obtain ⟨j, x, rfl⟩ := Quot.jointly_surjective x
      rw [← h, Equiv.apply_symm_apply]
      simpa [h] using congrFun (hm j) x }

Result:
no goals

Proof state:
case refine_1.refine_1
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
x y : Quot F
h : Quot.desc c x = Quot.desc c y
f : Quot F → ULift.{u, 0} Bool := fun z => { down := decide (x = z) }
⊢ f x = f y

Tactic:
rw [← Quot.desc_toCocone_desc c f hc x, h, Quot.desc_toCocone_desc]

Result:
no goals

Proof state:
case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
h : Function.Bijective (Quot.desc c)
e : Quot F ≃ c.pt := Equiv.ofBijective (Quot.desc c) h
⊢ IsColimit c

Tactic:
have h : ∀ j x, e.symm (c.ι.app j x) = Quot.ι F j x :=
  fun j x => e.injective (Equiv.ofBijective_apply_symm_apply _ _ _)

Result:
case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
h✝ : Function.Bijective (Quot.desc c)
e : Quot F ≃ c.pt := Equiv.ofBijective (Quot.desc c) h✝
h : ∀ (j : J) (x : F.obj j), e.symm (c.ι.app j x) = Quot.ι F j x
⊢ IsColimit c

Proof state:
case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
h : Function.Bijective (Quot.desc c)
⊢ IsColimit c

Tactic:
let e := Equiv.ofBijective _ h

Result:
case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
h : Function.Bijective (Quot.desc c)
e : Quot F ≃ c.pt := Equiv.ofBijective (Quot.desc c) h
⊢ IsColimit c

Proof state:
case refine_1.refine_1
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
x y : Quot F
h : Quot.desc c x = Quot.desc c y
f : Quot F → ULift.{u, 0} Bool := fun z => { down := decide (x = z) }
⊢ x = y

Tactic:
suffices f x = f y by simpa [f] using this

Result:
case refine_1.refine_1
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
x y : Quot F
h : Quot.desc c x = Quot.desc c y
f : Quot F → ULift.{u, 0} Bool := fun z => { down := decide (x = z) }
⊢ f x = f y

Proof state:
case h.intro
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
h✝ : Function.Bijective (Quot.desc c)
e : Quot F ≃ c.pt := Equiv.ofBijective (Quot.desc c) h✝
h : ∀ (j : J) (x : F.obj j), e.symm (c.ι.app j x) = Quot.ι F j x
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
⊢ m (e x) = (fun s => Quot.desc s ∘ ⇑e.symm) s (e x)

Tactic:
obtain ⟨j, x, rfl⟩ := Quot.jointly_surjective x

Result:
case h.intro.intro.intro
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
h✝ : Function.Bijective (Quot.desc c)
e : Quot F ≃ c.pt := Equiv.ofBijective (Quot.desc c) h✝
h : ∀ (j : J) (x : F.obj j), e.symm (c.ι.app j x) = Quot.ι F j x
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
j : J
x : F.obj j
⊢ m (e (Quot.ι F j x)) = (fun s => Quot.desc s ∘ ⇑e.symm) s (e (Quot.ι F j x))

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
x y : Quot F
h : Quot.desc c x = Quot.desc c y
f : Quot F → ULift.{u, 0} Bool := fun z => { down := decide (x = z) }
this : f x = f y
⊢ x = y

Tactic:
simpa [f] using this

Result:
no goals

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
h✝ : Function.Bijective (Quot.desc c)
e : Quot F ≃ c.pt := Equiv.ofBijective (Quot.desc c) h✝
h : ∀ (j : J) (x : F.obj j), e.symm (c.ι.app j x) = Quot.ι F j x
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
⊢ m = (fun s => Quot.desc s ∘ ⇑e.symm) s

Tactic:
ext x

Result:
case h
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
h✝ : Function.Bijective (Quot.desc c)
e : Quot F ≃ c.pt := Equiv.ofBijective (Quot.desc c) h✝
h : ∀ (j : J) (x : F.obj j), e.symm (c.ι.app j x) = Quot.ι F j x
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : c.pt
⊢ m x = (fun s => Quot.desc s ∘ ⇑e.symm) s x