-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
For : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
For₁ :
  ∀ (this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1),
    ∫⁻ (x : ι → ℝ), ‖u x‖ₑ ^ p ≤
      (∫⁻ (x : ι → ℝ), enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F) (fderiv ℝ u x)) ^ p
For₂ : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
For₃ For₄ :
  ∀ (this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1),
    ∫⁻ (x : ι → ℝ), ‖u x‖ₑ ^ p ≤
      (∫⁻ (x : ι → ℝ), enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F) (fderiv ℝ u x)) ^ p
For₅ :
  ∀ (this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1),
    ∫⁻ (x : ι → ℝ), ∏ _i : ι, ‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ≤
      ∫⁻ (x : (a : ι) → ℝ),
        ∏ i : ι,
          (∫⁻ (xᵢ : ℝ),
              enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
                (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i xᵢ))) ^
            (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)
hfg :
  ∀ (this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) (x : ι → ℝ) (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i →
      ‖u x‖ₑ ≤
        ∫⁻ (xᵢ : ℝ),
          enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
            (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i xᵢ))
hfg₁ :
  ∀ (this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) (x : ι → ℝ) (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i →
      ∫⁻ (xᵢ : ℝ) in Set.Iic (x i), ‖deriv (u ∘ update (β := fun (a : ι) ↦ ℝ) x i) xᵢ‖ₑ ≤
        ∫⁻ (xᵢ : ℝ),
          enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
            (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i xᵢ))
hfg₂ :
  ∀ (this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) (x : ι → ℝ) (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i → Measure.restrict volume (Set.Iic (x i)) ≤ volume
hfg₃ hfg₄ :
  ∀ (this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) (x : ι → ℝ) (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i →
      ∀ (y : ℝ),
        ‖deriv (u ∘ update (β := fun (a : ι) ↦ ℝ) x i) y‖ₑ ≤
          enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
            (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i y))
⊢ ∫⁻ (x : ι → ℝ), ‖u x‖ₑ ^ p ≤
    (∫⁻ (x : ι → ℝ), enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F) (fderiv ℝ u x)) ^ p

Tactic:
classical
  /- For a function `f` in one variable and `t ∈ ℝ` we have
  `|f(t)| = `|∫_{-∞}^t Df(s)∂s| ≤ ∫_ℝ |Df(s)| ∂s` where we use the fundamental theorem of calculus.
  For each `x ∈ ℝⁿ` we let `u` vary in one of the `n` coordinates and apply the inequality above.
  By taking the product over these `n` factors, raising them to the power `(n-1)⁻¹` and integrating,
  we get the inequality `∫ |u| ^ (n/(n-1)) ≤ ∫ x, ∏ i, (∫ xᵢ, |Du(update x i xᵢ)|)^(n-1)⁻¹`.
  The result then follows from the grid-lines lemma. -/
  have : (1 : ℝ) ≤ ↑#ι - 1 := by
    have hι : (2 : ℝ) ≤ #ι := by exact_mod_cast hp.lt
    linarith
  calc ∫⁻ x, ‖u x‖ₑ ^ p
      = ∫⁻ x, (‖u x‖ₑ ^ (1 / (#ι - 1 : ℝ))) ^ (#ι : ℝ) := by
        -- a little algebraic manipulation of the exponent
        congr! 2 with x
        rw [← ENNReal.rpow_mul, hp.conjugate_eq]
        field_simp
    _ = ∫⁻ x, ∏ _i : ι, ‖u x‖ₑ ^ (1 / (#ι - 1 : ℝ)) := by
        -- express the left-hand integrand as a product of identical factors
        congr! 2 with x
        simp_rw [prod_const]
        norm_cast
    _ ≤ ∫⁻ x, ∏ i, (∫⁻ xᵢ, ‖fderiv ℝ u (update x i xᵢ)‖ₑ) ^ ((1 : ℝ) / (#ι - 1 : ℝ)) := ?_
    _ ≤ (∫⁻ x, ‖fderiv ℝ u x‖ₑ) ^ p := by
        -- apply the grid-lines lemma
        apply lintegral_prod_lintegral_pow_le _ hp
        fun_prop
  -- we estimate |u x| using the fundamental theorem of calculus.
  gcongr with x i
  calc ‖u x‖ₑ
    _ ≤ ∫⁻ xᵢ in Iic (x i), ‖deriv (u ∘ update x i) xᵢ‖ₑ := by
        apply le_trans (by simp) (HasCompactSupport.enorm_le_lintegral_Ici_deriv _ _ _)
        · exact hu.comp (by convert! contDiff_update 1 x i)
        · exact h2u.comp_isClosedEmbedding (isClosedEmbedding_update x i)
    _ ≤ ∫⁻ xᵢ, ‖fderiv ℝ u (update x i xᵢ)‖ₑ := ?_
  gcongr with y
  · exact Measure.restrict_le_self
  -- bound the derivative which appears
  calc ‖deriv (u ∘ update x i) y‖ₑ = ‖fderiv ℝ u (update x i y) (deriv (update x i) y)‖ₑ := by
        rw [fderiv_comp_deriv _ (hu.differentiable one_ne_zero).differentiableAt
          (hasDerivAt_update x i y).differentiableAt]
    _ ≤ ‖fderiv ℝ u (update x i y)‖ₑ * ‖deriv (update x i) y‖ₑ := ContinuousLinearMap.le_opENorm _ _
    _ ≤ ‖fderiv ℝ u (update x i y)‖ₑ := by simp [deriv_update, Pi.enorm_single]

Premises used: Real, HSub.hSub, Fintype.card, HDiv.hDiv, fderiv, Nat.cast, ENorm.enorm, MeasureTheory.MeasureSpace.volume, MeasureTheory.Measure.restrict_le_self, ContinuousLinearMap.le_opENorm, OfNat.ofNat, MeasureTheory.lintegral