awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun (n : ℕ) ↦ (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) ((hf.approx n : (a : α) → β) x : β)
⊢ ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) (0 : β)

Tactic:
have hg_zero : ∀ x ∉ s, ∀ n, g_seq_s n x = 0 := by
    intro x hx n
    rw [SimpleFunc.coe_restrict _ hs, Set.indicator_of_notMem hx]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun (n : ℕ) ↦ (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) ((hf.approx n : (a : α) → β) x : β)
hg_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) (0 : β)
⊢ ∃ (fs : ℕ → α →ₛ β),
    (∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))) ∧
      ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)

Tactic:
⟨g_seq_s, fun x => ?_, hg_zero⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun (n : ℕ) ↦ (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) ((hf.approx n : (a : α) → β) x : β)
hg_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) (0 : β)
refine : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (g_seq_s n : (a : α) → β) x) atTop (𝓝 (f x))
⊢ ∃ (fs : ℕ → α →ₛ β),
    (∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))) ∧
      ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)

Tactic:
refine ⟨g_seq_s, fun x => ?_, hg_zero⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun (n : ℕ) ↦ (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) ((hf.approx n : (a : α) → β) x : β)
hg_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) (0 : β)
x : α
pos : ∀ (hx : x ∈ s), Tendsto (fun (n : ℕ) ↦ (g_seq_s n : (a : α) → β) x) atTop (𝓝 (f x))
neg : ∀ (hx : x ∉ s), Tendsto (fun (n : ℕ) ↦ (g_seq_s n : (a : α) → β) x) atTop (𝓝 (f x))
⊢ Tendsto (fun (n : ℕ) ↦ (g_seq_s n : (a : α) → β) x) atTop (𝓝 (f x))

Tactic:
by_cases hx : x ∈ s
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun (n : ℕ) ↦ (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) ((hf.approx n : (a : α) → β) x : β)
hg_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) (0 : β)
x : α
hx : x ∈ s
pos : Tendsto (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 (f x))
⊢ Tendsto (fun (n : ℕ) ↦ (g_seq_s n : (a : α) → β) x) atTop (𝓝 (f x))

Tactic:
simp_rw [hg_eq x hx]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun (n : ℕ) ↦ (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) ((hf.approx n : (a : α) → β) x : β)
hg_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) (0 : β)
x : α
hx : x ∈ s
⊢ Tendsto (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 (f x))

Tactic:
hf.tendsto_approx x

Premises used: MeasureTheory.StronglyMeasurable.tendsto_approx
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun (n : ℕ) ↦ (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) ((hf.approx n : (a : α) → β) x : β)
hg_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) (0 : β)
x : α
hx : x ∈ s
⊢ Tendsto (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 (f x))

Tactic:
exact hf.tendsto_approx x

Premises used: MeasureTheory.StronglyMeasurable.tendsto_approx
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun (n : ℕ) ↦ (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) ((hf.approx n : (a : α) → β) x : β)
hg_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) (0 : β)
x : α
hx : x ∉ s
neg : Tendsto.{0, u_2} (β := β) (fun (n : ℕ) ↦ 0) atTop (𝓝 0)
⊢ Tendsto (fun (n : ℕ) ↦ (g_seq_s n : (a : α) → β) x) atTop (𝓝 (f x))

Tactic:
simp_rw [hg_zero x hx, hf_zero x hx]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun (n : ℕ) ↦ (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) ((hf.approx n : (a : α) → β) x : β)
hg_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) (0 : β)
x : α
hx : x ∉ s
⊢ Tendsto.{0, u_2} (β := β) (fun (n : ℕ) ↦ 0) atTop (𝓝 0)

Tactic:
tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun (n : ℕ) ↦ (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) ((hf.approx n : (a : α) → β) x : β)
hg_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) (0 : β)
x : α
hx : x ∉ s
⊢ Tendsto.{0, u_2} (β := β) (fun (n : ℕ) ↦ 0) atTop (𝓝 0)

Tactic:
exact tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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
rw : MeasurableSet (s ∩ univ)
⊢ MeasurableSet s

Tactic:
rw [← Set.inter_univ s]

Premises used: Set.inter_univ
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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:
hs Set.univ ?_

Premises used: Set.univ
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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
refine : MeasurableSet (s ∩ univ)
⊢ MeasurableSet (s ∩ univ)

Tactic:
refine hs Set.univ ?_

Premises used: Set.univ
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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
rwa rwa₁ rwa₂ rwa₃ : MeasurableSet s
⊢ MeasurableSet (s ∩ univ)

Tactic:
rwa [Set.inter_univ]

Premises used: Set.inter_univ
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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

Tactic:
have hs_m₂ : MeasurableSet[m₂] s := by
    rw [← Set.inter_univ s]
    refine hs Set.univ ?_
    rwa [Set.inter_univ]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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
obtain :
  ∀ (g_seq_s : ℕ → α →ₛ E)
    (hg_seq_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (g_seq_s n : (a : α) → E) x) atTop (𝓝 (f x)))
    (hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)),
    StronglyMeasurable f
⊢ StronglyMeasurable f

Tactic:
obtain ⟨g_seq_s, hg_seq_tendsto, hg_seq_zero⟩ := stronglyMeasurable_in_set hs_m hf hf_zero

Premises used: MeasureTheory.StronglyMeasurable.stronglyMeasurable_in_set
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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 : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
rw :
  MeasurableSet
    (s ∩ preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∪ preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ)
⊢ MeasurableSet.{u_5} (α := α) (preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x})

Tactic:
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})]

Premises used: Set.inter_univ, Set.union_compl_self, Set.inter_comm, Set.preimage, Singleton.singleton, DFunLike.coe, Set.inter_union_distrib_left
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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 : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
⊢ MeasurableSet
    (s ∩ preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∪ preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ)

Tactic:
MeasurableSet.union (hs _ (hs_m.inter ?_)) ?_

Premises used: MeasurableSet.union, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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 : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
refine_1 : MeasurableSet.{u_5} (α := α) (preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x})
refine_2 : MeasurableSet (preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ)
⊢ MeasurableSet
    (s ∩ preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∪ preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ)

Tactic:
refine MeasurableSet.union (hs _ (hs_m.inter ?_)) ?_

Premises used: MeasurableSet.union, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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 : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
⊢ MeasurableSet.{u_5} (α := α) (preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x})

Tactic:
@SimpleFunc.measurableSet_fiber _ _ m _ _

Premises used: MeasureTheory.SimpleFunc.measurableSet_fiber
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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 : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
⊢ MeasurableSet.{u_5} (α := α) (preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x})

Tactic:
exact @SimpleFunc.measurableSet_fiber _ _ m _ _

Premises used: MeasureTheory.SimpleFunc.measurableSet_fiber
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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 : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
pos : ∀ (hx : x = 0), MeasurableSet (preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ)
neg : ∀ (hx : ¬x = 0), MeasurableSet (preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ)
⊢ MeasurableSet (preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ)

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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 : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
hx : x = 0
this : preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ = sᶜ
rw : MeasurableSet sᶜ
⊢ MeasurableSet (preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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 : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
hx : x = 0
this : preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ = sᶜ
⊢ MeasurableSet sᶜ

Tactic:
hs_m₂.compl

Premises used: MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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 : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
hx : x = 0
this : preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ = sᶜ
⊢ MeasurableSet sᶜ

Tactic:
exact hs_m₂.compl

Premises used: MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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 : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
hx : x = 0
pos : preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ = sᶜ
⊢ MeasurableSet (preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ)

Tactic:
suffices g_seq_s n ⁻¹' {x} ∩ sᶜ = sᶜ by
            rw [this]
            exact hs_m₂.compl
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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 : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
hx : x = 0
pos : ∀ (y : α), y ∈ preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ ↔ y ∈ sᶜ
⊢ preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ = sᶜ

Tactic:
ext1 y
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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 : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
hx : x = 0
y : α
pos : Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) y : E) (0 : E) ∧ y ∈ sᶜ ↔ y ∈ sᶜ
⊢ y ∈ preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ ↔ y ∈ sᶜ

Tactic:
rw [hx, Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff]

Premises used: Set.mem_inter_iff, Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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 : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
hx : x = 0
y : α
⊢ Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) y : E) (0 : E) ∧ y ∈ sᶜ ↔ y ∈ sᶜ

Tactic:
⟨fun h => h.2, fun h => ⟨hg_seq_zero y h n, h⟩⟩

Premises used: And.right, And.intro, Iff.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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 : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
hx : x = 0
y : α
⊢ Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) y : E) (0 : E) ∧ y ∈ sᶜ ↔ y ∈ sᶜ

Tactic:
exact ⟨fun h => h.2, fun h => ⟨hg_seq_zero y h n, h⟩⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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 : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
hx : ¬x = 0
this : preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ = ∅
rw : MeasurableSet.{u_5} (α := α) ∅
⊢ MeasurableSet (preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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 : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
hx : ¬x = 0
this : preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ = ∅
⊢ MeasurableSet.{u_5} (α := α) ∅

Tactic:
MeasurableSet.empty

Premises used: MeasurableSet.empty
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : 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 : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
hx : ¬x = 0
this : preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ = ∅
⊢ MeasurableSet.{u_5} (α := α) ∅

Tactic:
exact MeasurableSet.empty

Premises used: MeasurableSet.empty