awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : DecidableEq ι
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : Finset ι
f : ((i : ι) → X i) → E
mf : StronglyMeasurable f
x : (i : ι) → X i
g : ((i : ↥s) → X (↑i : ι)) → E := fun (y : (i : ↥s) → X (↑i : ι)) ↦ f (Function.updateFinset (π := X) x s y)
this : ∀ (y : (i : ι) → X i), g (s.restrict (π := X) y) = f y
⊢ AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := fun (i : ↥s) ↦ X (↑i : ι))) g
    (Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι))

Tactic:
mf.comp_measurable (measurable_updateFinset.mono le_rfl (piFinset.le s))
    |>.aestronglyMeasurable

Premises used: le_rfl, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.Filtration.piFinset, measurable_updateFinset, MeasureTheory.StronglyMeasurable.comp_measurable, MeasureTheory.Filtration.le, Measurable.mono
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : DecidableEq ι
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : Finset ι
f : ((i : ι) → X i) → E
mf : StronglyMeasurable f
x : (i : ι) → X i
g : ((i : ↥s) → X (↑i : ι)) → E := fun (y : (i : ↥s) → X (↑i : ι)) ↦ f (Function.updateFinset (π := X) x s y)
this : ∀ (y : (i : ι) → X i), g (s.restrict (π := X) y) = f y
⊢ AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := fun (i : ↥s) ↦ X (↑i : ι))) g
    (Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι))

Tactic:
exact mf.comp_measurable (measurable_updateFinset.mono le_rfl (piFinset.le s))
    |>.aestronglyMeasurable

Premises used: le_rfl, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.Filtration.piFinset, measurable_updateFinset, MeasureTheory.StronglyMeasurable.comp_measurable, MeasureTheory.Filtration.le, Measurable.mono
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : DecidableEq ι
s : Finset ι
f : ((i : ι) → X i) → ℝ≥0∞
mf : Measurable f
x : (i : ι) → X i
g : ((i : ↥s) → X (↑i : ι)) → ℝ≥0∞ := fun (y : (i : ↥s) → X (↑i : ι)) ↦ f (Function.updateFinset (π := X) x s y)
y : (i : ι) → X i
i : ι
hi : i ∈ (↑s : Set ι)
⊢ Function.updateFinset (π := X) x s (s.restrict (π := X) y) i = y i

Tactic:
simp_all [Function.updateFinset]

Premises used: Function.updateFinset
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : DecidableEq ι
s : Finset ι
f : ((i : ι) → X i) → ℝ≥0∞
mf : Measurable f
x : (i : ι) → X i
g : ((i : ↥s) → X (↑i : ι)) → ℝ≥0∞ := fun (y : (i : ↥s) → X (↑i : ι)) ↦ f (Function.updateFinset (π := X) x s y)
⊢ ∀ (y : (i : ι) → X i), g (s.restrict (π := X) y) = f y

Tactic:
have this y : g (s.restrict y) = f y :=
    mf.dependsOn_of_piFinset fun i hi ↦ by simp_all [Function.updateFinset]
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : DecidableEq ι
s : Finset ι
f : ((i : ι) → X i) → ℝ≥0∞
mf : Measurable f
x : (i : ι) → X i
g : ((i : ↥s) → X (↑i : ι)) → ℝ≥0∞ := fun (y : (i : ↥s) → X (↑i : ι)) ↦ f (Function.updateFinset (π := X) x s y)
this : ∀ (y : (i : ι) → X i), g (s.restrict (π := X) y) = f y
rw :
  (∫⁻ (y : (i : ↥s) → X (↑i : ι)), g y ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι)) =
    lmarginal (X := X) μ s f x
hf : Measurable g
⊢ ∫⁻ (y : (i : ι) → X i), f y ∂infinitePi (X := X) μ = lmarginal (X := X) μ s f x

Tactic:
rw [← lintegral_congr_ae <| ae_of_all _ this, lintegral_restrict_infinitePi]

Premises used: MeasureTheory.lintegral_restrict_infinitePi, MeasureTheory.lintegral_congr_ae, MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : DecidableEq ι
s : Finset ι
f : ((i : ι) → X i) → ℝ≥0∞
mf : Measurable f
x : (i : ι) → X i
g : ((i : ↥s) → X (↑i : ι)) → ℝ≥0∞ := fun (y : (i : ↥s) → X (↑i : ι)) ↦ f (Function.updateFinset (π := X) x s y)
this : ∀ (y : (i : ι) → X i), g (s.restrict (π := X) y) = f y
⊢ (∫⁻ (y : (i : ↥s) → X (↑i : ι)), g y ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι)) =
    lmarginal (X := X) μ s f x

Tactic:
rfl
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : DecidableEq ι
s : Finset ι
f : ((i : ι) → X i) → ℝ≥0∞
mf : Measurable f
x : (i : ι) → X i
g : ((i : ↥s) → X (↑i : ι)) → ℝ≥0∞ := fun (y : (i : ↥s) → X (↑i : ι)) ↦ f (Function.updateFinset (π := X) x s y)
this : ∀ (y : (i : ι) → X i), g (s.restrict (π := X) y) = f y
⊢ Measurable g

Tactic:
mf.comp (measurable_updateFinset.mono le_rfl (piFinset.le s))

Premises used: le_rfl, Measurable.comp, MeasureTheory.Filtration.piFinset, measurable_updateFinset, MeasureTheory.Filtration.le, Measurable.mono
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : DecidableEq ι
s : Finset ι
f : ((i : ι) → X i) → ℝ≥0∞
mf : Measurable f
x : (i : ι) → X i
g : ((i : ↥s) → X (↑i : ι)) → ℝ≥0∞ := fun (y : (i : ↥s) → X (↑i : ι)) ↦ f (Function.updateFinset (π := X) x s y)
this : ∀ (y : (i : ι) → X i), g (s.restrict (π := X) y) = f y
⊢ Measurable g

Tactic:
exact mf.comp (measurable_updateFinset.mono le_rfl (piFinset.le s))

Premises used: le_rfl, Measurable.comp, MeasureTheory.Filtration.piFinset, measurable_updateFinset, MeasureTheory.Filtration.le, Measurable.mono
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
apply : AEStronglyMeasurable (m₀ := Real.measurableSpace) ((Set.Ioc (-A) A).indicator id) (Measure.map f μ)
⊢ AEStronglyMeasurable (ProbabilityTheory.truncation f A) μ

Tactic:
apply AEStronglyMeasurable.comp_aemeasurable _ hf.aemeasurable

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.AEStronglyMeasurable.comp_aemeasurable
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
⊢ AEStronglyMeasurable (m₀ := Real.measurableSpace) ((Set.Ioc (-A) A).indicator id) (Measure.map f μ)

Tactic:
(stronglyMeasurable_id.indicator measurableSet_Ioc).aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, stronglyMeasurable_id, MeasureTheory.StronglyMeasurable.indicator, measurableSet_Ioc
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
⊢ AEStronglyMeasurable (m₀ := Real.measurableSpace) ((Set.Ioc (-A) A).indicator id) (Measure.map f μ)

Tactic:
exact (stronglyMeasurable_id.indicator measurableSet_Ioc).aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, stronglyMeasurable_id, MeasureTheory.StronglyMeasurable.indicator, measurableSet_Ioc
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
simp : |if f x ∈ Set.Ioc (-A) A then f x else 0| ≤ |A|
⊢ |truncation f A x| ≤ |A|

Tactic:
simp only [truncation, Set.indicator, id, Function.comp_apply]

Premises used: Set.indicator, id, Function.comp_apply, ProbabilityTheory.truncation
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
pos : ∀ (h : f x ∈ Set.Ioc (-A) A), |f x| ≤ |A|
neg : ∀ (h : f x ∉ Set.Ioc (-A) A), |0| ≤ |A|
⊢ |if f x ∈ Set.Ioc (-A) A then f x else 0| ≤ |A|

Tactic:
split_ifs with h
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : f x ∈ Set.Ioc (-A) A
⊢ |f x| ≤ |A|

Tactic:
abs_le_abs h.2 (neg_le.2 h.1.le)

Premises used: Iff.mpr, neg_le, LT.lt.le, And.right, And.left, abs_le_abs
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : f x ∈ Set.Ioc (-A) A
⊢ |f x| ≤ |A|

Tactic:
exact abs_le_abs h.2 (neg_le.2 h.1.le)

Premises used: Iff.mpr, neg_le, LT.lt.le, And.right, And.left, abs_le_abs
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : f x ∉ Set.Ioc (-A) A
⊢ |0| ≤ |A|

Tactic:
simp [abs_nonneg]

Premises used: abs_nonneg
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
simp : Eq (α := α → ℝ) ((fun (x : ℝ) ↦ 0) ∘ f) 0
⊢ truncation f 0 = 0

Tactic:
simp [truncation]

Premises used: ProbabilityTheory.truncation
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
⊢ Eq (α := α → ℝ) ((fun (x : ℝ) ↦ 0) ∘ f) 0

Tactic:
rfl
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
simp : |if f x ∈ Set.Ioc (-A) A then f x else 0| ≤ |f x|
⊢ |truncation f A x| ≤ |f x|

Tactic:
simp only [truncation, indicator, id, Function.comp_apply]

Premises used: Set.indicator, id, Function.comp_apply, ProbabilityTheory.truncation
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
pos : f x ∈ Set.Ioc (-A) A → |f x| ≤ |f x|
neg : f x ∉ Set.Ioc (-A) A → |0| ≤ |f x|
⊢ |if f x ∈ Set.Ioc (-A) A then f x else 0| ≤ |f x|

Tactic:
split_ifs
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : f x ∈ Set.Ioc (-A) A
⊢ |f x| ≤ |f x|

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : f x ∈ Set.Ioc (-A) A
⊢ |f x| ≤ |f x|

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : f x ∉ Set.Ioc (-A) A
⊢ |0| ≤ |f x|

Tactic:
simp [abs_nonneg]

Premises used: abs_nonneg
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : |f x| < A
simp : f x ∉ Set.Ioc (-A) A → 0 = f x
⊢ truncation f A x = f x

Tactic:
simp only [truncation, indicator, id, Function.comp_apply, ite_eq_left_iff]

Premises used: ite_eq_left_iff, Set.indicator, id, Function.comp_apply, ProbabilityTheory.truncation
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : |f x| < A
H : f x ∉ Set.Ioc (-A) A
apply : f x ∈ Set.Ioc (-A) A
⊢ 0 = f x

Tactic:
apply H.elim

Premises used: Not.elim
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : |f x| < A
H : f x ∉ Set.Ioc (-A) A
⊢ f x ∈ Set.Ioc (-A) A

Tactic:
simp [(abs_lt.1 h).1, (abs_lt.1 h).2.le]

Premises used: LT.lt.le, And.right, And.left, Iff.mp, abs_lt
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
h₁ : ∀ (x : α), truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x
⊢ truncation f A = (Set.Ioc 0 A).indicator id ∘ f

Tactic:
ext x
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
h₁ : ∀ (hx : 0 < f x), truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x
h₂ : ∀ (hx : 0 = f x), truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x
⊢ truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x

Tactic:
rcases (h x).lt_or_eq with (hx | hx)

Premises used: LE.le.lt_or_eq
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
h₁ : (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0
⊢ truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x

Tactic:
simp only [truncation, indicator, hx, Set.mem_Ioc, id, Function.comp_apply]

Premises used: Set.indicator, id, Set.mem_Ioc, Function.comp_apply, ProbabilityTheory.truncation
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
pos : ∀ (h'x : f x ≤ A), (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0
neg : ∀ (h'x : ¬f x ≤ A), (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0
⊢ (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0

Tactic:
by_cases h'x : f x ≤ A
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
h'x : f x ≤ A
linarith : f x ≤ -A → 2 * (0 - f x) + (f x - A) + (f x - -A) = 0
linarith₁ : f x ≤ -A → GT.gt (α := ℝ) 2 0
⊢ -A < f x

Tactic:
linarith [h x]
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
h'x : f x ≤ A
⊢ -A < f x

Tactic:
have : -A < f x := by linarith [h x]
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
h'x : f x ≤ A
this : -A < f x
⊢ (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0

Tactic:
simp only [this, true_and]

Premises used: true_and
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
h'x : ¬f x ≤ A
⊢ (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0

Tactic:
simp only [h'x, and_false]

Premises used: and_false
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 = f x
⊢ truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x

Tactic:
simp only [truncation, indicator, hx, id, Function.comp_apply, ite_self]

Premises used: Set.indicator, ite_self, id, Function.comp_apply, ProbabilityTheory.truncation
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : 0 ≤ f x
⊢ 0 ≤ truncation f A x

Tactic:
Set.indicator_apply_nonneg fun _ => h

Premises used: Set.indicator, ProbabilityTheory.truncation, Set.indicator_apply_nonneg, ite
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
A : ℝ
p : ℝ≥0∞
⊢ MemLp (truncation f A) p μ

Tactic:
MemLp.of_bound hf.truncation |A| (Eventually.of_forall fun _ => abs_truncation_le_bound _ _ _)

Premises used: abs, ProbabilityTheory.abs_truncation_le_bound, Filter.Eventually.of_forall, MeasureTheory.AEStronglyMeasurable.truncation, MeasureTheory.MemLp.of_bound
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
A : ℝ
rw : MemLp (truncation f A) 1 μ
⊢ Integrable (truncation f A) μ

Tactic:
rw [← memLp_one_iff_integrable]

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
A : ℝ
⊢ MemLp (truncation f A) 1 μ

Tactic:
hf.memLp_truncation

Premises used: MeasureTheory.AEStronglyMeasurable.memLp_truncation
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
A : ℝ
⊢ MemLp (truncation f A) 1 μ

Tactic:
exact hf.memLp_truncation

Premises used: MeasureTheory.AEStronglyMeasurable.memLp_truncation
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
⊢ MeasurableSet (Set.Ioc (-A) A)

Tactic:
have M : MeasurableSet (Set.Ioc (-A) A) := measurableSet_Ioc
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (y : ℝ) ↦ (Set.Ioc (-A) A).indicator id y ^ n)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (x : ℝ) ↦
      (Set.Ioc (-A) A).indicator (fun (x : ℝ) ↦ x ^ n) x)
rw₁ : -A ≤ A
rw₂ :
  AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (z : ℝ) ↦ (Set.Ioc (-A) A).indicator id z ^ n)
    (Measure.map f μ)
⊢ Eq (α := ℝ) (∫ (x : α), (fun (z : ℝ) ↦ (Set.Ioc (-A) A).indicator id z ^ n) (f x) ∂μ)
    (∫ (y : ℝ) in -A..A, y ^ n ∂Measure.map f μ)

Tactic:
rw [← integral_map (f := fun z => _ ^ n) hf.aemeasurable, intervalIntegral.integral_of_le,
    ← integral_indicator M]

Premises used: MeasureTheory.integral_indicator, MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.integral_map, intervalIntegral.integral_of_le
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (y : ℝ) ↦ (Set.Ioc (-A) A).indicator id y ^ n)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (x : ℝ) ↦
      (Set.Ioc (-A) A).indicator (fun (x : ℝ) ↦ x ^ n) x)

Tactic:
simp only [indicator, zero_pow hn, id, ite_pow]

Premises used: Set.indicator, ite_pow, id, zero_pow
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
linarith : A < -A → 2 * (0 - A) + (A - -A) = 0
linarith₁ : A < -A → GT.gt (α := ℝ) 2 0
⊢ -A ≤ A

Tactic:
linarith
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (z : ℝ) ↦ (Set.Ioc (-A) A).indicator id z ^ n)
    (Measure.map f μ)

Tactic:
((measurable_id.indicator M).pow_const n).aestronglyMeasurable

Premises used: measurable_id, Measurable.aestronglyMeasurable, Measurable.indicator, Measurable.pow_const
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (z : ℝ) ↦ (Set.Ioc (-A) A).indicator id z ^ n)
    (Measure.map f μ)

Tactic:
exact ((measurable_id.indicator M).pow_const n).aestronglyMeasurable

Premises used: measurable_id, Measurable.aestronglyMeasurable, Measurable.indicator, Measurable.pow_const
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
⊢ MeasurableSet (Set.Ioc 0 A)

Tactic:
have M : MeasurableSet (Set.Ioc 0 A) := measurableSet_Ioc
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
⊢ MeasurableSet (Set.Ioc A 0)

Tactic:
have M' : MeasurableSet (Set.Ioc A 0) := measurableSet_Ioc
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
rw : Eq (α := ℝ) (∫ (x : α), ((Set.Ioc 0 A).indicator id ∘ f) x ^ n ∂μ) (∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ)
⊢ Eq (α := ℝ) (∫ (x : α), truncation f A x ^ n ∂μ) (∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ)

Tactic:
rw [truncation_eq_of_nonneg h'f]

Premises used: ProbabilityTheory.truncation_eq_of_nonneg
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
inl :
  ∀ (hA : 0 ≤ A),
    Eq (α := ℝ) (∫ (x : α), (fun (z : ℝ) ↦ (Set.Ioc 0 A).indicator id z ^ n) (f x) ∂μ)
      (∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ)
inr :
  ∀ (hA : A < 0),
    Eq (α := ℝ) (∫ (x : α), (fun (z : ℝ) ↦ (Set.Ioc 0 A).indicator id z ^ n) (f x) ∂μ)
      (∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ)
⊢ Eq (α := ℝ) (∫ (x : α), (fun (z : ℝ) ↦ (Set.Ioc 0 A).indicator id z ^ n) (f x) ∂μ)
    (∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ)

Tactic:
rcases le_or_gt 0 A with (hA | hA)

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : 0 ≤ A
inl :
  Eq (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (y : ℝ) ↦ (Set.Ioc 0 A).indicator id y ^ n)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (x : ℝ) ↦
      (Set.Ioc 0 A).indicator (fun (x : ℝ) ↦ x ^ n) x)
inl₁ :
  AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (z : ℝ) ↦ (Set.Ioc 0 A).indicator id z ^ n)
    (Measure.map f μ)
⊢ Eq (α := ℝ) (∫ (x : α), (fun (z : ℝ) ↦ (Set.Ioc 0 A).indicator id z ^ n) (f x) ∂μ)
    (∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ)

Tactic:
rw [← integral_map (f := fun z => _ ^ n) hf.aemeasurable, intervalIntegral.integral_of_le hA,
      ← integral_indicator M]

Premises used: MeasureTheory.integral_indicator, MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.integral_map, intervalIntegral.integral_of_le
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : 0 ≤ A
⊢ Eq (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (y : ℝ) ↦ (Set.Ioc 0 A).indicator id y ^ n)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (x : ℝ) ↦
      (Set.Ioc 0 A).indicator (fun (x : ℝ) ↦ x ^ n) x)

Tactic:
simp only [indicator, zero_pow hn, id, ite_pow]

Premises used: Set.indicator, ite_pow, id, zero_pow
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : 0 ≤ A
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (z : ℝ) ↦ (Set.Ioc 0 A).indicator id z ^ n)
    (Measure.map f μ)

Tactic:
((measurable_id.indicator M).pow_const n).aestronglyMeasurable

Premises used: measurable_id, Measurable.aestronglyMeasurable, Measurable.indicator, Measurable.pow_const
-- Module: Mathlib.Probability.StrongLaw
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : 0 ≤ A
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (z : ℝ) ↦ (Set.Ioc 0 A).indicator id z ^ n)
    (Measure.map f μ)

Tactic:
exact ((measurable_id.indicator M).pow_const n).aestronglyMeasurable

Premises used: measurable_id, Measurable.aestronglyMeasurable, Measurable.indicator, Measurable.pow_const