no goals
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.59817
ε : Type ?u.59820
ι : Type ?u.59823
f✝ : α →. β
g : β → γ
f : α → β
x✝¹ : α
x✝ : γ
⊢ x✝ ∈ ↑(g ∘ f) x✝¹ ↔ x✝ ∈ comp (↑g) (↑f) x✝¹
simp only [coe_val, comp_apply, Function.comp, Part.bind_some]