mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
⊢ (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    ((μ.withDensity fun x ↦ ENNReal.ofReal (f x)).toSignedMeasure -
        (μ.withDensity fun x ↦ ENNReal.ofReal (-f x)).toSignedMeasure)
      i

Tactic:
_root_.sub_apply,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
⊢ (∫⁻ (a : α) in i, ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α) in i, ENNReal.ofReal (-f a) ∂μ).toReal =
    (μ.withDensity fun x ↦ ENNReal.ofReal (f x)).toSignedMeasure i -
      (μ.withDensity fun x ↦ ENNReal.ofReal (-f x)).toSignedMeasure i
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    (s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure) i

Tactic:
_root_.sub_apply,

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    s.toJordanDecomposition.posPart.toSignedMeasure i - s.toJordanDecomposition.negPart.toSignedMeasure i
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
⊢ (t + μ.withDensityᵥ f) i =
    ((t.toJordanDecomposition.posPart + μ.withDensity fun x ↦ ENNReal.ofReal (f x)).toSignedMeasure -
        (t.toJordanDecomposition.negPart + μ.withDensity fun x ↦ ENNReal.ofReal (-f x)).toSignedMeasure)
      i

Tactic:
_root_.sub_apply,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
⊢ (t + μ.withDensityᵥ f) i =
    (t.toJordanDecomposition.posPart + μ.withDensity fun x ↦ ENNReal.ofReal (f x)).toSignedMeasure i -
      (t.toJordanDecomposition.negPart + μ.withDensity fun x ↦ ENNReal.ofReal (-f x)).toSignedMeasure i
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
p : ℝ≥0∞
⊢ lpNorm (fun x ↦ ‖f x‖) p μ = lpNorm f p μ

Tactic:
rw [← toReal_eLpNorm hf, ← toReal_eLpNorm (by fun_prop)]; simp

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: case neg.inr.inr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
hf : ¬AEStronglyMeasurable f μ
hp₀ : p ≠ 0
hc : c ≠ 0
⊢ lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ

Tactic:
rw [lpNorm_of_not_aestronglyMeasurable hf, lpNorm_of_not_aestronglyMeasurable fun h ↦ hf <| by
    simpa [hc] using h.smul_measure c⁻¹]

Goal state after:
case neg.inr.inr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
hf : ¬AEStronglyMeasurable f μ
hp₀ : p ≠ 0
hc : c ≠ 0
⊢ 0 = c ^ p.toReal⁻¹ • 0
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 : α), μ[fun x ↦ ‖f x‖ ^ p | m] x ∂μ ≤ ∫ (x : α), ‖f x‖ ^ p ∂μ

Tactic:
by
    apply integral_condExp_le_of_ae_nonneg
    filter_upwards with ω using by positivity

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set (α × β)
u : Set α
Hu : MeasurableSet u
v : Set β
Hv : MeasurableSet v
Heq : u ×ˢ v = s✝
⊢ Measurable fun a ↦ ((↑a.1).prod ↑a.2) s✝

Tactic:
← Heq,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set (α × β)
u : Set α
Hu : MeasurableSet u
v : Set β
Hv : MeasurableSet v
Heq : u ×ˢ v = s✝
⊢ Measurable fun a ↦ ((↑a.1).prod ↑a.2) (u ×ˢ v)
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
zero : μ.mass ≠ 0
⊢ (↑μ univ)⁻¹ * ↑μ univ = 1

Tactic:
← ENNReal.coe_ne_zero,

Goal state after:
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
zero : ↑μ.mass ≠ 0
⊢ (↑μ univ)⁻¹ * ↑μ univ = 1
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
Heval : ∀ {u : Set α} {v : Set β}, MeasurableSet u → MeasurableSet v → Measurable fun a ↦ ↑a.1 u * ↑a.2 v
s✝ : Set (α × β)
x✝¹ : Set α
Hu : MeasurableSet x✝¹
x✝ : Set β
Hv : MeasurableSet x✝
Heq : x✝¹ ×ˢ x✝ = s✝
⊢ Measurable fun a ↦ ((↑a.1).prod ↑a.2) s✝

Tactic:
← Heq,

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
Heval : ∀ {u : Set α} {v : Set β}, MeasurableSet u → MeasurableSet v → Measurable fun a ↦ ↑a.1 u * ↑a.2 v
s✝ : Set (α × β)
x✝¹ : Set α
Hu : MeasurableSet x✝¹
x✝ : Set β
Hv : MeasurableSet x✝
Heq : x✝¹ ×ˢ x✝ = s✝
⊢ Measurable fun a ↦ ((↑a.1).prod ↑a.2) (x✝¹ ×ˢ x✝)
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_1
β : Type u_3
γ : Type u_4
x✝ : MeasurableSpace Ω
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
μ : Measure Ω
⊢ f ⟂ᵢ[μ] g ↔ Indep (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) μ

Tactic:
by
  simp only [IndepFun, Indep, Kernel.IndepFun]

Goal state after:
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:
by
  refine tendsto_of_forall_isOpen_le_liminf' ?_
  rwa [← limsup_measure_closed_le_iff_liminf_measure_open_ge]

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX : ¬AEMeasurable X ℙ
⊢ pdf X ℙ μ =ᵐ[μ] 0

Tactic:
rw [pdf_def, map_of_not_aemeasurable hX]

Goal state after:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX : ¬AEMeasurable X ℙ
⊢ rnDeriv 0 μ =ᵐ[μ] 0
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x1 x2 ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun n ↦ {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ n, p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
| ∀ (i : ι), Indep (m i) m' κ μ

Tactic:
conv =>

Goal state after:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x1 x2 ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun n ↦ {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ n, p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
i : ι
| Indep (generateFrom (p i)) (generateFrom p') κ μ
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case indicator
Ω : 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
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ ∫⁻ (ω : Ω), (s' ∩ T).indicator (fun j ↦ c' * c) ω ∂μ =
    (∫⁻ (ω : Ω), s'.indicator (fun x ↦ c') ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ

Tactic:
lintegral_indicator (MeasurableSet.inter (hMf _ h_meas_s') h_meas_T),

Goal state after:
case indicator
Ω : 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
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ ∫⁻ (a : Ω) in s' ∩ T, c' * c ∂μ =
    (∫⁻ (ω : Ω), s'.indicator (fun x ↦ c') ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
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 α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
a : ι
S : Finset ι
ha_notin_S : a ∉ S
h_rec : (∀ i ∈ S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i) → ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ S, f i) = ∏ i ∈ S, (η a) (f i)
hf_m : ∀ i ∈ insert a S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i
hf_m_S : ∀ x ∈ S, MeasurableSet (f x)
p : Set (Set Ω) := piiUnionInter π ↑S
m_p : MeasurableSpace Ω := generateFrom p
hS_eq_generate : m_p = generateFrom p
h_indep : Indep m_p (m a) η μ
h : ∀ᵐ (a_1 : α) ∂μ, (η a_1) (f a ∩ ⋂ n ∈ S, f n) = (η a_1) (f a) * (η a_1) (⋂ n ∈ S, f n)
a' : α
ha' : (η a') (⋂ i ∈ S, f i) = ∏ i ∈ S, (η a') (f i)
h' : (η a') (f a ∩ ⋂ n ∈ S, f n) = (η a') (f a) * (η a') (⋂ n ∈ S, f n)
⊢ (η a') (f a ∩ ⋂ x ∈ S, f x) = ∏ i ∈ insert a S, (η a') (f i)

Tactic:
Finset.prod_insert ha_notin_S,

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
a : ι
S : Finset ι
ha_notin_S : a ∉ S
h_rec : (∀ i ∈ S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i) → ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ S, f i) = ∏ i ∈ S, (η a) (f i)
hf_m : ∀ i ∈ insert a S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i
hf_m_S : ∀ x ∈ S, MeasurableSet (f x)
p : Set (Set Ω) := piiUnionInter π ↑S
m_p : MeasurableSpace Ω := generateFrom p
hS_eq_generate : m_p = generateFrom p
h_indep : Indep m_p (m a) η μ
h : ∀ᵐ (a_1 : α) ∂μ, (η a_1) (f a ∩ ⋂ n ∈ S, f n) = (η a_1) (f a) * (η a_1) (⋂ n ∈ S, f n)
a' : α
ha' : (η a') (⋂ i ∈ S, f i) = ∏ i ∈ S, (η a') (f i)
h' : (η a') (f a ∩ ⋂ n ∈ S, f n) = (η a') (f a) * (η a') (⋂ n ∈ S, f n)
⊢ (η a') (f a ∩ ⋂ x ∈ S, f x) = (η a') (f a) * ∏ x ∈ S, (η a') (f x)
Module: Mathlib.Probability.Moments.Covariance

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

Tactic:
simp [mul_comm, covariance_const_mul_left]

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

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

Tactic:
calc cov[-X, Y; μ]
  _ = cov[(-1 : ℝ) • X, Y; μ] := by simp
  _ = -cov[X, Y; μ] := by rw [covariance_smul_left]; simp

Goal state after:
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: case σf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
M : Type u_3
inst✝³ : Monoid M
mM : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
X Y : Ω → M
hX : HasLaw X μ P
hY : HasLaw Y ν P
hXY : X ⟂ᵢ[P] Y
⊢ SigmaFinite (map X P)

pp: case σg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
M : Type u_3
inst✝³ : Monoid M
mM : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
X Y : Ω → M
hX : HasLaw X μ P
hY : HasLaw Y ν P
hXY : X ⟂ᵢ[P] Y
⊢ SigmaFinite (map Y P)

Tactic:
· rwa [hX.map_eq]

Goal state after:
case σg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
M : Type u_3
inst✝³ : Monoid M
mM : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
X Y : Ω → M
hX : HasLaw X μ P
hY : HasLaw Y ν P
hXY : X ⟂ᵢ[P] Y
⊢ SigmaFinite (map Y P)
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:
by
    convert! ProbabilityMeasure.tendsto_map_of_tendsto_of_continuous _ _ h.tendsto hg
    · simp only [ProbabilityMeasure.map, ProbabilityMeasure.coe_mk, Subtype.mk.injEq]
      rw [AEMeasurable.map_map_of_aemeasurable hg.aemeasurable (h.forall_aemeasurable _)]
    · simp only [ProbabilityMeasure.map, ProbabilityMeasure.coe_mk]
      congr
      rw [AEMeasurable.map_map_of_aemeasurable hg.aemeasurable h.aemeasurable_limit]

Goal state after:
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
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
h_right : f k = (fun p ↦ p ⟨k, ⋯⟩) ∘ fun a j ↦ f (↑j) a
h_meas_right : Measurable fun p ↦ p ⟨k, ⋯⟩
s : Finset ι := {i, j}
⊢ IndepFun (fun a ↦ (f i a, f j a)) (f k) κ μ

Tactic:
have h_left : (fun ω => (f i ω, f j ω)) = (fun p : ∀ l : s, β l =>
      (p ⟨i, Finset.mem_insert_self i _⟩,
        p ⟨j, Finset.mem_insert_of_mem (Finset.mem_singleton_self _)⟩)) ∘
        fun a (j : s) => f j a := by
    ext1 a
    simp only
    constructor

Goal state after:
α : 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
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
h_right : f k = (fun p ↦ p ⟨k, ⋯⟩) ∘ fun a j ↦ f (↑j) a
h_meas_right : Measurable fun p ↦ p ⟨k, ⋯⟩
s : Finset ι := {i, j}
h_left : (fun ω ↦ (f i ω, f j ω)) = (fun p ↦ (p ⟨i, ⋯⟩, p ⟨j, ⋯⟩)) ∘ fun a j ↦ f (↑j) a
⊢ IndepFun (fun a ↦ (f i a, f j a)) (f k) κ μ
Module: Mathlib.MeasureTheory.Function.Floor

Goal state before:
pp: R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorRing R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : OpensMeasurableSpace R
x : R
⊢ MeasurableSet (floor ⁻¹' {⌊x⌋})

Tactic:
simpa only [Int.preimage_floor_singleton] using measurableSet_Ico

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

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst✝¹ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst✝ : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Infinite ι
e : ℕ ≃ ι
g : (n : ℕ) → ι → Fin (n + 1) := fun n i ↦ if hi : ∃ m < n, i = e m then ⟨hi.choose, ⋯⟩ else Fin.last n
n : ℕ
b : Fin (n + 1)
hb : ↑b < n
⊢ (if hi : ∃ m < n, e ↑b = e m then ⟨hi.choose, ⋯⟩ else Fin.last n) = b

Tactic:
have : ∃ m < n, e b = e m := ⟨b, ⟨hb, rfl⟩⟩
      simpa only [this, Fin.ext_iff] using! e.injective this.choose_spec.2.symm

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

Goal state before:
pp: p q : ℝ
hp : 0 < p
hq : -1 < q
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 1 / p * (x✝ ^ (1 / p - 1) * ((x✝ ^ (1 / p)) ^ q * rexp (-x✝))) = 1 / p * (rexp (-x✝) * x✝ ^ (1 / p - 1 + q / p))

Tactic:
rw [← rpow_mul (le_of_lt hx), div_mul_eq_mul_div, one_mul, rpow_add hx]

Goal state after:
p q : ℝ
hp : 0 < p
hq : -1 < q
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ x✝ ^ (1 / p - 1) * (x✝ ^ (1 / p * q) * rexp (-x✝)) / p = 1 / p * (rexp (-x✝) * (x✝ ^ (1 / p - 1) * x✝ ^ (q / p)))
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
ω₁ ω₂ : E → E →L[𝕜] F
γ : Path a b
⊢ curveIntegralFun (ω₁ - ω₂) γ = curveIntegralFun ω₁ γ - curveIntegralFun ω₂ γ

Tactic:
by
  simp [sub_eq_add_neg]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
⊢ (∫ (x : ℝ) in b..a, f x) - trapezoidal_integral f N b a = -(trapezoidal_integral f N b a - ∫ (x : ℝ) in b..a, f x)

Tactic:
neg_sub

Goal state after:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
⊢ (∫ (x : ℝ) in b..a, f x) - trapezoidal_integral f N b a = (∫ (x : ℝ) in b..a, f x) - trapezoidal_integral f N b a
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: case ys
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : fderiv ℝ f =O[𝓝 a] fun x ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, ‖fderiv ℝ f x‖ ≤ C * ‖‖x - a‖ ^ r‖
ε : ℝ
hε₀ : ε > 0
hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ ‖fderiv ℝ f y‖ ≤ C * ‖‖y - a‖ ^ r‖
y : E
hy : y ∈ ball a ε
hsub : closedBall a ‖y - a‖ ⊆ ball a ε
⊢ y ∈ closedBall a ‖y - a‖

Tactic:
simp [dist_eq_norm_sub]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: case inl.inr
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t✝ : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)
k✝ k : Ordinal.{u_1}
hk : k ≤ i
t : Set α
IH : ∀ j < k, ∀ t ∈ generateMeasurableRec s j, p t
ht : ∃ x, (∃ i, ∃ (_ : i < k), x ∈ generateMeasurableRec s i) ∧ xᶜ = t
⊢ p t

Tactic:
obtain ⟨u, ⟨⟨j, hj, hj'⟩, rfl⟩⟩ := ht

Goal state after:
case inl.inr
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)
k✝ k : Ordinal.{u_1}
hk : k ≤ i
IH : ∀ j < k, ∀ t ∈ generateMeasurableRec s j, p t
u : Set α
j : Ordinal.{u_1}
hj : j < k
hj' : u ∈ generateMeasurableRec s j
⊢ p uᶜ
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: case refine_3
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ ∀ (u : Set α),
    (∃ i, ∃ (_ : i < ω_ 1), u ∈ generateMeasurableRec s i) →
      (∃ j < ω_ 1, u ∈ generateMeasurableRec s j) → ∃ i, ∃ (_ : i < ω_ 1), uᶜ ∈ generateMeasurableRec s i

Tactic:
rintro u - ⟨j, hj, hj'⟩
    exact ⟨_, (isSuccLimit_omega 1).succ_lt hj,
      compl_mem_generateMeasurableRec (Order.lt_succ j) hj'⟩

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, ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)

Tactic:
have h_ε' := (div_pos hε'.1 (Nat.cast_pos'.mpr hN))

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) ≠ ∞
h_ε' : 0 < ε' / ↑N
⊢ ∃ V, ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
n : ℕ
t : ℝ
hint : MemLp id (↑n) μ
⊢ ((iteratedFDeriv ℝ n (charFun μ) t) fun x ↦ 1) = I ^ n * ∫ (x : ℝ), ↑x ^ n * cexp (↑t * ↑x * I) ∂μ

Tactic:
iteratedFDeriv_charFun hint

Goal state after:
μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
n : ℕ
t : ℝ
hint : MemLp id (↑n) μ
⊢ I ^ n * ∫ (y : ℝ), ↑(∏ i, ⟪y, 1⟫) * cexp (↑⟪y, t⟫ * I) ∂μ = I ^ n * ∫ (x : ℝ), ↑x ^ n * cexp (↑t * ↑x * I) ∂μ
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
mE : MeasurableSpace E
μ : Measure E
t : E
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
⊢ charFun μ t = ∫ (v : E), (innerProbChar t) v ∂μ

Tactic:
simp [charFun_apply, innerProbChar_apply]

Goal state after: