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

State before:
α : Type u_1
β : Type ?u.72067
γ : Type ?u.72070
δ : Type ?u.72073
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
f g : A ⟶ B
⊢ quotHom r f = quotHom r g ↔ Congruence.rel r A B f g
Tactic:
constructor
State after:
case mp
α : Type u_1
β : Type ?u.72067
γ : Type ?u.72070
δ : Type ?u.72073
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
f g : A ⟶ B
⊢ quotHom r f = quotHom r g → Congruence.rel r A B f g

case mpr
α : Type u_1
β : Type ?u.72067
γ : Type ?u.72070
δ : Type ?u.72073
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
f g : A ⟶ B
⊢ Congruence.rel r A B f g → quotHom r f = quotHom r g

State before:
case mp
α : Type u_1
β : Type ?u.72067
γ : Type ?u.72070
δ : Type ?u.72073
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
f g : A ⟶ B
⊢ quotHom r f = quotHom r g → Congruence.rel r A B f g
Tactic:
intro h
State after:
case mp
α : Type u_1
β : Type ?u.72067
γ : Type ?u.72070
δ : Type ?u.72073
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
f g : A ⟶ B
h : quotHom r f = quotHom r g
⊢ Congruence.rel r A B f g

State before:
case mp
α : Type u_1
β : Type ?u.72067
γ : Type ?u.72070
δ : Type ?u.72073
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
f g : A ⟶ B
h : quotHom r f = quotHom r g
⊢ Congruence.rel r A B f g
Tactic:
exact Quotient.exact h
State after:
no goals

State before:
case mpr
α : Type u_1
β : Type ?u.72067
γ : Type ?u.72070
δ : Type ?u.72073
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
f g : A ⟶ B
⊢ Congruence.rel r A B f g → quotHom r f = quotHom r g
Tactic:
intro h
State after:
case mpr
α : Type u_1
β : Type ?u.72067
γ : Type ?u.72070
δ : Type ?u.72073
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
f g : A ⟶ B
h : Congruence.rel r A B f g
⊢ quotHom r f = quotHom r g

State before:
case mpr
α : Type u_1
β : Type ?u.72067
γ : Type ?u.72070
δ : Type ?u.72073
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
f g : A ⟶ B
h : Congruence.rel r A B f g
⊢ quotHom r f = quotHom r g
Tactic:
exact Quotient.sound h
State after:
no goals