Theorem: Category.HomQuotient.quotient_essSurjective (CategoryTheory/Basic.lean)

State before:
α : Type u_1
β : Type ?u.92381
γ : Type ?u.92384
δ : Type ?u.92387
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
⊢ EssSurjective (quotient r)
Tactic:
intro B
State after:
α : Type u_1
β : Type ?u.92381
γ : Type ?u.92384
δ : Type ?u.92387
A B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
B : HomQuotient r
⊢ Nonempty ((A : α) ×' (Functor.obj (quotient r) A ≃ B))

State before:
α : Type u_1
β : Type ?u.92381
γ : Type ?u.92384
δ : Type ?u.92387
A B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
B : HomQuotient r
⊢ Nonempty ((A : α) ×' (Functor.obj (quotient r) A ≃ B))
Tactic:
exact ⟨⟨B.unquot, Iso.refl _⟩⟩
State after:
no goals