F : Type ?u.7720
α : Type u_2
β : Type ?u.7726
γ : Type ?u.7729
inst✝ : InvolutiveInv α
s t : Set α
a : α
ι : Sort u_1
f : ι → α
⊢ Inv.inv '' range f = range fun i => (f i)⁻¹
F : Type ?u.7720
α : Type u_2
β : Type ?u.7726
γ : Type ?u.7729
inst✝ : InvolutiveInv α
s t : Set α
a : α
ι : Sort u_1
f : ι → α
⊢ (range f)⁻¹ = range fun i => (f i)⁻¹
rw [← image_inv]
no goals
F : Type ?u.7720
α : Type u_2
β : Type ?u.7726
γ : Type ?u.7729
inst✝ : InvolutiveInv α
s t : Set α
a : α
ι : Sort u_1
f : ι → α
⊢ Inv.inv '' range f = range fun i => (f i)⁻¹
exact (range_comp _ _).symm