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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁷ : CommRing 𝕜
inst✝¹⁶ : LinearOrder 𝕜
inst✝¹⁵ : IsStrictOrderedRing 𝕜
inst✝¹⁴ : CommRing E
inst✝¹³ : LinearOrder E
inst✝¹² : IsStrictOrderedRing E
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : LinearOrder F
inst✝⁹ : IsOrderedAddMonoid F
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜 G
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module 𝕜 F
inst✝⁴ : Module E F
inst✝³ : IsScalarTower 𝕜 E F
inst✝² : SMulCommClass 𝕜 E F
inst✝¹ : IsOrderedModule 𝕜 F
inst✝ : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
hf : ConcaveOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
⊢ ConcaveOn 𝕜 s (f • g)

Tactic:
rw [← neg_convexOn_iff, ← smul_neg]
  exact hf.smul'' hg.neg hf₀ (fun x hx ↦ neg_nonpos.2 <| hg₀ hx) hfg.neg_right

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

Goal state before:
pp: case inr.inl
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ eLpNorm' (f + g) p.toReal μ ≤ p.LpAddConst * (eLpNorm' f p.toReal μ + eLpNorm' g p.toReal μ)

Tactic:
convert! eLpNorm'_add_le_of_le_one hf ENNReal.toReal_nonneg _

Goal state after:
case e'_4
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ p.LpAddConst = 2 ^ (1 / p.toReal - 1)

case inr.inl.convert_3
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
μ : Measure α
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
hp : p ≠ 0
h'p : p < 1
⊢ p.toReal ≤ 1
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: w₁ w₂ p₁ p₂ : ℝ
hw₁ : 0 ≤ w₁
hw₂ : 0 ≤ w₂
hp₁ : 0 ≤ p₁
hp₂ : 0 ≤ p₂
hw : w₁ + w₂ = 1
⊢ p₁ ^ w₁ * p₂ ^ w₂ = w₁ * p₁ + w₂ * p₂ ↔ w₁ = 0 ∨ w₂ = 0 ∨ p₁ = p₂

Tactic:
by
  have := geom_mean_eq_arith_mean_weighted_iff_of_nonneg univ ![w₁, w₂] ![p₁, p₂]
  simp at this
  grind

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: w₁ w₂ p₁ p₂ : ℝ
hw₁ : 0 < w₁
hw₂ : 0 < w₂
hp₁ : 0 ≤ p₁
hp₂ : 0 ≤ p₂
hw : w₁ + w₂ = 1
⊢ p₁ ^ w₁ * p₂ ^ w₂ < w₁ * p₁ + w₂ * p₂ ↔ p₁ ≠ p₂

Tactic:
have := geom_mean_lt_arith_mean_weighted_iff_of_pos univ ![w₁, w₂] ![p₁, p₂]
  simp at this
  grind

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

Goal state before:
pp: case inr.inl.inr.e_a.e_a
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hpq : p ≤ ∞
hq0_lt : 0 < ∞
hp_top : p ≠ ∞
hp_pos : 0 < p.toReal
⊢ 1 / p.toReal = p.toReal⁻¹

Tactic:
exact one_div _

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

Goal state before:
pp: α : Type u_2
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)

Tactic:
have hp0_ne : p ≠ 0 := (ne_of_lt hp0_lt).symm

Goal state after:
α : Type u_2
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp0_ne : p ≠ 0
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case h₂.inr.inl
α : 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 α
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 i ↦ ‖f i‖ * ‖g i‖) ∞ μ ≤ eLpNorm f ∞ μ * eLpNorm g ∞ μ

Tactic:
rw [← eLpNorm_norm f, ← eLpNorm_norm g]

Goal state after:
case h₂.inr.inl
α : 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 α
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 i ↦ ‖f i‖ * ‖g i‖) ∞ μ ≤ eLpNorm (fun x ↦ ‖f x‖) ∞ μ * eLpNorm (fun x ↦ ‖g x‖) ∞ μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case h₂.inr.inl
α : 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 α
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 i ↦ ‖f i‖ * ‖g i‖) ∞ μ ≤ eLpNorm (fun x ↦ ‖f x‖) ∞ μ * eLpNorm (fun x ↦ ‖g x‖) ∞ μ

Tactic:
eLpNorm_exponent_top,

Goal state after:
case h₂.inr.inl
α : 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 α
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‖₊
⊢ eLpNormEssSup (fun i ↦ ‖f i‖ * ‖g i‖) μ ≤ eLpNormEssSup (fun x ↦ ‖f x‖) μ * eLpNormEssSup (fun x ↦ ‖g x‖) μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case h₂.inr.inr
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
⊢ (∫⁻ (x : α), ‖‖f x‖ * ‖g x‖‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) ≤
    eLpNorm f ∞ μ * (∫⁻ (x : α), ‖g x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Tactic:
eLpNorm_exponent_top,

Goal state after:
case h₂.inr.inr
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ∞
⊢ (∫⁻ (x : α), ‖‖f x‖ * ‖g x‖‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) ≤
    eLpNormEssSup f μ * (∫⁻ (x : α), ‖g x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case right
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) ∈ upperBounds ((fun g ↦ ∑ i ∈ s, f i * g i) '' {g | ∑ i ∈ s, g i ^ q ≤ 1})

Tactic:
rintro _ ⟨g, hg, rfl⟩

Goal state after:
case right
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
g : ι → ℝ≥0
hg : g ∈ {g | ∑ i ∈ s, g i ^ q ≤ 1}
⊢ (fun g ↦ ∑ i ∈ s, f i * g i) g ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

Tactic:
by_cases h1 : p = 1

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
h1 : p = 1
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
h1 : ¬p = 1
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

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

Tactic:
eLpNorm_exponent_top,

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : SeminormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
l : Filter ι
f : ι → α → E
g : α → E
⊢ (∀ (ε : ℝ≥0∞), 0 < ε → ε ≠ ∞ → Tendsto (fun i ↦ μ {x | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0)) ↔
    ∀ (ε : ℝ≥0∞), 0 < ε → ε ≠ ∞ → Tendsto (fun i ↦ μ.real {x | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0)

Tactic:
congr! with ε hε hε_top

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : SeminormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
l : Filter ι
f : ι → α → E
g : α → E
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
⊢ Tendsto (fun i ↦ μ {x | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0) ↔ Tendsto (fun i ↦ μ.real {x | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0)
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

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

Tactic:
eLpNorm_exponent_top,

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoMetricSpace E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
⊢ (∀ (ε : ℝ), 0 < ε → Tendsto (fun i ↦ μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)) ↔
    ∀ (ε : ℝ), 0 < ε → Tendsto (fun i ↦ μ.real {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)

Tactic:
congr! with ε hε hε_top

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PseudoMetricSpace E
inst✝ : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun i ↦ μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0) ↔
    Tendsto (fun i ↦ μ.real {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : SeminormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
l : Filter ι
f : ι → α → E
g : α → E
⊢ (∀ (ε : ℝ), 0 < ε → Tendsto (fun i ↦ μ {x | ε ≤ ‖f i x - g x‖}) l (𝓝 0)) ↔
    ∀ (ε : ℝ), 0 < ε → Tendsto (fun i ↦ μ.real {x | ε ≤ ‖f i x - g x‖}) l (𝓝 0)

Tactic:
congr! with ε hε hε_top

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : SeminormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
l : Filter ι
f : ι → α → E
g : α → E
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun i ↦ μ {x | ε ≤ ‖f i x - g x‖}) l (𝓝 0) ↔ Tendsto (fun i ↦ μ.real {x | ε ≤ ‖f i x - g x‖}) l (𝓝 0)
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 : ↥(Lp E p μ)
⊢ Tendsto (fun b ↦ (eLpNorm (↑↑(f b) - ↑↑f_lim) p μ).toReal) fi (𝓝 0) ↔
    Tendsto (fun n ↦ eLpNorm (↑↑(f n) - ↑↑f_lim) p μ) fi (𝓝 0)

Tactic:
rw [← ENNReal.toReal_zero, ENNReal.tendsto_toReal_iff (fun n => ?_) ENNReal.zero_ne_top]

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 : ↥(Lp E p μ)
n : ι
⊢ eLpNorm (↑↑(f n) - ↑↑f_lim) p μ ≠ ∞
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
inst✝¹ : Nonempty ι
inst✝ : SemilatticeSup ι
hp : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
⊢ Tendsto (fun n ↦ (eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) p μ).toReal) atTop (𝓝 0) ↔
    Tendsto (fun n ↦ eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) p μ) atTop (𝓝 0)

Tactic:
rw [← ENNReal.toReal_zero, ENNReal.tendsto_toReal_iff (fun n => ?_) ENNReal.zero_ne_top]

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
ι : Type u_4
inst✝¹ : Nonempty ι
inst✝ : SemilatticeSup ι
hp : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
n : ι × ι
⊢ eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) p μ ≠ ∞
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
hf_sum : Summable fun i ↦ f i ^ p
hg_sum : Summable fun i ↦ g i ^ q
hf' : 0 ≤ ∑' (i : ι), f i ^ p
hg' : 0 ≤ ∑' (i : ι), g i ^ q
hr : 0 < r
i : ι
⊢ 0 ≤ (f i * g i) ^ r

Tactic:
positivity [hf i, hg i]

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 g : ↥(Lp E p μ)
⊢ edist f g = eLpNorm (↑↑f - ↑↑g) p μ

Tactic:
edist_eq_eLpNorm_neg_add,

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : ↥(Lp E p μ)
⊢ eLpNorm (-↑↑f + ↑↑g) p μ = eLpNorm (↑↑f - ↑↑g) p μ
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
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ TendstoInMeasure μ f atTop g

Tactic:
have hg : AEStronglyMeasurable g μ := aestronglyMeasurable_of_tendsto_ae _ hf hfg
  refine TendstoInMeasure.congr (fun i => (hf i).ae_eq_mk.symm) hg.ae_eq_mk.symm ?_
  refine tendstoInMeasure_of_tendsto_ae_of_measurable_edist
    (fun n ↦ ((hf n).stronglyMeasurable_mk.edist hg.stronglyMeasurable_mk).measurable) ?_
  have hf_eq_ae : ∀ᵐ x ∂μ, ∀ n, (hf n).mk (f n) x = f n x :=
    ae_all_iff.mpr fun n => (hf n).ae_eq_mk.symm
  filter_upwards [hf_eq_ae, hg.ae_eq_mk, hfg] with x hxf hxg hxfg
  rw [← hxg, funext fun n => hxf n]
  exact hxfg

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✝ : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ↑C
this : ↑‖f‖₊ ≤ ↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C)
⊢ ‖f‖ ≤ ↑(measureUnivNNReal μ) ^ p.toReal⁻¹ * ↑C

Tactic:
NNReal.coe_mul,

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
f : ↥(Lp E p μ)
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ↑C
this : ↑‖f‖₊ ≤ ↑(measureUnivNNReal μ ^ p.toReal⁻¹) * ↑C
⊢ ‖f‖ ≤ ↑(measureUnivNNReal μ) ^ p.toReal⁻¹ * ↑C
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 : α → α
hf : MeasurePreserving f μ μ
n : ℕ
⊢ (⇑(compMeasurePreserving f hf))^[n] = ⇑(compMeasurePreserving f^[n] ⋯)

Tactic:
funext
  induction n with
  | zero => simp
  | succ n h =>
    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: case pos
α : 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 ≤ ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) ∞ μ < B N
hp_top : True
h_cau_ae : ∀ᵐ (x : α) ∂μ, ∀ (N n m : ℕ), N ≤ n → N ≤ m → ‖(f n - f m) x‖ₑ < B N
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) atTop (𝓝 l)

Tactic:
eLpNorm_exponent_top,

Goal state after:
case pos
α : 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 → eLpNormEssSup (f n - f m_1) μ < B N
⊢ ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n ↦ f n x) atTop (𝓝 l)
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 ↦ -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
⊢ ∀ᶠ (t : R) in 𝓝 0, (↑x + t)⁻¹ʳ = (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * (↑x + t)⁻¹ʳ

Tactic:
filter_upwards [inverse_add x, hzero.eventually (inverse_one_sub_nth_order n)] with t ht ht'

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 ↦ -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
t : R
ht : (↑x + t)⁻¹ʳ = (1 + ↑x⁻¹ * t)⁻¹ʳ * ↑x⁻¹
ht' : (1 - -↑x⁻¹ * t)⁻¹ʳ = ∑ i ∈ range n, (-↑x⁻¹ * t) ^ i + (-↑x⁻¹ * t) ^ n * (1 - -↑x⁻¹ * t)⁻¹ʳ
⊢ (↑x + t)⁻¹ʳ = (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * (↑x + t)⁻¹ʳ
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
n : ℕ
⊢ (fun i ↦ (-↑x⁻¹ * i) ^ n * (↑x + i)⁻¹ʳ) =O[𝓝 0] fun t ↦ ‖t‖ ^ n

Tactic:
refine ((isBigO_refl _ _).norm_right.mul (inverse_add_norm x)).trans ?_

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
n : ℕ
⊢ (fun x_1 ↦ ‖(-↑x⁻¹ * x_1) ^ n‖ * 1) =O[𝓝 0] fun t ↦ ‖t‖ ^ n
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
x : E
C : ℝ
hC_pos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
⊢ ∃ M, 0 < M ∧ ∀ (x_1 : F), ‖f (x, x_1)‖ ≤ M * ‖x_1‖

Tactic:
refine ⟨C * max ‖x‖ 1, by positivity, fun y ↦ (hC x y).trans ?_⟩

Goal state after:
𝕜 : 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
x : E
C : ℝ
hC_pos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
y : F
⊢ C * ‖x‖ * ‖y‖ ≤ C * max ‖x‖ 1 * ‖y‖
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsQuotientMap (rangeFactorization f)
⊢ Continuous[inst✝¹, inst✝] f

Tactic:
exact continuous_rangeFactorization_iff.mp hf.continuous

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

Goal state before:
pp: case pos
𝕜 : 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₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖
m : (i : ι) → E i
i : ι
hi : ‖m i‖ = 0
⊢ 0 ≤ C * ∏ i, ‖m i‖

Tactic:
prod_eq_zero (mem_univ i) hi,

Goal state after:
case pos
𝕜 : 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₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖
m : (i : ι) → E i
i : ι
hi : ‖m i‖ = 0
⊢ 0 ≤ C * 0
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
f g : α → ε'
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : Integrable f (μ.restrict s)
hg : Integrable g (μ.restrict sᶜ)
⊢ Integrable (s.piecewise f g) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf hg ⊢

Goal state after:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
f g : α → ε'
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : MemLp f 1 (μ.restrict s)
hg : MemLp g 1 (μ.restrict sᶜ)
⊢ MemLp (s.piecewise f g) 1 μ
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : IsOrderedAddMonoid β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ Integrable (f ⊓ g) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf hg ⊢

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : IsOrderedAddMonoid β
f g : α → β
hf : MemLp f 1 μ
hg : MemLp g 1 μ
⊢ MemLp (f ⊓ g) 1 μ
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : IsOrderedAddMonoid β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ Integrable (f ⊔ g) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf hg ⊢

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : IsOrderedAddMonoid β
f g : α → β
hf : MemLp f 1 μ
hg : MemLp g 1 μ
⊢ MemLp (f ⊔ g) 1 μ