no goals
α : Type u_4
β : Type u_3
γ : Type u_1
δ : Type u_2
ε : Type ?u.59338
ι : Type ?u.59341
f✝ : α →. β
f : γ →. δ
g : β →. γ
h : α →. β
x✝¹ : α
x✝ : δ
⊢ x✝ ∈ comp (comp f g) h x✝¹ ↔ x✝ ∈ comp f (comp g h) x✝¹
simp only [comp_apply, Part.bind_comp]