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

Tactic:
congr
-- 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 : Eq (α := Finset ι) {i, j} ({i} ∪ {j})
⊢ Eq (α := Finset ι) {i, j} ({j} ∪ {i})

Tactic:
rw [Finset.union_comm]

Premises used: Finset.union_comm
-- 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
⊢ Eq (α := Finset ι) {i, j} ({i} ∪ {j})

Tactic:
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
hxy : j ≠ i
⊢ Disjoint (α := Finset ι) {j} {i}

Tactic:
rw [Finset.disjoint_singleton]

Premises used: Finset.disjoint_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
⊢ j ≠ i

Tactic:
fun h ↦ hi (h ▸ hj)

Premises used: Eq.rec, 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
⊢ j ≠ i

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 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
rw :
  ∀ (s : Finset ι) ⦃a : ι⦄,
    a ∉ s →
      T (A := A) μ p (lmarginal (X := A) μ (insert a s)ᶜ f) (insert a s) ≤ T (A := A) μ p (lmarginal (X := A) μ sᶜ f) s
⊢ Antitone (β := ((i : ι) → A i) → ℝ≥0∞) fun (s : Finset ι) ↦ T (A := A) μ p (lmarginal (X := A) μ sᶜ f) s

Tactic:
rw [Finset.antitone_iff_forall_insert_le]

Premises used: Finset.antitone_iff_forall_insert_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 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ T (A := A) μ p (lmarginal (X := A) μ (insert i s)ᶜ f) (insert i s) ≤
    T (A := A) μ p (lmarginal (X := A) μ {i} (lmarginal (X := A) μ (insert i s)ᶜ f)) s

Tactic:
T_insert_le_T_lmarginal_singleton μ hp₀ s ?_ i hi (hf.lmarginal μ)

Premises used: Measurable.lmarginal, MeasureTheory.GridLines.T_insert_le_T_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 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
h : lmarginal (X := A) μ sᶜ f = lmarginal (X := A) μ {i} (lmarginal (X := A) μ (insert i s)ᶜ f)
convert_1 : (↑(#s) : ℝ) * p ≤ 1
⊢ T (A := A) μ p (lmarginal (X := A) μ (insert i s)ᶜ f) (insert i s) ≤ T (A := A) μ p (lmarginal (X := A) μ sᶜ f) s

Tactic:
convert! T_insert_le_T_lmarginal_singleton μ hp₀ s ?_ i hi (hf.lmarginal μ) using 2

Premises used: Measurable.lmarginal, MeasureTheory.GridLines.T_insert_le_T_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 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
h : lmarginal (X := A) μ sᶜ f = lmarginal (X := A) μ ({i} ∪ (insert i s)ᶜ) f
h₁ : Disjoint {i} (insert i s)ᶜ
⊢ lmarginal (X := A) μ sᶜ f = lmarginal (X := A) μ {i} (lmarginal (X := A) μ (insert i s)ᶜ f)

Tactic:
rw [← lmarginal_union μ f hf]

Premises used: MeasureTheory.lmarginal_union
-- 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 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
h : lmarginal (X := A) μ (insert i (insert i s)ᶜ) f = lmarginal (X := A) μ ({i} ∪ (insert i s)ᶜ) f
⊢ lmarginal (X := A) μ sᶜ f = lmarginal (X := A) μ ({i} ∪ (insert i s)ᶜ) f

Tactic:
rw [← insert_compl_insert hi]

Premises used: Finset.insert_compl_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 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ lmarginal (X := A) μ (insert i (insert i s)ᶜ) f = lmarginal (X := A) μ ({i} ∪ (insert i s)ᶜ) f

Tactic:
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 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
h : i ∈ insert i s
⊢ Disjoint {i} (insert i s)ᶜ

Tactic:
rw [Finset.disjoint_singleton_left, notMem_compl]

Premises used: Finset.disjoint_singleton_left, Finset.notMem_compl
-- 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 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ i ∈ insert i s

Tactic:
mem_insert_self i s

Premises used: Finset.mem_insert_self
-- 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 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ i ∈ insert i s

Tactic:
exact mem_insert_self i s

Premises used: Finset.mem_insert_self
-- 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 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ (↑(#s) : ℝ) * p ≤ 1

Tactic:
le_trans ?_ hp

Premises used: le_trans
-- 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 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
convert_1 : (↑(#s) : ℝ) * p ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p
⊢ (↑(#s) : ℝ) * p ≤ 1

Tactic:
refine le_trans ?_ hp

Premises used: le_trans
-- 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 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
convert_1 : (↑(#s) : ℝ) ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
⊢ (↑(#s) : ℝ) * p ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * 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 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
this : HAdd.hAdd (α := ℝ) (↑(#s) : ℝ) 1 ≤ (↑#ι : ℝ)
linarith :
  HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 < (↑(#s) : ℝ) →
    HAdd.hAdd (α := ℝ) (↑(#s) : ℝ) 1 - (↑#ι : ℝ) + (HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 - (↑(#s) : ℝ)) = 0
⊢ (↑(#s) : ℝ) ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1

Tactic:
linarith
-- 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 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
convert_1 : HAdd.hAdd (α := ℝ) (↑(#s) : ℝ) 1 ≤ (↑#ι : ℝ)
⊢ (↑(#s) : ℝ) ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1

Tactic:
suffices (s.card : ℝ) + 1 ≤ #ι by linarith
-- 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 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
convert_1 : HAdd.hAdd (α := ℝ) (↑(#s) : ℝ) 1 ≤ (↑(#s + #sᶜ) : ℝ)
⊢ HAdd.hAdd (α := ℝ) (↑(#s) : ℝ) 1 ≤ (↑#ι : ℝ)

Tactic:
rw [← card_add_card_compl s]

Premises used: Finset.card_add_card_compl
-- 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 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
convert_1 : #s + 1 ≤ #s + #sᶜ
⊢ HAdd.hAdd (α := ℝ) (↑(#s) : ℝ) 1 ≤ (↑(#s + #sᶜ) : ℝ)

Tactic:
norm_cast
-- 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 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
convert_1 : 1 ≤ #sᶜ
⊢ #s + 1 ≤ #s + #sᶜ

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 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi rwa rwa₁ rwa₂ rwa₃ : i ∉ s
⊢ i ∈ sᶜ

Tactic:
rwa [Finset.mem_compl]

Premises used: Finset.mem_compl
-- 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 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ sᶜ.Nonempty

Tactic:
have hi' : sᶜ.Nonempty := ⟨i, by rwa [Finset.mem_compl]⟩
-- 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 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
hi' : sᶜ.Nonempty
convert_1 convert_1₁ convert_1₂ convert_1₃ : ∀ (hi' : 0 < #sᶜ), 1 ≤ #sᶜ
⊢ 1 ≤ #sᶜ

Tactic:
rwa [← card_pos] at hi'

Premises used: Finset.card_pos
-- 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 ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
inl :
  IsEmpty ((i : ι) → A i) →
    ∫⁻ (x : (i : ι) → A i),
        f x ^ (1 - HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p) *
          ∏ i : ι, (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ p ∂Measure.pi (α := A) μ ≤
      (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi (α := A) μ) ^ (1 + p)
inr :
  Nonempty ((i : ι) → A i) →
    ∫⁻ (x : (i : ι) → A i),
        f x ^ (1 - HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p) *
          ∏ i : ι, (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ p ∂Measure.pi (α := A) μ ≤
      (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi (α := A) μ) ^ (1 + p)
⊢ ∫⁻ (x : (i : ι) → A i),
      f x ^ (1 - HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p) *
        ∏ i : ι, (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ p ∂Measure.pi (α := A) μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi (α := A) μ) ^ (1 + p)

Tactic:
cases isEmpty_or_nonempty (∀ i, A i)

Premises used: isEmpty_or_nonempty
-- 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 ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
h : IsEmpty ((i : ι) → A i)
⊢ ∫⁻ (x : (i : ι) → A i),
      f x ^ (1 - HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p) *
        ∏ i : ι, (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ p ∂Measure.pi (α := A) μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi (α := A) μ) ^ (1 + p)

Tactic:
simp
-- 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 ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
h : Nonempty ((i : ι) → A i)
inr :
  ∀ (inhabited_h : Inhabited ((i : ι) → A i)),
    ∫⁻ (x : (i : ι) → A i),
        f x ^ (1 - HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p) *
          ∏ i : ι, (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ p ∂Measure.pi (α := A) μ ≤
      (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi (α := A) μ) ^ (1 + p)
⊢ ∫⁻ (x : (i : ι) → A i),
      f x ^ (1 - HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p) *
        ∏ i : ι, (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ p ∂Measure.pi (α := A) μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi (α := A) μ) ^ (1 + p)

Tactic:
inhabit ∀ i, A i
-- 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 ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
h : Nonempty ((i : ι) → A i)
inhabited_h : Inhabited ((i : ι) → A i)
⊢ LE.le.{u_1} (α := Finset ι) ∅ Finset.univ

Tactic:
have H : (∅ : Finset ι) ≤ Finset.univ := Finset.empty_subset _
-- 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 ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
h : Nonempty ((i : ι) → A i)
inhabited_h : Inhabited ((i : ι) → A i)
H : LE.le.{u_1} (α := Finset ι) ∅ Finset.univ
⊢ ∫⁻ (x : (i : ι) → A i),
      f x ^ (1 - HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p) *
        ∏ i : ι, (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ p ∂Measure.pi (α := A) μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi (α := A) μ) ^ (1 + p)

Tactic:
simpa [lmarginal_univ] using GridLines.T_lmarginal_antitone μ hp₀ hp hf H default

Premises used: MeasureTheory.lmarginal_univ, MeasureTheory.GridLines.T_lmarginal_antitone, Inhabited.default
-- 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 ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
⊢ 1 < #ι

Tactic:
exact_mod_cast hp.lt

Premises used: Real.HolderTriple.lt
-- 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 ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
⊢ Nontrivial ι

Tactic:
have : Nontrivial ι :=
    Fintype.one_lt_card_iff_nontrivial.mp (by exact_mod_cast hp.lt)
-- 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 ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
norm_cast : 1 < #ι
⊢ LT.lt (α := ℝ) 1 (↑#ι : ℝ)

Tactic:
norm_cast
-- 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 ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
⊢ 1 < #ι

Tactic:
Fintype.one_lt_card

Premises used: Fintype.one_lt_card
-- 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 ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
⊢ 1 < #ι

Tactic:
exact Fintype.one_lt_card

Premises used: Fintype.one_lt_card
-- 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 ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
⊢ LT.lt (α := ℝ) 1 (↑#ι : ℝ)

Tactic:
have h0 : (1 : ℝ) < #ι := by norm_cast; exact Fintype.one_lt_card
-- 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 ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
h0 : LT.lt (α := ℝ) 1 (↑#ι : ℝ)
linarith :
  HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 ≤ 0 → HSub.hSub (α := ℝ) 1 (↑#ι : ℝ) + (HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 - 0) = 0
⊢ 0 < HSub.hSub (α := ℝ) (↑#ι : ℝ) 1

Tactic:
linarith
-- 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 ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
h0 : LT.lt (α := ℝ) 1 (↑#ι : ℝ)
⊢ 0 < HSub.hSub (α := ℝ) (↑#ι : ℝ) 1

Tactic:
have h1 : (0 : ℝ) < #ι - 1 := by linarith
-- 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 ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
h0 : LT.lt (α := ℝ) 1 (↑#ι : ℝ)
h1 : 0 < HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
⊢ 0 ≤ 1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1

Tactic:
positivity