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

State before:
α : Type u_1
β : Type ?u.68744
γ : Type ?u.68747
δ : Type ?u.68750
A✝ B✝ C✝ D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B C : HomQuotient r
f₁ : B.unquot ⟶ C.unquot
g₁ : A.unquot ⟶ B.unquot
f₂ : B.unquot ⟶ C.unquot
g₂ : A.unquot ⟶ B.unquot
hf : Congruence.rel r B.unquot C.unquot f₁ f₂
hg : Congruence.rel r A.unquot B.unquot g₁ g₂
⊢ Quotient.mk (Congruence.setoid r A.unquot C.unquot) (f₁ ∘ g₁) =
    Quotient.mk (Congruence.setoid r A.unquot C.unquot) (f₂ ∘ g₂)
Tactic:
have h₁ := r.whisker_rel f₁ g₁ g₂ hg
State after:
α : Type u_1
β : Type ?u.68744
γ : Type ?u.68747
δ : Type ?u.68750
A✝ B✝ C✝ D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B C : HomQuotient r
f₁ : B.unquot ⟶ C.unquot
g₁ : A.unquot ⟶ B.unquot
f₂ : B.unquot ⟶ C.unquot
g₂ : A.unquot ⟶ B.unquot
hf : Congruence.rel r B.unquot C.unquot f₁ f₂
hg : Congruence.rel r A.unquot B.unquot g₁ g₂
h₁ : Congruence.rel r A.unquot C.unquot (f₁ ∘ g₁) (f₁ ∘ g₂)
⊢ Quotient.mk (Congruence.setoid r A.unquot C.unquot) (f₁ ∘ g₁) =
    Quotient.mk (Congruence.setoid r A.unquot C.unquot) (f₂ ∘ g₂)

State before:
α : Type u_1
β : Type ?u.68744
γ : Type ?u.68747
δ : Type ?u.68750
A✝ B✝ C✝ D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B C : HomQuotient r
f₁ : B.unquot ⟶ C.unquot
g₁ : A.unquot ⟶ B.unquot
f₂ : B.unquot ⟶ C.unquot
g₂ : A.unquot ⟶ B.unquot
hf : Congruence.rel r B.unquot C.unquot f₁ f₂
hg : Congruence.rel r A.unquot B.unquot g₁ g₂
h₁ : Congruence.rel r A.unquot C.unquot (f₁ ∘ g₁) (f₁ ∘ g₂)
⊢ Quotient.mk (Congruence.setoid r A.unquot C.unquot) (f₁ ∘ g₁) =
    Quotient.mk (Congruence.setoid r A.unquot C.unquot) (f₂ ∘ g₂)
Tactic:
have h₂ := r.rel_whisker f₁ f₂ g₂ hf
State after:
α : Type u_1
β : Type ?u.68744
γ : Type ?u.68747
δ : Type ?u.68750
A✝ B✝ C✝ D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B C : HomQuotient r
f₁ : B.unquot ⟶ C.unquot
g₁ : A.unquot ⟶ B.unquot
f₂ : B.unquot ⟶ C.unquot
g₂ : A.unquot ⟶ B.unquot
hf : Congruence.rel r B.unquot C.unquot f₁ f₂
hg : Congruence.rel r A.unquot B.unquot g₁ g₂
h₁ : Congruence.rel r A.unquot C.unquot (f₁ ∘ g₁) (f₁ ∘ g₂)
h₂ : Congruence.rel r A.unquot C.unquot (f₁ ∘ g₂) (f₂ ∘ g₂)
⊢ Quotient.mk (Congruence.setoid r A.unquot C.unquot) (f₁ ∘ g₁) =
    Quotient.mk (Congruence.setoid r A.unquot C.unquot) (f₂ ∘ g₂)

State before:
α : Type u_1
β : Type ?u.68744
γ : Type ?u.68747
δ : Type ?u.68750
A✝ B✝ C✝ D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B C : HomQuotient r
f₁ : B.unquot ⟶ C.unquot
g₁ : A.unquot ⟶ B.unquot
f₂ : B.unquot ⟶ C.unquot
g₂ : A.unquot ⟶ B.unquot
hf : Congruence.rel r B.unquot C.unquot f₁ f₂
hg : Congruence.rel r A.unquot B.unquot g₁ g₂
h₁ : Congruence.rel r A.unquot C.unquot (f₁ ∘ g₁) (f₁ ∘ g₂)
h₂ : Congruence.rel r A.unquot C.unquot (f₁ ∘ g₂) (f₂ ∘ g₂)
⊢ Quotient.mk (Congruence.setoid r A.unquot C.unquot) (f₁ ∘ g₁) =
    Quotient.mk (Congruence.setoid r A.unquot C.unquot) (f₂ ∘ g₂)
Tactic:
exact Quotient.sound ((r.equivalence _ _).trans h₁ h₂)
State after:
no goals