case inl
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : IsEmpty α
⊢ StronglyMeasurable f ↔ ∃ c, f = fun x => c

case inr
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
⊢ StronglyMeasurable f ↔ ∃ c, f = fun x => c
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
⊢ StronglyMeasurable f ↔ ∃ c, f = fun x => c
cases' isEmpty_or_nonempty α with hα hα
case inr.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
⊢ ∃ c, f = fun x => c

case inr.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf_eq : ∃ c, f = fun x => c
⊢ StronglyMeasurable f
case inr
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
⊢ StronglyMeasurable f ↔ ∃ c, f = fun x => c
refine' ⟨fun hf => _, fun hf_eq => _⟩
no goals
case inl
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : IsEmpty α
⊢ StronglyMeasurable f ↔ ∃ c, f = fun x => c
simp only [@Subsingleton.stronglyMeasurable' _ _ ⊥ _ _ f,
  eq_iff_true_of_subsingleton, exists_const]
case inr.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
⊢ f = fun x => f (Nonempty.some hα)
case inr.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
⊢ ∃ c, f = fun x => c
refine' ⟨f hα.some, _⟩
case inr.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := StronglyMeasurable.approx hf
⊢ f = fun x => f (Nonempty.some hα)
case inr.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
⊢ f = fun x => f (Nonempty.some hα)
let fs := hf.approx
case inr.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := StronglyMeasurable.approx hf
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
⊢ f = fun x => f (Nonempty.some hα)
case inr.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := StronglyMeasurable.approx hf
⊢ f = fun x => f (Nonempty.some hα)
have h_fs_tendsto : ∀ x, Tendsto (fun n => fs n x) atTop (𝓝 (f x)) := hf.tendsto_approx
case inr.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := StronglyMeasurable.approx hf
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), ↑(fs n) x = c
⊢ f = fun x => f (Nonempty.some hα)
case inr.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := StronglyMeasurable.approx hf
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
⊢ f = fun x => f (Nonempty.some hα)
have : ∀ n, ∃ c, ∀ x, fs n x = c := fun n => SimpleFunc.simpleFunc_bot (fs n)
case inr.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := StronglyMeasurable.approx hf
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), ↑(fs n) x = c
cs : ℕ → β := fun n => Exists.choose (_ : ∃ c, ∀ (x : α), ↑(fs n) x = c)
⊢ f = fun x => f (Nonempty.some hα)
case inr.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := StronglyMeasurable.approx hf
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), ↑(fs n) x = c
⊢ f = fun x => f (Nonempty.some hα)
let cs n := (this n).choose
case inr.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := StronglyMeasurable.approx hf
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), ↑(fs n) x = c
cs : ℕ → β := fun n => Exists.choose (_ : ∃ c, ∀ (x : α), ↑(fs n) x = c)
h_cs_eq : ∀ (n : ℕ), ↑(fs n) = fun x => cs n
⊢ f = fun x => f (Nonempty.some hα)
case inr.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := StronglyMeasurable.approx hf
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), ↑(fs n) x = c
cs : ℕ → β := fun n => Exists.choose (_ : ∃ c, ∀ (x : α), ↑(fs n) x = c)
⊢ f = fun x => f (Nonempty.some hα)
have h_cs_eq : ∀ n, ⇑(fs n) = fun _ => cs n := fun n => funext (this n).choose_spec
case inr.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := StronglyMeasurable.approx hf
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), ↑(fs n) x = c
cs : ℕ → β := fun n => Exists.choose (_ : ∃ c, ∀ (x : α), ↑(fs n) x = c)
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => (fun x => cs n) x) atTop (𝓝 (f x))
h_cs_eq : ∀ (n : ℕ), ↑(fs n) = fun x => cs n
⊢ f = fun x => f (Nonempty.some hα)
case inr.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := StronglyMeasurable.approx hf
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), ↑(fs n) x = c
cs : ℕ → β := fun n => Exists.choose (_ : ∃ c, ∀ (x : α), ↑(fs n) x = c)
h_cs_eq : ∀ (n : ℕ), ↑(fs n) = fun x => cs n
⊢ f = fun x => f (Nonempty.some hα)
conv at h_fs_tendsto => enter [x, 1, n]; rw [h_cs_eq]
case inr.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := StronglyMeasurable.approx hf
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), ↑(fs n) x = c
cs : ℕ → β := fun n => Exists.choose (_ : ∃ c, ∀ (x : α), ↑(fs n) x = c)
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => (fun x => cs n) x) atTop (𝓝 (f x))
h_cs_eq : ∀ (n : ℕ), ↑(fs n) = fun x => cs n
h_tendsto : Tendsto cs atTop (𝓝 (f (Nonempty.some hα)))
⊢ f = fun x => f (Nonempty.some hα)
case inr.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := StronglyMeasurable.approx hf
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), ↑(fs n) x = c
cs : ℕ → β := fun n => Exists.choose (_ : ∃ c, ∀ (x : α), ↑(fs n) x = c)
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => (fun x => cs n) x) atTop (𝓝 (f x))
h_cs_eq : ∀ (n : ℕ), ↑(fs n) = fun x => cs n
⊢ f = fun x => f (Nonempty.some hα)
have h_tendsto : Tendsto cs atTop (𝓝 (f hα.some)) := h_fs_tendsto hα.some
case inr.refine'_1.h
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := StronglyMeasurable.approx hf
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), ↑(fs n) x = c
cs : ℕ → β := fun n => Exists.choose (_ : ∃ c, ∀ (x : α), ↑(fs n) x = c)
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => (fun x => cs n) x) atTop (𝓝 (f x))
h_cs_eq : ∀ (n : ℕ), ↑(fs n) = fun x => cs n
h_tendsto : Tendsto cs atTop (𝓝 (f (Nonempty.some hα)))
x : α
⊢ f x = f (Nonempty.some hα)
case inr.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := StronglyMeasurable.approx hf
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), ↑(fs n) x = c
cs : ℕ → β := fun n => Exists.choose (_ : ∃ c, ∀ (x : α), ↑(fs n) x = c)
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => (fun x => cs n) x) atTop (𝓝 (f x))
h_cs_eq : ∀ (n : ℕ), ↑(fs n) = fun x => cs n
h_tendsto : Tendsto cs atTop (𝓝 (f (Nonempty.some hα)))
⊢ f = fun x => f (Nonempty.some hα)
ext1 x
no goals
case inr.refine'_1.h
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := StronglyMeasurable.approx hf
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), ↑(fs n) x = c
cs : ℕ → β := fun n => Exists.choose (_ : ∃ c, ∀ (x : α), ↑(fs n) x = c)
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => (fun x => cs n) x) atTop (𝓝 (f x))
h_cs_eq : ∀ (n : ℕ), ↑(fs n) = fun x => cs n
h_tendsto : Tendsto cs atTop (𝓝 (f (Nonempty.some hα)))
x : α
⊢ f x = f (Nonempty.some hα)
exact tendsto_nhds_unique (h_fs_tendsto x) h_tendsto
case inr.refine'_2.intro
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
c : β
⊢ StronglyMeasurable fun x => c
case inr.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf_eq : ∃ c, f = fun x => c
⊢ StronglyMeasurable f
obtain ⟨c, rfl⟩ := hf_eq
no goals
case inr.refine'_2.intro
α : Type u_2
β : Type u_1
γ : Type ?u.48568
ι : Type ?u.48571
inst✝³ : Countable ι
g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
c : β
⊢ StronglyMeasurable fun x => c
exact stronglyMeasurable_const