awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : AddZeroClass β
inst_2 : TopologicalSpace β
P : (f : α → β) → StronglyMeasurable f → Prop
ind : ∀ (c : β) ⦃s : Set α⦄ (hs : MeasurableSet s), P (s.indicator fun (x : α) ↦ c) ⋯
add :
  ∀ ⦃f g : α → β⦄ (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hfg : StronglyMeasurable (f + g)),
    Disjoint (support f) (support g) → P f hf → P g hg → P (f + g) hfg
lim :
  ∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
    (∀ (n : ℕ), P (f n) ⋯) → (∀ (x : α), Tendsto (fun (x_1 : ℕ) ↦ f x_1 x) atTop (𝓝 (g x))) → P g hg
f : α → β
hf : StronglyMeasurable f
s : ℕ → α →ₛ β := hf.approx
n : ℕ
⊢ P (⇑(s n) : (a : α) → β) ⋯
have induction₁ : ∀ (x : α →ₛ β), P (⇑x : (a : α) → β) sorry
Tactic: induction s n using SimpleFunc.induction with
  | const c hs => exact ind c hs
  | @add f g h_supp hf hg =>
    exact add f.stronglyMeasurable g.stronglyMeasurable (f + g).stronglyMeasurable h_supp hf hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Nonempty β
inst_2 : TopologicalSpace β
P : (f : α → β) → StronglyMeasurable f → Prop
const : ∀ (c : β), P (fun (x : α) ↦ c) ⋯
pcw :
  ∀ ⦃f g : α → β⦄ {s : Set α} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hs : MeasurableSet s),
    P f hf → P g hg → P (s.piecewise (β := fun (a : α) ↦ β) f g) ⋯
lim :
  ∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
    (∀ (n : ℕ), P (f n) ⋯) → (∀ (x : α), Tendsto (fun (x_1 : ℕ) ↦ f x_1 x) atTop (𝓝 (g x))) → P g hg
f : α → β
hf : StronglyMeasurable f
s : ℕ → α →ₛ β := hf.approx
⊢ P f hf
have refine : ∀ (n : ℕ), P (⇑(s n) : (a : α) → β) sorry
Tactic: refine lim (fun n ↦ (s n).stronglyMeasurable) hf (fun n ↦ ?_) hf.tendsto_approx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Nonempty β
inst_2 : TopologicalSpace β
P : (f : α → β) → StronglyMeasurable f → Prop
const : ∀ (c : β), P (fun (x : α) ↦ c) ⋯
pcw :
  ∀ ⦃f g : α → β⦄ {s : Set α} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hs : MeasurableSet s),
    P f hf → P g hg → P (s.piecewise (β := fun (a : α) ↦ β) f g) ⋯
lim :
  ∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
    (∀ (n : ℕ), P (f n) ⋯) → (∀ (x : α), Tendsto (fun (x_1 : ℕ) ↦ f x_1 x) atTop (𝓝 (g x))) → P g hg
f_1 : α → β
hf : StronglyMeasurable f_1
s_1 : ℕ → α →ₛ β := hf.approx
n : ℕ
f g : α →ₛ β
s : Set α
hs : MeasurableSet s
Pf : P (⇑f : (a : α) → β) ⋯
Pg : P (⇑g : (a : α) → β) ⋯
⊢ P (⇑(SimpleFunc.piecewise s hs f g) : (a : α) → β) ⋯
have pcw₁ : P (s.piecewise (β := fun (a : α) ↦ β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)) sorry
Tactic: simp_rw [SimpleFunc.coe_piecewise]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Nonempty β
inst_2 : TopologicalSpace β
P : (f : α → β) → StronglyMeasurable f → Prop
const : ∀ (c : β), P (fun (x : α) ↦ c) ⋯
pcw :
  ∀ ⦃f g : α → β⦄ {s : Set α} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hs : MeasurableSet s),
    P f hf → P g hg → P (s.piecewise (β := fun (a : α) ↦ β) f g) ⋯
lim :
  ∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
    (∀ (n : ℕ), P (f n) ⋯) → (∀ (x : α), Tendsto (fun (x_1 : ℕ) ↦ f x_1 x) atTop (𝓝 (g x))) → P g hg
f : α → β
hf : StronglyMeasurable f
s : ℕ → α →ₛ β := hf.approx
n : ℕ
⊢ P (⇑(s n) : (a : α) → β) ⋯
have induction : ∀ (x : α →ₛ β), P (⇑x : (a : α) → β) sorry
Tactic: induction s n with
  | const c => exact const c
  | @pcw f g s hs Pf Pg =>
    simp_rw [SimpleFunc.coe_piecewise]
    exact pcw f.stronglyMeasurable g.stronglyMeasurable hs Pf Pg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst : TopologicalSpace E
inst_1 : Preorder E
inst_2 : OrderClosedTopology E
inst_3 : PseudoMetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ MeasurableSet.{u_1} (α := α) {a : α | f a ≤ g a}
have this : let this : MeasurableSpace (E × E) := borel (E × E);
BorelSpace.{u_5} (E × E)
Tactic: borelize (E × E)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : TopologicalSpace E
inst_1 : Preorder E
inst_2 : OrderClosedTopology E
inst_3 : PseudoMetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f ≤ᶠ[ae μ] g
⊢ f ≤ᶠ[ae (μ.trim hm)] g
have rwa : MeasurableSet.{u_1} (α := α) {a : α | ¬f a ≤ g a}
Tactic: rwa [EventuallyLE, ae_iff, trim_measurableSet_eq hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
E : Type u_5
m : MeasurableSpace α
f g : α → E
inst : TopologicalSpace E
inst_1 : MetrizableSpace E
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ MeasurableSet.{u_1} (α := α) {a : α | f a = g a}
have this : let this : MeasurableSpace (E × E) := borel (E × E);
BorelSpace.{u_5} (E × E)
Tactic: borelize (E × E)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : TopologicalSpace E
inst_1 : MetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
⊢ f =ᶠ[ae (μ.trim hm)] g
have rwa : MeasurableSet.{u_1} (α := α) {a : α | ¬f a = g a}
Tactic: rwa [EventuallyEq, ae_iff, trim_measurableSet_eq hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
x : α
hx : x ∈ s
n : ℕ
⊢ Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) ((hf.approx n : (a : α) → β) x : β)
have rw : Eq.{u_2 + 1} (α := β) (s.indicator (⇑(hf.approx n) : (a : α) → β) x : β) ((hf.approx n : (a : α) → β) x : β)
Tactic: rw [SimpleFunc.coe_restrict _ hs, Set.indicator_of_mem hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
x : α
hx : x ∈ s
n : ℕ
rw : Eq.{u_2 + 1} (α := β) (s.indicator (⇑(hf.approx n) : (a : α) → β) x : β) ((hf.approx n : (a : α) → β) x : β)
⊢ Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) ((hf.approx n : (a : α) → β) x : β)
have rw₁ : Eq.{u_2 + 1} (α := β) ((hf.approx n : (a : α) → β) x : β) ((hf.approx n : (a : α) → β) x : β)
Tactic: rw [SimpleFunc.coe_restrict _ hs, Set.indicator_of_mem hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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
⊢ ∃ (fs : ℕ → α →ₛ β),
    (∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))) ∧
      ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
have hg_eq : ∀ x ∈ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) ((hf.approx n : (a : α) → β) x : β)
Tactic: have hg_eq : ∀ x ∈ s, ∀ n, g_seq_s n x = hf.approx n x := by
    intro x hx n
    rw [SimpleFunc.coe_restrict _ hs, Set.indicator_of_mem hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : α
hx : x ∉ s
n : ℕ
⊢ Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) (0 : β)
have rw : Eq.{u_2 + 1} (α := β) (s.indicator (⇑(hf.approx n) : (a : α) → β) x) 0
Tactic: rw [SimpleFunc.coe_restrict _ hs, Set.indicator_of_notMem hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : α
hx : x ∉ s
n : ℕ
rw : Eq.{u_2 + 1} (α := β) (s.indicator (⇑(hf.approx n) : (a : α) → β) x) 0
⊢ Eq.{u_2 + 1} (α := β) ((g_seq_s n : (a : α) → β) x : β) (0 : β)
have rw₁ : Eq.{u_2 + 1} (α := β) 0 0
Tactic: rw [SimpleFunc.coe_restrict _ hs, Set.indicator_of_notMem hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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 : β)
⊢ ∃ (fs : ℕ → α →ₛ β),
    (∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))) ∧
      ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
have hg_zero : ∀ 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : β)
have refine : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (g_seq_s n : (a : α) → β) x) atTop (𝓝 (f x))
Tactic: refine ⟨g_seq_s, fun x => ?_, hg_zero⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : α
⊢ Tendsto (fun (n : ℕ) ↦ (g_seq_s n : (a : α) → β) x) atTop (𝓝 (f x))
have pos : ∀ (hx : x ∈ s), Tendsto (fun (n : ℕ) ↦ (g_seq_s n : (a : α) → β) x) atTop (𝓝 (f x))
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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))
⊢ Tendsto (fun (n : ℕ) ↦ (g_seq_s n : (a : α) → β) x) atTop (𝓝 (f x))
have neg : ∀ (hx : x ∉ s), Tendsto (fun (n : ℕ) ↦ (g_seq_s n : (a : α) → β) x) atTop (𝓝 (f x))
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : ℕ) ↦ (g_seq_s n : (a : α) → β) x) atTop (𝓝 (f x))
have pos : Tendsto (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 (f x))
Tactic: simp_rw [hg_eq x hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : ℕ) ↦ (g_seq_s n : (a : α) → β) x) atTop (𝓝 (f x))
have neg : Tendsto.{0, u_2} (β := β) (fun (n : ℕ) ↦ 0) atTop (𝓝 0)
Tactic: simp_rw [hg_zero x hx, hf_zero x hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
have rw : MeasurableSet (s ∩ univ)
Tactic: rw [← Set.inter_univ s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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)
have refine : MeasurableSet (s ∩ univ)
Tactic: refine hs Set.univ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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
⊢ StronglyMeasurable f
have hs_m₂ : MeasurableSet s
Tactic: have hs_m₂ : MeasurableSet[m₂] s := by
    rw [← Set.inter_univ s]
    refine hs Set.univ ?_
    rwa [Set.inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
⊢ StronglyMeasurable f
have 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
Tactic: obtain ⟨g_seq_s, hg_seq_tendsto, hg_seq_zero⟩ := stronglyMeasurable_in_set hs_m hf hf_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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})
have rw : MeasurableSet
  (s ∩ preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∪ preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ)
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})]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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ᶜ)
have refine_1 : MeasurableSet.{u_5} (α := α) (preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x})
Tactic: refine MeasurableSet.union (hs _ (hs_m.inter ?_)) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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})
⊢ MeasurableSet
    (s ∩ preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∪ preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ)
have refine_2 : MeasurableSet (preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ)
Tactic: refine MeasurableSet.union (hs _ (hs_m.inter ?_)) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 (preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ)
have pos : ∀ (hx : x = 0), MeasurableSet (preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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ᶜ)
⊢ MeasurableSet (preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ)
have neg : ∀ (hx : ¬x = 0), MeasurableSet (preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 (preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ)
have rw : MeasurableSet sᶜ
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
⊢ MeasurableSet (preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ)
have pos : preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ = sᶜ
Tactic: suffices g_seq_s n ⁻¹' {x} ∩ sᶜ = sᶜ by
            rw [this]
            exact hs_m₂.compl
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
⊢ preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ = sᶜ
have pos : ∀ (y : α), y ∈ preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ ↔ y ∈ sᶜ
Tactic: ext1 y