mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ContinuousMap.Compact

Goal state before:
pp: case a
α : Type u_1
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : SeminormedAddCommGroup E
f : C(α, E)
inst✝ : Fintype α
⊢ ∀ (i : α), ‖f i‖ ≤ ‖f‖

Tactic:
]

Goal state after:
case a
α : Type u_1
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : SeminormedAddCommGroup E
f : C(α, E)
inst✝ : Fintype α
⊢ ∀ (i : α), ‖f i‖ ≤ ‖f‖
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᵐ[μ] f
hg_nonneg : 0 ≤ᵐ[μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫ (a : α), f a * g a ∂μ = ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ
h_right_f : ∫ (a : α), f a ^ p ∂μ = ∫ (a : α), ‖f a‖ ^ p ∂μ
h_right_g : ∫ (a : α), g a ^ q ∂μ = ∫ (a : α), ‖g a‖ ^ q ∂μ
⊢ ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ ≤ (∫ (a : α), ‖f a‖ ^ p ∂μ) ^ (1 / p) * (∫ (a : α), ‖g a‖ ^ q ∂μ) ^ (1 / q)

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᵐ[μ] f
hg_nonneg : 0 ≤ᵐ[μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫ (a : α), f a * g a ∂μ = ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ
h_right_f : ∫ (a : α), f a ^ p ∂μ = ∫ (a : α), ‖f a‖ ^ p ∂μ
h_right_g : ∫ (a : α), g a ^ q ∂μ = ∫ (a : α), ‖g a‖ ^ q ∂μ
⊢ ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ ≤ (∫ (a : α), ‖f a‖ ^ p ∂μ) ^ (1 / p) * (∫ (a : α), ‖g a‖ ^ q ∂μ) ^ (1 / q)
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
⊢ μ' ≤ 0

Tactic:
]

Goal state after:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
⊢ μ' ≤ 0
Module: Mathlib.Topology.ContinuousMap.Compact

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : SeminormedAddCommGroup β
inst✝² : StarAddMonoid β
inst✝¹ : NormedStarGroup β
inst✝ : CompactSpace α
f : C(α, β)
⊢ ‖f‖ ≤ ‖f‖

Tactic:
]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Compact

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompactSpace α
inst✝² : NonUnitalNormedRing β
inst✝¹ : StarRing β
inst✝ : CStarRing β
f : C(α, β)
⊢ ∀ (x : α), ‖f x‖ ≤ √‖star f * f‖

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompactSpace α
inst✝² : NonUnitalNormedRing β
inst✝¹ : StarRing β
inst✝ : CStarRing β
f : C(α, β)
⊢ ∀ (x : α), ‖f x‖ ≤ √‖star f * f‖
Module: Mathlib.Topology.ContinuousMap.Compact

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompactSpace α
inst✝² : NonUnitalNormedRing β
inst✝¹ : StarRing β
inst✝ : CStarRing β
f : C(α, β)
x : α
⊢ ‖star (f x) * f x‖ ≤ ‖star f * f‖

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompactSpace α
inst✝² : NonUnitalNormedRing β
inst✝¹ : StarRing β
inst✝ : CStarRing β
f : C(α, β)
x : α
⊢ ‖star (f x) * f x‖ ≤ ‖star f * f‖
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
inst✝ : Unique α
f : α → E
⊢ μ.real univ • f default = μ.real univ • f default

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable (⇑f) μ
⊢ ∑ x ∈ (SimpleFunc.toLargerSpace hm f).range, μ.real (⇑(SimpleFunc.toLargerSpace hm f) ⁻¹' {x}) • x =
    ∑ x ∈ f.range, μ.real (⇑(SimpleFunc.toLargerSpace hm f) ⁻¹' {x}) • x

Tactic:
]

Goal state after:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable (⇑f) μ
⊢ ∑ x ∈ (SimpleFunc.toLargerSpace hm f).range, μ.real (⇑(SimpleFunc.toLargerSpace hm f) ⁻¹' {x}) • x =
    ∑ x ∈ f.range, μ.real (⇑(SimpleFunc.toLargerSpace hm f) ⁻¹' {x}) • x
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable (⇑f) μ
hf : StronglyMeasurable ⇑f
hf_int_m : Integrable (⇑f) (μ.trim hm)
⊢ ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) • x = ∑ x ∈ f.range, (μ.trim hm).real (⇑f ⁻¹' {x}) • x

Tactic:
]

Goal state after:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable (⇑f) μ
hf : StronglyMeasurable ⇑f
hf_int_m : Integrable (⇑f) (μ.trim hm)
⊢ ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) • x = ∑ x ∈ f.range, (μ.trim hm).real (⇑f ⁻¹' {x}) • x
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
h_im_zero : (fun f ↦ Integrable.toL1 ↑↑f ⋯) = 0
⊢ Continuous 0

Tactic:
]

Goal state after:
case pos
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
hμ'0 : μ' = 0
h_im_zero : (fun f ↦ Integrable.toL1 ↑↑f ⋯) = 0
⊢ Continuous 0
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case neg
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hf_int : ¬Integrable f μ
hf_int_m : ¬Integrable f (μ.trim hm)
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : α → ℝ≥0 × ℝ≥0∞ := fun x ↦ (1, infEDist x E / ENNReal.ofReal δ)
sub : ℝ≥0 × ℝ≥0∞ → ℝ≥0∞ := fun p ↦ ↑p.1 - p.2
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] (sub ∘ f)

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : α → ℝ≥0 × ℝ≥0∞ := fun x ↦ (1, infEDist x E / ENNReal.ofReal δ)
sub : ℝ≥0 × ℝ≥0∞ → ℝ≥0∞ := fun p ↦ ↑p.1 - p.2
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] (sub ∘ f)
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_mem : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case neg
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
⊢ ∀ (b : ↥(Lp G 1 μ)),
    ∀ ε > 0, ∃ δ > 0, ∀ (a : ↥(Lp G 1 μ)), dist a b < δ → dist (Integrable.toL1 ↑↑a ⋯) (Integrable.toL1 ↑↑b ⋯) < ε

Tactic:
]

Goal state after:
case neg
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
⊢ ∀ (b : ↥(Lp G 1 μ)),
    ∀ ε > 0, ∃ δ > 0, ∀ (a : ↥(Lp G 1 μ)), dist a b < δ → dist (Integrable.toL1 ↑↑a ⋯) (Integrable.toL1 ↑↑b ⋯) < ε
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEDist x E
⊢ thickenedIndicatorAux δ E x = 0

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEDist x E
⊢ thickenedIndicatorAux δ E x = 0
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEDist x E
key : 1 - infEDist x E / ENNReal.ofReal δ ≤ 1 - 1
⊢ 1 - infEDist x E / ENNReal.ofReal δ ≤ ⊥

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEDist x E
key : 1 - infEDist x E / ENNReal.ofReal δ ≤ 1 - 1
⊢ 1 - infEDist x E / ENNReal.ofReal δ ≤ ⊥
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: case inl
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
hle : infEDist x E / ENNReal.ofReal δ ≤ 1
⊢ infEDist x E / ENNReal.ofReal δ ≤ infEDist y E / ENNReal.ofReal δ

Tactic:
]

Goal state after:
case inl
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
hle : infEDist x E / ENNReal.ofReal δ ≤ 1
⊢ infEDist x E / ENNReal.ofReal δ ≤ infEDist y E / ENNReal.ofReal δ
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: case inr
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
hle : 1 ≤ infEDist x E / ENNReal.ofReal δ
⊢ 0 ≤ 0

pp: case inr
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
hle : 1 ≤ infEDist x E / ENNReal.ofReal δ
⊢ 1 ≤ infEDist y E / ENNReal.ofReal δ

Tactic:
]

Goal state after:
case inr
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
hle : 1 ≤ infEDist x E / ENNReal.ofReal δ
⊢ 1 ≤ infEDist y E / ENNReal.ofReal δ
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case h
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm (↑↑g - ↑↑f) 1 μ).toReal < ε / 2 / c'.toReal
⊢ (eLpNorm (↑↑(Integrable.toL1 ↑↑g ⋯) - ↑↑(Integrable.toL1 ↑↑f ⋯)) 1 μ').toReal < ε

Tactic:
]

Goal state after:
case h
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm (↑↑g - ↑↑f) 1 μ).toReal < ε / 2 / c'.toReal
⊢ (eLpNorm (↑↑(Integrable.toL1 ↑↑g ⋯) - ↑↑(Integrable.toL1 ↑↑f ⋯)) 1 μ').toReal < ε
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
⊢ ∀ (x : α),
    Tendsto (fun i ↦ thickenedIndicatorAux (δseq i) E x) atTop
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun x ↦ 1) x))

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
⊢ ∀ (x : α),
    Tendsto (fun i ↦ thickenedIndicatorAux (δseq i) E x) atTop
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun x ↦ 1) x))
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case h
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm (↑↑g - ↑↑f) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑↑f') μ' :=
  fun f' ↦ Integrable.of_measure_le_smul hc' hμ'_le (L1.integrable_coeFn f')
this : eLpNorm (↑↑(Integrable.toL1 ↑↑g ⋯) - ↑↑(Integrable.toL1 ↑↑f ⋯)) 1 μ' = eLpNorm (↑↑g - ↑↑f) 1 μ'
⊢ (eLpNorm (↑↑g - ↑↑f) 1 μ').toReal < ε

Tactic:
]

Goal state after:
case h
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm (↑↑g - ↑↑f) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑↑f') μ' :=
  fun f' ↦ Integrable.of_measure_le_smul hc' hμ'_le (L1.integrable_coeFn f')
this : eLpNorm (↑↑(Integrable.toL1 ↑↑g ⋯) - ↑↑(Integrable.toL1 ↑↑f ⋯)) 1 μ' = eLpNorm (↑↑g - ↑↑f) 1 μ'
⊢ (eLpNorm (↑↑g - ↑↑f) 1 μ').toReal < ε
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm (↑↑g - ↑↑f) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑↑f') μ' :=
  fun f' ↦ Integrable.of_measure_le_smul hc' hμ'_le (L1.integrable_coeFn f')
this : eLpNorm (↑↑(Integrable.toL1 ↑↑g ⋯) - ↑↑(Integrable.toL1 ↑↑f ⋯)) 1 μ' = eLpNorm (↑↑g - ↑↑f) 1 μ'
⊢ eLpNorm (↑↑(g - f)) 1 μ ≠ ∞

Tactic:
]

Goal state after:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm (↑↑g - ↑↑f) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑↑f') μ' :=
  fun f' ↦ Integrable.of_measure_le_smul hc' hμ'_le (L1.integrable_coeFn f')
this : eLpNorm (↑↑(Integrable.toL1 ↑↑g ⋯) - ↑↑(Integrable.toL1 ↑↑f ⋯)) 1 μ' = eLpNorm (↑↑g - ↑↑f) 1 μ'
⊢ eLpNorm (↑↑(g - f)) 1 μ ≠ ∞
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm (↑↑g - ↑↑f) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑↑f') μ' :=
  fun f' ↦ Integrable.of_measure_le_smul hc' hμ'_le (L1.integrable_coeFn f')
this : eLpNorm (↑↑(Integrable.toL1 ↑↑g ⋯) - ↑↑(Integrable.toL1 ↑↑f ⋯)) 1 μ' = eLpNorm (↑↑g - ↑↑f) 1 μ'
h_eLpNorm_ne_top : eLpNorm (↑↑g - ↑↑f) 1 μ ≠ ∞
⊢ c' ^ (1 / 1).toReal * eLpNorm (↑↑g - ↑↑f) 1 μ = c' * eLpNorm (↑↑g - ↑↑f) 1 μ

Tactic:
]

Goal state after:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm (↑↑g - ↑↑f) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑↑f') μ' :=
  fun f' ↦ Integrable.of_measure_le_smul hc' hμ'_le (L1.integrable_coeFn f')
this : eLpNorm (↑↑(Integrable.toL1 ↑↑g ⋯) - ↑↑(Integrable.toL1 ↑↑f ⋯)) 1 μ' = eLpNorm (↑↑g - ↑↑f) 1 μ'
h_eLpNorm_ne_top : eLpNorm (↑↑g - ↑↑f) 1 μ ≠ ∞
⊢ c' ^ (1 / 1).toReal * eLpNorm (↑↑g - ↑↑f) 1 μ = c' * eLpNorm (↑↑g - ↑↑f) 1 μ
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : AEStronglyMeasurable f (μ.trim hm)
⊢ ∫ (a : β), AEStronglyMeasurable.mk f hf a ∂μ = ∫ (a : β), AEStronglyMeasurable.mk f hf a ∂μ.trim hm

Tactic:
]

Goal state after:
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : AEStronglyMeasurable f (μ.trim hm)
⊢ ∫ (a : β), AEStronglyMeasurable.mk f hf a ∂μ = ∫ (a : β), AEStronglyMeasurable.mk f hf a ∂μ.trim hm
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ Tendsto (fun i ↦ 1) atTop (𝓝 1)

Tactic:
]

Goal state after:
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ Tendsto (fun i ↦ 1) atTop (𝓝 1)
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm (↑↑g - ↑↑f) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑↑f') μ' :=
  fun f' ↦ Integrable.of_measure_le_smul hc' hμ'_le (L1.integrable_coeFn f')
this : eLpNorm (↑↑(Integrable.toL1 ↑↑g ⋯) - ↑↑(Integrable.toL1 ↑↑f ⋯)) 1 μ' = eLpNorm (↑↑g - ↑↑f) 1 μ'
h_eLpNorm_ne_top : eLpNorm (↑↑g - ↑↑f) 1 μ ≠ ∞
⊢ ¬(c' = 0 ∨ c' = ∞)

Tactic:
]

Goal state after:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm (↑↑g - ↑↑f) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑↑f') μ' :=
  fun f' ↦ Integrable.of_measure_le_smul hc' hμ'_le (L1.integrable_coeFn f')
this : eLpNorm (↑↑(Integrable.toL1 ↑↑g ⋯) - ↑↑(Integrable.toL1 ↑↑f ⋯)) 1 μ' = eLpNorm (↑↑g - ↑↑f) 1 μ'
h_eLpNorm_ne_top : eLpNorm (↑↑g - ↑↑f) 1 μ ≠ ∞
⊢ ¬(c' = 0 ∨ c' = ∞)
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm (↑↑g - ↑↑f) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑↑f') μ' :=
  fun f' ↦ Integrable.of_measure_le_smul hc' hμ'_le (L1.integrable_coeFn f')
this : eLpNorm (↑↑(Integrable.toL1 ↑↑g ⋯) - ↑↑(Integrable.toL1 ↑↑f ⋯)) 1 μ' = eLpNorm (↑↑g - ↑↑f) 1 μ'
h_eLpNorm_ne_top : eLpNorm (↑↑g - ↑↑f) 1 μ ≠ ∞
⊢ c'.toReal ≠ 0

Tactic:
rw [Ne, toReal_eq_zero_iff]

Goal state after:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm (↑↑g - ↑↑f) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑↑f') μ' :=
  fun f' ↦ Integrable.of_measure_le_smul hc' hμ'_le (L1.integrable_coeFn f')
this : eLpNorm (↑↑(Integrable.toL1 ↑↑g ⋯) - ↑↑(Integrable.toL1 ↑↑f ⋯)) 1 μ' = eLpNorm (↑↑g - ↑↑f) 1 μ'
h_eLpNorm_ne_top : eLpNorm (↑↑g - ↑↑f) 1 μ ≠ ∞
⊢ ¬(c' = 0 ∨ c' = ∞)
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case h
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm (↑↑g - ↑↑f) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑↑f') μ' :=
  fun f' ↦ Integrable.of_measure_le_smul hc' hμ'_le (L1.integrable_coeFn f')
this : eLpNorm (↑↑(Integrable.toL1 ↑↑g ⋯) - ↑↑(Integrable.toL1 ↑↑f ⋯)) 1 μ' = eLpNorm (↑↑g - ↑↑f) 1 μ'
h_eLpNorm_ne_top : eLpNorm (↑↑g - ↑↑f) 1 μ ≠ ∞
⊢ (eLpNorm (↑↑g - ↑↑f) 1 μ').toReal < ε

Tactic:
calc
    (eLpNorm (⇑g - ⇑f) 1 μ').toReal ≤ (c' * eLpNorm (⇑g - ⇑f) 1 μ).toReal := by
      refine toReal_mono (ENNReal.mul_ne_top hc' h_eLpNorm_ne_top) ?_
      refine (eLpNorm_mono_measure (⇑g - ⇑f) hμ'_le).trans_eq ?_
      rw [eLpNorm_smul_measure_of_ne_zero hc'0, smul_eq_mul]
      simp
    _ = c'.toReal * (eLpNorm (⇑g - ⇑f) 1 μ).toReal := toReal_mul
    _ ≤ c'.toReal * (ε / 2 / c'.toReal) := by gcongr
    _ = ε / 2 := by
      refine mul_div_cancel₀ (ε / 2) ?_; rw [Ne, toReal_eq_zero_iff]; simp [hc', hc'0]
    _ < ε := half_lt_self hε_pos

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : r = 0
this : f =ᵐ[μ] 0
⊢ 0 ≤ 0

Tactic:
]

Goal state after:
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ Tendsto (fun i ↦ thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)

Tactic:
]

Goal state after:
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ Tendsto (fun i ↦ thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑0
hr : r = 0
⊢ f =ᵐ[μ] 0

Tactic:
]

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑0
hr : r = 0
⊢ f =ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
⊢ -∫ (a : α), f a ∂μ = 0

Tactic:
neg_eq_zero

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
⊢ ∫ (a : α), f a ∂μ = 0
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
⊢ ∫ (a : α), f a ∂μ = 0

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
⊢ ∫ (a : α), f a ∂μ = 0
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : ∀ ε > 0, ∀ᶠ (x : ℕ) in atTop, dist (δseq x) 0 < ε
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
⊢ Tendsto (fun i ↦ thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)

Tactic:
]

Goal state after:
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : ∀ ε > 0, ∀ᶠ (x : ℕ) in atTop, dist (δseq x) 0 < ε
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
⊢ Tendsto (fun i ↦ thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)