awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
⊢ Measurable ENNReal.ofNNReal

Tactic:
ENNReal.continuous_coe.measurable

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

Tactic:
ENNReal.continuous_coe.measurable.comp hf

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

Tactic:
ENNReal.continuous_coe.measurable.comp_aemeasurable hf

Premises used: ENNReal.ofNNReal, WithTop.some, Continuous.measurable, Measurable.comp_aemeasurable, ENNReal.continuous_coe
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
hf : Measurable f
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ ENNReal.ofReal (f x)

Tactic:
ENNReal.continuous_ofReal.measurable.comp hf

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

Tactic:
ENNReal.continuous_ofReal.measurable.comp_aemeasurable hf

Premises used: ENNReal.ofNNReal, ENNReal.ofReal, ENNReal.continuous_ofReal, WithTop.some, Continuous.measurable, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
h : Measurable (β := ℝ) fun (x : α) ↦ (↑(f x) : ℝ)
⊢ Measurable f

Tactic:
simpa only [Real.toNNReal_coe] using h.real_toNNReal

Premises used: Measurable.real_toNNReal, Real.toNNReal_coe
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
hf : Measurable f
h'f : ∀ (x : α), 0 ≤ f x
⊢ Measurable (β := ℝ≥0) fun (x : α) ↦ NNReal.mk (f x) ⋯

Tactic:
measurable_coe_nnreal_real_iff.mp hf

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

Tactic:
simpa only [Real.toNNReal_coe] using h.real_toNNReal

Premises used: AEMeasurable.real_toNNReal, Real.toNNReal_coe
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
α : Type u_1
mα : MeasurableSpace α
f : ℝ≥0∞ → α
h : Measurable.{0, u_1} (β := α) fun (p : ℝ≥0) ↦ f (↑p : ℝ≥0∞)
⊢ Measurable f

Tactic:
measurable_of_measurable_on_compl_singleton ∞
    (MeasurableEquiv.ennrealEquivNNReal.symm.measurable_comp_iff.1 h)

Premises used: MeasurableEquiv.symm, MeasurableEquiv.ennrealEquivNNReal, MeasurableEquiv.measurable_comp_iff, measurable_of_measurable_on_compl_singleton, Iff.mp, Top.top
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
β : Type u_2
γ : Type u_3
x : MeasurableSpace β
x_1 : MeasurableSpace γ
f : ℝ≥0∞ × β → γ
H₁ : Measurable.{u_2, u_3} (β := γ) fun (p : ℝ≥0 × β) ↦ f ((↑p.1 : ℝ≥0∞), p.2)
H₂ : Measurable.{u_2, u_3} (β := γ) fun (x : β) ↦ f (∞, x)
⊢ Measurable f

Tactic:
let e : ℝ≥0∞ × β ≃ᵐ (ℝ≥0 × β) ⊕ (Unit × β) :=
    (ennrealEquivSum.prodCongr (MeasurableEquiv.refl β)).trans
      (MeasurableEquiv.sumProdDistrib _ _ _)
  e.symm.measurable_comp_iff.1 <| measurable_fun_sum H₁ (H₂.comp measurable_id.snd)

Premises used: ENNReal.ennrealEquivSum, Measurable.comp, measurable_id, MeasurableEquiv.prodCongr, MeasurableEquiv.symm, MeasurableEquiv.refl, measurable_fun_sum, NNReal, MeasurableEquiv.trans, Unit, MeasurableEquiv.sumProdDistrib, MeasurableEquiv.measurable_comp_iff, Iff.mp, Measurable.snd
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
β : Type u_2
x : MeasurableSpace β
f : ℝ≥0∞ × ℝ≥0∞ → β
h₁ : Measurable.{0, u_2} (β := β) fun (p : ℝ≥0 × ℝ≥0) ↦ f ((↑p.1 : ℝ≥0∞), (↑p.2 : ℝ≥0∞))
h₂ : Measurable.{0, u_2} (β := β) fun (r : ℝ≥0) ↦ f (∞, (↑r : ℝ≥0∞))
h₃ : Measurable.{0, u_2} (β := β) fun (r : ℝ≥0) ↦ f ((↑r : ℝ≥0∞), ∞)
⊢ Measurable f

Tactic:
measurable_of_measurable_nnreal_prod
    (measurable_swap_iff.1 <| measurable_of_measurable_nnreal_prod (h₁.comp measurable_swap) h₃)
    (measurable_of_measurable_nnreal h₂)

Premises used: Measurable.comp, ENNReal.measurable_of_measurable_nnreal_prod, measurable_swap, ENNReal.measurable_of_measurable_nnreal, Iff.mp, measurable_swap_iff
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
⊢ Measurable ENNReal.ofReal

Tactic:
ENNReal.continuous_ofReal.measurable

Premises used: ENNReal.continuous_ofReal, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
⊢ Measurable ENNReal.toReal

Tactic:
ENNReal.measurable_of_measurable_nnreal measurable_coe_nnreal_real

Premises used: measurable_coe_nnreal_real, ENNReal.measurable_of_measurable_nnreal
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
⊢ Measurable ENNReal.toNNReal

Tactic:
ENNReal.measurable_of_measurable_nnreal measurable_id

Premises used: measurable_id, ENNReal.measurable_of_measurable_nnreal
-- 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 α
⊢ MeasurableMul₂ ℝ≥0∞

Tactic:
⟨measurable_of_measurable_nnreal_nnreal ?_ ?_ ?_⟩

Premises used: ENNReal.measurable_of_measurable_nnreal_nnreal, MeasurableMul₂.mk
-- 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 α
refine_1 :
  Measurable (β := ℝ≥0∞) fun (p : ℝ≥0 × ℝ≥0) ↦ ((↑p.1 : ℝ≥0∞), (↑p.2 : ℝ≥0∞)).1 * ((↑p.1 : ℝ≥0∞), (↑p.2 : ℝ≥0∞)).2
refine_2 : Measurable (β := ℝ≥0∞) fun (r : ℝ≥0) ↦ (∞, (↑r : ℝ≥0∞)).1 * (∞, (↑r : ℝ≥0∞)).2
refine_3 : Measurable (β := ℝ≥0∞) fun (r : ℝ≥0) ↦ ((↑r : ℝ≥0∞), ∞).1 * ((↑r : ℝ≥0∞), ∞).2
⊢ MeasurableMul₂ ℝ≥0∞

Tactic:
refine ⟨measurable_of_measurable_nnreal_nnreal ?_ ?_ ?_⟩
-- 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 (p : ℝ≥0 × ℝ≥0) ↦ ((↑p.1 : ℝ≥0∞), (↑p.2 : ℝ≥0∞)).1 * ((↑p.1 : ℝ≥0∞), (↑p.2 : ℝ≥0∞)).2

Tactic:
simp only [← ENNReal.coe_mul, measurable_mul.coe_nnreal_ennreal]

Premises used: MeasurableMul₂.measurable_mul, Measurable.coe_nnreal_ennreal, ENNReal.coe_mul
-- 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) ↦ if r = 0 then 0 else ∞

Tactic:
measurable_const.piecewise (measurableSet_singleton _) measurable_const

Premises used: MeasurableSingletonClass.measurableSet_singleton, Set.Mem, Measurable.piecewise, measurable_const, Set.piecewise
-- 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) ↦ if r = 0 then 0 else ∞

Tactic:
exact measurable_const.piecewise (measurableSet_singleton _) measurable_const

Premises used: MeasurableSingletonClass.measurableSet_singleton, Measurable.piecewise, measurable_const
-- 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) ↦ (∞, (↑r : ℝ≥0∞)).1 - (∞, (↑r : ℝ≥0∞)).2

Tactic:
simp
-- 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) ↦ ((↑r : ℝ≥0∞), ∞).1 - ((↑r : ℝ≥0∞), ∞).2

Tactic:
simp
-- 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 α
⊢ MeasurableInv ℝ≥0∞

Tactic:
⟨continuous_inv.measurable⟩

Premises used: MeasurableInv.mk, Continuous.measurable, ContinuousInv.continuous_inv
-- 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 α
x : ℝ≥0
⊢ Measurable (β := ℝ≥0∞) fun (x_1 : ℝ≥0∞) ↦ (↑x : ℝ≥0∞) • x_1

Tactic:
measurable_const_smul _

Premises used: MeasurableConstSMul.measurable_const_smul
-- 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 α
x : ℝ≥0
⊢ Measurable (β := ℝ≥0∞) fun (x_1 : ℝ≥0∞) ↦ (↑x : ℝ≥0∞) • x_1

Tactic:
exact measurable_const_smul _

Premises used: MeasurableConstSMul.measurable_const_smul
-- 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 α
x : ℝ≥0∞
⊢ Measurable (β := ℝ≥0∞) fun (x_1 : ℝ≥0) ↦ (↑x_1 : ℝ≥0∞) • x

Tactic:
measurable_coe_nnreal_ennreal.mul_const _

Premises used: measurable_coe_nnreal_ennreal, Measurable.mul_const
-- 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 α
x : ℝ≥0∞
⊢ Measurable (β := ℝ≥0∞) fun (x_1 : ℝ≥0) ↦ (↑x_1 : ℝ≥0∞) • x

Tactic:
exact measurable_coe_nnreal_ennreal.mul_const _

Premises used: measurable_coe_nnreal_ennreal, Measurable.mul_const
-- 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)
rcases : ∀ (x : ℕ → ι) (hx : Tendsto x atTop u), Measurable g
⊢ Measurable g

Tactic:
rcases u.exists_seq_tendsto with ⟨x, hx⟩

Premises used: Filter.exists_seq_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
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
x : ℕ → ι
hx : Tendsto x atTop u
rw : ∀ (lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))) (x : ℕ → ι) (hx : Tendsto x atTop u), Measurable g
⊢ Measurable g

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
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
h : ∀ (y : α), liminf (fun (n : ℕ) ↦ f (x n) y) atTop = g y
⊢ (fun (y : α) ↦ liminf (fun (n : ℕ) ↦ f (x n) y) atTop) = g

Tactic:
ext1 y
-- 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 : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
y : α
⊢ liminf (fun (n : ℕ) ↦ f (x n) y) atTop = g y

Tactic:
((lim y).comp hx).liminf_eq

Premises used: Filter.Tendsto.liminf_eq, 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
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
y : α
⊢ liminf (fun (n : ℕ) ↦ f (x n) y) atTop = g y

Tactic:
exact ((lim y).comp hx).liminf_eq

Premises used: Filter.Tendsto.liminf_eq, 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
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
⊢ (fun (y : α) ↦ liminf (fun (n : ℕ) ↦ f (x n) y) atTop) = g

Tactic:
have : (fun y => liminf (fun n => (f (x n) y : ℝ≥0∞)) atTop) = g := by
    ext1 y
    exact ((lim y).comp hx).liminf_eq
-- 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 : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
this : (fun (y : α) ↦ liminf (fun (n : ℕ) ↦ f (x n) y) atTop) = g
rw : Measurable (β := ℝ≥0∞) fun (y : α) ↦ liminf (fun (n : ℕ) ↦ f (x n) y) atTop
⊢ Measurable g

Tactic:
rw [← this]
-- 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 : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
this : (fun (y : α) ↦ liminf (fun (n : ℕ) ↦ f (x n) y) atTop) = g
⊢ Measurable (β := ℝ≥0∞) fun (y : α) ↦ liminf (fun (n : ℕ) ↦ f (x n) y) atTop

Tactic:
.liminf fun n => hf (x n)

Premises used: Measurable.liminf
-- 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 : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
this : (fun (y : α) ↦ liminf (fun (n : ℕ) ↦ f (x n) y) atTop) = g
⊢ Measurable (β := ℝ≥0∞) fun (y : α) ↦ liminf (fun (n : ℕ) ↦ f (x n) y) atTop

Tactic:
exact .liminf fun n => hf (x n)
-- 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: ENNReal.measurable_of_tendsto', Filter.atTop
-- 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))
rcases : ∀ (v : ℕ → ι) (hv : Tendsto v atTop u), AEMeasurable g μ
⊢ AEMeasurable g μ

Tactic:
rcases u.exists_seq_tendsto with ⟨v, hv⟩

Premises used: Filter.exists_seq_tendsto
-- 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
⊢ ∀ (n : ℕ), AEMeasurable (f (v n)) μ

Tactic:
have h'f : ∀ n, AEMeasurable (f (v n)) μ := fun n ↦ hf (v n)
-- 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))
x : α
hx : Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))
⊢ p x fun (n : ℕ) ↦ f (v n) x

Tactic:
hx.comp hv

Premises used: Filter.Tendsto.comp
-- 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))
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ Tendsto (fun (i : ι) ↦ f i a) u (𝓝 (g a))) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ p x fun (n : ℕ) ↦ f (v n) x) x} x}
      a
h₁ h₂ : ∀ (x : α) (hx : Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))), p x fun (n : ℕ) ↦ f (v n) x
⊢ ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x

Tactic:
filter_upwards [hlim] with x hx using hx.comp hv
-- 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))
⊢ ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x

Tactic:
have hp : ∀ᵐ x ∂μ, p x fun n ↦ f (v n) x := by
    filter_upwards [hlim] with x hx using hx.comp hv
-- 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
⊢ AEMeasurable g μ

Tactic:
⟨aeSeqLim, measurable_of_tendsto' atTop (aeSeq.measurable h'f p)
    (tendsto_pi_nhds.mpr fun x ↦ ?_), ?_⟩

Premises used: Iff.mpr, AEMeasurable, aeSeq.measurable, ENNReal.measurable_of_tendsto', tendsto_pi_nhds, Filter.atTop, And.intro, Exists.intro
-- 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
refine_1 : ∀ (x : α), Tendsto (fun (i : ℕ) ↦ aeSeq h'f p i x) atTop (𝓝 (aeSeqLim x))
refine_2 : g =ᶠ[ae μ] aeSeqLim
⊢ AEMeasurable g μ

Tactic:
refine ⟨aeSeqLim, measurable_of_tendsto' atTop (aeSeq.measurable h'f p)
    (tendsto_pi_nhds.mpr fun x ↦ ?_), ?_⟩
-- 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 : α
refine_1 : Tendsto (fun (i : ℕ) ↦ aeSeq h'f p i x) atTop (𝓝 (if x ∈ aeSeqSet h'f p then g x else ⋯.some))
⊢ Tendsto (fun (i : ℕ) ↦ aeSeq h'f p i x) atTop (𝓝 (aeSeqLim x))

Tactic:
unfold aeSeqLim
-- 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 : α
refine_1 :
  Tendsto (fun (i : ℕ) ↦ if x ∈ aeSeqSet h'f p then AEMeasurable.mk (f (v i)) ⋯ x else Nonempty.some ⋯) atTop
    (𝓝 (if x ∈ aeSeqSet h'f p then g x else ⋯.some))
⊢ Tendsto (fun (i : ℕ) ↦ aeSeq h'f p i x) atTop (𝓝 (if x ∈ aeSeqSet h'f p then g x else ⋯.some))

Tactic:
simp_rw [aeSeq]

Premises used: aeSeq
-- 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 : α
pos : ∀ (hx : x ∈ aeSeqSet h'f p), Tendsto (fun (i : ℕ) ↦ AEMeasurable.mk (f (v i)) ⋯ x) atTop (𝓝 (g x))
neg : ∀ (hx : x ∉ aeSeqSet h'f p), Tendsto (fun (i : ℕ) ↦ Nonempty.some ⋯) atTop (𝓝 ⋯.some)
⊢ Tendsto (fun (i : ℕ) ↦ if x ∈ aeSeqSet h'f p then AEMeasurable.mk (f (v i)) ⋯ x else Nonempty.some ⋯) atTop
    (𝓝 (if x ∈ aeSeqSet h'f p then g x else ⋯.some))

Tactic:
split_ifs with hx
-- 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
pos : Tendsto (fun (i : ℕ) ↦ f (v i) x) atTop (𝓝 (g x))
⊢ Tendsto (fun (i : ℕ) ↦ AEMeasurable.mk (f (v i)) ⋯ x) atTop (𝓝 (g x))

Tactic:
simp_rw [aeSeq.mk_eq_fun_of_mem_aeSeqSet h'f hx]

Premises used: aeSeq.mk_eq_fun_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 : ℕ) ↦ f (v i) x) atTop (𝓝 (g x))

Tactic:
aeSeq.fun_prop_of_mem_aeSeqSet h'f hx

Premises used: aeSeq.fun_prop_of_mem_aeSeqSet