awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ι) ↦ f i a) u (𝓝 (g a))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Tendsto f' atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → ℝ≥0∞ := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
hx : x ∈ aeSeqSet h'f p
⊢ Tendsto (fun (i : ℕ) ↦ f (v i) x) atTop (𝓝 (g x))

Tactic:
exact aeSeq.fun_prop_of_mem_aeSeqSet h'f hx

Premises used: aeSeq.fun_prop_of_mem_aeSeqSet
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ι) ↦ f i a) u (𝓝 (g a))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Tendsto f' atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → ℝ≥0∞ := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
hx : x ∉ aeSeqSet h'f p
⊢ Tendsto (fun (i : ℕ) ↦ Nonempty.some ⋯) atTop (𝓝 ⋯.some)

Tactic:
tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ι) ↦ f i a) u (𝓝 (g a))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Tendsto f' atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → ℝ≥0∞ := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
hx : x ∉ aeSeqSet h'f p
⊢ Tendsto (fun (i : ℕ) ↦ Nonempty.some ⋯) atTop (𝓝 ⋯.some)

Tactic:
exact tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ι) ↦ f i a) u (𝓝 (g a))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Tendsto f' atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → ℝ≥0∞ := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
⊢ g =ᶠ[ae μ] aeSeqLim

Tactic:
(ite_ae_eq_of_measure_compl_zero g (fun x ↦ (⟨f (v 0) x⟩ : Nonempty ℝ≥0∞).some)
      (aeSeqSet h'f p) (aeSeq.measure_compl_aeSeqSet_eq_zero h'f hp)).symm

Premises used: Nonempty.some, Nonempty.intro, aeSeq.measure_compl_aeSeqSet_eq_zero, MeasureTheory.ite_ae_eq_of_measure_compl_zero, aeSeqSet, OfNat.ofNat, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ι) ↦ f i a) u (𝓝 (g a))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Tendsto f' atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → ℝ≥0∞ := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
⊢ g =ᶠ[ae μ] aeSeqLim

Tactic:
exact (ite_ae_eq_of_measure_compl_zero g (fun x ↦ (⟨f (v 0) x⟩ : Nonempty ℝ≥0∞).some)
      (aeSeqSet h'f p) (aeSeq.measure_compl_aeSeqSet_eq_zero h'f hp)).symm

Premises used: Nonempty.some, Nonempty.intro, aeSeq.measure_compl_aeSeqSet_eq_zero, MeasureTheory.ite_ae_eq_of_measure_compl_zero, aeSeqSet, OfNat.ofNat, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ι) ↦ f i a) u (𝓝 (g a))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Tendsto f' atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
set set₁ : AEMeasurable g μ
refine_1 :
  let aeSeqLim : (x : α) → ℝ≥0∞ := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some;
  ∀ (x : α), Tendsto (fun (i : ℕ) ↦ aeSeq h'f p i x) atTop (𝓝 (aeSeqLim x))
refine_2 refine_2₁ :
  let aeSeqLim : (x : α) → ℝ≥0∞ := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some;
  g =ᶠ[ae μ] aeSeqLim
⊢ AEMeasurable g μ

Tactic:
classical
  set aeSeqLim := fun x ↦ ite (x ∈ aeSeqSet h'f p) (g x) (⟨f (v 0) x⟩ : Nonempty ℝ≥0∞).some
  refine ⟨aeSeqLim, measurable_of_tendsto' atTop (aeSeq.measurable h'f p)
    (tendsto_pi_nhds.mpr fun x ↦ ?_), ?_⟩
  · unfold aeSeqLim
    simp_rw [aeSeq]
    split_ifs with hx
    · simp_rw [aeSeq.mk_eq_fun_of_mem_aeSeqSet h'f hx]
      exact aeSeq.fun_prop_of_mem_aeSeqSet h'f hx
    · exact tendsto_const_nhds
  · exact (ite_ae_eq_of_measure_compl_zero g (fun x ↦ (⟨f (v 0) x⟩ : Nonempty ℝ≥0∞).some)
      (aeSeqSet h'f p) (aeSeq.measure_compl_aeSeqSet_eq_zero h'f hp)).symm

Premises used: tendsto_const_nhds, aeSeq
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
hf : ∀ (i : ℕ), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (g a))
⊢ AEMeasurable g μ

Tactic:
aemeasurable_of_tendsto' atTop hf hlim

Premises used: Filter.atTop, ENNReal.aemeasurable_of_tendsto'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Measurable (β := ℝ≥0) fun (x : α) ↦ (f x).toNNReal

Tactic:
ENNReal.measurable_toNNReal.comp hf

Premises used: Measurable.comp, ENNReal.measurable_toNNReal, ENNReal.toNNReal, WithTop.untopD, WithTop.recTopCoe
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) μ

Tactic:
ENNReal.measurable_toNNReal.comp_aemeasurable hf

Premises used: ENNReal.measurable_toNNReal, ENNReal.toNNReal, Measurable.comp_aemeasurable, WithTop.untopD, WithTop.recTopCoe
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
⊢ (Measurable (β := ℝ≥0∞) fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔ Measurable f

Tactic:
⟨fun h => h.ennreal_toNNReal, fun h => h.coe_nnreal_ennreal⟩

Premises used: Measurable.ennreal_toNNReal, Measurable.coe_nnreal_ennreal, Iff.intro
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
μ : Measure α
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) μ ↔ AEMeasurable f μ

Tactic:
⟨fun h => h.ennreal_toNNReal, fun h => h.coe_nnreal_ennreal⟩

Premises used: AEMeasurable.ennreal_toNNReal, AEMeasurable.coe_nnreal_ennreal, Iff.intro
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Measurable (β := ℝ) fun (x : α) ↦ (f x).toReal

Tactic:
ENNReal.measurable_toReal.comp hf

Premises used: Measurable.comp, ENNReal.measurable_toReal, ENNReal.toReal, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ) (fun (x : α) ↦ (f x).toReal) μ

Tactic:
ENNReal.measurable_toReal.comp_aemeasurable hf

Premises used: ENNReal.measurable_toReal, ENNReal.toReal, Measurable.comp_aemeasurable, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
simp_rw : Measurable (β := ℝ≥0∞) fun (x : α) ↦ ⨆ (s : Finset ι), ∑ i ∈ s, f i x
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ ∑' (i : ι), f i x

Tactic:
simp_rw [ENNReal.tsum_eq_iSup_sum]

Premises used: ENNReal.tsum_eq_iSup_sum
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ ⨆ (s : Finset ι), ∑ i ∈ s, f i x

Tactic:
.iSup fun s ↦ s.measurable_fun_sum fun i _ => h i

Premises used: Measurable.iSup, Finset.measurable_fun_sum
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ ⨆ (s : Finset ι), ∑ i ∈ s, f i x

Tactic:
exact .iSup fun s ↦ s.measurable_fun_sum fun i _ => h i
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ ∑' (i : ι), f i x

Tactic:
Measurable.ennreal_tsum h

Premises used: Measurable.ennreal_tsum
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
h₁ : ∀ (x : α), Eq (α := ℝ≥0∞) ((∑' (i : ι), f i) x) (∑' (i : ι), f i x)
⊢ Measurable.{u_1, 0} (α := α) (β := ℝ≥0∞) (∑' (i : ι), f i)

Tactic:
convert! Measurable.ennreal_tsum h with x

Premises used: Measurable.ennreal_tsum
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
x : α
⊢ Eq (α := ℝ≥0∞) ((∑' (i : ι), f i) x) (∑' (i : ι), f i x)

Tactic:
tsum_apply (Pi.summable.2 fun _ => ENNReal.summable)

Premises used: Iff.mpr, ENNReal.summable, tsum_apply, Pi.summable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
x : α
⊢ Eq (α := ℝ≥0∞) ((∑' (i : ι), f i) x) (∑' (i : ι), f i x)

Tactic:
exact tsum_apply (Pi.summable.2 fun _ => ENNReal.summable)

Premises used: Iff.mpr, ENNReal.summable, tsum_apply, Pi.summable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : ι → α → ℝ≥0
h : ∀ (i : ι), Measurable (f i)
simp_rw : Measurable (β := ℝ≥0) fun (x : α) ↦ ENNReal.toNNReal (∑' (b : ι), (↑(f b x) : ℝ≥0∞))
⊢ Measurable (β := ℝ≥0) fun (x : α) ↦ ∑' (i : ι), f i x

Tactic:
simp_rw [NNReal.tsum_eq_toNNReal_tsum]

Premises used: NNReal.tsum_eq_toNNReal_tsum
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : ι → α → ℝ≥0
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable (β := ℝ≥0) fun (x : α) ↦ ENNReal.toNNReal (∑' (b : ι), (↑(f b x) : ℝ≥0∞))

Tactic:
(Measurable.ennreal_tsum fun i => (h i).coe_nnreal_ennreal).ennreal_toNNReal

Premises used: Measurable.ennreal_toNNReal, Measurable.coe_nnreal_ennreal, Measurable.ennreal_tsum
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : ι → α → ℝ≥0
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable (β := ℝ≥0) fun (x : α) ↦ ENNReal.toNNReal (∑' (b : ι), (↑(f b x) : ℝ≥0∞))

Tactic:
exact (Measurable.ennreal_tsum fun i => (h i).coe_nnreal_ennreal).ennreal_toNNReal

Premises used: Measurable.ennreal_toNNReal, Measurable.coe_nnreal_ennreal, Measurable.ennreal_tsum
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : ι → α → ℝ≥0∞
μ : Measure α
h : ∀ (i : ι), AEMeasurable (f i) μ
simp_rw : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ⨆ (s : Finset ι), ∑ i ∈ s, f i x) μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ∑' (i : ι), f i x) μ

Tactic:
simp_rw [ENNReal.tsum_eq_iSup_sum]

Premises used: ENNReal.tsum_eq_iSup_sum
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : ι → α → ℝ≥0∞
μ : Measure α
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ⨆ (s : Finset ι), ∑ i ∈ s, f i x) μ

Tactic:
.iSup fun s ↦ Finset.aemeasurable_fun_sum s fun i _ => h i

Premises used: Finset.aemeasurable_fun_sum, AEMeasurable.iSup
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : ι → α → ℝ≥0∞
μ : Measure α
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ⨆ (s : Finset ι), ∑ i ∈ s, f i x) μ

Tactic:
exact .iSup fun s ↦ Finset.aemeasurable_fun_sum s fun i _ => h i
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_5
x : MeasurableSpace α
ι : Type u_6
inst : Countable ι
f : ι → α → ℝ≥0
μ : Measure α
h : ∀ (i : ι), AEMeasurable (f i) μ
simp_rw : AEMeasurable (β := ℝ≥0) (fun (x : α) ↦ ENNReal.toNNReal (∑' (b : ι), (↑(f b x) : ℝ≥0∞))) μ
⊢ AEMeasurable (β := ℝ≥0) (fun (x : α) ↦ ∑' (i : ι), f i x) μ

Tactic:
simp_rw [NNReal.tsum_eq_toNNReal_tsum]

Premises used: NNReal.tsum_eq_toNNReal_tsum
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_5
x : MeasurableSpace α
ι : Type u_6
inst : Countable ι
f : ι → α → ℝ≥0
μ : Measure α
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (β := ℝ≥0) (fun (x : α) ↦ ENNReal.toNNReal (∑' (b : ι), (↑(f b x) : ℝ≥0∞))) μ

Tactic:
(AEMeasurable.ennreal_tsum fun i => (h i).coe_nnreal_ennreal).ennreal_toNNReal

Premises used: AEMeasurable.ennreal_toNNReal, AEMeasurable.coe_nnreal_ennreal, AEMeasurable.ennreal_tsum
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_5
x : MeasurableSpace α
ι : Type u_6
inst : Countable ι
f : ι → α → ℝ≥0
μ : Measure α
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (β := ℝ≥0) (fun (x : α) ↦ ENNReal.toNNReal (∑' (b : ι), (↑(f b x) : ℝ≥0∞))) μ

Tactic:
exact (AEMeasurable.ennreal_tsum fun i => (h i).coe_nnreal_ennreal).ennreal_toNNReal

Premises used: AEMeasurable.ennreal_toNNReal, AEMeasurable.coe_nnreal_ennreal, AEMeasurable.ennreal_tsum
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
⊢ Measurable Real.toEReal

Tactic:
continuous_coe_real_ereal.measurable

Premises used: continuous_coe_real_ereal, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
hf : Measurable f
⊢ Measurable (β := EReal) fun (x : α) ↦ (↑(f x) : EReal)

Tactic:
measurable_coe_real_ereal.comp hf

Premises used: Measurable.comp, measurable_coe_real_ereal, Real.toEReal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable f μ
⊢ AEMeasurable (β := EReal) (fun (x : α) ↦ (↑(f x) : EReal)) μ

Tactic:
measurable_coe_real_ereal.comp_aemeasurable hf

Premises used: measurable_coe_real_ereal, Measurable.comp_aemeasurable, Real.toEReal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : EReal → α
h : Measurable.{0, u_1} (β := α) fun (p : ℝ) ↦ f (↑p : EReal)
⊢ Set.Finite (α := EReal) {⊥, ⊤}

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
⊢ Measurable (β := ℝ) fun (p : ℝ) ↦ (↑p : EReal).toReal

Tactic:
simpa using measurable_id

Premises used: measurable_id
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → EReal
hf : Measurable f
⊢ Measurable (β := ℝ) fun (x : α) ↦ (f x).toReal

Tactic:
measurable_ereal_toReal.comp hf

Premises used: measurable_ereal_toReal, Measurable.comp, EReal.toReal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → EReal
μ : Measure α
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ) (fun (x : α) ↦ (f x).toReal) μ

Tactic:
measurable_ereal_toReal.comp_aemeasurable hf

Premises used: measurable_ereal_toReal, EReal.toReal, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
⊢ Measurable ENNReal.toEReal

Tactic:
continuous_coe_ennreal_ereal.measurable

Premises used: continuous_coe_ennreal_ereal, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Measurable (β := EReal) fun (x : α) ↦ (↑(f x) : EReal)

Tactic:
measurable_coe_ennreal_ereal.comp hf

Premises used: Measurable.comp, measurable_coe_ennreal_ereal, ENNReal.toEReal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
hf : AEMeasurable f μ
⊢ AEMeasurable (β := EReal) (fun (x : α) ↦ (↑(f x) : EReal)) μ

Tactic:
measurable_coe_ennreal_ereal.comp_aemeasurable hf

Premises used: measurable_coe_ennreal_ereal, ENNReal.toEReal, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
⊢ Measurable (β := ℝ≥0∞) fun (p : ℝ) ↦ (↑p : EReal).toENNReal

Tactic:
simpa using ENNReal.measurable_ofReal

Premises used: ENNReal.measurable_ofReal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → EReal
hf : Measurable f
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (f x).toENNReal

Tactic:
measurable_ereal_toENNReal.comp hf

Premises used: measurable_ereal_toENNReal, Measurable.comp, EReal.toENNReal, ite
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → EReal
μ : Measure α
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (f x).toENNReal) μ

Tactic:
measurable_ereal_toENNReal.comp_aemeasurable hf

Premises used: measurable_ereal_toENNReal, EReal.toENNReal, Measurable.comp_aemeasurable, ite
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
mα : MeasurableSpace α
⊢ Measurable (β := ℝ≥0∞) fun (r : ℝ≥0 × ℝ≥0∞) ↦ (↑r.1 : ℝ≥0∞) * r.2

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0
g : α → ℝ≥0
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
simp_rw :
  ∀ (hf : ∀ (i : ι), Measurable (β := ℝ≥0∞) fun (x : α) ↦ (↑(f i x) : ℝ≥0∞)),
    Measurable (β := ℝ≥0∞) fun (x : α) ↦ (↑(g x) : ℝ≥0∞)
⊢ Measurable g

Tactic:
simp_rw [← measurable_coe_nnreal_ennreal_iff] at hf ⊢

Premises used: measurable_coe_nnreal_ennreal_iff
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0
g : α → ℝ≥0
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
lim : Tendsto f u (𝓝 g)
hf : ∀ (i : ι), Measurable (β := ℝ≥0∞) fun (x : α) ↦ (↑(f i x) : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (↑(g x) : ℝ≥0∞)

Tactic:
ENNReal.measurable_of_tendsto' u hf ?_

Premises used: ENNReal.measurable_of_tendsto'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0
g : α → ℝ≥0
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
lim : Tendsto f u (𝓝 g)
hf : ∀ (i : ι), Measurable (β := ℝ≥0∞) fun (x : α) ↦ (↑(f i x) : ℝ≥0∞)
refine :
  Tendsto.{u_5, u_1} (β := α → ℝ≥0∞) (fun (i : ι) (x : α) ↦ (↑(f i x) : ℝ≥0∞)) u (𝓝 fun (x : α) ↦ (↑(g x) : ℝ≥0∞))
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (↑(g x) : ℝ≥0∞)

Tactic:
refine ENNReal.measurable_of_tendsto' u hf ?_

Premises used: ENNReal.measurable_of_tendsto'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0
g : α → ℝ≥0
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
lim : Tendsto f u (𝓝 g)
hf : ∀ (i : ι), Measurable (β := ℝ≥0∞) fun (x : α) ↦ (↑(f i x) : ℝ≥0∞)
rw :
  ∀ (lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x)))
    (hf : ∀ (i : ι), Measurable (β := ℝ≥0∞) fun (x : α) ↦ (↑(f i x) : ℝ≥0∞)) (x : α),
    Tendsto (fun (i : ι) ↦ (↑(f i x) : ℝ≥0∞)) u (𝓝 (↑(g x) : ℝ≥0∞))
⊢ Tendsto.{u_5, u_1} (β := α → ℝ≥0∞) (fun (i : ι) (x : α) ↦ (↑(f i x) : ℝ≥0∞)) u (𝓝 fun (x : α) ↦ (↑(g x) : ℝ≥0∞))

Tactic:
rw [tendsto_pi_nhds] at lim ⊢

Premises used: tendsto_pi_nhds
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0
g : α → ℝ≥0
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))
hf : ∀ (i : ι), Measurable (β := ℝ≥0∞) fun (x : α) ↦ (↑(f i x) : ℝ≥0∞)
⊢ ∀ (x : α), Tendsto (fun (i : ι) ↦ (↑(f i x) : ℝ≥0∞)) u (𝓝 (↑(g x) : ℝ≥0∞))

Tactic:
fun x => (ENNReal.continuous_coe.tendsto (g x)).comp (lim x)

Premises used: ENNReal.ofNNReal, WithTop.some, Continuous.tendsto, ENNReal.continuous_coe, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0
g : α → ℝ≥0
u : Filter ι
inst : u.NeBot
inst_1 : u.IsCountablyGenerated
lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))
hf : ∀ (i : ι), Measurable (β := ℝ≥0∞) fun (x : α) ↦ (↑(f i x) : ℝ≥0∞)
⊢ ∀ (x : α), Tendsto (fun (i : ι) ↦ (↑(f i x) : ℝ≥0∞)) u (𝓝 (↑(g x) : ℝ≥0∞))

Tactic:
exact fun x => (ENNReal.continuous_coe.tendsto (g x)).comp (lim x)

Premises used: Continuous.tendsto, ENNReal.continuous_coe, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0
g : α → ℝ≥0
hf : ∀ (i : ℕ), Measurable (f i)
lim : Tendsto f atTop (𝓝 g)
⊢ Measurable g

Tactic:
measurable_of_tendsto' atTop hf lim

Premises used: Filter.atTop, NNReal.measurable_of_tendsto'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
⊢ MeasurableEmbedding Real.toEReal

Tactic:
isOpenEmbedding_coe.measurableEmbedding

Premises used: EReal.isOpenEmbedding_coe, Topology.IsOpenEmbedding.measurableEmbedding
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
mα : MeasurableSpace α
⊢ MeasurableAdd₂ EReal

Tactic:
⟨EReal.lowerSemicontinuous_add.measurable⟩

Premises used: MeasurableAdd₂.mk, LowerSemicontinuous.measurable, EReal.lowerSemicontinuous_add
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
β : Type u_6
γ : Type u_7
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : EReal × β → γ
h_real : Measurable.{u_6, u_7} (β := γ) fun (p : ℝ × β) ↦ f ((↑p.1 : EReal), p.2)
h_bot : Measurable.{u_6, u_7} (β := γ) fun (x : β) ↦ f (⊥, x)
h_top : Measurable.{u_6, u_7} (β := γ) fun (x : β) ↦ f (⊤, x)
⊢ Subset.{u_6} (α := Set (EReal × β)) univ (range (Prod.mk ⊥) ∪ range (Prod.mk ⊤) ∪ range (Prod.map Real.toEReal id))

Tactic:
simp [-univ_subset_iff, subset_def, EReal.forall]

Premises used: Set.univ_subset_iff, EReal.forall, Set.subset_def