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