mathlib-initiative/mathlib-tactics huggingface dataset:
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_tsum_1 : ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop
h_liminf_pow :
  ∫⁻ (a : α), liminf (fun n ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) atTop ^ p ∂μ =
    ∫⁻ (a : α), liminf (fun n ↦ (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p) atTop ∂μ
⊢ ∫⁻ (a : α), liminf (fun n ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) atTop ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p

Tactic:
h_liminf_pow

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_tsum_1 : ∀ (g : ℕ → ℝ≥0∞), ∑' (i : ℕ), g i = liminf (fun n ↦ ∑ i ∈ Finset.range (n + 1), g i) atTop
h_liminf_pow :
  ∫⁻ (a : α), liminf (fun n ↦ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) atTop ^ p ∂μ =
    ∫⁻ (a : α), liminf (fun n ↦ (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p) atTop ∂μ
⊢ ∫⁻ (a : α), liminf (fun n ↦ (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p) atTop ∂μ ≤ (∑' (i : ℕ), B i) ^ p
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜'
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝⁵ : RingHomIsometric σ
inst✝⁴ : Fact (1 ≤ p)
𝕜'' : Type u_8
inst✝³ : NormedRing 𝕜''
inst✝² : Module 𝕜'' F
inst✝¹ : IsBoundedSMul 𝕜'' F
inst✝ : SMulCommClass 𝕜' 𝕜'' F
c : 𝕜''
L : E →SL[σ] F
f : ↥(Lp E p μ)
⊢ (compLpL p μ (c • L)) f = (c • compLpL p μ L) f

Tactic:
exact smul_compLp c L f

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case pos.inl
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
H' : (∑ i ∈ s, f i ^ p) ^ (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)

pp: case pos.inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
H' : (∑ i ∈ s, g i ^ p) ^ (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:
<;>

Goal state after:
case pos.inl
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
H' : (∑ i ∈ s, f i ^ p) ^ (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)

case pos.inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
H' : (∑ i ∈ s, g i ^ p) ^ (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)
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
f g : ↥(Lp E p μ)
⊢ ↑↑f ≤ᵐ[μ] ↑↑g ↔ f ≤ g

Tactic:
← Subtype.coe_le_coe,

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup E
inst✝ : PartialOrder E
f g : ↥(Lp E p μ)
⊢ ↑↑f ≤ᵐ[μ] ↑↑g ↔ ↑f ≤ ↑g
Module: Mathlib.Data.Fintype.CardEmbedding

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : ‖α₁ ↪ β‖ = ‖β‖.descFactorial ‖α₁‖
⊢ ‖α₂ ↪ β‖ = ‖β‖.descFactorial ‖α₂‖

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
⊢ ‖PEmpty.{u_1 + 1} ↪ β‖ = ‖β‖.descFactorial ‖PEmpty.{u_1 + 1}‖

pp: case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = ‖β‖.descFactorial ‖γ‖
⊢ ‖Option γ ↪ β‖ = ‖β‖.descFactorial ‖Option γ‖

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : ‖α₁ ↪ β‖ = ‖β‖.descFactorial ‖α₁‖
⊢ ‖α₂ ↪ β‖ = ‖β‖.descFactorial ‖α₂‖

case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
⊢ ‖PEmpty.{u_1 + 1} ↪ β‖ = ‖β‖.descFactorial ‖PEmpty.{u_1 + 1}‖

case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
emb : Fintype (α ↪ β)
γ : Type u_1
h : Fintype γ
ih : ‖γ ↪ β‖ = ‖β‖.descFactorial ‖γ‖
⊢ ‖Option γ ↪ β‖ = ‖β‖.descFactorial ‖Option γ‖
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
val✝ : α
⊢ {
        toFun := fun x ↦
          match x with
          | Sum.inl a => (inl.trans f) a
          | Sum.inr b => (inr.trans f) b,
        inj' := ⋯ }
      (Sum.inl val✝) =
    f (Sum.inl val✝)

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
val✝ : β
⊢ {
        toFun := fun x ↦
          match x with
          | Sum.inl a => (inl.trans f) a
          | Sum.inr b => (inr.trans f) b,
        inj' := ⋯ }
      (Sum.inr val✝) =
    f (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
val✝ : α
⊢ {
        toFun := fun x ↦
          match x with
          | Sum.inl a => (inl.trans f) a
          | Sum.inr b => (inr.trans f) b,
        inj' := ⋯ }
      (Sum.inl val✝) =
    f (Sum.inl val✝)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
val✝ : β
⊢ {
        toFun := fun x ↦
          match x with
          | Sum.inl a => (inl.trans f) a
          | Sum.inr b => (inr.trans f) b,
        inj' := ⋯ }
      (Sum.inr val✝) =
    f (Sum.inr val✝)
Module: Mathlib.Topology.Algebra.Module.Multilinear.Basic

Goal state before:
pp: R : Type u
ι : Type v
M₁ : ι → Type w₁
M₂ : Type w₂
M₃ : Type w₃
inst✝⁹ : Semiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : (i : ι) → TopologicalSpace (M₁ i)
inst✝¹ : TopologicalSpace M₂
inst✝ : TopologicalSpace M₃
f g : ContinuousMultilinearMap R M₁ (M₂ × M₃)
⊢ f = g ↔
    (ContinuousLinearMap.fst R M₂ M₃).compContinuousMultilinearMap f =
        (ContinuousLinearMap.fst R M₂ M₃).compContinuousMultilinearMap g ∧
      (ContinuousLinearMap.snd R M₂ M₃).compContinuousMultilinearMap f =
        (ContinuousLinearMap.snd R M₂ M₃).compContinuousMultilinearMap g

Tactic:
rw [← Prod.mk_inj, ← prodEquiv_symm_apply, ← prodEquiv_symm_apply, Equiv.apply_eq_iff_eq]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded

Goal state before:
pp: case inl
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : ContinuousSMul 𝕜 F
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
h : IsEmpty ι
⊢ IsVonNBounded 𝕜 (⇑f '' s)

Tactic:
exact (isBounded_iff_isVonNBounded _).1 <|
      @Set.Finite.isBounded _ (vonNBornology 𝕜 F) _ (s.toFinite.image _)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
h_is_o : (fun t ↦ (↑x + t)⁻¹ʳ - ↑x⁻¹) =o[𝓝 0] fun x ↦ 1
h_lim : Tendsto (fun y ↦ y - ↑x) (𝓝 ↑x) (𝓝 0)
⊢ ContinuousAt inverse ↑x

Tactic:
ContinuousAt,

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
h_is_o : (fun t ↦ (↑x + t)⁻¹ʳ - ↑x⁻¹) =o[𝓝 0] fun x ↦ 1
h_lim : Tendsto (fun y ↦ y - ↑x) (𝓝 ↑x) (𝓝 0)
⊢ Tendsto inverse (𝓝 ↑x) (𝓝 (↑x)⁻¹ʳ)
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ε : ∀ (x : E), ‖f x‖ < ε → ‖x‖ < 1
⊢ ∃ K, AntilipschitzWith K ⇑f

Tactic:
lift ε to ℝ≥0 using ε0.le

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 : 0 < ↑ε
hε : ∀ (x : E), ‖f x‖ < ↑ε → ‖x‖ < 1
⊢ ∃ K, AntilipschitzWith K ⇑f
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : Module 𝕜 F
⊢ IsBoundedLinearMap 𝕜 fun x ↦ x.1

Tactic:
refine (LinearMap.fst 𝕜 E F).isLinear.with_bound 1 fun x => ?_

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : Module 𝕜 F
x : E × F
⊢ ‖(LinearMap.fst 𝕜 E F) x‖ ≤ 1 * ‖x‖
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: case fst
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x✝ : ↥p
⊢ ↑((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf) ↑x✝).1 = ↑(x✝, 0).1

pp: case snd
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x✝ : ↥p
⊢ ↑((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf) ↑x✝).2 = ↑(x✝, 0).2

Tactic:
<;>

Goal state after:
case fst
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x✝ : ↥p
⊢ ↑((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf) ↑x✝).1 = ↑(x✝, 0).1

case snd
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x✝ : ↥p
⊢ ↑((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf) ↑x✝).2 = ↑(x✝, 0).2
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: case fst
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x✝ : ↥(↑f).ker
⊢ ↑((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf) ↑x✝).1 = ↑(0, x✝).1

pp: case snd
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x✝ : ↥(↑f).ker
⊢ ↑((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf) ↑x✝).2 = ↑(0, x✝).2

Tactic:
<;>

Goal state after:
case fst
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x✝ : ↥(↑f).ker
⊢ ↑((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf) ↑x✝).1 = ↑(0, x✝).1

case snd
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x✝ : ↥(↑f).ker
⊢ ↑((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf) ↑x✝).2 = ↑(0, x✝).2
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
  · simp [Measure.real, hs]
  · exact measureReal_mono subset_union_left (measure_union_lt_top hs h.lt_top).ne

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
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ η, 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun x ↦ c) p μ ≤ ε

Tactic:
rcases eq_or_ne p 0 with (rfl | h'p)
  · exact ⟨1, zero_lt_one, fun s _ => by simp⟩
  have hp₀ : 0 < p := bot_lt_iff_ne_bot.2 h'p
  have hp₀' : 0 ≤ 1 / p.toReal := div_nonneg zero_le_one ENNReal.toReal_nonneg
  have hp₀'' : 0 < p.toReal := ENNReal.toReal_pos hp₀.ne' hp
  obtain ⟨η, hη_pos, hη_le⟩ : ∃ η : ℝ≥0, 0 < η ∧ ‖c‖ₑ * (η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε := by
    have :
      Filter.Tendsto (fun x : ℝ≥0 => ((‖c‖₊ * x ^ (1 / p.toReal) : ℝ≥0) : ℝ≥0∞)) (𝓝 0)
        (𝓝 (0 : ℝ≥0)) := by
      rw [ENNReal.tendsto_coe]
      convert! (NNReal.continuousAt_rpow_const (Or.inr hp₀')).tendsto.const_mul _
      simp [hp₀''.ne']
    have hε' : 0 < ε := hε.bot_lt
    obtain ⟨δ, hδ, hδε'⟩ := NNReal.nhds_zero_basis.eventually_iff.mp (this.eventually_le_const hε')
    obtain ⟨η, hη, hηδ⟩ := exists_between hδ
    refine ⟨η, hη, ?_⟩
    simpa only [← ENNReal.coe_rpow_of_nonneg _ hp₀', enorm, ← ENNReal.coe_mul] using hδε' hηδ
  refine ⟨η, hη_pos, fun s hs => ?_⟩
  grw [eLpNorm_indicator_const_le, ← hη_le, hs]

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
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ (‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)).toReal = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

pp: case h0
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ p ≠ 0

pp: case hμ
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ μ ≠ 0

Tactic:
<;>

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ (‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)).toReal = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

case h0
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ p ≠ 0

case hμ
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : IsFiniteMeasure μ
c : E
inst✝ : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ μ ≠ 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
inst✝ : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
⊢ (‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)).toReal = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

pp: case h0
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
⊢ p ≠ 0

pp: case h_top
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
⊢ p ≠ ∞

Tactic:
<;>

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
⊢ (‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)).toReal = ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

case h0
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
⊢ p ≠ 0

case h_top
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
⊢ p ≠ ∞
Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator

Goal state before:
pp: case pos
α : 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
hy_mem : y ∈ s
⊢ s.indicator (fun x_1 ↦ x) y = s.indicator (fun x ↦ 1) y • x

pp: case neg
α : 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
hy_mem : y ∉ s
⊢ s.indicator (fun x_1 ↦ x) y = s.indicator (fun x ↦ 1) y • x

Tactic:
<;>

Goal state after:
case pos
α : 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
hy_mem : y ∈ s
⊢ s.indicator (fun x_1 ↦ x) y = s.indicator (fun x ↦ 1) y • x

case neg
α : 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
hy_mem : y ∉ s
⊢ s.indicator (fun x_1 ↦ x) y = s.indicator (fun x ↦ 1) y • x
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : PseudoMetrizableSpace ε
f : α → ε
hμ : MemLp f 1 μ
hν : MemLp f 1 ν
⊢ eLpNorm f 1 (μ + ν) < ∞

Tactic:
eLpNorm_one_add_measure,

Goal state after:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : PseudoMetrizableSpace ε
f : α → ε
hμ : MemLp f 1 μ
hν : MemLp f 1 ν
⊢ eLpNorm f 1 μ + eLpNorm f 1 ν < ∞
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: case left
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
⊢ AEStronglyMeasurable f 0

pp: case right
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
⊢ HasFiniteIntegral f 0

Tactic:
<;>

Goal state after:
case left
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
⊢ AEStronglyMeasurable f 0

case right
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
⊢ HasFiniteIntegral f 0
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: case empty
α : Type u_1
ε : Type u_5
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : PseudoMetrizableSpace ε
ι : Type u_8
m : MeasurableSpace α
f : α → ε
μ : ι → Measure α
⊢ Integrable f (∑ i ∈ ∅, μ i) ↔ ∀ i ∈ ∅, Integrable f (μ i)

pp: case insert
α : Type u_1
ε : Type u_5
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : PseudoMetrizableSpace ε
ι : Type u_8
m : MeasurableSpace α
f : α → ε
μ : ι → Measure α
a✝² : ι
s✝ : Finset ι
a✝¹ : a✝² ∉ s✝
a✝ : Integrable f (∑ i ∈ s✝, μ i) ↔ ∀ i ∈ s✝, Integrable f (μ i)
⊢ Integrable f (∑ i ∈ insert a✝² s✝, μ i) ↔ ∀ i ∈ insert a✝² s✝, Integrable f (μ i)

Tactic:
<;>

Goal state after:
case empty
α : Type u_1
ε : Type u_5
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : PseudoMetrizableSpace ε
ι : Type u_8
m : MeasurableSpace α
f : α → ε
μ : ι → Measure α
⊢ Integrable f (∑ i ∈ ∅, μ i) ↔ ∀ i ∈ ∅, Integrable f (μ i)

case insert
α : Type u_1
ε : Type u_5
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : PseudoMetrizableSpace ε
ι : Type u_8
m : MeasurableSpace α
f : α → ε
μ : ι → Measure α
a✝² : ι
s✝ : Finset ι
a✝¹ : a✝² ∉ s✝
a✝ : Integrable f (∑ i ∈ s✝, μ i) ↔ ∀ i ∈ s✝, Integrable f (μ i)
⊢ Integrable f (∑ i ∈ insert a✝² s✝, μ i) ↔ ∀ i ∈ insert a✝² s✝, Integrable f (μ i)
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
f : α → ε'
x : α
inst✝ : MeasurableSingletonClass α
hfx : ‖f x‖ₑ ≠ ∞
⊢ IntegrableOn f {x} μ ↔ ‖f x‖ₑ = 0 ∨ μ {x} < ∞

Tactic:
have : f =ᵐ[μ.restrict {x}] fun _ => f x := by
    filter_upwards [ae_restrict_mem (measurableSet_singleton x)] with _ ha
    simp only [mem_singleton_iff.1 ha]

Goal state after:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
f : α → ε'
x : α
inst✝ : MeasurableSingletonClass α
hfx : ‖f x‖ₑ ≠ ∞
this : f =ᵐ[μ.restrict {x}] fun x_1 ↦ f x
⊢ IntegrableOn f {x} μ ↔ ‖f x‖ₑ = 0 ∨ μ {x} < ∞
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: case left
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : Integrable f μ
⊢ AEStronglyMeasurable (fun x ↦ ‖f x‖ₑ) μ

pp: case right
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : Integrable f μ
⊢ HasFiniteIntegral (fun x ↦ ‖f x‖ₑ) μ

Tactic:
<;>

Goal state after:
case left
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : Integrable f μ
⊢ AEStronglyMeasurable (fun x ↦ ‖f x‖ₑ) μ

case right
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : Integrable f μ
⊢ HasFiniteIntegral (fun x ↦ ‖f x‖ₑ) μ