mathlib-initiative/mathlib-tactics huggingface dataset:
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
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
B1 : ℕ → ℝ≥0∞ := fun n ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
⊢ ∑' (i : ℕ), B1 i < ∞

Tactic:
hB1_has.tsum_eq

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
B1 : ℕ → ℝ≥0∞ := fun n ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
⊢ ENNReal.ofReal M < ∞
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: case neg
α : 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
hμ : ¬μ = 0
⊢ ↑‖f‖₊ ≤ ↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C)

Tactic:
nnnorm_def,

Goal state after:
case neg
α : 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
hμ : ¬μ = 0
⊢ ↑(eLpNorm (↑↑f) p μ).toNNReal ≤ ↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C)
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
c : 𝕜
f : ↥(Lp E p μ)
⊢ eLpNorm (c • ↑↑f) p μ < ∞

Tactic:
exact eLpNorm_const_smul_le.trans_lt <| (by finiteness)

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
p_zero : ¬p = 0
⊢ eLpNorm (fun x ↦ ‖f x‖ₑ ^ 0) ∞ μ < ∞

Tactic:
simpa only [ENNReal.rpow_zero, eLpNorm_exponent_top] using (memLp_top_const_enorm (by simp)).2

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
K : Type u_8
inst✝ : RCLike K
f : α → K
⊢ MemLp (fun x ↦ RCLike.re (f x)) p μ ∧ MemLp (fun x ↦ RCLike.im (f x)) p μ ↔ MemLp f p μ

Tactic:
refine ⟨?_, fun hf => ⟨hf.re, hf.im⟩⟩

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
K : Type u_8
inst✝ : RCLike K
f : α → K
⊢ MemLp (fun x ↦ RCLike.re (f x)) p μ ∧ MemLp (fun x ↦ RCLike.im (f x)) p μ → MemLp f 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)
L L' : E →SL[σ] F
⊢ compLpL p μ (L + L') = compLpL p μ L + compLpL p μ L'

Tactic:
ext1 f

Goal state after:
α : 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)
L L' : E →SL[σ] F
f : ↥(Lp E p μ)
⊢ (compLpL p μ (L + L')) f = (compLpL p μ L + compLpL p μ L') f
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
⊢ compLpL p μ (c • L) = c • compLpL p μ L

Tactic:
ext1 f

Goal state after:
α : 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
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: case neg
𝕜 : 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
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖
x : E
hx : ¬x = 0
⊢ ‖f x‖ ≤ C * ‖x‖

Tactic:
exact SemilinearMapClass.bound_of_shell_semi_normed f ε_pos hc hf (norm_ne_zero_iff.2 hx)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
⊢ IsOpen (range toContinuousLinearMap)

Tactic:
rw [isOpen_iff_mem_nhds, forall_mem_range]

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
⊢ ∀ (i : E ≃L[𝕜] F), range toContinuousLinearMap ∈ 𝓝 ↑i
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: case pos
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this✝ : {ξ₀}ᶜ ∈ 𝓝 0
this : balancedCore 𝕜 {ξ₀}ᶜ ∈ 𝓝 0
ξ : 𝕜
hξ : ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ
hξ0 : ξ = 0
⊢ ξ ∈ Metric.closedBall 0 ε

Tactic:
rw [hξ0]

Goal state after:
case pos
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
t : TopologicalSpace 𝕜
h₁ : IsTopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this✝ : {ξ₀}ᶜ ∈ 𝓝 0
this : balancedCore 𝕜 {ξ₀}ᶜ ∈ 𝓝 0
ξ : 𝕜
hξ : ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ
hξ0 : ξ = 0
⊢ 0 ∈ Metric.closedBall 0 ε
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ENormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u μ
v : Set α := toMeasurable μ u
⊢ ∀ x ∈ u, ‖f x‖ₑ ≠ 0

Tactic:
intro x hx; simpa using hx.2

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᵐ[μ] f
h_le₂ : f ≤ᵐ[μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
x : α
hx : ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
⊢ max ‖g₁ x‖ ‖g₂ x‖ ≤ ‖g₁ x‖ + ‖g₂ x‖

Tactic:
exact max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _)

Goal state after:
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst✝²] ↑l.ker
H : ¬finrank 𝕜 ↥l.range = 0
this✝ : finrank 𝕜 ↥l.range = 1
hi : Function.Injective ⇑(l.ker.liftQ l ⋯)
hs : Function.Surjective ⇑(l.ker.liftQ l ⋯)
φ : (E ⧸ l.ker) ≃ₗ[𝕜] 𝕜 := LinearEquiv.ofBijective (l.ker.liftQ l ⋯) ⋯
hlφ : ⇑l = ⇑φ ∘ ⇑l.ker.mkQ
this : induced (⇑φ.toEquiv.symm) inferInstance = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
⊢ Continuous[QuotientModule.Quotient.topologicalSpace l.ker, coinduced (⇑φ.toEquiv) inferInstance] ⇑φ.toEquiv

Tactic:
exact continuous_coinduced_rng

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
K K' : ℝ≥0
f : α → β
g : β → γ
hg : LipschitzWith K g
hg' : AntilipschitzWith K' g
g0 : g 0 = 0
⊢ Integrable (g ∘ f) μ ↔ Integrable f μ

Tactic:
simp [← memLp_one_iff_integrable, hg.memLp_comp_iff_of_antilipschitz hg' g0]

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

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁵ : PartialOrder α
inst✝⁴ : MeasurableSingletonClass α
inst✝³ : TopologicalSpace ε'
inst✝² : ESeminormedAddMonoid ε'
inst✝¹ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
inst✝ : NullSingletonClass μ
ha : ‖f a‖ₑ ≠ ∞
⊢ μ {a} ≠ ∞

Tactic:
by rw [measure_singleton]; exact ENNReal.zero_ne_top

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

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁵ : PartialOrder α
inst✝⁴ : MeasurableSingletonClass α
inst✝³ : TopologicalSpace ε'
inst✝² : ESeminormedAddMonoid ε'
inst✝¹ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
inst✝ : NullSingletonClass μ
hb : ‖f b‖ₑ ≠ ∞
⊢ μ {b} ≠ ∞

Tactic:
by rw [measure_singleton]; exact ENNReal.zero_ne_top

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

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁵ : PartialOrder α
inst✝⁴ : MeasurableSingletonClass α
inst✝³ : TopologicalSpace ε'
inst✝² : ESeminormedAddMonoid ε'
inst✝¹ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
b : α
inst✝ : NullSingletonClass μ
hb : ‖f b‖ₑ ≠ ∞
⊢ μ {b} ≠ ∞

Tactic:
by rw [measure_singleton]; exact ENNReal.zero_ne_top

Goal state after:
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
Eᵤ : Type u_6
inst✝⁵ : AddCommGroup Eᵤ
inst✝⁴ : Module 𝕜 Eᵤ
inst✝³ : UniformSpace Eᵤ
inst✝² : T2Space Eᵤ
inst✝¹ : IsUniformAddGroup Eᵤ
inst✝ : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : U ∈ 𝓝 0
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
⊢ FiniteDimensional 𝕜 Eᵤ

Tactic:
let : FiniteDimensional 𝕜 M := Finite.span_of_finite 𝕜 hF_finite

Goal state after:
𝕜 : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
Eᵤ : Type u_6
inst✝⁵ : AddCommGroup Eᵤ
inst✝⁴ : Module 𝕜 Eᵤ
inst✝³ : UniformSpace Eᵤ
inst✝² : T2Space Eᵤ
inst✝¹ : IsUniformAddGroup Eᵤ
inst✝ : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : U ∈ 𝓝 0
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional 𝕜 ↥M := Finite.span_of_finite 𝕜 hF_finite
⊢ FiniteDimensional 𝕜 Eᵤ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
ε : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝¹ : PseudoMetrizableSpace ε
inst✝ : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen[inst✝⁴] U
hZ : IsClosed[inst✝⁴] Z
hf : ∀ k ⊆ U ∩ Z, IsCompact k → IntegrableOn f k μ
hx : x ∈ U ∩ Z
⊢ IntegrableAtFilter f (𝓝[U ∩ Z] x) μ

Tactic:
rcases exists_compact_subset hU hx.1 with ⟨K, hK, hxK, hKU⟩

Goal state after:
X : Type u_1
ε : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝¹ : PseudoMetrizableSpace ε
inst✝ : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen[inst✝⁴] U
hZ : IsClosed[inst✝⁴] Z
hf : ∀ k ⊆ U ∩ Z, IsCompact k → IntegrableOn f k μ
hx : x ∈ U ∩ Z
K : Set X
hK : IsCompact K
hxK : x ∈ interior K
hKU : K ⊆ U
⊢ IntegrableAtFilter f (𝓝[U ∩ Z] x) μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
ε : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝¹ : PseudoMetrizableSpace ε
inst✝ : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen[inst✝⁴] U
hZ : IsClosed[inst✝⁴] Z
hf : ∀ k ⊆ U ∩ Z, IsCompact k → IntegrableOn f k μ
hx : x ∈ U ∩ Z
K : Set X
hK : IsCompact K
hxK : x ∈ interior K
hKU : K ⊆ U
⊢ IntegrableAtFilter f (𝓝[Z] x) μ

Tactic:
refine ⟨Z ∩ K, inter_mem_nhdsWithin _ (mem_interior_iff_mem_nhds.1 hxK), ?_⟩

Goal state after:
X : Type u_1
ε : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝¹ : PseudoMetrizableSpace ε
inst✝ : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen[inst✝⁴] U
hZ : IsClosed[inst✝⁴] Z
hf : ∀ k ⊆ U ∩ Z, IsCompact k → IntegrableOn f k μ
hx : x ∈ U ∩ Z
K : Set X
hK : IsCompact K
hxK : x ∈ interior K
hKU : K ⊆ U
⊢ IntegrableOn f (Z ∩ K) μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝ : SecondCountableTopology X
hf : LocallyIntegrable f μ
⊢ ∃ u, (∀ (n : ℕ), IsOpen[inst✝³] (u n)) ∧ ⋃ n, u n = univ ∧ ∀ (n : ℕ), IntegrableOn f (u n) μ

Tactic:
by
  rcases (hf.locallyIntegrableOn univ).exists_nat_integrableOn with ⟨u, u_open, u_union, hu⟩
  refine ⟨u, u_open, eq_univ_of_univ_subset u_union, fun n ↦ ?_⟩
  simpa only [inter_univ] using hu n

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
hSp : ∀ i ∈ sι, μ (S i) ≠ ∞
h_disj : ∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)
⊢ T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)

Tactic:
revert hSp h_disj

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
⊢ (∀ i ∈ sι, μ (S i) ≠ ∞) → (∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
hp_ne_top : p ≠ ∞
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : eLpNorm f p μ < ∞
⊢ Tendsto (fun n ↦ eLpNorm (⇑(approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) - f) p μ) atTop (𝓝 0)

Tactic:
refine tendsto_approxOn_Lp_eLpNorm fmeas _ hp_ne_top ?_ ?_

Goal state after:
case refine_1
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
hp_ne_top : p ≠ ∞
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : eLpNorm f p μ < ∞
⊢ ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})

case refine_2
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
hp_ne_top : p ≠ ∞
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : eLpNorm f p μ < ∞
⊢ eLpNorm (fun x ↦ f x - 0) p μ < ∞
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
⊢ DominatedFinMeasAdditive μ' T C

Tactic:
by
  have h' : ∀ s, μ s = ∞ → μ' s = ∞ := fun s hs ↦ top_unique <| hs.symm.trans_le (h _)
  refine ⟨hT.1.of_eq_top_imp_eq_top fun s _ ↦ h' s, fun s hs hμ's ↦ ?_⟩
  have hμs : μ s < ∞ := (h s).trans_lt hμ's
  calc
    ‖T s‖ ≤ C * μ.real s := hT.2 s hs hμs
    _ ≤ C * μ'.real s := by
      simp only [measureReal_def]
      gcongr
      exact hμ's.ne

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

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst✝³ : NormedAddCommGroup G''
inst✝² : PartialOrder G''
inst✝¹ : IsOrderedAddMonoid G''
inst✝ : NormedSpace ℝ G''
T T' : Set α → E →L[ℝ] G''
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : E), (T s) x ≤ (T' s) x
f : α →ₛ E
hf : Integrable (⇑f) μ
i : E
a✝ : i ∈ f.range
h0 : ¬i = 0
⊢ (T (⇑f ⁻¹' {i})) i ≤ (T' (⇑f ⁻¹' {i})) i

Tactic:
· exact hTT' _ (measurableSet_fiber _ _) (measure_preimage_lt_top_of_integrable _ hf h0) i

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

Goal state before:
pp: case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ (T (⇑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x})) x +
      ∑ x_1 ∈ {0}, (T (⇑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 =
    (T s) x

Tactic:
rw [sum_singleton, (T _).map_zero, add_zero]

Goal state after:
case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ (T (⇑(piecewise s hs (const α x) (const α 0)) ⁻¹' {x})) x = (T s) x
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᵐ[ν] f
hfi : Integrable f ν
hE : ¬CompleteSpace E
⊢ ∫ (a : α), f a ∂μ ≤ ∫ (a : α), f a ∂ν

pp: case pos
α : Type u_1
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᵐ[ν] f
hfi : Integrable f ν
hE : CompleteSpace E
⊢ ∫ (a : α), f a ∂μ ≤ ∫ (a : α), f a ∂ν

Tactic:
· simp [integral, hE]

Goal state after:
case pos
α : Type u_1
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᵐ[ν] f
hfi : Integrable f ν
hE : CompleteSpace E
⊢ ∫ (a : α), f a ∂μ ≤ ∫ (a : α), f a ∂ν
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹⁴ : Ring S
inst✝¹³ : Ring R
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module R V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module R W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : Module S W
inst✝⁴ : SMulCommClass R S W
inst✝³ : ContinuousConstSMul S W
inst✝² : AddTorsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalAddTorsor Q
f : V →ᴬ[R] Q
x : V
⊢ (f.contLinear.toContinuousAffineMap +ᵥ const R V (f 0)) x = f x

Tactic:
vadd_apply,

Goal state after:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹⁴ : Ring S
inst✝¹³ : Ring R
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module R V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module R W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : Module S W
inst✝⁴ : SMulCommClass R S W
inst✝³ : ContinuousConstSMul S W
inst✝² : AddTorsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalAddTorsor Q
f : V →ᴬ[R] Q
x : V
⊢ f.contLinear.toContinuousAffineMap x +ᵥ (const R V (f 0)) x = f x
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case f_nn
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
i : ℕ
⊢ 0 ≤ᵐ[μ] fun a ↦ f i a - f 0 a

Tactic:
filter_upwards [hf_mono] with a h_mono

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
i : ℕ
a : α
h_mono : Monotone fun i ↦ f i a
⊢ 0 a ≤ f i a - f 0 a
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
x y : P
⊢ dist ((pointReflection 𝕜 x) y) y = ‖2‖ * dist x y

Tactic:
rw [dist_pointReflection_self', two_nsmul, ← two_smul 𝕜, norm_smul, ← dist_eq_norm_vsub V]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: case mpr
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
⊢ (∀ (x : α), dist (f x) (g x) < C) → dist f g < C

Tactic:
· by_cases h : Nonempty α
    · exact dist_lt_of_nonempty_compact
    · rintro -
      convert! C0
      apply le_antisymm _ dist_nonneg'
      rw [dist_eq]
      exact csInf_le ⟨0, fun C => And.left⟩ ⟨le_rfl, fun x => False.elim (h (Nonempty.intro x))⟩

Goal state after: