A : Sort u_1
B : Sort u_2
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ ∃ g, Function.LeftInverse g f ∧ Function.RightInverse g f
A : Sort u_1
B : Sort u_2
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ Function.Bijective f
rw [Function.bijective_iff_has_inverse]
no goals
A : Sort u_1
B : Sort u_2
inst✝¹ : Unique A
inst✝ : Unique B
f : A → B
⊢ ∃ g, Function.LeftInverse g f ∧ Function.RightInverse g f
refine' ⟨default, _, _⟩ <;> intro x <;> simp