-- 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
calc :
  ∫⁻ (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
calc₁ :
  ∫⁻ (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
calc₂ :
  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)
calc₃ :
  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)
calc₄ :
  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
calc₅ :
  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
⊢ ∫⁻ (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

Tactic:
calc ∫⁻ t, f (X t) ^ (1 - k * p)
          * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p ∂(μ i)
      = ∫⁻ t, (∫⋯∫⁻_{i}, f ∂μ) (X t) ^ p * (f (X t) ^ (1 - k * p)
          * ∏ j ∈ s, ((∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p)) ∂(μ i) := by
              -- rewrite integrand so that `(∫⋯∫⁻_insert i s, f ∂μ) ^ p` comes first
              clear_value X
              congr! 2 with t
              simp_rw [prod_insert hi]
              ring_nf
    _ = (∫⋯∫⁻_{i}, f ∂μ) x ^ p *
          ∫⁻ t, f (X t) ^ (1 - k * p) * ∏ j ∈ s, ((∫⋯∫⁻_{j}, f ∂μ) (X t)) ^ p ∂(μ i) := by
              -- pull out this constant factor
              have : ∀ t, (∫⋯∫⁻_{i}, f ∂μ) (X t) = (∫⋯∫⁻_{i}, f ∂μ) x := by
                intro t
                rw [lmarginal_update_of_mem]
                exact Iff.mpr Finset.mem_singleton rfl
              simp_rw [this]
              rw [lintegral_const_mul]
              exact (hF₀.pow_const _).mul <| Finset.measurable_fun_prod _ fun _ _ ↦ hF₁.pow_const _
    _ ≤ (∫⋯∫⁻_{i}, f ∂μ) x ^ p *
          ((∫⁻ t, f (X t) ∂μ i) ^ (1 - k * p)
          * ∏ j ∈ s, (∫⁻ t, (∫⋯∫⁻_{j}, f ∂μ) (X t) ∂μ i) ^ p) := by
              -- apply Hölder's inequality
              gcongr
              apply ENNReal.lintegral_mul_prod_norm_pow_le
              · exact hF₀.aemeasurable
              · intros
                exact hF₁.aemeasurable
              · simp only [sum_const, nsmul_eq_mul]
                ring
              · exact hk'
              · exact fun _ _ ↦ hp₀
    _ = (∫⋯∫⁻_{i}, f ∂μ) x ^ p *
          ((∫⋯∫⁻_{i}, f ∂μ) x ^ (1 - k * p) * ∏ j ∈ s, (∫⋯∫⁻_{i, j}, f ∂μ) x ^ p) := by
              -- absorb the newly-created integrals into `∫⋯∫`
              congr! 2
              · rw [lmarginal_singleton]
              refine prod_congr rfl fun j hj => ?_
              have hi' : i ∉ ({j} : Finset ι) := by
                simp only [Finset.mem_singleton] at hj ⊢
                exact fun h ↦ hi (h ▸ hj)
              rw [lmarginal_insert _ hf hi']
    _ = (∫⋯∫⁻_{i}, f ∂μ) x ^ (p + (1 - k * p)) * ∏ j ∈ s, (∫⋯∫⁻_{i, j}, f ∂μ) x ^ p := by
              -- combine two `(∫⋯∫⁻_insert i s, f ∂μ) x` terms
              rw [ENNReal.rpow_add_of_nonneg]
              · ring
              · exact hp₀
              · exact hk'
    _ ≤ (∫⋯∫⁻_{i}, f ∂μ) x ^ (1 - (s.card - 1 : ℝ) * p) *
          ∏ j ∈ s, (∫⋯∫⁻_{j}, (∫⋯∫⁻_{i}, f ∂μ) ∂μ) x ^ p := by
              -- identify the result with the RHS integrand
              congr! 2 with j hj
              · ring
              · congr! 1
                rw [← lmarginal_union μ f hf]
                · congr
                  rw [Finset.union_comm]
                  rfl
                · rw [Finset.disjoint_singleton]
                  simp only at hj
                  exact fun h ↦ hi (h ▸ hj)

Premises used: HMul.hMul, HSub.hSub, Insert.insert, Nat.cast, Finset.prod, HPow.hPow, HAdd.hAdd, MeasureTheory.lmarginal, Finset.card, Singleton.singleton, OfNat.ofNat, MeasureTheory.lintegral