case refine_2
α✝ : Type ?u.13198
β✝ : Type ?u.13201
γ : Type ?u.13204
ι : Type ?u.13207
inst✝³ : Countable ι
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
f_sf : α →ₛ β :=
  { toFun := f, measurableSet_fiber' := (_ : ∀ (x : β), MeasurableSet (f ⁻¹' {x})),
    finite_range' := (_ : Set.Finite (range f)) }
⊢ StronglyMeasurable f

case refine_1
α✝ : Type ?u.13198
β✝ : Type ?u.13201
γ : Type ?u.13204
ι : Type ?u.13207
inst✝³ : Countable ι
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
x : β
⊢ MeasurableSet (f ⁻¹' {x})
α✝ : Type ?u.13198
β✝ : Type ?u.13201
γ : Type ?u.13204
ι : Type ?u.13207
inst✝³ : Countable ι
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
⊢ StronglyMeasurable f
let f_sf : α →ₛ β := ⟨f, fun x => ?_, Set.Subsingleton.finite Set.subsingleton_of_subsingleton⟩
no goals
case refine_2
α✝ : Type ?u.13198
β✝ : Type ?u.13201
γ : Type ?u.13204
ι : Type ?u.13207
inst✝³ : Countable ι
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
f_sf : α →ₛ β :=
  { toFun := f, measurableSet_fiber' := (_ : ∀ (x : β), MeasurableSet (f ⁻¹' {x})),
    finite_range' := (_ : Set.Finite (range f)) }
⊢ StronglyMeasurable f
exact ⟨fun _ => f_sf, fun x => tendsto_const_nhds⟩
case refine_1
α✝ : Type ?u.13198
β✝ : Type ?u.13201
γ : Type ?u.13204
ι : Type ?u.13207
inst✝³ : Countable ι
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
x : β
h_univ : f ⁻¹' {x} = univ
⊢ MeasurableSet (f ⁻¹' {x})
case refine_1
α✝ : Type ?u.13198
β✝ : Type ?u.13201
γ : Type ?u.13204
ι : Type ?u.13207
inst✝³ : Countable ι
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
x : β
⊢ MeasurableSet (f ⁻¹' {x})
have h_univ : f ⁻¹' {x} = Set.univ := by
  ext1 y
  simp
case refine_1
α✝ : Type ?u.13198
β✝ : Type ?u.13201
γ : Type ?u.13204
ι : Type ?u.13207
inst✝³ : Countable ι
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
x : β
h_univ : f ⁻¹' {x} = univ
⊢ MeasurableSet univ
case refine_1
α✝ : Type ?u.13198
β✝ : Type ?u.13201
γ : Type ?u.13204
ι : Type ?u.13207
inst✝³ : Countable ι
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
x : β
h_univ : f ⁻¹' {x} = univ
⊢ MeasurableSet (f ⁻¹' {x})
rw [h_univ]
no goals
case refine_1
α✝ : Type ?u.13198
β✝ : Type ?u.13201
γ : Type ?u.13204
ι : Type ?u.13207
inst✝³ : Countable ι
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
x : β
h_univ : f ⁻¹' {x} = univ
⊢ MeasurableSet univ
exact MeasurableSet.univ
case h
α✝ : Type ?u.13198
β✝ : Type ?u.13201
γ : Type ?u.13204
ι : Type ?u.13207
inst✝³ : Countable ι
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
x : β
y : α
⊢ y ∈ f ⁻¹' {x} ↔ y ∈ univ
α✝ : Type ?u.13198
β✝ : Type ?u.13201
γ : Type ?u.13204
ι : Type ?u.13207
inst✝³ : Countable ι
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
x : β
⊢ f ⁻¹' {x} = univ
ext1 y
no goals
case h
α✝ : Type ?u.13198
β✝ : Type ?u.13201
γ : Type ?u.13204
ι : Type ?u.13207
inst✝³ : Countable ι
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton β
f : α → β
x : β
y : α
⊢ y ∈ f ⁻¹' {x} ↔ y ∈ univ
simp