sorry_proof
X✝ : Type ?u.1497
inst✝⁸ : Nonempty X✝
Y✝ : Type ?u.1503
inst✝⁷ : Nonempty Y✝
Z✝ : Type ?u.1509
inst✝⁶ : Nonempty Z✝
X₁ : Type ?u.1515
inst✝⁵ : Nonempty X₁
X₂ : Type ?u.1521
inst✝⁴ : Nonempty X₂
X : Type u_2
inst✝³ : Nonempty X
Y : Type u_1
inst✝² : Nonempty Y
Z : Type ?u.1539
inst✝¹ : Nonempty Z
inst✝ : Group Y
f : X → Y
hf : Bijective f
⊢ (invFun fun x => (f x)⁻¹) = fun y => invFun f y⁻¹
no goals