-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem stronglyMeasurable_of_measurableSpace_le_on {α E} {m m₂ : MeasurableSpace α}
    [TopologicalSpace E] [Zero E] {s : Set α} {f : α → E} (hs_m : MeasurableSet[m] s)
    (hs : ∀ t, MeasurableSet[m] (s ∩ t) → MeasurableSet[m₂] (s ∩ t))
    (hf : StronglyMeasurable[m] f) (hf_zero : ∀ x ∉ s, f x = 0) :
    StronglyMeasurable[m₂] f

Proof state:
case neg
α : Type u_5
E : Type u_6
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 ∉ 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 ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0
n : ℕ
x : E
hx : ¬x = 0
⊢ ⇑(g_seq_s n) ⁻¹' {x} ∩ sᶜ = ∅

Tactic:
ext1 y

Result:
case neg.h
α : Type u_5
E : Type u_6
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 ∉ 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 ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0
n : ℕ
x : E
hx : ¬x = 0
y : α
⊢ y ∈ ⇑(g_seq_s n) ⁻¹' {x} ∩ sᶜ ↔ y ∈ ∅

Proof state:
case neg.h
α : Type u_5
E : Type u_6
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 ∉ 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 ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0
n : ℕ
x : E
hx : ¬x = 0
y : α
⊢ y ∈ ⇑(g_seq_s n) ⁻¹' {x} ∩ sᶜ ↔ y ∈ ∅

Tactic:
simp only [mem_inter_iff, mem_preimage, mem_singleton_iff, mem_compl_iff,
  mem_empty_iff_false, iff_false, not_and, not_not_mem]

Result:
case neg.h
α : Type u_5
E : Type u_6
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 ∉ 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 ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0
n : ℕ
x : E
hx : ¬x = 0
y : α
⊢ (g_seq_s n) y = x → y ∈ s

Proof state:
case neg.h
α : Type u_5
E : Type u_6
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 ∉ 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 ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0
n : ℕ
x : E
hx : ¬x = 0
y : α
hys : y ∉ s
⊢ ¬(g_seq_s n) y = x

Tactic:
rw [hg_seq_zero y hys n]

Result:
case neg.h
α : Type u_5
E : Type u_6
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 ∉ 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 ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0
n : ℕ
x : E
hx : ¬x = 0
y : α
hys : y ∉ s
⊢ ¬0 = x

Proof state:
α : Type u_5
E : Type u_6
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 ∉ s, f x = 0
⊢ MeasurableSet (s ∩ univ)

Tactic:
rwa [Set.inter_univ]

Result:
no goals

Proof state:
case neg.h
α : Type u_5
E : Type u_6
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 ∉ 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 ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0
n : ℕ
x : E
hx : ¬x = 0
y : α
hys : y ∉ s
⊢ ¬0 = x

Tactic:
exact Ne.symm hx

Result:
no goals

Proof state:
α : Type u_5
E : Type u_6
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 ∉ 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 ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0
n : ℕ
x : E
hx : x = 0
this : ⇑(g_seq_s n) ⁻¹' {x} ∩ sᶜ = sᶜ
⊢ MeasurableSet sᶜ

Tactic:
exact hs_m₂.compl

Result:
no goals

Proof state:
case pos
α : Type u_5
E : Type u_6
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 ∉ 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 ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0
n : ℕ
x : E
hx : x = 0
⊢ MeasurableSet (⇑(g_seq_s n) ⁻¹' {x} ∩ sᶜ)

Tactic:
suffices g_seq_s n ⁻¹' {x} ∩ sᶜ = sᶜ by
  rw [this]
  exact hs_m₂.compl

Result:
case pos
α : Type u_5
E : Type u_6
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 ∉ 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 ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0
n : ℕ
x : E
hx : x = 0
⊢ ⇑(g_seq_s n) ⁻¹' {x} ∩ sᶜ = sᶜ

Proof state:
α : Type u_5
E : Type u_6
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 ∉ s, f x = 0
⊢ StronglyMeasurable f

Tactic:
have hs_m₂ : MeasurableSet[m₂] s := by
  rw [← Set.inter_univ s]
  refine hs Set.univ ?_
  rwa [Set.inter_univ]

Result:
α : Type u_5
E : Type u_6
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 ∉ s, f x = 0
hs_m₂ : MeasurableSet s
⊢ StronglyMeasurable f