awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
⊢ (lmarginal (X := A) μ s fun (x : (i : ι) → A i) ↦
      ∫⁻ (xᵢ : A i),
        HMul.hMul (β := (x : (i : ι) → A i) → ℝ≥0∞) (f ^ (1 - (↑(#s) : ℝ) * p))
          (∏ j ∈ insert i s, lmarginal (X := A) μ {j} f ^ p) (update (β := A) x i xᵢ) ∂μ i) =
    lmarginal (X := A) μ s fun (x : (i : ι) → A i) ↦
      ∫⁻ (t : A i),
        f (update (β := A) x i t) ^ (1 - (↑(#s) : ℝ) * p) *
          ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (update (β := A) x i t) ^ p ∂μ i

Tactic:
simp only [Pi.mul_apply, Pi.pow_apply, Finset.prod_apply]

Premises used: Pi.mul_apply, Finset.prod_apply, Pi.pow_apply
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
simp :
  Measurable (β := ℝ≥0∞) fun (x : (i : ι) → A i) ↦
    f x ^ (1 - (↑(#s) : ℝ) * p) * ∏ x_1 ∈ insert i s, lmarginal (X := A) μ {x_1} f x ^ p
⊢ Measurable (β := ℝ≥0∞) fun (x : (i : ι) → A i) ↦
    HMul.hMul (β := (x : (i : ι) → A i) → ℝ≥0∞) (f ^ (1 - (↑(#s) : ℝ) * p))
      (∏ j ∈ insert i s, lmarginal (X := A) μ {j} f ^ p) x

Tactic:
simp only [Pi.mul_apply, Pi.pow_apply, Finset.prod_apply]

Premises used: Pi.mul_apply, Finset.prod_apply, Pi.pow_apply
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
⊢ Measurable (β := ℝ≥0∞) fun (x : (i : ι) → A i) ↦
    f x ^ (1 - (↑(#s) : ℝ) * p) * ∏ x_1 ∈ insert i s, lmarginal (X := A) μ {x_1} f x ^ p

Tactic:
(hf.pow_const _).mul <| Finset.measurable_fun_prod _ ?_

Premises used: Measurable.mul, Finset.measurable_fun_prod, Measurable.pow_const
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
refine : ∀ i_1 ∈ insert i s, Measurable (β := ℝ≥0∞) fun (x : (i : ι) → A i) ↦ lmarginal (X := A) μ {i_1} f x ^ p
⊢ Measurable (β := ℝ≥0∞) fun (x : (i : ι) → A i) ↦
    f x ^ (1 - (↑(#s) : ℝ) * p) * ∏ x_1 ∈ insert i s, lmarginal (X := A) μ {x_1} f x ^ p

Tactic:
refine (hf.pow_const _).mul <| Finset.measurable_fun_prod _ ?_

Premises used: Measurable.mul, Finset.measurable_fun_prod, Measurable.pow_const
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
⊢ ∀ i_1 ∈ insert i s, Measurable (β := ℝ≥0∞) fun (x : (i : ι) → A i) ↦ lmarginal (X := A) μ {i_1} f x ^ p

Tactic:
fun _ _ ↦ hf.lmarginal μ |>.pow_const _

Premises used: Measurable.lmarginal, Measurable.pow_const
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
⊢ ∀ i_1 ∈ insert i s, Measurable (β := ℝ≥0∞) fun (x : (i : ι) → A i) ↦ lmarginal (X := A) μ {i_1} f x ^ p

Tactic:
exact fun _ _ ↦ hf.lmarginal μ |>.pow_const _

Premises used: Measurable.lmarginal, Measurable.pow_const
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
⊢ (lmarginal (X := A) μ s fun (x : (i : ι) → A i) ↦
      ∫⁻ (t : A i),
        f (update (β := A) x i t) ^ (1 - (↑(#s) : ℝ) * p) *
          ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (update (β := A) x i t) ^ p ∂μ i) ≤
    T (A := A) μ p (lmarginal (X := A) μ {i} f) s

Tactic:
lmarginal_mono (s := s) (fun x ↦ ?_)

Premises used: MeasureTheory.GridLines.T, MeasureTheory.lmarginal_mono
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
calc :
  ∀ (x : (i : ι) → A i),
    ∫⁻ (t : A i),
        f (update (β := A) x i t) ^ (1 - (↑(#s) : ℝ) * p) *
          ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (update (β := A) x i t) ^ p ∂μ i ≤
      HMul.hMul (β := (x : (i : ι) → A i) → ℝ≥0∞)
        (lmarginal (X := A) μ {i} f ^ (1 - HSub.hSub (α := ℝ) (↑(#s) : ℝ) 1 * p))
        (∏ i_1 ∈ s, lmarginal (X := A) μ {i_1} (lmarginal (X := A) μ {i} f) ^ p) x
⊢ T (A := A) μ p f (insert i s) ≤ T (A := A) μ p (lmarginal (X := A) μ {i} f) s

Tactic:
calc T μ p f (insert i s)
      = ∫⋯∫⁻_insert i s,
            f ^ (1 - (s.card : ℝ) * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) ^ p ∂μ := by
          -- unfold `T` and reformulate the exponents
          simp_rw [T, card_insert_of_notMem hi]
          congr!
          push_cast
          ring
    _ = ∫⋯∫⁻_s, (fun x ↦ ∫⁻ (t : A i),
            (f (update x i t) ^ (1 - (s.card : ℝ) * p)
            * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) (update x i t) ^ p) ∂(μ i)) ∂μ := by
          -- pull out the integral over `xᵢ`
          rw [lmarginal_insert' _ _ hi]
          · simp only [Pi.mul_apply, Pi.pow_apply, Finset.prod_apply]
          · change Measurable (fun x ↦ _)
            simp only [Pi.mul_apply, Pi.pow_apply, Finset.prod_apply]
            refine (hf.pow_const _).mul <| Finset.measurable_fun_prod _ ?_
            exact fun _ _ ↦ hf.lmarginal μ |>.pow_const _
    _ ≤ T μ p (∫⋯∫⁻_{i}, f ∂μ) s := lmarginal_mono (s := s) (fun x ↦ ?_)

Premises used: MeasureTheory.GridLines.T, Function.update, HMul.hMul, HSub.hSub, Insert.insert, Nat.cast, Finset.prod, HPow.hPow, MeasureTheory.lmarginal, Finset.card, Singleton.singleton, OfNat.ofNat, MeasureTheory.lintegral, MeasureTheory.lmarginal_mono
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
simp :
  ∫⁻ (t : A i),
      f (update (β := A) x i t) ^ (1 - (↑(#s) : ℝ) * p) *
        ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (update (β := A) x i t) ^ p ∂μ i ≤
    lmarginal (X := A) μ {i} f x ^ (1 - HSub.hSub (α := ℝ) (↑(#s) : ℝ) 1 * p) *
      ∏ x_1 ∈ s, lmarginal (X := A) μ {x_1} (lmarginal (X := A) μ {i} f) x ^ p
⊢ ∫⁻ (t : A i),
      f (update (β := A) x i t) ^ (1 - (↑(#s) : ℝ) * p) *
        ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (update (β := A) x i t) ^ p ∂μ i ≤
    HMul.hMul (β := (x : (i : ι) → A i) → ℝ≥0∞)
      (lmarginal (X := A) μ {i} f ^ (1 - HSub.hSub (α := ℝ) (↑(#s) : ℝ) 1 * p))
      (∏ i_1 ∈ s, lmarginal (X := A) μ {i_1} (lmarginal (X := A) μ {i} f) ^ p) x

Tactic:
simp only [Pi.mul_apply, Pi.pow_apply, Finset.prod_apply]

Premises used: Pi.mul_apply, Finset.prod_apply, Pi.pow_apply
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
set :
  let X := update (β := A) x i;
  ∫⁻ (t : A i), f (X t) ^ (1 - (↑(#s) : ℝ) * p) * ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i ≤
    lmarginal (X := A) μ {i} f x ^ (1 - HSub.hSub (α := ℝ) (↑(#s) : ℝ) 1 * p) *
      ∏ x_1 ∈ s, lmarginal (X := A) μ {x_1} (lmarginal (X := A) μ {i} f) x ^ p
⊢ ∫⁻ (t : A i),
      f (update (β := A) x i t) ^ (1 - (↑(#s) : ℝ) * p) *
        ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (update (β := A) x i t) ^ p ∂μ i ≤
    lmarginal (X := A) μ {i} f x ^ (1 - HSub.hSub (α := ℝ) (↑(#s) : ℝ) 1 * p) *
      ∏ x_1 ∈ s, lmarginal (X := A) μ {x_1} (lmarginal (X := A) μ {i} f) x ^ p

Tactic:
set X := update x i

Premises used: Function.update
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
⊢ ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)

Tactic:
have hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t) :=
    fun {_} ↦ hf.lmarginal μ |>.comp <| measurable_update _
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
⊢ Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)

Tactic:
have hF₀ : Measurable fun t ↦ f (X t) := hf.comp <| measurable_update _
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
linarith : 1 - k * p < 0 → 1 - k * p - 0 + ((↑(#s) : ℝ) * p - 1) = 0
⊢ 0 ≤ 1 - k * p

Tactic:
linarith only [hp]
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
⊢ 0 ≤ 1 - k * p

Tactic:
have hk' : 0 ≤ 1 - k * p := by linarith only [hp]
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
clear_value :
  ∀ (X : (v : A i) → (a : ι) → A a)
    (hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t))
    (hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)),
    let k : ℝ := (↑(#s) : ℝ);
    ∀ (hk' : 0 ≤ 1 - k * p),
      ∫⁻ (t : A i), f (X t) ^ (1 - k * p) * ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i =
        ∫⁻ (t : A i),
          lmarginal (X := A) μ {i} f (X t) ^ p *
            (f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p) ∂μ i
⊢ ∫⁻ (t : A i), f (X t) ^ (1 - k * p) * ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i =
    ∫⁻ (t : A i),
      lmarginal (X := A) μ {i} f (X t) ^ p *
        (f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p) ∂μ i

Tactic:
clear_value X
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
h :
  ∀ (t : A i),
    f (X t) ^ (1 - k * p) * ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (X t) ^ p =
      lmarginal (X := A) μ {i} f (X t) ^ p * (f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p)
⊢ ∫⁻ (t : A i), f (X t) ^ (1 - k * p) * ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i =
    ∫⁻ (t : A i),
      lmarginal (X := A) μ {i} f (X t) ^ p *
        (f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p) ∂μ i

Tactic:
congr! 2 with t
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
t : A i
h :
  f (X t) ^ (1 - k * p) * (lmarginal (X := A) μ {i} f (X t) ^ p * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p) =
    lmarginal (X := A) μ {i} f (X t) ^ p * (f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p)
⊢ f (X t) ^ (1 - k * p) * ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (X t) ^ p =
    lmarginal (X := A) μ {i} f (X t) ^ p * (f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p)

Tactic:
simp_rw [prod_insert hi]

Premises used: Finset.prod_insert
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
t : A i
⊢ f (X t) ^ (1 - k * p) * (lmarginal (X := A) μ {i} f (X t) ^ p * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p) =
    lmarginal (X := A) μ {i} f (X t) ^ p * (f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
t : A i
hi₁ : Membership.mem (γ := Finset ι) {i} i
⊢ lmarginal (X := A) μ {i} f (X t) = lmarginal (X := A) μ {i} f x

Tactic:
rw [lmarginal_update_of_mem]

Premises used: MeasureTheory.lmarginal_update_of_mem
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
t : A i
⊢ Membership.mem (γ := Finset ι) {i} i

Tactic:
Iff.mpr Finset.mem_singleton rfl

Premises used: Iff.mpr, Finset.mem_singleton, rfl
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
t : A i
⊢ Membership.mem (γ := Finset ι) {i} i

Tactic:
exact Iff.mpr Finset.mem_singleton rfl

Premises used: Iff.mpr, Finset.mem_singleton, rfl
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
⊢ ∀ (t : A i), lmarginal (X := A) μ {i} f (X t) = lmarginal (X := A) μ {i} f x

Tactic:
have : ∀ t, (∫⋯∫⁻_{i}, f ∂μ) (X t) = (∫⋯∫⁻_{i}, f ∂μ) x := by
                intro t
                rw [lmarginal_update_of_mem]
                exact Iff.mpr Finset.mem_singleton rfl
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
this : ∀ (t : A i), lmarginal (X := A) μ {i} f (X t) = lmarginal (X := A) μ {i} f x
simp_rw :
  ∫⁻ (t : A i),
      lmarginal (X := A) μ {i} f x ^ p * (f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p) ∂μ i =
    lmarginal (X := A) μ {i} f x ^ p *
      ∫⁻ (t : A i), f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i
⊢ ∫⁻ (t : A i),
      lmarginal (X := A) μ {i} f (X t) ^ p *
        (f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p) ∂μ i =
    lmarginal (X := A) μ {i} f x ^ p *
      ∫⁻ (t : A i), f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i

Tactic:
simp_rw [this]
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
this : ∀ (t : A i), lmarginal (X := A) μ {i} f (X t) = lmarginal (X := A) μ {i} f x
hf₁ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p
⊢ ∫⁻ (t : A i),
      lmarginal (X := A) μ {i} f x ^ p * (f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p) ∂μ i =
    lmarginal (X := A) μ {i} f x ^ p *
      ∫⁻ (t : A i), f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i

Tactic:
rw [lintegral_const_mul]

Premises used: MeasureTheory.lintegral_const_mul
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
this : ∀ (t : A i), lmarginal (X := A) μ {i} f (X t) = lmarginal (X := A) μ {i} f x
⊢ Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p

Tactic:
(hF₀.pow_const _).mul <| Finset.measurable_fun_prod _ fun _ _ ↦ hF₁.pow_const _

Premises used: Measurable.mul, Finset.measurable_fun_prod, Measurable.pow_const
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
this : ∀ (t : A i), lmarginal (X := A) μ {i} f (X t) = lmarginal (X := A) μ {i} f x
⊢ Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p

Tactic:
exact (hF₀.pow_const _).mul <| Finset.measurable_fun_prod _ fun _ _ ↦ hF₁.pow_const _

Premises used: Measurable.mul, Finset.measurable_fun_prod, Measurable.pow_const