m : Type u_1 → Type u_2
α : Type u_1
p q : α → Prop
inst✝¹ : Functor m
inst✝ : LawfulFunctor m
x✝ : m α
h✝ : SatisfiesM p x✝
H : ∀ {a : α}, p a → q a
x : m { a // p a }
h : Subtype.val <$> x = x✝
⊢ (Subtype.val ∘ fun x =>
        match x with
        | { val := a, property := h } => { val := a, property := (_ : q a) }) <$>
      x =
    Subtype.val <$> x
m : Type u_1 → Type u_2
α : Type u_1
p q : α → Prop
inst✝¹ : Functor m
inst✝ : LawfulFunctor m
x✝ : m α
h✝ : SatisfiesM p x✝
H : ∀ {a : α}, p a → q a
x : m { a // p a }
h : Subtype.val <$> x = x✝
⊢ Subtype.val <$>
      (fun x =>
          match x with
          | { val := a, property := h } => { val := a, property := (_ : q a) }) <$>
        x =
    x✝
rw [← h, ← comp_map]
no goals
m : Type u_1 → Type u_2
α : Type u_1
p q : α → Prop
inst✝¹ : Functor m
inst✝ : LawfulFunctor m
x✝ : m α
h✝ : SatisfiesM p x✝
H : ∀ {a : α}, p a → q a
x : m { a // p a }
h : Subtype.val <$> x = x✝
⊢ (Subtype.val ∘ fun x =>
        match x with
        | { val := a, property := h } => { val := a, property := (_ : q a) }) <$>
      x =
    Subtype.val <$> x
rfl