mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

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

Tactic:
by positivity

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : Subsingleton ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬↑ε = ∞
i : ι
s : Set α
left✝ : MeasurableSet s
hμs : μ s < ∞
hfε : eLpNorm (sᶜ.indicator (f i)) p μ < ↑ε
j : ι
⊢ eLpNorm (sᶜ.indicator (f j)) p μ ≤ ↑ε

Tactic:
convert! hfε.le

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

Goal state before:
pp: G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : LocallyCompactSpace G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
μ : Measure G
inst✝ : μ.IsHaarMeasure
g : G
ν : Measure G := haar
f : G → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
f_nonneg : 0 ≤ { toFun := f, continuous_toFun := f_cont }
f_one : { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∀ (μ₀ : Measure G) [μ₀.IsHaarMeasure], ∫ (x : G), f x ∂μ₀ ≠ 0
t : ∫ (x : G), f (x * g) ∂ν = ∫ (x : G), f (x * g) ∂ν.haarScalarFactor μ • μ
r : ↑(ν.haarScalarFactor μ) / ↑(ν.haarScalarFactor μ) = 1
⊢ ↑(modularCharacterFun g) = ↑((map (fun x ↦ x * g) ν).haarScalarFactor ν)

Tactic:
borelize G

Goal state after:
G : Type u_1
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
g : G
f : G → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
f_nonneg : 0 ≤ { toFun := f, continuous_toFun := f_cont }
f_one : { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
inst✝¹ : BorelSpace G
μ : Measure G
inst✝ : μ.IsHaarMeasure
ν : Measure G := haar
int_f_ne_zero : ∀ (μ₀ : Measure G) [μ₀.IsHaarMeasure], ∫ (x : G), f x ∂μ₀ ≠ 0
t : ∫ (x : G), f (x * g) ∂ν = ∫ (x : G), f (x * g) ∂ν.haarScalarFactor μ • μ
r : ↑(ν.haarScalarFactor μ) / ↑(ν.haarScalarFactor μ) = 1
this✝ : MeasurableSpace G := borel G
⊢ ↑(modularCharacterFun g) = ↑((map (fun x ↦ x * g) ν).haarScalarFactor ν)
Module: Mathlib.MeasureTheory.Integral.CircleTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x✝ : ℝ
⊢ circleTransformDeriv R z w f x✝ = (circleMap z R x✝ - w)⁻¹ • circleTransform R z w f x✝

Tactic:
simp_rw [circleTransformDeriv, circleTransform, ← mul_smul, ← mul_assoc]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
x✝ : ℝ
⊢ ((2 * ↑π * I)⁻¹ * deriv (circleMap z R) x✝ * ((circleMap z R x✝ - w) ^ 2)⁻¹) • f (circleMap z R x✝) =
    ((circleMap z R x✝ - w)⁻¹ * (2 * ↑π * I)⁻¹ * deriv (circleMap z R) x✝ * (circleMap z R x✝ - w)⁻¹) •
      f (circleMap z R x✝)
Module: Mathlib.MeasureTheory.Group.ModularCharacter

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : LocallyCompactSpace G
g : G
⊢ 0 < modularCharacterFun g

Tactic:
borelize G

Goal state after:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : LocallyCompactSpace G
g : G
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
⊢ 0 < modularCharacterFun g
Module: Mathlib.MeasureTheory.Group.ModularCharacter

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : LocallyCompactSpace G
g h : G
⊢ modularCharacterFun (g * h) = modularCharacterFun g * modularCharacterFun h

Tactic:
borelize G

Goal state after:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : LocallyCompactSpace G
g h : G
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
⊢ modularCharacterFun (g * h) = modularCharacterFun g * modularCharacterFun h
Module: Mathlib.MeasureTheory.Integral.CircleTransform

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

Tactic:
← one_div

Goal state after:
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun w ↦ (1 / (circleMap z R w.2 - w.1)) ^ 2) (closedBall z r ×ˢ univ)
Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers

Goal state before:
pp: 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 : ℕ
⊢ 0 ≤ 1 + ↑(u n)

Tactic:
by positivity

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 c : E
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
⊢ 0 ≤ 1 / 2

Tactic:
by positivity

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
⊢ (fun x ↦ ‖deriv f x‖) ≤ᵐ[volume.restrict (Ioc a b)] B

Tactic:
← Measure.restrict_congr_set Ioo_ae_eq_Ioc,

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
⊢ (fun x ↦ ‖deriv f x‖) ≤ᵐ[volume.restrict (Ioo a b)] B
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: 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 ε
⊢ 0 ≤ ‖y - a‖ ^ (r + 1)

Tactic:
by positivity

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

Goal state before:
pp: 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 ε
⊢ 0 ≤ ‖y - a‖

Tactic:
by positivity

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

Goal state before:
pp: 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 ε
⊢ r + 1 ≠ 0

Tactic:
by positivity

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

Goal state before:
pp: 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 ε
z : E
hz : z ∈ closedBall a ‖y - a‖
⊢ 0 ≤ ‖z - a‖ ^ r

Tactic:
by positivity

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

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
h_f_int : IntervalIntegrable f volume a (a + ↑N * h)
k✝ : ℕ
hk✝ : k✝ < N
h_pos : 0 ≤ h
k : ℕ
hk : ↑k ≤ ↑N
⊢ 0 ≤ ↑k * h

Tactic:
by positivity

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
ε : ℝ≥0
εpos : 0 < ε
α : ℝ≥0
α_hyp : α < rieszContentAux Λ K + ε
f : X →C_c ℝ≥0
f_hyp : f ∈ {f | ∀ x ∈ K, 1 ≤ f x} ∧ Λ f = α
⊢ Λ f < rieszContentAux Λ K + ε

Tactic:
f_hyp.right

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
ε : ℝ≥0
εpos : 0 < ε
α : ℝ≥0
α_hyp : α < rieszContentAux Λ K + ε
f : X →C_c ℝ≥0
f_hyp : f ∈ {f | ∀ x ∈ K, 1 ≤ f x} ∧ Λ f = α
⊢ α < rieszContentAux Λ K + ε
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: case h
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : s₀ᶜ ∪ s₁ᶜ = univ
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
h : x ∈ s₀ᶜ ∨ x ∈ s₁ᶜ
h1 : x ∈ s₁ᶜ
⊢ x ∈ s₁ᶜ

Tactic:
exact h1

Goal state after:
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| ≤ ζ
⊢ DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1)))) (Set.Icc (ak k) (ak (k + 1)))

Tactic:
refine h_ddf.congr_mono (fun x hx ↦ ?_) h3

Goal state after:
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
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 ℝ
hf : ∀ (x : X), 0 ≤ f x ∧ f x ≤ 1
V : Set X
hV : tsupport ⇑f ⊆ V
this :
  (rieszContent (toNNRealLinear Λ)).measure ↑{ carrier := tsupport ⇑f, isCompact' := ⋯ } =
    (rieszContent (toNNRealLinear Λ)) { carrier := tsupport ⇑f, isCompact' := ⋯ }
⊢ ENNReal.ofReal (Λ f) ≤
    { toFun := rieszContentAux (toNNRealLinear Λ), mono' := ⋯, sup_disjoint' := ⋯, sup_le' := ⋯ }
      { carrier := tsupport ⇑f, isCompact' := ⋯ }

Tactic:
ENNReal.ofReal_eq_coe_nnreal (Λ.map_nonneg fun x ↦ (hf x).1),

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 ℝ
hf : ∀ (x : X), 0 ≤ f x ∧ f x ≤ 1
V : Set X
hV : tsupport ⇑f ⊆ V
this :
  (rieszContent (toNNRealLinear Λ)).measure ↑{ carrier := tsupport ⇑f, isCompact' := ⋯ } =
    (rieszContent (toNNRealLinear Λ)) { carrier := tsupport ⇑f, isCompact' := ⋯ }
⊢ ↑(NNReal.mk (Λ f) ⋯) ≤
    { toFun := rieszContentAux (toNNRealLinear Λ), mono' := ⋯, sup_disjoint' := ⋯, sup_le' := ⋯ }
      { carrier := tsupport ⇑f, isCompact' := ⋯ }
Module: Mathlib.MeasureTheory.Integral.TorusIntegral

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
C : ℝ
hf : ∀ (θ : Fin n → ℝ), ‖f (torusMap c R θ)‖ ≤ C
θ : Fin n → ℝ
x✝ : θ ∈ Icc 0 fun x ↦ 2 * π
⊢ 0 ≤ ∏ i, |R i|

Tactic:
by positivity

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

Goal state before:
pp: a' b' ε : ℝ
hε : 0 < ε
A : Tendsto (fun N ↦ a' / N * (b' + a' / N)) atTop (𝓝 (0 * (b' + 0)))
⊢ ∃ N, 0 < N ∧ a' / ↑N * (b' + a' / ↑N) ≤ ε

Tactic:
have B := A.comp tendsto_natCast_atTop_atTop

Goal state after:
a' b' ε : ℝ
hε : 0 < ε
A : Tendsto (fun N ↦ a' / N * (b' + a' / N)) atTop (𝓝 (0 * (b' + 0)))
B : Tendsto ((fun N ↦ a' / N * (b' + a' / N)) ∘ Nat.cast) atTop (𝓝 (0 * (b' + 0)))
⊢ ∃ N, 0 < N ∧ a' / ↑N * (b' + a' / ↑N) ≤ ε
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: case h2
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ max (#↑s) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
C : #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ≤ max (#↑s) 2 ^ ℵ₀
⊢ #↑(range fun f ↦ ⋃ n, ↑(f n)) ≤ max (#↑s) 2 ^ ℵ₀

Tactic:
· apply mk_range_le.trans
    simp only [mk_pi, prod_const, Cardinal.lift_uzero, mk_denumerable, lift_aleph0]
    have := @power_le_power_right _ _ ℵ₀ C
    rwa [← power_mul, aleph0_mul_aleph0] at this

Goal state after:
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
inst✝³ : SecondCountableTopology E
inst✝² : CompleteSpace E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ∀ (x : E), ∫ (v : E), (innerProbChar x) v ∂μ = ∫ (v : E), (innerProbChar x) v ∂ν
⊢ μ = ν

Tactic:
refine ext_of_integral_char_eq continuous_probChar probChar_ne_one (L := innerₗ E)
    ?_ ?_ h

Goal state after:
case refine_1
E : Type u_3
inst✝⁷ : MeasurableSpace E
μ ν : Measure E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : CompleteSpace E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ∀ (x : E), ∫ (v : E), (innerProbChar x) v ∂μ = ∫ (v : E), (innerProbChar x) v ∂ν
⊢ ∀ (v : E), v ≠ 0 → (innerₗ E) v ≠ 0

case refine_2
E : Type u_3
inst✝⁷ : MeasurableSpace E
μ ν : Measure E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : CompleteSpace E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ∀ (x : E), ∫ (v : E), (innerProbChar x) v ∂μ = ∫ (v : E), (innerProbChar x) v ∂ν
⊢ Continuous fun p ↦ ((innerₗ E) p.1) p.2
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u_1
t₁ t₂ : TopologicalSpace X
ht₁ : CompletelyRegularSpace X
ht₂ : CompletelyRegularSpace X
⊢ CompletelyRegularSpace X

Tactic:
apply completelyRegularSpace_iInf

Goal state after:
X : Type u_1
t₁ t₂ : TopologicalSpace X
ht₁ : CompletelyRegularSpace X
ht₂ : CompletelyRegularSpace X
⊢ ∀ (i : Bool), CompletelyRegularSpace X
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
p : ℝ≥0∞
inst✝² : Fact (1 ≤ p)
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : StrongDual ℝ (WithLp p (E × F))
⊢ ∫ (v : WithLp p (E × F)), cexp (↑(L v) * I) ∂Measure.map (toLp p) (μ.prod ν) =
    ∫ (z : E × F),
      cexp
        (↑((L ∘SL ↑(prodContinuousLinearEquiv p ℝ E F).symm ∘SL ContinuousLinearMap.inl ℝ E F) z.1) * I +
          ↑((L ∘SL ↑(prodContinuousLinearEquiv p ℝ E F).symm ∘SL ContinuousLinearMap.inr ℝ E F) z.2) * I) ∂μ.prod ν

Tactic:
← add_mul,

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
p : ℝ≥0∞
inst✝² : Fact (1 ≤ p)
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : StrongDual ℝ (WithLp p (E × F))
⊢ ∫ (v : WithLp p (E × F)), cexp (↑(L v) * I) ∂Measure.map (toLp p) (μ.prod ν) =
    ∫ (z : E × F),
      cexp
        ((↑((L ∘SL ↑(prodContinuousLinearEquiv p ℝ E F).symm ∘SL ContinuousLinearMap.inl ℝ E F) z.1) +
            ↑((L ∘SL ↑(prodContinuousLinearEquiv p ℝ E F).symm ∘SL ContinuousLinearMap.inr ℝ E F) z.2)) *
          I) ∂μ.prod ν
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T35Space X
x y : X
x_ne_y : x ≠ y
⊢ ∃ f ∈ {f | Continuous[inst✝¹, _] f}, f x ≠ f y

Tactic:
obtain ⟨f, f_cont, f_zero, f_one⟩ :=
    CompletelyRegularSpace.completely_regular x {y} isClosed_singleton x_ne_y

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T35Space X
x y : X
x_ne_y : x ≠ y
f : X → ↑I
f_cont : Continuous[inst✝¹, _] f
f_zero : f x = 0
f_one : EqOn f 1 {y}
⊢ ∃ f ∈ {f | Continuous[inst✝¹, _] f}, f x ≠ f y
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

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

Tactic:
by positivity

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
⊢ s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal

Tactic:
rw [← hs_add_r, ← ENNReal.toReal_add]

Goal state after:
case ha
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
⊢ s ≠ ∞

case hb
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
⊢ r ≠ ∞