awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
m m₀ : MeasurableSpace α
μ : Measure α
g : α → E
c : E
hg : AEStronglyMeasurable g μ
⊢ AEStronglyMeasurable.{u_1, u_2} (β := 𝕜) (fun (x : α) ↦ ⟪c, g x⟫) μ

Tactic:
aestronglyMeasurable_const.inner hg

Premises used: MeasureTheory.aestronglyMeasurable_const, MeasureTheory.AEStronglyMeasurable.inner
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : MeasurableSingletonClass α
a : α
f : α → β
⊢ AEStronglyMeasurable (m₀ := m) f (Measure.dirac a)

Tactic:
⟨fun _ ↦ f a, stronglyMeasurable_const, ae_eq_dirac f⟩

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.ae_eq_dirac, And.intro, Exists.intro, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
g : α → β
γ : Type u_4
x : MeasurableSpace γ
x_1 : MeasurableSpace α
f : γ → α
μ : Measure γ
ν : Measure α
hg : AEStronglyMeasurable g ν
hf : MeasurePreserving f μ ν
⊢ AEStronglyMeasurable (g ∘ f) μ

Tactic:
hg.comp_quasiMeasurePreserving hf.quasiMeasurePreserving

Premises used: MeasureTheory.AEStronglyMeasurable.comp_quasiMeasurePreserving, MeasureTheory.MeasurePreserving.quasiMeasurePreserving
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace γ
β : Type u_4
f : α → β
mα : MeasurableSpace α
μa : Measure α
mβ : MeasurableSpace β
μb : Measure β
hf : MeasurePreserving f μa μb
h₂ : MeasurableEmbedding f
g : β → γ
rw : AEStronglyMeasurable (g ∘ f) μa ↔ AEStronglyMeasurable (m₀ := mβ) g (Measure.map f μa)
rw₁ rw₂ : AEStronglyMeasurable (g ∘ f) μa ↔ AEStronglyMeasurable (g ∘ f) μa
⊢ AEStronglyMeasurable (g ∘ f) μa ↔ AEStronglyMeasurable g μb

Tactic:
rw [← hf.map_eq, h₂.aestronglyMeasurable_map_iff]

Premises used: MeasurableEmbedding.aestronglyMeasurable_map_iff, MeasureTheory.MeasurePreserving.map_eq
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
E : Type u_5
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
⊢ AEStronglyMeasurable.{u_1, u_5} (β := E) (fun (x : α) ↦ f x • c) μ ↔ AEStronglyMeasurable f μ

Tactic:
(isClosedEmbedding_smul_left hc).isEmbedding.aestronglyMeasurable_comp_iff

Premises used: Topology.IsClosedEmbedding.isEmbedding, Topology.IsEmbedding.aestronglyMeasurable_comp_iff, isClosedEmbedding_smul_left
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_6
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
_m : MeasurableSpace α
φ : α → F →L[𝕜] E
hφ : StronglyMeasurable φ
v : F
⊢ StronglyMeasurable.{u_1, u_5} (β := E) fun (a : α) ↦ (φ a : (a : F) → E) v

Tactic:
(ContinuousLinearMap.apply 𝕜 E v).continuous.comp_stronglyMeasurable hφ

Premises used: ContinuousLinearMap.continuous, Continuous.comp_stronglyMeasurable, ContinuousLinearMap.apply, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_6
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
φ : α → F →L[𝕜] E
hφ : AEStronglyMeasurable φ μ
v : F
⊢ AEStronglyMeasurable.{u_1, u_5} (β := E) (fun (a : α) ↦ (φ a : (a : F) → E) v) μ

Tactic:
(ContinuousLinearMap.apply 𝕜 E v).continuous.comp_aestronglyMeasurable hφ

Premises used: Continuous.comp_aestronglyMeasurable, ContinuousLinearMap.continuous, ContinuousLinearMap.apply, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_6
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_7
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
L : E →L[𝕜] F →L[𝕜] G
f : α → E
g : α → F
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ AEStronglyMeasurable.{u_1, u_7} (β := G)
    (fun (x : α) ↦ (((L : (a : E) → F →L[𝕜] G) (f x) : F →L[𝕜] G) : (a : F) → G) (g x)) μ

Tactic:
L.continuous₂.comp_aestronglyMeasurable₂ hf hg

Premises used: ContinuousLinearMap.continuous₂, Continuous.comp_aestronglyMeasurable₂
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
mp :
  AEStronglyMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) →
    AEStronglyMeasurable.{u_1, u_4} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
mpr :
  AEStronglyMeasurable.{u_1, u_4} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ →
    AEStronglyMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
⊢ AEStronglyMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    AEStronglyMeasurable.{u_1, u_4} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
⊢ MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}

Tactic:
have A : MeasurableSet { x : α | f x ≠ 0 } := (hf (measurableSet_singleton 0)).compl
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
⊢ AEStronglyMeasurable.{u_1, u_4} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ

Tactic:
⟨fun x => (f x : ℝ) • g' x, hf.coe_nnreal_real.stronglyMeasurable.smul g'meas, ?_⟩

Premises used: Measurable.stronglyMeasurable, MeasureTheory.StronglyMeasurable.smul, Measurable.coe_nnreal_real, And.intro, Exists.intro, HSMul.hSMul, NNReal.toReal, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
mp : EventuallyEq.{u_1, u_4} (β := E) (ae μ) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) fun (x : α) ↦ (↑(f x) : ℝ) • g' x
⊢ AEStronglyMeasurable.{u_1, u_4} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ

Tactic:
refine ⟨fun x => (f x : ℝ) • g' x, hf.coe_nnreal_real.stronglyMeasurable.smul g'meas, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
mp :
  ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0},
    Eq.{u_4 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)
mp₁ :
  ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0}ᶜ,
    Eq.{u_4 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)
⊢ EventuallyEq.{u_1, u_4} (β := E) (ae μ) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) fun (x : α) ↦ (↑(f x) : ℝ) • g' x

Tactic:
apply @ae_of_ae_restrict_of_ae_restrict_compl _ _ _ { x | f x ≠ 0 }

Premises used: MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl, setOf, Ne, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x

Tactic:
rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal] at hg'

Premises used: Measurable.coe_nnreal_ennreal, MeasureTheory.ae_withDensity_iff, Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
hg'₁ : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
⊢ MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}

Tactic:
rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal] at hg'

Premises used: Measurable.coe_nnreal_ennreal, MeasureTheory.ae_withDensity_iff, Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
mp :
  ∀ᵐ (x : α) ∂μ,
    Membership.mem (γ := Set α) {x : α | f x ≠ 0} x →
      Eq.{u_4 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)
⊢ ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0},
    Eq.{u_4 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)

Tactic:
rw [ae_restrict_iff' A]

Premises used: MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
h : ∀ (a : α) (ha : (↑(f a) : ℝ≥0∞) ≠ 0 → g a = g' a) (h'a : f a ≠ 0), (↑(f a) : ℝ) • g a = (↑(f a) : ℝ) • g' a
⊢ ∀ᵐ (x : α) ∂μ,
    Membership.mem (γ := Set α) {x : α | f x ≠ 0} x →
      Eq.{u_4 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)

Tactic:
filter_upwards [hg'] with a ha h'a
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
a : α
ha : (↑(f a) : ℝ≥0∞) ≠ 0 → g a = g' a
h'a : f a ≠ 0
⊢ (↑(f a) : ℝ≥0∞) ≠ 0

Tactic:
simpa only [Ne, ENNReal.coe_eq_zero] using h'a

Premises used: Ne, ENNReal.coe_eq_zero
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
a : α
ha : (↑(f a) : ℝ≥0∞) ≠ 0 → g a = g' a
h'a : f a ≠ 0
⊢ (↑(f a) : ℝ≥0∞) ≠ 0

Tactic:
have : (f a : ℝ≥0∞) ≠ 0 := by simpa only [Ne, ENNReal.coe_eq_zero] using h'a
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
a : α
ha : (↑(f a) : ℝ≥0∞) ≠ 0 → g a = g' a
h'a : f a ≠ 0
this : (↑(f a) : ℝ≥0∞) ≠ 0
h h₁ : (↑(f a) : ℝ) • g' a = (↑(f a) : ℝ) • g' a
⊢ (↑(f a) : ℝ) • g a = (↑(f a) : ℝ) • g' a

Tactic:
rw [ha this]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
h : ∀ (x : α) (hx : Membership.mem (γ := Set α) {x : α | f x ≠ 0}ᶜ x), (↑(f x) : ℝ) • g x = (↑(f x) : ℝ) • g' x
⊢ ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0}ᶜ,
    Eq.{u_4 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)

Tactic:
filter_upwards [ae_restrict_mem A.compl] with x hx

Premises used: MeasureTheory.ae_restrict_mem, MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
x : α
hx : Membership.mem (γ := Set α) {x : α | f x ≠ 0}ᶜ x
⊢ f x = 0

Tactic:
simp only [Classical.not_not, mem_setOf_eq, mem_compl_iff] at hx

Premises used: Classical.not_not, Set.mem_setOf_eq, Set.mem_compl_iff
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
x : α
hx : f x = 0
⊢ (↑(f x) : ℝ) • g x = (↑(f x) : ℝ) • g' x

Tactic:
simp [hx]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
⊢ AEStronglyMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))

Tactic:
⟨fun x => (f x : ℝ)⁻¹ • g' x, hf.coe_nnreal_real.inv.stronglyMeasurable.smul g'meas, ?_⟩

Premises used: Measurable.stronglyMeasurable, MeasureTheory.StronglyMeasurable.smul, Measurable.coe_nnreal_real, Inv.inv, Measurable.inv, And.intro, Exists.intro, HSMul.hSMul, NNReal.toReal, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
mpr : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] fun (x : α) ↦ (↑(f x) : ℝ)⁻¹ • g' x
⊢ AEStronglyMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))

Tactic:
refine ⟨fun x => (f x : ℝ)⁻¹ • g' x, hf.coe_nnreal_real.inv.stronglyMeasurable.smul g'meas, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
mpr : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = (↑(f x) : ℝ)⁻¹ • g' x
⊢ g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] fun (x : α) ↦ (↑(f x) : ℝ)⁻¹ • g' x

Tactic:
rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal]

Premises used: Measurable.coe_nnreal_ennreal, MeasureTheory.ae_withDensity_iff, Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
h : ∀ (x : α) (hx : (↑(f x) : ℝ) • g x = g' x) (h'x : (↑(f x) : ℝ≥0∞) ≠ 0), g x = (↑(f x) : ℝ)⁻¹ • g' x
⊢ ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = (↑(f x) : ℝ)⁻¹ • g' x

Tactic:
filter_upwards [hg'] with x hx h'x
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
x : α
hx : (↑(f x) : ℝ) • g x = g' x
h'x : (↑(f x) : ℝ≥0∞) ≠ 0
h : (↑(f x) : ℝ) ≠ 0
⊢ g x = (↑(f x) : ℝ)⁻¹ • g' x

Tactic:
rw [← hx, smul_smul, inv_mul_cancel₀, one_smul]

Premises used: smul_smul, one_smul, inv_mul_cancel₀
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
x : α
hx : (↑(f x) : ℝ) • g x = g' x
h'x : (↑(f x) : ℝ≥0∞) ≠ 0
⊢ ¬f x = 0

Tactic:
simp only [Ne, ENNReal.coe_eq_zero] at h'x

Premises used: Ne, ENNReal.coe_eq_zero
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
x : α
hx : (↑(f x) : ℝ) • g x = g' x
h'x : ¬f x = 0
⊢ (↑(f x) : ℝ) ≠ 0

Tactic:
simpa only [NNReal.coe_eq_zero, Ne] using h'x

Premises used: NNReal.coe_eq_zero, Ne
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp
Goal:
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ let this := borel G;
  BorelSpace G

Tactic:
borelize G
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp
Goal:
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
⊢ SeparableSpace.{u_2} (↑(Set.range f ∪ {0}) : Type u_2)

Tactic:
haveI : SeparableSpace (Set.range f ∪ {0} : Set G) :=
    hf_meas.separableSpace_range_union_singleton
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp
Goal:
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
this : SeparableSpace.{u_2} (↑(Set.range f ∪ {0}) : Type u_2)
⊢ 0 ∈ Set.range f ∪ {0}

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp
Goal:
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
this : SeparableSpace.{u_2} (↑(Set.range f ∪ {0}) : Type u_2)
fs : (n : ℕ) → α →ₛ G := SimpleFunc.approxOn f ⋯ (Set.range f ∪ {0}) 0 ⋯
⊢ FinStronglyMeasurable f μ

Tactic:
⟨fs, ?_, ?_⟩

Premises used: And.intro, Exists.intro, MeasureTheory.FinStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp
Goal:
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
this : SeparableSpace.{u_2} (↑(Set.range f ∪ {0}) : Type u_2)
fs : (n : ℕ) → α →ₛ G := SimpleFunc.approxOn f ⋯ (Set.range f ∪ {0}) 0 ⋯
refine_1 :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := G) (⇑(fs n) : (a : α) → G)) : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → G) x) atTop (𝓝 (f x))
⊢ FinStronglyMeasurable f μ

Tactic:
refine ⟨fs, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp
Goal:
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
this : SeparableSpace.{u_2} (↑(Set.range f ∪ {0}) : Type u_2)
fs : (n : ℕ) → α →ₛ G := SimpleFunc.approxOn f ⋯ (Set.range f ∪ {0}) 0 ⋯
⊢ ∀ (n : ℕ), MemLp.{u_1, u_2} (ε := G) (⇑(fs n) : (a : α) → G) p μ

Tactic:
have h_fs_Lp : ∀ n, MemLp (fs n) p μ :=
      SimpleFunc.memLp_approxOn_range hf_meas.measurable hf
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp
Goal:
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
this : SeparableSpace.{u_2} (↑(Set.range f ∪ {0}) : Type u_2)
fs : (n : ℕ) → α →ₛ G := SimpleFunc.approxOn f ⋯ (Set.range f ∪ {0}) 0 ⋯
h_fs_Lp : ∀ (n : ℕ), MemLp.{u_1, u_2} (ε := G) (⇑(fs n) : (a : α) → G) p μ
⊢ ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := G) (⇑(fs n) : (a : α) → G)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
fun n => (fs n).measure_support_lt_top_of_memLp (h_fs_Lp n) hp_ne_zero hp_ne_top

Premises used: MeasureTheory.SimpleFunc.measure_support_lt_top_of_memLp
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp
Goal:
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
this : SeparableSpace.{u_2} (↑(Set.range f ∪ {0}) : Type u_2)
fs : (n : ℕ) → α →ₛ G := SimpleFunc.approxOn f ⋯ (Set.range f ∪ {0}) 0 ⋯
h_fs_Lp : ∀ (n : ℕ), MemLp.{u_1, u_2} (ε := G) (⇑(fs n) : (a : α) → G) p μ
⊢ ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := G) (⇑(fs n) : (a : α) → G)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact fun n => (fs n).measure_support_lt_top_of_memLp (h_fs_Lp n) hp_ne_zero hp_ne_top

Premises used: MeasureTheory.SimpleFunc.measure_support_lt_top_of_memLp
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp
Goal:
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this_1 : MeasurableSpace G := borel G
this_2 : BorelSpace G
this : SeparableSpace.{u_2} (↑(Set.range f ∪ {0}) : Type u_2)
fs : (n : ℕ) → α →ₛ G := SimpleFunc.approxOn f ⋯ (Set.range f ∪ {0}) 0 ⋯
x : α
refine_2 : f x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})
⊢ Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → G) x) atTop (𝓝 (f x))

Tactic:
apply SimpleFunc.tendsto_approxOn

Premises used: MeasureTheory.SimpleFunc.tendsto_approxOn