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

Goal state before:
pp: case h₂.inr.inr
α : 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‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
⊢ ∫⁻ (x : α), (‖f x‖ₑ * ‖g x‖ₑ) ^ p.toReal ∂μ ≤
    essSup (fun x ↦ ‖f x‖ₑ) μ ^ p.toReal * ((∫⁻ (x : α), ‖g x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹) ^ p.toReal

Tactic:
ENNReal.rpow_inv_rpow hp.ne',

Goal state after:
case h₂.inr.inr
α : 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‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
⊢ ∫⁻ (x : α), (‖f x‖ₑ * ‖g x‖ₑ) ^ p.toReal ∂μ ≤ essSup (fun x ↦ ‖f x‖ₑ) μ ^ p.toReal * ∫⁻ (x : α), ‖g x‖ₑ ^ p.toReal ∂μ
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 :
  ∫⁻ (a : α), (f + g) a ^ p ∂μ ≤
    ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / q)
h_one_div_q : 1 / q = 1 - 1 / p
⊢ 1 ≤
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
      ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))

Tactic:
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

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

Goal state before:
pp: ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
⊢ (∑ i ∈ s, f i) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, f i ^ p

Tactic:
rcases eq_or_lt_of_le hp with hp | hp

Goal state after:
case inl
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 = p
⊢ (∑ i ∈ s, f i) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, f i ^ p

case inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ (∑ i ∈ s, f i) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, f i ^ p
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

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

Tactic:
eLpNorm_exponent_top_lim_eq_essSup_liminf h_lim

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
hp : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
⊢ eLpNorm (↑↑(f + g)) p μ ≤ eLpNorm (↑↑f) p μ + eLpNorm (↑↑g) p μ

Tactic:
exact (eLpNorm_congr_ae (AEEqFun.coeFn_add _ _)).trans_le
            (eLpNorm_add_le (Lp.aestronglyMeasurable _) (Lp.aestronglyMeasurable _) hp.out)

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

Goal state before:
pp: 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

Tactic:
ext x
    have : q.toReal * q.toReal⁻¹ = 1 :=
      CommGroupWithZero.mul_inv_cancel q.toReal <| ENNReal.toReal_ne_zero.mpr ⟨q_zero, q_top⟩
    simp [← ENNReal.rpow_mul, this, ENNReal.rpow_one]

Goal state after:
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
h_lt_ε_real : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k ↦ {x | 2⁻¹ ^ k ≤ edist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : μ s = 0
x : α
ε : ℝ≥0∞
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hNx : edist (f (ns n) x) (g x) < 2⁻¹ ^ n
hn_ge : n ≥ max N (k - 1)
⊢ 2⁻¹ ^ n ≤ 2 * 2⁻¹ ^ k

Tactic:
nth_rw 2 [← pow_one (2 : ℝ≥0∞)]

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k ↦ {x | 2⁻¹ ^ k ≤ edist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : μ s = 0
x : α
ε : ℝ≥0∞
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hNx : edist (f (ns n) x) (g x) < 2⁻¹ ^ n
hn_ge : n ≥ max N (k - 1)
⊢ 2⁻¹ ^ n ≤ 2 ^ 1 * 2⁻¹ ^ k
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
𝕜✝ : Type u_2
𝕜'✝ : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
g✝ : E → F
c : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝ : RingHomIsometric σ
L : E →SL[σ] F
f g : ↥(Lp E p μ)
⊢ ↑↑(L.compLp (f + g)) =ᵐ[μ] ↑↑(L.compLp f + L.compLp g)

Tactic:
filter_upwards [Lp.coeFn_add f g, coeFn_compLp L (f + g), coeFn_compLp L f,
      coeFn_compLp L g, Lp.coeFn_add (L.compLp f) (L.compLp g)]

Goal state after:
α : Type u_1
𝕜✝ : Type u_2
𝕜'✝ : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
g✝ : E → F
c : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝ : RingHomIsometric σ
L : E →SL[σ] F
f g : ↥(Lp E p μ)
⊢ ∀ (a : α),
    ↑↑(f + g) a = (↑↑f + ↑↑g) a →
      ↑↑(L.compLp (f + g)) a = L (↑↑(f + g) a) →
        ↑↑(L.compLp f) a = L (↑↑f a) →
          ↑↑(L.compLp g) a = L (↑↑g a) →
            ↑↑(L.compLp f + L.compLp g) a = (↑↑(L.compLp f) + ↑↑(L.compLp g)) a →
              ↑↑(L.compLp (f + g)) a = ↑↑(L.compLp f + L.compLp g) a
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ (∑ i ∈ s, f i) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, f i ^ p

Tactic:
rcases eq_or_lt_of_le hp with hp | hp

Goal state after:
case inl
ι : Type u
s : Finset ι
f : ι → ℝ≥0∞
p : ℝ
hp✝ : 1 ≤ p
hp : 1 = p
⊢ (∑ i ∈ s, f i) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, f i ^ p

case inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0∞
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ (∑ i ∈ s, f i) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, f i ^ p
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
𝕜✝ : Type u_2
𝕜'✝ : Type u_3
E : Type u_4
F✝ : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F✝
g : E → F✝
c✝ : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜'
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace 𝕜' F✝
σ : 𝕜 →+* 𝕜'
inst✝⁵ : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fact (1 ≤ p)
B : G →L[𝕜] E →L[𝕜] F
c : G
f : ↥(Lp E p μ)
⊢ ‖(B c).compLp f‖ ≤ ‖B‖ * ‖c‖ * ‖f‖

Tactic:
grw [norm_compLp_le, le_opNorm]

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
inst✝¹ : NormedSpace ℝ E
ν : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ≤ c • ν
inst✝ : Fact (1 ≤ p)
f : ↥(Lp E p ν)
⊢ ‖(LpToLpOfMeasureLeSMulₗ hc h) f‖ ≤ c.toReal ^ (1 / p).toReal * ‖f‖

Tactic:
by
  simp only [← toReal_enorm]
  rw [ENNReal.toReal_rpow, ← ENNReal.toReal_mul]
  grw [enorm_LpToLpOfMeasureLeSMulₗ_apply_le]
  simp [ENNReal.mul_eq_top, hc]

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

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

Tactic:
_root_.dist_eq_norm,

Goal state after:
case pos.refine_1
α : Type u_1
m✝ : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
hp : 1 ≤ ∞
hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → essSup (fun x ↦ ‖(f n - f m) x‖ₑ) μ < B N
x : α
n m N : ℕ
hx : ‖(f n - f m) x‖ₑ < B N
hnN : N ≤ n
hmN : N ≤ m
⊢ ‖f n x - f m x‖ ≤ (B N).toReal
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : 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 ≠ ∞
hp_top : ¬p = ∞
hp1 : 1 ≤ p.toReal
N n m : ℕ
h_cau : eLpNorm (f n - f m) p μ < B N
hn : N ≤ n
hm : N ≤ m
⊢ eLpNorm' (f n - f m) p.toReal μ < B N

Tactic:
rwa [eLpNorm_eq_eLpNorm' (zero_lt_one.trans_le hp).ne.symm hp_top] at h_cau

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁵ : NormedDivisionRing R
inst✝⁴ : NormedAlgebra 𝕜 R
inst✝³ : Module R E
inst✝² : NormSMulClass R E
inst✝¹ : IsScalarTower 𝕜 R E
inst✝ : Nontrivial E
a : R
⊢ ‖(lsmul 𝕜 R) a‖ = ‖a‖

Tactic:
by
  refine ContinuousLinearMap.opNorm_eq_of_bounds (norm_nonneg _) (fun x => ?_) fun N _ h => ?_
  · simp [norm_smul]
  obtain ⟨y, hy⟩ := exists_ne (0 : E)
  refine le_of_mul_le_mul_right ?_ (norm_pos_iff.mpr hy)
  simpa [norm_smul] using h y

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

Goal state before:
pp: E : Type u_2
p : ℝ≥0∞
inst✝³ : NormedAddCommGroup E
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasureOnCompacts μ
f : X → E
hf : HasCompactSupport f
h2f : AEStronglyMeasurable f μ
C : ℝ
hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
⊢ MemLp f p μ

Tactic:
by
  have := memLp_top_of_bound h2f C hfC
  exact this.mono_exponent_of_measure_support_ne_top
    (fun x ↦ image_eq_zero_of_notMem_tsupport) (hf.measure_lt_top.ne) le_top

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℕ
hf : MemLp f (↑p) μ
⊢ Integrable (fun x ↦ ‖f x‖ ^ p) μ

Tactic:
by simpa using hf.integrable_norm_rpow'

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ (eLpNorm (fun x ↦ c) p μ).toReal = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

Tactic:
eLpNorm_const

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ (‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)).toReal = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

case h0
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ p ≠ 0

case hμ
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ μ ≠ 0
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s t : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
h : IntegrableOn f s (μ.restrict t)
⊢ IntegrableOn f (s ∩ t) μ

Tactic:
by
  have := h.mono_set (inter_subset_left (t := t))
  rwa [IntegrableOn, μ.restrict_restrict_of_subset inter_subset_right] at this

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

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : PseudoMetrizableSpace ε
s : Set β
t : β → Set α
a✝¹ : β
s✝ : Set β
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
hf : IntegrableOn f (⋃ i ∈ s✝, t i) μ ↔ ∀ i ∈ s✝, IntegrableOn f (t i) μ
⊢ IntegrableOn f (⋃ i ∈ insert a✝¹ s✝, t i) μ ↔ ∀ i ∈ insert a✝¹ s✝, IntegrableOn f (t i) μ

Tactic:
simp [hf, or_imp, forall_and]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure α
s : Set β
⊢ Integrable f ((Measure.map e μ).restrict s) ↔ Integrable (f ∘ e) (μ.restrict (e ⁻¹' s))

Tactic:
he.restrict_map,

Goal state after:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure α
s : Set β
⊢ Integrable f (Measure.map e (μ.restrict (e ⁻¹' s))) ↔ Integrable (f ∘ e) (μ.restrict (e ⁻¹' s))
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
s : Set β
hs : s ⊆ range e
⊢ IntegrableOn f s μ ↔ IntegrableOn (f ∘ e) (e ⁻¹' s) (Measure.comap e μ)

Tactic:
← he.integrableOn_map_iff,

Goal state after:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
s : Set β
hs : s ⊆ range e
⊢ IntegrableOn f s μ ↔ IntegrableOn f s (Measure.map e (Measure.comap e μ))
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ENormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
h1s : support f ⊆ s
h : IntegrableOn f s μ
x : α
hx : f x ≠ 0
⊢ x ∈ s

Tactic:
exact h1s (mem_support.2 hx)

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
⊢ Measurable fun x ↦ (f x).toNNReal

Tactic:
exact hf.ennreal_toNNReal

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
⊢ AEMeasurable (fun x ↦ (f x).toNNReal) μ

Tactic:
exact hf.ennreal_toNNReal

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
⊢ ∀ (y : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))),
    MemLp.toLp (fun x ↦ f x • ↑↑(u + y) x) ⋯ = MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯ + MemLp.toLp (fun x ↦ f x • ↑↑y x) ⋯

Tactic:
v

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
⊢ MemLp.toLp (fun x ↦ f x • ↑↑(u + v) x) ⋯ = MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯ + MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
r : ℝ
u : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
⊢ ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑(r • u) x) ⋯) =ᵐ[μ] ↑↑((RingHom.id ℝ) r • MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯)

Tactic:
filter_upwards [(ae_withDensity_iff f_meas.coe_nnreal_ennreal).1 (Lp.coeFn_smul r u),
      (memL1_smul_of_L1_withDensity f_meas (r • u)).coeFn_toLp,
      Lp.coeFn_smul r ((memL1_smul_of_L1_withDensity f_meas u).toLp _),
      (memL1_smul_of_L1_withDensity f_meas u).coeFn_toLp]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
r : ℝ
u : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
⊢ ∀ (a : α),
    (↑(f a) ≠ 0 → ↑↑(r • u) a = (r • ↑↑u) a) →
      ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑(r • u) x) ⋯) a = f a • ↑↑(r • u) a →
        ↑↑(r • MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) a = (r • ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯)) a →
          ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) a = f a • ↑↑u a →
            ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑(r • u) x) ⋯) a = ↑↑((RingHom.id ℝ) r • MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) a
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
⊢ ‖f m₁ - f m₂‖ ≤ C * ↑(Fintype.card ι) * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖

Tactic:
by
  classical
  have A :
    ∀ i : ι,
      ∏ j, (if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤
        ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) := by
    intro i
    calc
      ∏ j, (if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤
          ∏ j : ι, Function.update (fun _ => max ‖m₁‖ ‖m₂‖) i ‖m₁ - m₂‖ j := by
        gcongr with j
        rcases eq_or_ne j i with rfl | h
        · simp only [ite_true, Function.update_self]
          exact norm_le_pi_norm (m₁ - m₂) _
        · simp [h, -le_sup_iff, -sup_le_iff, sup_le_sup, norm_le_pi_norm]
      _ = ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) := by
        rw [prod_update_of_mem (Finset.mem_univ _)]
        simp [card_univ_sdiff]
  calc
    ‖f m₁ - f m₂‖ ≤ C * ∑ i, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ :=
      f.norm_image_sub_le_of_bound' hC H m₁ m₂
    _ ≤ C * ∑ _i, ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) := by gcongr; apply A
    _ = C * Fintype.card ι * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖ := by
      rw [sum_const, card_univ, nsmul_eq_mul]
      ring

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

Goal state before:
pp: X : Type u_1
ε : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f g : X → ε
μ : Measure X
s : Set X
h : f =ᵐ[μ.restrict s] g
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
t : Set X
hxt : t ∈ 𝓝[s] x
hft : IntegrableOn f t μ
⊢ IntegrableOn g (s ∩ t) μ

Tactic:
refine (hft.mono_set inter_subset_right).congr ?_

Goal state after:
X : Type u_1
ε : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f g : X → ε
μ : Measure X
s : Set X
h : f =ᵐ[μ.restrict s] g
hf : LocallyIntegrableOn f s μ
x : X
hx : x ∈ s
t : Set X
hxt : t ∈ 𝓝[s] x
hft : IntegrableOn f t μ
⊢ f =ᵐ[μ.restrict (s ∩ t)] g
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹⁰ : Fintype ι'
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
c : 𝕜
f : ContinuousMultilinearMap 𝕜 E 𝕜
⊢ { toFun := fun z ↦ (c • f).smulRight z, map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id 𝕜) c • { toFun := fun z ↦ f.smulRight z, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by ext; simp [smul_smul]

Goal state after: