α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
hf_meas : ∀ (x : β), MeasurableSet (↑f ⁻¹' {x})
⊢ ∃ c, ∀ (x : α), ↑f x = c
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
⊢ ∃ c, ∀ (x : α), ↑f x = c
have hf_meas := @SimpleFunc.measurableSet_fiber α _ ⊥ f
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
hf_meas : ∀ (x : β), ↑f ⁻¹' {x} = ∅ ∨ ↑f ⁻¹' {x} = univ
⊢ ∃ c, ∀ (x : α), ↑f x = c
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
hf_meas : ∀ (x : β), MeasurableSet (↑f ⁻¹' {x})
⊢ ∃ c, ∀ (x : α), ↑f x = c
simp_rw [MeasurableSpace.measurableSet_bot_iff] at hf_meas
case inl
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
hf_meas : ∀ (x : β), ↑f ⁻¹' {x} = ∅ ∨ ↑f ⁻¹' {x} = univ
h : IsEmpty α
⊢ ∃ c, ∀ (x : α), ↑f x = c

case inr
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
hf_meas : ∀ (x : β), ↑f ⁻¹' {x} = ∅ ∨ ↑f ⁻¹' {x} = univ
h : Nonempty α
⊢ ∃ c, ∀ (x : α), ↑f x = c
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
hf_meas : ∀ (x : β), ↑f ⁻¹' {x} = ∅ ∨ ↑f ⁻¹' {x} = univ
⊢ ∃ c, ∀ (x : α), ↑f x = c
cases' isEmpty_or_nonempty α with h h
no goals
case inl
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
hf_meas : ∀ (x : β), ↑f ⁻¹' {x} = ∅ ∨ ↑f ⁻¹' {x} = univ
h : IsEmpty α
⊢ ∃ c, ∀ (x : α), ↑f x = c
simp only [IsEmpty.forall_iff, exists_const]
case inr
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = ∅ ∨ ↑f ⁻¹' {↑f (Nonempty.some h)} = univ
⊢ ∃ c, ∀ (x : α), ↑f x = c
case inr
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
hf_meas : ∀ (x : β), ↑f ⁻¹' {x} = ∅ ∨ ↑f ⁻¹' {x} = univ
h : Nonempty α
⊢ ∃ c, ∀ (x : α), ↑f x = c
specialize hf_meas (f h.some)
case inr.inl
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = ∅
⊢ ∃ c, ∀ (x : α), ↑f x = c

case inr.inr
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = univ
⊢ ∃ c, ∀ (x : α), ↑f x = c
case inr
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = ∅ ∨ ↑f ⁻¹' {↑f (Nonempty.some h)} = univ
⊢ ∃ c, ∀ (x : α), ↑f x = c
cases' hf_meas with hf_meas hf_meas
case inr.inl.h
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = ∅
⊢ False
case inr.inl
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = ∅
⊢ ∃ c, ∀ (x : α), ↑f x = c
exfalso
case inr.inl.h
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = ∅
⊢ Nonempty.some h ∈ ∅
case inr.inl.h
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = ∅
⊢ False
refine' Set.not_mem_empty h.some _
case inr.inl.h
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = ∅
⊢ ↑f (Nonempty.some h) ∈ {↑f (Nonempty.some h)}
case inr.inl.h
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = ∅
⊢ Nonempty.some h ∈ ∅
rw [← hf_meas, Set.mem_preimage]
no goals
case inr.inl.h
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = ∅
⊢ ↑f (Nonempty.some h) ∈ {↑f (Nonempty.some h)}
exact Set.mem_singleton _
case inr.inr
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = univ
x : α
⊢ ↑f x = ↑f (Nonempty.some h)
case inr.inr
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = univ
⊢ ∃ c, ∀ (x : α), ↑f x = c
refine' ⟨f h.some, fun x => _⟩
case inr.inr
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = univ
x : α
this : x ∈ ↑f ⁻¹' {↑f (Nonempty.some h)}
⊢ ↑f x = ↑f (Nonempty.some h)
case inr.inr
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = univ
x : α
⊢ ↑f x = ↑f (Nonempty.some h)
have : x ∈ f ⁻¹' {f h.some} := by
  rw [hf_meas]
  exact Set.mem_univ x
no goals
case inr.inr
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = univ
x : α
this : x ∈ ↑f ⁻¹' {↑f (Nonempty.some h)}
⊢ ↑f x = ↑f (Nonempty.some h)
rwa [Set.mem_preimage, Set.mem_singleton_iff] at this
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = univ
x : α
⊢ x ∈ univ
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = univ
x : α
⊢ x ∈ ↑f ⁻¹' {↑f (Nonempty.some h)}
rw [hf_meas]
no goals
α✝ : Type ?u.20769
β : Type u_2
γ : Type ?u.20775
δ : Type ?u.20778
inst✝¹ : MeasurableSpace α✝
α : Type u_1
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = univ
x : α
⊢ x ∈ univ
exact Set.mem_univ x