-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem _root_.stronglyMeasurable_bot_iff [Nonempty β] [T2Space β] :
    StronglyMeasurable[⊥] f ↔ ∃ c, f = fun _ => c

Proof state:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), (fs n) x = c
cs : ℕ → β := fun n => ⋯.choose
⊢ f = fun x => f hα.some

Tactic:
have h_cs_eq : ∀ n, ⇑(fs n) = fun _ => cs n := fun n => funext (this n).choose_spec

Result:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), (fs n) x = c
cs : ℕ → β := fun n => ⋯.choose
h_cs_eq : ∀ (n : ℕ), ⇑(fs n) = fun x => cs n
⊢ f = fun x => f hα.some

Proof state:
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
⊢ StronglyMeasurable f ↔ ∃ c, f = fun x => c

Tactic:
rcases isEmpty_or_nonempty α with hα | hα

Result:
case inl
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : IsEmpty α
⊢ StronglyMeasurable f ↔ ∃ c, f = fun x => c

case inr
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
⊢ StronglyMeasurable f ↔ ∃ c, f = fun x => c

Proof state:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
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 hα.some

Tactic:
let cs n := (this n).choose

Result:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), (fs n) x = c
cs : ℕ → β := fun n => ⋯.choose
⊢ f = fun x => f hα.some

Proof state:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), (fs n) x = c
cs : ℕ → β := fun n => ⋯.choose
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 hα.some

Tactic:
have h_tendsto : Tendsto cs atTop (𝓝 (f hα.some)) := h_fs_tendsto hα.some

Result:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), (fs n) x = c
cs : ℕ → β := fun n => ⋯.choose
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 hα.some))
⊢ f = fun x => f hα.some

Proof state:
case inr.refine_2
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf_eq : ∃ c, f = fun x => c
⊢ StronglyMeasurable f

Tactic:
obtain ⟨c, rfl⟩ := hf_eq

Result:
case inr.refine_2.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
c : β
⊢ StronglyMeasurable fun x => c

Proof state:
case inr.refine_2.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
c : β
⊢ StronglyMeasurable fun x => c

Tactic:
exact stronglyMeasurable_const

Result:
no goals

Proof state:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))
⊢ f = fun x => f hα.some

Tactic:
have : ∀ n, ∃ c, ∀ x, fs n x = c := fun n => SimpleFunc.simpleFunc_bot (fs n)

Result:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
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 hα.some

Proof state:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
⊢ ∃ c, f = fun x => c

Tactic:
refine ⟨f hα.some, ?_⟩

Result:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
⊢ f = fun x => f hα.some

Proof state:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
⊢ f = fun x => f hα.some

Tactic:
let fs := hf.approx

Result:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
⊢ f = fun x => f hα.some

Proof state:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
⊢ f = fun x => f hα.some

Tactic:
have h_fs_tendsto : ∀ x, Tendsto (fun n => fs n x) atTop (𝓝 (f x)) := hf.tendsto_approx

Result:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))
⊢ f = fun x => f hα.some

Proof state:
case inr
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
⊢ StronglyMeasurable f ↔ ∃ c, f = fun x => c

Tactic:
refine ⟨fun hf => ?_, fun hf_eq => ?_⟩

Result:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
⊢ ∃ c, f = fun x => c

case inr.refine_2
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf_eq : ∃ c, f = fun x => c
⊢ StronglyMeasurable f

Proof state:
case inl
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : IsEmpty α
⊢ StronglyMeasurable f ↔ ∃ c, f = fun x => c

Tactic:
simp only [@Subsingleton.stronglyMeasurable' _ _ ⊥ _ _ f,
  eq_iff_true_of_subsingleton, exists_const]

Result:
no goals

Proof state:
case inr.refine_1.h
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), (fs n) x = c
cs : ℕ → β := fun n => ⋯.choose
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 hα.some))
x : α
⊢ f x = f hα.some

Tactic:
exact tendsto_nhds_unique (h_fs_tendsto x) h_tendsto

Result:
no goals