m : Type u_1 → Type u_2
α : Type u_1
p : α → Prop
α✝ : Type u_1
q : α✝ → Prop
f : α → α✝
inst✝¹ : Functor m
inst✝ : LawfulFunctor m
x : m α
hx✝ : SatisfiesM p x
hf : ∀ {a : α}, p a → q (f a)
x' : m { a // p a }
hx : Subtype.val <$> x' = x
⊢ SatisfiesM q (f <$> x)
m : Type u_1 → Type u_2
α : Type u_1
p : α → Prop
α✝ : Type u_1
q : α✝ → Prop
f : α → α✝
inst✝¹ : Functor m
inst✝ : LawfulFunctor m
x : m α
hx : SatisfiesM p x
hf : ∀ {a : α}, p a → q (f a)
⊢ SatisfiesM q (f <$> x)
let ⟨x', hx⟩ := hx
m : Type u_1 → Type u_2
α : Type u_1
p : α → Prop
α✝ : Type u_1
q : α✝ → Prop
f : α → α✝
inst✝¹ : Functor m
inst✝ : LawfulFunctor m
x : m α
hx✝ : SatisfiesM p x
hf : ∀ {a : α}, p a → q (f a)
x' : m { a // p a }
hx : Subtype.val <$> x' = x
⊢ Subtype.val <$>
      (fun x =>
          match x with
          | { val := a, property := h } => { val := f a, property := (_ : q (f a)) }) <$>
        x' =
    f <$> x
m : Type u_1 → Type u_2
α : Type u_1
p : α → Prop
α✝ : Type u_1
q : α✝ → Prop
f : α → α✝
inst✝¹ : Functor m
inst✝ : LawfulFunctor m
x : m α
hx✝ : SatisfiesM p x
hf : ∀ {a : α}, p a → q (f a)
x' : m { a // p a }
hx : Subtype.val <$> x' = x
⊢ SatisfiesM q (f <$> x)
refine ⟨(fun ⟨a, h⟩ => ⟨f a, hf h⟩) <$> x', ?_⟩
m : Type u_1 → Type u_2
α : Type u_1
p : α → Prop
α✝ : Type u_1
q : α✝ → Prop
f : α → α✝
inst✝¹ : Functor m
inst✝ : LawfulFunctor m
x : m α
hx✝ : SatisfiesM p x
hf : ∀ {a : α}, p a → q (f a)
x' : m { a // p a }
hx : Subtype.val <$> x' = x
⊢ Subtype.val <$>
      (fun x =>
          match x with
          | { val := a, property := h } => { val := f a, property := (_ : q (f a)) }) <$>
        x' =
    f <$> Subtype.val <$> x'
m : Type u_1 → Type u_2
α : Type u_1
p : α → Prop
α✝ : Type u_1
q : α✝ → Prop
f : α → α✝
inst✝¹ : Functor m
inst✝ : LawfulFunctor m
x : m α
hx✝ : SatisfiesM p x
hf : ∀ {a : α}, p a → q (f a)
x' : m { a // p a }
hx : Subtype.val <$> x' = x
⊢ Subtype.val <$>
      (fun x =>
          match x with
          | { val := a, property := h } => { val := f a, property := (_ : q (f a)) }) <$>
        x' =
    f <$> x
rw [← hx]
no goals
m : Type u_1 → Type u_2
α : Type u_1
p : α → Prop
α✝ : Type u_1
q : α✝ → Prop
f : α → α✝
inst✝¹ : Functor m
inst✝ : LawfulFunctor m
x : m α
hx✝ : SatisfiesM p x
hf : ∀ {a : α}, p a → q (f a)
x' : m { a // p a }
hx : Subtype.val <$> x' = x
⊢ Subtype.val <$>
      (fun x =>
          match x with
          | { val := a, property := h } => { val := f a, property := (_ : q (f a)) }) <$>
        x' =
    f <$> Subtype.val <$> x'
simp [← comp_map, Function.comp]