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

Goal state before:
pp: X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst✝³ : IsFiniteMeasureOnCompacts μ
inst✝² : μ.InnerRegularCompactLTTop
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
r : ENNReal
hr : μ k < r
U : Set X
kU : k ⊆ U
U_open : IsOpen U
mu_U : μ U < r
f : X → ℝ
f_cont : Continuous f
fk : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 k
fU : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 0 Uᶜ
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
f_range : ∀ (x : X), { toFun := f, continuous_toFun := f_cont } x ∈ Icc 0 1
⊢ ∃ i, Continuous i ∧ HasCompactSupport i ∧ EqOn i 1 k ∧ 0 ≤ i ∧ ENNReal.ofReal (∫ (x : X), i x ∂μ) < r

Tactic:
refine ⟨f, f_cont, f_comp, fk, fun x ↦ (f_range x).1, ?_⟩

Goal state after:
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst✝³ : IsFiniteMeasureOnCompacts μ
inst✝² : μ.InnerRegularCompactLTTop
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
r : ENNReal
hr : μ k < r
U : Set X
kU : k ⊆ U
U_open : IsOpen U
mu_U : μ U < r
f : X → ℝ
f_cont : Continuous f
fk : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 k
fU : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 0 Uᶜ
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
f_range : ∀ (x : X), { toFun := f, continuous_toFun := f_cont } x ∈ Icc 0 1
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) < r
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: case e_a.e_a
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
k : ℕ
hk : k ∈ Finset.range (N - 1)
⊢ a + (↑N - ↑(Nat.succ 0) - ↑k.succ + ↑1) * (b - a) / ↑N = b + ↑(k + 1) * (a - b) / ↑N

Tactic:
field

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

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ ∑ x ∈ Finset.range N, (↑x + 1 - ↑x) * h / 2 * (f (a + ↑x * h) + f (a + (↑x + 1) * h)) =
    trapezoidal_integral f N a (a + ↑N * h)

Tactic:
trapezoidal_integral,

Goal state after:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ ∑ x ∈ Finset.range N, (↑x + 1 - ↑x) * h / 2 * (f (a + ↑x * h) + f (a + (↑x + 1) * h)) =
    (a + ↑N * h - a) / ↑N *
      ((f a + f (a + ↑N * h)) / 2 + ∑ k ∈ Finset.range (N - 1), f (a + (↑k + 1) * (a + ↑N * h - a) / ↑N))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ ↑N * (h / ↑N) = h

Tactic:
field

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
y : ℝ
hy : y ∈ Set.Icc a b
⊢ HasDerivWithinAt g (dg y) (Set.Icc a b) y

Tactic:
unfold g trapezoidal_error trapezoidal_integral

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
ddg : ℝ → ℝ := fun t ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
y : ℝ
hy : y ∈ Set.Icc a b
⊢ HasDerivWithinAt
    (fun t ↦
      (t - a) / ↑1 * ((f a + f t) / 2 + ∑ k ∈ Finset.range (1 - 1), f (a + (↑k + 1) * (t - a) / ↑1)) -
        ∫ (x : ℝ) in a..t, f x)
    (dg y) (Set.Icc a b) y
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
x : ℝ
hx : x ∈ Set.Icc a b
⊢ |(x - a) / 2| * |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ / 2 * (x - a)

Tactic:
abs_div,

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
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
x : ℝ
hx : x ∈ Set.Icc a b
⊢ |x - a| / |2| * |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ / 2 * (x - a)
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
φ φ' : ℝ → ℝ
h : ∀ x ∈ Set.Icc a b, HasDerivWithinAt φ (φ' x) (Set.Icc a b) x
h0 : φ a = 0
c : ℝ
n : ℕ
h_bound : ∀ t ∈ Set.Icc a b, |φ' t| ≤ c * (t - a) ^ n
t : ℝ
ht : t ∈ Set.Icc a b
⊢ |φ t| ≤ c / (↑n + 1) * (t - a) ^ (n + 1)

Tactic:
have hB (x) : HasDerivAt (fun y ↦ c / (n + 1) * (y - a) ^ (n + 1)) (c * (x - a) ^ n) x := by
      convert!
        (hasDerivAt_const x (c / (n + 1))).mul
          (((hasDerivAt_id x).sub (hasDerivAt_const x a)).pow (n + 1)) using 1
      simp [sub_eq_add_neg, field]

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
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
φ φ' : ℝ → ℝ
h : ∀ x ∈ Set.Icc a b, HasDerivWithinAt φ (φ' x) (Set.Icc a b) x
h0 : φ a = 0
c : ℝ
n : ℕ
h_bound : ∀ t ∈ Set.Icc a b, |φ' t| ≤ c * (t - a) ^ n
t : ℝ
ht : t ∈ Set.Icc a b
hB : ∀ (x : ℝ), HasDerivAt (fun y ↦ c / (↑n + 1) * (y - a) ^ (n + 1)) (c * (x - a) ^ n) x
⊢ |φ t| ≤ c / (↑n + 1) * (t - a) ^ (n + 1)
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| ≤ ζ
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
⊢ b = a + ↑N * h

Tactic:
field

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| ≤ ζ
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
this : ∀ k ∈ Finset.range N, |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * h ^ 3
⊢ ↑N * (ζ / 12 * h ^ 3) = (a + ↑N * h - a) ^ 3 * ζ / (12 * ↑N ^ 2)

Tactic:
field

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n) μ
x : Fin n → E
h : innerₗ E = ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)
hint' : ∀ (k : ℕ), ↑k ≤ ↑n → Integrable (fun x ↦ ‖x‖ ^ k * ‖1 x‖) μ
⊢ (-((↑Real.pi)⁻¹ * 2⁻¹)) ^ n *
      ∫ (v : E),
        cexp (2 * ↑Real.pi * ((↑Real.pi)⁻¹ * 2⁻¹ * ↑⟪v, t⟫) * I) * ((-(2 * ↑Real.pi * I)) ^ n * ∏ i, ↑⟪v, x i⟫) ∂μ =
    I ^ n * ∫ (y : E), (∏ i, ↑⟪y, x i⟫) * cexp (↑⟪y, t⟫ * I) ∂μ

Tactic:
simp_rw [mul_left_comm (exp _), integral_const_mul, ← mul_assoc, ← mul_pow]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n) μ
x : Fin n → E
h : innerₗ E = ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)
hint' : ∀ (k : ℕ), ↑k ≤ ↑n → Integrable (fun x ↦ ‖x‖ ^ k * ‖1 x‖) μ
⊢ (-((↑Real.pi)⁻¹ * 2⁻¹) * -(2 * ↑Real.pi * I)) ^ n *
      ∫ (a : E), cexp (2 * ↑Real.pi * (↑Real.pi)⁻¹ * 2⁻¹ * ↑⟪a, t⟫ * I) * ∏ i, ↑⟪a, x i⟫ ∂μ =
    I ^ n * ∫ (y : E), (∏ i, ↑⟪y, x i⟫) * cexp (↑⟪y, t⟫ * I) ∂μ
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

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

Tactic:
by
  simp [charFun_apply, innerProbChar_apply]

Goal state after:
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
hK : IsClosed[inst✝²] K
hx : x ∉ K
cx : IsClosed[inst✝²] (closure[inst✝²] {x})
d : Disjoint (closure[inst✝²] {x}) K
f : X → ℝ
cf : Continuous[inst✝², _] f
hfx : EqOn (⇑{ toFun := f, continuous_toFun := cf }) 0 (closure[inst✝²] {x})
hfK : EqOn (⇑{ toFun := f, continuous_toFun := cf }) 1 K
hficc : ∀ (x : X), { toFun := f, continuous_toFun := cf } x ∈ Icc 0 1
⊢ ∃ f, Continuous[inst✝², _] f ∧ f x = 0 ∧ EqOn f 1 K

Tactic:
let g : X → I := fun x => ⟨f x, hficc x⟩

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
inst✝ : R0Space X
x : X
K : Set X
hK : IsClosed[inst✝²] K
hx : x ∉ K
cx : IsClosed[inst✝²] (closure[inst✝²] {x})
d : Disjoint (closure[inst✝²] {x}) K
f : X → ℝ
cf : Continuous[inst✝², _] f
hfx : EqOn (⇑{ toFun := f, continuous_toFun := cf }) 0 (closure[inst✝²] {x})
hfK : EqOn (⇑{ toFun := f, continuous_toFun := cf }) 1 K
hficc : ∀ (x : X), { toFun := f, continuous_toFun := cf } x ∈ Icc 0 1
g : X → ↑I := fun x ↦ ⟨f x, ⋯⟩
⊢ ∃ f, Continuous[inst✝², _] f ∧ f x = 0 ∧ EqOn f 1 K
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: ι : Type u_6
inst✝³ : Fintype ι
E : ι → Type u_7
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
t : PiLp 2 E
⊢ ∫ (x : WithLp 2 ((i : ι) → E i)), cexp (↑⟪x, t⟫ * I) ∂Measure.map (toLp 2) (Measure.pi μ) =
    ∏ i, ∫ (x : E i), cexp (↑⟪x, t.ofLp i⟫ * I) ∂μ i

Tactic:
PiLp.inner_apply,

Goal state after:
ι : Type u_6
inst✝³ : Fintype ι
E : ι → Type u_7
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
t : PiLp 2 E
⊢ ∫ (x : WithLp 2 ((i : ι) → E i)), cexp (↑(∑ i, ⟪x.ofLp i, t.ofLp i⟫) * I) ∂Measure.map (toLp 2) (Measure.pi μ) =
    ∏ i, ∫ (x : E i), cexp (↑⟪x, t.ofLp i⟫ * I) ∂μ i
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: case a
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
x : X
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝¹] U
⊢ ∃ i, stoneCechUnit x ∈ i ∧ IsOpen i ∧ stoneCechUnit ⁻¹' i ⊆ U

Tactic:
obtain ⟨f, hf, efx, hfU⟩ :=
      CompletelyRegularSpace.completely_regular_isOpen x U hU hxU

Goal state after:
case a
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
x : X
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝¹] U
f : X → ↑I
hf : Continuous[inst✝¹, _] f
efx : f x = 0
hfU : EqOn f 1 Uᶜ
⊢ ∃ i, stoneCechUnit x ∈ i ∧ IsOpen i ∧ stoneCechUnit ⁻¹' i ⊆ U
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: ι : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
E : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
L : StrongDual ℝ ((i : ι) → E i)
⊢ charFunDual (Measure.pi μ) L = ∏ i, charFunDual (μ i) (L ∘SL ContinuousLinearMap.single ℝ E i)

Tactic:
by
  simp_rw [charFunDual_apply, ← L.sum_comp_single, ofReal_sum, Finset.sum_mul, Complex.exp_sum,
    ← integral_fintype_prod_eq_prod]

Goal state after:
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 : ¬δ = ∞
x : ℝ≥0∞
⊢ ∀ (B : Set Ω),
    0 < x →
      x < ∞ →
        MeasurableSet B → μ B ≤ ν (thickening (δ + x).toReal B) + δ + x ∧ ν B ≤ μ (thickening (δ + x).toReal B) + δ + x

Tactic:
B

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 : ¬δ = ∞
x : ℝ≥0∞
B : Set Ω
⊢ 0 < x →
    x < ∞ →
      MeasurableSet B → μ B ≤ ν (thickening (δ + x).toReal B) + δ + x ∧ ν B ≤ μ (thickening (δ + x).toReal B) + δ + x
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 ν κ = ∞
ε : ℝ≥0∞
⊢ ∀ (B : Set Ω),
    0 < ε →
      ε < ∞ →
        MeasurableSet B →
          μ B ≤
              κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
                  (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
                ε ∧
            κ B ≤
              μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
                  (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
                ε

Tactic:
B

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.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 ν κ + ε
hs_add_r' : s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal
⊢ μ (thickening r.toReal (thickening s.toReal B)) + r + s = μ (thickening r.toReal (thickening s.toReal B)) + (s + r)

Tactic:
by rw [add_assoc, add_comm r]

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

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ : ℝ≥0∞
h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ∞ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε
ε : ℝ≥0∞
⊢ ∀ (B : Set Ω),
    δ < ε → ε < ∞ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε ∧ ν B ≤ μ (thickening ε.toReal B) + ε

Tactic:
B

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

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ : ℝ
δ_nn : 0 ≤ δ
h : ∀ (ε : ℝ) (B : Set Ω), δ < ε → MeasurableSet B → μ B ≤ ν (thickening ε B) + ENNReal.ofReal ε
ε : ℝ≥0∞
⊢ ∀ (B : Set Ω), ENNReal.ofReal δ < ε → ε < ∞ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε

Tactic:
B

Goal state after:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ : ℝ
δ_nn : 0 ≤ δ
h : ∀ (ε : ℝ) (B : Set Ω), δ < ε → MeasurableSet B → μ B ≤ ν (thickening ε B) + ENNReal.ofReal ε
ε : ℝ≥0∞
B : Set Ω
⊢ ENNReal.ofReal δ < ε → ε < ∞ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (fun x ↦ ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs x) ν + εs x) {a | t ≤ f a})) atTop
    (𝓝 (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
εs_pos : 0 < εs n
hn :
  ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs n) ν + εs n) {a | t ≤ f a}) <
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}) + δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
bound :
  ∫ (ω : Ω), f ω ∂↑(Ps n) ≤
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs n) ν + εs n) {a | t ≤ f a})) + (dist (μs n) ν + εs n) * ‖f‖
⊢ δ / 2 + ‖f‖ * (‖f‖⁻¹ * δ / 2) = δ

Tactic:
field

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Goal state before:
pp: case hle
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a b c d : E
γ₁ : Path a b
γ₂ : Path c d
s : Set (↑I × ↑I)
t : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : (↑γ₁).Homotopy ↑γ₂
hs : s.Countable
hφt : ∀ a_1 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, φ (a_1, b_1) ∈ t
hω : ∀ a_1 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, (a_1, b_1) ∉ s → HasFDerivWithinAt ω (dω (φ (a_1, b_1))) t (φ (a_1, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ a_1 ∈ Ioo 0 1,
    ∀ b_1 ∈ Ioo 0 1,
      (a_1, b_1) ∉ s →
        ∀ u ∈ tangentConeAt ℝ t (φ (a_1, b_1)),
          ∀ v ∈ tangentConeAt ℝ t (φ (a_1, b_1)), ((dω (φ (a_1, b_1))) u) v = ((dω (φ (a_1, b_1))) v) u
U : Set (ℝ × ℝ) := Ioo 0 1 ×ˢ Ioo 0 1
hU : U = Ioo 0 1 ×ˢ Ioo 0 1
hinterior : interior (Icc 0 1) = U
hunique : UniqueDiffOn ℝ (Icc 0 1)
hUopen : IsOpen U
hU_subset : U ⊆ Icc 0 1
hclosure : closure U = Icc 0 1
ψ : ℝ × ℝ → E := fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hcontdiff : ContDiffOn ℝ 2 ψ (Icc 0 1)
hψ : ψ = fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hψφ : ∀ (a_1 b_1 : ↑I), ψ (↑a_1, ↑b_1) = φ (a_1, b_1)
hψ_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ψ
hψUt : MapsTo ψ U t
dψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fderivWithin ℝ ψ (Icc 0 1)
s' : Set (ℝ × ℝ) := Prod.map Subtype.val Subtype.val '' s
hs' : s' = Prod.map Subtype.val Subtype.val '' s
hmem_s' : ∀ (x y : ↑I), (↑x, ↑y) ∈ s' ↔ (x, y) ∈ s
hs'c : s'.Countable
hdψ : ∀ a ∈ U, HasFDerivAt ψ (dψ a) a
d2ψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] E := fderivWithin ℝ dψ (Icc 0 1)
hd2ψ : ∀ a ∈ U, HasFDerivAt dψ (d2ψ a) a
hd2ψ_symm : ∀ a ∈ Icc 0 1, ∀ (x y : ℝ × ℝ), ((d2ψ a) x) y = ((d2ψ a) y) x
η : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := fun a ↦ ω (ψ a) ∘SL dψ a
f : ℝ × ℝ → F := fun a ↦ (η a) (0, 1)
hf : ∀ a ∈ Icc 0 1, f a = (ω (ψ a)) (derivWithin (ψ ∘ fun x ↦ (a.1, x)) I a.2)
g : ℝ × ℝ → F := fun a ↦ -(η a) (1, 0)
hg : ∀ a ∈ Icc 0 1, g a = (ω (ψ a)) (-derivWithin (ψ ∘ fun x ↦ (x, a.2)) I a.1)
dη : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] F :=
  fun a ↦ (ContinuousLinearMap.compL ℝ (ℝ × ℝ) E F) (ω (ψ a)) ∘SL d2ψ a + (dω (ψ a)).bilinearComp (dψ a) (dψ a)
hdη : ∀ a ∈ U \ s', HasFDerivAt η (dη a) a
hdη_symm : ∀ a ∈ U \ s', ∀ (u v : ℝ × ℝ), ((dη a) u) v = ((dη a) v) u
f' : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := fun a ↦ (ContinuousLinearMap.apply ℝ F) (0, 1) ∘SL dη a
hf' : ∀ a ∈ U \ s', HasFDerivAt f (f' a) a
g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := fun a ↦ -(ContinuousLinearMap.apply ℝ F) (1, 0) ∘SL dη a
hg' : ∀ a ∈ U \ s', HasFDerivAt g (g' a) a
hf'g' : (fun a ↦ (f' a) (1, 0) + (g' a) (0, 1)) =ᵐ[volume.restrict (Icc 0 1)] 0
this : ∫ (a : ℝ × ℝ) in Icc 0 1, (f' a) (1, 0) + (g' a) (0, 1) = 0
hηc : ContinuousOn η (Icc 0 1)
⊢ 0 ≤ 1

Tactic:
exact zero_le_one

Goal state after: