case h
α : Type u_1
β : Type u_2
γ : Type ?u.68574
ι : Sort ?u.68577
π : α → Type ?u.68582
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 ∪ range fᶜ
α : Type u_1
β : Type u_2
γ : Type ?u.68574
ι : Sort ?u.68577
π : α → Type ?u.68582
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 ∪ range fᶜ
ext x
case h.inl.intro
α : Type u_1
β : Type u_2
γ : Type ?u.68574
ι : Sort ?u.68577
π : α → Type ?u.68582
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 ∪ range fᶜ

case h.inr
α : Type u_1
β : Type u_2
γ : Type ?u.68574
ι : Sort ?u.68577
π : α → Type ?u.68582
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 ∪ range fᶜ
case h
α : Type u_1
β : Type u_2
γ : Type ?u.68574
ι : Sort ?u.68577
π : α → Type ?u.68582
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 ∪ range fᶜ
rcases em (x ∈ range f) with (⟨a, rfl⟩ | hx)
no goals
case h.inl.intro
α : Type u_1
β : Type u_2
γ : Type ?u.68574
ι : Sort ?u.68577
π : α → Type ?u.68582
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 ∪ range fᶜ
simp only [mem_preimage, mem_union, mem_compl_iff, mem_range_self, not_true, or_false,
  leftInverse_invFun hf _, hf.mem_set_image]
no goals
case h.inr
α : Type u_1
β : Type u_2
γ : Type ?u.68574
ι : Sort ?u.68577
π : α → Type ?u.68582
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 ∪ range fᶜ
simp only [mem_preimage, invFun_neg hx, h, hx, mem_union, mem_compl_iff, not_false_iff, or_true]