case h
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
⊢ y ∈ insert (f x) (f '' {x}ᶜ) ↔ y ∈ range f
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
⊢ insert (f x) (f '' {x}ᶜ) = range f
ext y
case h
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
⊢ (y = f x ∨ ∃ x_1, x_1 ∈ {x}ᶜ ∧ f x_1 = y) ↔ ∃ y_1, f y_1 = y
case h
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
⊢ y ∈ insert (f x) (f '' {x}ᶜ) ↔ y ∈ range f
rw [mem_range, mem_insert_iff, mem_image]
case h.mp
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
⊢ (y = f x ∨ ∃ x_1, x_1 ∈ {x}ᶜ ∧ f x_1 = y) → ∃ y_1, f y_1 = y

case h.mpr
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
⊢ (∃ y_1, f y_1 = y) → y = f x ∨ ∃ x_1, x_1 ∈ {x}ᶜ ∧ f x_1 = y
case h
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
⊢ (y = f x ∨ ∃ x_1, x_1 ∈ {x}ᶜ ∧ f x_1 = y) ↔ ∃ y_1, f y_1 = y
constructor
case h.mp.inl
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
h : y = f x
⊢ ∃ y_1, f y_1 = y

case h.mp.inr.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
left✝ : x' ∈ {x}ᶜ
h : f x' = y
⊢ ∃ y_1, f y_1 = y
case h.mp
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
⊢ (y = f x ∨ ∃ x_1, x_1 ∈ {x}ᶜ ∧ f x_1 = y) → ∃ y_1, f y_1 = y
rintro (h | ⟨x', _, h⟩)
no goals
case h.mp.inl
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
h : y = f x
⊢ ∃ y_1, f y_1 = y
exact ⟨x, h.symm⟩
no goals
case h.mp.inr.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
left✝ : x' ∈ {x}ᶜ
h : f x' = y
⊢ ∃ y_1, f y_1 = y
exact ⟨x', h⟩
case h.mpr.intro
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
h : f x' = y
⊢ y = f x ∨ ∃ x_1, x_1 ∈ {x}ᶜ ∧ f x_1 = y
case h.mpr
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
⊢ (∃ y_1, f y_1 = y) → y = f x ∨ ∃ x_1, x_1 ∈ {x}ᶜ ∧ f x_1 = y
rintro ⟨x', h⟩
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
h : f x' = y
hx : x' = x
⊢ y = f x ∨ ∃ x_1, x_1 ∈ {x}ᶜ ∧ f x_1 = y

case neg
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
h : f x' = y
hx : ¬x' = x
⊢ y = f x ∨ ∃ x_1, x_1 ∈ {x}ᶜ ∧ f x_1 = y
case h.mpr.intro
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
h : f x' = y
⊢ y = f x ∨ ∃ x_1, x_1 ∈ {x}ᶜ ∧ f x_1 = y
by_cases hx : x' = x
case pos.h
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
h : f x' = y
hx : x' = x
⊢ y = f x
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
h : f x' = y
hx : x' = x
⊢ y = f x ∨ ∃ x_1, x_1 ∈ {x}ᶜ ∧ f x_1 = y
left
no goals
case pos.h
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
h : f x' = y
hx : x' = x
⊢ y = f x
rw [← h, hx]
case neg.h
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
h : f x' = y
hx : ¬x' = x
⊢ ∃ x_1, x_1 ∈ {x}ᶜ ∧ f x_1 = y
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
h : f x' = y
hx : ¬x' = x
⊢ y = f x ∨ ∃ x_1, x_1 ∈ {x}ᶜ ∧ f x_1 = y
right
case neg.h
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
h : f x' = y
hx : ¬x' = x
⊢ x' ∈ {x}ᶜ
case neg.h
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
h : f x' = y
hx : ¬x' = x
⊢ ∃ x_1, x_1 ∈ {x}ᶜ ∧ f x_1 = y
refine' ⟨_, _, h⟩
case neg.h
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
h : f x' = y
hx : ¬x' = x
⊢ x' ≠ x
case neg.h
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
h : f x' = y
hx : ¬x' = x
⊢ x' ∈ {x}ᶜ
rw [mem_compl_singleton_iff]
no goals
case neg.h
α : Type u_2
β : Type u_1
γ : Type ?u.73337
ι : Sort ?u.73340
ι' : Sort ?u.73343
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
h : f x' = y
hx : ¬x' = x
⊢ x' ≠ x
exact hx