mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim : Tendsto νs L (𝓝 ν)
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
⊢ Tendsto (fun i ↦ (νs i).map ⋯) L (𝓝 (ν.map ⋯))

Tactic:
rw [ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto] at lim ⊢

Goal state after:
Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
ι : Type u_3
L : Filter ι
νs : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
lim : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (ω : Ω), ↑(f ω) ∂↑(νs i)) L (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂↑ν))
f : Ω → Ω'
f_cont : Continuous[inst✝³, inst✝¹] f
⊢ ∀ (f_1 : Ω' →ᵇ ℝ≥0),
    Tendsto (fun i ↦ ∫⁻ (ω : Ω'), ↑(f_1 ω) ∂↑((νs i).map ⋯)) L (𝓝 (∫⁻ (ω : Ω'), ↑(f_1 ω) ∂↑(ν.map ⋯)))
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 : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
⊢ eLpNorm (f i) p μ ≤ ↑(↑C * μ univ ^ p.toReal⁻¹ + 1).toNNReal

Tactic:
calc
    eLpNorm (f i) p μ ≤
        eLpNorm ({ x : α | ‖f i x‖₊ < C }.indicator (f i)) p μ +
          eLpNorm ({ x : α | C ≤ ‖f i x‖₊ }.indicator (f i)) p μ := by
      refine le_trans (eLpNorm_mono_enorm fun x => ?_) (eLpNorm_add_le
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator ((hf i).nnnorm.measurableSet_lt stronglyMeasurable_const)))
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator (stronglyMeasurable_const.measurableSet_le (hf i).nnnorm))) hp)
      rw [Pi.add_apply, Set.indicator_apply]
      split_ifs with hx
      · rw [Set.indicator_of_notMem, add_zero]
        simpa using hx
      · rw [Set.indicator_of_mem, zero_add]
        simpa using hx
    _ ≤ (C : ℝ≥0∞) * μ Set.univ ^ p.toReal⁻¹ + 1 := by
      have : ∀ᵐ x ∂μ, ‖{ x : α | ‖f i x‖₊ < C }.indicator (f i) x‖₊ ≤ C := by
        filter_upwards
        simp_rw [nnnorm_indicator_eq_indicator_nnnorm]
        exact Set.indicator_le fun x (hx : _ < _) => hx.le
      refine add_le_add (le_trans (eLpNorm_le_of_ae_bound this) ?_) (ENNReal.ofReal_one ▸ hC i)
      simp_rw [NNReal.val_eq_coe, ENNReal.ofReal_coe_nnreal, mul_comm]
      exact le_rfl
    _ = ((C : ℝ≥0∞) * μ Set.univ ^ p.toReal⁻¹ + 1 : ℝ≥0∞).toNNReal := by
      rw [ENNReal.coe_toNNReal (by finiteness)]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
m : Measure (Measure α)
inst✝ : IsProbabilityMeasure m
hm : ∀ᵐ (μ : Measure α) ∂m, IsProbabilityMeasure μ
⊢ ∫⁻ (μ : Measure α), μ univ ∂m = 1

Tactic:
isProbabilityMeasure_iff

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
m : Measure (Measure α)
inst✝ : IsProbabilityMeasure m
hm : ∀ᵐ (μ : Measure α) ∂m, μ univ = 1
⊢ ∫⁻ (μ : Measure α), μ univ ∂m = 1
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
m : Measure α
inst✝ : IsProbabilityMeasure m
f : α → Measure β
hf₀ : AEMeasurable f m
hf₁ : ∀ᵐ (μ : α) ∂m, IsProbabilityMeasure (f μ)
⊢ ∫⁻ (a : α), (f a) univ ∂m = 1

Tactic:
isProbabilityMeasure_iff

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
m : Measure α
inst✝ : IsProbabilityMeasure m
f : α → Measure β
hf₀ : AEMeasurable f m
hf₁ : ∀ᵐ (μ : α) ∂m, (f μ) univ = 1
⊢ ∫⁻ (a : α), (f a) univ ∂m = 1
Module: Mathlib.MeasureTheory.Measure.Tight

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
inst✝² : TopologicalSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed[inst✝²] s) MeasurableSet
⊢ IsTightMeasureSet {μ}

Tactic:
isTightMeasureSet_iff_exists_isCompact_measure_compl_le

Goal state after:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
inst✝² : TopologicalSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed[inst✝²] s) MeasurableSet
⊢ ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ {μ}, μ_1 Kᶜ ≤ ε
Module: Mathlib.MeasureTheory.Measure.Tight

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst✝⁴ : TopologicalSpace 𝓧
inst✝³ : TopologicalSpace 𝓨
inst✝² : MeasurableSpace 𝓨
inst✝¹ : OpensMeasurableSpace 𝓨
inst✝ : T2Space 𝓨
hS : IsTightMeasureSet S
f : 𝓧 → 𝓨
hf : Continuous[inst✝⁴, inst✝³] f
⊢ IsTightMeasureSet (Measure.map f '' S)

Tactic:
isTightMeasureSet_iff_exists_isCompact_measure_compl_le

Goal state after:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst✝⁴ : TopologicalSpace 𝓧
inst✝³ : TopologicalSpace 𝓨
inst✝² : MeasurableSpace 𝓨
inst✝¹ : OpensMeasurableSpace 𝓨
inst✝ : T2Space 𝓨
hS : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
f : 𝓧 → 𝓨
hf : Continuous[inst✝⁴, inst✝³] f
⊢ ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ Measure.map f '' S, μ Kᶜ ≤ ε
Module: Mathlib.MeasureTheory.Measure.Tight

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
inst✝¹ : TopologicalSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
inst✝ : TopologicalSpace 𝓨
μ : Set (Measure (𝓧 × 𝓨))
hμ₁ : IsTightMeasureSet (Measure.fst '' μ)
hμ₂ : IsTightMeasureSet (Measure.snd '' μ)
⊢ IsTightMeasureSet μ

Tactic:
isTightMeasureSet_iff_exists_isCompact_measure_compl_le

Goal state after:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
inst✝¹ : TopologicalSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
inst✝ : TopologicalSpace 𝓨
μ : Set (Measure (𝓧 × 𝓨))
hμ₁ : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ Measure.fst '' μ, μ_1 Kᶜ ≤ ε
hμ₂ : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ Measure.snd '' μ, μ_1 Kᶜ ≤ ε
⊢ ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ μ, μ_1 Kᶜ ≤ ε
Module: Mathlib.MeasureTheory.Measure.Tight

Goal state before:
pp: case h₂
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
inst✝¹ : TopologicalSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
inst✝ : TopologicalSpace 𝓨
μ : Set (Measure (𝓧 × 𝓨))
hμ₁ : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ Measure.fst '' μ, μ_1 Kᶜ ≤ ε
hμ₂ : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ Measure.snd '' μ, μ_1 Kᶜ ≤ ε
ε : ENNReal
hε : 0 < ε
K₁ : Set 𝓧
hK₁_compact : IsCompact K₁
hK₁_le : ∀ μ_1 ∈ Measure.fst '' μ, μ_1 K₁ᶜ ≤ ε / 2
K₂ : Set 𝓨
hK₂_compact : IsCompact K₂
hK₂_le : ∀ μ_1 ∈ Measure.snd '' μ, μ_1 K₂ᶜ ≤ ε / 2
κ : Measure (𝓧 × 𝓨)
hκ_mem : κ ∈ μ
⊢ κ (univ ×ˢ K₂ᶜ) ≤ ε / 2

Tactic:
specialize hK₂_le _ <| Set.mem_image_of_mem _ hκ_mem

Goal state after:
case h₂
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
inst✝¹ : TopologicalSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
inst✝ : TopologicalSpace 𝓨
μ : Set (Measure (𝓧 × 𝓨))
hμ₁ : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ Measure.fst '' μ, μ_1 Kᶜ ≤ ε
hμ₂ : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ Measure.snd '' μ, μ_1 Kᶜ ≤ ε
ε : ENNReal
hε : 0 < ε
K₁ : Set 𝓧
hK₁_compact : IsCompact K₁
hK₁_le : ∀ μ_1 ∈ Measure.fst '' μ, μ_1 K₁ᶜ ≤ ε / 2
K₂ : Set 𝓨
hK₂_compact : IsCompact K₂
κ : Measure (𝓧 × 𝓨)
hK₂_le : κ.snd K₂ᶜ ≤ ε / 2
hκ_mem : κ ∈ μ
⊢ κ (univ ×ˢ K₂ᶜ) ≤ ε / 2
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s : Set Ω
⊢ IndepSet s ∅ κ μ

Tactic:
by
  simp only [IndepSet, generateFrom_singleton_empty]
  exact indep_bot_right _

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
f : ι → Set Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
⊢ iIndep (fun i ↦ MeasurableSpace.comap (fun x ↦ x ∈ f i) ⊤) κ μ ↔ iIndepSet f κ μ

Tactic:
← generateFrom_singleton,

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
f : ι → Set Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
⊢ iIndep (fun i ↦ generateFrom {f i}) κ μ ↔ iIndepSet f κ μ
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
ι : Type u_2
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h_opens : ∀ (G : Set Ω), IsOpen[inst✝²] G → ↑μ G ≤ liminf (fun i ↦ ↑(μs i) G) L
⊢ Tendsto (fun i ↦ μs i) L (𝓝 μ)

Tactic:
apply Filter.tendsto_of_seq_tendsto fun u hu ↦ ?_

Goal state after:
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
ι : Type u_2
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h_opens : ∀ (G : Set Ω), IsOpen[inst✝²] G → ↑μ G ≤ liminf (fun i ↦ ↑(μs i) G) L
u : ℕ → ι
hu : Tendsto u atTop L
⊢ Tendsto ((fun i ↦ μs i) ∘ u) atTop (𝓝 μ)
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
ι : Type u_2
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h_opens : ∀ (G : Set Ω), IsOpen[inst✝²] G → μ G ≤ liminf (fun i ↦ (μs i) G) L
⊢ Tendsto (fun i ↦ μs i) L (𝓝 μ)

Tactic:
apply Filter.tendsto_of_seq_tendsto fun u hu ↦ ?_

Goal state after:
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
ι : Type u_2
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h_opens : ∀ (G : Set Ω), IsOpen[inst✝²] G → μ G ≤ liminf (fun i ↦ (μs i) G) L
u : ℕ → ι
hu : Tendsto u atTop L
⊢ Tendsto ((fun i ↦ μs i) ∘ u) atTop (𝓝 μ)
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h : ∀ (F : Set Ω), IsClosed[inst✝²] F → limsup (fun i ↦ (μs i) F) L ≤ μ F
⊢ Tendsto μs L (𝓝 μ)

Tactic:
apply Filter.tendsto_of_seq_tendsto fun u hu ↦ ?_

Goal state after:
Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h : ∀ (F : Set Ω), IsClosed[inst✝²] F → limsup (fun i ↦ (μs i) F) L ≤ μ F
u : ℕ → ι
hu : Tendsto u atTop L
⊢ Tendsto (μs ∘ u) atTop (𝓝 μ)
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case pos
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝ : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
h₀ :
  ∀ {s : (i : ι) → Set (β i)},
    (∀ (i : ι), MeasurableSet (s i)) →
      ∏ i, μ (f i ⁻¹' s i) = ∏ i, (Measure.map (f i) μ) (s i) ∧
        μ (⋂ i, f i ⁻¹' s i) = (Measure.map (fun ω i ↦ f i ω) μ) (univ.pi s)
h : Measure.map (fun ω i ↦ f i ω) μ = Measure.pi fun i ↦ Measure.map (f i) μ
S : Finset ι
s : (i : ι) → Set (β i)
hs : ∀ i ∈ S, MeasurableSet (s i)
i : ι
hiS : i ∈ S
⊢ MeasurableSet (s i)

Tactic:
simp [hiS, hs]

Goal state after:
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝ : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
h₀ :
  ∀ {s : (i : ι) → Set (β i)},
    (∀ (i : ι), MeasurableSet (s i)) →
      ∏ i, μ (f i ⁻¹' s i) = ∏ i, (Measure.map (f i) μ) (s i) ∧
        μ (⋂ i, f i ⁻¹' s i) = (Measure.map (fun ω i ↦ f i ω) μ) (univ.pi s)
h : Measure.map (fun ω i ↦ f i ω) μ = Measure.pi fun i ↦ Measure.map (f i) μ
S : Finset ι
s : (i : ι) → Set (β i)
hs : ∀ i ∈ S, MeasurableSet (s i)
i : ι
hiS : i ∉ S
⊢ MeasurableSet univ

Tactic:
simp [hiS, hs]

Goal state after:
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_7
mΩ : MeasurableSpace Ω
μ : Measure Ω
M : Type u_10
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
f g : Ω → M
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (Measure.map f μ)
σg : SigmaFinite (Measure.map g μ)
hfg : f ⟂ᵢ[μ] g
⊢ Measure.map ((fun x ↦ x.1 * x.2) ∘ fun ω ↦ (f ω, g ω)) μ = Measure.map f μ ∗ₘ Measure.map g μ

Tactic:
rw [← measurable_mul.aemeasurable.map_map_of_aemeasurable (hf.prodMk hg),
    (indepFun_iff_map_prod_eq_prod_map_map' hf hg σf σg).mp hfg, Measure.mconv]

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᵐ[volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
⊢ (fun i ↦ ‖f i‖ₑ * ENNReal.ofReal (pdf X ℙ volume i).toReal) =ᵐ[volume] fun x ↦ ‖f x * (pdf X ℙ volume x).toReal‖ₑ

Tactic:
simp_rw [← smul_eq_mul, enorm_smul, smul_eq_mul]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᵐ[volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
⊢ (fun i ↦ ‖f i‖ₑ * ENNReal.ofReal (pdf X ℙ volume i).toReal) =ᵐ[volume] fun x ↦ ‖f x‖ₑ * ‖(pdf X ℙ volume x).toReal‖ₑ
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case iSup
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a ↦ g a * T.indicator (fun x ↦ c) a
f : ℕ → Ω → ℝ≥0∞
h_meas_f : ∀ (n : ℕ), Measurable (f n)
h_mono_f : Monotone f
h_ind_f :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), f n ω * T.indicator (fun x ↦ c) ω ∂μ = (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
h_measM_f : ∀ (n : ℕ), Measurable (f n)
⊢ ⨆ n, ∫⁻ (a : Ω), f n a * T.indicator (fun x ↦ c) a ∂μ =
    ⨆ i, (∫⁻ (a : Ω), f i a ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ

Tactic:
← h_ind_f

Goal state after:
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (fun ω ↦ -X ω ^ 2) μ
hX_int₁ : Integrable (fun ω ↦ (a + b) * X ω) μ
h0 : 0 ≤ -∫ (x : Ω), (X ^ 2) x ∂μ + (a + b) * ∫ (x : Ω), X x ∂μ - a * b
⊢ Var[X; μ] ≤ (a + b) * ∫ (x : Ω), X x ∂μ - a * b - (∫ (x : Ω), X x ∂μ) ^ 2

Tactic:
rw [variance_eq_sub (memLp_of_bounded h hX.aestronglyMeasurable 2)]
      linarith

Goal state after:
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (fun ω ↦ -X ω ^ 2) μ
hX_int₁ : Integrable (fun ω ↦ (a + b) * X ω) μ
h0 : 0 ≤ -∫ (x : Ω), (X ^ 2) x ∂μ + (a + b) * ∫ (x : Ω), X x ∂μ - a * b
⊢ Var[X; μ] ≤ (b - ∫ (x : Ω), X x ∂μ) * (∫ (x : Ω), X x ∂μ - a)

Tactic:
calc
    _ ≤ (a + b) * μ[X] - a * b - μ[X] ^ 2 := by
      rw [variance_eq_sub (memLp_of_bounded h hX.aestronglyMeasurable 2)]
      linarith
    _ = (b - μ[X]) * (μ[X] - a) := by ring

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

Goal state before:
pp: ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝⁶ : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst✝⁴ : TopologicalSpace E
F : Type u_6
inst✝³ : OpensMeasurableSpace E
inst✝² : TopologicalSpace F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
g : E → F
hg : Continuous[inst✝⁴, inst✝²] g
h : TendstoInDistribution X l Z μ μ'
⊢ Tendsto (fun n ↦ ⟨Measure.map (g ∘ X n) (μ n), ⋯⟩) l (𝓝 ⟨Measure.map (g ∘ Z) μ', ⋯⟩)

Tactic:
convert! ProbabilityMeasure.tendsto_map_of_tendsto_of_continuous _ _ h.tendsto hg

Goal state after:
case e'_3
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝⁶ : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst✝⁴ : TopologicalSpace E
F : Type u_6
inst✝³ : OpensMeasurableSpace E
inst✝² : TopologicalSpace F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
g : E → F
hg : Continuous[inst✝⁴, inst✝²] g
h : TendstoInDistribution X l Z μ μ'
x✝ : ι
⊢ ⟨Measure.map (g ∘ X x✝) (μ x✝), ⋯⟩ = ProbabilityMeasure.map ⟨Measure.map (X x✝) (μ x✝), ⋯⟩ ⋯

case e'_5
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝⁶ : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst✝⁴ : TopologicalSpace E
F : Type u_6
inst✝³ : OpensMeasurableSpace E
inst✝² : TopologicalSpace F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
g : E → F
hg : Continuous[inst✝⁴, inst✝²] g
h : TendstoInDistribution X l Z μ μ'
⊢ ⟨Measure.map (g ∘ Z) μ', ⋯⟩ = ProbabilityMeasure.map ⟨Measure.map Z μ', ⋯⟩ ⋯
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: case h_bound
ι : Type u_1
E : Type u_2
Ω' : Type u_3
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝³ : IsProbabilityMeasure μ'
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst✝² : TopologicalSpace E
inst✝¹ : l.IsCountablyGenerated
inst✝ : OpensMeasurableSpace E
X : ι → Ω' → E
hX₁ : ∀ (i : ι), AEMeasurable (X i) μ'
hZ : AEMeasurable Z μ'
hX₂ : ∀ᵐ (ω : Ω') ∂μ', Tendsto (fun i ↦ X i ω) l (𝓝 (Z ω))
f : BoundedContinuousFunction E NNReal
⊢ ∀ᶠ (n : ι) in l, ∀ᵐ (a : Ω') ∂μ', ↑(f (X n a)) ≤ edist 0 f

Tactic:
simp [f.apply_le_edist_zero]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst✝¹ : MeasurableSpace Z
inst✝ : MeasurableSingletonClass Z
hg : Measurable g
x₁ x₂ : X
h : f x₁ = f x₂
s : Set Y
hs : f ⁻¹' s = g ⁻¹' {g x₂}
⊢ g x₁ ∈ {g x₂}

Tactic:
← mem_preimage,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst✝¹ : MeasurableSpace Z
inst✝ : MeasurableSingletonClass Z
hg : Measurable g
x₁ x₂ : X
h : f x₁ = f x₂
s : Set Y
hs : f ⁻¹' s = g ⁻¹' {g x₂}
⊢ x₁ ∈ g ⁻¹' {g x₂}
Module: Mathlib.MeasureTheory.Function.FactorsThrough

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst✝¹ : MeasurableSpace Z
inst✝ : MeasurableSingletonClass Z
hg : Measurable g
x₁ x₂ : X
h : f x₁ = f x₂
s : Set Y
hs : f ⁻¹' s = g ⁻¹' {g x₂}
⊢ f x₂ ∈ s

Tactic:
← mem_preimage,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst✝¹ : MeasurableSpace Z
inst✝ : MeasurableSingletonClass Z
hg : Measurable g
x₁ x₂ : X
h : f x₁ = f x₂
s : Set Y
hs : f ⁻¹' s = g ⁻¹' {g x₂}
⊢ x₂ ∈ f ⁻¹' s
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right : f i = (fun p ↦ p ⟨i, ⋯⟩) ∘ fun a j ↦ f (↑j) a
⊢ IndepFun (∏ j ∈ s, f j) (f i) κ μ

Tactic:
have h_meas_right : Measurable fun p : ({i} : Finset ι) → β =>
      p ⟨i, Finset.mem_singleton_self i⟩ := measurable_pi_apply _

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right : f i = (fun p ↦ p ⟨i, ⋯⟩) ∘ fun a j ↦ f (↑j) a
h_meas_right : Measurable fun p ↦ p ⟨i, ⋯⟩
⊢ IndepFun (∏ j ∈ s, f j) (f i) κ μ
Module: Mathlib.MeasureTheory.Integral.CircleTransform

Goal state before:
pp: R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
⊢ ∃ B ε, 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B

Tactic:
obtain ⟨⟨⟨a, b⟩, ⟨ha, hb⟩⟩, hab⟩ :=
    norm_circleTransformBoundingFunction_le hr (pos_of_mem_ball hrx).le z

Goal state after:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑⟨(a, b), ⋯⟩‖
⊢ ∃ B ε, 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : μ Eg < ∞
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : μ Ef < ∞
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : μ E < ∞
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (μ E < ∞)
hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
n : ℕ
hn : n ≥ N
hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ
hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3
hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ
hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3
hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ
hfnEcε : eLpNorm (Eᶜ.indicator (f n)) p μ ≤ ε / 3
hmfngEc : AEStronglyMeasurable (Eᶜ.indicator (f n - g)) μ
hfngEcε : eLpNorm (Eᶜ.indicator (f n - g)) p μ ≤ ε / 3 + ε / 3
⊢ eLpNorm (Eᶜ.indicator (f n - g) + E.indicator (f n - g)) p μ ≤
    eLpNorm (Eᶜ.indicator (f n - g)) p μ + eLpNorm (E.indicator (f n - g)) p μ

Tactic:
apply eLpNorm_add_le (by assumption) (by assumption) hp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b : E
h : ¬CompleteSpace F
ω : E → E →L[𝕜] F
γ : Path a b
⊢ ∫ᶜ (x : E) in γ, ω x = 0

Tactic:
simp [curveIntegral, intervalIntegral, integral, h]

Goal state after: