mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ (∫⁻ (x : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) x ∂μ).toReal =
    ∑ x ∈ (toSimpleFunc f).range, (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖

Tactic:
rw [SimpleFunc.lintegral_eq_lintegral, SimpleFunc.map_lintegral, ENNReal.toReal_sum]

Goal state after:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ ∑ a ∈ (toSimpleFunc f).range, (‖a‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {a})).toReal =
    ∑ x ∈ (toSimpleFunc f).range, (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖

α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ ∀ a ∈ (toSimpleFunc f).range, ‖a‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {a}) ≠ ∞
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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f✝ : ↥(Lp E 1 μ)
f : ↥(α →₁ₛ[μ] E)
⊢ (setToL1 hT') ↑f = (setToL1SCLM α E μ hT) f

Tactic:
setToL1_eq_setToL1SCLM

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 α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f✝ : ↥(Lp E 1 μ)
f : ↥(α →₁ₛ[μ] E)
⊢ (setToL1SCLM α E μ hT') f = (setToL1SCLM α E μ hT) f
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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T s = T' s
f✝ : ↥(Lp E 1 μ)
f : ↥(α →₁ₛ[μ] E)
⊢ (setToL1 hT') ↑f = (setToL1SCLM α E μ hT) f

Tactic:
setToL1_eq_setToL1SCLM

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 α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T s = T' s
f✝ : ↥(Lp E 1 μ)
f : ↥(α →₁ₛ[μ] E)
⊢ (setToL1SCLM α E μ hT') f = (setToL1SCLM α E μ hT) f
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
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
x : E
⊢ (setToL1 hT) ↑(indicatorConst 1 hs ⋯ x) = (T s) x

Tactic:
setToL1_eq_setToL1SCLM

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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
x : E
⊢ (setToL1SCLM α E μ hT) (indicatorConst 1 hs ⋯ x) = (T s) x
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : 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)
hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)
h_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f' i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone fun i ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
⊢ (fun i ↦ f i a) = fun i ↦ (ENNReal.ofReal (f i a - f 0 a)).toReal + f 0 a

Tactic:
ext i

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)
hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)
h_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f' i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone fun i ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
i : ℕ
⊢ f i a = (ENNReal.ofReal (f i a - f 0 a)).toReal + f 0 a
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁸ : NormedAddCommGroup G''
inst✝⁷ : PartialOrder G''
inst✝⁶ : IsOrderedAddMonoid G''
inst✝⁵ : NormedSpace ℝ G''
inst✝⁴ : CompleteSpace G''
inst✝³ : NormedAddCommGroup G'
inst✝² : PartialOrder G'
inst✝¹ : NormedSpace ℝ G'
inst✝ : ClosedIciTopology G''
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : ↥(Lp G' 1 μ)
hf : 0 ≤ f
g✝ : { g // 0 ≤ g }
g : { g // 0 ≤ g }
this : ↑(coeSimpleFuncNonnegToLpNonneg 1 μ G' g) = ↑↑g
⊢ 0 ≤ (setToL1 hT) ↑↑g

Tactic:
setToL1_eq_setToL1SCLM

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁸ : NormedAddCommGroup G''
inst✝⁷ : PartialOrder G''
inst✝⁶ : IsOrderedAddMonoid G''
inst✝⁵ : NormedSpace ℝ G''
inst✝⁴ : CompleteSpace G''
inst✝³ : NormedAddCommGroup G'
inst✝² : PartialOrder G'
inst✝¹ : NormedSpace ℝ G'
inst✝ : ClosedIciTopology G''
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : ↥(Lp G' 1 μ)
hf : 0 ≤ f
g✝ : { g // 0 ≤ g }
g : { g // 0 ≤ g }
this : ↑(coeSimpleFuncNonnegToLpNonneg 1 μ G' g) = ↑↑g
⊢ 0 ≤ (setToL1SCLM α G' μ hT) ↑g
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
i : ι
s : Finset ι
his : i ∉ s
ih : (∀ i ∈ s, Integrable (f i) μ) → setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
⊢ setToFun μ T hT (f i) + setToFun μ T hT (∑ i ∈ s, f i) = setToFun μ T hT (f i) + ∑ i ∈ s, setToFun μ T hT (f i)

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
i : ι
s : Finset ι
his : i ∉ s
ih : (∀ i ∈ s, Integrable (f i) μ) → setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
⊢ Integrable (∑ i ∈ s, f i) μ

Tactic:
· rw [ih fun i hi => hf i (Finset.mem_insert_of_mem hi)]

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 : Finset ι
his : i ∉ s
ih : (∀ i ∈ s, Integrable (f i) μ) → setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
⊢ Integrable (∑ i ∈ s, f i) μ
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case cons
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
ι : Type u_6
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
a✝ : ι
s✝ : Finset ι
h : a✝ ∉ s✝
ih : (∀ i ∈ s✝, Integrable f (μ i)) → ∫ (a : α), f a ∂∑ i ∈ s✝, μ i = ∑ i ∈ s✝, ∫ (a : α), f a ∂μ i
hf : ∀ i ∈ Finset.cons a✝ s✝ h, Integrable f (μ i)
⊢ ∫ (a : α), f a ∂∑ i ∈ Finset.cons a✝ s✝ h, μ i = ∑ i ∈ Finset.cons a✝ s✝ h, ∫ (a : α), f a ∂μ i

Tactic:
rw [Finset.forall_mem_cons] at hf
    rw [Finset.sum_cons, Finset.sum_cons, ← ih hf.2]
    exact integral_add_measure hf.1 (integrable_finsetSum_measure.2 hf.2)

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
hE : CompleteSpace E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
⊢ ∫ (x : α) in s, f x ∂Measure.dirac a = if a ∈ s then f a else 0

Tactic:
rw [restrict_dirac' hs]
  split_ifs
  · exact integral_dirac' _ _ hf
  · exact integral_zero_measure _

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁸ : NormedAddCommGroup G''
inst✝⁷ : PartialOrder G''
inst✝⁶ : IsOrderedAddMonoid G''
inst✝⁵ : NormedSpace ℝ G''
inst✝⁴ : NormedAddCommGroup G'
inst✝³ : PartialOrder G'
inst✝² : NormedSpace ℝ G'
inst✝¹ : ClosedIciTopology G''
inst✝ : IsOrderedAddMonoid G'
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f g : α → G'
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᵐ[μ] g
⊢ setToFun μ T hT f ≤ setToFun μ T hT g

Tactic:
by
  rw [← sub_nonneg, ← setToFun_sub hT hg hf]
  refine setToFun_nonneg hT hT_nonneg (hfg.mono fun a ha => ?_)
  rw [Pi.sub_apply, Pi.zero_apply, sub_nonneg]
  exact ha

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

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁶ : PseudoMetricSpace 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMul 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c₁ c₂ : 𝕜
f : α →ᵇ β
⊢ dist (c₁ • f) (c₂ • f) ≤ dist c₁ c₂ * dist f 0

Tactic:
rw [dist_le (by positivity)]
    intro x
    refine (dist_pair_smul c₁ c₂ (f x)).trans ?_
    gcongr
    apply dist_coe_le_dist (g := 0)

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 C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x✝ : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h : ∀ (s : Set β) (x : E), MeasurableSet s → (T' s) x = (T (φ ⁻¹' s)) x
hF : CompleteSpace F
hfi' : Integrable f μ'
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : SeparableSpace ↑(range f ∪ {0})
i : ℕ
⊢ setToFun μ' T' hT' ⇑(SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i) =
    setToFun μ T hT ⇑(SimpleFunc.approxOn (f ∘ φ) ⋯ (range f ∪ {0}) 0 ⋯ i)

Tactic:
rw [setToFun_simpleFunc _ _ (SimpleFunc.integrable_approxOn_range _ hfi' _),
    setToFun_simpleFunc, SimpleFunc.approxOn_comp hfm.measurable hφ]

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 C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x✝ : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h : ∀ (s : Set β) (x : E), MeasurableSet s → (T' s) x = (T (φ ⁻¹' s)) x
hF : CompleteSpace F
hfi' : Integrable f μ'
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : SeparableSpace ↑(range f ∪ {0})
i : ℕ
⊢ ∑ x ∈ (SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i).range,
      (T' (⇑(SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i) ⁻¹' {x})) x =
    ∑ x ∈ ((SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i).comp φ hφ).range,
      (T (⇑((SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i).comp φ hφ) ⁻¹' {x})) x

case hf
α : 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 C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x✝ : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h : ∀ (s : Set β) (x : E), MeasurableSet s → (T' s) x = (T (φ ⁻¹' s)) x
hF : CompleteSpace F
hfi' : Integrable f μ'
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : SeparableSpace ↑(range f ∪ {0})
i : ℕ
⊢ Integrable (⇑(SimpleFunc.approxOn (f ∘ φ) ⋯ (range f ∪ {0}) 0 ⋯ i)) μ
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : LocallyCompactSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
⊢ ProperSpace E

Tactic:
have : ProperSpace 𝕜 := .of_locallyCompactSpace 𝕜

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : LocallyCompactSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
this : ProperSpace 𝕜
⊢ ProperSpace E
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 C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x✝ : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : AEStronglyMeasurable f (Measure.map φ μ)
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h : ∀ (s : Set β) (x : E), MeasurableSet s → (T' s) x = (T (φ ⁻¹' s)) x
⊢ setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ)

Tactic:
let g := hfm.mk

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 C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x✝ : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : AEStronglyMeasurable f (Measure.map φ μ)
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h : ∀ (s : Set β) (x : E), MeasurableSet s → (T' s) x = (T (φ ⁻¹' s)) x
g : β → E := AEStronglyMeasurable.mk f hfm
⊢ setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ)
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → |δseq b| < ε
n : ℕ
n_large : n ≥ N
⊢ thickenedIndicatorAux (δseq n) E x = 0

Tactic:
have key : x ∉ thickening ε E := by simpa only [thickening, mem_ofPred_eq, not_lt] using ε_lt.le

Goal state after:
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → |δseq b| < ε
n : ℕ
n_large : n ≥ N
key : x ∉ thickening ε E
⊢ thickenedIndicatorAux (δseq n) E x = 0
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 T' : Set α → E →L[ℝ] F
C C' : ℝ
f : α → E
ν : Measure α
hTμ : DominatedFinMeasAdditive μ T C
hTν : DominatedFinMeasAdditive ν T' C'
hμ : Integrable f μ
hν : Integrable f ν
hTμ_add : DominatedFinMeasAdditive (μ + ν) T (max C 0)
hTν_add : DominatedFinMeasAdditive (μ + ν) T' (max C' 0)
⊢ setToFun (μ + ν) T hTμ_add f + setToFun (μ + ν) T' hTν_add f = setToFun μ T hTμ f + setToFun ν T' hTν f

Tactic:
rw [setToFun_congr_measure_of_add_right hTμ_add hTμ f (hμ.add_measure hν),
        setToFun_congr_measure_of_add_left hTν_add hTν f (hμ.add_measure hν)]

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 = 0

Tactic:
by
  refine setToFun_measure_zero' hT fun s _ hμs => ?_
  rw [lt_top_iff_ne_top] at hμs
  simp only [true_and, Measure.smul_apply, ENNReal.mul_eq_top,
    top_ne_zero, Ne, not_false_iff, not_or, Classical.not_not, smul_eq_mul] at hμs
  simp only [hμs.right, Measure.smul_apply, mul_zero, smul_eq_mul]

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

Goal state before:
pp: δ : Type u_1
X : δ → Type u_3
inst✝² : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝¹ : DecidableEq δ
s : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
i : δ
hi : i ∉ s
x : (i : δ) → X i
⊢ (∫⋯∫⁻_insert i s, f ∂μ) x = ∫⁻ (xᵢ : X i), (∫⋯∫⁻_s, f ∂μ) (update x i xᵢ) ∂μ i

Tactic:
by
  rw [Finset.insert_eq, lmarginal_union μ f hf (Finset.disjoint_singleton_left.mpr hi),
    lmarginal_singleton]

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

Goal state before:
pp: δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
f : ((i : δ) → X i) → ℝ≥0∞
e : ↥Finset.univ ≃ δ := subtypeUnivEquiv ⋯
x : (i : δ) → X i
⊢ (∫⁻ (y : (i : ↥Finset.univ) → X ↑i), f (updateFinset x Finset.univ y) ∂Measure.pi fun i ↦ μ ↑i) =
    ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi μ

Tactic:
measurePreserving_piCongrLeft μ e |>.lintegral_map_equiv,

Goal state after:
δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
f : ((i : δ) → X i) → ℝ≥0∞
e : ↥Finset.univ ≃ δ := subtypeUnivEquiv ⋯
x : (i : δ) → X i
⊢ (∫⁻ (y : (i : ↥Finset.univ) → X ↑i), f (updateFinset x Finset.univ y) ∂Measure.pi fun i ↦ μ ↑i) =
    ∫⁻ (a : (b : ↥Finset.univ) → X (e b)), f ((MeasurableEquiv.piCongrLeft X e) a) ∂Measure.pi fun i' ↦ μ (e i')
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case e'_5
α : 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
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
this :
  Tendsto (fun n ↦ (L1.setToL1 hT) (Integrable.toL1 (fs n) ⋯)) atTop (𝓝 ((L1.setToL1 hT) (Integrable.toL1 f f_int)))
⊢ setToFun μ T hT f = (L1.setToL1 hT) (Integrable.toL1 f f_int)

Tactic:
exact setToFun_eq hT f_int

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

Goal state before:
pp: case hν
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
⊢ Integrable f (μ.restrict (s \ t))

Tactic:
exact Integrable.mono_measure hfs (Measure.restrict_mono sdiff_subset le_rfl)

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] x).NeBot
⊢ leftLim f x ≤ f y

Tactic:
rw [leftLim_eq_sSup hf]

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] x).NeBot
⊢ sSup (f '' Iio x) ≤ f y
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] y).NeBot
⊢ f x ≤ leftLim f y

Tactic:
rw [leftLim_eq_sSup hf]

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] y).NeBot
⊢ f x ≤ sSup (f '' Iio y)