mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.CircleTransform

Goal state before:
pp: R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑x‖

Tactic:
by
  have cts := continuousOn_norm_circleTransformBoundingFunction hr z
  have comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]]) := by
    apply_rules [IsCompact.prod, ProperSpace.isCompact_closedBall z r, isCompact_uIcc]
  have none : (closedBall z r ×ˢ [[0, 2 * π]]).Nonempty :=
    (nonempty_closedBall.2 hr').prod nonempty_uIcc
  have := IsCompact.exists_isMaxOn comp none (cts.mono <| prod_mono_right (subset_univ _))
  simpa [isMaxOn_iff] using this

Goal state after:
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
⊢ toNNRealLinear (toRealPositiveLinear Λ) = Λ

Tactic:
by
  ext f
  simp

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

Goal state before:
pp: case e_a
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
x : ℝ
hx : 0 < x
⊢ x * |x| ^ q * rexp (-|x| ^ p) = x ^ (q + 1) * rexp (-x ^ p)

Tactic:
abs_eq_self.mpr hx.le,

Goal state after:
case e_a
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
x : ℝ
hx : 0 < x
⊢ x * x ^ q * rexp (-x ^ p) = x ^ (q + 1) * rexp (-x ^ p)
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e_a
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x : ℝ
hx : 0 < x
⊢ x * |x| ^ q * rexp (-b * |x| ^ p) = x ^ (q + 1) * rexp (-b * x ^ p)

Tactic:
abs_eq_self.mpr hx.le,

Goal state after:
case e_a
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x : ℝ
hx : 0 < x
⊢ x * x ^ q * rexp (-b * x ^ p) = x ^ (q + 1) * rexp (-b * x ^ p)
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
⊢ |trapezoidal_error f 1 a b| ≤ ζ / 12 * (b - a) ^ 3

Tactic:
let dg (t : ℝ) := (1 / 2) * (f a + f t) + ((t - a) / 2) * (derivWithin f (Icc a b) t) - f t

Goal state after:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
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
⊢ |trapezoidal_error f 1 a b| ≤ ζ / 12 * (b - a) ^ 3
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

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

Tactic:
refine ((le_iff_forall_one_lt_le_mul₀ (zero_le (a := Λ f))).mpr fun α hα ↦ ?_).trans hfle.le

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : ↑K ⊆ interior ↑i), ↑(rieszContentAux Λ i)
this : b < ∞
ε : ℝ≥0
hε : 0 < ↑ε
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, 1 ≤ f x
hfle : ↑(Λ f) < ↑(sInf (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x}) + NNReal.mk ↑ε ⋯)
α : ℝ≥0
hα : 1 < α
⊢ b.toNNReal ≤ Λ f * α
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
K : Set X
hK : IsCompact K
hfK : ∀ x ∈ K, f x = 1
p : NNReal
hp : ENNReal.ofReal (Λ f) = ENNReal.ofReal ↑p
⊢ (rieszContent (toNNRealLinear Λ)).toFun { carrier := K, isCompact' := hK } ≤ p

Tactic:
ENNReal.ofReal_eq_ofReal_iff (Λ.map_nonneg hf) NNReal.zero_le_coe

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
K : Set X
hK : IsCompact K
hfK : ∀ x ∈ K, f x = 1
p : NNReal
hp : Λ f = ↑p
⊢ (rieszContent (toNNRealLinear Λ)).toFun { carrier := K, isCompact' := hK } ≤ p
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f : X →C_c ℝ≥0
⊢ ∫ (x : X), ↑(f x) ∂rieszMeasure Λ = ↑(Λ f)

Tactic:
← eq_toRealPositiveLinear_toReal Λ f,

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f : X →C_c ℝ≥0
⊢ ∫ (x : X), ↑(f x) ∂rieszMeasure Λ = (toRealPositiveLinear Λ) f.toReal
Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
β : Type u_2
inst✝¹ : MeasurableSpace β
f : α → α
g : α → β
inst✝ : MeasurableSingletonClass β
h : Measurable g
x : α
⊢ x ∈ f ⁻¹' g ⁻¹' {g x}

Tactic:
rw [(h <| measurableSet_singleton (g x)).2, Set.mem_preimage, Set.mem_singleton_iff]

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
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : μ.outerMeasure E ≠ ∞
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, f x < c
⊢ ∃ V, E ⊆ ↑V ∧ (∀ x ∈ V, f x < c) ∧ μ.measure ↑V ≤ μ.measure E + ENNReal.ofReal ε

Tactic:
by
  have hε' := ne_of_gt <| Real.toNNReal_pos.mpr hε
  obtain ⟨V₁ : Opens X, hV₁⟩ := Content.outerMeasure_exists_open μ hμ hε'
  let V₂ : Opens X := ⟨(f ⁻¹' Iio c), IsOpen.preimage f.1.2 isOpen_Iio⟩
  use V₁ ⊓ V₂
  refine ⟨subset_inter hV₁.1 hfE, ?_, ?_⟩
  · intro x hx
    suffices ∀ x ∈ V₂.carrier, f x < c from this x (mem_of_mem_inter_right hx)
    exact fun _ a ↦ a
  · calc
      _ ≤ μ.measure V₁ := by simp [measure_mono]
      _ = μ.outerMeasure V₁ := Content.measure_apply μ (V₁.2.measurableSet)
      _ ≤ μ.outerMeasure E + ε.toNNReal := hV₁.2
      _ = _ := by rw [Content.measure_apply μ hμ', ENNReal.ofNNReal_toNNReal]

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)
⊢ Λ f ≤ ∫ (x : X), f x ∂rieszMeasure Λ + ε

Tactic:
let y : Fin N → ℝ := fun n ↦ a + ε' * (n + 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 ℝ
μ : 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)
⊢ Λ f ≤ ∫ (x : X), f x ∂rieszMeasure Λ + ε
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,
    (∀ (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)

Tactic:
have : tsupport f ⊆ ⋃ n, (V n).carrier := calc
      _ = ⋃ j, E j := hE.1
      _ ⊆ _ := by gcongr with n; exact (hV n).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 ℝ
μ : 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)
this : tsupport ⇑f ⊆ ⋃ n, (V n).carrier
⊢ ∃ g,
    (∀ (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)
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
hint : MemLp id 2 (Measure.map X P)
t : ℝ
⊢ taylorWithinEval (charFun (Measure.map X P)) 2 univ 0 t =
    1 + ↑(∫ (x : Ω), X x ∂P) * ↑t * I - ↑(∫ (x : Ω), (X ^ 2) x ∂P) * ↑t ^ 2 / 2

Tactic:
by
  have : IsProbabilityMeasure (P.map X) := Measure.isProbabilityMeasure_map hX
  convert! taylorWithinEval_charFun_zero hint t with x
  simp only [Pi.pow_apply, Nat.reduceAdd, Finset.sum_range_succ, Finset.range_one,
    Finset.sum_singleton, Nat.factorial_zero, Nat.cast_one, inv_one, pow_zero, mul_one,
    integral_const, probReal_univ, smul_eq_mul, ofReal_one, Nat.factorial_one, pow_one, one_mul,
    Nat.factorial_two, Nat.cast_ofNat]
  rw [integral_map, integral_map]
  any_goals fun_prop
  simp [field]
  ring

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
t : E
⊢ ‖VectorFourier.fourierIntegral probChar μ (innerₗ E) 1 (-t)‖ ≤ μ.real Set.univ

Tactic:
exact (VectorFourier.norm_fourierIntegral_le_integral_norm _ _ _ _ _).trans_eq (by simp)

Goal state after:
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
I' : Finset ι
V U : ↥I' → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
hU : ∀ (i : ↥I'), IsOpen[t ↑i] (U i)
hxU : ∀ (i : ↥I'), x ∈ U i
⊢ ∃ f, Continuous[⨅ i, t i, _] f ∧ f x = 0 ∧ EqOn f 1 (⋂ i, V i)ᶜ

Tactic:
replace hU := fun (i : ↥I') =>
    @CompletelyRegularSpace.completely_regular_isOpen _ (t i) (ht i) x (U i) (hU i) (hxU i)

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
I' : Finset ι
V U : ↥I' → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
hxU : ∀ (i : ↥I'), x ∈ U i
hU : ∀ (i : ↥I'), ∃ f, Continuous[t ↑i, _] f ∧ f x = 0 ∧ EqOn f 1 (U i)ᶜ
⊢ ∃ f, Continuous[⨅ i, t i, _] f ∧ f x = 0 ∧ EqOn f 1 (⋂ i, V i)ᶜ
Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi

Goal state before:
pp: case h
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
inst✝³ : (i : ι) → TopologicalSpace (α i)
inst✝² : ∀ (i : ι), SecondCountableTopology (α i)
inst✝¹ : ∀ (i : ι), PseudoMetrizableSpace (α i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) := ⋯
this✝ : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := ⋯
u : Set ((i : ι) → α i)
u_open : IsOpen[Pi.topologicalSpace] u
x : (i : ι) → α i
xu : x ∈ u
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ u
r : ι → ℝ
rpos : ∀ (i : ι), r i ∈ Ioo 0 ε
hr : ∀ (i : ι), ↑(μ i) (frontier (thickening (r i) {x i})) = 0
i : ι
hi : i ∈ univ
⊢ r i ≤ ε

Tactic:
exact (rpos i).2.le

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
μ ν : Measure X
inst✝³ : LocallyCompactSpace X
inst✝² : ν.OuterRegular
inst✝¹ : IsFiniteMeasureOnCompacts ν
inst✝ : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : ν K < ∞
hνK : ν K ≠ ∞
hμK : μ K ≠ ∞
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst✝⁷] V
pV3 : ν V ≤ ν K + ↑ε
VltTop : ν V < ∞
⊢ ∃ f, EqOn (⇑f) 1 K ∧ tsupport ⇑f ⊆ V ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
obtain ⟨f, hf1, hf2, hf3⟩ := exists_continuousMap_one_of_isCompact_subset_isOpen hK pV2 pV1
    exact ⟨⟨f, hasCompactSupport_def.mpr hf2⟩, hf1, hf3⟩

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

Goal state before:
pp: case e_f
μ : Measure ℝ
r : ℝ
inst✝ : IsFiniteMeasure μ
hr : 0 < r
h_int : Integrable (Function.uncurry fun x y ↦ cexp (↑x * ↑y * I)) ((volume.restrict (Set.uIoc (-r) r)).prod μ)
y : ℝ
⊢ (if r * y = 0 then 2 * ↑r else ↑y⁻¹ * ∫ (x : ℝ) in -(y * r)..y * r, cexp (↑x * I)) = 2 * ↑r * ↑(sinc (r * y))

Tactic:
integral_exp_mul_I_eq_sinc

Goal state after:
case e_f
μ : Measure ℝ
r : ℝ
inst✝ : IsFiniteMeasure μ
hr : 0 < r
h_int : Integrable (Function.uncurry fun x y ↦ cexp (↑x * ↑y * I)) ((volume.restrict (Set.uIoc (-r) r)).prod μ)
y : ℝ
⊢ (if r * y = 0 then 2 * ↑r else ↑y⁻¹ * (2 * ↑(y * r) * ↑(sinc (y * r)))) = 2 * ↑r * ↑(sinc (r * y))
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
this : volume (Metric.ball 0 1) = ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))
⊢ volume (Metric.ball x r) = ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))

Tactic:
rw [Measure.addHaar_ball _ _ hr, this, ofReal_pow hr, finrank_euclideanSpace]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case e'_3
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
⊢ √π = 2 * Gamma (1 / 2 + 1)

Tactic:
rw [Gamma_add_one (by simp), Gamma_one_half_eq, ← mul_assoc, mul_div_cancel₀ _
        two_ne_zero, one_mul]

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

Goal state before:
pp: E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_2
ι : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype ι
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h : ∀ (i : ι), Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖⟪b i, x⟫_𝕜‖}) atTop (𝓝 0)
⊢ IsTightMeasureSet S

Tactic:
rcases subsingleton_or_nontrivial E with hE | hE

Goal state after:
case inl
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_2
ι : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype ι
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h : ∀ (i : ι), Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖⟪b i, x⟫_𝕜‖}) atTop (𝓝 0)
hE : Subsingleton E
⊢ IsTightMeasureSet S

case inr
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_2
ι : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype ι
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h : ∀ (i : ι), Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖⟪b i, x⟫_𝕜‖}) atTop (𝓝 0)
hE : Nontrivial E
⊢ IsTightMeasureSet S
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
s : Set 𝕜
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
⊢ ∃ g, ∀ a ∈ s, HasDerivWithinAt g (f a) s a

Tactic:
by
  let : NormedSpace ℝ E := .restrictScalars ℝ 𝕜 E
  apply hs.exists_forall_hasFDerivWithinAt_of_hasFDerivWithinAt_symmetric
  · intro a ha
    exact (ContinuousLinearMap.smulRightL 𝕜 𝕜 E 1).hasFDerivAt
      |>.comp_hasDerivWithinAt a (hf a ha).hasDerivWithinAt |>.restrictScalars ℝ
  · rintro a ha x - y -
    simpa using smul_comm ..

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s₁ s₂ : Set X
hs₁ : MeasurableSet s₁
hs₂ : MeasurableSet s₂
h : s₁ ⊆ s₂
P : Finpartition ⟨s₁, hs₁⟩
⊢ ∑ p ∈ P.parts, f ↑p ≤ preVariationFun f s₂

Tactic:
calc
    ∑ p ∈ P.parts, f p ≤ ∑ p ∈ (P.extendOfLE h).parts, f p :=
      Finset.sum_le_sum_of_subset (P.parts_subset_extendOfLE h)
    _ ≤ preVariationFun f s₂ := sum_le f hs₂ _

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

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition ⟨⋃ i, s i, ⋯⟩
hQ : b < ∑ p ∈ Q.parts, f ↑p
s' : ℕ → Subtype MeasurableSet := fun i ↦ ⟨s i, ⋯⟩
P : (i : ℕ) → Finpartition (s' i) := fun i ↦ Q.restrict ⋯
q : Subtype MeasurableSet
hq : q ∈ Q.parts
hq_eq : ↑q = ⋃ i, ↑q ∩ s i
⊢ f ↑q ≤ ∑' (i : ℕ), f (↑q ⊓ ↑(s' i))

Tactic:
let t (i : ℕ) : Subtype MeasurableSet := ⟨q.val ∩ s i, q.2.inter (hs i)⟩

Goal state after:
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition ⟨⋃ i, s i, ⋯⟩
hQ : b < ∑ p ∈ Q.parts, f ↑p
s' : ℕ → Subtype MeasurableSet := fun i ↦ ⟨s i, ⋯⟩
P : (i : ℕ) → Finpartition (s' i) := fun i ↦ Q.restrict ⋯
q : Subtype MeasurableSet
hq : q ∈ Q.parts
hq_eq : ↑q = ⋃ i, ↑q ∩ s i
t : ℕ → Subtype MeasurableSet := fun i ↦ ⟨↑q ∩ s i, ⋯⟩
⊢ f ↑q ≤ ∑' (i : ℕ), f (↑q ⊓ ↑(s' i))
Module: Mathlib.MeasureTheory.Measure.Support

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
⊢ μ.support = Set.univ

Tactic:
by
  simpa [Set.eq_univ_iff_forall, mem_support_iff_forall] using fun _ _ ↦ μ.measure_pos_of_mem_nhds

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

Goal state before:
pp: case h₁
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst✝ : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this : Filter.Tendsto (fun n ↦ (μ (accumulate f n)).toReal) Filter.atTop (nhds (μ (⋃ i, f i)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist (μ (accumulate f n)).toReal (μ (⋃ i, f i)).toReal < ε / 2
g : ℕ → Set X
g_mem : ∀ (n : ℕ), g n ∈ 𝒜
hg : ∀ (n : ℕ), μ.real (f n ∆ g n) < ε / (2 * (↑N + 1))
⊢ dist (μ (⋃ n, f n)).toReal (μ (⋃ n, ⋃ (_ : n ≤ N), f n)).toReal < ε / 2

Tactic:
exact (dist_comm (α := ℝ) .. ▸ hN N (le_refl N))

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
this✝ : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep : ∀ x ∈ univ, ∀ y ∈ univ, (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : ℕ → Set α := fun n ↦ if h : μ (A n) = 1 then A n else (A n)ᶜ
mBn : MeasurableSet (⋂ n, B n)
hBn : μ (⋂ n, B n) = 1
x₀ : α
hx₀ : ⋂ n, B n = {x₀}
s : Set α
hs : MeasurableSet s
h : x₀ ∉ s
this : μ s ≤ μ univ - μ (⋂ n, B n)
⊢ μ s = 0

Tactic:
MeasureTheory.measure_univ,

Goal state after:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
this✝ : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep : ∀ x ∈ univ, ∀ y ∈ univ, (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : ℕ → Set α := fun n ↦ if h : μ (A n) = 1 then A n else (A n)ᶜ
mBn : MeasurableSet (⋂ n, B n)
hBn : μ (⋂ n, B n) = 1
x₀ : α
hx₀ : ⋂ n, B n = {x₀}
s : Set α
hs : MeasurableSet s
h : x₀ ∉ s
this : μ s ≤ 1 - μ (⋂ n, B n)
⊢ μ s = 0