mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝ : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm
⊢ (map (⇑(MeasurableEquiv.piOptionEquivProd β).symm) ((Measure.pi fun i ↦ μ (some i)).prod (μ none))) (univ.pi s) =
    ∏ i, (μ i) (s i)

Tactic:
have me := MeasurableEquiv.measurableEmbedding e_meas

Goal state after:
ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝ : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm
me : MeasurableEmbedding ⇑e_meas
⊢ (map (⇑(MeasurableEquiv.piOptionEquivProd β).symm) ((Measure.pi fun i ↦ μ (some i)).prod (μ none))) (univ.pi s) =
    ∏ i, (μ i) (s i)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
c : ε
s : Set α
p : ℝ≥0∞
hp : p ≠ 0
h'p : p ≠ ∞
t : Set α := toMeasurable μ s
⊢ ‖c‖ₑ * μ t ^ (1 / p.toReal) = ‖c‖ₑ * μ s ^ (1 / p.toReal)

Tactic:
measure_toMeasurable

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
c : ε
s : Set α
p : ℝ≥0∞
hp : p ≠ 0
h'p : p ≠ ∞
t : Set α := toMeasurable μ s
⊢ ‖c‖ₑ * μ s ^ (1 / p.toReal) = ‖c‖ₑ * μ s ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
x : α
hx : x ∉ s
⊢ ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun x ↦ c) x‖

Tactic:
simp [Set.indicator_of_notMem hx]

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

Goal state before:
pp: case neg
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
h0 : ¬p = 0
h_top : ¬p = ∞
⊢ eLpNorm (-f) p μ = eLpNorm f p μ

Tactic:
simp [eLpNorm_eq_eLpNorm' h0 h_top]

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

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε' : Type u_7
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
c : ε'
hc : ‖c‖ₑ ≠ ∞
h : μ = 0
⊢ eLpNorm (fun x ↦ c) ∞ μ < ∞

Tactic:
simp [eLpNorm_const _, h, hc.lt_top]

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

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε' : Type u_7
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
c : ε'
hc : ‖c‖ₑ ≠ ∞
h : ¬μ = 0
⊢ eLpNorm (fun x ↦ c) ∞ μ < ∞

Tactic:
simp [eLpNorm_const _, h, hc.lt_top]

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

Goal state before:
pp: x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
⊢ (rexp y - rexp x) / (y - x) < rexp y

Tactic:
have h2 : x - y < 0 := by linarith

Goal state after:
x y z : ℝ
hxy : x < y
hyz : y < z
h1 : 0 < y - x
h2 : x - y < 0
⊢ (rexp y - rexp x) / (y - x) < rexp y
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ p ≠ ∞ ↔ 1 < q

Tactic:
ne_top_iff_ne_one _ q,

Goal state after:
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ q ≠ 1 ↔ 1 < q
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : p = ∞
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ

pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ

Tactic:
· simp only [hp_top, eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm]
    exact ENNReal.essSup_restrict_eq_of_support_subset fun x hx ↦ hsf <| enorm_ne_zero.1 hx

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
p : ℝ
hp : 0 ≤ p
f : α → ε
c : ℝ≥0∞
⊢ eLpNorm' f p (c • μ) = c ^ (1 / p) * eLpNorm' f p μ

Tactic:
simp [eLpNorm', ENNReal.mul_rpow_of_nonneg, hp]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : AEStronglyMeasurable f μ
h : MemLp (fun x ↦ ‖f x‖ₑ) p μ
⊢ eLpNorm f p μ < ∞

Tactic:
rw [← eLpNorm_enorm]; exact h.2

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

Goal state before:
pp: p : ℝ≥0∞
hp✝ : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ (p - 1 + 1) / (p - 1) = (1⁻¹ - p⁻¹)⁻¹

Tactic:
rw [tsub_add_cancel_of_le, ← inv_eq_iff_eq_inv, div_eq_mul_inv, ENNReal.mul_inv, inv_inv,
        ENNReal.mul_sub, ENNReal.inv_mul_cancel, mul_one]

Goal state after:
p : ℝ≥0∞
hp✝ : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ 1 - p⁻¹ = 1⁻¹ - p⁻¹

case h0
p : ℝ≥0∞
hp✝ : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ p ≠ 0

case ht
p : ℝ≥0∞
hp✝ : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ p ≠ ∞

p : ℝ≥0∞
hp✝ : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ 0 < 1 → 1 < p → p⁻¹ ≠ ∞

case ha
p : ℝ≥0∞
hp✝ : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ p ≠ 0 ∨ (p - 1)⁻¹ ≠ ∞

case hb
p : ℝ≥0∞
hp✝ : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ p ≠ ∞ ∨ (p - 1)⁻¹ ≠ 0

p : ℝ≥0∞
hp✝ : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ 1 ≤ p
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 < p
f : α → ℝ≥0∞
a : α
⊢ (f a * ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹) ^ p = f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹

Tactic:
mul_rpow_of_nonneg _ _ (le_of_lt hp0)

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 < p
f : α → ℝ≥0∞
a : α
⊢ f a ^ p * ((∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p))⁻¹ ^ p = f a ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p * (1 / q)) ≤ a ^ p + b ^ p

Tactic:
mul_one_div

Goal state after:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
⊢ ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, w j ≠ 0 → z j = ∑ i ∈ s, w i * z i

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

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : CommRing 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
n : ℕ
⊢ ConvexOn 𝕜 univ fun x ↦ x ^ (2 * n)

Tactic:
pow_mul

Goal state after:
𝕜 : Type u_1
inst✝² : CommRing 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
n : ℕ
⊢ ConvexOn 𝕜 univ fun x ↦ (x ^ 2) ^ n
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p * (1 / q)) ≤ a ^ p + b ^ p

Tactic:
mul_one_div

Goal state after:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: z₁ z₂ p : ℝ≥0∞
p_zero : ¬p = 0
⊢ p = (ENNReal.ofReal p⁻¹.toReal)⁻¹

Tactic:
ENNReal.ofReal_toReal (by simpa),

Goal state after:
z₁ z₂ p : ℝ≥0∞
p_zero : ¬p = 0
⊢ p = p⁻¹⁻¹
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : ∑ i ∈ s, f i ^ p ≤ 1
hg : ∑ i ∈ s, g i ^ q ≤ 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ 1 / p.toNNReal + 1 / q.toNNReal = 1

Tactic:
by simp_rw [one_div, hpq.toNNReal.inv_add_inv_eq_one]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

Tactic:
have h0_rpow : (∫⁻ a, (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0 := by
    simp [h_add_zero, h_add_top, -Pi.add_apply]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: 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
hp1_lt : 1 < p
hpq : p.HolderConjugate p.conjExponent
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

Tactic:
by_cases h0 : (∫⁻ a, (f + g) a ^ p ∂μ) = 0

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
hp1_lt : 1 < p
hpq : p.HolderConjugate p.conjExponent
h0 : ∫⁻ (a : α), (f + g) a ^ p ∂μ = 0
⊢ (∫⁻ (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
hp1_lt : 1 < p
hpq : p.HolderConjugate p.conjExponent
h0 : ¬∫⁻ (a : α), (f + g) a ^ p ∂μ = 0
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
inst✝ : NormedAddCommGroup E
f : ↥(Lp E p 0)
⊢ (eLpNorm (↑↑f) p 0).toReal = 0

Tactic:
eLpNorm_measure_zero,

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
inst✝ : NormedAddCommGroup E
f : ↥(Lp E p 0)
⊢ ENNReal.toReal 0 = 0
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k ↦ {x | 2⁻¹ ^ k ≤ edist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : μ s = 0
⊢ ∀ x ∈ sᶜ, Tendsto (fun i ↦ f (ns i) x) atTop (𝓝 (g x))

Tactic:
refine fun x hx => EMetric.tendsto_atTop.mpr fun ε hε => ?_

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k ↦ {x | 2⁻¹ ^ k ≤ edist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : μ s = 0
x : α
hx : x ∈ sᶜ
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, edist (f (ns n) x) (g x) < ε
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
g✝ : E → F
c✝ : ℝ≥0
inst✝ : NormedSpace ℝ E
ν : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ≤ c • ν
f g : ↥(Lp E p ν)
⊢ ↑↑(f + g) =ᵐ[μ] ↑↑f + ↑↑g

Tactic:
have : μ ≪ ν := Measure.absolutelyContinuous_of_le_smul h

Goal state after:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
g✝ : E → F
c✝ : ℝ≥0
inst✝ : NormedSpace ℝ E
ν : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ≤ c • ν
f g : ↥(Lp E p ν)
this : μ ≪ ν
⊢ ↑↑(f + g) =ᵐ[μ] ↑↑f + ↑↑g
Module: Mathlib.MeasureTheory.Function.LpOrder

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝⁴ : NormedAddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Fact (1 ≤ p)
inst✝ : ClosedIciTopology E
f : ℕ → ↥(Lp E p μ)
f₀ : ↥(Lp E p μ)
h_tendsto : Filter.Tendsto f Filter.atTop (nhds f₀)
hf : ∀ (n : ℕ), 0 ≤ᵐ[μ] ↑↑(f n)
φ : ℕ → ℕ
hφ : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun i ↦ ↑↑(f (φ i)) x) Filter.atTop (nhds (↑↑f₀ x))
x : α
hx : x ∈ ⋂ i, {x | 0 x ≤ ↑↑(f i) x}
⊢ Filter.Tendsto (fun i ↦ ↑↑(f (φ i)) x) Filter.atTop (nhds (↑↑f₀ x)) → 0 x ≤ ↑↑f₀ x

Tactic:
hφx

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝⁴ : NormedAddCommGroup E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Fact (1 ≤ p)
inst✝ : ClosedIciTopology E
f : ℕ → ↥(Lp E p μ)
f₀ : ↥(Lp E p μ)
h_tendsto : Filter.Tendsto f Filter.atTop (nhds f₀)
hf : ∀ (n : ℕ), 0 ≤ᵐ[μ] ↑↑(f n)
φ : ℕ → ℕ
hφ : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun i ↦ ↑↑(f (φ i)) x) Filter.atTop (nhds (↑↑f₀ x))
x : α
hx : x ∈ ⋂ i, {x | 0 x ≤ ↑↑(f i) x}
hφx : Filter.Tendsto (fun i ↦ ↑↑(f (φ i)) x) Filter.atTop (nhds (↑↑f₀ x))
⊢ 0 x ≤ ↑↑f₀ x
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
g : E → F
c✝¹ : ℝ≥0
inst✝ : NormedSpace ℝ E
ν : Measure α
c✝ : ℝ≥0∞
hc : c✝ ≠ ∞
h : μ ≤ c✝ • ν
c : ℝ
f : ↥(Lp E p ν)
⊢ ↑↑(c • f) =ᵐ[μ] (RingHom.id ℝ) c • ↑↑f

Tactic:
have : μ ≪ ν := Measure.absolutelyContinuous_of_le_smul h

Goal state after:
α : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
g : E → F
c✝¹ : ℝ≥0
inst✝ : NormedSpace ℝ E
ν : Measure α
c✝ : ℝ≥0∞
hc : c✝ ≠ ∞
h : μ ≤ c✝ • ν
c : ℝ
f : ↥(Lp E p ν)
this : μ ≪ ν
⊢ ↑↑(c • f) =ᵐ[μ] (RingHom.id ℝ) c • ↑↑f
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
a : α
h : ↑↑(negPart f) a = max (-↑↑f a) 0
⊢ max (-↑↑f a) 0 = max (-↑↑f a) (-0)

Tactic:
neg_zero

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
a : α
h : ↑↑(negPart f) a = max (-↑↑f a) 0
⊢ max (-↑↑f a) 0 = max (-↑↑f a) 0
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
a₁ : α
b₂ : β
f_eq : f a₁ = g b₂
⊢ Sum.inl a₁ = Sum.inr b₂

pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
b₁ : β
a₂ : α
f_eq : g b₁ = f a₂
⊢ Sum.inr b₁ = Sum.inl a₂

pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
b₁ b₂ : β
f_eq : g b₁ = g b₂
⊢ Sum.inr b₁ = Sum.inr b₂

Tactic:
· exfalso
        exact disj.le_bot ⟨⟨a₁, f_eq⟩, ⟨b₂, by simp⟩⟩

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
b₁ : β
a₂ : α
f_eq : g b₁ = f a₂
⊢ Sum.inr b₁ = Sum.inl a₂

case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
b₁ b₂ : β
f_eq : g b₁ = g b₂
⊢ Sum.inr b₁ = Sum.inr b₂
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
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
h_sub : eLpNorm (f n - f_lim) p μ ≤ liminf (fun m_1 ↦ eLpNorm (f n - f m_1) p μ) atTop
⊢ ∀ (a : ℕ), ∃ b, a ≤ b ∧ eLpNorm (f n - f b) p μ ≤ ε

Tactic:
refine fun N1 => ⟨max N N1, le_max_right _ _, ?_⟩

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ∞
h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
h_sub : eLpNorm (f n - f_lim) p μ ≤ liminf (fun m_1 ↦ eLpNorm (f n - f m_1) p μ) atTop
N1 : ℕ
⊢ eLpNorm (f n - f (max N N1)) p μ ≤ ε
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
⊢ (fun t ↦ (1 - t)⁻¹ʳ) =O[𝓝 0] fun _t ↦ 1

Tactic:
simp only [IsBigO, IsBigOWith, Metric.eventually_nhds_iff]
  refine ⟨‖(1 : R)‖ + 1, (2 : ℝ)⁻¹, by simp, fun t ht ↦ ?_⟩
  rw [dist_zero_right] at ht
  have ht' : ‖t‖ < 1 := by linarith
  simp only [inverse_one_sub t ht', norm_one, mul_one]
  change ‖∑' n : ℕ, t ^ n‖ ≤ _
  have := tsum_geometric_le_of_norm_lt_one t ht'
  have : (1 - ‖t‖)⁻¹ ≤ 2 := inv_le_of_inv_le₀ (by simp) (by linarith)
  linarith

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (⇑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ
ε0 : 0 < ε
hε : ⇑f ⁻¹' ball 0 ε ⊆ ball 0 1
⊢ ∃ K, AntilipschitzWith K ⇑f

Tactic:
simp only [Set.subset_def, Set.mem_preimage, mem_ball_zero_iff] at hε

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (⇑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ
ε0 : 0 < ε
hε : ∀ (x : E), ‖f x‖ < ε → ‖x‖ < 1
⊢ ∃ K, AntilipschitzWith K ⇑f
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (⇑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖σ₁₂ c‖
x : E
hx : ¬f x = 0
hc₀ : c ≠ 0
n : ℤ
hlt : ‖f (c ^ n • x)‖ < ↑ε
hle : ‖c ^ n‖⁻¹ ≤ (↑ε)⁻¹ * ‖c‖ * ‖f x‖
⊢ ‖c ^ n‖⁻¹ * ‖c ^ n • x‖ ≤ ‖c ^ n‖⁻¹ * 1

Tactic:
by gcongr; exact (hε _ hlt).le

Goal state after: