mathlib-initiative/mathlib-tactics huggingface dataset:
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
s : Set X
inst✝¹ : PseudoMetrizableSpace ε
inst✝ : LocallyCompactSpace X
hs : IsLocallyClosed s
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
x : X
hx : x ∈ s
⊢ IntegrableAtFilter f (𝓝[s] x) μ

Tactic:
rcases hs with ⟨U, Z, hU, hZ, rfl⟩

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
⊢ IntegrableAtFilter f (𝓝[U ∩ Z] x) μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
ε'' : Type u_5
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace ε''
inst✝² : ESeminormedAddMonoid ε''
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → ε''
μ : Measure X
h : LocallyIntegrable (f ∘ ⇑e) μ
x : Y
U : Set X
hU : U ∈ 𝓝 (e.symm x)
h'U : IntegrableOn (f ∘ ⇑e) U μ
⊢ IntegrableAtFilter f (𝓝 x) (Measure.map (⇑e) μ)

Tactic:
refine ⟨e.symm ⁻¹' U, e.symm.continuous.continuousAt.preimage_mem_nhds hU, ?_⟩

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
ε'' : Type u_5
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace ε''
inst✝² : ESeminormedAddMonoid ε''
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → ε''
μ : Measure X
h : LocallyIntegrable (f ∘ ⇑e) μ
x : Y
U : Set X
hU : U ∈ 𝓝 (e.symm x)
h'U : IntegrableOn (f ∘ ⇑e) U μ
⊢ IntegrableOn f (⇑e.symm ⁻¹' U) (Measure.map (⇑e) μ)
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
⊢ (K.indicator fun x ↦ g x • f x) = fun x ↦ g x • f x

Tactic:
apply indicator_eq_self.2

Goal state after:
X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := ⋯
hK : IsCompact K
⊢ (support fun x ↦ g x • f x) ⊆ K
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
⊢ (K.indicator fun x ↦ f x • g x) = fun x ↦ f x • g x

Tactic:
apply indicator_eq_self.2

Goal state after:
X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := ⋯
hK : IsCompact K
⊢ (support fun x ↦ f x • g x) ⊆ K
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case h
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E₁ G
k : ℕ
x : (i : ι) → E₁ i
e : Fin k ↪ ι
a✝ : e ∈ univ
⊢ ‖(f.iteratedFDerivComponent e.toEquivRange) fun i ↦ x ↑i‖ ≤ ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)

Tactic:
simpa using norm_iteratedFDerivComponent_le f e.toEquivRange x

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞
hp0 : ¬p = 0
hp_top : ¬p = ∞
y : E
x✝ : y ∈ f.range
⊢ ‖y‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {y}) < ∞

Tactic:
by_cases hy0 : y = 0

Goal state after:
case pos
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞
hp0 : ¬p = 0
hp_top : ¬p = ∞
y : E
x✝ : y ∈ f.range
hy0 : y = 0
⊢ ‖y‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {y}) < ∞

case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞
hp0 : ¬p = 0
hp_top : ¬p = ∞
y : E
x✝ : y ∈ f.range
hy0 : ¬y = 0
⊢ ‖y‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {y}) < ∞
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: case refine_1
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup Eₗ
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 Eₗ
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst✝ : RingHomIsometric σ₁₂
h_dense : DenseRange ⇑e
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
⊢ 0 ≤ ↑N * ‖f‖

pp: case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup Eₗ
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 Eₗ
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst✝ : RingHomIsometric σ₁₂
h_dense : DenseRange ⇑e
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
⊢ Continuous fun x ↦ ‖(f.extend e) x‖

pp: case refine_3
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup Eₗ
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 Eₗ
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst✝ : RingHomIsometric σ₁₂
h_dense : DenseRange ⇑e
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
x : E
⊢ ‖(f.extend e) (e x)‖ ≤ ↑N * ‖f‖ * ‖e x‖

Tactic:
· cases le_total 0 N with
    | inl hN => exact mul_nonneg hN (norm_nonneg _)
    | inr hN =>
      have : Unique E := ⟨⟨0⟩, fun x ↦ norm_le_zero_iff.mp <|
        (h_e x).trans (mul_nonpos_of_nonpos_of_nonneg hN (norm_nonneg _))⟩
      obtain rfl : f = 0 := Subsingleton.elim ..
      simp

Goal state after:
case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup Eₗ
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 Eₗ
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst✝ : RingHomIsometric σ₁₂
h_dense : DenseRange ⇑e
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
⊢ Continuous fun x ↦ ‖(f.extend e) x‖

case refine_3
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup Eₗ
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 Eₗ
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst✝ : RingHomIsometric σ₁₂
h_dense : DenseRange ⇑e
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
x : E
⊢ ‖(f.extend e) (e x)‖ ≤ ↑N * ‖f‖ * ‖e x‖
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable (⇑f) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
a : E
a0 : a = 0
⊢ 0 ≠ ∞

Tactic:
exact WithTop.zero_ne_top

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ integral f = integralCLM f

Tactic:
simp only [integral]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ integral f = (setToL1 ⋯) f

Tactic:
simp only [integral]

Goal state after:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ integralCLM f = (setToL1 ⋯) f
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
⊢ integral 0 = 0

Tactic:
simp only [integral]

Goal state after:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
⊢ integralCLM 0 = 0
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ↥(Lp E 1 μ)
⊢ integral (f + g) = integral f + integral g

Tactic:
simp only [integral]

Goal state after:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ↥(Lp E 1 μ)
⊢ integralCLM (f + g) = integralCLM f + integralCLM g
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ integral (-f) = -integral f

Tactic:
simp only [integral]

Goal state after:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ integralCLM (-f) = -integralCLM f
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ↥(Lp E 1 μ)
⊢ integral (f - g) = integral f - integral g

Tactic:
simp only [integral]

Goal state after:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ↥(Lp E 1 μ)
⊢ integralCLM (f - g) = integralCLM f - integralCLM g
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ ‖integral f‖ = ‖integralCLM f‖

Tactic:
simp only [integral]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
⊢ Continuous fun f ↦ integral f

Tactic:
simp only [integral]

Goal state after:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
⊢ Continuous fun f ↦ integralCLM f
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ Continuous integral

Tactic:
simp only [integral]

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ Continuous ⇑integralCLM
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ¬(True ∧ HasFiniteIntegral f μ)
⊢ 0 = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal

Tactic:
hasFiniteIntegral_iff_norm,

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ¬(True ∧ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ∞)
⊢ 0 = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case ae_le
α : 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✝² : ClosedIciTopology E
β : Type u_6
inst✝¹ : AddCommMonoid β
inst✝ : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable (fun x ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ (fun x ↦ f x (p • a + q • b)) ≤ᵐ[μ] fun x ↦ p • f x a + q • f x b

Tactic:
case ae_le =>
                    filter_upwards [hf_conv] with x hx
                    exact hx.2 ha hb hp hq hpq

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this : Tendsto (fun n ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
⊢ Tendsto (fun n ↦ ∫ (x : α), - -f n x ∂μ) atTop (𝓝 (∫ (x : α), - -F x ∂μ))

Tactic:
convert! this.neg

Goal state after:
case e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this : Tendsto (fun n ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
x✝ : ℕ
⊢ ∫ (x : α), - -f x✝ x ∂μ = -∫ (x : α), -f x✝ x ∂μ

case e'_5
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this : Tendsto (fun n ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
⊢ ∫ (x : α), - -F x ∂μ = -∫ (x : α), -F x ∂μ
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ ↑‖z‖ ≠ 0

Tactic:
simp only [z_zero, RCLike.ofReal_eq_zero, norm_eq_zero, Ne, not_false_iff]

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

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst✝ : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + ↑ε
s : Finset ι
hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun i ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + ↑ε
ν : Measure X
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
⊢ ∫ (x : X), f x ∂∑ i ∈ s, μ i ∈ Metric.ball (∫ (x : X), f x ∂Measure.sum μ) ↑ε

Tactic:
rw [Metric.mem_ball, ← coe_nndist, NNReal.coe_lt_coe, ← ENNReal.coe_lt_coe, ← hν]

Goal state after:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst✝ : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + ↑ε
s : Finset ι
hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun i ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + ↑ε
ν : Measure X
hν : ∑ i ∈ s, μ i + ν = Measure.sum μ
⊢ ↑(nndist (∫ (x : X), f x ∂∑ i ∈ s, μ i) (∫ (x : X), f x ∂(∑ i ∈ s, μ i + ν))) < ↑ε
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : Countable ι
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst✝ : FiniteDimensional ℝ E
hc : ∀ (i : ι), c i ≠ ∞
⊢ (∫ (x : X), f x ∂Measure.sum fun i ↦ c i • Measure.dirac (x i)) = ∑' (i : ι), (c i).toReal • f (x i)

Tactic:
by_cases hf : Integrable f (.sum (fun i ↦ (c i) • .dirac (x i)))
  · rw [integral_sum_measure hf]
    congr with i
    rw [integral_smul_measure, integral_dirac]
  · rw [integral_undef hf, tsum_eq_zero_of_not_summable]
    apply mt Summable.norm
    convert! mt (integrable_sum_dirac hc) hf
    simp [norm_smul]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, Integrable (f i) μ
⊢ setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)

Tactic:
revert hf

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
s : Finset ι
f : ι → α → E
⊢ (∀ i ∈ s, Integrable (f i) μ) → setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : ι → E
⊢ ‖(↑LinearMap.toContinuousLinearMap ∘ₗ ↑(LinearEquiv.piRing 𝕜 E ι 𝕜).symm) g‖ ≤ ↑(Fintype.card ι) * ‖g‖

Tactic:
rw [← nsmul_eq_mul]

Goal state after:
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : ι → E
⊢ ‖(↑LinearMap.toContinuousLinearMap ∘ₗ ↑(LinearEquiv.piRing 𝕜 E ι 𝕜).symm) g‖ ≤ Fintype.card ι • ‖g‖
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖u (v i)‖₊ ≤ M
e : E
⊢ ‖u e‖₊ ≤ Fintype.card ι • ‖↑v.equivFunL‖₊ * M * ‖e‖₊

Tactic:
set φ := v.equivFunL.toContinuousLinearMap
    calc
      ‖u e‖₊ = ‖u (∑ i, v.equivFun e i • v i)‖₊ := by rw [v.sum_equivFun]
      _ = ‖∑ i, v.equivFun e i • (u <| v i)‖₊ := by simp only [equivFun_apply, map_sum, map_smul]
      _ ≤ ∑ i, ‖v.equivFun e i • (u <| v i)‖₊ := nnnorm_sum_le _ _
      _ = ∑ i, ‖v.equivFun e i‖₊ * ‖u (v i)‖₊ := by simp only [nnnorm_smul]
      _ ≤ ∑ i, ‖v.equivFun e i‖₊ * M := by gcongr; apply hu
      _ = (∑ i, ‖v.equivFun e i‖₊) * M := by rw [Finset.sum_mul]
      _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M := by
        gcongr
        calc
          ∑ i, ‖v.equivFun e i‖₊ ≤ Fintype.card ι • ‖φ e‖₊ := Pi.sum_nnnorm_apply_le_nnnorm _
          _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) := nsmul_le_nsmul_right (φ.le_opNNNorm e) _
      _ = Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊ := by simp only [smul_mul_assoc, mul_right_comm]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : SecondCountableTopology F
d : ℕ := finrank 𝕜 E
e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq ⋯
e₂ : (E →L[𝕜] F) ≃L[𝕜] Fin d → F := (e₁.arrowCongr 1).trans (ContinuousLinearEquiv.piRing (Fin d))
⊢ SecondCountableTopology (E →L[𝕜] F)

Tactic:
exact e₂.toHomeomorph.secondCountableTopology

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f g : C(α, β)
C : ℝ
inst✝ : Nonempty α
⊢ dist f g < C ↔ ∀ (x : α), dist (f x) (g x) < C

Tactic:
simp only [← dist_mkOfCompact, dist_lt_iff_of_nonempty_compact, mkOfCompact_apply]

Goal state after:
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 = ∫ (x : β), f x ∂μ.trim hm

Tactic:
integral_undef hf_int_m

Goal state after:
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
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
⊢ eLpNorm 0 1 μ ≤ 2 * μ univ * ↑r

Tactic:
eLpNorm_zero,

Goal state after:
α : 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 ≤ 2 * μ univ * ↑r