mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
⊢ ∑ x, μ[E | X ⁻¹' {x}] * μ (X ⁻¹' {x}) = ∑ x, μ (X ⁻¹' {x} ∩ E)

Tactic:
cond_mul_eq_inter (hX (.singleton _))

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

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

Tactic:
exact @prod.instSigmaFinite _ _ _ _ _ _ _ ih

Goal state after:
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 γ
R : Type u_5
inst✝² : TopologicalSpace R
inst✝¹ : InvolutiveStar R
inst✝ : ContinuousStar R
f : α →ₘ[μ] R
⊢ comp (star ∘ star) ⋯ f = f

Tactic:
simp [star_involutive.comp_self]

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✝ : (i : ι) → MetricSpace (α i)
x : (i : ι) → α i
r : ℝ
hr : 0 ≤ r
⊢ (Measure.pi μ) (Metric.closedBall x r) = ∏ i, (μ i) (Metric.closedBall (x i) r)

Tactic:
rw [closedBall_pi _ hr, pi_pi]

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

Goal state before:
pp: case pos
α : 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
⊢ MemLp (s.piecewise f g) p μ

Tactic:
simp only [hp_zero, memLp_zero_iff_aestronglyMeasurable]

Goal state after:
case pos
α : 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
⊢ AEStronglyMeasurable (s.piecewise f g) μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : 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
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ

Tactic:
have hp' : ¬(p < 0) := by linarith
  by_cases hc : c = ⊤
  · by_cases hg' : eLpNorm' g p μ = 0
    · have : ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0 := by
        simp only [eLpNorm'_eq_lintegral_enorm, one_div, ENNReal.rpow_eq_zero_iff, inv_pos, hp,
          and_true, inv_neg'', hp', and_false, or_false] at hg'
        rw [MeasureTheory.lintegral_eq_zero_iff' (by fun_prop)] at hg'
        exact hg'.mono fun x hx ↦ by simpa [hp, hp'] using hx
      have : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = 0 := (this.and h).mono fun x ⟨h, h'⟩ ↦ by simp_all
      simpa only [hg', mul_zero, nonpos_iff_eq_zero] using eLpNorm'_eq_zero_of_ae_eq_zero hp this
    · simp_all
  have : c ^ p ≠ ⊤ := by simp [hp.le, hc]
  simp_rw [eLpNorm'_eq_lintegral_enorm]
  rw [← ENNReal.rpow_le_rpow_iff hp, ENNReal.mul_rpow_of_nonneg _ _ hp.le]
  simp_rw [← ENNReal.rpow_mul, one_div, inv_mul_cancel₀ hp.ne', ENNReal.rpow_one,
    ← lintegral_const_mul' _ _ this]
  apply lintegral_mono_ae
  have aux (x) : (↑c) ^ p * ‖g x‖ₑ ^ p = (↑c * ‖g x‖ₑ) ^ p := by
    simp [ENNReal.mul_rpow_eq_ite, hp']
  simpa [ENNReal.coe_rpow_of_nonneg _ hp.le, aux, ENNReal.rpow_le_rpow_iff hp]

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

Goal state before:

Tactic:
q⁻¹ ≤ r⁻¹ := HolderTriple.inv_le_inv q p r
    _ < ∞ := by simpa using pos_iff_ne_zero.mpr hr

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

Goal state before:
pp: s : ℝ
hs : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
⊢ 1 + p * s < (1 + s) ^ p

Tactic:
have hp' : 0 < p := zero_lt_one.trans hp
  rcases eq_or_lt_of_le hs with rfl | hs
  · rwa [add_neg_cancel, zero_rpow hp'.ne', mul_neg_one, add_neg_lt_iff_lt_add, zero_add]
  have hs1 : 0 < 1 + s := neg_lt_iff_pos_add'.mp hs
  rcases le_or_gt (1 + p * s) 0 with hs2 | hs2
  · exact hs2.trans_lt (rpow_pos_of_pos hs1 _)
  have hs3 : 1 + s ≠ 1 := hs' ∘ add_eq_left.mp
  have hs4 : 1 + p * s ≠ 1 := by
    contrapose hs'; rwa [add_eq_left, mul_eq_zero, eq_false_intro hp'.ne', false_or] at hs'
  rw [rpow_def_of_pos hs1, ← exp_log hs2]
  apply exp_strictMono
  rcases lt_or_gt_of_ne hs' with hs' | hs'
  · rw [← div_lt_iff₀ hp', ← div_lt_div_right_of_neg hs']
    convert! strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs2 hs1 hs4 hs3 _ using 1
    · rw [add_sub_cancel_left, log_one, sub_zero]
    · rw [add_sub_cancel_left, div_div, log_one, sub_zero]
    · gcongr
      exact mul_lt_of_one_lt_left hs' hp
  · rw [← div_lt_iff₀ hp', ← div_lt_div_iff_of_pos_right hs']
    convert! strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs1 hs2 hs3 hs4 _ using 1
    · rw [add_sub_cancel_left, div_div, log_one, sub_zero]
    · rw [add_sub_cancel_left, log_one, sub_zero]
    · gcongr
      exact lt_mul_of_one_lt_left hs' hp

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

Goal state before:
pp: p q r : ℝ≥0
hr : r ≠ 0
h : (↑p).HolderTriple ↑q ↑r
hp : p ≠ 0
hq : q ≠ 0
⊢ p⁻¹ + q⁻¹ = r⁻¹

Tactic:
by exact_mod_cast h.inv_add_inv_eq_inv

Goal state after:
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_toNNReal h.ne

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 μ
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case pos.mp
ι : 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
h : 0 = ∑ i ∈ s, w i * z i
j : ι
hj : j ∈ s
⊢ z j = 0

Tactic:
apply eq_zero_of_ne_zero_of_mul_left_eq_zero (ne_of_lt (hw j hj)).symm

Goal state after:
case pos.mp
ι : 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
h : 0 = ∑ i ∈ s, w i * z i
j : ι
hj : j ∈ s
⊢ w j * z j = 0
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p : ℝ
a b : ℝ≥0
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
by
  have hp_pos : 0 < p := by positivity
  by_cases h_zero : a + b = 0
  · simp [add_eq_zero.mp h_zero, hp_pos.ne']
  have h_nonzero : ¬(a = 0 ∧ b = 0) := by rwa [add_eq_zero] at h_zero
  have h_add : a / (a + b) + b / (a + b) = 1 := by rw [← add_div, div_self h_zero]
  have h := add_rpow_le_one_of_add_le_one (a / (a + b)) (b / (a + b)) h_add.le hp1
  rw [div_rpow a (a + b), div_rpow b (a + b)] at h
  have hab_0 : (a + b) ^ p ≠ 0 := by simp [h_nonzero]
  have h_mul : (a + b) ^ p * (a ^ p / (a + b) ^ p + b ^ p / (a + b) ^ p) ≤ (a + b) ^ p := by
    nth_rw 4 [← mul_one ((a + b) ^ p)]; gcongr
  rwa [div_eq_mul_inv, div_eq_mul_inv, mul_add, mul_comm (a ^ p), mul_comm (b ^ p), ← mul_assoc, ←
    mul_assoc, mul_inv_cancel₀ hab_0, one_mul, one_mul] at h_mul

Goal state after:
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, w j ≠ 0 → ∀ k ∈ s, w k ≠ 0 → z j = z k

Tactic:
by
  have :
      ∏ i ∈ s with w i ≠ 0, z i ^ w i = ∑ i ∈ s with w i ≠ 0, w i * z i ↔
        ∀ j ∈ {x ∈ s | w x ≠ 0}, ∀ k ∈ {x ∈ s | w x ≠ 0}, z j = z k :=
    geom_mean_eq_arith_mean_weighted_iff_of_pos _ w z (by grind)
      (sum_filter_ne_zero _ |>.trans hw') (hz _ <| mem_of_mem_filter · ·)
  grind [prod_filter_of_ne, sum_filter_of_ne, rpow_zero]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
n : ℕ
⊢ ConvexOn 𝕜 (Ioi 0) fun x ↦ x ^ -[n+1]

Tactic:
by
    simp_rw [zpow_negSucc, ← inv_pow]
    refine (convexOn_iff_forall_pos.2 ⟨convex_Ioi _, ?_⟩).pow (fun x (hx : 0 < x) ↦ by positivity) _
    rintro x (hx : 0 < x) y (hy : 0 < y) a b ha hb hab
    simp only [smul_eq_mul]
    field_simp
    have H : 0 ≤ a * b * (x - y) ^ 2 := by positivity
    linear_combination H - x * y * (a + b + 1) * hab

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

Goal state before:

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

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

Goal state before:
pp: case pos
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
p q : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : p = ∞
⊢ eLpNorm f p μ < ∞

Tactic:
have hq_top : q = ∞ := by rwa [hp_top, top_le_iff] at hpq

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

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

Tactic:
simp [mul_rpow, div_inv_eq_mul, one_mul, one_div, hp₀, hp₁]

Goal state after:
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
H₁ : ∀ (s : Finset ι), ∑ i ∈ s, (f i * g i) ^ r ≤ (∑' (i : ι), f i ^ p) ^ (r / p) * (∑' (i : ι), g i ^ q) ^ (r / q)
s : Finset ι
⊢ (fun s ↦ ∑ i ∈ s, (f i * g i) ^ r) s ≤ (∑' (i : ι), f i ^ p) ^ (r / p) * (∑' (i : ι), g i ^ q) ^ (r / q)

Tactic:
exact H₁ s

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

Tactic:
2

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)))
| (∫⁻ (a : α), (f + g) a ^ p ∂μ) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p))
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
E : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : MulActionWithZero 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : α → E
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
φ : α → 𝕜
⊢ eLpNorm (φ • f) p μ ≤ eLpNorm φ ∞ μ * eLpNorm f p μ

Tactic:
by
  simpa using! (eLpNorm_le_eLpNorm_top_mul_eLpNorm p φ hf (· • ·) 1
    (.of_forall fun _ => by simpa using! nnnorm_smul_le _ _) :)

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i ↦ f i ^ p
hg : Summable fun i ↦ g i ^ p
pos : 0 < p
H₁ :
  ∀ (s : Finset ι), ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p
s : Finset ι
⊢ (fun s ↦ ∑ i ∈ s, (f i + g i) ^ p) s ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p

Tactic:
exact H₁ s

Goal state after:
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
ι : Type u_4
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
⊢ Tendsto (fun n ↦ eLpNorm (↑↑(f n) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) p μ) fi (𝓝 0) ↔
    Tendsto (fun n ↦ eLpNorm (↑↑(f n) - f_lim) p μ) fi (𝓝 0)

Tactic:
suffices h_eq :
      (fun n => eLpNorm (⇑(f n) - ⇑(MemLp.toLp f_lim f_lim_ℒp)) p μ) =
        (fun n => eLpNorm (⇑(f n) - f_lim) p μ) by
    rw [h_eq]

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝¹ : NormedAddCommGroup E
ι : Type u_4
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
⊢ (fun n ↦ eLpNorm (↑↑(f n) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) p μ) = fun n ↦ eLpNorm (↑↑(f n) - f_lim) p μ
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 : ↥(Lp E p μ)
h : ↑↑f =ᵐ[μ] ↑↑g
⊢ f = g

Tactic:
by
  ext
  exact h

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 : α → E
hf : MemLp f p μ
⊢ edist (MemLp.toLp f hf) 0 = eLpNorm f p μ

Tactic:
by
  simpa using edist_toLp_toLp f 0 hf .zero

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable fun a ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : μ t ≤ ↑δ
hunif : TendstoUniformlyOn f g atTop tᶜ
⊢ ∃ N, ∀ n ≥ N, μ {x | ε ≤ edist (f n x) (g x)} ≤ ↑δ

Tactic:
rw [EMetric.tendstoUniformlyOn_iff] at hunif

Goal state after:
case neg
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable fun a ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : μ t ≤ ↑δ
hunif : ∀ ε > 0, ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ tᶜ, edist (g x) (f n x) < ε
⊢ ∃ N, ∀ n ≥ N, μ {x | ε ≤ edist (f n x) (g x)} ≤ ↑δ
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

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

Tactic:
rw [div_eq_mul_inv, inv_inv, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
      mul_one]

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

Goal state before:
pp: case e'_7
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (fun x ↦ ‖f x‖ ^ q.toReal) (p / q) μ
⊢ p = p / q / q⁻¹

Tactic:
rw [div_eq_mul_inv, inv_inv, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
      mul_one]

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

Goal state before:
pp: α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
f f' : ↥(Lp E p μ)
⊢ ‖hg.compLp g0 f - hg.compLp g0 f'‖ ≤ ↑c * ‖f - f'‖

Tactic:
apply Lp.norm_le_mul_norm_of_ae_le_mul

Goal state after:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
f f' : ↥(Lp E p μ)
⊢ ∀ᵐ (x : α) ∂μ, ‖↑↑(hg.compLp g0 f - hg.compLp g0 f') x‖ ≤ ↑c * ‖↑↑(f - f') x‖
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
⊢ ∃ ns, StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f (ns i) x) atTop (𝓝 (g x))

Tactic:
have h_lt_ε_real (ε : ℝ≥0∞) (hε : 0 < ε) : ∃ k : ℕ, 2 * (2 : ℝ≥0∞)⁻¹ ^ k < ε := by
    obtain ⟨k, h_k⟩ : ∃ k : ℕ, (2 : ℝ≥0∞)⁻¹ ^ k < ε := ENNReal.exists_inv_two_pow_lt hε.ne'
    refine ⟨k + 1, lt_of_eq_of_lt ?_ h_k⟩
    rw [pow_succ', ← mul_assoc, ENNReal.mul_inv_cancel, one_mul]
    · positivity
    · simp
  set ns := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
  use ns
  let S := fun k => { x | (2 : ℝ≥0∞)⁻¹ ^ k ≤ edist (f (ns k) x) (g x) }
  have hμS_le : ∀ k, μ (S k) ≤ (2 : ℝ≥0∞)⁻¹ ^ k :=
    fun k => ExistsSeqTendstoAe.seqTendstoAeSeq_spec hfg k (ns k) le_rfl
  set s := Filter.atTop.limsup S with hs
  have hμs : μ s = 0 := by
    refine measure_limsup_atTop_eq_zero (ne_top_of_le_ne_top ?_ (ENNReal.tsum_le_tsum hμS_le))
    simpa only [ENNReal.tsum_geometric, ENNReal.one_sub_inv_two, inv_inv] using ENNReal.ofNat_ne_top
  have h_tendsto : ∀ x ∈ sᶜ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x)) := by
    refine fun x hx => EMetric.tendsto_atTop.mpr fun ε hε => ?_
    rw [hs, limsup_eq_iInf_iSup_of_nat] at hx
    simp only [S, Set.iSup_eq_iUnion, Set.iInf_eq_iInter, Set.compl_iInter, Set.compl_iUnion,
      Set.mem_iUnion, Set.mem_iInter, Set.mem_compl_iff, Set.mem_ofPred_eq, not_le] at hx
    obtain ⟨N, hNx⟩ := hx
    obtain ⟨k, hk_lt_ε⟩ := h_lt_ε_real ε hε
    refine ⟨max N (k - 1), fun n hn_ge => lt_of_le_of_lt ?_ hk_lt_ε⟩
    specialize hNx n ((le_max_left _ _).trans hn_ge)
    have h_inv_n_le_k : (2 : ℝ≥0∞)⁻¹ ^ n ≤ 2 * (2 : ℝ≥0∞)⁻¹ ^ k := by
      nth_rw 2 [← pow_one (2 : ℝ≥0∞)]
      rw [mul_comm, ← ENNReal.inv_pow, ← ENNReal.inv_pow, ENNReal.inv_le_iff_le_mul, ← mul_assoc,
        mul_comm (_ ^ n), mul_assoc, ← ENNReal.inv_le_iff_le_mul, inv_inv, ← pow_add]
      · gcongr
        · simp
        · omega
      all_goals simp
    exact le_trans hNx.le h_inv_n_le_k
  rw [ae_iff]
  refine ⟨ExistsSeqTendstoAe.seqTendstoAeSeq_strictMono hfg, measure_mono_null (fun x => ?_) hμs⟩
  rw [Set.mem_ofPred_eq, ← @Classical.not_not (x ∈ s), not_imp_not]
  exact h_tendsto x

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‖ₑ.toReal ≤ c.toReal ^ (1 / p).toReal * ‖f‖ₑ.toReal

Tactic:
rw [ENNReal.toReal_rpow, ← ENNReal.toReal_mul]

Goal state after:
α : 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‖ₑ.toReal ≤ (c ^ (1 / p).toReal * ‖f‖ₑ).toReal
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
x y : E
h : (lsmul 𝕜 R).flip x = (lsmul 𝕜 R).flip y
⊢ x = y

Tactic:
simpa using congr($h 1)

Goal state after:
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
M : Type u_5
inst✝³ : Monoid M
inst✝² : DistribMulAction M F
inst✝¹ : SMulCommClass 𝕜 M F
inst✝ : ContinuousConstSMul M F
⊢ ContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E F)

Tactic:
let := IsTopologicalAddGroup.rightUniformSpace F
  have := isUniformAddGroup_of_addCommGroup (G := F)
  infer_instance

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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℝ
hp✝ : 0 ≤ p
hq✝ : 0 ≤ q
hpq : p ≤ q
hint : Integrable (fun x ↦ ‖f x‖ ^ q) μ
hp : 0 < p
hq : 0 < q
⊢ Integrable (fun x ↦ ‖f x‖ ^ p) μ

Tactic:
← ENNReal.toReal_ofReal hp.le,

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℝ
hp✝ : 0 ≤ p
hq✝ : 0 ≤ q
hpq : p ≤ q
hint : Integrable (fun x ↦ ‖f x‖ ^ q) μ
hp : 0 < p
hq : 0 < q
⊢ Integrable (fun x ↦ ‖f x‖ ^ (ENNReal.ofReal p).toReal) μ
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
h : Integrable f (μ + ν)
⊢ Integrable f μ

Tactic:
by
  rw [← memLp_one_iff_integrable] at h ⊢
  exact h.left_of_add_measure

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
⊢ Integrable (↑↑(indicatorConstLp p hs hμs c)) μ

Tactic:
integrable_congr indicatorConstLp_coeFn,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
⊢ Integrable (s.indicator fun x ↦ c) μ