mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_4
Eₗ : Type u_5
Fₗ : Type u_7
Gₗ : Type u_9
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : SeminormedAddCommGroup Fₗ
inst✝⁵ : SeminormedAddCommGroup Gₗ
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜 Eₗ
inst✝¹ : NormedSpace 𝕜 Fₗ
inst✝ : NormedSpace 𝕜 Gₗ
L : E →L[𝕜] Fₗ →L[𝕜] Gₗ
⊢ ‖precompL Eₗ L‖ ≤ ‖L‖

Tactic:
precompL,

Goal state after:
𝕜 : Type u_1
E : Type u_4
Eₗ : Type u_5
Fₗ : Type u_7
Gₗ : Type u_9
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : SeminormedAddCommGroup Fₗ
inst✝⁵ : SeminormedAddCommGroup Gₗ
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜 Eₗ
inst✝¹ : NormedSpace 𝕜 Fₗ
inst✝ : NormedSpace 𝕜 Gₗ
L : E →L[𝕜] Fₗ →L[𝕜] Gₗ
⊢ ‖(precompR Eₗ L.flip).flip‖ ≤ ‖L‖
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: f : Filter ℝ
hf : ¬IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
⊢ f.limsSup = 0

Tactic:
rw [limsSup]

Goal state after:
f : Filter ℝ
hf : ¬IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
⊢ sInf {a | ∀ᶠ (n : ℝ) in f, n ≤ a} = 0
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : μ s ≠ ∞
u : Set Ω
a✝ : MeasurableSet u
⊢ μ[|s][u | t] = μ[u | s ∩ t]

Tactic:
obtain hst | hst := eq_or_ne (μ (s ∩ t)) 0

Goal state after:
case inl
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : μ s ≠ ∞
u : Set Ω
a✝ : MeasurableSet u
hst : μ (s ∩ t) = 0
⊢ μ[|s][u | t] = μ[u | s ∩ t]

case inr
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
hcs : μ s ≠ ∞
u : Set Ω
a✝ : MeasurableSet u
hst : μ (s ∩ t) ≠ 0
⊢ μ[|s][u | t] = μ[u | s ∩ t]
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case pos
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf✝ : f.NeBot
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
c : ℝ
⊢ (∀ y < c, ∃ᶠ (a : ι) in f, y < ↑(u a)) ↔ c.toNNReal ≤ limsup u f

Tactic:
le_limsup_iff ‹_›

Goal state after:
case pos
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf✝ : f.NeBot
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
c : ℝ
⊢ (∀ y < c, ∃ᶠ (a : ι) in f, y < ↑(u a)) ↔ ∀ y < c.toNNReal, ∃ᶠ (a : ι) in f, y < u a
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
⊢ limsup (fun x ↦ u x * a) f = a * limsup u f

Tactic:
by
  simpa [mul_comm] using limsup_const_mul

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
⊢ StronglyMeasurable
    (if h : ∃ b, f = mk (const α b) ⋯ then const α (Classical.choose h)
    else AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯)

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ∃ b, f = mk (const α b) ⋯
⊢ StronglyMeasurable (const α (Classical.choose h))

case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ b, f = mk (const α b) ⋯
⊢ StronglyMeasurable (AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯)
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
⊢ mk
      (if h : ∃ b, f = mk (const α b) ⋯ then const α (Classical.choose h)
      else AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯)
      ⋯ =
    f

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ∃ b, f = mk (const α b) ⋯
⊢ mk (const α (Classical.choose h)) ⋯ = f

case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ b, f = mk (const α b) ⋯
⊢ mk (AEStronglyMeasurable.mk ↑(Quotient.out f) ⋯) ⋯ = f
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
⊢ (uniformOn {ω}) t = if ω ∈ t then 1 else 0

Tactic:
rw [uniformOn, cond_apply (measurableSet_singleton ω), Measure.count_singleton, inv_one,
    one_mul]
  split_ifs
  · rw [(by simpa : ({ω} : Set Ω) ∩ t = {ω}), Measure.count_singleton]
  · simpa

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case cons
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝³ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝² : (i : ι) → MeasurableSpace (α i)
μ✝ : (i : ι) → Measure (α i)
δ : Type u_4
X : δ → Type u_5
inst✝¹ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
i : δ
l : List δ
ih : SigmaFinite (Measure.tprod l μ)
⊢ SigmaFinite (Measure.tprod (i :: l) μ)

Tactic:
rw [tprod_cons]; exact @prod.instSigmaFinite _ _ _ _ _ _ _ ih

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
⊢ (if h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯ then Function.const α (Classical.choose h)
      else AEStronglyMeasurable.mk ↑(Quotient.out (const α b)) ⋯)
      x =
    b

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯
⊢ Function.const α (Classical.choose h) x = b

case neg
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
h : ¬∃ b_1, const α b = mk (Function.const α b_1) ⋯
⊢ AEStronglyMeasurable.mk ↑(Quotient.out (const α b)) ⋯ x = b
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
b : β
⊢ ∃ b',
    (if h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯ then Function.const α (Classical.choose h)
      else AEStronglyMeasurable.mk ↑(Quotient.out (const α b)) ⋯) =
      fun x ↦ b'

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
b : β
h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯
⊢ ∃ b', Function.const α (Classical.choose h) = fun x ↦ b'

case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
b : β
h : ¬∃ b_1, const α b = mk (Function.const α b_1) ⋯
⊢ ∃ b', AEStronglyMeasurable.mk ↑(Quotient.out (const α b)) ⋯ = fun x ↦ b'
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: case refine_2
⊢ Measurable fun x ↦ if x = 0 then 1 else 0

Tactic:
exact Measurable.ite (measurableSet_singleton 0) measurable_const measurable_const

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
c : ε
s : Set α
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
⊢ (∫⁻ (x : α), ‖s.indicator (fun x ↦ c) x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) =
    (∫⁻ (x : α), s.indicator (fun x ↦ ‖c‖ₑ ^ p.toReal) x ∂μ) ^ (1 / p.toReal)

Tactic:
congr 2
      refine (Set.comp_indicator_const c (fun x ↦ (‖x‖ₑ) ^ p.toReal) ?_)
      simp [hp_pos]

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ

Tactic:
have : c ^ p ≠ ⊤ := by simp [hp.le, hc]

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
this : c ^ p ≠ ∞
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inr.inr.inr
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ 1 + s < 1 + p * s

Tactic:
gcongr
      exact lt_mul_of_one_lt_left hs' hp

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inr.inl
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + s) * p < log (1 + p * s)

Tactic:
rw [← lt_div_iff₀ hp1, ← div_lt_div_right_of_neg hs']

Goal state after:
case inr.inl
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + p * s) / p / s < log (1 + s) / s
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: a : ℝ≥0
ha₀ : 0 < a
ha₁ : a < 1
⊢ a⁻¹⁻¹ + (1 - a)⁻¹⁻¹ = 1

Tactic:
simpa using add_tsub_cancel_of_le ha₁.le

Goal state after:
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
⊢ (f y - f a) / (y - a) < (f x - f a) / (x - a)

Tactic:
have key := hf.neg.secant_strict_mono ha hx hy hxa hya hxy

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConcaveOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy : x < y
key : ((-f) x - (-f) a) / (x - a) < ((-f) y - (-f) a) / (y - a)
⊢ (f y - f a) / (y - a) < (f x - f a) / (x - a)
Module: Mathlib.Algebra.Order.Monovary

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f g : ι → α
s : Set ι
⊢ AntivaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) * (g j - g i) ≤ 0

Tactic:
by
  simp only [smul_eq_mul, antivaryOn_iff_forall_smul_nonpos]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_3.inl
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz✝ : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
this : ∏ x ∈ s, rexp (log (z x) * w x) ≤ ∑ x ∈ s, w x * rexp (log (z x))
i : ι
hi : i ∈ s
hz : 0 = z i
⊢ z i ^ w i = rexp (log (z i) * w i)

pp: case e'_3.inr
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz✝ : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
this : ∏ x ∈ s, rexp (log (z x) * w x) ≤ ∑ x ∈ s, w x * rexp (log (z x))
i : ι
hi : i ∈ s
hz : 0 < z i
⊢ z i ^ w i = rexp (log (z i) * w i)

Tactic:
· simp [A i hi hz.symm]

Goal state after:
case e'_3.inr
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz✝ : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
this : ∏ x ∈ s, rexp (log (z x) * w x) ≤ ∑ x ∈ s, w x * rexp (log (z x))
i : ι
hi : i ∈ s
hz : 0 < z i
⊢ z i ^ w i = rexp (log (z i) * w i)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_4.inl
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz✝ : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
this : ∏ x ∈ s, rexp (log (z x) * w x) ≤ ∑ x ∈ s, w x * rexp (log (z x))
i : ι
hi : i ∈ s
hz : 0 = z i
⊢ w i * z i = w i * rexp (log (z i))

pp: case e'_4.inr
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz✝ : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
this : ∏ x ∈ s, rexp (log (z x) * w x) ≤ ∑ x ∈ s, w x * rexp (log (z x))
i : ι
hi : i ∈ s
hz : 0 < z i
⊢ w i * z i = w i * rexp (log (z i))

Tactic:
· simp [A i hi hz.symm]

Goal state after:
case e'_4.inr
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz✝ : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
this : ∏ x ∈ s, rexp (log (z x) * w x) ≤ ∑ x ∈ s, w x * rexp (log (z x))
i : ι
hi : i ∈ s
hz : 0 < z i
⊢ w i * z i = w i * rexp (log (z i))
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
this : 0 < p
⊢ (∑ i ∈ s, w i * z i) ^ p ≤ ((∑ i ∈ s, w i * z i ^ p) ^ (1 / p)) ^ p

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
this : 0 < p
⊢ 0 ≤ ∑ i ∈ s, w i * z i

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
this : 0 < p
⊢ 0 ≤ (∑ i ∈ s, w i * z i ^ p) ^ (1 / p)

Tactic:
← rpow_mul,

Goal state after:
ι : 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
this : 0 < p
⊢ (∑ i ∈ s, w i * z i) ^ p ≤ (∑ i ∈ s, w i * z i ^ p) ^ (1 / p * p)

case hx
ι : 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
this : 0 < p
⊢ 0 ≤ ∑ i ∈ s, w i * z i ^ p

ι : 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
this : 0 < p
⊢ 0 ≤ ∑ i ∈ s, w i * z i

ι : 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
this : 0 < p
⊢ 0 ≤ (∑ i ∈ s, w i * z i ^ p) ^ (1 / p)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 < p
f : α → ℝ≥0∞
a : α
⊢ (((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)) ^ p)⁻¹ = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹

Tactic:
← rpow_mul,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 < p
f : α → ℝ≥0∞
a : α
⊢ ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p * p))⁻¹ = (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case inl
z₁ z₂ : ℝ≥0
hp : 1 ≤ 1
⊢ (z₁ + z₂) ^ 1 ≤ 2 ^ (1 - 1) * (z₁ ^ 1 + z₂ ^ 1)

pp: case inr
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ (z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)

Tactic:
· simp only [rpow_one, sub_self, rpow_zero, one_mul]; rfl

Goal state after:
case inr
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ (z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : ∑ i ∈ s, w i = 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
h_top_rpow_sum : (∑ i ∈ s, w i * z i) ^ p ≠ ∞
a✝ : ∑ i ∈ s, w i * z i ^ p ≠ ∞
⊢ ∑ i ∈ s, w i * z i ≠ ∞

Tactic:
intro h
        rw [h, top_rpow_of_pos hp_pos] at h_top_rpow_sum
        exact h_top_rpow_sum rfl

Goal state after:
Module: Mathlib.Analysis.Convex.Mul

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁸ : CommRing 𝕜
inst✝¹⁷ : LinearOrder 𝕜
inst✝¹⁶ : IsStrictOrderedRing 𝕜
inst✝¹⁵ : CommRing E
inst✝¹⁴ : LinearOrder E
inst✝¹³ : IsStrictOrderedRing E
inst✝¹² : AddCommGroup F
inst✝¹¹ : LinearOrder F
inst✝¹⁰ : IsOrderedAddMonoid F
inst✝⁹ : AddCommGroup G
inst✝⁸ : Module 𝕜 G
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : IsOrderedModule 𝕜 F
inst✝¹ : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
inst✝ : IsOrderedModule 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
⊢ ConcaveOn 𝕜 s (f • g)

Tactic:
refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ ?_⟩
  dsimp
  refine (smul_le_smul (hf.2 hx hy ha hb hab) (hg.2 hx hy ha hb hab)
    (add_nonneg (smul_nonneg ha <| hf₀ hx) <| smul_nonneg hb <| hf₀ hy)
    (hg₀ <| hf.1 hx hy ha hb hab)).trans' ?_
  calc a • f x • g x + b • f y • g y
        = (a * (a + b)) • (f x • g x) + (b * (a + b)) • (f y • g y) := by simp_rw [hab, mul_one]
    _ = (a * a) • (f x • g x) + (b * b) • (f y • g y) + (a * b) • (f x • g x + f y • g y) := by
        simp only [mul_add, add_smul, smul_add, mul_comm _ a]; abel
    _ ≤ (a * a) • (f x • g x) + (b * b) • (f y • g y) + (a * b) • (f x • g y + f y • g x) := by
        gcongr _ + (a * b) • ?_; exact hfg.smul_add_smul_le_smul_add_smul hx hy
    _ = _ := ?_
  simp only [add_smul, smul_add]
  rw [← smul_smul_smul_comm a, ← smul_smul_smul_comm b, ← smul_smul_smul_comm a b,
    ← smul_smul_smul_comm b b, smul_eq_mul, smul_eq_mul, smul_eq_mul, smul_eq_mul, mul_comm b a,
    add_comm ((a * b) • f x • g y), add_comm ((a * b) • f x • g y), add_add_add_comm]

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p : ℝ≥0∞
⊢ (if p ∈ Set.Ioo 0 1 then 2 ^ (1 / p.toReal - 1) else 1) < ∞

Tactic:
split_ifs with h

Goal state after:
case pos
p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ 2 ^ (1 / p.toReal - 1) < ∞

case neg
p : ℝ≥0∞
h : p ∉ Set.Ioo 0 1
⊢ 1 < ∞
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case hq
α : 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 : ι → ℝ := ⋯
hq : ∑ i ∈ s, q i = 1
h2q : ∀ i ∈ s, 0 ≤ q i
⊢ 0 ≤ 1 - p i₀

pp: case hpq
α : 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 : ι → ℝ := ⋯
hq : ∑ i ∈ s, q i = 1
h2q : ∀ i ∈ s, 0 ≤ q i
⊢ p i₀ + (1 - p i₀) = 1

Tactic:
· exact hpi₀

Goal state after:
case hpq
α : 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 : ι → ℝ := ⋯
hq : ∑ i ∈ s, q i = 1
h2q : ∀ i ∈ s, 0 ≤ q i
⊢ p i₀ + (1 - p i₀) = 1
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
q : ℝ
hq_pos : 0 < q
h_le : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ ∫⁻ (x : α), eLpNormEssSup f μ ^ q ∂μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) ≤ eLpNormEssSup f μ ^ 1 * μ Set.univ ^ (1 / q)

Tactic:
nth_rw 2 [← mul_inv_cancel₀ (ne_of_lt hq_pos).symm]

Goal state after:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
q : ℝ
hq_pos : 0 < q
h_le : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ ∫⁻ (x : α), eLpNormEssSup f μ ^ q ∂μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) ≤ eLpNormEssSup f μ ^ (q * q⁻¹) * μ Set.univ ^ (1 / q)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case refine_1.none
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
hi : none ∈ insertNone s
⊢ AEMeasurable (fun t ↦ none.elim (g t) fun j ↦ f j t) μ

Tactic:
exact hg

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
hp1 : 1 ≤ p
⊢ ∫⁻ (a : α), (f + g) a ^ p ∂μ < ∞

Tactic:
by
  calc
    (∫⁻ a : α, (f a + g a) ^ p ∂μ) ≤
        ∫⁻ a, (2 : ℝ≥0∞) ^ (p - 1) * f a ^ p + (2 : ℝ≥0∞) ^ (p - 1) * g a ^ p ∂μ := by
      refine lintegral_mono fun a => ?_
      simpa [mul_add] using ENNReal.rpow_add_le_mul_rpow_add_rpow (f a) (g a) hp1
    _ < ⊤ := by
      rw [lintegral_add_left', lintegral_const_mul'' _ (hf.pow_const p),
        lintegral_const_mul' _ _ (by finiteness), ENNReal.add_lt_top]
      · constructor <;> finiteness
      · fun_prop

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ eLpNorm (fun x ↦ b (f x) (g x)) p μ ≤ ↑c * eLpNorm f ∞ μ * eLpNorm g p μ

Tactic:
by
  calc
    eLpNorm (fun x => b (f x) (g x)) p μ ≤ eLpNorm (fun x => (c : ℝ) • ‖f x‖ * ‖g x‖) p μ :=
      eLpNorm_mono_ae_real h
    _ ≤ c * eLpNorm f ∞ μ * eLpNorm g p μ := ?_
  simp only [smul_mul_assoc, ← Pi.smul_def, eLpNorm_const_smul]
  rw [Real.enorm_eq_ofReal c.coe_nonneg, ENNReal.ofReal_coe_nnreal, mul_assoc]
  gcongr
  obtain (rfl | rfl | hp) := ENNReal.trichotomy p
  · simp
  · rw [← eLpNorm_norm f, ← eLpNorm_norm g]
    simp_rw [eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm, enorm_mul, enorm_norm]
    exact ENNReal.essSup_mul_le (‖f ·‖ₑ) (‖g ·‖ₑ)
  obtain ⟨hp₁, hp₂⟩ := ENNReal.toReal_pos_iff.mp hp
  simp_rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp₁.ne' hp₂.ne, eLpNorm_exponent_top,
    eLpNormEssSup, one_div, ENNReal.rpow_inv_le_iff hp, enorm_mul, enorm_norm]
  rw [ENNReal.mul_rpow_of_nonneg (hz := hp.le), ENNReal.rpow_inv_rpow hp.ne',
    ← lintegral_const_mul'' _ (by fun_prop)]
  simp only [← ENNReal.mul_rpow_of_nonneg (hz := hp.le)]
  apply lintegral_mono_ae
  filter_upwards [h, enorm_ae_le_eLpNormEssSup f μ] with x hb hf
  gcongr
  exact hf

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inr.inr.refine_1
ι : 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, f i ^ p) / ((∑ i ∈ s, f i ^ p) ^ (1 / p)) ^ p = 1

Tactic:
← rpow_mul,

Goal state after:
case inr.inr.refine_1
ι : 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, f i ^ p) / (∑ i ∈ s, f i ^ p) ^ (1 / p * p) = 1