case h.mk.intro
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
x : α
⊢ ↑(ofInjective f hf).symm { val := f x, property := (_ : ∃ y, f y = f x) } =
    rangeSplitting f { val := f x, property := (_ : ∃ y, f y = f x) }
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ ↑(ofInjective f hf).symm = rangeSplitting f
ext ⟨y, x, rfl⟩
case h.mk.intro.a
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
x : α
⊢ f (↑(ofInjective f hf).symm { val := f x, property := (_ : ∃ y, f y = f x) }) =
    f (rangeSplitting f { val := f x, property := (_ : ∃ y, f y = f x) })
case h.mk.intro
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
x : α
⊢ ↑(ofInjective f hf).symm { val := f x, property := (_ : ∃ y, f y = f x) } =
    rangeSplitting f { val := f x, property := (_ : ∃ y, f y = f x) }
apply hf
no goals
case h.mk.intro.a
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
x : α
⊢ f (↑(ofInjective f hf).symm { val := f x, property := (_ : ∃ y, f y = f x) }) =
    f (rangeSplitting f { val := f x, property := (_ : ∃ y, f y = f x) })
simp [apply_rangeSplitting f]