mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case refine_2.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : Set.univ = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = Set.univ
⊢ MeasurableSet t

Tactic:
rw [← hu']

Goal state after:
case refine_2.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : Set.univ = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = Set.univ
⊢ MeasurableSet Set.univ
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case refine_2.inr.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : s n = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = s n
⊢ MeasurableSet t

Tactic:
rw [← hu']

Goal state after:
case refine_2.inr.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : s n = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = s n
⊢ MeasurableSet (s n)
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case refine_2.inr.inr.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : (s n)ᶜ = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet t

Tactic:
rw [← hu']

Goal state after:
case refine_2.inr.inr.inl
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : (s n)ᶜ = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = (s n)ᶜ
⊢ MeasurableSet (s n)ᶜ
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case refine_2.inr.inr.inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : ∅ = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = ∅
⊢ MeasurableSet t

Tactic:
rw [← hu']

Goal state after:
case refine_2.inr.inr.inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁵ : (i : ι) → TopologicalSpace (β i)
inst✝⁴ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝³ : ∀ (i : ι), BorelSpace (β i)
inst✝² : Preorder ι
inst✝¹ : (i : ι) → MulZeroOneClass (β i)
inst✝ : ∀ (i : ι), Nontrivial (β i)
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t✝ : Set Ω
n : ι
ht : MeasurableSet t✝
t : Set Ω
hn : n ≤ i
u : Set (β n)
left✝ : MeasurableSet u
hu' : ∅ = t
heq : ((s n).indicator fun x ↦ 1) ⁻¹' u = ∅
⊢ MeasurableSet ∅
Module: Mathlib.MeasureTheory.Function.Piecewise

Goal state before:
pp: ι : 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
sg : ∀ (n : ℕ), Function.Surjective (g n)
G : (n : ℕ) → IndexedPartition fun k ↦ ⋃ i ∈ g n ⁻¹' {k}, s i
x : α
y : ℕ
hy : e y = hs.index x
b : ℕ
hb : y + 1 ≤ b
⊢ e ↑((G b).index x) = hs.index x

Tactic:
have : y = (⟨y, by lia⟩ : Fin (b + 1)).1 := rfl

Goal state after:
ι : 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
sg : ∀ (n : ℕ), Function.Surjective (g n)
G : (n : ℕ) → IndexedPartition fun k ↦ ⋃ i ∈ g n ⁻¹' {k}, s i
x : α
y : ℕ
hy : e y = hs.index x
b : ℕ
hb : y + 1 ≤ b
this : y = ↑⟨y, ⋯⟩
⊢ e ↑((G b).index x) = hs.index x
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hg : UnifTight g p μ
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
⊢ UnifTight (f - g) p μ

Tactic:
by
  rw [sub_eq_add_neg]
  exact hf.add hg.neg hf_meas fun i => (hg_meas i).neg

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
ω : E → E →L[𝕜] F
inst✝ : NormedSpace ℝ E
⊢ EqOn (curveIntegralFun ω (Path.segment a b)) (fun t ↦ (ω ((lineMap a b) t)) (b - a)) (Ι 0 1)

Tactic:
uIoc_of_le zero_le_one

Goal state after:
𝕜 : 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
inst✝ : NormedSpace ℝ E
⊢ EqOn (curveIntegralFun ω (Path.segment a b)) (fun t ↦ (ω ((lineMap a b) t)) (b - a)) (Ioc 0 1)
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
inst✝ : NormedSpace ℝ E
C : ℝ
h : ∀ z ∈ ⇑(lineMap a b) '' Icc 0 1, ‖ω z‖ ≤ C
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
t : ℝ
ht : t ∈ Ι 0 1
⊢ ‖(ω ((lineMap a b) t)) (b - a)‖ ≤ C * ‖b - a‖

Tactic:
uIoc_of_le zero_le_one

Goal state after:
𝕜 : 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
inst✝ : NormedSpace ℝ E
C : ℝ
h : ∀ z ∈ ⇑(lineMap a b) '' Icc 0 1, ‖ω z‖ ≤ C
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
t : ℝ
ht : t ∈ Ioc 0 1
⊢ ‖(ω ((lineMap a b) t)) (b - a)‖ ≤ C * ‖b - a‖
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
h₁ : CurveIntegrable ω₁ γ
h₂ : CurveIntegrable ω₂ γ
⊢ curveIntegral (ω₁ + -ω₂) γ = ∫ᶜ (x : E) in γ, ω₁ x + -∫ᶜ (x : E) in γ, ω₂ x

Tactic:
curveIntegral_add h₁ h₂.neg,

Goal state after:
𝕜 : 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
h₁ : CurveIntegrable ω₁ γ
h₂ : CurveIntegrable ω₂ γ
⊢ ∫ᶜ (x : E) in γ, ω₁ x + ∫ᶜ (x : E) in γ, (-ω₂) x = ∫ᶜ (x : E) in γ, ω₁ x + -∫ᶜ (x : E) in γ, ω₂ x
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✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
⊢ ∃ δ > 0, ball a δ ∩ s ⊆ {z | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}

Tactic:
rw [← Metric.mem_nhdsWithin_iff, ofPred_and, inter_mem_iff]
    exact ⟨hω, (hω.self_of_nhdsWithin ha).eventually <| closedBall_mem_nhds _ hε⟩

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

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
h_f_c2 : ContDiffOn ℝ 2 f [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_ne : a ≠ b
⊢ DifferentiableOn ℝ (_root_.derivWithin f [[a, b]]) [[a, b]]

Tactic:
rw [← iteratedDerivWithin_one]

Goal state after:
f : ℝ → ℝ
a b : ℝ
h_f_c2 : ContDiffOn ℝ 2 f [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_ne : a ≠ b
⊢ DifferentiableOn ℝ (iteratedDerivWithin 1 f [[a, b]]) [[a, b]]
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
h✝ : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i < j
⊢ x = ⋃ n, x

Tactic:
exact (iUnion_const x).symm

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

Goal state before:
pp: α : Type u
s : Set (Set α)
⊢ {t | GenerateMeasurable s t} = generateMeasurableRec s (ω_ 1)

Tactic:
by
  apply (generateMeasurableRec_subset s _).antisymm'
  intro t ht
  induction ht with
  | basic u hu => exact self_subset_generateMeasurableRec s _ hu
  | empty => exact empty_mem_generateMeasurableRec s _
  | compl u _ IH =>
    rw [generateMeasurableRec_omega_one, mem_iUnion₂] at IH
    obtain ⟨i, hi, hi'⟩ := IH
    exact generateMeasurableRec_mono _ ((isSuccLimit_omega 1).succ_lt hi).le
      (compl_mem_generateMeasurableRec (Order.lt_succ i) hi')
  | iUnion f _ IH =>
    simp_rw [generateMeasurableRec_omega_one, mem_iUnion₂, exists_prop] at IH
    exact iUnion_mem_generateMeasurableRec IH

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

Goal state before:
pp: case inl
α : Type u
s : Set (Set α)
i : Ordinal.{v}
this : ∀ i ≤ ω_ 1, #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
hi : i ≤ ω_ 1
⊢ #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀

pp: case inr
α : Type u
s : Set (Set α)
i : Ordinal.{v}
this : ∀ i ≤ ω_ 1, #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
hi : ω_ 1 < i
⊢ #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀

Tactic:
· exact this i hi

Goal state after:
case inr
α : Type u
s : Set (Set α)
i : Ordinal.{v}
this : ∀ i ≤ ω_ 1, #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
hi : ω_ 1 < i
⊢ #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion

Goal state before:
pp: case hint
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
t : ℝ
⊢ ∫ (a : ℝ), id a ^ 2 ∂Measure.map X P ≠ 0

Tactic:
rw [integral_map]

Goal state after:
case hint
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
t : ℝ
⊢ ∫ (x : Ω), id (X x) ^ 2 ∂P ≠ 0

case hint.hφ
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
t : ℝ
⊢ AEMeasurable X P

case hint.hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
t : ℝ
⊢ AEStronglyMeasurable (fun a ↦ id a ^ 2) (Measure.map X P)
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion

Goal state before:
pp: case convert_7
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
⊢ ∫ (a : ℝ), id a ^ 2 ∂Measure.map X P ≠ 0

Tactic:
rw [integral_map]

Goal state after:
case convert_7
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
⊢ ∫ (x : Ω), id (X x) ^ 2 ∂P ≠ 0

case convert_7.hφ
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
⊢ AEMeasurable X P

case convert_7.hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
⊢ AEStronglyMeasurable (fun a ↦ id a ^ 2) (Measure.map X P)
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
⊢ ∫ (x : E), cexp (↑(L x) * I) ∂μ = ∫ (x : ℝ), cexp (↑x * I) ∂Measure.map (⇑L) μ

Tactic:
rw [integral_map]

Goal state after:
case hφ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
⊢ AEMeasurable (⇑L) μ

case hfm
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
⊢ AEStronglyMeasurable (fun x ↦ cexp (↑x * I)) (Measure.map (⇑L) μ)
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ ∫ (x : E), cexp (↑((u • L) x) * I) ∂μ = ∫ (x : ℝ), cexp (↑u * ↑x * I) ∂Measure.map (⇑L) μ

Tactic:
rw [integral_map]

Goal state after:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ ∫ (x : E), cexp (↑((u • L) x) * I) ∂μ = ∫ (x : E), cexp (↑u * ↑(L x) * I) ∂μ

case hφ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ AEMeasurable (⇑L) μ

case hfm
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ AEStronglyMeasurable (fun x ↦ cexp (↑u * ↑x * I)) (Measure.map (⇑L) μ)
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case neg
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    δ < ε → ε < ∞ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε ∧ ν B ≤ μ (thickening ε.toReal B) + ε
δ_top : ¬δ = ∞
⊢ levyProkhorovEDist μ ν ≤ δ

Tactic:
apply levyProkhorovEDist_le_of_forall_add_pos_le

Goal state after:
case neg
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    δ < ε → ε < ∞ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε ∧ ν B ≤ μ (thickening ε.toReal B) + ε
δ_top : ¬δ = ∞
⊢ ∀ (ε : ℝ≥0∞) (B : Set Ω),
    0 < ε →
      ε < ∞ →
        MeasurableSet B → μ B ≤ ν (thickening (δ + ε).toReal B) + δ + ε ∧ ν B ≤ μ (thickening (δ + ε).toReal B) + δ + ε
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case pos
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : levyProkhorovEDist μ ν = ∞
⊢ levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ

pp: case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
⊢ levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ

Tactic:
· simp [LPμν_finite]

Goal state after:
case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
⊢ levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
⊢ levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ

Tactic:
apply levyProkhorovEDist_le_of_forall_add_pos_le

Goal state after:
case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
⊢ ∀ (ε : ℝ≥0∞) (B : Set Ω),
    0 < ε →
      ε < ∞ →
        MeasurableSet B →
          μ B ≤
              κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
                  (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
                ε ∧
            κ B ≤
              μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
                  (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
                ε
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case hf
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 := ⋯
K : Set X := ⋯
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < 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 → ℝ := ⋯
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)
n : Fin N
⊢ ∀ x ∈ E n, y n - ε' ≤ f x

pp: case hfint
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 := ⋯
K : Set X := ⋯
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < 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 → ℝ := ⋯
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)
n : Fin N
⊢ IntegrableOn (fun x ↦ f x) (E n) μ

Tactic:
· intro x hx
        dsimp [y]; linarith [(hE.2.2.1 n x hx).1]

Goal state after:
case hfint
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 := ⋯
K : Set X := ⋯
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < 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 → ℝ := ⋯
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)
n : Fin N
⊢ IntegrableOn (fun x ↦ f x) (E n) μ
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)
n : Fin N
⊢ a + ε' * ↑N = b

Tactic:
by simp [field, ε']

Goal state after: