no goals
α : Type u
β : Type v
f fa g : α → α
x y : α
fb : β → β
m n k : ℕ
e : Perm α
h : Commute f g
⊢ Set.BijOn g (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))
simpa only [h.comp_eq] using bijOn_fixedPoints_comp f g