mathlib-initiative/mathlib-tactics huggingface dataset:
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 γ
𝕜 : Type u_5
𝕜' : Type u_6
inst✝⁵ : SMul 𝕜 γ
inst✝⁴ : ContinuousConstSMul 𝕜 γ
inst✝³ : SMul 𝕜' γ
inst✝² : ContinuousConstSMul 𝕜' γ
inst✝¹ : SMul 𝕜 𝕜'
inst✝ : IsScalarTower 𝕜 𝕜' γ
a : 𝕜
b : 𝕜'
f✝ : α →ₘ[μ] γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ mk ((a • b) • f) ⋯ = mk (a • b • f) ⋯

Tactic:
smul_assoc

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

Goal state before:
pp: α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ
hp : 0 < p
⊢ ∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ ≤ ↑c ^ p * ∫⁻ (a : α), ↑‖g a‖₊ ^ p ∂μ

Tactic:
← ENNReal.coe_rpow_of_nonneg _ hp.le,

Goal state after:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ
hp : 0 < p
⊢ ∫⁻ (a : α), ↑(‖f a‖₊ ^ p) ∂μ ≤ ↑(c ^ p) * ∫⁻ (a : α), ↑(‖g a‖₊ ^ p) ∂μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ
p : ℝ
hp : 0 < p
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ ≤ ↑c ^ p * ∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ

Tactic:
← ENNReal.coe_rpow_of_nonneg _ hp.le,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ
p : ℝ
hp : 0 < p
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ ≤ ↑(c ^ p) * ∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp₀ : p ≠ 0
⊢ ∃ s, MeasurableSet s ∧ μ s < ∞ ∧ ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal

Tactic:
apply exists_setLIntegral_compl_lt

Goal state after:
case hf
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp₀ : p ≠ 0
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ ≠ ∞

case hε
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp₀ : p ≠ 0
⊢ ε ^ p.toReal ≠ 0
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
s : γ → Set α
left✝¹ : s ∈ univ.pi fun i ↦ {s | MeasurableSet s}
t : γ → Set β
left✝ : t ∈ univ.pi fun i ↦ {s | MeasurableSet s}
⊢ ((Measure.pi μ).prod (Measure.pi ν)) ((fun x1 x2 ↦ x1 ×ˢ x2) (univ.pi s) (univ.pi t)) =
    (Measure.pi fun i ↦ (μ i).prod (ν i)) (univ.pi fun i ↦ s i ×ˢ t i)

Tactic:
simp_rw [pi_pi, prod_prod, pi_pi, Finset.prod_mul_distrib]

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

Goal state before:
pp: case pos
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ∞
h_rpow : essSup (fun x ↦ ‖‖f x‖ₑ ^ q‖ₑ) μ = essSup (fun x ↦ ‖f x‖ₑ ^ q) μ
h_rpow_mono : StrictMono fun x ↦ x ^ q
h_rpow_surj : Function.Surjective fun y ↦ y ^ q
⊢ essSup (fun x ↦ ‖f x‖ₑ ^ q) μ = essSup (fun x ↦ ‖f x‖ₑ) μ ^ q

Tactic:
let iso := h_rpow_mono.orderIsoOfSurjective _ h_rpow_surj

Goal state after:
case pos
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hq_pos : 0 < q
h0 : ¬p = 0
hp_top : p = ∞
h_rpow : essSup (fun x ↦ ‖‖f x‖ₑ ^ q‖ₑ) μ = essSup (fun x ↦ ‖f x‖ₑ ^ q) μ
h_rpow_mono : StrictMono fun x ↦ x ^ q
h_rpow_surj : Function.Surjective fun y ↦ y ^ q
iso : ℝ≥0∞ ≃o ℝ≥0∞ := StrictMono.orderIsoOfSurjective (fun x ↦ x ^ q) h_rpow_mono h_rpow_surj
⊢ essSup (fun x ↦ ‖f x‖ₑ ^ q) μ = essSup (fun x ↦ ‖f x‖ₑ) μ ^ q
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case e'_3
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + s) / s = (log (1 + s) - 0) / s

Tactic:
sub_zero

Goal state after:
case e'_3
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + s) / s = log (1 + s) / s
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case e'_4
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + p * s) / (p * s) = (log (1 + p * s) - 0) / (p * s)

Tactic:
sub_zero

Goal state after:
case e'_4
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + p * s) / (p * s) = log (1 + p * s) / (p * s)
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case e'_3
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + p * s) / (p * s) = (log (1 + p * s) - 0) / (p * s)

Tactic:
sub_zero

Goal state after:
case e'_3
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + p * s) / (p * s) = log (1 + p * s) / (p * s)
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case e'_4
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + s) / s = (log (1 + s) - 0) / s

Tactic:
sub_zero

Goal state after:
case e'_4
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + s) / s = log (1 + s) / s
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case e'_3
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + p * s) / (p * s) = (log (1 + p * s) - 0) / (p * s)

Tactic:
sub_zero

Goal state after:
case e'_3
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + p * s) / (p * s) = log (1 + p * s) / (p * s)
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case e'_4
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + s) / s = (log (1 + s) - 0) / s

Tactic:
sub_zero

Goal state after:
case e'_4
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + s) / s = log (1 + s) / s
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ
h : p.HolderConjugate q
⊢ q = p / (p - 1)

Tactic:
convert! inv_inv q ▸ congr($(h.symm.inv_sub_inv_eq_inv.symm)⁻¹) using 1

Goal state after:
p q : ℝ
h : p.HolderConjugate q
⊢ p / (p - 1) = (1⁻¹ - p⁻¹)⁻¹
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case e'_3
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + s) / s = (log (1 + s) - 0) / s

Tactic:
sub_zero

Goal state after:
case e'_3
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + s) / s = log (1 + s) / s
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q : ℝ≥0
hp : 1 < p
⊢ 1 < ↑p

Tactic:
exact_mod_cast hp

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

Goal state before:
pp: case e'_4
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + p * s) / (p * s) = (log (1 + p * s) - 0) / (p * s)

Tactic:
sub_zero

Goal state after:
case e'_4
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + p * s) / (p * s) = log (1 + p * s) / (p * s)
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p q r : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal r.toReal
hp : 0 < p.toReal
⊢ p.HolderTriple q r

Tactic:
have hq := h.symm.pos

Goal state after:
p q r : ℝ≥0∞
h : p.toReal.HolderTriple q.toReal r.toReal
hp : 0 < p.toReal
hq : 0 < q.toReal
⊢ p.HolderTriple q r
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case hpq
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  (∀ i ∈ s, AEMeasurable (f i) μ) →
    ∀ {p : ι → ℝ},
      ∑ i ∈ s, p i = 1 →
        (∀ i ∈ s, 0 ≤ p i) → ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : ∑ i ∈ insert i₀ s, p i = 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : ι → ℝ := ⋯
hq : ∑ i ∈ s, q i = 1
h2q : ∀ i ∈ s, 0 ≤ q i
⊢ p i₀ + (1 - p i₀) = 1

Tactic:
· apply add_sub_cancel

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)

Tactic:
have hpq := Real.HolderConjugate.conjExponent hp

Goal state after:
case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hpq : p.HolderConjugate p.conjExponent
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst✝¹ : PseudoEMetricSpace F
inst✝ : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
⊢ TendstoInMeasure μ (fun i ↦ s.indicator (f i)) l (s.indicator g)

Tactic:
by
  refine fun ε hε => tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds (hg ε hε) ?_ ?_
  · intro; simp
  · refine fun n => measure_mono (fun x hx => ?_)
    by_cases x ∈ s <;> simp_all

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

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

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

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
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:
eLpNorm_eq_eLpNorm' (zero_lt_one.trans_le hp).ne.symm hp_top

Goal state after:
α : 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.toReal μ < B N
hn : N ≤ n
hm : N ≤ m
⊢ eLpNorm' (f n - f m) p.toReal μ < B N
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: case left
α : 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_lim - f N) p μ ≤ 1

Tactic:
have h_neg : f_lim - f N = -(f N - f_lim) := by simp

Goal state after:
case left
α : 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
h_neg : f_lim - f N = -(f N - f_lim)
⊢ eLpNorm (f_lim - f N) p μ ≤ 1
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
t : R
ht : dist t 0 < ‖↑x⁻¹‖⁻¹
⊢ (↑x + t)⁻¹ʳ = (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹

Tactic:
dist_zero_right

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
a✝ : Nontrivial R
t : R
ht : ‖t‖ < ‖↑x⁻¹‖⁻¹
⊢ (↑x + t)⁻¹ʳ = (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
t : R
ht : dist t 0 < 2⁻¹
⊢ ‖(1 - t)⁻¹ʳ‖ ≤ (‖1‖ + 1) * ‖1‖

Tactic:
dist_zero_right

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
⊢ ‖(1 - t)⁻¹ʳ‖ ≤ (‖1‖ + 1) * ‖1‖
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedAddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : SeminormedAddCommGroup G
inst✝ : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f

Tactic:
refine continuous_iff_continuousAt.2 fun x ↦ tendsto_sub_nhds_zero_iff.1 ?_
  suffices Tendsto (fun y : E × F ↦ f (y.1 - x.1, y.2) + f (x.1, y.2 - x.2)) (𝓝 x) (𝓝 (0 + 0)) by
    simpa only [h.map_sub_left, h.map_sub_right, sub_add_sub_cancel, zero_add] using this
  apply Tendsto.add
  · rw [← isLittleO_one_iff ℝ, ← one_mul 1]
    refine h.isBigO_comp.trans_isLittleO ?_
    refine (IsLittleO.norm_left ?_).mul_isBigO (IsBigO.norm_left ?_)
    · exact (isLittleO_one_iff _).2 (tendsto_sub_nhds_zero_iff.2 (continuous_fst.tendsto _))
    · exact (continuous_snd.tendsto _).isBigO_one ℝ
  · rw [← isLittleO_one_iff ℝ]
    refine h.isBigO_comp.trans_isLittleO ?_
    apply IsLittleO.const_mul_left
    rw [isLittleO_norm_left, isLittleO_one_iff, ← sub_self x.2]
    exact continuous_snd.continuousAt.sub tendsto_const_nhds

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

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

Tactic:
simp only [measureReal_def]
  rw [measure_sdiff_null']
  exact (measureReal_eq_zero_iff (measure_ne_top_of_subset inter_subset_left h')).1 h

Goal state after:
Module: Mathlib.Order.Filter.IndicatorFunction

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f g : α → M
l : Filter α
hf : f =ᶠ[l ⊓ 𝓟 s] g
hs : s =ᶠ[l] t
x : α
hst : x ∈ s ↔ x ∈ t
hfg : x ∈ s → f x = g x
hxs : x ∉ s
⊢ s.mulIndicator f x = t.mulIndicator g x

Tactic:
simp only [mulIndicator_of_notMem, hxs, mt hst.2 hxs, not_false_eq_true]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
c : β
hc : c ≠ 0
⊢ Integrable (fun x ↦ c) μ ↔ IsFiniteMeasure μ

Tactic:
simp [integrable_const_iff, hc, isFiniteMeasure_iff]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
s : Set α
inst✝ : NormedSpace ℝ E
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E
h_compLp :
  ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) =ᵐ[μ] fun a ↦
    (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
y : α
hy : ↑↑(indicatorConstLp 2 hs hμs 1) y = s.indicator (fun x ↦ 1) y
⊢ s.indicator (fun x_1 ↦ x) y = (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) y)

Tactic:
rw [hy]

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
s : Set α
inst✝ : NormedSpace ℝ E
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E
h_compLp :
  ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) =ᵐ[μ] fun a ↦
    (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
y : α
hy : ↑↑(indicatorConstLp 2 hs hμs 1) y = s.indicator (fun x ↦ 1) y
⊢ s.indicator (fun x_1 ↦ x) y = (ContinuousLinearMap.toSpanSingleton ℝ x) (s.indicator (fun x ↦ 1) y)
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
f : α → ε'
hs : MeasurableSet s
⊢ IntegrableOn (s.indicator f) t μ ↔ IntegrableOn f (s ∩ t) μ

Tactic:
simp_rw [IntegrableOn, integrable_indicator_iff hs, IntegrableOn, Measure.restrict_restrict hs]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
R : Type u_8
inst✝² : NormedRing R
inst✝¹ : Module R β
inst✝ : IsBoundedSMul R β
f : α → β
hf : MemLp f 1 μ
g : α → R
g_aestronglyMeasurable : AEStronglyMeasurable g μ
ess_sup_g : essSup (fun x ↦ ‖g x‖ₑ) μ ≠ ∞
hg' : eLpNorm g ∞ μ ≠ ∞
⊢ eLpNorm (fun x ↦ g x • f x) 1 μ ≤ eLpNorm g ∞ μ * eLpNorm f 1 μ

Tactic:
by
      simpa using! MeasureTheory.eLpNorm_smul_le_mul_eLpNorm hf.1 g_aestronglyMeasurable
        (p := ∞) (q := 1)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
f : α → β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : AddLeftMono β
hf : Integrable f μ
c : β
c_neg : c < 0
this✝ : 0 < ‖c‖
x : α
hx : x ∈ {a | f a ≤ c}
this : -c ≤ -f x
⊢ x ∈ {x | ‖c‖ ≤ ‖f x‖}

Tactic:
exact norm_le_norm_of_abs_le_abs <| abs_of_nonpos c_neg.le ▸ this.trans (neg_le_abs _)

Goal state after:
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 ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
A : (insert i s).piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₂ i)
B : s.piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₁ i)
⊢ C * ∏ i_1, ‖update (s.piecewise m₂ m₁) i (m₁ i - m₂ i) i_1‖ ≤
    C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
gcongr with j

Goal state after:
case h1
𝕜 : 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 ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
A : (insert i s).piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₂ i)
B : s.piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₁ i)
j : ι
a✝ : j ∈ univ
⊢ ‖update (s.piecewise m₂ m₁) i (m₁ i - m₂ i) j‖ ≤ if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : 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 ∈ map e l, IntegrableOn f s μ) ↔ ∃ s ∈ map e l, IntegrableOn f s (Measure.map e (Measure.comap e μ))

Tactic:
he.map_comap

Goal state after:
α : 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 ∈ map e l, IntegrableOn f s μ) ↔ ∃ s ∈ map e l, IntegrableOn f s (μ.restrict (range e))
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
i : ι
⊢ (∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤ ∏ j, update (fun x ↦ max ‖m₁‖ ‖m₂‖) i ‖m₁ - m₂‖ j

Tactic:
gcongr with j

Goal state after:
case h1
𝕜 : 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
i j : ι
a✝ : j ∈ univ
⊢ (if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤ update (fun x ↦ max ‖m₁‖ ‖m₂‖) i ‖m₁ - m₂‖ j