case intro
α : Type u
β : Type v
f : Perm α
s : Set α
inst✝ : Finite ↑s
h : Set.MapsTo (↑f) s s
val✝ : Fintype ↑s
⊢ Set.MapsTo (↑f⁻¹) s s
α : Type u
β : Type v
f : Perm α
s : Set α
inst✝ : Finite ↑s
h : Set.MapsTo (↑f) s s
⊢ Set.MapsTo (↑f⁻¹) s s
cases nonempty_fintype s
no goals
case intro
α : Type u
β : Type v
f : Perm α
s : Set α
inst✝ : Finite ↑s
h : Set.MapsTo (↑f) s s
val✝ : Fintype ↑s
⊢ Set.MapsTo (↑f⁻¹) s s
exact fun x hx =>
  Set.mem_toFinset.mp <|
    perm_inv_on_of_perm_on_finset
      (fun a ha => Set.mem_toFinset.mpr (h (Set.mem_toFinset.mp ha)))
      (Set.mem_toFinset.mpr hx)