mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F✝ : Type u_4
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F✝
inst✝⁶ : Module 𝕜₂ F✝
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : UniformSpace F
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : CompleteSpace F
hF : T2Space F
⊢ IsClosed[(UniformOnFun.uniformSpace E F 𝔖).toTopologicalSpace] (range (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe))

Tactic:
have H₁ : IsClosed {f : E →ᵤ[𝔖] F | Continuous ((UniformOnFun.toFun 𝔖) f)} :=
    UniformOnFun.isClosed_setOfPred_continuous h𝔖

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F✝ : Type u_4
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F✝
inst✝⁶ : Module 𝕜₂ F✝
𝔖 : Set (Set E)
h𝔖 : IsCoherentWith 𝔖
h𝔖U : ⋃₀ 𝔖 = univ
F : Type u_4
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
inst✝³ : UniformSpace F
inst✝² : IsUniformAddGroup F
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : CompleteSpace F
hF : T2Space F
H₁ :
  IsClosed[UniformOnFun.topologicalSpace E F 𝔖]
    {f | Continuous[inst✝⁸, inst✝³.toTopologicalSpace] ((UniformOnFun.toFun 𝔖) f)}
⊢ IsClosed[(UniformOnFun.uniformSpace E F 𝔖).toTopologicalSpace] (range (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe))
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
hbdd : ∀ y ∈ (fun x ↦ ‖f x‖₊) '' closedBall 0 1, y ≤ ‖f‖₊
⊢ sSup ((fun x ↦ ‖f x‖₊) '' closedBall 0 1) = ‖f‖₊

Tactic:
refine le_antisymm (csSup_le ((nonempty_closedBall.mpr zero_le_one).image _) hbdd) ?_

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
hbdd : ∀ y ∈ (fun x ↦ ‖f x‖₊) '' closedBall 0 1, y ≤ ‖f‖₊
⊢ ‖f‖₊ ≤ sSup ((fun x ↦ ‖f x‖₊) '' closedBall 0 1)
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
K : Set X
hK : IsCompact K
⊢ ContinuousOn (⇑(CompactCoherentification.mk X)) K

Tactic:
rw [continuousOn_iff_continuous_domRestrict]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
K : Set X
hK : IsCompact K
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpace] (K.domRestrict ⇑(CompactCoherentification.mk X))
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: case inr
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hms : MeasurableSet s
hcs' : μ s ≠ ∞
t : Set Ω
hcs : μ s ≠ 0
⊢ μ[t | s] * μ s = μ (s ∩ t)

Tactic:
· rw [cond_apply hms, mul_comm, ← mul_assoc, ENNReal.mul_inv_cancel hcs hcs', one_mul]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : TopologicalSpace α
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
inst✝¹ : Field 𝕜
inst✝ : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : f x - f y ≠ 0
⊢ ∃ f ∈ ↑s, f x = v x ∧ f y = v y

Tactic:
let a := v x

Goal state after:
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
𝕜 : Type u_5
inst✝² : TopologicalSpace 𝕜
inst✝¹ : Field 𝕜
inst✝ : IsTopologicalRing 𝕜
s : Subalgebra 𝕜 C(α, 𝕜)
h : s.SeparatesPoints
v : α → 𝕜
x y : α
n : ¬x = y
f : C(α, 𝕜)
hf : f ∈ ↑s
hxy : f x - f y ≠ 0
a : 𝕜 := v x
⊢ ∃ f ∈ ↑s, f x = v x ∧ f y = v y
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝ : f.NeBot
u : α → ℝ≥0∞
C : ℝ≥0
hf : ∀ᶠ (a : α) in f, u a ≤ ↑C
⊢ ENNReal.ofReal (limsup (fun a ↦ (u a).toReal) f) = limsup u f

Tactic:
by
  have h₁ : IsCoboundedUnder (· ≤ ·) f (fun a ↦ (u a).toReal) :=
    IsCoboundedUnder.of_frequently_ge <| .of_forall fun _ ↦ by positivity
  have h₂ : IsBoundedUnder (· ≤ ·) f (fun a ↦ (u a).toReal) := by
    refine isBoundedUnder_of_eventually_le (a := C) ?_
    filter_upwards [hf] with a ha
    exact ENNReal.toReal_le_coe_of_le_coe ha
  refine (ENNReal.ofReal_limsup h₁ h₂).trans (limsup_congr ?_)
  filter_upwards [hf] with x hx
  exact ENNReal.ofReal_toReal (ne_top_of_le_ne_top (by simp : C ≠ ∞) hx)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f μ
hgf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
⊢ essSup (g ∘ f) μ ≤ essSup g (Measure.map f μ)

Tactic:
refine limsSup_le_limsSup_of_le ?_ hgf hg
  rw [← map_map]
  exact map_mono (Measure.tendsto_ae_map hf)

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: case pos
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : s ∩ t = ∅
⊢ (uniformOn s) (t ∩ u) = (uniformOn (s ∩ t)) u * (uniformOn s) t

Tactic:
hst,

Goal state after:
case pos
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : s ∩ t = ∅
⊢ (uniformOn s) (t ∩ u) = (uniformOn ∅) u * (uniformOn s) t
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: case pos
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : s ∩ t = ∅
⊢ s ∩ t ∩ u = ∅

Tactic:
hst,

Goal state after:
case pos
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : s ∩ t = ∅
⊢ ∅ ∩ u = ∅
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹⁴ : MeasurableSpace α
μ : Measure α
inst✝¹³ : TopologicalSpace δ
inst✝¹² : TopologicalSpace β
inst✝¹¹ : TopologicalSpace γ
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : PseudoMetrizableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : MeasurableSpace γ
inst✝⁶ : PseudoMetrizableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : SecondCountableTopologyEither β γ
inst✝³ : MeasurableSpace δ
inst✝² : PseudoMetrizableSpace δ
inst✝¹ : OpensMeasurableSpace δ
inst✝ : SecondCountableTopology δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ comp₂Measurable g hg f₁ f₂ = mk (fun a ↦ g (↑f₁ a) (↑f₂ a)) ⋯

Tactic:
by
  rw [comp₂Measurable_eq_pair, pair_eq_mk, compMeasurable_mk]; rfl

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : MeasurableSingletonClass Ω
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : Finite Ω
f : ι → Set Ω
⊢ uniformOn (Set.univ.pi f) = Measure.pi fun i ↦ uniformOn (f i)

Tactic:
refine (MeasureTheory.Measure.pi_eq fun t ht ↦ ?_).symm

Goal state after:
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : MeasurableSingletonClass Ω
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : Finite Ω
f t : ι → Set Ω
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ (uniformOn (Set.univ.pi f)) (Set.univ.pi t) = ∏ i, (uniformOn (f i)) (t i)
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: case refine_2
⊢ Measurable fun x ↦ (∞, x).1 ^ (∞, x).2

Tactic:
simp_rw [ENNReal.top_rpow_def]
    refine Measurable.ite measurableSet_Ioi measurable_const ?_
    exact Measurable.ite (measurableSet_singleton 0) measurable_const measurable_const

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

Goal state before:
pp: α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → μ {x | ‖f x‖ₑ = ∞} = 0
⊢ μ {x | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal

Tactic:
by_cases h : ε = ∞
  · have : (0 : ℝ≥0∞) ^ p.toReal = 0 := by
      rw [ENNReal.zero_rpow_of_pos (ENNReal.toReal_pos hp_ne_zero hp_ne_top)]
    simp [h, this, hmeas_top]
  · have hεpow : ε ^ p.toReal ≠ 0 := (ENNReal.rpow_pos (pos_iff_ne_zero.2 hε) h).ne.symm
    have hεpow' : ε ^ p.toReal ≠ ∞ := by finiteness
    rw [ENNReal.inv_rpow, ← ENNReal.mul_le_mul_iff_right hεpow hεpow', ← mul_assoc,
      ENNReal.mul_inv_cancel hεpow hεpow', one_mul]
    exact mul_meas_ge_le_pow_eLpNorm' μ hp_ne_zero hp_ne_top hf ε

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ μ {x | ε ≤ ↑‖f x‖₊} < ∞

Tactic:
by
  by_cases h : ε = ∞
  · simp [h]
  exact hℒp.meas_ge_lt_top'_enorm hp_ne_zero hp_ne_top hε (by simp)

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝ : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
this : (fun x i ↦ f i (x i)) ⁻¹' univ.pi s = univ.pi fun i ↦ f i ⁻¹' s i
⊢ ∏ i, (μ i) (f i ⁻¹' s i) = ∏ i, (map (f i) (μ i)) (s i)

Tactic:
congr with i

Goal state after:
case e_f
ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝ : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
this : (fun x i ↦ f i (x i)) ⁻¹' univ.pi s = univ.pi fun i ↦ f i ⁻¹' s i
i : ι
⊢ (μ i) (f i ⁻¹' s i) = (map (f i) (μ i)) (s i)
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 ε
s : Set α
f : α → ε
inst✝ : DecidablePred fun x ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
x : α
hx : x ∈ sᶜ
⊢ ‖s.piecewise f g x‖ₑ ^ p.toReal = ‖g x‖ₑ ^ p.toReal

Tactic:
have hx' : x ∉ s := hx

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst✝ : DecidablePred fun x ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
x : α
hx : x ∈ sᶜ
hx' : x ∉ s
⊢ ‖s.piecewise f g x‖ₑ ^ p.toReal = ‖g x‖ₑ ^ p.toReal
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : 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 : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
hxz' : x ≠ z
ha : 0 < (z - y) / (z - x)
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)

Tactic:
have hb : 0 < (y - x) / (z - x) := by positivity

Goal state after:
𝕜 : 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 : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
hxz' : x ≠ z
ha : 0 < (z - y) / (z - x)
hb : 0 < (y - x) / (z - x)
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: α₁ : Type u_4
β₁ : Type u_5
α₂ : Type u_6
β₂ : Type u_7
inst✝⁴ : Fintype α₁
inst✝³ : Fintype α₂
inst✝² : MeasurableSpace β₁
inst✝¹ : MeasurableSpace β₂
μ : α₁ → Measure β₁
ν : α₂ → Measure β₂
inst✝ : ∀ (i : α₂), SigmaFinite (ν i)
eα : α₁ ≃ α₂
eβ : β₁ ≃ᵐ β₂
hm : ∀ (i : α₁), MeasurePreserving (⇑eβ) (μ i) (ν (eα i))
⊢ MeasurePreserving (⇑(MeasurableEquiv.arrowCongr' eα eβ)) (Measure.pi fun i ↦ μ i) (Measure.pi fun i ↦ ν i)

Tactic:
convert!
    (measurePreserving_piCongrLeft (fun i : α₂ ↦ ν i) eα).comp
      (measurePreserving_pi μ (fun i : α₁ ↦ ν (eα i)) hm)

Goal state after:
α₁ : Type u_4
β₁ : Type u_5
α₂ : Type u_6
β₂ : Type u_7
inst✝⁴ : Fintype α₁
inst✝³ : Fintype α₂
inst✝² : MeasurableSpace β₁
inst✝¹ : MeasurableSpace β₂
μ : α₁ → Measure β₁
ν : α₂ → Measure β₂
inst✝ : ∀ (i : α₂), SigmaFinite (ν i)
eα : α₁ ≃ α₂
eβ : β₁ ≃ᵐ β₂
hm : ∀ (i : α₁), MeasurePreserving (⇑eβ) (μ i) (ν (eα i))
⊢ ⇑(MeasurableEquiv.arrowCongr' eα eβ) = ⇑(MeasurableEquiv.piCongrLeft (fun i ↦ β₂) eα) ∘ fun a i ↦ eβ (a i)
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hz : 0 < z
hxy : x < y
hyz : y < z
hy : 0 < y
h : 0 < z - y
hyz' : 0 < z / y
hyz'' : z / y ≠ 1
⊢ log z - log y = log (z / y)

Tactic:
by rw [← log_div hz.ne' hy.ne']

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✝ : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ

Tactic:
by
  by_cases hp0 : p = 0
  · simp [hp0]
  by_cases hp_top : p = ∞
  · simp only [hp_top, eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm]
    exact ENNReal.essSup_restrict_eq_of_support_subset fun x hx ↦ hsf <| enorm_ne_zero.1 hx
  · simp_rw [eLpNorm_eq_eLpNorm' hp0 hp_top, eLpNorm'_eq_lintegral_enorm]
    congr 1
    apply setLIntegral_eq_of_support_subset
    have : ¬(p.toReal ≤ 0) := by simpa only [not_le] using ENNReal.toReal_pos hp0 hp_top
    simpa [this] using hsf

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 : 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)
⊢ (z - x) * f y < (z - y) * f x + (y - x) * f z

Tactic:
have hb : 0 < (y - x) / (z - x) := by positivity

Goal state after:
𝕜 : 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)
⊢ (z - x) * f y < (z - y) * f x + (y - x) * f z
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
h : eLpNormEssSup f μ < ∞
⊢ ∀ᶠ (x : ℝ≥0) in map (fun x ↦ ‖f x‖₊) (ae μ), (fun x1 x2 ↦ x1 ≤ x2) x (eLpNormEssSup f μ).toNNReal

Tactic:
by
    simp_rw [← ENNReal.coe_le_coe, ENNReal.coe_toNNReal h.ne]; exact ae_le_eLpNormEssSup

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case pos
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ 0 ≤ ∑ i ∈ s, w i * z i

Tactic:
exact sum_nonneg fun j hj => mul_nonneg (hw j hj) (hz j hj)

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p q : ℝ
a✝ b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0
⊢ a ^ q = a ^ (p * p⁻¹ * q)

Tactic:
mul_inv_cancel₀ hp_pos.ne.symm,

Goal state after:
p q : ℝ
a✝ b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0
⊢ a ^ q = a ^ (1 * q)
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p

Tactic:
refine rpow_add_rpow_le_add (a ^ p) (b ^ p) ?_

Goal state after:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
⊢ 1 ≤ q / p
Module: Mathlib.Analysis.MeanInequalities

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
⊢ ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, ∀ k ∈ s, z j = z k

Tactic:
refine ⟨by grind [geom_mean_eq_arith_mean_weighted_iff_of_pos' s w z hw hw' hz], fun h ↦ ?_⟩

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
h : ∀ j ∈ s, ∀ k ∈ s, z j = z k
⊢ ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p

Tactic:
refine rpow_add_rpow_le_add (a ^ p) (b ^ p) ?_

Goal state after:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
⊢ 1 ≤ q / p
Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp : 1 ≤ p
⊢ eLpNorm (f - g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ

Tactic:
by
  simpa [LpAddConst_of_one_le hp] using eLpNorm_sub_le' hf hg p

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 μ
a : α
h_zero : ¬(f + g) a = 0
h_top : (f + g) a = ∞
⊢ (f + g) a ^ p ≤ (f + g) a * (f + g) a ^ (p - 1)

pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
a : α
h_zero : ¬(f + g) a = 0
h_top : ¬(f + g) a = ∞
⊢ (f + g) a ^ p ≤ (f + g) a * (f + g) a ^ (p - 1)

Tactic:
· rw [h_top, ENNReal.top_rpow_of_pos hpq.sub_one_pos, ENNReal.top_mul_top]
        exact le_top

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
a : α
h_zero : ¬(f + g) a = 0
h_top : ¬(f + g) a = ∞
⊢ (f + g) a ^ p ≤ (f + g) a * (f + g) a ^ (p - 1)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : 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 ∈ s, f i * g i = ∑ i ∈ s, g i * f i

Tactic:
congr with i

Goal state after:
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)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q) =
    ((∑ i ∈ s, f i ^ p) ^ (r / p) * (∑ i ∈ s, g i ^ q) ^ (r / q)) ^ (1 / r)

Tactic:
have hr := hpqr.pos'.ne'

Goal state after:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hr : r ≠ 0
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q) =
    ((∑ i ∈ s, f i ^ p) ^ (r / p) * (∑ i ∈ s, g i ^ q) ^ (r / q)) ^ (1 / r)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inr.calc_1
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
⊢ ∑ i ∈ s, w i * f i = ∑ i ∈ s, w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i)

Tactic:
congr with i

Goal state after:
case inr.calc_1.e_f
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
i : ι
⊢ ↑(w i * f i) = ↑(w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i))
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ q
⊢ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q) =
    ((∑' (i : ι), f i ^ p) ^ (r / p) * (∑' (i : ι), g i ^ q) ^ (r / q)) ^ (1 / r)

Tactic:
have hr := hpqr.pos'.ne'

Goal state after:
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ q
hr : r ≠ 0
⊢ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q) =
    ((∑' (i : ι), f i ^ p) ^ (r / p) * (∑' (i : ι), g i ^ q) ^ (r / q)) ^ (1 / r)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp : 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:
rcases eq_or_lt_of_le hp with (rfl | hp)
  · simp [Finset.sum_add_distrib]
  have hpq := Real.HolderConjugate.conjExponent hp
  have := isGreatest_Lp s (f + g) hpq
  simp only [Pi.add_apply, add_mul, sum_add_distrib] at this
  rcases this.1 with ⟨φ, hφ, H⟩
  rw [← H]
  exact add_le_add ((isGreatest_Lp s f hpq).2 ⟨φ, hφ, rfl⟩) ((isGreatest_Lp s g hpq).2 ⟨φ, hφ, rfl⟩)

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 q r : ℝ≥0∞
f : α → E
g : α → F
b : E → F → G
c : ℝ≥0
hf : MemLp f p μ
hg : MemLp g q μ
h : AEStronglyMeasurable (fun x ↦ b (f x) (g x)) μ
hb : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr : p.HolderTriple q r
⊢ eLpNorm (fun x ↦ b (f x) (g x)) r μ < ∞

Tactic:
apply (eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm hf.1 hg.1 b c hb (hpqr := hpqr)).trans_lt

Goal state after:
α : 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 q r : ℝ≥0∞
f : α → E
g : α → F
b : E → F → G
c : ℝ≥0
hf : MemLp f p μ
hg : MemLp g q μ
h : AEStronglyMeasurable (fun x ↦ b (f x) (g x)) μ
hb : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr : p.HolderTriple q r
⊢ ↑c * eLpNorm f p μ * eLpNorm g q μ < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case cons
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x✝ : MeasurableSpace α
inst✝ : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : (∀ i ∈ s, MemLp (f i) (p i) μ) → MemLp (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ
hf : ∀ i_1 ∈ cons i s hi, MemLp (f i_1) (p i_1) μ
⊢ MemLp (∏ i ∈ cons i s hi, f i) (∑ i ∈ cons i s hi, (p i)⁻¹)⁻¹ μ

Tactic:
| cons i s hi ih =>

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 μ
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ + ∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

Tactic:
rw [← lintegral_add_left' (hf.pow_const p)]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p + g a ^ p ∂μ) ^ (1 / p)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_3.a
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ f i * g i = |f i * g i|

Tactic:
abs_of_nonneg (mul_nonneg (hf i hi) (hg i hi))

Goal state after:
case e'_3.a
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ f i * g i = f i * g i