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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
n : ℕ
hn : Nonempty (ι ≃ Fin n)
ε : ℝ
hε : 0 < ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
let g : Fin n → α → β := f ∘ hn.some.symm

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
n : ℕ
hn : Nonempty (ι ≃ Fin n)
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := f ∘ ⇑hn.some.symm
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
j : JordanDecomposition α
h : s = j.toSignedMeasure
⊢ s.toJordanDecomposition = j

Tactic:
h,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
j : JordanDecomposition α
h : s = j.toSignedMeasure
⊢ j.toSignedMeasure.toJordanDecomposition = j
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ s ≤[B] 0} ∧ s (B n) = f n
⊢ ∃ i, MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0

Tactic:
have hB₁ : ∀ n, MeasurableSet (B n) := fun n => (hB n).1.1

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
f : ℕ → ℝ
left✝ : Antitone f
hf₂ : Tendsto f atTop (nhds (sInf s.measureOfNegatives))
B : ℕ → Set α
hB : ∀ (n : ℕ), B n ∈ {B | MeasurableSet B ∧ s ≤[B] 0} ∧ s (B n) = f n
hB₁ : ∀ (n : ℕ), MeasurableSet (B n)
⊢ ∃ i, MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ (μ.withDensityᵥ (-f)) i = ∫ (a : α) in i, -f a ∂μ

Tactic:
withDensityᵥ_apply hf.neg hi

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, (-f) x ∂μ = ∫ (a : α) in i, -f a ∂μ
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
g : α → E
hf : AEMeasurable f μ
hfg : Integrable (f • g) μ
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensityᵥ (f • g)) s = ((μ.withDensity fun x ↦ ↑(f x)).withDensityᵥ g) s

Tactic:
withDensityᵥ_apply hfg hs,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
g : α → E
hf : AEMeasurable f μ
hfg : Integrable (f • g) μ
s : Set α
hs : MeasurableSet s
⊢ ∫ (x : α) in s, (f • g) x ∂μ = ((μ.withDensity fun x ↦ ↑(f x)).withDensityᵥ g) s
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f μ
j : Set α
hj₁ : MeasurableSet j
hj₂ : μ j = 0
⊢ ((μ.withDensityᵥ f).trim hm) j = 0

Tactic:
rw [VectorMeasure.trim_measurableSet_eq hm hj₁, withDensityᵥ_apply hfi (hm _ hj₁)]

Goal state after:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f μ
j : Set α
hj₁ : MeasurableSet j
hj₂ : μ j = 0
⊢ ∫ (x : α) in j, f x ∂μ = 0
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
⊢ lpNorm (f + g) p μ ≤ lpNorm f p μ + lpNorm g p μ

Tactic:
by_cases hg : MemLp g p μ
  · rw [← toReal_eLpNorm (hf.add hg).aestronglyMeasurable,
      ← toReal_eLpNorm hf.aestronglyMeasurable, ← toReal_eLpNorm hg.aestronglyMeasurable,
      ← ENNReal.toReal_add hf.eLpNorm_ne_top hg.eLpNorm_ne_top]
    gcongr
    exacts [ENNReal.add_ne_top.2 ⟨hf.eLpNorm_ne_top, hg.eLpNorm_ne_top⟩,
      eLpNorm_add_le hf.aestronglyMeasurable hg.aestronglyMeasurable hp]
  · rw [lpNorm_of_not_memLp fun hfg ↦ hg <| by simpa using hfg.sub hf, lpNorm_of_not_memLp hg]
    simp

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hg : MemLp g p μ
hfg : Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
this : f = (fun x ↦ g) + fun n ↦ f n - g
⊢ UnifIntegrable (fun x ↦ g) p μ

Tactic:
exact unifIntegrable_const hp hp' hg

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case a
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
| ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure

Tactic:
congr
      rw [toJordanDecomposition_smul, JordanDecomposition.smul_negPart, singularPart_smul]

Goal state after:
case a.μ
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
| r • s.toJordanDecomposition.negPart.singularPart μ
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

Goal state before:
pp: Ω : Type u_1
inst✝³ : TopologicalSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c
fs_lim : Tendsto (fun n ω ↦ (fs n) ω) atTop (𝓝 (E.indicator fun x ↦ 1))
⊢ ∀ (ω : Ω), Tendsto (fun n ↦ (fs n) ω) atTop (𝓝 (E.indicator (fun x ↦ 1) ω))

Tactic:
tendsto_pi_nhds

Goal state after:
Ω : Type u_1
inst✝³ : TopologicalSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c
fs_lim : ∀ (x : Ω), Tendsto (fun i ↦ (fs i) x) atTop (𝓝 (E.indicator (fun x ↦ 1) x))
⊢ ∀ (ω : Ω), Tendsto (fun n ↦ (fs n) ω) atTop (𝓝 (E.indicator (fun x ↦ 1) ω))
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

Goal state before:
pp: case h.refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace.PseudoMetrizableSpace X
this : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
F : Set X
hF : IsClosed[inst✝¹] F
key :
  Tendsto (fun n ↦ ⇑(thickenedIndicator ⋯ F)) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F).indicator fun x ↦ 1))
⊢ Tendsto (fun n x ↦ ((fun n ↦ thickenedIndicator ⋯ F) n) x) atTop (𝓝 (F.indicator fun x ↦ 1))

Tactic:
tendsto_pi_nhds

Goal state after:
case h.refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace.PseudoMetrizableSpace X
this : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
F : Set X
hF : IsClosed[inst✝¹] F
key :
  ∀ (x : X),
    Tendsto (fun i ↦ (thickenedIndicator ⋯ F) x) atTop
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F).indicator (fun x ↦ 1) x))
⊢ ∀ (x : X), Tendsto (fun i ↦ ((fun n ↦ thickenedIndicator ⋯ F) i) x) atTop (𝓝 (F.indicator (fun x ↦ 1) x))
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
s : Set Ω
h : ν s = 0
⊢ ↑(ν s) = 0

Tactic:
h,

Goal state after:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
s : Set Ω
h : ν s = 0
⊢ ↑0 = 0
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
ν : FiniteMeasure Ω
s : Set Ω
h : ν s = 0
⊢ ↑(ν s) = 0

Tactic:
h,

Goal state after:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ν : FiniteMeasure Ω
s : Set Ω
h : ν s = 0
⊢ ↑0 = 0
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∈ {x | C ≤ ‖f i x‖₊}
⊢ {x | C ≤ ‖g i x‖₊}.indicator (g i) x = {x | C ≤ ‖f i x‖₊}.indicator (f i) x

Tactic:
Set.indicator_of_mem hfx,

Goal state after:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∈ {x | C ≤ ‖f i x‖₊}
⊢ {x | C ≤ ‖g i x‖₊}.indicator (g i) x = f i x
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
X : Type u_2
inst✝ : TopologicalSpace X
μs : X → ProbabilityMeasure Ω
⊢ Continuous[inst✝, instTopologicalSpace] μs ↔ ∀ (f : Ω →ᵇ ℝ), Continuous[inst✝, _] fun x ↦ ∫ (ω : Ω), f ω ∂↑(μs x)

Tactic:
simp [continuous_iff_continuousAt, ContinuousAt, tendsto_iff_forall_integral_tendsto,
    forall_comm (α := X)]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ Continuous[instTopologicalSpace, _] ((fun φ ↦ φ f) ∘ toWeakDualBCNN)

Tactic:
refine Continuous.comp ?_ (toWeakDualBCNN_continuous (Ω := Ω))

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ Continuous fun φ ↦ φ f
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i ↦ ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))
⊢ Tendsto μs F (𝓝 μ)

Tactic:
by
  apply tendsto_iff_forall_lintegral_tendsto.mpr
  intro f
  apply (ENNReal.tendsto_toReal_iff (fi := F)
      (fun i ↦ (f.lintegral_lt_top_of_nnreal (μs i)).ne) (f.lintegral_lt_top_of_nnreal μ).ne).mp
  have lip : LipschitzWith 1 ((↑) : ℝ≥0 → ℝ) := NNReal.isometry_coe.lipschitz
  set f₀ := BoundedContinuousFunction.comp _ lip f with _def_f₀
  have f₀_eq : ⇑f₀ = ((↑) : ℝ≥0 → ℝ) ∘ ⇑f := rfl
  have f₀_nn : 0 ≤ ⇑f₀ := fun _ ↦ by
    simp only [f₀_eq, Pi.zero_apply, Function.comp_apply, NNReal.zero_le_coe]
  have f₀_ae_nn : 0 ≤ᵐ[(μ : Measure Ω)] ⇑f₀ := .of_forall f₀_nn
  have f₀_ae_nns : ∀ i, 0 ≤ᵐ[(μs i : Measure Ω)] ⇑f₀ := fun i ↦ .of_forall f₀_nn
  have aux :=
    integral_eq_lintegral_of_nonneg_ae f₀_ae_nn f₀.continuous.measurable.aestronglyMeasurable
  have auxs := fun i ↦
    integral_eq_lintegral_of_nonneg_ae (f₀_ae_nns i) f₀.continuous.measurable.aestronglyMeasurable
  simp_rw [f₀_eq, Function.comp_apply, ENNReal.ofReal_coe_nnreal] at aux auxs
  simpa only [← aux, ← auxs] using! h f₀

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᵐ[μ] f i
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∈ {x | C ≤ ‖f i x‖₊}
⊢ {x | C ≤ ‖g i x‖₊}.indicator (g i) x = {x | C ≤ ‖f i x‖₊}.indicator (f i) x

Tactic:
Set.indicator_of_mem hfx,

Goal state after:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᵐ[μ] f i
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∈ {x | C ≤ ‖f i x‖₊}
⊢ {x | C ≤ ‖g i x‖₊}.indicator (g i) x = f i x
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
ε : ℝ
hε : 0 < ε
hfu : UnifIntegrable f p μ
M : ℝ≥0
hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑M
ℐ : ℝ≥0 → ι
δ : ℝ≥0
hδpos : 0 < ↑δ
hδ :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal ↑δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hℐ : ∀ (C : ℝ≥0), ENNReal.ofReal ↑δ < μ {x | C ≤ ‖f (ℐ C) x‖₊}
C : ℝ≥0
⊢ C • ↑δ ^ (1 / p.toReal) ≤ eLpNorm (f (ℐ C)) p μ

Tactic:
calc
        C • (δ : ℝ≥0∞) ^ (1 / p.toReal) ≤ C • μ { x | C ≤ ‖f (ℐ C) x‖₊ } ^ (1 / p.toReal) := by
          rw [ENNReal.smul_def, ENNReal.smul_def, smul_eq_mul, smul_eq_mul]
          simp_rw [ENNReal.ofReal_coe_nnreal] at hℐ
          refine mul_le_mul' le_rfl
            (ENNReal.rpow_le_rpow (hℐ C).le (one_div_nonneg.2 ENNReal.toReal_nonneg))
        _ ≤ eLpNorm ({ x | C ≤ ‖f (ℐ C) x‖₊ }.indicator (f (ℐ C))) p μ := by
          refine le_eLpNorm_of_bddBelow hp hp' _
            (measurableSet_le measurable_const (hf _).nnnorm.measurable)
            (Eventually.of_forall fun x hx => ?_)
          rwa [nnnorm_indicator_eq_indicator_nnnorm, Set.indicator_of_mem hx]
        _ ≤ eLpNorm (f (ℐ C)) p μ := eLpNorm_indicator_le _

Goal state after:
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
X : Type u_2
inst✝ : TopologicalSpace X
μs : X → FiniteMeasure Ω
⊢ Continuous[inst✝, instTopologicalSpace] μs ↔ ∀ (f : Ω →ᵇ ℝ), Continuous[inst✝, _] fun x ↦ ∫ (ω : Ω), f ω ∂↑(μs x)

Tactic:
simp [continuous_iff_continuousAt, ContinuousAt, tendsto_iff_forall_integral_tendsto,
    forall_comm (α := X)]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∈ {x | C ≤ ‖f i x‖₊}
⊢ {x | C ≤ ‖f i x‖₊}.indicator (f i) x = {x | C ≤ ‖g i x‖₊}.indicator (g i) x

Tactic:
Set.indicator_of_mem hfx,

Goal state after:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∈ {x | C ≤ ‖f i x‖₊}
⊢ f i x = {x | C ≤ ‖g i x‖₊}.indicator (g i) x
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : PseudoMetrizableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
μs : ι → Measure Ω
h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i ↦ (μs i) E) L (𝓝 (μ E))
F : Set Ω
F_closed : IsClosed[inst✝³] F
this : PseudoMetricSpace Ω := pseudoMetrizableSpacePseudoMetric Ω
h✝ : L.NeBot
ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0
rs : ℕ → ℝ := Classical.choose ex
rs_lim : Tendsto rs atTop (𝓝 0)
rs_pos : ∀ (n : ℕ), 0 < rs n
rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0
Fthicks_open : ∀ (n : ℕ), IsOpen[inst✝³] (Metric.thickening (rs n) F)
key : ∀ (n : ℕ), Tendsto (fun i ↦ (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))
ε : ℝ≥0
ε_pos : 0 < ε
⊢ μ F < ∞ → limsup (fun i ↦ (μs i) F) L ≤ μ F + ↑ε

Tactic:
μF_finite

Goal state after:
case inr
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : PseudoMetrizableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
μs : ι → Measure Ω
h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i ↦ (μs i) E) L (𝓝 (μ E))
F : Set Ω
F_closed : IsClosed[inst✝³] F
this : PseudoMetricSpace Ω := pseudoMetrizableSpacePseudoMetric Ω
h✝ : L.NeBot
ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0
rs : ℕ → ℝ := Classical.choose ex
rs_lim : Tendsto rs atTop (𝓝 0)
rs_pos : ∀ (n : ℕ), 0 < rs n
rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0
Fthicks_open : ∀ (n : ℕ), IsOpen[inst✝³] (Metric.thickening (rs n) F)
key : ∀ (n : ℕ), Tendsto (fun i ↦ (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))
ε : ℝ≥0
ε_pos : 0 < ε
μF_finite : μ F < ∞
⊢ limsup (fun i ↦ (μs i) F) L ≤ μ F + ↑ε
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
setsΩ : ι → Set Ω
h_meas : ∀ i ∈ S, setsΩ i ∈ (fun x ↦ {s | MeasurableSet s}) i
setsβ : (i : ι) → Set (β i) := fun i ↦ if hi_mem : i ∈ S then Exists.choose ⋯ else univ
i : ι
⊢ i ∈ S → MeasurableSet (setsβ i)

Tactic:
hi_mem

Goal state after:
α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
setsΩ : ι → Set Ω
h_meas : ∀ i ∈ S, setsΩ i ∈ (fun x ↦ {s | MeasurableSet s}) i
setsβ : (i : ι) → Set (β i) := fun i ↦ if hi_mem : i ∈ S then Exists.choose ⋯ else univ
i : ι
hi_mem : i ∈ S
⊢ MeasurableSet (setsβ i)
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
setsΩ : ι → Set Ω
h_meas : ∀ i ∈ S, setsΩ i ∈ (fun x ↦ {s | MeasurableSet s}) i
setsβ : (i : ι) → Set (β i) := fun i ↦ if hi_mem : i ∈ S then Exists.choose ⋯ else univ
h_measβ : ∀ i ∈ S, MeasurableSet (setsβ i)
i : ι
⊢ i ∈ S → setsΩ i = f i ⁻¹' setsβ i

Tactic:
hi_mem

Goal state after:
α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
setsΩ : ι → Set Ω
h_meas : ∀ i ∈ S, setsΩ i ∈ (fun x ↦ {s | MeasurableSet s}) i
setsβ : (i : ι) → Set (β i) := fun i ↦ if hi_mem : i ∈ S then Exists.choose ⋯ else univ
h_measβ : ∀ i ∈ S, MeasurableSet (setsβ i)
i : ι
hi_mem : i ∈ S
⊢ setsΩ i = f i ⁻¹' setsβ i
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
u : Set Ω
hu : MeasurableSet u
ihu : ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ u) = (κ a) t1 * (κ a) u
a : α
ha : (κ a) (t1 ∩ u) = (κ a) t1 * (κ a) u
⊢ (κ a) t1 - (κ a) t1 * (κ a) u = (κ a) t1 * (1 - (κ a) u)

Tactic:
ENNReal.mul_sub,

Goal state after:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
u : Set Ω
hu : MeasurableSet u
ihu : ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ u) = (κ a) t1 * (κ a) u
a : α
ha : (κ a) (t1 ∩ u) = (κ a) t1 * (κ a) u
⊢ (κ a) t1 - (κ a) t1 * (κ a) u = (κ a) t1 * 1 - (κ a) t1 * (κ a) u

α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
u : Set Ω
hu : MeasurableSet u
ihu : ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ u) = (κ a) t1 * (κ a) u
a : α
ha : (κ a) (t1 ∩ u) = (κ a) t1 * (κ a) u
⊢ 0 < (κ a) u → (κ a) u < 1 → (κ a) t1 ≠ ∞