case h.h
α : Type u_1
β : Type u_4
γ : Type u_3
δ : Type u_2
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ ((r ∘r p) ∘r q) a d = (r ∘r p ∘r q) a d
α : Type u_1
β : Type u_4
γ : Type u_3
δ : Type u_2
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
⊢ (r ∘r p) ∘r q = r ∘r p ∘r q
funext a d
case h.h.a
α : Type u_1
β : Type u_4
γ : Type u_3
δ : Type u_2
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ ((r ∘r p) ∘r q) a d ↔ (r ∘r p ∘r q) a d
case h.h
α : Type u_1
β : Type u_4
γ : Type u_3
δ : Type u_2
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ ((r ∘r p) ∘r q) a d = (r ∘r p ∘r q) a d
apply propext
case h.h.a.mp
α : Type u_1
β : Type u_4
γ : Type u_3
δ : Type u_2
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ ((r ∘r p) ∘r q) a d → (r ∘r p ∘r q) a d

case h.h.a.mpr
α : Type u_1
β : Type u_4
γ : Type u_3
δ : Type u_2
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ (r ∘r p ∘r q) a d → ((r ∘r p) ∘r q) a d
case h.h.a
α : Type u_1
β : Type u_4
γ : Type u_3
δ : Type u_2
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ ((r ∘r p) ∘r q) a d ↔ (r ∘r p ∘r q) a d
constructor
case h.h.a.mpr
α : Type u_1
β : Type u_4
γ : Type u_3
δ : Type u_2
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ (r ∘r p ∘r q) a d → ((r ∘r p) ∘r q) a d
case h.h.a.mp
α : Type u_1
β : Type u_4
γ : Type u_3
δ : Type u_2
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ ((r ∘r p) ∘r q) a d → (r ∘r p ∘r q) a d

case h.h.a.mpr
α : Type u_1
β : Type u_4
γ : Type u_3
δ : Type u_2
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ (r ∘r p ∘r q) a d → ((r ∘r p) ∘r q) a d
exact fun ⟨c, ⟨b, hab, hbc⟩, hcd⟩ ↦ ⟨b, hab, c, hbc, hcd⟩
no goals
case h.h.a.mpr
α : Type u_1
β : Type u_4
γ : Type u_3
δ : Type u_2
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ (r ∘r p ∘r q) a d → ((r ∘r p) ∘r q) a d
exact fun ⟨b, hab, c, hbc, hcd⟩ ↦ ⟨c, ⟨b, hab, hbc⟩, hcd⟩