awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p_1 : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ = 1
h2p : ∀ i ∈ s, p i = 0
⊢ Eq (α := ℝ≥0∞) (∏ i ∈ s, 1) (∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i)

Tactic:
apply prod_congr rfl fun i hi ↦ by rw [h2p i hi, ENNReal.rpow_zero]

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p_1 : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ = 1
h2p : ∀ i ∈ s, p i = 0
calc : ∫⁻ (a : α), f i₀ a ^ p i₀ * ∏ i ∈ s, f i a ^ p i ∂μ = ∫⁻ (a : α), f i₀ a ^ p i₀ * ∏ i ∈ s, 1 ∂μ
calc₁ : ∫⁻ (a : α), f i₀ a ^ p i₀ * ∏ i ∈ s, 1 ∂μ ≤ (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, 1
calc₂ :
  (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, 1 = (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
⊢ ∫⁻ (a : α), f i₀ a ^ p i₀ * ∏ i ∈ s, f i a ^ p i ∂μ ≤
    (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i

Tactic:
calc ∫⁻ a, f i₀ a ^ p i₀ * ∏ i ∈ s, f i a ^ p i ∂μ
          = ∫⁻ a, f i₀ a ^ p i₀ * ∏ i ∈ s, 1 ∂μ := by
            congr! 3 with x
            apply prod_congr rfl fun i hi ↦ by rw [h2p i hi, ENNReal.rpow_zero]
        _ ≤ (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, 1 := by simp [h2i₀]
        _ = (∫⁻ a, f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, (∫⁻ a, f i a ∂μ) ^ p i := by
            congr 1
            apply prod_congr rfl fun i hi ↦ by rw [h2p i hi, ENNReal.rpow_zero]

Premises used: MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
simp_rw : p i₀ ≤ 1
simp_rw₁ : p i₀ ≤ ∑ i ∈ insert i₀ s, p i
⊢ 0 ≤ 1 - p i₀

Tactic:
simp_rw [sub_nonneg, ← hp, single_le_sum h2p (mem_insert_self ..)]

Premises used: Finset.mem_insert_self, Finset.single_le_sum, sub_nonneg
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
⊢ 0 ≤ 1 - p i₀

Tactic:
have hpi₀ : 0 ≤ 1 - p i₀ := by
        simp_rw [sub_nonneg, ← hp, single_le_sum h2p (mem_insert_self ..)]
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
rwa : 1 ≠ p i₀
rwa₁ rwa₂ rwa₃ rwa₄ : p i₀ ≠ 1
⊢ 1 - p i₀ ≠ 0

Tactic:
rwa [sub_ne_zero, ne_comm]

Premises used: sub_ne_zero, ne_comm
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
⊢ 1 - p i₀ ≠ 0

Tactic:
have h2pi₀ : 1 - p i₀ ≠ 0 := by
        rwa [sub_ne_zero, ne_comm]
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : (i : ι) → ℝ := fun (i : ι) ↦ p i / (1 - p i₀)
rw : (∑ i ∈ s, p i) / (1 - p i₀) = 1
rw₁ : (∑ x ∈ insert i₀ s, p x - p i₀) / (1 - p i₀) = 1
rw₂ : (1 - p i₀) / (1 - p i₀) = 1
rw₃ rw₄ : Eq (α := ℝ) 1 1
⊢ Eq (α := ℝ) (∑ i ∈ s, q i) 1

Tactic:
rw [← Finset.sum_div, ← sum_insert_sub hi₀, hp, div_self h2pi₀]

Premises used: Finset.sum_insert_sub, Finset.sum_div, div_self
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : (i : ι) → ℝ := fun (i : ι) ↦ p i / (1 - p i₀)
⊢ Eq (α := ℝ) (∑ i ∈ s, q i) 1

Tactic:
have hq : ∑ i ∈ s, q i = 1 := by
        rw [← Finset.sum_div, ← sum_insert_sub hi₀, hp, div_self h2pi₀]
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : (i : ι) → ℝ := fun (i : ι) ↦ p i / (1 - p i₀)
hq : Eq (α := ℝ) (∑ i ∈ s, q i) 1
⊢ ∀ i ∈ s, 0 ≤ q i

Tactic:
have h2q : ∀ i ∈ s, 0 ≤ q i :=
        fun i hi ↦ div_nonneg (h2p i <| mem_insert_of_mem hi) hpi₀
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : (i : ι) → ℝ := fun (i : ι) ↦ p i / (1 - p i₀)
hq : Eq (α := ℝ) (∑ i ∈ s, q i) 1
h2q : ∀ i ∈ s, 0 ≤ q i
⊢ ∫⁻ (a : α), ∏ i ∈ insert i₀ s, f i a ^ p i ∂μ = ∫⁻ (a : α), f i₀ a ^ p i₀ * ∏ i ∈ s, f i a ^ p i ∂μ

Tactic:
simp [hi₀]
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : (i : ι) → ℝ := fun (i : ι) ↦ p i / (1 - p i₀)
hq : Eq (α := ℝ) (∑ i ∈ s, q i) 1
h2q : ∀ i ∈ s, 0 ≤ q i
⊢ ∫⁻ (a : α), f i₀ a ^ p i₀ * ∏ i ∈ s, f i a ^ p i ∂μ =
    ∫⁻ (a : α), f i₀ a ^ p i₀ * HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i a ^ q i) (1 - p i₀) ∂μ

Tactic:
simp [q, ← ENNReal.prod_rpow_of_nonneg hpi₀, ← ENNReal.rpow_mul,
              div_mul_cancel₀ (h := h2pi₀)]

Premises used: ENNReal.rpow_mul, div_mul_cancel₀, ENNReal.prod_rpow_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : (i : ι) → ℝ := fun (i : ι) ↦ p i / (1 - p i₀)
hq : Eq (α := ℝ) (∑ i ∈ s, q i) 1
h2q : ∀ i ∈ s, 0 ≤ q i
hf₁ : AEMeasurable (f i₀) μ
hg : AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ∏ i ∈ s, f i a ^ q i) μ
hp₁ : 0 ≤ p i₀
hq₁ : 0 ≤ 1 - p i₀
hpq : p i₀ + (1 - p i₀) = 1
⊢ ∫⁻ (a : α), f i₀ a ^ p i₀ * HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, f i a ^ q i) (1 - p i₀) ∂μ ≤
    (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * (∫⁻ (a : α), ∏ i ∈ s, f i a ^ q i ∂μ) ^ (1 - p i₀)

Tactic:
apply ENNReal.lintegral_mul_norm_pow_le

Premises used: ENNReal.lintegral_mul_norm_pow_le
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : (i : ι) → ℝ := fun (i : ι) ↦ p i / (1 - p i₀)
hq : Eq (α := ℝ) (∑ i ∈ s, q i) 1
h2q : ∀ i ∈ s, 0 ≤ q i
⊢ AEMeasurable (f i₀) μ

Tactic:
hf i₀ <| mem_insert_self ..

Premises used: Finset.mem_insert_self
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : (i : ι) → ℝ := fun (i : ι) ↦ p i / (1 - p i₀)
hq : Eq (α := ℝ) (∑ i ∈ s, q i) 1
h2q : ∀ i ∈ s, 0 ≤ q i
⊢ AEMeasurable (f i₀) μ

Tactic:
exact hf i₀ <| mem_insert_self ..

Premises used: Finset.mem_insert_self
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : (i : ι) → ℝ := fun (i : ι) ↦ p i / (1 - p i₀)
hq : Eq (α := ℝ) (∑ i ∈ s, q i) 1
h2q : ∀ i ∈ s, 0 ≤ q i
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ∏ i ∈ s, f i a ^ q i) μ

Tactic:
s.aemeasurable_fun_prod fun i hi ↦ (hf i <| mem_insert_of_mem hi).pow_const _

Premises used: AEMeasurable.pow_const, Finset.aemeasurable_fun_prod, Finset.mem_insert_of_mem
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : (i : ι) → ℝ := fun (i : ι) ↦ p i / (1 - p i₀)
hq : Eq (α := ℝ) (∑ i ∈ s, q i) 1
h2q : ∀ i ∈ s, 0 ≤ q i
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ∏ i ∈ s, f i a ^ q i) μ

Tactic:
exact s.aemeasurable_fun_prod fun i hi ↦ (hf i <| mem_insert_of_mem hi).pow_const _

Premises used: AEMeasurable.pow_const, Finset.aemeasurable_fun_prod, Finset.mem_insert_of_mem
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : (i : ι) → ℝ := fun (i : ι) ↦ p i / (1 - p i₀)
hq : Eq (α := ℝ) (∑ i ∈ s, q i) 1
h2q : ∀ i ∈ s, 0 ≤ q i
⊢ 0 ≤ p i₀

Tactic:
h2p i₀ <| mem_insert_self ..

Premises used: Finset.mem_insert_self
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : (i : ι) → ℝ := fun (i : ι) ↦ p i / (1 - p i₀)
hq : Eq (α := ℝ) (∑ i ∈ s, q i) 1
h2q : ∀ i ∈ s, 0 ≤ q i
⊢ 0 ≤ p i₀

Tactic:
exact h2p i₀ <| mem_insert_self ..

Premises used: Finset.mem_insert_self
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : (i : ι) → ℝ := fun (i : ι) ↦ p i / (1 - p i₀)
hq : Eq (α := ℝ) (∑ i ∈ s, q i) 1
h2q : ∀ i ∈ s, 0 ≤ q i
⊢ 0 ≤ 1 - p i₀

Tactic:
hpi₀
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : (i : ι) → ℝ := fun (i : ι) ↦ p i / (1 - p i₀)
hq : Eq (α := ℝ) (∑ i ∈ s, q i) 1
h2q : ∀ i ∈ s, 0 ≤ q i
⊢ 0 ≤ 1 - p i₀

Tactic:
exact hpi₀
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : (i : ι) → ℝ := fun (i : ι) ↦ p i / (1 - p i₀)
hq : Eq (α := ℝ) (∑ i ∈ s, q i) 1
h2q : ∀ i ∈ s, 0 ≤ q i
⊢ p i₀ + (1 - p i₀) = 1

Tactic:
apply add_sub_cancel

Premises used: add_sub_cancel
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : (i : ι) → ℝ := fun (i : ι) ↦ p i / (1 - p i₀)
hq : Eq (α := ℝ) (∑ i ∈ s, q i) 1
h2q : ∀ i ∈ s, 0 ≤ q i
bc : ∫⁻ (a : α), ∏ i ∈ s, f i a ^ q i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ q i
⊢ (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * (∫⁻ (a : α), ∏ i ∈ s, f i a ^ q i ∂μ) ^ (1 - p i₀) ≤
    (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ q i) (1 - p i₀)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : (i : ι) → ℝ := fun (i : ι) ↦ p i / (1 - p i₀)
hq : Eq (α := ℝ) (∑ i ∈ s, q i) 1
h2q : ∀ i ∈ s, 0 ≤ q i
⊢ ∫⁻ (a : α), ∏ i ∈ s, f i a ^ q i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ q i

Tactic:
ih (fun i hi ↦ hf i <| mem_insert_of_mem hi) hq h2q

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : (i : ι) → ℝ := fun (i : ι) ↦ p i / (1 - p i₀)
hq : Eq (α := ℝ) (∑ i ∈ s, q i) 1
h2q : ∀ i ∈ s, 0 ≤ q i
⊢ ∫⁻ (a : α), ∏ i ∈ s, f i a ^ q i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ q i

Tactic:
exact ih (fun i hi ↦ hf i <| mem_insert_of_mem hi) hq h2q

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : (i : ι) → ℝ := fun (i : ι) ↦ p i / (1 - p i₀)
hq : Eq (α := ℝ) (∑ i ∈ s, q i) 1
h2q : ∀ i ∈ s, 0 ≤ q i
⊢ (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * HPow.hPow (α := ℝ≥0∞) (∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ q i) (1 - p i₀) =
    (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i

Tactic:
simp [q, ← ENNReal.prod_rpow_of_nonneg hpi₀, ← ENNReal.rpow_mul,
              div_mul_cancel₀ (h := h2pi₀)]

Premises used: ENNReal.rpow_mul, div_mul_cancel₀, ENNReal.prod_rpow_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_2
ι : Type u_3
inst : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : Eq (α := ℝ) (∑ i ∈ s, p i) 1) (h2p : ∀ i ∈ s, 0 ≤ p i),
    ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : Eq (α := ℝ) (∑ i ∈ insert i₀ s, p i) 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : (i : ι) → ℝ := fun (i : ι) ↦ p i / (1 - p i₀)
hq : Eq (α := ℝ) (∑ i ∈ s, q i) 1
h2q : ∀ i ∈ s, 0 ≤ q i
⊢ (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i =
    ∏ i ∈ insert i₀ s, (∫⁻ (a : α), f i a ∂μ) ^ p i

Tactic:
simp [hi₀]