α : Type u_2
β : Type u_1
γ : Type ?u.121829
f : α → β
s✝ t : Set α
s : Set β
h : ∀ (x : α), ¬f x ∈ s
⊢ ∀ (x : β), x ∈ s → ∀ (x_1 : α), ¬f x_1 = x
α : Type u_2
β : Type u_1
γ : Type ?u.121829
f : α → β
s✝ t : Set α
s : Set β
h : f ⁻¹' s = ∅
⊢ Disjoint s (range f)
simp only [eq_empty_iff_forall_not_mem, disjoint_iff_inter_eq_empty, not_exists, mem_inter_iff,
  not_and, mem_range, mem_preimage] at h ⊢
α : Type u_2
β : Type u_1
γ : Type ?u.121829
f : α → β
s✝ t : Set α
s : Set β
h : ∀ (x : α), ¬f x ∈ s
y : β
hy : y ∈ s
x : α
hx : f x = y
⊢ False
α : Type u_2
β : Type u_1
γ : Type ?u.121829
f : α → β
s✝ t : Set α
s : Set β
h : ∀ (x : α), ¬f x ∈ s
⊢ ∀ (x : β), x ∈ s → ∀ (x_1 : α), ¬f x_1 = x
intro y hy x hx
α : Type u_2
β : Type u_1
γ : Type ?u.121829
f : α → β
s✝ t : Set α
s : Set β
h : ∀ (x : α), ¬f x ∈ s
y : β
x : α
hy : f x ∈ s
hx : f x = y
⊢ False
α : Type u_2
β : Type u_1
γ : Type ?u.121829
f : α → β
s✝ t : Set α
s : Set β
h : ∀ (x : α), ¬f x ∈ s
y : β
hy : y ∈ s
x : α
hx : f x = y
⊢ False
rw [← hx] at hy
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.121829
f : α → β
s✝ t : Set α
s : Set β
h : ∀ (x : α), ¬f x ∈ s
y : β
x : α
hy : f x ∈ s
hx : f x = y
⊢ False
exact h x hy