mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:

Tactic:
(∫⁻ a : α, (f * g) a ∂μ) ≤
        ∫⁻ a : α, f a ^ p / ENNReal.ofReal p + g a ^ q / ENNReal.ofReal q ∂μ :=
      lintegral_mono fun a => young_inequality (f a) (g a) hpq
    _ = 1 := by
      simp only [div_eq_mul_inv]
      rw [lintegral_add_left']
      · rw [lintegral_mul_const'' _ (hf.pow_const p), lintegral_mul_const', hf_norm, hg_norm,
          one_mul, one_mul, hpq.inv_add_inv_ennreal]
        simp [hpq.symm.pos]
      · exact (hf.pow_const _).mul_const _

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case hx
ι : 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
⊢ 0 ≤ ∑ i ∈ s, w i * z i ^ p

Tactic:
apply_rules [sum_nonneg, rpow_nonneg]

Goal state after:
case hx
ι : 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, 0 ≤ w i * z i ^ p
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
⊢ 0 ≤ ∑ i ∈ s, w i * z i

Tactic:
apply_rules [sum_nonneg, rpow_nonneg]

Goal state after:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ ∀ i ∈ s, 0 ≤ w i * z i
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
⊢ 0 ≤ (∑ i ∈ s, w i * z i ^ p) ^ (1 / p)

Tactic:
apply_rules [sum_nonneg, rpow_nonneg]

Goal state after:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ ∀ i ∈ s, 0 ≤ w i * z i ^ p
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:

Tactic:
(∫⁻ a : α, (f * g) a ∂μ) =
        ∫⁻ a : α, (funMulInvSnorm f p μ * funMulInvSnorm g q μ) a * (npf * nqg) ∂μ := by
      refine lintegral_congr fun a => ?_
      rw [Pi.mul_apply, fun_eq_funMulInvSnorm_mul_eLpNorm f hf_nonzero hf_nontop,
        fun_eq_funMulInvSnorm_mul_eLpNorm g hg_nonzero hg_nontop, Pi.mul_apply]
      ring
    _ ≤ npf * nqg := by
      rw [lintegral_mul_const' (npf * nqg) _
          (by simp [npf, nqg, hf_nontop, hg_nontop, hf_nonzero, hg_nonzero, ENNReal.mul_eq_top])]
      refine mul_le_of_le_one_left' ?_
      have hf1 := lintegral_rpow_funMulInvSnorm_eq_one hpq.pos hf_nonzero hf_nontop
      have hg1 := lintegral_rpow_funMulInvSnorm_eq_one hpq.symm.pos hg_nonzero hg_nontop
      exact lintegral_mul_le_one_of_lintegral_rpow_eq_one hpq (hf.mul_const _) hf1 hg1

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

Goal state before:
pp: case neg
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ∞
hp1_real : 1 ≤ p.toReal
⊢ eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ

Tactic:
repeat rw [eLpNorm_eq_eLpNorm' hp0 hp_top]

Goal state after:
case neg
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
p : ℝ≥0∞
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
hp1 : 1 ≤ p
hp0 : ¬p = 0
hp_top : ¬p = ∞
hp1_real : 1 ≤ p.toReal
⊢ eLpNorm' (f + g) p.toReal μ ≤ eLpNorm' f p.toReal μ + eLpNorm' g p.toReal μ
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 μ := ?_

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
p : ℝ≥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 ↦ ↑c • ‖f x‖ * ‖g x‖) p μ ≤ ↑c * eLpNorm f ∞ μ * eLpNorm g p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
p q r : ℝ≥0∞
f : α → E
g : α → F
b : E → F → G
c : ℝ≥0
hf : MemLp f p μ
hg : MemLp g q μ
h : AEStronglyMeasurable (fun x ↦ b (f x) (g x)) μ
hb : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr : p.HolderTriple q r
⊢ MemLp (fun x ↦ b (f x) (g x)) r μ

Tactic:
refine ⟨h, ?_⟩

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
p q r : ℝ≥0∞
f : α → E
g : α → F
b : E → F → G
c : ℝ≥0
hf : MemLp f p μ
hg : MemLp g q μ
h : AEStronglyMeasurable (fun x ↦ b (f x) (g x)) μ
hb : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hpqr : p.HolderTriple q r
⊢ eLpNorm (fun x ↦ b (f x) (g x)) r μ < ∞
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
p q r : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
φ : α → 𝕜
hφ : AEStronglyMeasurable φ μ
hpqr : p.HolderTriple q r
⊢ eLpNorm (φ • f) r μ ≤ eLpNorm φ p μ * eLpNorm f q μ

Tactic:
simpa using! (eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm hφ 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
bdd : BddAbove (Set.range fun s ↦ ∑ i ∈ s, (f i + g i) ^ p)
H₂ : Summable fun i ↦ (f i + g i) ^ p
⊢ ∑' (i : ι), (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p

Tactic:
exact H₂.tsum_le_of_sum_le H₁

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
i : ι
x✝ : i ∈ s
⊢ 0 ≤ w i

Tactic:
have := hw i; positivity

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : eLpNorm' (fun x ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
⊢ ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p

Tactic:
← inv_inv p,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hn : eLpNorm' (fun x ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
⊢ ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p⁻¹⁻¹ ∂μ ≤ (∑' (i : ℕ), B i) ^ p⁻¹⁻¹
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_4
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  ∑ x ∈ s, ↑(w x).toNNReal * ↑(f x).toNNReal ≤ (∑ i ∈ s, ↑(w i).toNNReal) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
⊢ (∑ i ∈ s, w i) ^ (1 - p⁻¹) = (∑ i ∈ s, ↑(w i).toNNReal) ^ (1 - p⁻¹)

Tactic:
convert! rfl with i hi
    exact coe_toNNReal (H'.1 _ hi)

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

Goal state before:
pp: case pos.refine_2
α : 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_1 : ℕ), N ≤ n → N ≤ m_1 → essSup (fun x ↦ ‖(f n - f m_1) x‖ₑ) μ < B N
x : α
hx : ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
⊢ Tendsto (fun n ↦ (B n).toReal) atTop (𝓝 0)

Tactic:
← ENNReal.toReal_zero

Goal state after:
case pos.refine_2
α : 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_1 : ℕ), N ≤ n → N ≤ m_1 → essSup (fun x ↦ ‖(f n - f m_1) x‖ₑ) μ < B N
x : α
hx : ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
⊢ Tendsto (fun n ↦ (B n).toReal) atTop (𝓝 (ENNReal.toReal 0))
Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic

Goal state before:
pp: R : Type u
ι : Type v
M : Type u_1
inst✝⁷ : Fintype ι
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousMul R
inst✝ : ContinuousSMul R M
z : M
⊢ ContinuousMultilinearMap.mkPiRing R ι z = 0 ↔ z = 0

Tactic:
rw [← mkPiRing_zero, mkPiRing_eq_iff]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x | IsUnit x}

Tactic:
nontriviality R
  rw [Metric.isOpen_iff]
  rintro _ ⟨x, rfl⟩
  refine ⟨‖(↑x⁻¹ : R)‖⁻¹, _root_.inv_pos.mpr (Units.norm_pos x⁻¹), fun y hy ↦ ?_⟩
  rw [mem_ball_iff_norm] at hy
  exact (x.ofNearby y hy).isUnit

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ.real (s₃ \ s₁) = 0
h' : μ (s₃ \ s₁) ≠ ∞
⊢ μ.real s₁ = μ.real s₂ ∧ μ.real s₂ = μ.real s₃

Tactic:
have A : μ s₁ = μ s₂ ∧ μ s₂ = μ s₃ :=
    measure_eq_measure_of_between_null_sdiff h12 h23 ((measureReal_eq_zero_iff h').1 h_nulldiff)

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ.real (s₃ \ s₁) = 0
h' : μ (s₃ \ s₁) ≠ ∞
A : μ s₁ = μ s₂ ∧ μ s₂ = μ s₃
⊢ μ.real s₁ = μ.real s₂ ∧ μ.real s₂ = μ.real s₃
Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator

Goal state before:
pp: case refine_1
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : MemLp (f + g) p μ
⊢ MemLp f p μ

Tactic:
rw [← Set.indicator_add_eq_left h]

Goal state after:
case refine_1
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : MemLp (f + g) p μ
⊢ MemLp ((support f).indicator (f + g)) p μ
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

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

Tactic:
simpa using hf.integrable_norm_rpow (mod_cast hp) (by simp)

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
s : Set β
hs : s ∈ map e l
int : IntegrableOn f s (μ.restrict (range e))
⊢ ∃ s ∈ map e l, IntegrableOn f s μ

Tactic:
exact ⟨_, inter_mem hs range_mem_map, int.inter_of_restrict⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SeminormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
k n : ℕ
f : G [×n]→L[𝕜] G'
s : Finset (Fin n)
hk : #s = k
z : G
⊢ ‖f.restr s hk z‖ ≤ ‖f‖ * ‖z‖ ^ (n - k)

Tactic:
apply MultilinearMap.mkContinuous_norm_le

Goal state after:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SeminormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
k n : ℕ
f : G [×n]→L[𝕜] G'
s : Finset (Fin n)
hk : #s = k
z : G
⊢ 0 ≤ ‖f‖ * ‖z‖ ^ (n - k)
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: case pos
X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (fun i ↦ f i) L
h✝¹ : L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝ : Function.HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝
⊢ StronglyMeasurable (L.support.mulIndicator (fun i ↦ f i) x✝¹.down)

Tactic:
rw [Set.mulIndicator]

Goal state after:
case pos
X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (fun i ↦ f i) L
h✝¹ : L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝ : Function.HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝
⊢ StronglyMeasurable (if x✝¹.down ∈ L.support then f x✝¹.down else 1)
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: case pos
X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝ : Function.HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝
⊢ AEStronglyMeasurable (L.support.mulIndicator (fun i ↦ f i) x✝¹.down) μ

Tactic:
rw [Set.mulIndicator]

Goal state after:
case pos
X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝ : Function.HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝
⊢ AEStronglyMeasurable (if x✝¹.down ∈ L.support then f x✝¹.down else 1) μ
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case refine_1
𝕜 : 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 ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
⊢ ‖f.flipMultilinear‖ ≤ ‖f‖

Tactic:
apply MultilinearMap.mkContinuous_norm_le

Goal state after:
case refine_1
𝕜 : 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 ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
⊢ 0 ≤ ‖f‖
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞
⊢ MemLp (⇑f) p μ

Tactic:
by
  by_cases hp0 : p = 0
  · rw [hp0, memLp_zero_iff_aestronglyMeasurable]; exact f.aestronglyMeasurable
  by_cases hp_top : p = ∞
  · rw [hp_top]; exact memLp_top f μ
  refine ⟨f.aestronglyMeasurable, ?_⟩
  rw [eLpNorm_eq_eLpNorm' hp0 hp_top, f.eLpNorm'_eq]
  refine ENNReal.rpow_lt_top_of_nonneg (by simp) (ENNReal.sum_lt_top.mpr fun y _ => ?_).ne
  by_cases hy0 : y = 0
  · simp [hy0, ENNReal.toReal_pos hp0 hp_top]
  · refine ENNReal.mul_lt_top ?_ (hf y hy0)
    exact ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg ENNReal.coe_ne_top

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PartialOrder F
inst✝ : IsOrderedModule ℝ F
s : Set α
x : F
hx : 0 ≤ x
⊢ 0 ≤ μ.real s • x

Tactic:
exact smul_nonneg toReal_nonneg hx

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PartialOrder F
inst✝ : IsOrderedModule ℝ F
s : Set α
x : F
hx : 0 ≤ x
⊢ 0 ≤ (weightedSMul μ s) x

Tactic:
simp only [weightedSMul, _root_.id, coe_id', smul_apply]
  exact smul_nonneg toReal_nonneg hx

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' T'' : Set α → E →L[ℝ] F
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
this : ∀ x ∈ {x ∈ f.range | x ≠ 0}, T'' (⇑f ⁻¹' {x}) = T (⇑f ⁻¹' {x}) + T' (⇑f ⁻¹' {x})
x : E
hx : x ∈ {x ∈ f.range | x ≠ 0}
⊢ (T'' (⇑f ⁻¹' {x})) x = (T (⇑f ⁻¹' {x})) x + (T' (⇑f ⁻¹' {x})) x

Tactic:
rw [this x hx]

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' T'' : Set α → E →L[ℝ] F
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
this : ∀ x ∈ {x ∈ f.range | x ≠ 0}, T'' (⇑f ⁻¹' {x}) = T (⇑f ⁻¹' {x}) + T' (⇑f ⁻¹' {x})
x : E
hx : x ∈ {x ∈ f.range | x ≠ 0}
⊢ (T (⇑f ⁻¹' {x}) + T' (⇑f ⁻¹' {x})) x = (T (⇑f ⁻¹' {x})) x + (T' (⇑f ⁻¹' {x})) x
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝⁶ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ integral f = (integralCLM' 𝕜) f

Tactic:
by
  apply isClosed_property (simpleFunc.denseRange one_ne_top)
    (isClosed_eq _ (integralCLM' 𝕜).continuous) _ f
  · simp_rw [integral_def]
    exact (integralCLM (E := E)).continuous
  intro f
  norm_cast

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (fun i ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
⊢ Tendsto (fun i ↦ ∫ (x : α), F i x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))

Tactic:
by
  simp only [integral_eq_setToFun]
  exact tendsto_setToFun_of_L1 (dominatedFinMeasAdditive_weightedSMul μ) f hfi hFi hF

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (fun i ↦ eLpNorm (F i - f) 1 μ) l (𝓝 0)
⊢ Tendsto (fun i ↦ ∫ (x : α), F i x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))

Tactic:
refine tendsto_integral_of_L1 f hfi hFi ?_
  simp_rw [eLpNorm_one_eq_lintegral_enorm, Pi.sub_apply] at hF
  exact hF

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

Goal state before:
pp: case inl
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
x : F
hs : MeasurableSet ∅
⊢ setToSimpleFunc T (piecewise ∅ hs (const α x) (const α 0)) = (T ∅) x

Tactic:
simp only [hT_empty, zero_apply, piecewise_empty, const_zero,
      setToSimpleFunc_zero_apply]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
⊢ Tendsto v l (𝓝 c)

Tactic:
by_cases h : c = 0

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
h : c = 0
⊢ Tendsto v l (𝓝 c)

case neg
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
h : ¬c = 0
⊢ Tendsto v l (𝓝 c)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ ∀ (x : α), 0 x ≤ f x → (fun a ↦ ENNReal.ofReal (-f a)) x = 0 x

Tactic:
simp only [Pi.zero_apply]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ ∀ (x : α), 0 ≤ f x → ENNReal.ofReal (-f x) = 0
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case mpr.refine_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ Tendsto (φ - 1) l (𝓝 (1 - 1))

Tactic:
exact hφ.sub tendsto_const_nhds

Goal state after: