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

State before:
α : Type u_1
β : Type ?u.92190
γ : Type ?u.92193
δ : Type ?u.92196
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
⊢ Full (quotient r)
Tactic:
intro A B g
State after:
α : Type u_1
β : Type ?u.92190
γ : Type ?u.92193
δ : Type ?u.92196
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
g : Functor.obj (quotient r) A ⟶ Functor.obj (quotient r) B
⊢ ∃ f, Functor.map (quotient r) f = g

State before:
α : Type u_1
β : Type ?u.92190
γ : Type ?u.92193
δ : Type ?u.92196
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
g : Functor.obj (quotient r) A ⟶ Functor.obj (quotient r) B
⊢ ∃ f, Functor.map (quotient r) f = g
Tactic:
refine Quotient.inductionOn g ?_
State after:
α : Type u_1
β : Type ?u.92190
γ : Type ?u.92193
δ : Type ?u.92196
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
g : Functor.obj (quotient r) A ⟶ Functor.obj (quotient r) B
⊢ ∀ (a : (Functor.obj (quotient r) A).unquot ⟶ (Functor.obj (quotient r) B).unquot),
    ∃ f,
      Functor.map (quotient r) f =
        Quotient.mk (Congruence.setoid r (Functor.obj (quotient r) A).unquot (Functor.obj (quotient r) B).unquot) a

State before:
α : Type u_1
β : Type ?u.92190
γ : Type ?u.92193
δ : Type ?u.92196
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
g : Functor.obj (quotient r) A ⟶ Functor.obj (quotient r) B
⊢ ∀ (a : (Functor.obj (quotient r) A).unquot ⟶ (Functor.obj (quotient r) B).unquot),
    ∃ f,
      Functor.map (quotient r) f =
        Quotient.mk (Congruence.setoid r (Functor.obj (quotient r) A).unquot (Functor.obj (quotient r) B).unquot) a
Tactic:
intro g
State after:
α : Type u_1
β : Type ?u.92190
γ : Type ?u.92193
δ : Type ?u.92196
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
g✝ : Functor.obj (quotient r) A ⟶ Functor.obj (quotient r) B
g : (Functor.obj (quotient r) A).unquot ⟶ (Functor.obj (quotient r) B).unquot
⊢ ∃ f,
    Functor.map (quotient r) f =
      Quotient.mk (Congruence.setoid r (Functor.obj (quotient r) A).unquot (Functor.obj (quotient r) B).unquot) g

State before:
α : Type u_1
β : Type ?u.92190
γ : Type ?u.92193
δ : Type ?u.92196
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
g✝ : Functor.obj (quotient r) A ⟶ Functor.obj (quotient r) B
g : (Functor.obj (quotient r) A).unquot ⟶ (Functor.obj (quotient r) B).unquot
⊢ ∃ f,
    Functor.map (quotient r) f =
      Quotient.mk (Congruence.setoid r (Functor.obj (quotient r) A).unquot (Functor.obj (quotient r) B).unquot) g
Tactic:
exact ⟨g, rfl⟩
State after:
no goals