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∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨C, fun i => le_trans (le_of_eq <| eLpNorm_congr_ae ?_) (hC i)⟩

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 ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
⊢ {x | C ≤ ‖f i x‖₊}.indicator (f i) =ᵐ[μ] {x | C ≤ ‖g i x‖₊}.indicator (g i)
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: case h
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω'
inst✝⁵ : TopologicalSpace Ω'
inst✝⁴ : BorelSpace Ω'
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : BorelSpace Ω
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') := {μ | μ (range f)ᶜ = 0}
A : IsEmbedding Subtype.val
μ : FiniteMeasure Ω
s : Set Ω
hs : MeasurableSet s
⊢ Function.Injective f

Tactic:
exact hf.injective

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

Goal state before:
pp: case hfi
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω'
inst✝⁵ : TopologicalSpace Ω'
inst✝⁴ : BorelSpace Ω'
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : BorelSpace Ω
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') := {μ | μ (range f)ᶜ = 0}
A : IsEmbedding Subtype.val
μ : FiniteMeasure Ω
s : Set Ω
hs : MeasurableSet s
⊢ Function.Injective f

Tactic:
exact hf.injective

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
μ : Measure Ω
⊢ iIndep m μ ↔ iIndepSets (fun x ↦ {s | MeasurableSet s}) μ

Tactic:
by
  simp only [iIndep, iIndepSets, Kernel.iIndep]

Goal state after:
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 : ι → Ω → β
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 : ∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
⊢ μ[⋂ i ∈ s, f i | ⋂ i, Y i ⁻¹' t i] = ∏ i ∈ s, μ[f i | Y i ⁻¹' t i]

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
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 : ∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val✝ : Fintype ι
⊢ μ[⋂ i ∈ s, f i | ⋂ i, Y i ⁻¹' t i] = ∏ i ∈ s, μ[f i | Y i ⁻¹' t i]
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case e'_2
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
u : Set α
h : ∫⁻ (a : α) in u, ((κ.map fun ω ↦ (f ω, g ω)) a) (s ×ˢ t) ∂μ = ∫⁻ (a : α) in u, ((κ.map f ×ₖ κ.map g) a) (s ×ˢ t) ∂μ
hu : MeasurableSet u
hμu : μ u < ⊤
ω : α
⊢ (κ ω) (f ⁻¹' s ∩ g ⁻¹' t) = ((κ.map fun ω ↦ (f ω, g ω)) ω) (s ×ˢ t)

Tactic:
rw [map_apply' _ (by fun_prop) _ (hs.prod ht), mk_preimage_prod]

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ HasPDF X ℙ μ

Tactic:
refine ⟨hX, ?_, ?_⟩

Goal state after:
case refine_1
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ (map X ℙ).HaveLebesgueDecomposition μ

case refine_2
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ map X ℙ ≪ μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
⊢ Var[X; 0] = 0

Tactic:
by simp [variance]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ cov[X, Y; μ] = ∫ (x : Ω), (X * Y) x ∂μ - (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ

Tactic:
by
   simp_rw [covariance, sub_mul, mul_sub]
   repeat rw [integral_sub]
   · simp_rw [integral_mul_const, integral_const_mul, integral_const, probReal_univ,
       one_smul]
     simp
   · exact hY.const_mul _ |>.integrable (by simp)
   · exact integrable_const _
   · exact hX.integrable_mul hY
   · exact hX.mul_const _ |>.integrable (by simp)
   · exact (hX.integrable_mul hY).sub (hX.mul_const _ |>.integrable (by simp))
   · exact (hY.const_mul _ |>.integrable (by simp)).sub (integrable_const _)

Goal state after:
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✝¹ : IsStrictOrderedRing R
inst✝ : BorelSpace R
s : Set R
hs : MeasurableSet s
⊢ MeasurableSet (Int.fract '' s)

Tactic:
by
  simp only [Int.image_fract, sub_eq_add_neg, image_add_right']
  exact MeasurableSet.iUnion fun m => (measurable_add_const _ hs).inter measurableSet_Ico

Goal state after:
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)
⊢ ∀ᵐ (a : α) ∂μ, (κ a)[⋂ i ∈ s, f i | ⋂ i, Y i ⁻¹' t i] = ∏ i ∈ s, (κ a)[f i | Y i ⁻¹' t i]

Tactic:
cases nonempty_fintype ι

Goal state after:
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 ι
⊢ ∀ᵐ (a : α) ∂μ, (κ a)[⋂ i ∈ s, f i | ⋂ i, Y i ⁻¹' t i] = ∏ i ∈ s, (κ a)[f i | Y i ⁻¹' t i]
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifTight f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬↑ε = ∞
g : Fin n → α → β := fun k ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
S : Set α
hμS : μ S ≠ ∞
hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ ↑ε
s : Set α
left✝ : MeasurableSet s
hμs : μ s < ∞
hfε : eLpNorm (sᶜ.indicator (f (Fin.last n))) p μ < ↑ε
i : Fin (n + 1)
hi : n ≤ ↑i
⊢ eLpNorm ((s ∪ S)ᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
obtain rfl : i = Fin.last n := Fin.ext (le_antisymm i.is_le hi)
      rw [compl_union, inter_comm, ← indicator_indicator]
      exact (eLpNorm_indicator_le _).trans hfε.le

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

Goal state before:
pp: case hg.hg.hf
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun i ↦ ((circleMap z R i.2 - i.1) ^ 2)⁻¹) (closedBall z r ×ˢ univ)

Tactic:
· simpa only [inv_pow] using continuousOn_prod_circle_transform_function hr

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

Goal state before:
pp: case refine_1
E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯.choose
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun n ↦ (1 + u n) • K
Z : ℕ → Set E := fun n ↦ ↑(S n) ∩ (↑L \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
⊢ Z (n + 1) ⊆ Z n

Tactic:
refine Set.inter_subset_inter_left _ (SetLike.coe_subset_coe.mpr ?_)

Goal state after:
case refine_1
E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯.choose
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun n ↦ (1 + u n) • K
Z : ℕ → Set E := fun n ↦ ↑(S n) ∩ (↑L \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
⊢ S (n + 1) ≤ S n
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
f f' : ℕ → α → β
g g' : α → β
hff' : ∀ (n : ℕ), f n =ᵐ[μ] f' n
hgg' : g =ᵐ[μ] g'
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f' n x) atTop (𝓝 (g' x))

Tactic:
have hff'' := eventually_countable_forall.mpr hff'

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
f f' : ℕ → α → β
g g' : α → β
hff' : ∀ (n : ℕ), f n =ᵐ[μ] f' n
hgg' : g =ᵐ[μ] g'
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
hff'' : ∀ᵐ (x : α) ∂μ, ∀ (i : ℕ), f i x = f' i x
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f' n x) atTop (𝓝 (g' x))
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : TendstoInMeasure μ f atTop g
ns : ℕ → ℕ
hns : Tendsto ns atTop atTop
⊢ ∃ ms, Tendsto (fun n ↦ eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)

Tactic:
obtain ⟨ms, _, hms'⟩ := TendstoInMeasure.exists_seq_tendsto_ae fun ε hε => (hfg ε hε).comp hns

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : TendstoInMeasure μ f atTop g
ns : ℕ → ℕ
hns : Tendsto ns atTop atTop
ms : ℕ → ℕ
left✝ : StrictMono ms
hms' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f (ns (ms i)) x) atTop (𝓝 (g x))
⊢ ∃ ms, Tendsto (fun n ↦ eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:

Tactic:
_ = ∫ x in Ioi (0 : ℝ) ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)) := by
      rw [← Complex.integral_comp_polarCoord_symm, polarCoord_target]
      simp_rw [Complex.norm_polarCoord_symm, smul_eq_mul]
    _ = (∫ x in Ioi (0 : ℝ), x * |x| ^ q * rexp (-|x| ^ p)) * ∫ _ in Ioo (-π) π, 1 := by
      rw [← setIntegral_prod_mul, volume_eq_prod]
      simp_rw [mul_one]
      congr! 2; ring
    _ = 2 * π * ∫ x in Ioi (0 : ℝ), x * |x| ^ q * rexp (-|x| ^ p) := by
      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]
    _ = 2 * π * ∫ x in Ioi (0 : ℝ), x ^ (q + 1) * rexp (-x ^ p) := by
      congr 1
      refine setIntegral_congr_fun measurableSet_Ioi (fun x hx => ?_)
      rw [mem_Ioi] at hx
      rw [abs_eq_self.mpr hx.le, rpow_add hx, rpow_one]
      ring
    _ = (2 * Real.pi / p) * Real.Gamma ((q + 2) / p) := by
      rw [_root_.integral_rpow_mul_exp_neg_rpow (by linarith) (by linarith), add_assoc,
        one_add_one_eq_two]
      ring

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

Goal state before:
pp: E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
f✝ : ℝ → E✝
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t

Tactic:
have hfB' : (‖deriv f ·‖) ≤ᵐ[volume.restrict (uIoc a b)] B := by
    rwa [uIoc_of_le hab, ← Measure.restrict_congr_set Ioo_ae_eq_Ioc, EventuallyLE,
        ae_restrict_iff' measurableSet_Ioo]

Goal state after:
E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
f✝ : ℝ → E✝
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun x ↦ ‖deriv f x‖) ≤ᵐ[volume.restrict (uIoc a b)] B
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
f✝ : ℝ → E✝
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun x ↦ ‖deriv f x‖) ≤ᵐ[volume.restrict (uIoc a b)] B
⊢ ∀ᵐ (t : ℝ), t ∈ Ioc a b → ‖deriv f t‖ ≤ B t

Tactic:
rwa [← ae_restrict_iff' measurableSet_Ioc, ← uIoc_of_le hab]

Goal state after:
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| ≤ ζ
g : ℝ → ℝ := fun t ↦ trapezoidal_error f 1 a t
dg : ℝ → ℝ := fun t ↦ 1 / 2 * (f a + f t) + (t - a) / 2 * _root_.derivWithin f (Set.Icc a b) t - f t
ddg : ℝ → ℝ := fun t ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
h_dg : ∀ y ∈ Set.Icc a b, HasDerivWithinAt g (dg y) (Set.Icc a b) y
h_ddg : ∀ y ∈ Set.Icc a b, HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
bound_ddg : ∀ x ∈ Set.Icc a b, |ddg x| ≤ ζ / 2 * (x - a) ^ 1
key :
  ∀ {φ φ' : ℝ → ℝ},
    (∀ x ∈ Set.Icc a b, HasDerivWithinAt φ (φ' x) (Set.Icc a b) x) →
      φ a = 0 →
        ∀ {c : ℝ} {n : ℕ},
          (∀ t ∈ Set.Icc a b, |φ' t| ≤ c * (t - a) ^ n) → ∀ t ∈ Set.Icc a b, |φ t| ≤ c / (↑n + 1) * (t - a) ^ (n + 1)
⊢ ζ / 2 / (↑1 + 1) / (↑(1 + 1) + 1) * (b - a) ^ (1 + 1 + 1) = ζ / 12 * (b - a) ^ 3

Tactic:
by ring_nf

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
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
K : Set X
hK : IsCompact K
h : tsupport ⇑f ⊆ K
ε : ℝ≥0
hε : 0 < ε
g : X →C_c ℝ≥0
hg :
  (∀ x ∈ { carrier := K, isCompact' := hK }, 1 ≤ g x) ∧ Λ g < rieszContentAux Λ { carrier := K, isCompact' := hK } + ε
⊢ Λ f ≤ Λ g

Tactic:
apply monotone_of_nnreal Λ

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
K : Set X
hK : IsCompact K
h : tsupport ⇑f ⊆ K
ε : ℝ≥0
hε : 0 < ε
g : X →C_c ℝ≥0
hg :
  (∀ x ∈ { carrier := K, isCompact' := hK }, 1 ≤ g x) ∧ Λ g < rieszContentAux Λ { carrier := K, isCompact' := hK } + ε
⊢ f ≤ g
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
inst✝ : R0Space X
x : X
⊢ ∀ (K : Set X), IsClosed[inst✝²] K → x ∉ K → ∃ f, Continuous[inst✝², _] f ∧ f x = 0 ∧ EqOn f 1 K

Tactic:
K

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
inst✝ : R0Space X
x : X
K : Set X
⊢ IsClosed[inst✝²] K → x ∉ K → ∃ f, Continuous[inst✝², _] f ∧ f x = 0 ∧ EqOn f 1 K
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_3
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : BorelSpace E
r t : E
⊢ charFun (Measure.map (fun x ↦ x + r) μ) t = charFun μ t * cexp (↑⟪r, t⟫ * I)

Tactic:
rw [charFun_apply, charFun_apply, integral_map (by fun_prop) (by fun_prop),
    ← integral_mul_const]

Goal state after:
E : Type u_3
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : BorelSpace E
r t : E
⊢ ∫ (x : E), cexp (↑⟪x + r, t⟫ * I) ∂μ = ∫ (a : E), cexp (↑⟪a, t⟫ * I) * cexp (↑⟪r, t⟫ * I) ∂μ
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ i, t i
x : X
⊢ ∀ (K : Set X), IsOpen[⨅ i, t i] K → x ∈ K → ∃ f, Continuous[⨅ i, t i, _] f ∧ f x = 0 ∧ EqOn f 1 Kᶜ

Tactic:
K

Goal state after:
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ i, t i
x : X
K : Set X
⊢ IsOpen[⨅ i, t i] K → x ∈ K → ∃ f, Continuous[⨅ i, t i, _] f ∧ f x = 0 ∧ EqOn f 1 Kᶜ
Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝⁹ : Group G
inst✝⁸ : AddCommGroup A
inst✝⁷ : DistribMulAction G A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalAddGroup A
inst✝⁴ : LocallyCompactSpace A
inst✝³ : ContinuousConstSMul G A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
g : G
⊢ μ.addHaarScalarFactor ((DomMulAct.mk g)⁻¹ • μ) = (distribHaarChar A) g

Tactic:
rw [← addHaarScalarFactor_domSMul _ _ (DomMulAct.mk g)]
  simp_rw [← mul_smul, mul_inv_cancel, one_smul]
  exact addHaarScalarFactor_smul_eq_distribHaarChar ..

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

Goal state before:
pp: Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
P : ProbabilityMeasure Ω
⊢ ∀ ε > 0, ∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist (ofMeasure x) (ofMeasure P) < ε

Tactic:
intro ε ε_pos

Goal state after:
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
⊢ ∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist (ofMeasure x) (ofMeasure P) < ε
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : ⋃ n, Es n = univ
Es_disjoint : Pairwise fun n m ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : {J | J ⊆ Iio N}.Finite
⊢ ∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist (ofMeasure x) (ofMeasure P) < ε

Tactic:
set Gs := (fun (J : Set ℕ) ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}

Goal state after:
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : ⋃ n, Es n = univ
Es_disjoint : Pairwise fun n m ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : {J | J ⊆ Iio N}.Finite
Gs : Set (Set Ω) := (fun J ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J | J ⊆ Iio N}
⊢ ∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist (ofMeasure x) (ofMeasure P) < ε
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

Goal state before:
pp: case e_a
μ : Measure ℝ
r : ℝ
inst✝ : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (fun x ↦ sinc (r * x)) μ
⊢ 2 = r * r⁻¹ * 2

Tactic:
rw [mul_inv_cancel₀ (by positivity), one_mul]

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

Goal state before:
pp: μ : Measure ℝ
r : ℝ
inst✝ : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (fun x ↦ sinc (r * x)) μ
⊢ 2 * ‖∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ‖ =
    2⁻¹ * r * ‖2 * (↑r)⁻¹ + 2 * ↑r⁻¹ - 2 * (2 * ↑r⁻¹) * ↑(∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ)‖

Tactic:
by
    norm_cast
    rw [← two_mul, mul_assoc 2, ← mul_sub, norm_mul, Real.norm_ofNat, ← mul_assoc,
      ← mul_one_sub, norm_mul, Real.norm_of_nonneg (r := 2 * r⁻¹) (by positivity), ← mul_assoc]
    congr
    · ring_nf
      rw [mul_inv_cancel₀ (by positivity), one_mul]
    · rw [integral_sub (integrable_const _) (integrable_sinc_const_mul _)]
      simp

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

Goal state before:
pp: case e'_4
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
L : StrongDual ℝ E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (Measure.map (⇑L) μ)
x : ℝ
⊢ charFunDual μ (x • L) = charFun (Measure.map (⇑L) μ) x

Tactic:
· rw [charFun_map_eq_charFunDual_smul]

Goal state after: