F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α β : Type u
g : α → β
x : F α
⊢ supp (g <$> abs (repr x)) = g '' supp (abs (repr x))
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α β : Type u
g : α → β
x : F α
⊢ supp (g <$> x) = g '' supp x
rw [← abs_repr x]
case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α β : Type u
g : α → β
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
⊢ supp (g <$> abs { fst := a, snd := f }) = g '' supp (abs { fst := a, snd := f })
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α β : Type u
g : α → β
x : F α
⊢ supp (g <$> abs (repr x)) = g '' supp (abs (repr x))
cases' repr x with a f
case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α β : Type u
g : α → β
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
⊢ supp (abs { fst := a, snd := g ∘ f }) = g '' supp (abs { fst := a, snd := f })
case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α β : Type u
g : α → β
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
⊢ supp (g <$> abs { fst := a, snd := f }) = g '' supp (abs { fst := a, snd := f })
rw [← abs_map, PFunctor.map_eq]
no goals
case mk
F : Type u → Type u
inst✝ : Functor F
q : Qpf F
h : IsUniform
α β : Type u
g : α → β
x : F α
a : (P F).A
f : PFunctor.B (P F) a → α
⊢ supp (abs { fst := a, snd := g ∘ f }) = g '' supp (abs { fst := a, snd := f })
rw [supp_eq_of_isUniform h, supp_eq_of_isUniform h, image_comp]