no goals
m : Type u_1 → Type u_2
α : Type u_1
p : α → Prop
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
x : m α
h : ∀ (a : α), p a
⊢ Subtype.val <$> (fun a => { val := a, property := (_ : p a) }) <$> x = x
simp [← comp_map, Function.comp]