mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

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

Tactic:
and_iff_right hf,

Goal state after:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun x ↦ ‖f x‖ₑ) μ ∧ HasFiniteIntegral (fun x ↦ ‖f x‖ₑ) μ ↔ HasFiniteIntegral f μ
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun a ↦ ‖f a‖) μ ∧ HasFiniteIntegral (fun a ↦ ‖f a‖) μ ↔
    AEStronglyMeasurable f μ ∧ HasFiniteIntegral f μ

Tactic:
and_iff_right hf,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun a ↦ ‖f a‖) μ ∧ HasFiniteIntegral (fun a ↦ ‖f a‖) μ ↔ HasFiniteIntegral f μ
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖↑(f a).toNNReal‖ ∂μ < ∞

Tactic:
refine lt_of_le_of_lt ?_ ((hasFiniteIntegral_iff_norm _).1 hf.hasFiniteIntegral)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖↑(f a).toNNReal‖ ∂μ ≤ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : 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 ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
A : (insert i s).piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₂ i)
B : s.piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₁ i)
⊢ ‖f (update (s.piecewise m₂ m₁) i (m₁ i)) - f (update (s.piecewise m₂ m₁) i (m₂ i))‖ ≤
    C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
← f.map_update_sub

Goal state after:
𝕜 : 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 ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
A : (insert i s).piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₂ i)
B : s.piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₁ i)
⊢ ‖f (update (s.piecewise m₂ m₁) i (m₁ i - m₂ i))‖ ≤ C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case neg
𝕜 : 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 ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
A : (insert i s).piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₂ i)
B : s.piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₁ i)
j : ι
a✝ : j ∈ univ
h : ¬j = i
⊢ ‖update (s.piecewise m₂ m₁) i (m₁ i - m₂ i) j‖ ≤ if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
· by_cases h' : j ∈ s <;> simp [h', h]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ
this : (fun x ↦ g x * (f x).toReal) = fun x ↦ (f x).toReal • g x
⊢ Integrable g (μ.withDensity f) ↔ Integrable (fun x ↦ g x * (f x).toReal) μ

Tactic:
rw [this]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ
this : (fun x ↦ g x * (f x).toReal) = fun x ↦ (f x).toReal • g x
⊢ Integrable g (μ.withDensity f) ↔ Integrable (fun x ↦ (f x).toReal • g x) μ
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: case inr
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace E
inst✝² : Countable ι
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst✝ : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x | ∃ c, Tendsto (fun x_1 ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
hconv : StronglyMeasurable fun x ↦ l.limUnder fun x_1 ↦ f x_1 ↑x
this :
  (fun x ↦ l.limUnder fun x_1 ↦ f x_1 x) = Function.extend Subtype.val (fun x ↦ l.limUnder fun x_1 ↦ f x_1 ↑x) fun x ↦ e
⊢ StronglyMeasurable fun x ↦ l.limUnder fun x_1 ↦ f x_1 x

Tactic:
rw [this]

Goal state after:
case inr
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace E
inst✝² : Countable ι
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst✝ : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x | ∃ c, Tendsto (fun x_1 ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
hconv : StronglyMeasurable fun x ↦ l.limUnder fun x_1 ↦ f x_1 ↑x
this :
  (fun x ↦ l.limUnder fun x_1 ↦ f x_1 x) = Function.extend Subtype.val (fun x ↦ l.limUnder fun x_1 ↦ f x_1 ↑x) fun x ↦ e
⊢ StronglyMeasurable (Function.extend Subtype.val (fun x ↦ l.limUnder fun x_1 ↦ f x_1 ↑x) fun x ↦ e)
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: case succ
𝕜 : 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
h_cover : U ⊆ ↑M + c • U
n : ℕ
ih : U ⊆ ↑M + c ^ n • U
⊢ U ⊆ ↑M + c ^ (n + 1) • U

Tactic:
calc
        U ⊆ M + c ^ n • U := ih
        _ ⊆ M + c ^ n • (M + c • U) := by gcongr
        _ ⊆ M + c ^ (n + 1) • U := by
          rw [smul_add, smul_smul, pow_succ, ← add_assoc]
          congr!
          lift c to 𝕜ˣ using isUnit_iff_ne_zero.mpr hc_ne
          simp [← Units.val_pow_eq_pow_val, ← Units.smul_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : α →ₘ[μ] β
⊢ f.Integrable → g.Integrable → (f + g).Integrable

Tactic:
refine induction_on₂ f g fun f hf g hg hfi hgi => ?_

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f✝ g✝ : α →ₘ[μ] β
f : α → β
hf : AEStronglyMeasurable f μ
g : α → β
hg : AEStronglyMeasurable g μ
hfi : (mk f hf).Integrable
hgi : (mk g hg).Integrable
⊢ (mk f hf + mk g hg).Integrable
Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ (if 1 = ∞ then eLpNormEssSup (↑↑f - ↑↑g) μ else ∫⁻ (a : α), ‖↑↑f a - ↑↑g a‖ₑ ∂μ) =
    ∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ

Tactic:
simp [edist_eq_enorm_sub]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ (if 1 = ∞ then eLpNormEssSup (f - g) μ else ∫⁻ (a : α), ‖f a - g a‖ₑ ∂μ) = ∫⁻ (a : α), edist (f a) (g a) ∂μ

Tactic:
simp [edist_eq_enorm_sub]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹⁰ : Fintype ι'
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
x : G
m : (i : ι) → E i
⊢ ‖{ toFun := fun m ↦ (f m) x, map_update_add' := ⋯, map_update_smul' := ⋯ } m‖ ≤ ‖f‖ * ‖x‖ * ∏ i, ‖m i‖

Tactic:
MultilinearMap.coe_mk,

Goal state after:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹⁰ : Fintype ι'
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
x : G
m : (i : ι) → E i
⊢ ‖(f m) x‖ ≤ ‖f‖ * ‖x‖ * ∏ i, ‖m i‖
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i
this : g = (g.compContinuousLinearMap fun i ↦ ↑↑(f i)).compContinuousLinearMap fun i ↦ ↑↑(f i).symm
| ‖g‖

Tactic:
rw [this]

Goal state after:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i
this : g = (g.compContinuousLinearMap fun i ↦ ↑↑(f i)).compContinuousLinearMap fun i ↦ ↑↑(f i).symm
| ‖(g.compContinuousLinearMap fun i ↦ ↑↑(f i)).compContinuousLinearMap fun i ↦ ↑↑(f i).symm‖
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
x : 𝕜
⊢ ↑(x • 0) = ↑0

Tactic:
exact smul_zero _

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 α
f : ↥(α →₁ₛ[μ] E)
⊢ ‖f‖ = SimpleFunc.integral μ (SimpleFunc.map norm (toSimpleFunc f))

Tactic:
rw [norm_eq_sum_mul f, (toSimpleFunc f).map_integral norm (SimpleFunc.integrable f) norm_zero]
  simp_rw [smul_eq_mul]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
a✝ : α
h : (toSimpleFunc (posPart f)) a✝ = (toSimpleFunc f).posPart a✝
⊢ (toSimpleFunc f).posPart a✝ = (SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝

Tactic:
rw [SimpleFunc.map_apply, h]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
a✝ : α
h : (toSimpleFunc (posPart f)) a✝ = (toSimpleFunc f).posPart a✝
⊢ (toSimpleFunc f).posPart a✝ = ‖(toSimpleFunc f).posPart a✝‖
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
a✝ : α
h : (toSimpleFunc (negPart f)) a✝ = (toSimpleFunc f).negPart a✝
⊢ (toSimpleFunc f).negPart a✝ = (SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝

Tactic:
rw [SimpleFunc.map_apply, h]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
a✝ : α
h : (toSimpleFunc (negPart f)) a✝ = (toSimpleFunc f).negPart a✝
⊢ (toSimpleFunc f).negPart a✝ = ‖(toSimpleFunc f).negPart a✝‖
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
⊢ ∫ (a : α), f a + g a ∂μ = ∫ (a : α), f a ∂μ + ∫ (a : α), g a ∂μ

Tactic:
simp only [integral_eq_setToFun]
  exact setToFun_add (dominatedFinMeasAdditive_weightedSMul μ) hf hg

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

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
⊢ (∫⁻ (a : α), ENNReal.ofReal ‖f a - g a‖ ∂μ).toReal ≤ (∫⁻ (a : α), edist (f a) (g a) ∂μ).toReal

Tactic:
simp [edist_eq_enorm_sub]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ AEMeasurable (fun a ↦ ENNReal.ofReal (-f a)) μ

Tactic:
exact measurable_ofReal.comp_aemeasurable hfm.aemeasurable.neg

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
a : α
h : 0 a ≤ f a
⊢ ENNReal.ofReal (f a) = ENNReal.ofReal ‖f a‖

Tactic:
rw [Real.norm_eq_abs, abs_of_nonneg h]

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

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

Tactic:
by_cases hfi : Integrable f μ
  · rw [integral_eq_lintegral_pos_part_sub_lintegral_neg_part hfi]
    have h_min : ∫⁻ a, ENNReal.ofReal (-f a) ∂μ = 0 := by
      rw [lintegral_eq_zero_iff']
      · refine hf.mono ?_
        simp only [Pi.zero_apply]
        intro a h
        simp only [h, neg_nonpos, ofReal_eq_zero]
      · exact measurable_ofReal.comp_aemeasurable hfm.aemeasurable.neg
    rw [h_min, toReal_zero, _root_.sub_zero]
  · rw [integral_undef hfi]
    simp_rw [Integrable, hfm, hasFiniteIntegral_iff_norm, lt_top_iff_ne_top, Ne, true_and,
      Classical.not_not] at hfi
    have : ∫⁻ a : α, ENNReal.ofReal (f a) ∂μ = ∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ := by
      refine lintegral_congr_ae (hf.mono fun a h => ?_)
      dsimp only
      rw [Real.norm_eq_abs, abs_of_nonneg h]
    rw [this, hfi, toReal_top]

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

Goal state before:
pp: case add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun x ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f | motive ↑↑f}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
⊢ ∀ ⦃f g : α →ₛ E⦄,
    Disjoint (support ⇑f) (support ⇑g) →
      (MemLp (⇑f) p μ → motive ⇑f) → (MemLp (⇑g) p μ → motive ⇑g) → MemLp (⇑(f + g)) p μ → motive ⇑(f + g)

Tactic:
intro f g hfg hf hg int_fg
      rw [SimpleFunc.coe_add,
        memLp_add_of_disjoint hfg f.stronglyMeasurable g.stronglyMeasurable] at int_fg
      exact add hfg int_fg.1 int_fg.2 (hf int_fg.1) (hg int_fg.2)

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

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
H : ∀ (f' : α →ₛ E) (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f') p μ → ∃ g, eLpNorm (⇑f' - g) p μ ≤ δ ∧ P g
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < ε
f' : α →ₛ E
hf' : eLpNorm (f - ⇑f') p μ < η
f'_mem : MemLp (⇑f') p μ
g : α → E
hg : eLpNorm (⇑f' - g) p μ ≤ η
Pg : P g
⊢ eLpNorm (f - g) p μ ≤ ε

Tactic:
convert!
      (hη _ _ (hf.aestronglyMeasurable.sub f'.aestronglyMeasurable)
          (f'.aestronglyMeasurable.sub (h2P g Pg)) hf'.le hg).le using 2

Goal state after:
case e'_3
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
H : ∀ (f' : α →ₛ E) (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f') p μ → ∃ g, eLpNorm (⇑f' - g) p μ ≤ δ ∧ P g
η : ℝ≥0∞
ηpos : 0 < η
hη :
  ∀ (f g : α → E),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < ε
f' : α →ₛ E
hf' : eLpNorm (f - ⇑f') p μ < η
f'_mem : MemLp (⇑f') p μ
g : α → E
hg : eLpNorm (⇑f' - g) p μ ≤ η
Pg : P g
⊢ f - g = f - ⇑f' + (⇑f' - g)
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : f.contLinear = 0 ↔ (↑f).linear = 0
⊢ ∀ (q : Q), f = const R P q ↔ ↑f = AffineMap.const R P q

Tactic:
intro q

Goal state after:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : f.contLinear = 0 ↔ (↑f).linear = 0
q : Q
⊢ f = const R P q ↔ ↑f = AffineMap.const R P q
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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
A : ↥(Lp E 1 μ) →L[ℝ] F
hA : ∀ (f : ↥(α →₁ₛ[μ] E)), (setToL1SCLM α E μ hT) f = A ↑f
f : ↥(Lp E 1 μ)
this : setToL1 hT = A
⊢ (setToL1 hT) f = A f

Tactic:
rw [this]

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

Goal state before:
pp: case pos
α : 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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ (L1.setToL1 ⋯) (Integrable.toL1 f hf) =
    (L1.setToL1 hT) (Integrable.toL1 f hf) + (L1.setToL1 hT') (Integrable.toL1 f hf)

Tactic:
L1.setToL1_add_left hT hT'

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hf : ContinuousOn f (interior s)
x : α
h : x ∈ interior s
⊢ ContinuousAt (s.mulIndicator f) x

Tactic:
have hs : interior s ∈ 𝓝 x := mem_interior_iff_mem_nhds.mp (by rwa [interior_interior])
    exact ContinuousAt.congr (hf.continuousAt hs) <| Filter.eventuallyEq_iff_exists_mem.mpr
      ⟨interior s, hs, Set.eqOn_mulIndicator.symm.mono interior_subset⟩

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

Goal state before:
pp: case refine_2
α : 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
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, Integrable (f i) μ) → setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)) →
        (∀ i ∈ insert a s, Integrable (f i) μ) →
          setToFun μ T hT (∑ i ∈ insert a s, f i) = ∑ i ∈ insert a s, setToFun μ T hT (f i)

Tactic:
intro i s his ih hf
    simp only [his, Finset.sum_insert, not_false_iff]
    rw [setToFun_add hT (hf i (Finset.mem_insert_self i s)) _]
    · rw [ih fun i hi => hf i (Finset.mem_insert_of_mem hi)]
    · convert! integrable_finsetSum s fun i hi => hf i (Finset.mem_insert_of_mem hi) with x
      simp

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
f : α → E
⊢ setToFun μ T hT (-f) = -setToFun μ T hT f

Tactic:
by
  by_cases hF : CompleteSpace F; swap
  · simp [setToFun, hF]
  by_cases hf : Integrable f μ
  · rw [setToFun_eq hT hf, setToFun_eq hT hf.neg, Integrable.toL1_neg,
      (L1.setToL1 hT).map_neg]
  · rw [setToFun_undef hT hf, setToFun_undef hT, neg_zero]
    rwa [← integrable_neg_iff] at hf

Goal state after: