awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : (x : F) → E := fun (x : F) ↦ g (x₀ - x)
If : Integrable f μ
apply : ContinuousAt f 0
⊢ Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • f x ∂μ) atTop (𝓝 (f 0))

Tactic:
apply tendsto_integral_comp_smul_smul_of_integrable hφ h'φ h If

Premises used: tendsto_integral_comp_smul_smul_of_integrable
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : (x : F) → E := fun (x : F) ↦ g (x₀ - x)
If : Integrable f μ
⊢ ContinuousAt g (x₀ - 0)

Tactic:
simpa using h'g
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : (x : F) → E := fun (x : F) ↦ g (x₀ - x)
If : Integrable f μ
⊢ ContinuousAt g (x₀ - 0)

Tactic:
have A : ContinuousAt g (x₀ - 0) := by simpa using h'g
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : (x : F) → E := fun (x : F) ↦ g (x₀ - x)
If : Integrable f μ
A : ContinuousAt g (x₀ - 0)
⊢ ContinuousAt (X := F) (HSub.hSub x₀) 0

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : (x : F) → E := fun (x : F) ↦ g (x₀ - x)
If : Integrable f μ
A : ContinuousAt g (x₀ - 0)
⊢ ContinuousAt f 0

Tactic:
exact A.comp <| by fun_prop

Premises used: ContinuousAt.comp
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : (x : F) → E := fun (x : F) ↦ g (x₀ - x)
If : Integrable f μ
⊢ Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • f x ∂μ) atTop (𝓝 (f 0))

Tactic:
have : Tendsto (fun (c : ℝ) ↦ ∫ x, (c ^ (finrank ℝ F) * φ (c • x)) • f x ∂μ)
      atTop (𝓝 (f 0)) := by
    apply tendsto_integral_comp_smul_smul_of_integrable hφ h'φ h If
    have A : ContinuousAt g (x₀ - 0) := by simpa using h'g
    exact A.comp <| by fun_prop
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : (x : F) → E := fun (x : F) ↦ g (x₀ - x)
If : Integrable f μ
this : Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • f x ∂μ) atTop (𝓝 (f 0))
⊢ Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ) atTop (𝓝 (g x₀))

Tactic:
simp only [f, sub_zero] at this

Premises used: sub_zero
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : (x : F) → E := fun (x : F) ↦ g (x₀ - x)
If : Integrable f μ
this : Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ) atTop (𝓝 (g x₀))
⊢ Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ) atTop (𝓝 (g x₀))

Tactic:
this
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : (x : F) → E := fun (x : F) ↦ g (x₀ - x)
If : Integrable f μ
this : Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ) atTop (𝓝 (g x₀))
h₁ :
  ∀ (c : ℝ),
    Eq.{u_2 + 1} (α := E) (∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ)
      (∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ)
⊢ Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ) atTop (𝓝 (g x₀))

Tactic:
convert! this using 2 with c
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : (x : F) → E := fun (x : F) ↦ g (x₀ - x)
If : Integrable f μ
this : Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ) atTop (𝓝 (g x₀))
c : ℝ
rw : ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ + -x))) • g (x₀ - (x₀ + -x)) ∂μ
| ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ

Tactic:
rw [← integral_add_left_eq_self x₀ (μ := μ)
    (f := fun x ↦ (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x)), ← integral_neg_eq_self]

Premises used: Real, HMul.hMul, MeasureTheory.integral_add_left_eq_self, HSub.hSub, HPow.hPow, HSMul.hSMul, MeasureTheory.integral_neg_eq_self, Module.finrank
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : (x : F) → E := fun (x : F) ↦ g (x₀ - x)
If : Integrable f μ
this : Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ) atTop (𝓝 (g x₀))
c : ℝ
h₁ :
  Eq.{u_2 + 1} (α := E) (∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ)
    (∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ + -x))) • g (x₀ - (x₀ + -x)) ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ)
    (∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ)

Tactic:
conv_rhs => rw [← integral_add_left_eq_self x₀ (μ := μ)
    (f := fun x ↦ (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x)), ← integral_neg_eq_self]

Premises used: Real, HMul.hMul, MeasureTheory.integral_add_left_eq_self, HSub.hSub, HPow.hPow, HSMul.hSMul, MeasureTheory.integral_neg_eq_self, Module.finrank
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : FiniteDimensional ℝ F
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
μ : Measure F
inst_8 : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : Eq (α := ℝ) (∫ (x : F), φ x ∂μ) 1
h : Tendsto (β := ℝ) (fun (x : F) ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : (x : F) → E := fun (x : F) ↦ g (x₀ - x)
If : Integrable f μ
this : Tendsto (fun (c : ℝ) ↦ ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ) atTop (𝓝 (g x₀))
c : ℝ
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ)
    (∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ + -x))) • g (x₀ - (x₀ + -x)) ∂μ)

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
𝕜 : Type u_1
inst : NormedCommRing 𝕜
E : Fin 0 → Type u_3
mE : (i : Fin 0) → MeasurableSpace (E i)
μ : (i : Fin 0) → Measure (E i)
inst_1 : ∀ (i : Fin 0), SigmaFinite (μ i)
f : (i : Fin 0) → E i → 𝕜
hf : ∀ (i : Fin 0), Integrable (f i) (μ i)
⊢ Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin 0) → E i) ↦ ∏ i : Fin 0, f i (x i)) (Measure.pi (α := E) μ)

Tactic:
simp only [Finset.univ_eq_empty, Finset.prod_empty, isFiniteMeasure_iff,
      integrable_const_iff, pi_empty_univ, ENNReal.one_lt_top, or_true]

Premises used: Finset.prod_empty, MeasureTheory.isFiniteMeasure_iff, ENNReal.one_lt_top, Finset.univ_eq_empty, MeasureTheory.integrable_const_iff, MeasureTheory.Measure.pi_empty_univ, or_true
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
𝕜 : Type u_1
inst : NormedCommRing 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] {f : (i : Fin n) → E i → 𝕜} (hf : ∀ (i : Fin n), Integrable (f i) (μ i)),
    Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin n) → E i) ↦ ∏ i : Fin n, f i (x i)) (Measure.pi (α := E) μ)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst_1 : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
⊢ MeasurePreserving (α := E 0 × ((j : Fin n) → E (Fin.succAbove 0 j)))
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove E 0)) :
      (a : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) → (j : Fin (n + 1)) → E j)
    (Measure.prod (μ 0)
      (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
    (Measure.pi (α := E) μ)

Tactic:
have := ((measurePreserving_piFinSuccAbove μ 0).symm)
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
𝕜 : Type u_1
inst : NormedCommRing 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] {f : (i : Fin n) → E i → 𝕜} (hf : ∀ (i : Fin n), Integrable (f i) (μ i)),
    Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin n) → E i) ↦ ∏ i : Fin n, f i (x i)) (Measure.pi (α := E) μ)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst_1 : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
this :
  MeasurePreserving (α := E 0 × ((j : Fin n) → E (Fin.succAbove 0 j)))
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove E 0)) :
      (a : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) → (j : Fin (n + 1)) → E j)
    (Measure.prod (μ 0)
      (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
    (Measure.pi (α := E) μ)
succ :
  @Integrable.{u_1, u_3} 𝕜 _ _ (E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) Prod.instMeasurableSpace
    ((fun (x : (i : Fin (n + 1)) → E i) ↦ ∏ i : Fin (n + 1), f i (x i)) ∘
      (⇑(MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove E 0)) :
        (a : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) → (j : Fin (n + 1)) → E j))
    (Measure.prod (μ 0)
      (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
⊢ Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin (n + 1)) → E i) ↦ ∏ i : Fin (n + 1), f i (x i))
    (Measure.pi (α := E) μ)

Tactic:
rw [← this.integrable_comp_emb (MeasurableEquiv.measurableEmbedding _)]

Premises used: MeasurableEquiv.measurableEmbedding, MeasureTheory.MeasurePreserving.integrable_comp_emb
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
𝕜 : Type u_1
inst : NormedCommRing 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] {f : (i : Fin n) → E i → 𝕜} (hf : ∀ (i : Fin n), Integrable (f i) (μ i)),
    Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin n) → E i) ↦ ∏ i : Fin n, f i (x i)) (Measure.pi (α := E) μ)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst_1 : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
this :
  MeasurePreserving (α := E 0 × ((j : Fin n) → E (Fin.succAbove 0 j)))
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove E 0)) :
      (a : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) → (j : Fin (n + 1)) → E j)
    (Measure.prod (μ 0)
      (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
    (Measure.pi (α := E) μ)
succ :
  @Integrable.{u_1, u_3} 𝕜 _ _ (E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) Prod.instMeasurableSpace
    ((fun (x : (i : Fin (n + 1)) → E i) ↦ f 0 (x 0) * ∏ i : Fin n, f i.succ (x i.succ)) ∘
      (⇑{
            toFun := fun (f : E 0 × ((i : Fin n) → E (Fin.succAbove 0 i))) ↦
              Fin.cons (α := E) f.1 fun (j : Fin n) ↦ cast ⋯ (f.2 j),
            invFun := fun (f : (i : Fin (n + 1)) → E i) ↦ (f 0, Fin.removeNth (α := E) 0 f), left_inv := ⋯,
            right_inv := ⋯ } :
        (a : E 0 × ((i : Fin n) → E (Fin.succAbove 0 i))) → (i : Fin (n + 1)) → E i))
    (Measure.prod (μ 0)
      (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
⊢ @Integrable.{u_1, u_3} 𝕜 _ _ (E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) Prod.instMeasurableSpace
    ((fun (x : (i : Fin (n + 1)) → E i) ↦ ∏ i : Fin (n + 1), f i (x i)) ∘
      (⇑(MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove E 0)) :
        (a : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) → (j : Fin (n + 1)) → E j))
    (Measure.prod (μ 0)
      (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))

Tactic:
simp_rw [MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.insertNthEquiv,
        Fin.prod_univ_succ, Fin.insertNth_zero]

Premises used: Fin.prod_univ_succ, Fin.insertNth_zero, Fin.insertNthEquiv, MeasurableEquiv.piFinSuccAbove_symm_apply
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
𝕜 : Type u_1
inst : NormedCommRing 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] {f : (i : Fin n) → E i → 𝕜} (hf : ∀ (i : Fin n), Integrable (f i) (μ i)),
    Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin n) → E i) ↦ ∏ i : Fin n, f i (x i)) (Measure.pi (α := E) μ)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst_1 : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
this :
  MeasurePreserving (α := E 0 × ((j : Fin n) → E (Fin.succAbove 0 j)))
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove E 0)) :
      (a : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) → (j : Fin (n + 1)) → E j)
    (Measure.prod (μ 0)
      (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
    (Measure.pi (α := E) μ)
succ :
  @Integrable.{u_1, u_3} 𝕜 _ _ _ Prod.instMeasurableSpace
    (fun (x : E 0 × ((j : Fin n) → E j.succ)) ↦
      f 0
          (({ toFun := fun (f : E 0 × ((i : Fin n) → E i.succ)) ↦ Fin.cons (α := E) f.1 fun (j : Fin n) ↦ f.2 j,
                invFun := fun (f : (i : Fin (n + 1)) → E i) ↦ (f 0, Fin.removeNth (α := E) 0 f), left_inv := ⋯,
                right_inv := ⋯ : E 0 × ((i : Fin n) → E i.succ) ≃ ((i : Fin (n + 1)) → E i) } :
              (a : E 0 × ((i : Fin n) → E i.succ)) → (i : Fin (n + 1)) → E i)
            x 0) *
        ∏ i : Fin n,
          f i.succ
            (({ toFun := fun (f : E 0 × ((i : Fin n) → E i.succ)) ↦ Fin.cons (α := E) f.1 fun (j : Fin n) ↦ f.2 j,
                  invFun := fun (f : (i : Fin (n + 1)) → E i) ↦ (f 0, Fin.removeNth (α := E) 0 f), left_inv := ⋯,
                  right_inv := ⋯ } :
                (a : E 0 × ((i : Fin n) → E i.succ)) → (i : Fin (n + 1)) → E i)
              x i.succ))
    (Measure.prod (μ 0) (Measure.pi (α := fun (j : Fin n) ↦ E j.succ) fun (j : Fin n) ↦ μ j.succ))
⊢ @Integrable.{u_1, u_3} 𝕜 _ _ (E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) Prod.instMeasurableSpace
    ((fun (x : (i : Fin (n + 1)) → E i) ↦ f 0 (x 0) * ∏ i : Fin n, f i.succ (x i.succ)) ∘
      (⇑{
            toFun := fun (f : E 0 × ((i : Fin n) → E (Fin.succAbove 0 i))) ↦
              Fin.cons (α := E) f.1 fun (j : Fin n) ↦ cast ⋯ (f.2 j),
            invFun := fun (f : (i : Fin (n + 1)) → E i) ↦ (f 0, Fin.removeNth (α := E) 0 f), left_inv := ⋯,
            right_inv := ⋯ } :
        (a : E 0 × ((i : Fin n) → E (Fin.succAbove 0 i))) → (i : Fin (n + 1)) → E i))
    (Measure.prod (μ 0)
      (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))

Tactic:
simp only [Fin.zero_succAbove, cast_eq, Function.comp_def]

Premises used: Fin.zero_succAbove, Function.comp_def, cast_eq
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
𝕜 : Type u_1
inst : NormedCommRing 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] {f : (i : Fin n) → E i → 𝕜} (hf : ∀ (i : Fin n), Integrable (f i) (μ i)),
    Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin n) → E i) ↦ ∏ i : Fin n, f i (x i)) (Measure.pi (α := E) μ)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst_1 : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
this :
  MeasurePreserving (α := E 0 × ((j : Fin n) → E (Fin.succAbove 0 j)))
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove E 0)) :
      (a : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) → (j : Fin (n + 1)) → E j)
    (Measure.prod (μ 0)
      (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
    (Measure.pi (α := E) μ)
⊢ @Integrable.{u_1, u_3} 𝕜 _ _ _ (MeasurableSpace.pi (X := fun (j : Fin n) ↦ E j.succ))
    (fun (x : (j : Fin n) → E j.succ) ↦ ∏ j : Fin n, f j.succ (x j))
    (Measure.pi (α := fun (j : Fin n) ↦ E j.succ) fun (i : Fin n) ↦ μ i.succ)

Tactic:
have : Integrable (fun (x : (j : Fin n) → E (Fin.succ j)) ↦ ∏ j, f (Fin.succ j) (x j))
          (Measure.pi (fun i ↦ μ i.succ)) :=
        n_ih (fun i ↦ hf _)
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
𝕜 : Type u_1
inst : NormedCommRing 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] {f : (i : Fin n) → E i → 𝕜} (hf : ∀ (i : Fin n), Integrable (f i) (μ i)),
    Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin n) → E i) ↦ ∏ i : Fin n, f i (x i)) (Measure.pi (α := E) μ)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst_1 : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
this_1 :
  MeasurePreserving (α := E 0 × ((j : Fin n) → E (Fin.succAbove 0 j)))
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove E 0)) :
      (a : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) → (j : Fin (n + 1)) → E j)
    (Measure.prod (μ 0)
      (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
    (Measure.pi (α := E) μ)
this :
  @Integrable.{u_1, u_3} 𝕜 _ _ _ (MeasurableSpace.pi (X := fun (j : Fin n) ↦ E j.succ))
    (fun (x : (j : Fin n) → E j.succ) ↦ ∏ j : Fin n, f j.succ (x j))
    (Measure.pi (α := fun (j : Fin n) ↦ E j.succ) fun (i : Fin n) ↦ μ i.succ)
⊢ @Integrable.{u_1, u_3} 𝕜 _ _ _ Prod.instMeasurableSpace
    (fun (x : E 0 × ((j : Fin n) → E j.succ)) ↦
      f 0
          (({ toFun := fun (f : E 0 × ((i : Fin n) → E i.succ)) ↦ Fin.cons (α := E) f.1 fun (j : Fin n) ↦ f.2 j,
                invFun := fun (f : (i : Fin (n + 1)) → E i) ↦ (f 0, Fin.removeNth (α := E) 0 f), left_inv := ⋯,
                right_inv := ⋯ : E 0 × ((i : Fin n) → E i.succ) ≃ ((i : Fin (n + 1)) → E i) } :
              (a : E 0 × ((i : Fin n) → E i.succ)) → (i : Fin (n + 1)) → E i)
            x 0) *
        ∏ i : Fin n,
          f i.succ
            (({ toFun := fun (f : E 0 × ((i : Fin n) → E i.succ)) ↦ Fin.cons (α := E) f.1 fun (j : Fin n) ↦ f.2 j,
                  invFun := fun (f : (i : Fin (n + 1)) → E i) ↦ (f 0, Fin.removeNth (α := E) 0 f), left_inv := ⋯,
                  right_inv := ⋯ } :
                (a : E 0 × ((i : Fin n) → E i.succ)) → (i : Fin (n + 1)) → E i)
              x i.succ))
    (Measure.prod (μ 0) (Measure.pi (α := fun (j : Fin n) ↦ E j.succ) fun (j : Fin n) ↦ μ j.succ))

Tactic:
Integrable.mul_prod (hf 0) this

Premises used: Fin.succAbove, Eq.mpr, MeasureTheory.Integrable.mul_prod, Fin.succ, Fin.cons, Fin.induction.go, Fin.ofNat, Fin.induction, Nat.mod, Fin.cases, OfNat.ofNat, ite