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

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

Tactic:
refine fun ⟨hc⟩ => ⟨fun x y h => ?_, fun x => ?_⟩

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
⊢ x = y

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
⊢ ∃ a, Quot.desc c a = x

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) }
j : J
x : F.obj j
⊢ (c.ι.app j ≫ f₁) x = (c.ι.app j ≫ f₂) x

Tactic:
simpa [f₁, f₂] using ⟨Quot.ι F j x, by simp⟩

Result:
no goals

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

Tactic:
refine fun 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)
⊢ IsColimit c

Proof state:
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

Tactic:
obtain ⟨x, rfl⟩ := e.surjective x

Result:
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)

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✝ : 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) }
j : J
x : F.obj j
⊢ Quot.desc c (Quot.ι F j x) = c.ι.app j x

Tactic:
simp

Result:
no goals

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) }
⊢ f₁ = f₂

Tactic:
refine hc.hom_ext fun j => funext fun 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) }
j : J
x : F.obj j
⊢ (c.ι.app j ≫ f₁) x = (c.ι.app j ≫ f₂) x

Proof state:
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
j : J
x : F.obj j
⊢ (c.ι.app j ≫ (fun s => Quot.desc s ∘ ⇑e.symm) s) x = s.ι.app j x

Tactic:
simp [h]

Result:
no goals

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
⊢ ∃ a, Quot.desc c a = x

Tactic:
let f₁ : c.pt ⟶ ULift.{u} Bool := fun _ => ULift.up true

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 }
⊢ ∃ a, Quot.desc c a = x

Proof state:
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 (c.ι.app j x) = (fun s => Quot.desc s ∘ ⇑e.symm) s (c.ι.app j x)

Tactic:
simpa [h] using congrFun (hm j) x

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
j : J
⊢ c.ι.app j ≫ (fun s => Quot.desc s ∘ ⇑e.symm) s = s.ι.app j

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
j : J
x : F.obj j
⊢ (c.ι.app j ≫ (fun s => Quot.desc s ∘ ⇑e.symm) s) x = s.ι.app j x

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

Tactic:
refine ⟨?_, ?_⟩

Result:
case refine_1
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
⊢ Nonempty (IsColimit c) → Function.Bijective (Quot.desc c)

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

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 : 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) }
this : f₁ = f₂
⊢ ∃ a, Quot.desc c a = x

Tactic:
simpa [f₁, f₂] using congrFun this 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
⊢ x = y

Tactic:
let f : Quot F → ULift.{u} Bool := fun z => ULift.up (x = z)

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) }
⊢ x = y

Proof state:
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))

Tactic:
rw [← h, Equiv.apply_symm_apply]

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 (c.ι.app j x) = (fun s => Quot.desc s ∘ ⇑e.symm) s (c.ι.app j x)