mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: case pos
X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (fun i ↦ f i) L
h✝¹ : L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝ : Function.HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝
⊢ StronglyMeasurable (if x✝¹.down ∈ L.support then f x✝¹.down else 1)

Tactic:
split_ifs

Goal state after:
case pos
X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (fun i ↦ f i) L
h✝² : L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝¹ : Function.HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝¹
h✝ : x✝¹.down ∈ L.support
⊢ StronglyMeasurable (f x✝¹.down)

case neg
X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (fun i ↦ f i) L
h✝² : L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝¹ : Function.HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝¹
h✝ : x✝¹.down ∉ L.support
⊢ StronglyMeasurable 1
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
this : FiniteDimensional 𝕜 ↥M := Finite.span_of_finite 𝕜 hF_finite
h_cover : U ⊆ ↑M + c • U
h_ind : ∀ (n : ℕ), U ⊆ ↑M + c ^ n • U
h_small : Tendsto (fun n ↦ c ^ n • U) atTop (𝓝 0).smallSets
x : Eᵤ
hx : x ∈ U
m : ℕ → Eᵤ
hm : ∀ (n : ℕ), m n ∈ ↑M
u : ℕ → Eᵤ
hu : ∀ (n : ℕ), u n ∈ c ^ n • U
h_eq : ∀ (n : ℕ), (fun x1 x2 ↦ x1 + x2) (m n) (u n) = x
⊢ x ∈ ↑M

Tactic:
have hu_tendsto : Tendsto u atTop (𝓝 0) := by
      intro W hW
      exact (tendsto_smallSets_iff.mp h_small W hW).mono fun n hn ↦ hn (hu n)

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
h_cover : U ⊆ ↑M + c • U
h_ind : ∀ (n : ℕ), U ⊆ ↑M + c ^ n • U
h_small : Tendsto (fun n ↦ c ^ n • U) atTop (𝓝 0).smallSets
x : Eᵤ
hx : x ∈ U
m : ℕ → Eᵤ
hm : ∀ (n : ℕ), m n ∈ ↑M
u : ℕ → Eᵤ
hu : ∀ (n : ℕ), u n ∈ c ^ n • U
h_eq : ∀ (n : ℕ), (fun x1 x2 ↦ x1 + x2) (m n) (u n) = x
hu_tendsto : Tendsto u atTop (𝓝 0)
⊢ x ∈ ↑M
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module 𝕜 E
inst✝¹ : ContinuousSMul 𝕜 E
p q : Submodule 𝕜 E
h : IsCompl p q
hp : IsClosed[inst✝⁴] ↑p
inst✝ : FiniteDimensional 𝕜 (E ⧸ p)
⊢ IsTopCompl p q

Tactic:
by
  let φ : E ⧸ p →L[𝕜] q := (p.quotientEquivOfIsCompl q h).toLinearMap.toContinuousLinearMap
  have := (φ ∘L p.mkQL).isTopCompl_of_proj fun x ↦ by simp [φ]
  simpa [φ] using this.symm

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: case pos
X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝ : Function.HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝
⊢ AEStronglyMeasurable (if x✝¹.down ∈ L.support then f x✝¹.down else 1) μ

Tactic:
split_ifs

Goal state after:
case pos
X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝² : L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝¹ : Function.HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝¹
h✝ : x✝¹.down ∈ L.support
⊢ AEStronglyMeasurable (f x✝¹.down) μ

case neg
X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝² : L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝¹ : Function.HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝¹
h✝ : x✝¹.down ∉ L.support
⊢ AEStronglyMeasurable 1 μ
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 ι
inst✝ : DecidableEq ι
f : (i : ι) → E i →L[𝕜] E₁ i
i : ι
a : 𝕜
f₀ : E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : ι) → E i
⊢ ((compContinuousLinearMapL (update f i (a • f₀))) g) x = ((a • compContinuousLinearMapL (update f i f₀)) g) x

Tactic:
change (g fun j ↦ update f i (a • f₀) j <| x j) = a • g fun j ↦ update f i f₀ j (x j)

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 ι
inst✝ : DecidableEq ι
f : (i : ι) → E i →L[𝕜] E₁ i
i : ι
a : 𝕜
f₀ : E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : ι) → E i
⊢ (g fun j ↦ (update f i (a • f₀) j) (x j)) = a • g fun j ↦ (update f i f₀ j) (x j)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
⊢ ⇑(toSimpleFunc f) =ᵐ[μ] ↑↑↑f

Tactic:
convert! (AEEqFun.coeFn_mk (toSimpleFunc f) (toSimpleFunc f).aestronglyMeasurable).symm using 2
    exact (Classical.choose_spec f.2).symm

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁷ : AddCommGroup E
inst✝¹⁶ : UniformSpace E
inst✝¹⁵ : IsUniformAddGroup E
inst✝¹⁴ : AddCommGroup F
inst✝¹³ : UniformSpace F
inst✝¹² : IsUniformAddGroup F
inst✝¹¹ : T0Space F
inst✝¹⁰ : AddCommMonoid Eₗ
inst✝⁹ : UniformSpace Eₗ
inst✝⁸ : ContinuousAdd Eₗ
inst✝⁷ : Semiring 𝕜
inst✝⁶ : Semiring 𝕜₂
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : Module 𝕜 Eₗ
inst✝² : ContinuousConstSMul 𝕜 Eₗ
inst✝¹ : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst✝ : CompleteSpace F
e : E →L[𝕜] Eₗ
h_dense : DenseRange ⇑e
h_e : IsUniformInducing ⇑e
x : E
⊢ (f.extend e) (e x) = f x

Tactic:
by
  simp only [extend, h_dense, h_e, and_self, ↓reduceDIte, coe_mk', LinearMap.coe_mk, AddHom.coe_mk]
  exact IsDenseInducing.extend_eq (h_e.isDenseInducing h_dense) f.cont _

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝⁷ : DivisionRing 𝕜
inst✝⁶ : DivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁵ : AddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : SeminormedAddCommGroup Eₗ
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜₂ F
inst✝ : Module 𝕜 Eₗ
f : E →ₛₗ[σ₁₂] F
g : E →ₗ[𝕜] Eₗ
h_norm : ∃ C, ∀ (x : E), ‖f x‖ ≤ C * ‖g x‖
x : E
y : Eₗ
hx : g x = y
⊢ (f.compLeftInverse g) ⟨y, ⋯⟩ = f x

Tactic:
by
  simp [compLeftInverse, h_norm, ← hx]

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
g : α →ₛ G
hp : AEEqFun.mk ⇑g ⋯ ∈ Lp G p μ
hf : 0 ≤ᵐ[μ] ⇑g
x : α
⊢ 0 x ≤ g x → g x = (SimpleFunc.map ({x | 0 ≤ x}.piecewise id 0) g) x

Tactic:
(hx : 0 ≤ g x)

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
g : α →ₛ G
hp : AEEqFun.mk ⇑g ⋯ ∈ Lp G p μ
hf : 0 ≤ᵐ[μ] ⇑g
x : α
hx : 0 ≤ g x
⊢ g x = (SimpleFunc.map ({x | 0 ≤ x}.piecewise id 0) g) x
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
T : Set α → E →L[ℝ] F
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ‖T s‖ ≤ C * μ.real s
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ C * ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) * ‖x‖ = C * ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) • ‖x‖

Tactic:
simp_rw [smul_eq_mul]

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)
⊢ ∑ x ∈ (toSimpleFunc f).range, μ.real (⇑(toSimpleFunc f) ⁻¹' {x}) * ‖x‖ =
    ∑ x ∈ (toSimpleFunc f).range, μ.real (⇑(toSimpleFunc f) ⁻¹' {x}) • ‖x‖

Tactic:
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 : ↥(α →₁ₛ[μ] ℝ)
eq : ∀ (a : α), (toSimpleFunc f).posPart a = max ((toSimpleFunc f) a) 0
ae_eq : ∀ᵐ (a : α) ∂μ, (toSimpleFunc (posPart f)) a = max ((toSimpleFunc f) a) 0
⊢ ⇑(toSimpleFunc (posPart f)) =ᵐ[μ] ⇑(toSimpleFunc f).posPart

Tactic:
refine ae_eq.mono fun a h => ?_

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
eq : ∀ (a : α), (toSimpleFunc f).posPart a = max ((toSimpleFunc f) a) 0
ae_eq : ∀ᵐ (a : α) ∂μ, (toSimpleFunc (posPart f)) a = max ((toSimpleFunc f) a) 0
a : α
h : (toSimpleFunc (posPart f)) a = max ((toSimpleFunc f) a) 0
⊢ (toSimpleFunc (posPart f)) a = (toSimpleFunc f).posPart a
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

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 T' T'' : Set α → E →L[ℝ] F
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ setToSimpleFunc T'' f = setToSimpleFunc T f + setToSimpleFunc T' f

Tactic:
by
  classical
  simp_rw [setToSimpleFunc_eq_sum_filter]
  suffices ∀ x ∈ {x ∈ f.range | x ≠ 0}, T'' (f ⁻¹' {x}) = T (f ⁻¹' {x}) + T' (f ⁻¹' {x}) by
    rw [← sum_add_distrib]
    refine Finset.sum_congr rfl fun x hx => ?_
    rw [this x hx]
    push_cast
    rw [Pi.add_apply]
  intro x hx
  refine
    h_add (f ⁻¹' {x}) (measurableSet_preimage _ _) (measure_preimage_lt_top_of_integrable _ hf ?_)
  rw [mem_filter] at hx
  exact hx.2

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

Goal state before:
pp: case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
s : ↥(α →₁ₛ[μ] ℝ)
⊢ SimpleFunc.integral s = ‖SimpleFunc.posPart s‖ - ‖SimpleFunc.negPart s‖

Tactic:
exact SimpleFunc.integral_eq_norm_posPart_sub _

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 α
ι : Type u_6
f : α → G
hf : HasFiniteIntegral f μ
l : Filter ι
s : ι → Set α
hs : Tendsto (⇑μ ∘ s) l (𝓝 0)
⊢ Tendsto (fun i ↦ ∫ (x : α) in s i, f x ∂μ) l (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]
  simp_rw [← coe_nnnorm, ← NNReal.coe_zero, NNReal.tendsto_coe, ← ENNReal.tendsto_coe,
    ENNReal.coe_zero]
  exact tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
    (tendsto_setLIntegral_zero (ne_of_lt hf) hs) (fun i => zero_le)
    fun i => enorm_integral_le_lintegral_enorm _

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 α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (fun i ↦ eLpNorm (F i - f) 1 μ) l (𝓝 0)
s : Set α
⊢ Tendsto (fun i ↦ ∫ (x : α) in s, F i x ∂μ) l (𝓝 (∫ (x : α) in s, f x ∂μ))

Tactic:
by
  refine tendsto_setIntegral_of_L1 f hfi hFi ?_ s
  simp_rw [eLpNorm_one_eq_lintegral_enorm, Pi.sub_apply] at hF
  exact hF

Goal state after:
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
⊢ u ~[l] 0 ↔ u =O[l] 0

Tactic:
by
  refine ⟨IsEquivalent.isBigO, fun h ↦ ?_⟩
  rw [isEquivalent_zero_iff_eventually_zero, eventuallyEq_iff_exists_mem]
  exact ⟨{ x : α | u x = 0 }, isBigO_zero_right_iff.mp h, fun x hx ↦ hx⟩

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
⊢ ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal

Tactic:
have eq₂ : ENNReal.toReal (∫⁻ a, ENNReal.ofReal (-f a) ∂μ) = ‖Lp.negPart f₁‖ := by
    rw [L1.norm_def]
    congr 1
    apply lintegral_congr_ae
    filter_upwards [Lp.coeFn_negPart f₁, hf.coeFn_toL1] with _ h₁ h₂
    rw [h₁, h₂, ENNReal.ofReal]
    congr 1
    apply NNReal.eq
    simp only [Real.coe_toNNReal', coe_nnnorm, nnnorm_neg]
    rw [Real.norm_of_nonpos (min_le_right _ _), ← max_neg_neg, neg_zero]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
eq₂ : (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal = ‖Lp.negPart f₁‖
⊢ ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
eq₂ : (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal = ‖Lp.negPart f₁‖
⊢ ∫ (a : α), f a ∂μ = ‖Lp.posPart f₁‖ - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal

Tactic:
eq₂,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
eq₂ : (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal = ‖Lp.negPart f₁‖
⊢ ∫ (a : α), f a ∂μ = ‖Lp.posPart f₁‖ - ‖Lp.negPart f₁‖
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case mp.refine_2
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
⊢ u =ᶠ[l] (φ + 1) * v

Tactic:
convert! h.fun_add (EventuallyEq.refl l v)

Goal state after:
case e'_4
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
x✝ : α
⊢ u x✝ = (u - v) x✝ + v x✝

case e'_5
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
x✝ : α
⊢ ((φ + 1) * v) x✝ = (φ * v) x✝ + v x✝
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 : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
⊢ 0 = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal

Tactic:
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]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst✝ : SeparableSpace ↑(range f ∪ {0})
⊢ Tendsto (fun n ↦ ∫ (x : α), ‖(approxOn f fmeas (range f ∪ {0}) 0 ⋯ n) x - f x‖ ∂μ) atTop (𝓝 0)

Tactic:
by
  convert! (tendsto_toReal zero_ne_top).comp (tendsto_approxOn_range_L1_enorm fmeas hf) with n
  rw [integral_norm_eq_lintegral_enorm]
  · simp
  · apply (SimpleFunc.aestronglyMeasurable _).sub
    apply (stronglyMeasurable_iff_measurable_separable.2 ⟨fmeas, ?_⟩).aestronglyMeasurable
    exact .mono (.of_subtype (range f ∪ {0})) subset_union_left

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
⊢ ∃ g, eLpNorm (f - g) p μ ≤ ε ∧ P g

Tactic:
rcases eq_or_ne p 0 with (rfl | hp_pos)
  · rcases h0P (0 : E) MeasurableSet.empty (by simp only [measure_empty, zero_lt_top])
        hε with ⟨g, _, Pg⟩
    exact ⟨g, by simp, Pg⟩
  suffices H : ∀ (f' : α →ₛ E) (δ : ℝ≥0∞) (hδ : δ ≠ 0), MemLp f' p μ →
      ∃ g, eLpNorm (⇑f' - g) p μ ≤ δ ∧ P g by
    obtain ⟨η, ηpos, hη⟩ := exists_Lp_half E μ p hε
    rcases hf.exists_simpleFunc_eLpNorm_sub_lt hp_ne_top ηpos.ne' with ⟨f', hf', f'_mem⟩
    rcases H f' η ηpos.ne' f'_mem with ⟨g, hg, Pg⟩
    refine ⟨g, ?_, Pg⟩
    convert!
      (hη _ _ (hf.aestronglyMeasurable.sub f'.aestronglyMeasurable)
          (f'.aestronglyMeasurable.sub (h2P g Pg)) hf'.le hg).le using 2
    simp only [sub_add_sub_cancel]
  apply SimpleFunc.induction
  · intro c s hs ε εpos Hs
    rcases eq_or_ne c 0 with (rfl | hc)
    · rcases h0P (0 : E) MeasurableSet.empty (by simp only [measure_empty, zero_lt_top])
          εpos with ⟨g, hg, Pg⟩
      rw [← eLpNorm_neg, neg_sub] at hg
      refine ⟨g, ?_, Pg⟩
      convert! hg
      ext x
      simp
    · have : μ s < ∞ := SimpleFunc.measure_lt_top_of_memLp_indicator hp_pos hp_ne_top hc hs Hs
      rcases h0P c hs this εpos with ⟨g, hg, Pg⟩
      rw [← eLpNorm_neg, neg_sub] at hg
      exact ⟨g, hg, Pg⟩
  · intro f f' hff' hf hf' δ δpos int_ff'
    obtain ⟨η, ηpos, hη⟩ := exists_Lp_half E μ p δpos
    rw [SimpleFunc.coe_add,
      memLp_add_of_disjoint hff' f.stronglyMeasurable f'.stronglyMeasurable] at int_ff'
    rcases hf η ηpos.ne' int_ff'.1 with ⟨g, hg, Pg⟩
    rcases hf' η ηpos.ne' int_ff'.2 with ⟨g', hg', Pg'⟩
    refine ⟨g + g', ?_, h1P g g' Pg Pg'⟩
    convert!
      (hη _ _ (f.aestronglyMeasurable.sub (h2P g Pg)) (f'.aestronglyMeasurable.sub (h2P g' Pg')) hg
          hg').le using 2
    rw [SimpleFunc.coe_add]
    abel

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 : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
⊢ Tendsto (fun n ↦ ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))

Tactic:
by
  -- switch from the Bochner to the Lebesgue integral
  let f' := fun n x ↦ f n x - f 0 x
  have hf'_nonneg : ∀ᵐ x ∂μ, ∀ n, 0 ≤ f' n x := by
    filter_upwards [h_mono] with a ha n
    simp [f', ha zero_le]
  have hf'_meas : ∀ n, Integrable (f' n) μ := fun n ↦ (hf n).sub (hf 0)
  suffices Tendsto (fun n ↦ ∫ x, f' n x ∂μ) atTop (𝓝 (∫ x, (F - f 0) x ∂μ)) by
    simp_rw [f', integral_sub (hf _) (hf _), integral_sub' hF (hf 0),
      tendsto_sub_const_iff] at this
    exact this
  have hF_ge : 0 ≤ᵐ[μ] fun x ↦ (F - f 0) x := by
    filter_upwards [h_tendsto, h_mono] with x hx_tendsto hx_mono
    simp only [Pi.zero_apply, Pi.sub_apply, sub_nonneg]
    exact ge_of_tendsto' hx_tendsto (fun n ↦ hx_mono zero_le)
  rw [ae_all_iff] at hf'_nonneg
  simp_rw [integral_eq_lintegral_of_nonneg_ae (hf'_nonneg _) (hf'_meas _).1]
  rw [integral_eq_lintegral_of_nonneg_ae hF_ge (hF.1.sub (hf 0).1)]
  have h_cont := ENNReal.continuousAt_toReal (x := ∫⁻ a, ENNReal.ofReal ((F - f 0) a) ∂μ) ?_
  swap
  · rw [← ofReal_integral_eq_lintegral_ofReal (hF.sub (hf 0)) hF_ge]
    finiteness
  refine h_cont.tendsto.comp ?_
  -- use the result for the Lebesgue integral
  refine lintegral_tendsto_of_tendsto_of_monotone ?_ ?_ ?_
  · exact fun n ↦ ((hf n).sub (hf 0)).aemeasurable.ennreal_ofReal
  · filter_upwards [h_mono] with x hx n m hnm
    refine ENNReal.ofReal_le_ofReal ?_
    simp only [f', tsub_le_iff_right, sub_add_cancel]
    exact hx hnm
  · filter_upwards [h_tendsto] with x hx
    refine (ENNReal.continuous_ofReal.tendsto _).comp ?_
    simp only [Pi.sub_apply]
    exact Tendsto.sub hx tendsto_const_nhds

Goal state after:
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
x : E
hx : x ≠ 0
⊢ ‖(↑‖x‖)⁻¹ • x‖ = 1

Tactic:
by
  have : ‖x‖ ≠ 0 := by simp [hx]
  simp [field, norm_smul]

Goal state after: