case H.a
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
f_inv : β → α
hf : LeftInverse f_inv f
x✝ : α
⊢ ↑(↑(ofLeftInverse' f f_inv hf) x✝) = ↑(↑(ofInjective f (_ : Injective f)) x✝)
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
f_inv : β → α
hf : LeftInverse f_inv f
⊢ ofLeftInverse' f f_inv hf = ofInjective f (_ : Injective f)
ext
no goals
case H.a
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
f_inv : β → α
hf : LeftInverse f_inv f
x✝ : α
⊢ ↑(↑(ofLeftInverse' f f_inv hf) x✝) = ↑(↑(ofInjective f (_ : Injective f)) x✝)
simp