case h.mk.intro.intro
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
u s : Set α
a : α
has : a ∈ s
⊢ { val := f a, property := (_ : ∃ a_1, a_1 ∈ s ∧ f a_1 = f a) } ∈ (fun x => ↑(↑(Set.image f s hf).symm x)) ⁻¹' u ↔
    { val := f a, property := (_ : ∃ a_1, a_1 ∈ s ∧ f a_1 = f a) } ∈ Subtype.val ⁻¹' (f '' u)
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
u s : Set α
⊢ (fun x => ↑(↑(Set.image f s hf).symm x)) ⁻¹' u = Subtype.val ⁻¹' (f '' u)
ext ⟨b, a, has, rfl⟩
case h.mk.intro.intro
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
u s : Set α
a : α
has : a ∈ s
this : ∀ (h : ∃ a', a' ∈ s ∧ a' = a), Classical.choose h = a
⊢ { val := f a, property := (_ : ∃ a_1, a_1 ∈ s ∧ f a_1 = f a) } ∈ (fun x => ↑(↑(Set.image f s hf).symm x)) ⁻¹' u ↔
    { val := f a, property := (_ : ∃ a_1, a_1 ∈ s ∧ f a_1 = f a) } ∈ Subtype.val ⁻¹' (f '' u)
case h.mk.intro.intro
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
u s : Set α
a : α
has : a ∈ s
⊢ { val := f a, property := (_ : ∃ a_1, a_1 ∈ s ∧ f a_1 = f a) } ∈ (fun x => ↑(↑(Set.image f s hf).symm x)) ⁻¹' u ↔
    { val := f a, property := (_ : ∃ a_1, a_1 ∈ s ∧ f a_1 = f a) } ∈ Subtype.val ⁻¹' (f '' u)
have : ∀ h : ∃ a', a' ∈ s ∧ a' = a, Classical.choose h = a := fun h => (Classical.choose_spec h).2
no goals
case h.mk.intro.intro
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
u s : Set α
a : α
has : a ∈ s
this : ∀ (h : ∃ a', a' ∈ s ∧ a' = a), Classical.choose h = a
⊢ { val := f a, property := (_ : ∃ a_1, a_1 ∈ s ∧ f a_1 = f a) } ∈ (fun x => ↑(↑(Set.image f s hf).symm x)) ⁻¹' u ↔
    { val := f a, property := (_ : ∃ a_1, a_1 ∈ s ∧ f a_1 = f a) } ∈ Subtype.val ⁻¹' (f '' u)
simp [Equiv.Set.image, Equiv.Set.imageOfInjOn, hf.eq_iff, this]