mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
⊢ Measure.map (⇑(MeasurableEquiv.arrowProdEquivProdArrow α β γ)) (Measure.pi fun i ↦ (μ i).prod (ν i)) =
    (Measure.pi fun i ↦ μ i).prod (Measure.pi fun i ↦ ν i)

Tactic:
by
    refine (FiniteSpanningSetsIn.ext ?_ (isPiSystem_pi.prod isPiSystem_pi)
      ((FiniteSpanningSetsIn.pi fun i ↦ (μ i).toFiniteSpanningSetsIn).prod
      (FiniteSpanningSetsIn.pi (fun i ↦ (ν i).toFiniteSpanningSetsIn))) ?_).symm
    · refine (generateFrom_eq_prod generateFrom_pi generateFrom_pi ?_ ?_).symm
      · exact (FiniteSpanningSetsIn.pi (fun i ↦ (μ i).toFiniteSpanningSetsIn)).isCountablySpanning
      · exact (FiniteSpanningSetsIn.pi (fun i ↦ (ν i).toFiniteSpanningSetsIn)).isCountablySpanning
    · rintro _ ⟨s, ⟨s, _, rfl⟩, ⟨_, ⟨t, _, rfl⟩, rfl⟩⟩
      rw [MeasurableEquiv.map_apply, MeasurableEquiv.arrowProdEquivProdArrow,
        MeasurableEquiv.coe_mk]
      rw [show Equiv.arrowProdEquivProdArrow γ _ _ ⁻¹' (univ.pi s ×ˢ univ.pi t) =
          (univ.pi fun i ↦ s i ×ˢ t i) by
          ext; simp [Set.mem_pi, forall_and]]
      simp_rw [pi_pi, prod_prod, pi_pi, Finset.prod_mul_distrib]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: case neg
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ∞
⊢ eLpNorm' f p.toReal μ ≤ c • eLpNorm' g p.toReal μ

Tactic:
exact eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul h (ENNReal.toReal_pos h0 h_top)

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ContinuousENorm ε'
c : ε'
hc : ‖c‖ₑ ≠ ∞
inst✝ : IsFiniteMeasure μ
⊢ MemLp (fun x ↦ c) p μ

Tactic:
refine ⟨aestronglyMeasurable_const, ?_⟩
  by_cases h0 : p = 0
  · simp [h0]
  by_cases hμ : μ = 0
  · simp [hμ]
  rw [eLpNorm_const c h0 hμ]
  finiteness

Goal state after:
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
r' : ℝ≥0∞
hr' : p.HolderTriple q r'
⊢ r⁻¹ = r'⁻¹

Tactic:
inv_eq p q r,

Goal state after:
p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
r' : ℝ≥0∞
hr' : p.HolderTriple q r'
⊢ p⁻¹ + q⁻¹ = r'⁻¹
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
key : f (((z - y) / (z - x)) • x + ((y - x) / (z - x)) • z) ≤ ((z - y) / (z - x)) • f x + ((y - x) / (z - x)) • f z
⊢ (z - x) * f y ≤ (z - y) * f x + (y - x) * f z

Tactic:
simp only [smul_eq_mul] at key
    ring_nf at key
    field_simp at key
    linear_combination key

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hμν : ν ≪ μ
⊢ eLpNormEssSup f ν ≤ eLpNormEssSup f μ

Tactic:
eLpNormEssSup

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hμν : ν ≪ μ
⊢ essSup (fun x ↦ ‖f x‖ₑ) ν ≤ essSup (fun x ↦ ‖f x‖ₑ) μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝⁵ : ENorm ε
R : Type u_7
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : Module R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
f : α → ε
⊢ eLpNormEssSup f (c • μ) = eLpNormEssSup f μ

Tactic:
eLpNormEssSup

Goal state after:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝⁵ : ENorm ε
R : Type u_7
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : Module R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
f : α → ε
⊢ essSup (fun x ↦ ‖f x‖ₑ) (c • μ) = essSup (fun x ↦ ‖f x‖ₑ) μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
⊢ eLpNormEssSup f (c • μ) = eLpNormEssSup f μ

Tactic:
eLpNormEssSup

Goal state after:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
⊢ essSup (fun x ↦ ‖f x‖ₑ) (c • μ) = essSup (fun x ↦ ‖f x‖ₑ) μ
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 < (z - y) / (z - x)
hb : 0 < (y - x) / (z - x)
key : f (((z - y) / (z - x)) • x + ((y - x) / (z - x)) • z) < ((z - y) / (z - x)) • f x + ((y - x) / (z - x)) • f z
⊢ (z - x) * f y < (z - y) * f x + (y - x) * f z

Tactic:
simp only [smul_eq_mul] at key
    ring_nf at key
    field_simp at key
    linear_combination key

Goal state after:
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p : ℝ≥0
hp : 1 < p
⊢ ↑(p / (p - 1)) = (↑p).conjExponent

Tactic:
conjExponent

Goal state after:
p : ℝ≥0
hp : 1 < p
⊢ ↑(p / (p - 1)) = 1 + (↑p - 1)⁻¹
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case e'_12
b : ℝ
hb : 0 < b
x : ℝ
⊢ b ^ x = (rexp ∘ ⇑((LinearMap.mul ℝ ℝ) (log b))) x

Tactic:
simp [Real.rpow_def_of_pos hb]

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
⊢ ∑ i ∈ s, w i * z i ≤ (∑ i ∈ s, w i * z i ^ p) ^ (1 / p)

Tactic:
by
  have : 0 < p := by positivity
  rw [← rpow_le_rpow_iff _ _ this, ← rpow_mul, one_div_mul_cancel (ne_of_gt this), rpow_one]
  · exact rpow_arith_mean_le_arith_mean_rpow s w z hw hw' hz hp
  all_goals
    apply_rules [sum_nonneg, rpow_nonneg]
    intro i hi
    positivity [hw i hi, hz i hi]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ∫⁻ (a : α), g a ^ q ∂μ = 0
⊢ ∫⁻ (a : α), (f * g) a ∂μ = 0

Tactic:
rw [mul_comm]

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_zero : ¬∫⁻ (a : α), f a ^ p ∂μ = 0
hg_zero : ∫⁻ (a : α), g a ^ q ∂μ = 0
⊢ ∫⁻ (a : α), (g * f) a ∂μ = 0
Module: Mathlib.Analysis.Convex.Mul

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
G : Type u_4
inst✝¹¹ : CommRing 𝕜
inst✝¹⁰ : LinearOrder 𝕜
inst✝⁹ : IsStrictOrderedRing 𝕜
inst✝⁸ : CommRing E
inst✝⁷ : LinearOrder E
inst✝⁶ : IsStrictOrderedRing E
inst✝⁵ : AddCommGroup G
inst✝⁴ : Module 𝕜 G
inst✝³ : Module 𝕜 E
s : Set G
inst✝² : IsOrderedModule 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
f : G → E
hf : ConvexOn 𝕜 s f
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
n : ℕ
⊢ ConvexOn 𝕜 s (f ^ (n + 1))

Tactic:
rw [pow_succ']
    exact hf.mul (hf.pow hf₀ _) hf₀ (fun x hx ↦ pow_nonneg (hf₀ hx) _) <|
      (monovaryOn_self f s).pow_right₀ hf₀ n

Goal state after:
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  (∀ i ∈ s, AEMeasurable (f i) μ) →
    ∀ {p : ι → ℝ},
      ∑ i ∈ s, p i = 1 →
        (∀ i ∈ s, 0 ≤ p i) → ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : ∑ i ∈ insert i₀ s, p i = 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : ι → ℝ := fun i ↦ p i / (1 - p i₀)
hq : ∑ i ∈ s, q i = 1
h2q : ∀ i ∈ s, 0 ≤ q i
⊢ ∫⁻ (a : α), f i₀ a ^ p i₀ * (∏ i ∈ s, f i a ^ q i) ^ (1 - p i₀) ∂μ ≤
    (∫⁻ (a : α), f i₀ a ∂μ) ^ p i₀ * (∫⁻ (a : α), ∏ i ∈ s, f i a ^ q i ∂μ) ^ (1 - p i₀)

Tactic:
by
            apply ENNReal.lintegral_mul_norm_pow_le
            · exact hf i₀ <| mem_insert_self ..
            · exact s.aemeasurable_fun_prod fun i hi ↦ (hf i <| mem_insert_of_mem hi).pow_const _
            · exact h2p i₀ <| mem_insert_self ..
            · exact hpi₀
            · apply add_sub_cancel

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a ≠ ∞ ∧ b ≠ ∞
⊢ ↑(a.toNNReal * b.toNNReal) ≤ ↑(a.toNNReal ^ p / p.toNNReal) + ↑(b.toNNReal ^ q / q.toNNReal)

Tactic:
← coe_add,

Goal state after:
case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a ≠ ∞ ∧ b ≠ ∞
⊢ ↑(a.toNNReal * b.toNNReal) ≤ ↑(a.toNNReal ^ p / p.toNNReal + b.toNNReal ^ q / q.toNNReal)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h0 : a ≠ 0 ∧ b ≠ 0
h : a ≠ ∞ ∧ b ≠ ∞
⊢ ↑(a.toNNReal * b.toNNReal) = ↑(a.toNNReal ^ p / p.toNNReal) + ↑(b.toNNReal ^ q / q.toNNReal) ↔
    ↑a.toNNReal = ∞ ∧ ↑b.toNNReal ≠ 0 ∨ ↑a.toNNReal ≠ 0 ∧ ↑b.toNNReal = ∞ ∨ ↑(a.toNNReal ^ p) = ↑(b.toNNReal ^ q)

Tactic:
← coe_add,

Goal state after:
case neg
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h0 : a ≠ 0 ∧ b ≠ 0
h : a ≠ ∞ ∧ b ≠ ∞
⊢ ↑(a.toNNReal * b.toNNReal) = ↑(a.toNNReal ^ p / p.toNNReal + b.toNNReal ^ q / q.toNNReal) ↔
    ↑a.toNNReal = ∞ ∧ ↑b.toNNReal ≠ 0 ∨ ↑a.toNNReal ≠ 0 ∧ ↑b.toNNReal = ∞ ∨ ↑(a.toNNReal ^ p) = ↑(b.toNNReal ^ q)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e_f
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
hg : ∑ i ∈ s, g i ^ q = 0
i : ι
⊢ ↑(f i * g i) = ↑(g i * f i)

Tactic:
rw [mul_comm]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inr.inr.refine_2
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
hg : 0 < ∑ i ∈ s, g i ^ q
f' : ι → ℝ≥0 := fun i ↦ f i / (∑ i ∈ s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i ↦ g i / (∑ i ∈ s, g i ^ q) ^ (1 / q)
⊢ ∑ i ∈ s, g' i ^ q = 1

Tactic:
simp_rw [g', div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel₀ hpq.symm.ne_zero,
      rpow_one, div_self hg.ne']

Goal state after:
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
h_one_div_q : 1 / q = 1 - 1 / p
h :
  ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
    ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
      ((∫⁻ (a : α), (f + g) a ^ p ∂μ) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)))
| (∫⁻ (a : α), (f + g) a ^ p ∂μ) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p))

Tactic:
rw [mul_comm]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
h_one_div_q : 1 / q = 1 - 1 / p
h :
  ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
    ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
      ((∫⁻ (a : α), (f + g) a ^ p ∂μ) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)))
| (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) * ∫⁻ (a : α), (f + g) a ^ p ∂μ
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case left
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) ∈ (fun g ↦ ∑ i ∈ s, f i * g i) '' {g | ∑ i ∈ s, g i ^ q ≤ 1}

pp: case right
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) ∈ upperBounds ((fun g ↦ ∑ i ∈ s, f i * g i) '' {g | ∑ i ∈ s, g i ^ q ≤ 1})

Tactic:
· use fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)
    obtain hf | hf := eq_zero_or_pos (∑ i ∈ s, f i ^ p)
    · simp [hf, hpq.ne_zero, hpq.symm.ne_zero]
    · have A : p + q - q ≠ 0 := by simp [hpq.ne_zero]
      have B : ∀ y : ℝ≥0, y * y ^ p / y = y ^ p := by
        refine fun y => mul_div_cancel_left_of_imp fun h => ?_
        simp [h, hpq.ne_zero]
      simp only [Set.mem_ofPred_eq, div_rpow, ← sum_div, ← rpow_mul,
        div_mul_cancel₀ _ hpq.symm.ne_zero, rpow_one, div_le_iff₀ hf, one_mul, hpq.mul_eq_add, ←
        rpow_sub' A, add_sub_cancel_right, le_refl, true_and, ← mul_div_assoc, B]
      rw [div_eq_iff, ← rpow_add hf.ne', one_div, one_div, hpq.inv_add_inv_eq_one, rpow_one]
      simpa [hpq.symm.ne_zero] using hf.ne'

Goal state after:
case right
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) ∈ upperBounds ((fun g ↦ ∑ i ∈ s, f i * g i) '' {g | ∑ i ∈ s, g i ^ q ≤ 1})
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hpq : p.HolderConjugate p.conjExponent
this :
  IsGreatest ((fun a ↦ ∑ x ∈ s, f x * a x + ∑ x ∈ s, g x * a x) '' {g | ∑ i ∈ s, g i ^ p.conjExponent ≤ 1})
    ((∑ x ∈ s, (f x + g x) ^ p) ^ (1 / p))
φ : ι → ℝ≥0
hφ : φ ∈ {g | ∑ i ∈ s, g i ^ p.conjExponent ≤ 1}
H : (fun a ↦ ∑ x ∈ s, f x * a x + ∑ x ∈ s, g x * a x) φ = (∑ x ∈ s, (f x + g x) ^ p) ^ (1 / p)
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)

Tactic:
rw [← H]

Goal state after:
case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hpq : p.HolderConjugate p.conjExponent
this :
  IsGreatest ((fun a ↦ ∑ x ∈ s, f x * a x + ∑ x ∈ s, g x * a x) '' {g | ∑ i ∈ s, g i ^ p.conjExponent ≤ 1})
    ((∑ x ∈ s, (f x + g x) ^ p) ^ (1 / p))
φ : ι → ℝ≥0
hφ : φ ∈ {g | ∑ i ∈ s, g i ^ p.conjExponent ≤ 1}
H : (fun a ↦ ∑ x ∈ s, f x * a x + ∑ x ∈ s, g x * a x) φ = (∑ x ∈ s, (f x + g x) ^ p) ^ (1 / p)
⊢ (fun a ↦ ∑ x ∈ s, f x * a x + ∑ x ∈ s, g x * a x) φ ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : SeminormedAddGroup E
ι : Type u_3
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → E
p : ℝ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
h_no_pow : ∫⁻ (a : α), ‖f_lim a‖ₑ ^ p ∂μ = ∫⁻ (a : α), liminf (fun m ↦ ‖f m a‖ₑ ^ p) atTop ∂μ
⊢ eLpNorm' f_lim p μ = (∫⁻ (a : α), liminf (fun x ↦ ‖f x a‖ₑ ^ p) atTop ∂μ) ^ (1 / p)

Tactic:
by
    rw [eLpNorm'_eq_lintegral_enorm, h_no_pow]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), ↑(f a) * ↑(g a) ∂μ ≤ (∫⁻ (a : α), ↑(f a) ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ↑(g a) ^ q ∂μ) ^ (1 / q)

Tactic:
exact ENNReal.lintegral_mul_le_Lp_mul_Lq μ hpq hf.coe_nnreal_ennreal hg.coe_nnreal_ennreal

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : SeminormedAddGroup E
ι : Type u_3
inst✝² : Nonempty ι
inst✝¹ : Countable ι
inst✝ : LinearOrder ι
f : ι → α → E
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
⊢ essSup (fun x ↦ liminf (fun m ↦ ‖f m x‖ₑ) atTop) μ ≤ liminf (fun n ↦ eLpNormEssSup (f n) μ) atTop

Tactic:
eLpNormEssSup

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : SeminormedAddGroup E
ι : Type u_3
inst✝² : Nonempty ι
inst✝¹ : Countable ι
inst✝ : LinearOrder ι
f : ι → α → E
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
⊢ essSup (fun x ↦ liminf (fun m ↦ ‖f m x‖ₑ) atTop) μ ≤ liminf (fun n ↦ essSup (fun x ↦ ‖f n x‖ₑ) μ) atTop
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
hp : 1 ≤ ∞
hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNormEssSup (f n - f m_1) μ < B N
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) atTop (𝓝 l)

Tactic:
eLpNormEssSup

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
hp : 1 ≤ ∞
hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → essSup (fun x ↦ ‖(f n - f m_1) x‖ₑ) μ < B N
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) atTop (𝓝 l)
Module: Mathlib.Data.Fintype.CardEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
⊢ ‖α ↪ β‖ = ‖β‖.descFactorial ‖α‖

Tactic:
refine Fintype.induction_empty_option (P := fun t ↦ ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖)
        (fun α₁ α₂ h₂ e ih ↦ ?_) (?_) (fun γ h ih ↦ ?_) α <;> clear! α

Goal state after:
case refine_1
β : Type u_2
inst✝ : Fintype β
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : ‖α₁ ↪ β‖ = ‖β‖.descFactorial ‖α₁‖
⊢ ‖α₂ ↪ β‖ = ‖β‖.descFactorial ‖α₂‖

case refine_2
β : Type u_2
inst✝ : Fintype β
⊢ ‖PEmpty.{u_1 + 1} ↪ β‖ = ‖β‖.descFactorial ‖PEmpty.{u_1 + 1}‖

case refine_3
β : Type u_2
inst✝ : Fintype β
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = ‖β‖.descFactorial ‖γ‖
⊢ ‖Option γ ↪ β‖ = ‖β‖.descFactorial ‖Option γ‖
Module: Mathlib.Analysis.Normed.Module.Span

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
x : E
c : 𝕜
⊢ ‖(toSpanSingleton 𝕜 E x) c‖ = ‖x‖ * ‖c‖

Tactic:
rw [mul_comm]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
x : E
c : 𝕜
⊢ ‖(toSpanSingleton 𝕜 E x) c‖ = ‖c‖ * ‖x‖
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝³ : RingHomInvPair σ₂₁ σ₁₂
inst✝² : RingHomIsometric σ₂₁
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : Nontrivial E
e : E ≃SL[σ₁₂] F
⊢ 1 ≤ ‖↑e‖ * ‖↑e.symm‖

Tactic:
rw [mul_comm]

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝³ : RingHomInvPair σ₂₁ σ₁₂
inst✝² : RingHomIsometric σ₂₁
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : Nontrivial E
e : E ≃SL[σ₁₂] F
⊢ 1 ≤ ‖↑e.symm‖ * ‖↑e‖
Module: Mathlib.Topology.Algebra.Module.Multilinear.Topology

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : (i : ι) → TopologicalSpace (E i)
inst✝¹² : (i : ι) → AddCommGroup (E i)
inst✝¹¹ : (i : ι) → Module 𝕜 (E i)
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : Module 𝕜 F
inst✝⁸ : UniformSpace F
inst✝⁷ : IsUniformAddGroup F
𝕜' : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜'
inst✝⁵ : NormedAlgebra 𝕜' 𝕜
inst✝⁴ : (i : ι) → Module 𝕜' (E i)
inst✝³ : ∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)
inst✝² : Module 𝕜' F
inst✝¹ : IsScalarTower 𝕜' 𝕜 F
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝¹⁴, non_trivial := ⋯ }
⊢ IsUniformEmbedding (toUniformOnFun ∘ restrictScalars 𝕜')

Tactic:
convert! isUniformEmbedding_toUniformOnFun using 4 with s

Goal state after:
case e'_4
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : (i : ι) → TopologicalSpace (E i)
inst✝¹² : (i : ι) → AddCommGroup (E i)
inst✝¹¹ : (i : ι) → Module 𝕜 (E i)
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : Module 𝕜 F
inst✝⁸ : UniformSpace F
inst✝⁷ : IsUniformAddGroup F
𝕜' : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜'
inst✝⁵ : NormedAlgebra 𝕜' 𝕜
inst✝⁴ : (i : ι) → Module 𝕜' (E i)
inst✝³ : ∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)
inst✝² : Module 𝕜' F
inst✝¹ : IsScalarTower 𝕜' 𝕜 F
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
this : NontriviallyNormedField 𝕜 := ⋯
s : Set ((i : ι) → E i)
⊢ IsVonNBounded 𝕜' s ↔ IsVonNBounded 𝕜 s
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
μ : Measure α
s : Finset β
f : β → Set α
⊢ μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)

Tactic:
by
  classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ hx IH =>
    simp only [hx, Finset.mem_insert, iUnion_iUnion_eq_or_left, not_false_eq_true,
      Finset.sum_insert]
    exact (measureReal_union_le _ _).trans (by gcongr)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : Fintype β
f : β → Set α
⊢ μ.real (⋃ b, f b) ≤ ∑ p, μ.real (f p)

Tactic:
convert! measureReal_biUnion_finset_le Finset.univ f

Goal state after:
case e'_3.e'_4
α : Type u_1
β : Type u_2
x✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : Fintype β
f : β → Set α
x✝ : β
⊢ f x✝ = ⋃ (_ : x✝ ∈ Finset.univ), f x✝
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: case ha
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h : μ s ≠ ∞
⊢ μ (s ∩ t) ≠ ∞

pp: case hb
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h : μ s ≠ ∞
⊢ μ (s \ t) ≠ ∞

Tactic:
· exact measure_ne_top_of_subset inter_subset_left h

Goal state after:
case hb
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h : μ s ≠ ∞
⊢ μ (s \ t) ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: case ha
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
h : μ s ≠ ∞
⊢ μ (s ∩ t) ≠ ∞

pp: case hb
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
h : μ s ≠ ∞
⊢ μ (s \ t) ≠ ∞

Tactic:
· exact measure_ne_top_of_subset inter_subset_left h

Goal state after:
case hb
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
h : μ s ≠ ∞
⊢ μ (s \ t) ≠ ∞