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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ HasFiniteIntegral (fun x ↦ ↑(f x).toNNReal) μ

Tactic:
hasFiniteIntegral_iff_norm

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∫⁻ (a : α), ENNReal.ofReal ‖↑(f a).toNNReal‖ ∂μ < ∞
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst✝¹ : OpensMeasurableSpace α
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ IsSeparable (f '' s)

Tactic:
cases h.out

Goal state after:
case inl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst✝¹ : OpensMeasurableSpace α
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology α
⊢ IsSeparable (f '' s)

case inr
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst✝¹ : OpensMeasurableSpace α
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
h✝ : SecondCountableTopology β
⊢ IsSeparable (f '' s)
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : CommMonoid E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : ContinuousMul E
L : SummationFilter ι
inst✝³ : L.NeBot
inst✝² : L.filter.IsCountablyGenerated
inst✝¹ : IsCompletelyPseudoMetrizableSpace E
inst✝ : Countable ι
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
⊢ StronglyMeasurable fun x ↦ ∏'[L] (i : ι), f i x

Tactic:
by
  let E := { x | Multipliable (f · x) L }
  have hE : MeasurableSet E := StronglyMeasurable.measurableSet_exists_tendsto (by fun_prop)
  have h0 : (Eᶜ.domRestrict fun x => ∏'[L] i, f i x) = fun _ => 1 :=
    funext fun ⟨x, hx⟩ => tprod_eq_one_of_not_multipliable hx
  refine stronglyMeasurable_of_restrict_of_restrict_compl hE ?_ (h0 ▸ stronglyMeasurable_const)
  refine stronglyMeasurable_of_tendsto L.filter ?_ (tendsto_pi_nhds.mpr fun e => e.2.hasProd)
  fun_prop

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 : α → β
hf : Integrable f μ
⊢ edist (toL1 f hf) 0 = ∫⁻ (a : α), edist (f a) 0 ∂μ

Tactic:
simp only [edist_zero_right, Lp.enorm_def, toL1_eq_mk, eLpNorm_aeeqFun]
  apply eLpNorm_one_eq_lintegral_enorm

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

Goal state before:
pp: X : Type u_1
E : Type u_6
F : Type u_7
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure X
f : X → E
hf : LocallyIntegrableOn f univ μ
g : X → F
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖
⊢ LocallyIntegrableOn g univ μ

Tactic:
exact hf.mono hg h

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

Goal state before:
pp: case hf
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
this : (K.indicator fun x ↦ g x • f x) = fun x ↦ g x • f x
⊢ IntegrableOn f K μ

Tactic:
exact hf.integrableOn_isCompact hK

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

Goal state before:
pp: case hφ
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
this : (K.indicator fun x ↦ f x • g x) = fun x ↦ f x • g x
⊢ IntegrableOn f K μ

Tactic:
exact hf.integrableOn_isCompact hK

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

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

Tactic:
refine tendsto_approxOn_Lp_eLpNorm fmeas _ hp_ne_top ?_ ?_
  · filter_upwards with x using subset_closure (by simp)
  · simpa using hf

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

Goal state before:
pp: case neg.hS_meas
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ∞
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
h_left_eq : (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a))
h_left_eq' :
  (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a)) =
    (T (⋃ y ∈ {b ∈ f.range | g b = g (f a)}, ⇑f ⁻¹' {y})) (g (f a))
⊢ ∀ (i : G), MeasurableSet (⇑f ⁻¹' {i})

Tactic:
exact fun i => measurableSet_fiber _ _

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✝ = ‖(toSimpleFunc f).posPart a✝‖

Tactic:
conv_lhs => rw [← SimpleFunc.posPart_map_norm, SimpleFunc.map_apply]

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

Goal state before:
pp: case h
α : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
G'' : Type u_8
inst✝³ : NormedAddCommGroup G''
inst✝² : PartialOrder G''
inst✝¹ : IsOrderedAddMonoid G''
inst✝ : NormedSpace ℝ G''
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] G''
hTT' : ∀ (s : Set α) (x : F), (T s) x ≤ (T' s) x
f : α →ₛ F
x : F
a✝ : x ∈ f.range
⊢ (T (⇑f ⁻¹' {x})) x ≤ (T' (⇑f ⁻¹' {x})) x

Tactic:
apply hTT'

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
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ integral f = ∫ (a : α), ↑↑f a ∂μ

Tactic:
simp only [integral, L1.integral, integral_eq_setToFun]
  exact (L1.setToFun_eq_setToL1 (dominatedFinMeasAdditive_weightedSMul μ) f).symm

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

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✝ : IsOrderedAddMonoid G'
T : Set α → G' →L[ℝ] G''
h_add : FinMeasAdditive μ T
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f g : α →ₛ G'
hfi : Integrable (⇑f) μ
hgi : Integrable (⇑g) μ
hfg : f ≤ g
⊢ 0 ≤ setToSimpleFunc T (g - f)

Tactic:
refine setToSimpleFunc_nonneg' T hT_nonneg _ ?_ (hgi.sub hfi)

Goal state after:
α : 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✝ : IsOrderedAddMonoid G'
T : Set α → G' →L[ℝ] G''
h_add : FinMeasAdditive μ T
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f g : α →ₛ G'
hfi : Integrable (⇑f) μ
hgi : Integrable (⇑g) μ
hfg : f ≤ g
⊢ 0 ≤ g - f
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (fun x ↦ Real.exp (f x)) μ
⊢ 0 < ∫ (x : α), Real.exp (f x) ∂μ

Tactic:
integral_pos_iff_support_of_nonneg (fun x ↦ (Real.exp_pos _).le) hf

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (fun x ↦ Real.exp (f x)) μ
⊢ 0 < μ (Function.support fun x ↦ Real.exp (f x))
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))
⊢ Tendsto (fun n ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))

Tactic:
refine integral_tendsto_of_tendsto_of_monotone (fun n ↦ (hf n).neg) hF.neg ?_ ?_

Goal state after:
case refine_1
α : 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))
⊢ ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ -f n x

case refine_2
α : 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))
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ -f n x) atTop (𝓝 (-F x))
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case refine_1
α : 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))
⊢ ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ -f n x

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

Tactic:
· filter_upwards [h_mono] with x hx n m hnm using neg_le_neg_iff.mpr <| hx hnm

Goal state after:
case refine_2
α : 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))
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ -f n x) atTop (𝓝 (-F x))
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case neg
α : 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 μ
⊢ setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f

Tactic:
· simp_rw [setToFun_undef _ hf, add_zero]

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

Goal state before:
pp: case neg
α : 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
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hT'' : DominatedFinMeasAdditive μ T'' C''
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ T'' hT'' f = setToFun μ T hT f + setToFun μ T' hT' f

Tactic:
· simp_rw [setToFun_undef _ hf, add_zero]

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 : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hg : Integrable g μ
⊢ setToFun μ T hT f + setToFun μ T hT (-g) = setToFun μ T hT f + -setToFun μ T hT g

Tactic:
setToFun_neg hT g

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 : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hg : Integrable g μ
⊢ setToFun μ T hT f + -setToFun μ T hT g = setToFun μ T hT f + -setToFun μ T hT g
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case inr
𝕜 : 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
f : E →ₗ[𝕜] F
hf : Function.Injective ⇑f
h✝ : Nontrivial E
e : E ≃L[𝕜] ↥f.range := (LinearEquiv.ofInjective f hf).toContinuousLinearEquiv
⊢ ∃ K > 0, AntilipschitzWith K ⇑f

Tactic:
exact ⟨_, e.nnnorm_symm_pos, e.antilipschitz⟩

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ ≤ (∫ (a : α), ‖f a‖ ^ p ∂μ) ^ (1 / p) * (∫ (a : α), ‖g a‖ ^ q ∂μ) ^ (1 / q)

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae,
    integral_eq_lintegral_of_nonneg_ae]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ).toReal ^ (1 / p) *
      (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ).toReal ^ (1 / q)

case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ 0 ≤ᵐ[μ] fun a ↦ ‖g a‖ ^ q

case hfm
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ AEStronglyMeasurable (fun a ↦ ‖g a‖ ^ q) μ

case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ 0 ≤ᵐ[μ] fun a ↦ ‖f a‖ ^ p

case hfm
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ AEStronglyMeasurable (fun a ↦ ‖f a‖ ^ p) μ

case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ 0 ≤ᵐ[μ] fun a ↦ ‖f a‖ * ‖g a‖

case hfm
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ AEStronglyMeasurable (fun a ↦ ‖f a‖ * ‖g a‖) μ
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 𝕜
n : ℕ
⊢ IsOpen {f | ↑n ≤ (↑f).rank}

Tactic:
simp only [LinearMap.le_rank_iff_exists_linearIndependent_finset, ofPred_exists, ← exists_prop]
  refine isOpen_biUnion fun t _ => ?_
  have : Continuous fun f : E →L[𝕜] F => fun x : (t : Set E) => f x :=
    continuous_pi fun x => (ContinuousLinearMap.apply 𝕜 F (x : E)).continuous
  exact isOpen_setOfPred_linearIndependent.preimage this

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty α
f : α →ᵇ β
M : ℝ
⊢ ‖f‖ ≤ M ↔ ∀ (x : α), ‖f x‖ ≤ M

Tactic:
by
  simp_rw [norm_def, ← dist_zero_right]
  exact dist_le_iff_of_nonempty

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
⊢ ∀ (s : Set (C(α, β) × C(α, β))),
    s ∈ uniformity C(α, β) ↔
      ∃ t ∈ uniformity (α →ᵇ β),
        ∀ (x y : C(α, β)), ((equivBoundedOfCompact α β) x, (equivBoundedOfCompact α β) y) ∈ t → (x, y) ∈ s

Tactic:
by
      simp only [hasBasis_compactConvergenceUniformity.mem_iff, uniformity_basis_dist_le.mem_iff]
      exact fun s =>
        ⟨fun ⟨⟨a, b⟩, ⟨_, ⟨ε, hε, hb⟩⟩, hs⟩ =>
          ⟨{ p | ∀ x, (p.1 x, p.2 x) ∈ b }, ⟨ε, hε, fun _ h x => hb ((dist_le hε.le).mp h x)⟩,
            fun f g h => hs fun x _ => h x⟩,
          fun ⟨_, ⟨ε, hε, ht⟩, hs⟩ =>
          ⟨⟨Set.univ, { p | dist p.1 p.2 ≤ ε }⟩, ⟨isCompact_univ, ⟨ε, hε, fun _ h => h⟩⟩,
            fun ⟨f, g⟩ h => hs _ _ (ht ((dist_le hε.le).mpr fun x => h x (mem_univ x)))⟩⟩

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' : ℝ
c : ℝ≥0
hT : DominatedFinMeasAdditive μ T C
hT_smul : DominatedFinMeasAdditive (c • μ) T C'
f : α → E
⊢ setToFun μ T hT f = setToFun (c • μ) T hT_smul f

Tactic:
rw! [ENNReal.smul_def]
  apply setToFun_congr_smul_measure _ (by simp)

Goal state after:
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
δ : ℝ
hδ : x ∉ cthickening δ E
⊢ (cthickening δ E).mulIndicator f x =
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x

Tactic:
simp only [hδ, not_false_eq_true, mulIndicator_of_notMem, x_mem_closure]

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

Goal state before:
pp: case insert
δ : Type u_1
δ' : Type u_2
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : DecidableEq δ'
e : δ' → δ
he : Injective e
f : ((i : δ') → X (e i)) → ℝ≥0∞
hf : Measurable f
h : Measurable fun x ↦ (fun {x_1} ↦ x) ∘' e
a✝ : δ'
s✝ : Finset δ'
hi : a✝ ∉ s✝
ih :
  ∀ (x : (i : δ) → X i),
    (∫⋯∫⁻_Finset.image e s✝, f ∘ fun x ↦ (fun {x_1} ↦ x) ∘' e ∂μ) x =
      (∫⋯∫⁻_s✝, f ∂(fun {x} ↦ μ) ∘' e) ((fun {x_1} ↦ x) ∘' e)
x : (i : δ) → X i
⊢ ∫⁻ (xᵢ : X (e a✝)), (∫⋯∫⁻_Finset.image e s✝, f ∘ fun x ↦ (fun {x_1} ↦ x) ∘' e ∂μ) (update x (e a✝) xᵢ) ∂μ (e a✝) =
    (∫⋯∫⁻_insert a✝ s✝, f ∂(fun {x} ↦ μ) ∘' e) ((fun {x_1} ↦ x) ∘' e)

Tactic:
lmarginal_insert _ hf hi

Goal state after:
case insert
δ : Type u_1
δ' : Type u_2
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : DecidableEq δ'
e : δ' → δ
he : Injective e
f : ((i : δ') → X (e i)) → ℝ≥0∞
hf : Measurable f
h : Measurable fun x ↦ (fun {x_1} ↦ x) ∘' e
a✝ : δ'
s✝ : Finset δ'
hi : a✝ ∉ s✝
ih :
  ∀ (x : (i : δ) → X i),
    (∫⋯∫⁻_Finset.image e s✝, f ∘ fun x ↦ (fun {x_1} ↦ x) ∘' e ∂μ) x =
      (∫⋯∫⁻_s✝, f ∂(fun {x} ↦ μ) ∘' e) ((fun {x_1} ↦ x) ∘' e)
x : (i : δ) → X i
⊢ ∫⁻ (xᵢ : X (e a✝)), (∫⋯∫⁻_Finset.image e s✝, f ∘ fun x ↦ (fun {x_1} ↦ x) ∘' e ∂μ) (update x (e a✝) xᵢ) ∂μ (e a✝) =
    ∫⁻ (xᵢ : X (e a✝)), (∫⋯∫⁻_s✝, f ∂(fun {x} ↦ μ) ∘' e) (update ((fun {x_1} ↦ x) ∘' e) a✝ xᵢ) ∂((fun {x} ↦ μ) ∘' e) a✝
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case hf
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ u ∈ {x ∈ t.powerset | x.Nonempty}, MeasurableSet (⋂ i ∈ u, s i)
this :
  ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, (-1) ^ (#x + 1) • f a ∂μ =
    ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X), (⋂ i ∈ x, s i).indicator (fun a ↦ (-1) ^ (#x + 1) • f a) a ∂μ
u : Finset ι
hu : u ∈ {x ∈ t.powerset | x.Nonempty}
⊢ IntegrableOn (fun a ↦ (-1) ^ (#u + 1) • f a) (⋂ i ∈ u, s i) μ

Tactic:
apply Integrable.smul

Goal state after:
case hf
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ u ∈ {x ∈ t.powerset | x.Nonempty}, MeasurableSet (⋂ i ∈ u, s i)
this :
  ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, (-1) ^ (#x + 1) • f a ∂μ =
    ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X), (⋂ i ∈ x, s i).indicator (fun a ↦ (-1) ^ (#x + 1) • f a) a ∂μ
u : Finset ι
hu : u ∈ {x ∈ t.powerset | x.Nonempty}
⊢ Integrable f (μ.restrict (⋂ i ∈ u, s i))
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: case convert_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ i ∈ t, K' i
L : ℕ → Compacts G := fun n ↦ { carrier := K' n, isCompact' := ⋯ }
⊢ ∀ i ∈ t, μ (L i) ≤ μ.innerContent (U i)

Tactic:
intro i _

Goal state after:
case convert_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ i ∈ t, K' i
L : ℕ → Compacts G := fun n ↦ { carrier := K' n, isCompact' := ⋯ }
i : ℕ
a✝ : i ∈ t
⊢ μ (L i) ≤ μ.innerContent (U i)