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
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
bc :
  ∫⁻ (t : A i), f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i ≤
    (∫⁻ (t : A i), f (X t) ∂μ i) ^ (1 - k * p) * ∏ j ∈ s, (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ p
⊢ 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 ≤
    lmarginal (X := A) μ {i} f x ^ p *
      ((∫⁻ (t : A i), f (X t) ∂μ i) ^ (1 - k * p) * ∏ j ∈ s, (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ p)

Tactic:
gcongr
-- 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
bc : AEMeasurable (β := ℝ≥0∞) (fun (a : A i) ↦ f (X a)) (μ i)
bc₁ : ∀ i_1 ∈ s, AEMeasurable (β := ℝ≥0∞) (fun (a : A i) ↦ lmarginal (X := A) μ {i_1} f (X a)) (μ i)
bc₂ : 1 - k * p + ∑ i ∈ s, p = 1
bc₃ : 0 ≤ 1 - k * p
bc₄ : ∀ i ∈ s, 0 ≤ p
⊢ ∫⁻ (t : A i), f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i ≤
    (∫⁻ (t : A i), f (X t) ∂μ i) ^ (1 - k * p) * ∏ j ∈ s, (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ p

Tactic:
apply ENNReal.lintegral_mul_prod_norm_pow_le

Premises used: ENNReal.lintegral_mul_prod_norm_pow_le
-- 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
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : A i) ↦ f (X a)) (μ i)

Tactic:
hF₀.aemeasurable

Premises used: Measurable.aemeasurable
-- 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
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : A i) ↦ f (X a)) (μ i)

Tactic:
exact hF₀.aemeasurable

Premises used: Measurable.aemeasurable
-- 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
i_1 : ι
h : i_1 ∈ s
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : A i) ↦ lmarginal (X := A) μ {i_1} f (X a)) (μ i)

Tactic:
hF₁.aemeasurable

Premises used: Measurable.aemeasurable
-- 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
i_1 : ι
h : i_1 ∈ s
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : A i) ↦ lmarginal (X := A) μ {i_1} f (X a)) (μ i)

Tactic:
exact hF₁.aemeasurable

Premises used: Measurable.aemeasurable
-- 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
bc : 1 - k * p + (↑(#s) : ℝ) * p = 1
⊢ 1 - k * p + ∑ i ∈ s, p = 1

Tactic:
simp only [sum_const, nsmul_eq_mul]

Premises used: nsmul_eq_mul, Finset.sum_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
⊢ 1 - k * p + (↑(#s) : ℝ) * p = 1

Tactic:
ring
-- 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
⊢ 0 ≤ 1 - k * p

Tactic:
hk'
-- 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
⊢ 0 ≤ 1 - k * p

Tactic:
exact hk'
-- 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
⊢ ∀ i ∈ s, 0 ≤ p

Tactic:
fun _ _ ↦ 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
⊢ ∀ i ∈ s, 0 ≤ p

Tactic:
exact fun _ _ ↦ 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
h : (∫⁻ (t : A i), f (X t) ∂μ i) ^ (1 - k * p) = lmarginal (X := A) μ {i} f x ^ (1 - k * p)
h₁ :
  Eq (α := ℝ≥0∞) (∏ j ∈ s, (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ p)
    (∏ j ∈ s, lmarginal (X := A) μ {i, j} f x ^ p)
⊢ lmarginal (X := A) μ {i} f x ^ p *
      ((∫⁻ (t : A i), f (X t) ∂μ i) ^ (1 - k * p) *
        ∏ j ∈ s, (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ p) =
    lmarginal (X := A) μ {i} f x ^ p *
      (lmarginal (X := A) μ {i} f x ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {i, j} f x ^ p)

Tactic:
congr! 2
-- 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
h h₁ :
  (∫⁻ (t : A i), f (X t) ∂μ i) ^ (1 - k * p) =
    HPow.hPow (α := ℝ≥0∞) ((fun (x : (a : ι) → A a) ↦ ∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) x) (1 - k * p)
⊢ (∫⁻ (t : A i), f (X t) ∂μ i) ^ (1 - k * p) = lmarginal (X := A) μ {i} f x ^ (1 - k * p)

Tactic:
rw [lmarginal_singleton]

Premises used: MeasureTheory.lmarginal_singleton
-- 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
⊢ Eq (α := ℝ≥0∞) (∏ j ∈ s, (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ p)
    (∏ j ∈ s, lmarginal (X := A) μ {i, j} f x ^ p)

Tactic:
prod_congr rfl fun j hj => ?_

Premises used: Finset.prod_congr, 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
h :
  ∀ (j : ι) (hj : j ∈ s),
    (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ p = lmarginal (X := A) μ {i, j} f x ^ p
⊢ Eq (α := ℝ≥0∞) (∏ j ∈ s, (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ p)
    (∏ j ∈ s, lmarginal (X := A) μ {i, j} f x ^ p)

Tactic:
refine prod_congr rfl fun j hj => ?_

Premises used: Finset.prod_congr, 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
j : ι
hj : j ∈ s
simp : ¬i = j
⊢ i ∉ {j}

Tactic:
simp only [Finset.mem_singleton] at hj ⊢

Premises used: Finset.mem_singleton
-- 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
j : ι
hj : j ∈ s
⊢ ¬i = j

Tactic:
fun h ↦ hi (h ▸ hj)

Premises used: Eq.rec, Eq.symm, Not
-- 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
j : ι
hj : j ∈ s
⊢ ¬i = j

Tactic:
exact fun h ↦ hi (h ▸ hj)
-- 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
j : ι
hj : j ∈ s
⊢ i ∉ {j}

Tactic:
have hi' : i ∉ ({j} : Finset ι) := by
                simp only [Finset.mem_singleton] at hj ⊢
                exact fun h ↦ hi (h ▸ hj)
-- 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
j : ι
hj : j ∈ s
hi' : i ∉ {j}
h h₁ :
  (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ p =
    (∫⁻ (xᵢ : A i), lmarginal (X := A) μ {j} f (update (β := A) x i xᵢ) ∂μ i) ^ p
⊢ (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ p = lmarginal (X := A) μ {i, j} f x ^ p

Tactic:
rw [lmarginal_insert _ hf hi']

Premises used: MeasureTheory.lmarginal_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 := 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
rw :
  lmarginal (X := A) μ {i} f x ^ p *
      (lmarginal (X := A) μ {i} f x ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {i, j} f x ^ p) =
    lmarginal (X := A) μ {i} f x ^ p * lmarginal (X := A) μ {i} f x ^ (1 - k * p) *
      ∏ j ∈ s, lmarginal (X := A) μ {i, j} f x ^ p
hy : 0 ≤ p
hz : 0 ≤ 1 - k * p
⊢ lmarginal (X := A) μ {i} f x ^ p *
      (lmarginal (X := A) μ {i} f x ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {i, j} f x ^ p) =
    lmarginal (X := A) μ {i} f x ^ (p + (1 - k * p)) * ∏ j ∈ s, lmarginal (X := A) μ {i, j} f x ^ p

Tactic:
rw [ENNReal.rpow_add_of_nonneg]

Premises used: ENNReal.rpow_add_of_nonneg
-- 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
⊢ lmarginal (X := A) μ {i} f x ^ p *
      (lmarginal (X := A) μ {i} f x ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {i, j} f x ^ p) =
    lmarginal (X := A) μ {i} f x ^ p * lmarginal (X := A) μ {i} f x ^ (1 - k * p) *
      ∏ j ∈ s, lmarginal (X := A) μ {i, j} f x ^ p

Tactic:
ring
-- 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
⊢ 0 ≤ p

Tactic:
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
⊢ 0 ≤ p

Tactic:
exact 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
hxy : p + (1 - k * p) = 1 - HSub.hSub (α := ℝ) (↑(#s) : ℝ) 1 * p
hxy₁ :
  ∀ (j : ι) (hj : j ∈ s),
    lmarginal (X := A) μ {i, j} f x ^ p = lmarginal (X := A) μ {j} (lmarginal (X := A) μ {i} f) x ^ p
⊢ lmarginal (X := A) μ {i} f x ^ (p + (1 - k * p)) * ∏ j ∈ s, lmarginal (X := A) μ {i, j} f x ^ p ≤
    lmarginal (X := A) μ {i} f x ^ (1 - HSub.hSub (α := ℝ) (↑(#s) : ℝ) 1 * p) *
      ∏ j ∈ s, lmarginal (X := A) μ {j} (lmarginal (X := A) μ {i} f) x ^ p

Tactic:
congr! 2 with j hj
-- 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
⊢ p + (1 - k * p) = 1 - HSub.hSub (α := ℝ) (↑(#s) : ℝ) 1 * p

Tactic:
ring
-- 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
j : ι
hj : j ∈ s
hxy : lmarginal (X := A) μ {i, j} f x = lmarginal (X := A) μ {j} (lmarginal (X := A) μ {i} f) x
⊢ lmarginal (X := A) μ {i, j} f x ^ p = lmarginal (X := A) μ {j} (lmarginal (X := A) μ {i} f) x ^ p

Tactic:
congr! 1
-- 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
j : ι
hj : j ∈ s
hxy : lmarginal (X := A) μ {i, j} f x = lmarginal (X := A) μ ({j} ∪ {i}) f x
hxy₁ : Disjoint (α := Finset ι) {j} {i}
⊢ lmarginal (X := A) μ {i, j} f x = lmarginal (X := A) μ {j} (lmarginal (X := A) μ {i} f) x

Tactic:
rw [← lmarginal_union μ f hf]

Premises used: MeasureTheory.lmarginal_union