case h.mk
α : Type u_1
β : Type u_2
γ : Type ?u.62111
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α → β
hf : Injective f
inst✝ : Nonempty α
b : β
h : b ∈ Set.range f
⊢ Set.restrict (Set.range f) (invFun f) { val := b, property := h } = invOfMemRange hf { val := b, property := h }
α : Type u_1
β : Type u_2
γ : Type ?u.62111
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α → β
hf : Injective f
inst✝ : Nonempty α
⊢ Set.restrict (Set.range f) (invFun f) = invOfMemRange hf
ext ⟨b, h⟩
case h.mk.a
α : Type u_1
β : Type u_2
γ : Type ?u.62111
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α → β
hf : Injective f
inst✝ : Nonempty α
b : β
h : b ∈ Set.range f
⊢ f (Set.restrict (Set.range f) (invFun f) { val := b, property := h }) =
    f (invOfMemRange hf { val := b, property := h })
case h.mk
α : Type u_1
β : Type u_2
γ : Type ?u.62111
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α → β
hf : Injective f
inst✝ : Nonempty α
b : β
h : b ∈ Set.range f
⊢ Set.restrict (Set.range f) (invFun f) { val := b, property := h } = invOfMemRange hf { val := b, property := h }
apply hf
no goals
case h.mk.a
α : Type u_1
β : Type u_2
γ : Type ?u.62111
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α → β
hf : Injective f
inst✝ : Nonempty α
b : β
h : b ∈ Set.range f
⊢ f (Set.restrict (Set.range f) (invFun f) { val := b, property := h }) =
    f (invOfMemRange hf { val := b, property := h })
simp [hf.left_inv_of_invOfMemRange, @invFun_eq _ _ _ f b (Set.mem_range.mp h)]