case h
α : Type u_1
β : Type u_2
γ : Type ?u.70004
ι : Sort ?u.70007
π : α → Type ?u.70012
s✝ s₁ s₂ : Set α
t : Set β
f✝ : α → β
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
x : β
⊢ x ∈ Function.invFun f ⁻¹' s ↔ x ∈ f '' s
α : Type u_1
β : Type u_2
γ : Type ?u.70004
ι : Sort ?u.70007
π : α → Type ?u.70012
s✝ s₁ s₂ : Set α
t : Set β
f✝ : α → β
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
⊢ Function.invFun f ⁻¹' s = f '' s
ext x
case h.inl.intro
α : Type u_1
β : Type u_2
γ : Type ?u.70004
ι : Sort ?u.70007
π : α → Type ?u.70012
s✝ s₁ s₂ : Set α
t : Set β
f✝ : α → β
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
a : α
⊢ f a ∈ Function.invFun f ⁻¹' s ↔ f a ∈ f '' s

case h.inr
α : Type u_1
β : Type u_2
γ : Type ?u.70004
ι : Sort ?u.70007
π : α → Type ?u.70012
s✝ s₁ s₂ : Set α
t : Set β
f✝ : α → β
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
x : β
hx : ¬x ∈ range f
⊢ x ∈ Function.invFun f ⁻¹' s ↔ x ∈ f '' s
case h
α : Type u_1
β : Type u_2
γ : Type ?u.70004
ι : Sort ?u.70007
π : α → Type ?u.70012
s✝ s₁ s₂ : Set α
t : Set β
f✝ : α → β
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
x : β
⊢ x ∈ Function.invFun f ⁻¹' s ↔ x ∈ f '' s
rcases em (x ∈ range f) with (⟨a, rfl⟩ | hx)
no goals
case h.inl.intro
α : Type u_1
β : Type u_2
γ : Type ?u.70004
ι : Sort ?u.70007
π : α → Type ?u.70012
s✝ s₁ s₂ : Set α
t : Set β
f✝ : α → β
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
a : α
⊢ f a ∈ Function.invFun f ⁻¹' s ↔ f a ∈ f '' s
rw [mem_preimage, leftInverse_invFun hf, hf.mem_set_image]
case h.inr
α : Type u_1
β : Type u_2
γ : Type ?u.70004
ι : Sort ?u.70007
π : α → Type ?u.70012
s✝ s₁ s₂ : Set α
t : Set β
f✝ : α → β
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
x : β
hx : ¬x ∈ range f
this : ¬x ∈ f '' s
⊢ x ∈ Function.invFun f ⁻¹' s ↔ x ∈ f '' s
case h.inr
α : Type u_1
β : Type u_2
γ : Type ?u.70004
ι : Sort ?u.70007
π : α → Type ?u.70012
s✝ s₁ s₂ : Set α
t : Set β
f✝ : α → β
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
x : β
hx : ¬x ∈ range f
⊢ x ∈ Function.invFun f ⁻¹' s ↔ x ∈ f '' s
have : x ∉ f '' s := fun h' => hx (image_subset_range _ _ h')
no goals
case h.inr
α : Type u_1
β : Type u_2
γ : Type ?u.70004
ι : Sort ?u.70007
π : α → Type ?u.70012
s✝ s₁ s₂ : Set α
t : Set β
f✝ : α → β
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
x : β
hx : ¬x ∈ range f
this : ¬x ∈ f '' s
⊢ x ∈ Function.invFun f ⁻¹' s ↔ x ∈ f '' s
simp only [mem_preimage, invFun_neg hx, h, this]