mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
t : ι → Set β
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) μ
hy : ∀ (i : ι), μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, MeasurableSet (f i)
⊢ μ[⋂ i ∈ s, f i | ⋂ i, Y i ⁻¹' t i] = ∏ i ∈ s, μ[f i | ⋂ i, Y i ⁻¹' t i]

Tactic:
convert! cond_iInter hY hindep hf (fun i _ ↦ hy _) ht using 2 with i hi

Goal state after:
case a
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
t : ι → Set β
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) μ
hy : ∀ (i : ι), μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, MeasurableSet (f i)
i : ι
hi : i ∈ s
⊢ μ[f i | ⋂ i, Y i ⁻¹' t i] = μ[f i | Y i ⁻¹' t i]
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝⁴ : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst✝³ : IsFiniteMeasure ℙ
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : HasPDF (fun ω ↦ (X ω, Y ω)) ℙ (μ.prod ν)
this✝ : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
s : Set E
t : Set F
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ) * ∫⁻ (y : F) in t, pdf Y ℙ ν y ∂ν = (∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ) * (map Y ℙ) t

Tactic:
map_eq_setLIntegral_pdf Y ℙ ν ht

Goal state after:
Ω : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝⁴ : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst✝³ : IsFiniteMeasure ℙ
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : HasPDF (fun ω ↦ (X ω, Y ω)) ℙ (μ.prod ν)
this✝ : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
s : Set E
t : Set F
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ) * ∫⁻ (y : F) in t, pdf Y ℙ ν y ∂ν =
    (∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ) * ∫⁻ (x : F) in t, pdf Y ℙ ν x ∂ν
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Var[X - Y; μ] = Var[X; μ] - 2 * cov[X, Y; μ] + Var[Y; μ]

Tactic:
rw [sub_eq_add_neg, variance_add hX hY.neg, variance_neg, covariance_neg_right]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Var[X; μ] + 2 * -cov[X, Y; μ] + Var[Y; μ] = Var[X; μ] - 2 * cov[X, Y; μ] + Var[Y; μ]
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
c : ℝ
⊢ cov[X, c • Y; μ] = c * cov[X, Y; μ]

Tactic:
rw [covariance_comm, covariance_smul_left, covariance_comm]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
c : ℝ
hc : 0 < c
⊢ μ {ω | c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤ ENNReal.ofReal Var[X; μ] / ENNReal.ofReal (c ^ 2)

Tactic:
hX.ofReal_variance_eq

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
c : ℝ
hc : 0 < c
⊢ μ {ω | c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤ eVar[X; μ] / ENNReal.ofReal (c ^ 2)
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 ω) μ
⊢ 0 ≤ ∫ (ω : Ω), (b - X ω) * (X ω - a) ∂μ

Tactic:
apply integral_nonneg_of_ae

Goal state after:
Ω : 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 ω) μ
⊢ 0 ≤ᵐ[μ] fun x ↦ (b - X x) * (X x - a)
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : Type u_3
β' : Type u_4
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
⊢ (∀ {φ : β → ℝ} {ψ : β' → ℝ},
      Measurable φ →
        Measurable ψ →
          Integrable (φ ∘ f) μ →
            Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)) →
    ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2

Tactic:
rintro h _ _ ⟨A, hA, rfl⟩ ⟨B, hB, rfl⟩

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : Type u_3
β' : Type u_4
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
h :
  ∀ {φ : β → ℝ} {ψ : β' → ℝ},
    Measurable φ →
      Measurable ψ →
        Integrable (φ ∘ f) μ →
          Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
⊢ μ (f ⁻¹' A ∩ g ⁻¹' B) = μ (f ⁻¹' A) * μ (g ⁻¹' B)
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
i : ι
⊢ MeasurableSet (g i)

Tactic:
by_cases hi : i ∈ s <;> simp only [hi, ↓reduceIte, g]

Goal state after:
case pos
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
i : ι
hi : i ∈ s
⊢ MeasurableSet (Y i ⁻¹' t i ∩ f i)

case neg
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
i : ι
hi : i ∉ s
⊢ MeasurableSet (Y i ⁻¹' t i)
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg : ∀ (i : ι), MeasurableSet (g i)
⊢ ∀ᵐ (a : α) ∂μ, (κ a)[⋂ i ∈ s, f i | ⋂ i, Y i ⁻¹' t i] = ∏ i ∈ s, (κ a)[f i | Y i ⁻¹' t i]

Tactic:
filter_upwards [hy, hindep.ae_isProbabilityMeasure, hindep.meas_iInter hYt, hindep.meas_iInter hg]
    with a hy _ hYt hg

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy✝ : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt✝ : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg✝ : ∀ (i : ι), MeasurableSet (g i)
a : α
hy : ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
a✝ : IsProbabilityMeasure (κ a)
hYt : (κ a) (⋂ i, Y i ⁻¹' t i) = ∏ i, (κ a) (Y i ⁻¹' t i)
hg : (κ a) (⋂ i, g i) = ∏ i, (κ a) (g i)
⊢ (κ a)[⋂ i ∈ s, f i | ⋂ i, Y i ⁻¹' t i] = ∏ i ∈ s, (κ a)[f i | Y i ⁻¹' t i]
Module: Mathlib.MeasureTheory.Function.Intersectivity

Goal state before:
pp: α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
hN₁ : ∀ (u : Finset ℕ), ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n)
f : ℕ → α → ℝ≥0∞ := fun n ↦ (↑(n + 1))⁻¹ • ∑ k ∈ Finset.range (n + 1), (s k).indicator 1
hfapp : ∀ (n : ℕ) (a : α), f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a
hf : ∀ (n : ℕ), Measurable (f n)
n : ℕ
a : α
⊢ ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a ≤ 1 * ↑n.succ

Tactic:
rw [mul_comm, ← nsmul_eq_mul, ← Finset.card_range n.succ]

Goal state after:
α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
hN₁ : ∀ (u : Finset ℕ), ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n)
f : ℕ → α → ℝ≥0∞ := fun n ↦ (↑(n + 1))⁻¹ • ∑ k ∈ Finset.range (n + 1), (s k).indicator 1
hfapp : ∀ (n : ℕ) (a : α), f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a
hf : ∀ (n : ℕ), Measurable (f n)
n : ℕ
a : α
⊢ ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a ≤ (Finset.range n.succ).card • 1
Module: Mathlib.MeasureTheory.Group.FoelnerFilter

Goal state before:
pp: 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
inst✝ : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u) F
g : G
s : Set X
⊢ mean μ u F (g • s) = mean μ u F s

Tactic:
by
  simpa using hfoel.mean_smul_eq_mean_smul g 1 s

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

Goal state before:

Tactic:
modularCharacterFun g * modularCharacterFun h =
      modularCharacterFun h * modularCharacterFun g := mul_comm _ _
    _ = haarScalarFactor (map (· * h) (map (· * g) ν)) (map (· * g) ν) *
      modularCharacterFun g := by
      rw [modularCharacterFun_eq_haarScalarFactor (map (· * g) ν) _]
    _ = haarScalarFactor (map (· * h) (map (· * g) ν)) (map (· * g) ν) *
      haarScalarFactor (map (· * g) ν) ν := rfl
    _ = haarScalarFactor (map (· * (g * h)) ν) ν := by simp only [map_map mul_h_meas mul_g_meas,
      comp_mul_right, ← haarScalarFactor_eq_mul]

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

Goal state before:
pp: p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ (∫ (x : ℝ) in Ioi 0, x * |x| ^ q * rexp (-|x| ^ p)) * ∫ (x : ℝ) in Ioo (-π) π, 1 =
    2 * π * ∫ (x : ℝ) in Ioi 0, x * |x| ^ q * rexp (-|x| ^ p)

Tactic:
simp_rw [integral_const, measureReal_restrict_apply MeasurableSet.univ, Set.univ_inter,
        volume_real_Ioo_of_le (a := -π) (b := π) (by linarith [pi_nonneg]),
        sub_neg_eq_add, ← two_mul, smul_eq_mul, mul_one, mul_comm]

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

Goal state before:
pp: p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ 2 * π * ∫ (x : ℝ) in Ioi 0, x ^ (q + 1) * rexp (-x ^ p) = 2 * π / p * Real.Gamma ((q + 2) / p)

Tactic:
rw [_root_.integral_rpow_mul_exp_neg_rpow (by linarith) (by linarith), add_assoc,
        one_add_one_eq_two]

Goal state after:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ 2 * π * (1 / p * Real.Gamma ((q + 2) / p)) = 2 * π / p * Real.Gamma ((q + 2) / p)
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ (∫ (x : ℝ) in Ioi 0, x * |x| ^ q * rexp (-b * |x| ^ p)) * ∫ (x : ℝ) in Ioo (-π) π, 1 =
    2 * π * ∫ (x : ℝ) in Ioi 0, x * |x| ^ q * rexp (-b * |x| ^ p)

Tactic:
simp_rw [integral_const, measureReal_restrict_apply MeasurableSet.univ, Set.univ_inter,
        volume_real_Ioo_of_le (a := -π) (b := π) (by linarith [pi_nonneg]),
        sub_neg_eq_add, ← two_mul, smul_eq_mul, mul_one, mul_comm]

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

Goal state before:
pp: case mpr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun x ↦ ↑(f x) • g x) =ᵐ[μ] g'
⊢ AEMeasurable g (μ.withDensity fun x ↦ ↑(f x))

Tactic:
refine ⟨fun x => (f x : ℝ)⁻¹ • g' x, hf.coe_nnreal_real.inv.smul g'meas, ?_⟩

Goal state after:
case mpr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun x ↦ ↑(f x) • g x) =ᵐ[μ] g'
⊢ g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] fun x ↦ (↑(f x))⁻¹ • g' x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / ↑N
ak : ℕ → ℝ := fun k ↦ a + ↑k * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + ↑N * h
⊢ |trapezoidal_error f N a b| ≤ (b - a) ^ 3 * ζ / (12 * ↑N ^ 2)

Tactic:
hb,

Goal state after:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / ↑N
ak : ℕ → ℝ := fun k ↦ a + ↑k * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + ↑N * h
⊢ |trapezoidal_error f N a (a + ↑N * h)| ≤ (a + ↑N * h - a) ^ 3 * ζ / (12 * ↑N ^ 2)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: case refine_1
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / ↑N
ak : ℕ → ℝ := fun k ↦ a + ↑k * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + ↑N * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
h5 :
  EqOn (_root_.derivWithin f (Set.Icc a b)) (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
h6 :
  EqOn (iteratedDerivWithin 2 f (Set.Icc a b)) (iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
h7 : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ
x : ℝ
hx : x ∈ Set.Icc (ak k) (ak (k + 1))
⊢ _root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))) x = _root_.derivWithin f (Set.Icc a b) x

Tactic:
exact derivWithin_subset h3 (uniqueDiffOn_Icc h4 x hx) (h_df x (h3 hx))

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : ↑K ⊆ interior ↑i), ↑(rieszContentAux Λ i)
this : b < ∞
ε : ℝ≥0
hε : 0 < ↑ε
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, 1 ≤ f x
hfle : Λ f < rieszContentAux Λ K + (↑ε).toNNReal
⊢ ↑b.toNNReal ≤ ↑(sInf (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x})) + ↑ε

Tactic:
rw [rieszContentAux, Real.toNNReal_of_nonneg hε.le, ← NNReal.coe_lt_coe] at hfle

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : ↑K ⊆ interior ↑i), ↑(rieszContentAux Λ i)
this : b < ∞
ε : ℝ≥0
hε : 0 < ↑ε
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, 1 ≤ f x
hfle : ↑(Λ f) < ↑(sInf (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x}) + NNReal.mk ↑ε ⋯)
⊢ ↑b.toNNReal ≤ ↑(sInf (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x})) + ↑ε
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: case refine_2
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
hX : #X < 𝔠
x✝ : X
s : Set X
hxs✝ : x✝ ∈ s
hs : IsOpen[inst✝¹] s
f : X → ↑I
hfc : Continuous[inst✝¹, _] f
hf₀ : f x✝ = 0
hf₁ : EqOn f 1 sᶜ
R : Set ↑I := range f
hR : #↑R < #↑I
r : ↑I
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r
x : X
hxs : x ∉ s
⊢ f x ∉ Iio r

Tactic:
simpa [hf₁ hxs] using le_one'

Goal state after:
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
this : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
⊢ μ (⋃ j, E j) = ∑ i, μ (E i)

Tactic:
rw [measure_iUnion (fun m n hmn ↦ hE.2.1 trivial trivial hmn) hE.2.2.2]

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
this : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
⊢ ∑' (i : Fin N), μ (E i) = ∑ i, μ (E i)
Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_2
inst✝² : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
α' : Type u_3
inst✝¹ : MeasurableSpace α'
β' : Type u_4
inst✝ : MeasurableSpace β'
f : α → α'
g : β → β'
f_mble : Measurable f
g_mble : Measurable g
⊢ (Measure.map f ↑μ).prod (Measure.map g ↑ν) = Measure.map (Prod.map f g) ((↑μ).prod ↑ν)

Tactic:
Measure.map_prod_map _ _ f_mble g_mble

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_2
inst✝² : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
α' : Type u_3
inst✝¹ : MeasurableSpace α'
β' : Type u_4
inst✝ : MeasurableSpace β'
f : α → α'
g : β → β'
f_mble : Measurable f
g_mble : Measurable g
⊢ Measure.map (Prod.map f g) ((↑μ).prod ↑ν) = Measure.map (Prod.map f g) ((↑μ).prod ↑ν)
Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_2
inst✝² : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
α' : Type u_3
inst✝¹ : MeasurableSpace α'
β' : Type u_4
inst✝ : MeasurableSpace β'
f : α → α'
g : β → β'
f_mble : Measurable f
g_mble : Measurable g
⊢ (Measure.map f ↑μ).prod (Measure.map g ↑ν) = Measure.map (Prod.map f g) ((↑μ).prod ↑ν)

Tactic:
Measure.map_prod_map _ _ f_mble g_mble

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
β : Type u_2
inst✝² : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
α' : Type u_3
inst✝¹ : MeasurableSpace α'
β' : Type u_4
inst✝ : MeasurableSpace β'
f : α → α'
g : β → β'
f_mble : Measurable f
g_mble : Measurable g
⊢ Measure.map (Prod.map f g) ((↑μ).prod ↑ν) = Measure.map (Prod.map f g) ((↑μ).prod ↑ν)
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ∞
μ : ProbabilityMeasure Ω
t : ℝ
⊢ Tendsto (fun a ↦ ↑μ (thickening a {a | t ≤ f a})) (𝓝[>] 0) (𝓝 (↑μ {a | t ≤ f a}))

Tactic:
apply tendsto_measure_thickening_of_isClosed ?_ ?_

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ∞
μ : ProbabilityMeasure Ω
t : ℝ
⊢ ∃ R > 0, ↑μ (thickening R {a | t ≤ f a}) ≠ ∞

Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ∞
μ : ProbabilityMeasure Ω
t : ℝ
⊢ IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] {a | t ≤ f a}