α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
⊢ StronglyMeasurable f
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
⊢ StronglyMeasurable f
have hs_m₂ : MeasurableSet[m₂] s := by
  rw [← Set.inter_univ s]
  refine' hs Set.univ _
  rwa [Set.inter_univ]
case intro.intro
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
⊢ StronglyMeasurable f
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
⊢ StronglyMeasurable f
obtain ⟨g_seq_s, hg_seq_tendsto, hg_seq_zero⟩ := stronglyMeasurable_in_set hs_m hf hf_zero
no goals
case intro.intro
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
g_seq_s₂ : ℕ → α →ₛ E :=
  fun n =>
    { toFun := ↑(g_seq_s n), measurableSet_fiber' := (_ : ∀ (x : E), MeasurableSet (↑(g_seq_s n) ⁻¹' {x})),
      finite_range' := (_ : Set.Finite (range ↑(g_seq_s n))) }
⊢ StronglyMeasurable f
exact ⟨g_seq_s₂, hg_seq_tendsto⟩
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
⊢ MeasurableSet (s ∩ univ)
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
⊢ MeasurableSet s
rw [← Set.inter_univ s]
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
⊢ MeasurableSet (s ∩ univ)
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
⊢ MeasurableSet (s ∩ univ)
refine' hs Set.univ _
no goals
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
⊢ MeasurableSet (s ∩ univ)
rwa [Set.inter_univ]
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
⊢ MeasurableSet (s ∩ ↑(g_seq_s n) ⁻¹' {x} ∪ ↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ)
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
⊢ MeasurableSet (↑(g_seq_s n) ⁻¹' {x})
rw [← Set.inter_univ (g_seq_s n ⁻¹' {x}), ← Set.union_compl_self s,
  Set.inter_union_distrib_left, Set.inter_comm (g_seq_s n ⁻¹' {x})]
case refine'_1
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
⊢ MeasurableSet (↑(g_seq_s n) ⁻¹' {x})

case refine'_2
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
⊢ MeasurableSet (↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ)
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
⊢ MeasurableSet (s ∩ ↑(g_seq_s n) ⁻¹' {x} ∪ ↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ)
refine' MeasurableSet.union (hs _ (hs_m.inter _)) _
case pos
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : x = 0
⊢ MeasurableSet (↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ)

case neg
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : ¬x = 0
⊢ MeasurableSet (↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ)
case refine'_2
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
⊢ MeasurableSet (↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ)
by_cases hx : x = 0
no goals
case refine'_1
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
⊢ MeasurableSet (↑(g_seq_s n) ⁻¹' {x})
exact @SimpleFunc.measurableSet_fiber _ _ m _ _
case pos
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : x = 0
⊢ ↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ = sᶜ
case pos
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : x = 0
⊢ MeasurableSet (↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ)
suffices g_seq_s n ⁻¹' {x} ∩ sᶜ = sᶜ by
  rw [this]
  exact hs_m₂.compl
case pos.h
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : x = 0
y : α
⊢ y ∈ ↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ ↔ y ∈ sᶜ
case pos
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : x = 0
⊢ ↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ = sᶜ
ext1 y
case pos.h
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : x = 0
y : α
⊢ ↑(g_seq_s n) y = 0 ∧ y ∈ sᶜ ↔ y ∈ sᶜ
case pos.h
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : x = 0
y : α
⊢ y ∈ ↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ ↔ y ∈ sᶜ
rw [hx, Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff]
no goals
case pos.h
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : x = 0
y : α
⊢ ↑(g_seq_s n) y = 0 ∧ y ∈ sᶜ ↔ y ∈ sᶜ
exact ⟨fun h => h.2, fun h => ⟨hg_seq_zero y h n, h⟩⟩
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : x = 0
this : ↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ = sᶜ
⊢ MeasurableSet (sᶜ)
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : x = 0
this : ↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ = sᶜ
⊢ MeasurableSet (↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ)
rw [this]
no goals
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : x = 0
this : ↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ = sᶜ
⊢ MeasurableSet (sᶜ)
exact hs_m₂.compl
case neg
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : ¬x = 0
⊢ ↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ = ∅
case neg
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : ¬x = 0
⊢ MeasurableSet (↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ)
suffices g_seq_s n ⁻¹' {x} ∩ sᶜ = ∅ by
  rw [this]
  exact MeasurableSet.empty
case neg.h
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : ¬x = 0
y : α
⊢ y ∈ ↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ ↔ y ∈ ∅
case neg
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : ¬x = 0
⊢ ↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ = ∅
ext1 y
case neg.h
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : ¬x = 0
y : α
⊢ ↑(g_seq_s n) y = x → y ∈ s
case neg.h
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : ¬x = 0
y : α
⊢ y ∈ ↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ ↔ y ∈ ∅
simp only [mem_inter_iff, mem_preimage, mem_singleton_iff, mem_compl_iff,
  mem_empty_iff_false, iff_false_iff, not_and, not_not_mem]
case neg.h
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : ¬x = 0
y : α
hys : ¬y ∈ s
⊢ ¬↑(g_seq_s n) y = x
case neg.h
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : ¬x = 0
y : α
⊢ ↑(g_seq_s n) y = x → y ∈ s
refine' Function.mtr fun hys => _
case neg.h
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : ¬x = 0
y : α
hys : ¬y ∈ s
⊢ ¬0 = x
case neg.h
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : ¬x = 0
y : α
hys : ¬y ∈ s
⊢ ¬↑(g_seq_s n) y = x
rw [hg_seq_zero y hys n]
no goals
case neg.h
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : ¬x = 0
y : α
hys : ¬y ∈ s
⊢ ¬0 = x
exact Ne.symm hx
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : ¬x = 0
this : ↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ = ∅
⊢ MeasurableSet ∅
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : ¬x = 0
this : ↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ = ∅
⊢ MeasurableSet (↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ)
rw [this]
no goals
α✝ : Type ?u.231002
β : Type ?u.231005
γ : Type ?u.231008
ι : Type ?u.231011
inst✝² : Countable ι
f✝ g : α✝ → β
α : Type u_1
E : Type u_2
m m₂ : MeasurableSpace α
inst✝¹ : TopologicalSpace E
inst✝ : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
n : ℕ
x : E
hx : ¬x = 0
this : ↑(g_seq_s n) ⁻¹' {x} ∩ sᶜ = ∅
⊢ MeasurableSet ∅
exact MeasurableSet.empty