no goals
ι : Type ?u.269970
ι' : Type ?u.269973
α : Type ?u.269976
β : Type u_1
γ : Type u_2
inst✝ : DecidableEq β
i : β → γ
j : γ → β
h : Function.LeftInverse j i
a : β
⊢ a ∈ Finset.image j {i a}
simp only [Finset.image_singleton, h a, Finset.mem_singleton]