mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : ConditionallyCompleteLattice β
c : ℝ≥0∞
hc : c ≠ 0
f : α → β
⊢ essSup f (c • μ) = essSup f μ

Tactic:
by
  simp_rw [essSup, Measure.ae_ennreal_smul_measure_eq hc]

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 : MeasurableEmbedding f
hg_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
hgf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
c : β
h_le : ∀ᶠ (n : β) in map (g ∘ f) (ae μ), n ≤ c
⊢ ∀ᶠ (n : β) in map g (ae (Measure.map f μ)), n ≤ c

Tactic:
rw [eventually_map] at h_le ⊢

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : MeasurableEmbedding f
hg_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
hgf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
c : β
h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c
⊢ ∀ᵐ (a : γ) ∂Measure.map f μ, g a ≤ c
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 : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : Measurable g
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
hgf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
c : β
h_le : ∀ᶠ (n : β) in map (g ∘ f) (ae μ), n ≤ c
⊢ ∀ᶠ (n : β) in map g (ae (Measure.map f μ)), n ≤ c

Tactic:
rw [eventually_map] at h_le ⊢

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : Measurable g
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
hgf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
c : β
h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c
⊢ ∀ᵐ (a : γ) ∂Measure.map f μ, g a ≤ c
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
⊢ (uniformOn s) t = 0 ↔ s ∩ t = ∅

Tactic:
by
  simp [uniformOn, cond_apply hs.measurableSet, Measure.count_apply_eq_top, Set.not_infinite.2 hs,
    Measure.count_apply_finite _ (hs.inter_of_left _)]

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

Goal state before:
pp: case refine_1
⊢ Measurable fun p ↦ (↑p.1, p.2).1 ^ (↑p.1, p.2).2

Tactic:
simp_rw [ENNReal.coe_rpow_def]

Goal state after:
case refine_1
⊢ Measurable fun p ↦ if p.1 = 0 ∧ p.2 < 0 then ∞ else ↑(p.1 ^ p.2)
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]

Goal state after:
case refine_2
⊢ Measurable fun x ↦ if 0 < x then ∞ else if x = 0 then 1 else 0
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ∀ j ∈ Finset.univ,
    j ≠ i → (μ j).toOuterMeasure (eval j '' (t ∩ (fun b ↦ b i) ⁻¹' s)) ≤ (μ j).toOuterMeasure (eval j '' t)

Tactic:
rintro j - _

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ (μ j).toOuterMeasure (eval j '' (t ∩ (fun b ↦ b i) ⁻¹' s)) ≤ (μ j).toOuterMeasure (eval j '' t)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case refine_3
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ ∀ j ∈ Finset.univ,
    j ≠ i → (μ j).toOuterMeasure (eval j '' (t \ (fun b ↦ b i) ⁻¹' s)) ≤ (μ j).toOuterMeasure (eval j '' t)

Tactic:
rintro j - _

Goal state after:
case refine_3
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
j : ι
a✝ : j ≠ i
⊢ (μ j).toOuterMeasure (eval j '' (t \ (fun b ↦ b i) ⁻¹' s)) ≤ (μ j).toOuterMeasure (eval j '' t)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (Measure.pi μ) (univ.pi s) = ∏ i, (μ i) (s i)

Tactic:
refine le_antisymm ?_ ?_
  · rw [Measure.pi, toMeasure_apply _ _ (MeasurableSet.pi countable_univ fun i _ => hs i)]
    apply OuterMeasure.pi_pi_le
  · have : Encodable ι := Fintype.toEncodable ι
    simp_rw [← pi'_pi μ s, Measure.pi,
      toMeasure_apply _ _ (MeasurableSet.pi countable_univ fun i _ => hs i)]
    suffices (pi' μ).toOuterMeasure ≤ OuterMeasure.pi fun i => (μ i).toOuterMeasure by exact this _
    clear hs s
    rw [OuterMeasure.le_pi]
    intro s _
    exact (pi'_pi μ s).le

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

Goal state before:
pp: case pos
α : 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:
by_cases hg' : eLpNorm' g p μ = 0

Goal state after:
case pos
α : 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 = ∞
hg' : eLpNorm' g p μ = 0
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ

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 = ∞
hg' : ¬eLpNorm' g p μ = 0
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case refine_1.refine_1
α : 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)
⊢ IsCountablySpanning (univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s})

Tactic:
exact (FiniteSpanningSetsIn.pi (fun i ↦ (μ i).toFiniteSpanningSetsIn)).isCountablySpanning

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

Goal state before:
pp: x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ (rexp y - rexp x) / (y - x) < rexp y

Tactic:
div_lt_iff₀ h1

Goal state after:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ rexp y - rexp x < rexp y * (y - x)
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: x y z : ℝ
hxy : x < y
hyz : y < z
⊢ rexp y < (rexp z - rexp y) / (z - y)

Tactic:
· have h1 : 0 < z - y := by linarith
    rw [lt_div_iff₀ h1]
    calc
      exp y * (z - y) < exp y * (exp (z - y) - 1) := by
        gcongr _ * ?_
        linarith [add_one_lt_exp h1.ne']
      _ = exp (z - y) * exp y - exp y := by ring
      _ ≤ exp z - exp y := by rw [← exp_add]; ring_nf; rfl

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

Goal state before:
pp: case mp
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ p = ∞ → q = 1

Tactic:
rintro rfl
    rw [← inv_inv q, ← one_sub_inv ∞ q]
    simp

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

Goal state before:
pp: p q : ℝ
hp : 1 < p
h : p⁻¹ + q⁻¹ = 1
hp' : 0 < p
⊢ 0 < q

Tactic:
← inv_lt_one₀ hp',

Goal state after:
p q : ℝ
hp : p⁻¹ < 1
h : p⁻¹ + q⁻¹ = 1
hp' : 0 < p
⊢ 0 < q
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ 0 ≤ x / y

Tactic:
div_nonneg_iff

Goal state after:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < y - x
⊢ 0 ≤ x ∧ 0 ≤ y ∨ x ≤ 0 ∧ y ≤ 0
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 μ), x ≤ (eLpNormEssSup f μ).toNNReal

Tactic:
← ENNReal.coe_le_coe,

Goal state after:
α : 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 μ), ↑x ≤ ↑(eLpNormEssSup f μ).toNNReal
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < z - y
⊢ 0 ≤ z / y

Tactic:
div_nonneg_iff

Goal state after:
p : ℝ
hp : 1 < p
x y z : ℝ
hx : 0 ≤ x
hz : 0 ≤ z
hxy : x < y
hyz : y < z
hy : 0 < y
hy' : 0 < y ^ p
q : 0 < z - y
⊢ 0 ≤ z ∧ 0 ≤ y ∨ z ≤ 0 ∧ y ≤ 0
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
eLpNorm_eq_lintegral_rpow_enorm_toReal hp_zero hp_top,

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
hp_top : ¬p = ∞
⊢ (∫⁻ (x : β), ‖g x‖ₑ ^ p.toReal ∂Measure.map f μ) ^ (1 / p.toReal) =
    (∫⁻ (x : α), ‖(g ∘ f) x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
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:
· rw [exp_log hz]

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case e'_4
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
⊢ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p

Tactic:
have A : p - 1 ≠ 0 := ne_of_gt (sub_pos.2 h'p)

Goal state after:
case e'_4
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
h'p : 1 < p
A : p - 1 ≠ 0
⊢ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ 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:
by grind [geom_mean_eq_arith_mean_weighted_iff_of_pos' s w z hw hw' hz]

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

Goal state before:
pp: α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
⊢ eLpNormEssSup (f + g) μ ≤ eLpNormEssSup f μ + eLpNormEssSup g μ

Tactic:
refine le_trans (essSup_mono_ae (Eventually.of_forall fun x => ?_)) (ENNReal.essSup_add_le _ _)
  simp_rw [Pi.add_apply]
  exact enorm_add_le _ _

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

Goal state before:
pp: case hp
α : 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 ≤ p i₀

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 h2p i₀ <| mem_insert_self ..

Goal state after:
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₀

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.TriangleInequality

Goal state before:
pp: case inr.inr
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : 1 ≤ p
⊢ eLpNorm (f + g) p μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)

Tactic:
· simpa [LpAddConst_of_one_le h'p] using eLpNorm_add_le hf hg h'p

Goal state after:
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 : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hq_top : ¬q = ∞
hq_eq_zero : q = 0
hpq : 0 ≤ q
hp0 : 0 ≠ 0
hp_top : ¬0 = ∞
hp_pos : 0 < ENNReal.toReal 0
⊢ False

Tactic:
rw [ENNReal.toReal_zero] at hp_pos

Goal state after:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hq_top : ¬q = ∞
hq_eq_zero : q = 0
hpq : 0 ≤ q
hp0 : 0 ≠ 0
hp_top : ¬0 = ∞
hp_pos : 0 < 0
⊢ False
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : ∑ i ∈ s, f i ^ p ≤ 1
hg : ∑ i ∈ s, g i ^ q ≤ 1
⊢ ∑ i ∈ s, f i * g i ≤ 1

Tactic:
have hp : 0 < p.toNNReal := zero_lt_one.trans hpq.toNNReal.lt

Goal state after:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : ∑ i ∈ s, f i ^ p ≤ 1
hg : ∑ i ∈ s, g i ^ q ≤ 1
hp : 0 < p.toNNReal
⊢ ∑ i ∈ s, f i * g i ≤ 1
Module: Mathlib.Analysis.MeanInequalities

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

Tactic:
simp only [hf, hpq.ne_zero, one_div, sum_eq_zero_iff, zero_rpow, zero_mul,
    inv_eq_zero, Ne, not_false_iff, le_zero_iff, mul_eq_zero]

Goal state after:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : ∑ i ∈ s, f i ^ p = 0
⊢ ∀ i ∈ s, f i = 0 ∨ g i = 0
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 : 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)
this : ∑ i ∈ s, f' i * g' i ≤ 1
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Tactic:
by
    simp_rw [f', g', div_mul_div_comm, ← sum_div] at this
    rwa [div_le_iff₀, one_mul] at this
    positivity

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : SeminormedAddGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
⊢ eLpNorm f_lim p μ ≤ liminf (fun n ↦ eLpNorm (f n) p μ) atTop

Tactic:
obtain rfl | hp0 := eq_or_ne p 0
  · simp
  by_cases hp_top : p = ∞
  · simp_rw [hp_top]
    exact eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top h_lim
  simp_rw [eLpNorm_eq_eLpNorm' hp0 hp_top]
  have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0 hp_top
  exact eLpNorm'_lim_le_liminf_eLpNorm' hp_pos hf h_lim

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

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
hfg : f =ᵐ[μ] g
⊢ toLp f hf = toLp g hg

Tactic:
simp [toLp, hfg]

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ C
hμ : ¬μ = 0
⊢ ‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C

Tactic:
← ENNReal.coe_le_coe,

Goal state after:
case neg
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ C
hμ : ¬μ = 0
⊢ ↑‖f‖₊ ≤ ↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C)
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
⊢ ∀ᵐ (a : α) ∂μ, ↑↑(negPart f) a = max (-↑↑f a) 0

Tactic:
rw [negPart]
  filter_upwards [coeFn_posPart (-f), coeFn_neg f] with _ h₁ h₂
  rw [h₁, h₂, Pi.neg_apply]

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

Goal state before:
pp: case neg
α : 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) μ
hp : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
hp_top : ¬p = ∞
hp1 : 1 ≤ p.toReal
h_cau' : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p.toReal μ < B N
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) atTop (𝓝 l)

Tactic:
exact ae_tendsto_of_cauchy_eLpNorm' hf hp1 hB h_cau'

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
⊢ ∀ᶠ (t : R) in 𝓝 0, (↑x + t)⁻¹ʳ = (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹

Tactic:
Metric.eventually_nhds_iff

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
⊢ ∃ ε > 0, ∀ ⦃y : R⦄, dist y 0 < ε → (↑x + y)⁻¹ʳ = (1 + ↑x⁻¹ * y)⁻¹ʳ * ↑x⁻¹
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✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
ι : Type u_5
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ (𝓝 0).HasBasis (fun Si ↦ IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun Si ↦ {f | MapsTo (⇑f) Si.1 (b Si.2)}

Tactic:
nhds_induced

Goal state after:
𝕜 : 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✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
ι : Type u_5
p : ι → Prop
b : ι → Set F
h : (𝓝 0).HasBasis p b
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ (Filter.comap toUniformOnFun (𝓝 (toUniformOnFun 0))).HasBasis (fun Si ↦ IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun Si ↦
    {f | MapsTo (⇑f) Si.1 (b Si.2)}