awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : ∀ (n : ℕ), ∃ (t : Set β), IsSeparable t ∧ f (v n) ⁻¹' t ∈ ae μ
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, g x ∈ t
have refine_2 : ∀ (t : (n : ℕ) → Set β) (t_sep : ∀ (n : ℕ), IsSeparable (t n)) (ht : ∀ (n : ℕ), f (v n) ⁻¹' t n ∈ ae μ),
  ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, g x ∈ t
Tactic: choose t t_sep ht using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
t : (n : ℕ) → Set β
t_sep : ∀ (n : ℕ), IsSeparable (t n)
ht : ∀ (n : ℕ), f (v n) ⁻¹' t n ∈ ae μ
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, g x ∈ t
have refine_2 : ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set β) (closure[inst] (⋃ (i : ℕ), t i)) (g x)
Tactic: refine ⟨closure (⋃ i, t i), .closure <| .iUnion t_sep, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
t : (n : ℕ) → Set β
t_sep : ∀ (n : ℕ), IsSeparable (t n)
ht : ∀ (n : ℕ), f (v n) ⁻¹' t n ∈ ae μ
⊢ ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set β) (closure[inst] (⋃ (i : ℕ), t i)) (g x)
have h : ∀ (x : α) (hx : ∀ (i : ℕ), f (v i) x ∈ t i) (h'x : Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))),
  Membership.mem (γ := Set β) (closure[inst] (⋃ (i : ℕ), t i)) (g x)
Tactic: filter_upwards [ae_all_iff.2 ht, lim] with x hx h'x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
t : (n : ℕ) → Set β
t_sep : ∀ (n : ℕ), IsSeparable (t n)
ht : ∀ (n : ℕ), f (v n) ⁻¹' t n ∈ ae μ
x : α
hx : ∀ (i : ℕ), f (v i) x ∈ t i
h'x : Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
⊢ Membership.mem (γ := Set β) (closure[inst] (⋃ (i : ℕ), t i)) (g x)
have h : ∀ᶠ (x_1 : ℕ) in atTop, Membership.mem (γ := Set β) (⋃ (i : ℕ), t i) (((fun (n : ι) ↦ f n x) ∘ v) x_1)
Tactic: apply mem_closure_of_tendsto (h'x.comp hv)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
t : (n : ℕ) → Set β
t_sep : ∀ (n : ℕ), IsSeparable (t n)
ht : ∀ (n : ℕ), f (v n) ⁻¹' t n ∈ ae μ
x : α
hx : ∀ (i : ℕ), f (v i) x ∈ t i
h'x : Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
⊢ ∀ᶠ (x_1 : ℕ) in atTop, Membership.mem (γ := Set β) (⋃ (i : ℕ), t i) (((fun (n : ι) ↦ f n x) ∘ v) x_1)
have h : ∀ (a : ℕ),
  Membership.mem (γ := Set ℕ)
    {x_1 : ℕ | (fun (x_2 : ℕ) ↦ Membership.mem (γ := Set β) (⋃ (i : ℕ), t i) (((fun (n : ι) ↦ f n x) ∘ v) x_2)) x_1} a
Tactic: filter_upwards with n using mem_iUnion_of_mem n (hx n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
t : (n : ℕ) → Set β
t_sep : ∀ (n : ℕ), IsSeparable (t n)
ht : ∀ (n : ℕ), f (v n) ⁻¹' t n ∈ ae μ
x : α
hx : ∀ (i : ℕ), f (v i) x ∈ t i
h'x : Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
h :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x_1 : ℕ | (fun (x_2 : ℕ) ↦ Membership.mem (γ := Set β) (⋃ (i : ℕ), t i) (((fun (n : ι) ↦ f n x) ∘ v) x_2)) x_1} a
⊢ ∀ᶠ (x_1 : ℕ) in atTop, Membership.mem (γ := Set β) (⋃ (i : ℕ), t i) (((fun (n : ι) ↦ f n x) ∘ v) x_1)
have h₁ : ∀ (a : ℕ), Membership.mem (γ := Set β) (⋃ (i : ℕ), t i) (((fun (n : ι) ↦ f n x) ∘ v) a)
Tactic: filter_upwards with n using mem_iUnion_of_mem n (hx n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : PseudoMetrizableSpace β
f : ℕ → α → β
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
⊢ ∃ (f_lim : α → β), StronglyMeasurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
have this : let this := borel β;
BorelSpace β
Tactic: borelize β
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : PseudoMetrizableSpace β
f : ℕ → α → β
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ ∃ (f_lim : α → β), StronglyMeasurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
have obtain : ∀ (g : α → β),
  Measurable g →
    ∀ (hg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))),
      ∃ (f_lim : α → β), StronglyMeasurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
Tactic: obtain ⟨g, _, hg⟩ :
    ∃ g : α → β, Measurable g ∧ ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x)) :=
    measurable_limit_of_tendsto_metrizable_ae (fun n => (hf n).aemeasurable) h_ae_tendsto
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : PseudoMetrizableSpace β
f : ℕ → α → β
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
g : α → β
left : Measurable g
hg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
⊢ ∃ (f_lim : α → β), StronglyMeasurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
have Hg : AEStronglyMeasurable g μ
Tactic: have Hg : AEStronglyMeasurable g μ := aestronglyMeasurable_of_tendsto_ae _ hf hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : PseudoMetrizableSpace β
f : ℕ → α → β
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
g : α → β
left : Measurable g
hg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
Hg : AEStronglyMeasurable g μ
⊢ ∃ (f_lim : α → β), StronglyMeasurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
have refine : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (AEStronglyMeasurable.mk g Hg x))
Tactic: refine ⟨Hg.mk g, Hg.stronglyMeasurable_mk, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : PseudoMetrizableSpace β
f : ℕ → α → β
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
g : α → β
left : Measurable g
hg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
Hg : AEStronglyMeasurable g μ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (AEStronglyMeasurable.mk g Hg x))
have h : ∀ (x : α) (hx : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))) (h'x : g x = AEStronglyMeasurable.mk g Hg x),
  Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (AEStronglyMeasurable.mk g Hg x))
Tactic: filter_upwards [hg, Hg.ae_eq_mk] with x hx h'x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : PseudoMetrizableSpace β
f : ℕ → α → β
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
g : α → β
left : Measurable g
hg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
Hg : AEStronglyMeasurable g μ
x : α
hx : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
h'x : g x = AEStronglyMeasurable.mk g Hg x
⊢ Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (AEStronglyMeasurable.mk g Hg x))
have h : ∀ (hx : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (AEStronglyMeasurable.mk g Hg x)))
  (h'x : g x = AEStronglyMeasurable.mk g Hg x), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (AEStronglyMeasurable.mk g Hg x))
Tactic: rwa [h'x] at hx
Cleared hypotheses: hx, h'x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
hf : AEStronglyMeasurable f μ
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
⊢ ∃ (g : α → β), StronglyMeasurable g ∧ (∀ (x : α), g x ∈ s) ∧ f =ᶠ[ae μ] g
have obtain : ∀ (f' : α → β) (hf' : StronglyMeasurable f') (hff' : f =ᶠ[ae μ] f'),
  ∃ (g : α → β), StronglyMeasurable g ∧ (∀ (x : α), g x ∈ s) ∧ f =ᶠ[ae μ] g
Tactic: obtain ⟨f', hf', hff'⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
⊢ ∃ (g : α → β), StronglyMeasurable g ∧ (∀ (x : α), g x ∈ s) ∧ f =ᶠ[ae μ] g
have refine : StronglyMeasurable ((f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s))
Tactic: refine ⟨(f' ⁻¹' s).piecewise f' (fun _ ↦ h_nonempty.some), ?meas, ?subset, ?ae_eq⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
refine : StronglyMeasurable ((f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s))
⊢ ∃ (g : α → β), StronglyMeasurable g ∧ (∀ (x : α), g x ∈ s) ∧ f =ᶠ[ae μ] g
have refine₁ : ∀ (x : α), (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' (fun (x : α) ↦ h_nonempty.some (s := s)) x ∈ s
Tactic: refine ⟨(f' ⁻¹' s).piecewise f' (fun _ ↦ h_nonempty.some), ?meas, ?subset, ?ae_eq⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
refine : StronglyMeasurable ((f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s))
refine₁ : ∀ (x : α), (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' (fun (x : α) ↦ h_nonempty.some (s := s)) x ∈ s
⊢ ∃ (g : α → β), StronglyMeasurable g ∧ (∀ (x : α), g x ∈ s) ∧ f =ᶠ[ae μ] g
have refine₂ : f =ᶠ[ae μ] (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s)
Tactic: refine ⟨(f' ⁻¹' s).piecewise f' (fun _ ↦ h_nonempty.some), ?meas, ?subset, ?ae_eq⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
⊢ ∀ (x : α), (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' (fun (x : α) ↦ h_nonempty.some (s := s)) x ∈ s
have rw : range ((f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s)) ⊆ s
Tactic: rw [← Set.range_subset_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
⊢ f =ᶠ[ae μ] (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s)
have apply : f' =ᶠ[ae μ] (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s)
Tactic: apply hff'.trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
⊢ f' =ᶠ[ae μ] (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s)
have h : ∀ (x : α) (hx : f x ∈ s) (hx' : f x = f' x),
  f' x = (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' (fun (x : α) ↦ h_nonempty.some (s := s)) x
Tactic: filter_upwards [h_mem, hff'] with x hx hx'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
⊢ f =ᶠ[ae μ] (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s)
have case : f' =ᶠ[ae μ] (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s)
Tactic: case ae_eq =>
    apply hff'.trans
    filter_upwards [h_mem, hff'] with x hx hx'
    exact Eq.symm <| (f' ⁻¹' s).piecewise_eq_of_mem f' _ (by simpa [hx'] using hx)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
case : f' =ᶠ[ae μ] (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s)
⊢ f =ᶠ[ae μ] (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s)
have h : ∀ (x : α) (hx : f x ∈ s) (hx' : f x = f' x),
  f' x = (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' (fun (x : α) ↦ h_nonempty.some (s := s)) x
Tactic: case ae_eq =>
    apply hff'.trans
    filter_upwards [h_mem, hff'] with x hx hx'
    exact Eq.symm <| (f' ⁻¹' s).piecewise_eq_of_mem f' _ (by simpa [hx'] using hx)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
⊢ ∃ (g : α → β), StronglyMeasurable g ∧ (∀ (x : α), g x ∈ s) ∧ f =ᶠ[ae μ] g
have refine : StronglyMeasurable ((f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s))
Tactic: classical
  refine ⟨(f' ⁻¹' s).piecewise f' (fun _ ↦ h_nonempty.some), ?meas, ?subset, ?ae_eq⟩
  case meas => exact hf'.piecewise (hf'.measurable hs) stronglyMeasurable_const
  case subset =>
    rw [← Set.range_subset_iff]
    simpa [Set.range_piecewise] using fun _ _ ↦ h_nonempty.some_mem
  case ae_eq =>
    apply hff'.trans
    filter_upwards [h_mem, hff'] with x hx hx'
    exact Eq.symm <| (f' ⁻¹' s).piecewise_eq_of_mem f' _ (by simpa [hx'] using hx)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
refine : StronglyMeasurable ((f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s))
⊢ ∃ (g : α → β), StronglyMeasurable g ∧ (∀ (x : α), g x ∈ s) ∧ f =ᶠ[ae μ] g
have refine₁ : ∀ (x : α), (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' (fun (x : α) ↦ h_nonempty.some (s := s)) x ∈ s
Tactic: classical
  refine ⟨(f' ⁻¹' s).piecewise f' (fun _ ↦ h_nonempty.some), ?meas, ?subset, ?ae_eq⟩
  case meas => exact hf'.piecewise (hf'.measurable hs) stronglyMeasurable_const
  case subset =>
    rw [← Set.range_subset_iff]
    simpa [Set.range_piecewise] using fun _ _ ↦ h_nonempty.some_mem
  case ae_eq =>
    apply hff'.trans
    filter_upwards [h_mem, hff'] with x hx hx'
    exact Eq.symm <| (f' ⁻¹' s).piecewise_eq_of_mem f' _ (by simpa [hx'] using hx)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
refine : StronglyMeasurable ((f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s))
refine₁ : ∀ (x : α), (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' (fun (x : α) ↦ h_nonempty.some (s := s)) x ∈ s
⊢ ∃ (g : α → β), StronglyMeasurable g ∧ (∀ (x : α), g x ∈ s) ∧ f =ᶠ[ae μ] g
have refine₂ : f =ᶠ[ae μ] (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s)
Tactic: classical
  refine ⟨(f' ⁻¹' s).piecewise f' (fun _ ↦ h_nonempty.some), ?meas, ?subset, ?ae_eq⟩
  case meas => exact hf'.piecewise (hf'.measurable hs) stronglyMeasurable_const
  case subset =>
    rw [← Set.range_subset_iff]
    simpa [Set.range_piecewise] using fun _ _ ↦ h_nonempty.some_mem
  case ae_eq =>
    apply hff'.trans
    filter_upwards [h_mem, hff'] with x hx hx'
    exact Eq.symm <| (f' ⁻¹' s).piecewise_eq_of_mem f' _ (by simpa [hx'] using hx)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
⊢ AEStronglyMeasurable (s.piecewise (β := fun (a : α) ↦ β) f g) μ
have refine : s.piecewise (β := fun (a : α) ↦ β) f g =ᶠ[ae μ]
  s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg)
Tactic: refine ⟨s.piecewise (hf.mk f) (hg.mk g),
    StronglyMeasurable.piecewise hs hf.stronglyMeasurable_mk hg.stronglyMeasurable_mk, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
⊢ s.piecewise (β := fun (a : α) ↦ β) f g =ᶠ[ae μ]
    s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg)
have refine_1 : ∀ᵐ (x : α) ∂μ.restrict s,
  s.piecewise (β := fun (a : α) ↦ β) f g x =
    s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
Tactic: refine ae_of_ae_restrict_of_ae_restrict_compl s ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
refine_1 :
  ∀ᵐ (x : α) ∂μ.restrict s,
    s.piecewise (β := fun (a : α) ↦ β) f g x =
      s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
⊢ s.piecewise (β := fun (a : α) ↦ β) f g =ᶠ[ae μ]
    s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg)
have refine_2 : ∀ᵐ (x : α) ∂μ.restrict sᶜ,
  s.piecewise (β := fun (a : α) ↦ β) f g x =
    s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
Tactic: refine ae_of_ae_restrict_of_ae_restrict_compl s ?_ ?_