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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬μ univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ p.toReal)
hμs' : ¬μ s = 0
⊢ eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ + ↑C * μ s ^ (1 / p.toReal) ≤
    ENNReal.ofReal (ε / 2) + ↑C * ENNReal.ofReal (ε / (2 * ↑C))

Tactic:
grw [hC i]
      gcongr
      rwa [one_div, ENNReal.rpow_inv_le_iff (ENNReal.toReal_pos hpzero hp'),
        ENNReal.ofReal_rpow_of_pos (div_pos hε (mul_pos two_pos (NNReal.coe_pos.2 hCpos)))]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ
hp : 1 ≤ p
f : α → E
hf : Integrable (fun x ↦ ‖f x‖ ^ p) μ
⊢ ∫ (x : α), ‖μ[f | m] x‖ ^ p ∂μ ≤ ∫ (x : α), μ[fun x ↦ ‖f x‖ ^ p | m] x ∂μ

Tactic:
refine integral_mono_of_nonneg ?_ integrable_condExp (Integrable.norm_condExp_rpow_le hp hf)

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ
hp : 1 ≤ p
f : α → E
hf : Integrable (fun x ↦ ‖f x‖ ^ p) μ
⊢ 0 ≤ᵐ[μ] fun x ↦ ‖μ[f | m] x‖ ^ p
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 : Ω →ᵇ ℝ≥0), Continuous[inst✝, _] fun x ↦ ∫⁻ (ω : Ω), ↑(f ω) ∂↑(μs x)

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

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

Goal state before:
pp: Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
h : μ ≠ 0
⊢ μ.mass ≠ 0

Tactic:
rwa [μ.mass_nonzero_iff]

Goal state after:
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 : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))
f : Ω →ᵇ ℝ
f_pos : Ω →ᵇ ℝ≥0 := f.nnrealPart
_def_f_pos : f_pos = f.nnrealPart
f_neg : Ω →ᵇ ℝ≥0 := (-f).nnrealPart
_def_f_neg : f_neg = (-f).nnrealPart
⊢ Tendsto (fun i ↦ ∫ (x : Ω), ↑(f_pos x) ∂↑(μs i) - ∫ (x : Ω), ↑(f_neg x) ∂↑(μs i)) F
    (𝓝 (∫ (x : Ω), ↑(f_pos x) ∂↑μ - ∫ (x : Ω), ↑(f_neg x) ∂↑μ))

Tactic:
have tends_pos := (ENNReal.tendsto_toReal (f_pos.lintegral_lt_top_of_nnreal μ).ne).comp (h f_pos)

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))
f : Ω →ᵇ ℝ
f_pos : Ω →ᵇ ℝ≥0 := f.nnrealPart
_def_f_pos : f_pos = f.nnrealPart
f_neg : Ω →ᵇ ℝ≥0 := (-f).nnrealPart
_def_f_neg : f_neg = (-f).nnrealPart
tends_pos : Tendsto (ENNReal.toReal ∘ fun i ↦ ∫⁻ (x : Ω), ↑(f_pos x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f_pos x) ∂↑μ).toReal)
⊢ Tendsto (fun i ↦ ∫ (x : Ω), ↑(f_pos x) ∂↑(μs i) - ∫ (x : Ω), ↑(f_neg x) ∂↑(μs i)) F
    (𝓝 (∫ (x : Ω), ↑(f_pos x) ∂↑μ - ∫ (x : Ω), ↑(f_neg 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‖₊}
⊢ False

Tactic:
have : ∀ C : ℝ≥0, C • (δ : ℝ≥0∞) ^ (1 / p.toReal) ≤ eLpNorm (f (ℐ C)) p μ := by
      intro C
      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:
α : 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‖₊}
this : ∀ (C : ℝ≥0), C • ↑δ ^ (1 / p.toReal) ≤ eLpNorm (f (ℐ C)) p μ
⊢ False
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μ₁ : ∀ (ε : 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, IsCompact K ∧ ∀ μ_1 ∈ μ, μ_1 Kᶜ ≤ ε

Tactic:
obtain ⟨K₂, hK₂_compact, hK₂_le⟩ := hμ₂ (ε / 2) (by aesop)

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
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
⊢ ∃ 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₁
K₂ : Set 𝓨
hK₂_compact : IsCompact K₂
hK₂_le : ∀ μ_1 ∈ Measure.snd '' μ, μ_1 K₂ᶜ ≤ ε / 2
κ : Measure (𝓧 × 𝓨)
hK₁_le : κ.fst K₁ᶜ ≤ ε / 2
hκ_mem : κ ∈ μ
⊢ κ (K₁ᶜ ×ˢ univ) ≤ ε / 2

Tactic:
Measure.fst,

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₁
K₂ : Set 𝓨
hK₂_compact : IsCompact K₂
hK₂_le : ∀ μ_1 ∈ Measure.snd '' μ, μ_1 K₂ᶜ ≤ ε / 2
κ : Measure (𝓧 × 𝓨)
hK₁_le : (Measure.map Prod.fst κ) K₁ᶜ ≤ ε / 2
hκ_mem : κ ∈ μ
⊢ κ (K₁ᶜ ×ˢ univ) ≤ ε / 2
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 : Ω →ᵇ ℝ≥0), Continuous[inst✝, _] fun x ↦ ∫⁻ (ω : Ω), ↑(f ω) ∂↑(μs x)

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

Goal state after:
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 ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
by
  set g : ι → α → β := fun i => (hfu.1 i).choose
  have hgmeas : ∀ i, StronglyMeasurable (g i) := fun i => (Exists.choose_spec <| hfu.1 i).1
  have hgunif : UniformIntegrable g p μ := hfu.ae_eq fun i => (Exists.choose_spec <| hfu.1 i).2
  obtain ⟨C, hC⟩ := hgunif.spec' hp hp' hgmeas hε
  refine ⟨C, fun i => le_trans (le_of_eq <| eLpNorm_congr_ae ?_) (hC i)⟩
  filter_upwards [(Exists.choose_spec <| hfu.1 i).2] with x hx
  by_cases hfx : x ∈ { x | C ≤ ‖f i x‖₊ }
  · rw [Set.indicator_of_mem hfx, Set.indicator_of_mem, hx]
    rwa [Set.mem_ofPred, hx] at hfx
  · rw [Set.indicator_of_notMem hfx, Set.indicator_of_notMem]
    rwa [Set.mem_ofPred, hx] at hfx

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : iIndepSets π κ μ
⊢ ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure (κ a)

Tactic:
by
  filter_upwards [h.meas_biInter ∅ (f := fun _ ↦ Set.univ) (by simp)] with a ha
  exact ⟨by simpa using ha⟩

Goal state after:
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
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, setsΩ i) = ∏ i ∈ S, (κ a) (setsΩ i)

Tactic:
let setsβ : ∀ i : ι, Set (β i) := fun i =>
    dite (i ∈ S) (fun hi_mem => (h_meas i hi_mem).choose) fun _ => Set.univ
  have h_measβ : ∀ i ∈ S, MeasurableSet[m i] (setsβ i) := by
    intro i hi_mem
    simp_rw [setsβ, dif_pos hi_mem]
    exact (h_meas i hi_mem).choose_spec.1
  have h_preim : ∀ i ∈ S, setsΩ i = f i ⁻¹' setsβ i := by
    intro i hi_mem
    simp_rw [setsβ, dif_pos hi_mem]
    exact (h_meas i hi_mem).choose_spec.2.symm
  simp_all

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

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h₁ : IsTightMeasureSet (range (ProbabilityMeasure.toMeasure ∘ μs))
h₂ : ∀ (F : Set Ω), IsCompact F → limsup (fun x ↦ (μs x) F) L ≤ μ F
h✝ : L.NeBot
F : Set Ω
hF_closed : IsClosed[inst✝²] F
ε : ℝ≥0
hε : 0 < ε
x✝ : ↑(μ F) < ∞
K : Set Ω
hKc : IsCompact K
hK_le : ∀ μ ∈ range (ProbabilityMeasure.toMeasure ∘ μs), μ Kᶜ ≤ ↑ε
⊢ limsup (fun i ↦ ↑((μs i) (F ∩ K)) + ↑ε) L ≤ ↑(μ F) + ↑ε

Tactic:
rw [limsup_add_const _ _ _ (by isBoundedDefault) (by isBoundedDefault)]

Goal state after:
case inr
Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h₁ : IsTightMeasureSet (range (ProbabilityMeasure.toMeasure ∘ μs))
h₂ : ∀ (F : Set Ω), IsCompact F → limsup (fun x ↦ (μs x) F) L ≤ μ F
h✝ : L.NeBot
F : Set Ω
hF_closed : IsClosed[inst✝²] F
ε : ℝ≥0
hε : 0 < ε
x✝ : ↑(μ F) < ∞
K : Set Ω
hKc : IsCompact K
hK_le : ∀ μ ∈ range (ProbabilityMeasure.toMeasure ∘ μs), μ Kᶜ ≤ ↑ε
⊢ limsup (fun i ↦ ↑((μs i) (F ∩ K))) L + ↑ε ≤ ↑(μ F) + ↑ε
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : HasPDF X ℙ μ
⊢ map X ℙ = μ.withDensity ((map X ℙ).rnDeriv μ)

Tactic:
withDensity_rnDeriv_eq _ _ hX.absolutelyContinuous

Goal state after:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : HasPDF X ℙ μ
⊢ map X ℙ = map X ℙ
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : s ⊆ S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
f : ι → Set Ω := fun n ↦ if n = a then t2 else if n ∈ s then ft1 n else univ
h_f_mem : ∀ n ∈ insert a s, f n ∈ π n
h_f_mem_pi : ∀ n ∈ s, f n ∈ π n
h_t1 : t1 = ⋂ n ∈ s, f n
h_μ_t1 : ∀ᵐ (a' : α) ∂μ, (κ a') t1 = ∏ n ∈ s, (κ a') (f n)
h_t2 : t2 = f a
h_μ_inter : ∀ᵐ (a' : α) ∂μ, (κ a') (t1 ∩ t2) = ∏ n ∈ insert a s, (κ a') (f n)
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
have has : a ∉ s := fun has_mem => haS (hs_mem has_mem)

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : s ⊆ S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
f : ι → Set Ω := fun n ↦ if n = a then t2 else if n ∈ s then ft1 n else univ
h_f_mem : ∀ n ∈ insert a s, f n ∈ π n
h_f_mem_pi : ∀ n ∈ s, f n ∈ π n
h_t1 : t1 = ⋂ n ∈ s, f n
h_μ_t1 : ∀ᵐ (a' : α) ∂μ, (κ a') t1 = ∏ n ∈ s, (κ a') (f n)
h_t2 : t2 = f a
h_μ_inter : ∀ᵐ (a' : α) ∂μ, (κ a') (t1 ∩ t2) = ∏ n ∈ insert a s, (κ a') (f n)
has : a ∉ s
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : ι → Set Ω
hf : ∀ (i : ι), MeasurableSet (f i)
i : ι
⊢ ∀ t ∈ {f i}, MeasurableSet t

Tactic:
rintro t (rfl : t = _)

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : ι → Set Ω
hf : ∀ (i : ι), MeasurableSet (f i)
i : ι
⊢ MeasurableSet (f i)
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ eVar[X; μ] = ∫⁻ (ω : Ω), ENNReal.ofReal ((X ω - ∫ (x : Ω), X x ∂μ) ^ 2) ∂μ

Tactic:
simp [evariance, ← enorm_pow, Real.enorm_of_nonneg (sq_nonneg _)]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
⊢ Var[0; μ] = 0

Tactic:
by
  simp only [variance, evariance_zero, ENNReal.toReal_zero]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
inst✝⁸ : TopologicalSpace E
inst✝⁷ : ContinuousENorm E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : OpensMeasurableSpace E
inst✝⁴ : NormedAddGroup F
inst✝³ : MeasurableSpace F
inst✝² : OpensMeasurableSpace F
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), ↑c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable (fun ω ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᵐ[μ] 0
H : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ = 0
I : (fun ω ↦ ‖Y ω‖ₑ) =ᵐ[μ] 0
ω : Ω
hω : ‖Y ω‖ₑ = 0 ω
⊢ Y ω = 0 ω

Tactic:
simpa using hω

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
inst✝⁸ : TopologicalSpace E
inst✝⁷ : ContinuousENorm E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : OpensMeasurableSpace E
inst✝⁴ : NormedAddGroup F
inst✝³ : MeasurableSpace F
inst✝² : OpensMeasurableSpace F
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), ↑c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable (fun ω ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᵐ[μ] 0
I : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖X a‖ₑ ∂μ = ∞
J : (fun x ↦ ‖X x‖ₑ) ⟂ᵢ[μ] fun x ↦ ‖Y x‖ₑ
⊢ ∞ = ↑c * ∞

Tactic:
mul_top (by simpa)

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
inst✝⁸ : TopologicalSpace E
inst✝⁷ : ContinuousENorm E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : OpensMeasurableSpace E
inst✝⁴ : NormedAddGroup F
inst✝³ : MeasurableSpace F
inst✝² : OpensMeasurableSpace F
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), ↑c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable (fun ω ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'Y : ¬Y =ᵐ[μ] 0
I : ∫⁻ (ω : Ω), ‖Y ω‖ₑ ∂μ ≠ 0
H : ∫⁻ (a : Ω), ‖X a‖ₑ ∂μ = ∞
J : (fun x ↦ ‖X x‖ₑ) ⟂ᵢ[μ] fun x ↦ ‖Y x‖ₑ
⊢ ∞ = ∞
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
⊢ ∫ (a : Ω), (X a - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ ≤ ∫ (x : Ω), (X ^ 2) x ∂μ

Tactic:
rw [integral_undef]

Goal state after:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
⊢ 0 ≤ ∫ (x : Ω), (X ^ 2) x ∂μ

case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
⊢ ¬Integrable (fun a ↦ (X a - ∫ (x : Ω), X x ∂μ) ^ 2) μ
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 : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
h : IndepFun (fun a i ↦ AEMeasurable.mk (f ↑i) ⋯ a) (fun a i ↦ AEMeasurable.mk (f ↑i) ⋯ a) κ μ
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ↥S), f ↑i =ᵐ[κ a] AEMeasurable.mk (f ↑i) ⋯
a : α
ha : ∀ (i : ↥S), f ↑i =ᵐ[κ a] AEMeasurable.mk (f ↑i) ⋯
b : Ω
hb : ∀ (i : ↥S), f (↑i) b = AEMeasurable.mk (f ↑i) ⋯ b
i : ↥S
⊢ AEMeasurable.mk (f ↑i) ⋯ b = f (↑i) b

Tactic:
exact (hb i).symm

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

Goal state before:
pp: case inr.inr
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
⊢ Tendsto (fun n ↦ ∫ (ω : E), F ω ∂Measure.map (Y n) μ'') l (𝓝 (∫ (ω : E), F ω ∂Measure.map Z μ'))

Tactic:
simp_rw [Metric.tendsto_nhds, Real.dist_eq]

Goal state after:
case inr.inr
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
⊢ ∀ ε > 0, ∀ᶠ (x : ι) in l, |∫ (ω : E), F ω ∂Measure.map (Y x) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'| < ε
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 : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
h : IndepFun (fun a i ↦ AEMeasurable.mk (f ↑i) ⋯ a) (fun a i ↦ AEMeasurable.mk (f ↑i) ⋯ a) κ μ
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ↥T), f ↑i =ᵐ[κ a] AEMeasurable.mk (f ↑i) ⋯
a : α
ha : ∀ (i : ↥T), f ↑i =ᵐ[κ a] AEMeasurable.mk (f ↑i) ⋯
b : Ω
hb : ∀ (i : ↥T), f (↑i) b = AEMeasurable.mk (f ↑i) ⋯ b
i : ↥T
⊢ AEMeasurable.mk (f ↑i) ⋯ b = f (↑i) b

Tactic:
exact (hb i).symm

Goal state after:
Module: Mathlib.MeasureTheory.Group.FoelnerFilter

Goal state before:
pp: case h
G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
s : Set X
mem_Icc : ∀ᶠ (i : ι) in ↑u, μ (s ∩ F i) / μ (F i) ∈ Icc 0 1
x : ℝ≥0∞
hx : x ∈ Icc 0 1 ∧ ↑(Ultrafilter.map (fun i ↦ μ (s ∩ F i) / μ (F i)) u) ≤ 𝓝 x
⊢ Tendsto (fun i ↦ μ (s ∩ F i) / μ (F i)) (↑u) (𝓝 x)

Tactic:
exact hx.2

Goal state after: