case h
ι : Sort ?u.105472
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
y : β
⊢ y ∈ (f '' s)ᶜ ↔ y ∈ f '' sᶜ ∪ range fᶜ
ι : Sort ?u.105472
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
⊢ (f '' s)ᶜ = f '' sᶜ ∪ range fᶜ
ext y
case h.inl.intro
ι : Sort ?u.105472
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
x : α
⊢ f x ∈ (f '' s)ᶜ ↔ f x ∈ f '' sᶜ ∪ range fᶜ

case h.inr
ι : Sort ?u.105472
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
y : β
hx : ¬y ∈ range f
⊢ y ∈ (f '' s)ᶜ ↔ y ∈ f '' sᶜ ∪ range fᶜ
case h
ι : Sort ?u.105472
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
y : β
⊢ y ∈ (f '' s)ᶜ ↔ y ∈ f '' sᶜ ∪ range fᶜ
rcases em (y ∈ range f) with (⟨x, rfl⟩ | hx)
no goals
case h.inl.intro
ι : Sort ?u.105472
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
x : α
⊢ f x ∈ (f '' s)ᶜ ↔ f x ∈ f '' sᶜ ∪ range fᶜ
simp [hf.eq_iff]
case h.inr
ι : Sort ?u.105472
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
y : β
hx : ∀ (x : α), ¬f x = y
⊢ y ∈ (f '' s)ᶜ ↔ y ∈ f '' sᶜ ∪ range fᶜ
case h.inr
ι : Sort ?u.105472
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
y : β
hx : ¬y ∈ range f
⊢ y ∈ (f '' s)ᶜ ↔ y ∈ f '' sᶜ ∪ range fᶜ
rw [mem_range, not_exists] at hx
no goals
case h.inr
ι : Sort ?u.105472
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
y : β
hx : ∀ (x : α), ¬f x = y
⊢ y ∈ (f '' s)ᶜ ↔ y ∈ f '' sᶜ ∪ range fᶜ
simp [hx]