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

Goal state before:
pp: case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ↑(∑ i ∈ s, (f i).toNNReal * (g i).toNNReal) ≤
    ↑((∑ i ∈ s, (f i).toNNReal ^ p) ^ (1 / p) * (∑ i ∈ s, (g i).toNNReal ^ q) ^ (1 / q))
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Tactic:
simp [ENNReal.coe_rpow_of_nonneg, hpq.pos.le, hpq.symm.pos.le] at this

Goal state after:
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ i ∈ s, ↑(f i).toNNReal * ↑(g i).toNNReal ≤
    (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ p⁻¹ * (∑ x ∈ s, ↑(g x).toNNReal ^ q) ^ q⁻¹
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)
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
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
hp_pos : 0 < p
h_pow : ∫⁻ (a : α), (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
⊢ (∫⁻ (a : α), (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i

Tactic:
one_div,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
hp_pos : 0 < p
h_pow : ∫⁻ (a : α), (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
⊢ (∫⁻ (a : α), (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: case e'_6
α : 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) μ
x : α
⊢ ‖f x‖ = ‖‖f x‖ ^ q.toReal‖ ^ q⁻¹.toReal

Tactic:
Real.norm_eq_abs,

Goal state after:
case e'_6
α : 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) μ
x : α
⊢ ‖f x‖ = |‖f x‖ ^ q.toReal| ^ q⁻¹.toReal
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
K : Type u_8
inst✝ : RCLike K
f : α → K
⊢ MemLp (fun x ↦ RCLike.re (f x)) p μ ∧ MemLp (fun x ↦ RCLike.im (f x)) p μ → MemLp f p μ

Tactic:
rintro ⟨hre, him⟩

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
K : Type u_8
inst✝ : RCLike K
f : α → K
hre : MemLp (fun x ↦ RCLike.re (f x)) p μ
him : MemLp (fun x ↦ RCLike.im (f x)) p μ
⊢ MemLp f p μ
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
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
h : (∫⁻ (a : α), (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_tsum_lt_top : (∑' (i : ℕ), B i) ^ p < ∞
⊢ ∫⁻ (a : α), (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p

Tactic:
one_div,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
h : (∫⁻ (a : α), (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
hp_pos : 0 < p
h_tsum_lt_top : (∑' (i : ℕ), B i) ^ p < ∞
⊢ ∫⁻ (a : α), (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, 1 / ε ^ p.toReal * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ μ {x | ε ≤ edist (f n x) (g x)} ≤ 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal

Tactic:
one_div,

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst✝ : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, 1 / ε ^ p.toReal * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ μ {x | ε ≤ edist (f n x) (g x)} ≤ (ε ^ p.toReal)⁻¹ * eLpNorm (f n - g) p μ ^ p.toReal
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: case right
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ eLpNorm (f N) p μ < ∞

Tactic:
· exact (hf N).2

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ t ≠ ∞
⊢ μ.real s ≤ μ.real (s ∪ t)

Tactic:
rcases eq_top_or_lt_top (μ s) with hs | hs

Goal state after:
case inl
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ t ≠ ∞
hs : μ s = ∞
⊢ μ.real s ≤ μ.real (s ∪ t)

case inr
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ t ≠ ∞
hs : μ s < ∞
⊢ μ.real s ≤ μ.real (s ∪ t)
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
μ : Measure α
f : β → Set α
a✝ : β
s✝ : Finset β
hx : a✝ ∉ s✝
IH : μ.real (⋃ b ∈ s✝, f b) ≤ ∑ p ∈ s✝, μ.real (f p)
⊢ μ.real (⋃ b ∈ insert a✝ s✝, f b) ≤ ∑ p ∈ insert a✝ s✝, μ.real (f p)

Tactic:
simp only [hx, Finset.mem_insert, iUnion_iUnion_eq_or_left, not_false_eq_true,
      Finset.sum_insert]
    exact (measureReal_union_le _ _).trans (by gcongr)

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
this : μ (s ∪ t) ≠ ∞
⊢ μ.real ((s ∪ t) ∩ t) + μ.real ((s ∪ t) \ t) + μ.real (s ∩ t) = μ.real s + μ.real t

Tactic:
Set.union_inter_cancel_right,

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
this : μ (s ∪ t) ≠ ∞
⊢ μ.real t + μ.real ((s ∪ t) \ t) + μ.real (s ∩ t) = μ.real s + μ.real t
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
⊢ μ.real (s ∪ t) = μ.real s + μ.real t

Tactic:
simp only [Measure.real]
  rw [measure_union₀ ht hd, ENNReal.toReal_add h₁ h₂]

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
hst : s ⊆ t
ε : ℝ
h : μ.real t < μ.real s + ε
ht' : μ t ≠ ∞
⊢ μ.real (t \ s) < ε

Tactic:
by
  rw [measureReal_sdiff hst hs ht']; linarith

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
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
hp₁ : Fact (1 ≤ p)
β : Type u_3
l : Filter β
t : β → Set α
ht : ∀ (b : β), MeasurableSet (t b)
hμt : ∀ (b : β), μ (t b) ≠ ∞
hp : p ≠ ∞
h : Tendsto (fun b ↦ μ (t b ∆ s)) l (𝓝 0)
⊢ Tendsto (fun b ↦ indicatorConstLp p ⋯ ⋯ c) l (𝓝 (indicatorConstLp p hs hμs c))

Tactic:
tendsto_iff_dist_tendsto_zero

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
hp₁ : Fact (1 ≤ p)
β : Type u_3
l : Filter β
t : β → Set α
ht : ∀ (b : β), MeasurableSet (t b)
hμt : ∀ (b : β), μ (t b) ≠ ∞
hp : p ≠ ∞
h : Tendsto (fun b ↦ μ (t b ∆ s)) l (𝓝 0)
⊢ Tendsto (fun b ↦ dist (indicatorConstLp p ⋯ ⋯ c) (indicatorConstLp p hs hμs c)) l (𝓝 0)
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
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
hp₁ : Fact (1 ≤ p)
β : Type u_3
l : Filter β
t : β → Set α
ht : ∀ (b : β), MeasurableSet (t b)
hμt : ∀ (b : β), μ (t b) ≠ ∞
hp : p ≠ ∞
h : Tendsto (fun b ↦ μ (t b ∆ s)) l (𝓝 0)
⊢ Tendsto (fun b ↦ dist (indicatorConstLp p ⋯ ⋯ c) (indicatorConstLp p hs hμs c)) l (𝓝 0)

Tactic:
have hp₀ : p ≠ 0 := (one_pos.trans_le hp₁.out).ne'

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
hp₁ : Fact (1 ≤ p)
β : Type u_3
l : Filter β
t : β → Set α
ht : ∀ (b : β), MeasurableSet (t b)
hμt : ∀ (b : β), μ (t b) ≠ ∞
hp : p ≠ ∞
h : Tendsto (fun b ↦ μ (t b ∆ s)) l (𝓝 0)
hp₀ : p ≠ 0
⊢ Tendsto (fun b ↦ dist (indicatorConstLp p ⋯ ⋯ c) (indicatorConstLp p hs hμs c)) l (𝓝 0)
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

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

Tactic:
← Real.rpow_natCast

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℕ
hpq : p ≤ q
hint : Integrable (fun x ↦ ‖f x‖ ^ ↑q) μ
⊢ Integrable (fun x ↦ ‖f x‖ ^ ↑p) μ
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case inr
𝕜 : 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
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑f
h✝ : Nonempty ι
ε : ℝ
ε0 : 0 < ε
hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → ‖f m‖ < 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < (‖c‖ / ε) ^ Fintype.card ι
m : (i : ι) → E i
hcm : ∀ (i : ι), ε / ‖c‖ ≤ ‖m i‖
hm : ∀ (i : ι), ‖m i‖ < ε
⊢ 1 / (‖c‖ / ε) ^ Fintype.card ι ≤ ∏ i, ‖m i‖

Tactic:
one_div,

Goal state after:
case inr
𝕜 : 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
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑f
h✝ : Nonempty ι
ε : ℝ
ε0 : 0 < ε
hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → ‖f m‖ < 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < (‖c‖ / ε) ^ Fintype.card ι
m : (i : ι) → E i
hcm : ∀ (i : ι), ε / ‖c‖ ≤ ‖m i‖
hm : ∀ (i : ι), ‖m i‖ < ε
⊢ ((‖c‖ / ε) ^ Fintype.card ι)⁻¹ ≤ ∏ i, ‖m i‖
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst✝⁴ : TopologicalSpace ε
inst✝³ : ContinuousENorm ε
inst✝² : Preorder α
inst✝¹ : IsCodirectedOrder α
inst✝ : Nonempty α
⊢ IntegrableAtFilter f atBot μ ↔ ∃ a, IntegrableOn f (Iic a) μ

Tactic:
refine ⟨fun ⟨s, hs, hi⟩ ↦ ?_, fun ⟨a, ha⟩ ↦ ⟨Iic a, Iic_mem_atBot a, ha⟩⟩

Goal state after:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst✝⁴ : TopologicalSpace ε
inst✝³ : ContinuousENorm ε
inst✝² : Preorder α
inst✝¹ : IsCodirectedOrder α
inst✝ : Nonempty α
x✝ : IntegrableAtFilter f atBot μ
s : Set α
hs : s ∈ atBot
hi : IntegrableOn f s μ
⊢ ∃ a, IntegrableOn f (Iic a) μ
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝² : NormedAddCommGroup E
μ : Measure α
l : Filter α
𝕜 : Type u_7
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → E
c : 𝕜
hc : c ≠ 0
⊢ IntegrableAtFilter (c • f) l μ ↔ IntegrableAtFilter f l μ

Tactic:
refine ⟨fun hf ↦ ?_, fun h ↦ h.smul c⟩

Goal state after:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝² : NormedAddCommGroup E
μ : Measure α
l : Filter α
𝕜 : Type u_7
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → E
c : 𝕜
hc : c ≠ 0
hf : IntegrableAtFilter (c • f) l μ
⊢ IntegrableAtFilter f l μ
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_9
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
a✝ : AEStronglyMeasurable f μ
this : ∀ (x : ℝ≥0∞), x = 0 → x < ∞
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞ ∧ ‖c‖ₑ < ∞ ∨ ∫⁻ (a : α), ‖f a‖ₑ ∂μ = 0 ∨ ‖c‖ₑ = 0 ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

Tactic:
simp [hc, or_iff_left_of_imp (this _)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α →ₘ[μ] β
⊢ f.Integrable ↔ f ∈ Lp β 1 μ

Tactic:
by
  rw [← integrable_coeFn, ← memLp_one_iff_integrable, Lp.mem_Lp_iff_memLp]

Goal state after:
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 ι
g : ContinuousMultilinearMap 𝕜 E₁ G
h : DecidableEq ι
f : (i : ι) → E i →L[𝕜] E₁ i
i : ι
⊢ ∀ (c : 𝕜) (x : E i →L[𝕜] E₁ i),
    g.compContinuousLinearMap (update f i (c • x)) = c • g.compContinuousLinearMap (update f i x)

Tactic:
a

Goal state after:
𝕜 : 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 ι
g : ContinuousMultilinearMap 𝕜 E₁ G
h : DecidableEq ι
f : (i : ι) → E i →L[𝕜] E₁ i
i : ι
a : 𝕜
⊢ ∀ (x : E i →L[𝕜] E₁ i), g.compContinuousLinearMap (update f i (a • x)) = a • g.compContinuousLinearMap (update f i x)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x ↦ y₀) p μ
n : ℕ
hf' : MemLp (fun x ↦ ‖f x - y₀‖) p μ
x : β
⊢ ‖‖f x - y₀‖ + ‖f x - y₀‖‖ = ‖f x - y₀‖ + ‖f x - y₀‖

Tactic:
Real.norm_eq_abs,

Goal state after:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x ↦ y₀) p μ
n : ℕ
hf' : MemLp (fun x ↦ ‖f x - y₀‖) p μ
x : β
⊢ |‖f x - y₀‖ + ‖f x - y₀‖| = ‖f x - y₀‖ + ‖f x - y₀‖
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁷ : AddCommGroup E
inst✝¹⁶ : UniformSpace E
inst✝¹⁵ : IsUniformAddGroup E
inst✝¹⁴ : AddCommGroup F
inst✝¹³ : UniformSpace F
inst✝¹² : IsUniformAddGroup F
inst✝¹¹ : T0Space F
inst✝¹⁰ : AddCommMonoid Eₗ
inst✝⁹ : UniformSpace Eₗ
inst✝⁸ : ContinuousAdd Eₗ
inst✝⁷ : Semiring 𝕜
inst✝⁶ : Semiring 𝕜₂
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : Module 𝕜 Eₗ
inst✝² : ContinuousConstSMul 𝕜 Eₗ
inst✝¹ : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f g : E →SL[σ₁₂] F
inst✝ : CompleteSpace F
e : E →L[𝕜] Eₗ
h : DenseRange ⇑e ∧ IsUniformInducing ⇑e
cont : Continuous (⋯.extend ⇑f)
eq : ∀ (b : E), ⋯.extend (⇑f) (e b) = f b
k : 𝕜
b : Eₗ
x : E
⊢ ⋯.extend (⇑f) (k • e x) = σ₁₂ k • ⋯.extend (⇑f) (e x)

Tactic:
rw [← map_smul]

Goal state after:
case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁷ : AddCommGroup E
inst✝¹⁶ : UniformSpace E
inst✝¹⁵ : IsUniformAddGroup E
inst✝¹⁴ : AddCommGroup F
inst✝¹³ : UniformSpace F
inst✝¹² : IsUniformAddGroup F
inst✝¹¹ : T0Space F
inst✝¹⁰ : AddCommMonoid Eₗ
inst✝⁹ : UniformSpace Eₗ
inst✝⁸ : ContinuousAdd Eₗ
inst✝⁷ : Semiring 𝕜
inst✝⁶ : Semiring 𝕜₂
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : Module 𝕜 Eₗ
inst✝² : ContinuousConstSMul 𝕜 Eₗ
inst✝¹ : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f g : E →SL[σ₁₂] F
inst✝ : CompleteSpace F
e : E →L[𝕜] Eₗ
h : DenseRange ⇑e ∧ IsUniformInducing ⇑e
cont : Continuous (⋯.extend ⇑f)
eq : ∀ (b : E), ⋯.extend (⇑f) (e b) = f b
k : 𝕜
b : Eₗ
x : E
⊢ ⋯.extend (⇑f) (e (k • x)) = σ₁₂ k • ⋯.extend (⇑f) (e x)
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a✝ : α
⊢ ‖f.posPart a✝‖ = f.posPart a✝

Tactic:
Real.norm_eq_abs,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a✝ : α
⊢ |f.posPart a✝| = f.posPart a✝
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n ↦ approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
n : ℕ
⊢ 0 ≤ x n

Tactic:
a

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n ↦ approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
n : ℕ
a : α
⊢ 0 a ≤ (x n) a
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable (⇑f) (μ + ν)
⊢ setToSimpleFunc (weightedSMul (μ + ν)) f = setToSimpleFunc (weightedSMul μ) f + setToSimpleFunc (weightedSMul ν) f

Tactic:
refine setToSimpleFunc_add_left'
    (weightedSMul μ) (weightedSMul ν) (weightedSMul (μ + ν)) (fun s _ hμνs => ?_) hf

Goal state after:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable (⇑f) (μ + ν)
s : Set α
x✝ : MeasurableSet s
hμνs : (μ + ν) s < ∞
⊢ weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝² : MeasurableSpace G := borel G
this✝¹ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this✝ : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n ↦ approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp (⇑(x n)) p μ
h_toLp : ∀ (n : ℕ), ↑↑(MemLp.toLp ⇑(x n) ⋯) =ᵐ[μ] ⇑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
hx_tendsto : Tendsto (fun n ↦ eLpNorm (⇑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
this : Tendsto (fun n ↦ ↑((x n).toLp ⋯)) atTop (𝓝 ↑g)
⊢ Tendsto (fun n ↦ coeSimpleFuncNonnegToLpNonneg p μ G ⟨(x n).toLp ⋯, ⋯⟩) atTop (𝓝 g)

Tactic:
tendsto_iff_dist_tendsto_zero

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝² : MeasurableSpace G := borel G
this✝¹ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this✝ : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n ↦ approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp (⇑(x n)) p μ
h_toLp : ∀ (n : ℕ), ↑↑(MemLp.toLp ⇑(x n) ⋯) =ᵐ[μ] ⇑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
hx_tendsto : Tendsto (fun n ↦ eLpNorm (⇑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
this : Tendsto (fun b ↦ dist ↑((x b).toLp ⋯) ↑g) atTop (𝓝 0)
⊢ Tendsto (fun b ↦ dist (coeSimpleFuncNonnegToLpNonneg p μ G ⟨(x b).toLp ⋯, ⋯⟩) g) atTop (𝓝 0)
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
⊢ (u - u) =o[l] u

Tactic:
sub_self

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
⊢ 0 =o[l] u
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto u l (𝓝 c)
this : Tendsto (fun x ↦ u x - c) l (𝓝 (c - c))
⊢ Tendsto (u - fun x ↦ c) l (𝓝 0)

Tactic:
sub_self

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto u l (𝓝 c)
this : Tendsto (fun x ↦ u x - c) l (𝓝 0)
⊢ Tendsto (u - fun x ↦ c) l (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ

Tactic:
refine lintegral_congr_ae (hf.mono fun a h => ?_)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
a : α
h : 0 a ≤ f a
⊢ (fun a ↦ ENNReal.ofReal (f a)) a = (fun a ↦ ENNReal.ofReal ‖f a‖) a