mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
K : Set (𝐤X)
⊢ IsCompact K ↔ IsCompact (⇑(CompactCoherentification.mk X) ⁻¹' K)

Tactic:
by
  constructor
  · intro hK
    exact Equiv.image_symm_eq_preimage _ _ ▸ hK.image continuous_mk_symm
  · intro hK
    exact Equiv.image_preimage _ _ ▸ hK.image_of_continuousOn <| continuousOn_isCompact_mk hK

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝¹⁰ : SeminormedAddCommGroup E
inst✝⁹ : SeminormedAddCommGroup F
inst✝⁸ : SeminormedAddCommGroup G
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NontriviallyNormedField 𝕜₃
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x : E
y : F
⊢ ‖(f x) y‖ ≤ ‖f.flip‖ * ‖x‖ * ‖y‖

Tactic:
mul_right_comm

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝¹⁰ : SeminormedAddCommGroup E
inst✝⁹ : SeminormedAddCommGroup F
inst✝⁸ : SeminormedAddCommGroup G
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NontriviallyNormedField 𝕜₃
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x : E
y : F
⊢ ‖(f x) y‖ ≤ ‖f.flip‖ * ‖y‖ * ‖x‖
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
s : Set Ω
hms : MeasurableSet s
μ : Measure Ω
t : Set Ω
⊢ μ[t | s] = (μ s)⁻¹ * μ (s ∩ t)

Tactic:
rw [cond, Measure.smul_apply, Measure.restrict_apply' hms, Set.inter_comm, smul_eq_mul]

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 : γ → β
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
⊢ essSup g (Measure.map f μ) = essSup (g ∘ f) μ

Tactic:
by
  refine le_antisymm ?_ (essSup_comp_le_essSup_map_measure hf hgf_co hg_bdd)
  refine limsSup_le_limsSup hg_co hgf (fun c h_le => ?_)
  rw [eventually_map] at h_le ⊢
  rw [ae_map_iff hf (measurableSet_le hg measurable_const)]
  exact h_le

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : s ⊆ t
this : IsProbabilityMeasure (uniformOn s)
⊢ 1 ≤ (uniformOn s) t

Tactic:
← uniformOn_self hs hs'

Goal state after:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : s ⊆ t
this : IsProbabilityMeasure (uniformOn s)
⊢ (uniformOn s) s ≤ (uniformOn s) t
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLattice β
hμ : ∀ (a : α), μ {a} ≠ 0
f : α → β
⊢ essInf f μ = ⨅ i, f i

Tactic:
by
  rw [essInf, ae_eq_top.2 hμ, liminf_top_eq_iInf]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
⊢ piPremeasure m (univ.pi s) = ∏ i, (m i) (s i)

Tactic:
by
  cases isEmpty_or_nonempty ι
  · simp [piPremeasure]
  rcases (pi univ s).eq_empty_or_nonempty with h | h
  · rcases univ_pi_eq_empty_iff.mp h with ⟨i, hi⟩
    have : ∃ i, m i (s i) = 0 := ⟨i, by simp [hi]⟩
    simpa [h, Finset.card_univ, zero_pow Fintype.card_ne_zero, @eq_comm _ (0 : ℝ≥0∞),
      Finset.prod_eq_zero_iff, piPremeasure]
  · simp [h, piPremeasure]

Goal state after:
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)
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ ∏ i_1, (μ i_1) (update (fun j ↦ univ) i s i_1) = (∏ j ∈ Finset.univ.erase i, (μ j) univ) * (μ i) s

Tactic:
← Finset.prod_erase_mul _ _ (a := i) (by simp)

Goal state after:
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ (∏ x ∈ Finset.univ.erase i, (μ x) (update (fun j ↦ univ) i s x)) * (μ i) (update (fun j ↦ univ) i s i) =
    (∏ j ∈ Finset.univ.erase i, (μ j) univ) * (μ i) s
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 ε
f : α → ε
s : Set α
hs : MeasurableSet s
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)

Tactic:
by_cases hp_zero : p = 0
  · simp only [hp_zero, eLpNorm_exponent_zero]
  by_cases hp_top : p = ∞
  · simp_rw [hp_top, eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm,
       enorm_indicator_eq_indicator_enorm, ENNReal.essSup_indicator_eq_essSup_restrict hs]
  simp_rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_zero hp_top]
  rw [← lintegral_indicator hs]
  congr
  simp_rw [enorm_indicator_eq_indicator_enorm]
  rw [eq_comm, ← Function.comp_def (fun x : ℝ≥0∞ => x ^ p.toReal), Set.indicator_comp_of_zero,
    Function.comp_def]
  simp [ENNReal.toReal_pos hp_zero hp_top]

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:
rw [← inv_inj, inv_eq p q r, inv_eq p q r']

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

Goal state before:
pp: p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ 1 ≠ q ↔ 1 < q

Tactic:
lt_iff_le_and_ne

Goal state after:
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ 1 ≠ q ↔ 1 ≤ q ∧ 1 ≠ q
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : 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
⊢ (f z - f x) / (z - x) ≤ (f z - f y) / (z - y)

Tactic:
by
  have hyz' : 0 < z - y := by linarith
  have hxz' : 0 < z - x := by linarith
  field_simp
  linarith only [hf.secant_mono_aux1 hx hz hxy hyz]

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

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

Tactic:
simp_rw [hp, eLpNorm_exponent_top]
    exact hf.essSup_map_measure

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

Tactic:
exact rpow_arith_mean_le_arith_mean_rpow s w z hw hw' hz hp

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
⊢ a / (a + b) + b / (a + b) = 1

Tactic:
← add_div,

Goal state after:
p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
hp_pos : 0 < p
h_zero : ¬a + b = 0
h_nonzero : ¬(a = 0 ∧ b = 0)
⊢ (a + b) / (a + b) = 1
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 ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i

Tactic:
constructor
      · intro h
        rw [← h]
        intro j hj
        apply eq_zero_of_ne_zero_of_mul_left_eq_zero (ne_of_lt (hw j hj)).symm
        apply (sum_eq_zero_iff_of_nonneg ?_).mp h.symm j hj
        exact fun i hi => (mul_nonneg_iff_of_pos_left (hw i hi)).mpr (hz i hi)
      · intro h
        convert! h i his
        exact hzi.symm

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

Goal state before:
pp: case neg
α : 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
hf_top : ¬∫⁻ (a : α), f a ^ p ∂μ = ∞
hg_top : ¬∫⁻ (a : α), g a ^ q ∂μ = ∞
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
exact ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top hpq hf hf_top hg_top hf_zero hg_zero

Goal state after:
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 ≠ ∞
h_top : ∀ a ∈ s, w a * z a ≠ ∞
h_top_rpow : ∀ a ∈ s, w a * z a ^ p ≠ ∞
⊢ ∑ i ∈ s, w i = ∑ i ∈ s, ↑(w i).toNNReal

Tactic:
congr! with i hi

Goal state after:
case a
ι : 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 ≠ ∞
h_top : ∀ a ∈ s, w a * z a ≠ ∞
h_top_rpow : ∀ a ∈ s, w a * z a ^ p ≠ ∞
i : ι
hi : i ∈ s
⊢ w i = ↑(w i).toNNReal
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 a + g a) ^ p ≤ 2 ^ (p - 1) * f a ^ p + 2 ^ (p - 1) * g a ^ p

Tactic:
simpa [mul_add] using ENNReal.rpow_add_le_mul_rpow_add_rpow (f a) (g a) hp1

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:
ENNReal.toReal_zero

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.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:
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 h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ ∑ i ∈ s, f i ^ p = (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, f i ^ p) ^ (1 / q)

pp: case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / q) ≠ 0

Tactic:
← rpow_add hf.ne',

Goal state after:
case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ ∑ i ∈ s, f i ^ p = (∑ i ∈ s, f i ^ p) ^ (1 / p + 1 / q)

case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / q) ≠ 0
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 :
  1 * ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
    ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
      ((∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) * ∫⁻ (a : α), (f + g) a ^ p ∂μ)
⊢ 1 ≤
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
      ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))

Tactic:
rwa [← mul_assoc, ENNReal.mul_le_mul_iff_left h_add_zero h_add_top, mul_comm] at h

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

Tactic:
have h0_rpow : (∫⁻ a, (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0 := by
    simp [h_add_zero, h_add_top, -Pi.add_apply]
  suffices h :
    1 ≤
      (∫⁻ a : α, (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
        ((∫⁻ a : α, f a ^ p ∂μ) ^ (1 / p) + (∫⁻ a : α, g a ^ p ∂μ) ^ (1 / p)) by
    rwa [← ENNReal.mul_le_mul_iff_right h0_rpow (by finiteness),
      ← mul_assoc, ← rpow_add _ _ h_add_zero h_add_top, ←
      sub_eq_add_neg, _root_.sub_self, rpow_zero, one_mul, mul_one] at h
  have h :
    (∫⁻ a : α, (f + g) a ^ p ∂μ) ≤
      ((∫⁻ a : α, f a ^ p ∂μ) ^ (1 / p) + (∫⁻ a : α, g a ^ p ∂μ) ^ (1 / p)) *
        (∫⁻ a : α, (f + g) a ^ p ∂μ) ^ (1 / q) :=
    lintegral_rpow_add_le_add_eLpNorm_mul_lintegral_rpow_add hpq hf hg
  have h_one_div_q : 1 / q = 1 - 1 / p := by
    nth_rw 2 [← hpq.inv_add_inv_eq_one]
    ring
  simp_rw [h_one_div_q, sub_eq_add_neg 1 (1 / p), ENNReal.rpow_add _ _ h_add_zero h_add_top,
    rpow_one] at h
  conv_rhs at h => enter [2]; rw [mul_comm]
  conv_lhs at h => rw [← one_mul (∫⁻ a : α, (f + g) a ^ p ∂μ)]
  rwa [← mul_assoc, ENNReal.mul_le_mul_iff_left h_add_zero h_add_top, mul_comm] at h

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
p q r : ℝ
hpqr : p.HolderTriple q r
f g : ι → ℝ≥0
hf_sum : Summable fun a ↦ f a ^ p
hg_sum : Summable fun a ↦ g a ^ q
⊢ (Summable fun a ↦ (f a * g a) ^ r) ∧
    ∑' (a : ι), (f a * g a) ^ r ≤ (∑' (a : ι), f a ^ p) ^ (r / p) * (∑' (a : ι), g a ^ q) ^ (r / q)

Tactic:
exact NNReal.summable_and_Lr_rpow_le_Lp_mul_Lq_tsum hpqr hf_sum hg_sum

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

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
inst✝ : NormedAddCommGroup E
f : ↥(Lp E p 0)
⊢ ENNReal.toReal 0 = 0

Tactic:
ENNReal.toReal_zero

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

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ↥(Lp E 0 μ)
⊢ ENNReal.toReal 0 = 0

Tactic:
ENNReal.toReal_zero

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:
rw [← ENNReal.coe_le_coe, nnnorm_def, ENNReal.coe_toNNReal (eLpNorm_ne_top _)]

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
⊢ eLpNorm (↑↑f) p μ ≤ ↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C)
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n : ℕ
⊢ seqTendstoAeSeq hfg n < max (seqTendstoAeSeqAux hfg (n + 1)) (seqTendstoAeSeq hfg n + 1)

Tactic:
exact lt_of_lt_of_le (lt_add_one <| seqTendstoAeSeq hfg n) (le_max_right _ _)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (fun x ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
⊢ MemLp (fun x ↦ ‖f x‖ₑ) p μ

Tactic:
convert! h.enorm_rpow_div q⁻¹ using 1

Goal state after:
case e'_6
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (fun x ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
⊢ (fun x ↦ ‖f x‖ₑ) = fun x ↦ ‖‖f x‖ₑ ^ q.toReal‖ₑ ^ q⁻¹.toReal

case e'_7
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (fun x ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
⊢ p = p / q / q⁻¹
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: case succ
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → α
hf : MeasurePreserving f μ μ
x✝ : ↥(Lp E p μ)
n : ℕ
h : (⇑(compMeasurePreserving f hf))^[n] x✝ = (compMeasurePreserving f^[n] ⋯) x✝
⊢ (⇑(compMeasurePreserving f hf))^[1 + n] x✝ = (compMeasurePreserving f^[n + 1] ⋯) x✝

Tactic:
simp [Function.iterate_add, h, compMeasurePreserving_comp (hf.iterate n) hf]

Goal state after:
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
⊢ Disjoint (Set.range ⇑(inl.trans f, inr.trans f).1) (Set.range ⇑(inl.trans f, inr.trans f).2)

Tactic:
Set.disjoint_left

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
⊢ ∀ ⦃a : γ⦄, a ∈ Set.range ⇑(inl.trans f, inr.trans f).1 → ¬a ∈ Set.range ⇑(inl.trans f, inr.trans f).2
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : SeminormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
hfg : Tendsto (fun n ↦ eLpNorm (f n - g) ∞ μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g

Tactic:
refine tendstoInMeasure_of_ne_top fun δ hδ hδ_top ↦ ?_
  simp only [eLpNorm_exponent_top, eLpNormEssSup] at hfg
  rw [ENNReal.tendsto_nhds_zero] at hfg ⊢
  intro ε hε
  specialize hfg (δ / 2) (ENNReal.div_pos_iff.2 ⟨hδ.ne', ENNReal.ofNat_ne_top⟩)
  refine hfg.mono fun n hn => ?_
  simp only [Pi.sub_apply] at *
  have : essSup (fun x : α => ‖f n x - g x‖ₑ) μ < δ :=
    hn.trans_lt (ENNReal.half_lt_self hδ.ne' hδ_top)
  refine ((le_of_eq ?_).trans (ae_lt_of_essSup_lt this).le).trans hε.le
  congr with x
  simp [edist_eq_enorm_sub]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x✝ : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁷, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
c : ι → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : ∏ i ∈ I, c i ≠ 0
a : 𝕜
ha : a ∈ {y | ‖y‖ < ‖∏ i ∈ I, c i‖}
x : (i : ι) → E i
hx : x ∈ s
i₀ : ι
y : (i : ι) → E i := I.piecewise (fun i ↦ c i • x i) x
⊢ a • (∏ i ∈ I, c i)⁻¹ • (∏ i ∈ I, c i) • f x = a • f x

Tactic:
inv_smul_smul₀ hc₀'

Goal state after:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x✝ : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁷, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
c : ι → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : ∏ i ∈ I, c i ≠ 0
a : 𝕜
ha : a ∈ {y | ‖y‖ < ‖∏ i ∈ I, c i‖}
x : (i : ι) → E i
hx : x ∈ s
i₀ : ι
y : (i : ι) → E i := I.piecewise (fun i ↦ c i • x i) x
⊢ a • f x = a • f x
Module: Mathlib.Analysis.Normed.Operator.Mul

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁴ : SeminormedRing R
inst✝³ : NormedAlgebra 𝕜 R
inst✝² : Module R E
inst✝¹ : IsBoundedSMul R E
inst✝ : IsScalarTower 𝕜 R E
⊢ ‖lsmul 𝕜 R‖ₑ ≤ 1

Tactic:
rw [enorm_eq_nnnorm]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁴ : SeminormedRing R
inst✝³ : NormedAlgebra 𝕜 R
inst✝² : Module R E
inst✝¹ : IsBoundedSMul R E
inst✝ : IsScalarTower 𝕜 R E
⊢ ↑‖lsmul 𝕜 R‖₊ ≤ 1