case a
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Sort u_1
β : Type u_2
f : α → β
hf : Injective f
a : α
⊢ ↑(ofInjective f hf) (↑(ofInjective f hf).symm { val := f a, property := (_ : ∃ y, f y = f a) }) =
    ↑(ofInjective f hf) a
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Sort u_1
β : Type u_2
f : α → β
hf : Injective f
a : α
⊢ ↑(ofInjective f hf).symm { val := f a, property := (_ : ∃ y, f y = f a) } = a
apply (ofInjective f hf).injective
no goals
case a
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Sort u_1
β : Type u_2
f : α → β
hf : Injective f
a : α
⊢ ↑(ofInjective f hf) (↑(ofInjective f hf).symm { val := f a, property := (_ : ∃ y, f y = f a) }) =
    ↑(ofInjective f hf) a
simp [apply_ofInjective_symm hf]