α : Type u_2
β✝ : Type ?u.125758
γ : Type ?u.125761
δ : Type ?u.125764
inst✝ : MeasurableSpace α
β : Type u_1
hα : IsEmpty α
f : α →ₛ β
⊢ ¬Finset.Nonempty (SimpleFunc.range f)
α : Type u_2
β✝ : Type ?u.125758
γ : Type ?u.125761
δ : Type ?u.125764
inst✝ : MeasurableSpace α
β : Type u_1
hα : IsEmpty α
f : α →ₛ β
⊢ SimpleFunc.range f = ∅
rw [← Finset.not_nonempty_iff_eq_empty]
α : Type u_2
β✝ : Type ?u.125758
γ : Type ?u.125761
δ : Type ?u.125764
inst✝ : MeasurableSpace α
β : Type u_1
hα : IsEmpty α
f : α →ₛ β
h : Finset.Nonempty (SimpleFunc.range f)
⊢ False
α : Type u_2
β✝ : Type ?u.125758
γ : Type ?u.125761
δ : Type ?u.125764
inst✝ : MeasurableSpace α
β : Type u_1
hα : IsEmpty α
f : α →ₛ β
⊢ ¬Finset.Nonempty (SimpleFunc.range f)
by_contra h
case intro
α : Type u_2
β✝ : Type ?u.125758
γ : Type ?u.125761
δ : Type ?u.125764
inst✝ : MeasurableSpace α
β : Type u_1
hα : IsEmpty α
f : α →ₛ β
y : β
hy_mem : y ∈ SimpleFunc.range f
⊢ False
α : Type u_2
β✝ : Type ?u.125758
γ : Type ?u.125761
δ : Type ?u.125764
inst✝ : MeasurableSpace α
β : Type u_1
hα : IsEmpty α
f : α →ₛ β
h : Finset.Nonempty (SimpleFunc.range f)
⊢ False
obtain ⟨y, hy_mem⟩ := h
case intro
α : Type u_2
β✝ : Type ?u.125758
γ : Type ?u.125761
δ : Type ?u.125764
inst✝ : MeasurableSpace α
β : Type u_1
hα : IsEmpty α
f : α →ₛ β
y : β
hy_mem : ∃ y_1, ↑f y_1 = y
⊢ False
case intro
α : Type u_2
β✝ : Type ?u.125758
γ : Type ?u.125761
δ : Type ?u.125764
inst✝ : MeasurableSpace α
β : Type u_1
hα : IsEmpty α
f : α →ₛ β
y : β
hy_mem : y ∈ SimpleFunc.range f
⊢ False
rw [SimpleFunc.mem_range, Set.mem_range] at hy_mem
case intro.intro
α : Type u_2
β✝ : Type ?u.125758
γ : Type ?u.125761
δ : Type ?u.125764
inst✝ : MeasurableSpace α
β : Type u_1
hα : IsEmpty α
f : α →ₛ β
y : β
x : α
hxy : ↑f x = y
⊢ False
case intro
α : Type u_2
β✝ : Type ?u.125758
γ : Type ?u.125761
δ : Type ?u.125764
inst✝ : MeasurableSpace α
β : Type u_1
hα : IsEmpty α
f : α →ₛ β
y : β
hy_mem : ∃ y_1, ↑f y_1 = y
⊢ False
obtain ⟨x, hxy⟩ := hy_mem
case intro.intro
α : Type u_2
β✝ : Type ?u.125758
γ : Type ?u.125761
δ : Type ?u.125764
inst✝ : MeasurableSpace α
β : Type u_1
hα : α → False
f : α →ₛ β
y : β
x : α
hxy : ↑f x = y
⊢ False
case intro.intro
α : Type u_2
β✝ : Type ?u.125758
γ : Type ?u.125761
δ : Type ?u.125764
inst✝ : MeasurableSpace α
β : Type u_1
hα : IsEmpty α
f : α →ₛ β
y : β
x : α
hxy : ↑f x = y
⊢ False
rw [isEmpty_iff] at hα
no goals
case intro.intro
α : Type u_2
β✝ : Type ?u.125758
γ : Type ?u.125761
δ : Type ?u.125764
inst✝ : MeasurableSpace α
β : Type u_1
hα : α → False
f : α →ₛ β
y : β
x : α
hxy : ↑f x = y
⊢ False
exact hα x