mathlib-initiative/mathlib-tactics huggingface dataset:
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
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht : t < 1 / 2
⊢ curveIntegralFun ω (γab.trans γbc) t = 2 • curveIntegralFun ω γab (2 * t)

Tactic:
let instE := NormedSpace.restrictScalars ℝ 𝕜 E
  have H₁ : (γab.trans γbc).extend =ᶠ[𝓝 t] (fun s ↦ γab.extend (2 * s)) :=
    (eventually_le_nhds ht).mono fun _ ↦ Path.extend_trans_of_le_half _ _
  have H₂ : (2 : ℝ) • I =ᶠ[𝓝 (2 * t)] I := by
    rw [LinearOrderedField.smul_Icc two_pos, mul_zero, mul_one, ← nhdsWithin_eq_iff_eventuallyEq]
    rcases lt_trichotomy t 0 with ht₀ | rfl | ht₀
    · rw [notMem_closure_iff_nhdsWithin_eq_bot.mp, notMem_closure_iff_nhdsWithin_eq_bot.mp] <;>
        simp_intro h <;> linarith
    · simp
    · rw [nhdsWithin_eq_nhds.2, nhdsWithin_eq_nhds.2] <;> simp [*] <;> linarith
  rw [curveIntegralFun_def, H₁.self_of_nhds, H₁.derivWithin_eq_of_nhds, curveIntegralFun_def,
    derivWithin_comp_mul_left, ofNat_smul_eq_nsmul, map_nsmul, derivWithin_congr_set H₂]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, 1 ∂ν
hν0 : ∫ (x : α) in s, 1 ∂ν = 0
c : α
hc : c ∈ s
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ

Tactic:
refine ⟨c, hc, ?_⟩

Goal state after:
case pos
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, 1 ∂ν
hν0 : ∫ (x : α) in s, 1 ∂ν = 0
c : α
hc : c ∈ s
⊢ ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
Module: Mathlib.MeasureTheory.Integral.MeanValue

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, 1 ∂ν
hν0 : ¬∫ (x : α) in s, 1 ∂ν = 0
hν0' : (ν s).toReal ≠ 0
hνfin : ν s ≠ ⊤
hν0'' : ν s ≠ 0
hint : IntegrableOn f s ν
c : α
hc : c ∈ s
h_ave : f c = ⨍ (x : α) in s, f x ∂ν
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ

Tactic:
refine ⟨c, hc, ?_⟩

Goal state after:
case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, 1 ∂ν
hν0 : ¬∫ (x : α) in s, 1 ∂ν = 0
hν0' : (ν s).toReal ≠ 0
hνfin : ν s ≠ ⊤
hν0'' : ν s ≠ 0
hint : IntegrableOn f s ν
c : α
hc : c ∈ s
h_ave : f c = ⨍ (x : α) in s, f x ∂ν
⊢ ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
Module: Mathlib.MeasureTheory.Integral.MeanValue

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ x ∈ s, 0 ≤ g x
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ

Tactic:
by
  have hg0_ae : ∀ᵐ x ∂(μ.restrict s), 0 ≤ g x := by
    rw [ae_restrict_iff' hs_meas]
    exact ae_of_all μ hg0
  exact exists_eq_const_mul_setIntegral_of_ae_nonneg hs_conn hs_meas hf hg hfg hg0_ae

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

Goal state before:
pp: 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
⊢ ∀ (a_1 b_1 : ↑I), ψ (↑a_1, ↑b_1) = φ (a_1, b_1)

Tactic:
simp [ψ]

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

Goal state before:
pp: case bound
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
⊢ z ∈ closedBall a ‖y - a‖ → ‖fderiv ℝ f z‖ ≤ C * ‖y - a‖ ^ r

Tactic:
hz

Goal state after:
case bound
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‖
⊢ ‖fderiv ℝ f z‖ ≤ C * ‖y - a‖ ^ r
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, (∀ x ∈ K, 1 ≤ f x) ∧ Λ f < rieszContentAux Λ K + ε

Tactic:
refine ⟨f, f_hyp.left, ?_⟩

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 = α
⊢ Λ f < rieszContentAux Λ K + ε
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
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)
x : ℝ
hx : x ∈ Set.Icc (ak k) (ak (k + 1))
⊢ _root_.derivWithin f (Set.Icc a b) x = _root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))) x

Tactic:
rw [← derivWithin_subset h3 (uniqueDiffOn_Icc h4 x hx) (h_df x (h3 hx))]

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range ⇑f ⊆ Ioo a (a + ↑N * ε)
b : ℝ := a + ↑N * ε
y : Fin N → ℝ := fun n ↦ a + ε * (↑↑n + 1)
hy : ∀ {n m : Fin N}, n < m → y n + ε ≤ y m
E : Fin N → Set X := fun n ↦ ⇑f ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport ⇑f
a✝ : ℝ
⊢ a✝ ∈ range ⇑f → a✝ ∈ Ioc (a + ↑0 * ε) (a + ↑N * ε)

Tactic:
hz

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range ⇑f ⊆ Ioo a (a + ↑N * ε)
b : ℝ := a + ↑N * ε
y : Fin N → ℝ := fun n ↦ a + ε * (↑↑n + 1)
hy : ∀ {n m : Fin N}, n < m → y n + ε ≤ y m
E : Fin N → Set X := fun n ↦ ⇑f ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport ⇑f
a✝ : ℝ
hz : a✝ ∈ range ⇑f
⊢ a✝ ∈ Ioc (a + ↑0 * ε) (a + ↑N * ε)
Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA : (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm ⋯) (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
heq' : ∀ g ∈ A_toReal, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
f : E →ᵇ ℝ
h0 : Tendsto (fun ε ↦ 6 * √ε) (𝓝[>] 0) (𝓝 0)
⊢ Tendsto (fun ε ↦ |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'|) (𝓝[>] 0) (𝓝 0)

Tactic:
apply squeeze_zero' (eventually_nhdsWithin_of_forall (fun x _ => abs_nonneg _))
      (eventually_nhdsWithin_of_forall _) h0

Goal state after:
E : Type u_1
𝕜 : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA : (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) := ⋯
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
heq' : ∀ g ∈ A_toReal, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
f : E →ᵇ ℝ
h0 : Tendsto (fun ε ↦ 6 * √ε) (𝓝[>] 0) (𝓝 0)
⊢ ∀ x ∈ Set.Ioi 0, |∫ (x_1 : E), x.mulExpNegMulSq (f x_1) ∂P - ∫ (x_1 : E), x.mulExpNegMulSq (f x_1) ∂P'| ≤ 6 * √x
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 : ℝ
this : IsProbabilityMeasure (Measure.map X P)
⊢ 1 + ↑(∫ (x : Ω), X x ∂P) * ↑t * I - ↑(∫ (x : Ω), X x ^ 2 ∂P) * ↑t ^ 2 / 2 =
    1 + ↑t * I * ↑(∫ (x : ℝ), x ∂Measure.map X P) + 2⁻¹ * (↑t * I) ^ 2 * ↑(∫ (x : ℝ), x ^ 2 ∂Measure.map X P)

Tactic:
integral_map,

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

case hφ
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
hint : MemLp id 2 (Measure.map X P)
t : ℝ
this : IsProbabilityMeasure (Measure.map X P)
⊢ AEMeasurable X P

case hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
hint : MemLp id 2 (Measure.map X P)
t : ℝ
this : IsProbabilityMeasure (Measure.map X P)
⊢ AEStronglyMeasurable (fun x ↦ x) (Measure.map X P)
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
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

Tactic:
conv at hfU => equals Uᶜ ⊆ f ⁻¹' {1} => simp [EqOn, subset_def]

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 : Uᶜ ⊆ f ⁻¹' {1}
⊢ ∃ i, stoneCechUnit x ∈ i ∧ IsOpen i ∧ stoneCechUnit ⁻¹' i ⊆ U
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst✝¹] s
f : X → ↑I
hfc : Continuous[inst✝¹, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
⊢ ∃ v ∈ {s | IsClopen s}, x ∈ v ∧ v ⊆ s

Tactic:
let R := Set.range f

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst✝¹] s
f : X → ↑I
hfc : Continuous[inst✝¹, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set ↑I := range f
⊢ ∃ v ∈ {s | IsClopen s}, x ∈ v ∧ v ⊆ s
Module: Mathlib.MeasureTheory.Measure.DiracProba

Goal state before:
pp: X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
⊢ Continuous[instTopologicalSpaceSubtype, inst✝³] ⇑diracProbaEquiv.symm

Tactic:
apply continuous_iff_continuousAt.mpr

Goal state after:
X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
⊢ ∀ (x : ↑(range diracProba)), ContinuousAt (⇑diracProbaEquiv.symm) x
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
t : ℝ
⊢ ν (thickening (ENNReal.ofReal ε).toReal {a | t ≤ f a}) + ENNReal.ofReal ε ≠ ∞

Tactic:
· exact ENNReal.add_ne_top.mpr ⟨measure_ne_top ν _, ofReal_ne_top⟩

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

Goal state before:
pp: case h.refine_2
ι : 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)) :=
  {t | ∃ s, t = univ.pi s ∧ (∀ (i : ι), MeasurableSet (s i)) ∧ ∀ (i : ι), (μ i) (frontier (s i)) = 0}
this✝ : IsPiSystem S
this : (i : ι) → PseudoMetricSpace (α i) := fun i ↦ pseudoMetrizableSpacePseudoMetric (α 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
⊢ (univ.pi fun i ↦ ball (x i) (r i)) ⊆ u

Tactic:
calc univ.pi fun i ↦ ball (x i) (r i)
      _ ⊆ univ.pi fun i ↦ ball (x i) ε := by gcongr with i hi; exact (rpos i).2.le
      _ ⊆ u := by rwa [← ball_pi _ εpos]

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

Goal state before:
pp: α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
⊢ ContinuousAt (fun μ ↦ μ.1.prod μ.2) μ

Tactic:
let S : Set (Set (α × β)) := {t | ∃ (a : Set α) (b : Set β),
    MeasurableSet a ∧ μ.1 (frontier a) = 0 ∧ MeasurableSet b ∧ μ.2 (frontier b) = 0
    ∧ t = a ×ˢ b}

Goal state after:
α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
μ : ProbabilityMeasure α × ProbabilityMeasure β
S : Set (Set (α × β)) :=
  {t | ∃ a b, MeasurableSet a ∧ μ.1 (frontier a) = 0 ∧ MeasurableSet b ∧ μ.2 (frontier b) = 0 ∧ t = a ×ˢ b}
⊢ ContinuousAt (fun μ ↦ μ.1.prod μ.2) μ
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✝¹ : μ.Regular
inst✝ : ν.Regular
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ = ∫ (x : X), f x ∂ν
⊢ μ = ν

Tactic:
apply Measure.OuterRegular.ext_isOpen
  apply Measure.InnerRegularWRT.eq_of_innerRegularWRT_of_forall_eq Measure.Regular.innerRegular
    Measure.Regular.innerRegular
  intro K hK
  apply le_antisymm
  · exact measure_le_of_isCompact_of_integral (fun f ↦ (hμν f).le) hK
  · exact measure_le_of_isCompact_of_integral (fun f ↦ (hμν f).ge) hK

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 Ω
⊢ ContinuousAt ofMeasure P

Tactic:
continuousAt_iff'

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

Goal state before:
pp: μ : Measure ℝ
r : ℝ
inst✝ : IsProbabilityMeasure μ
hr : 0 < r
⊢ μ.real {x | r < |x|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun μ t‖

Tactic:
by
  have integrable_sinc_const_mul (r : ℝ) : Integrable (fun x ↦ sinc (r * x)) μ :=
    (integrable_map_measure stronglyMeasurable_sinc.aestronglyMeasurable (by fun_prop)).mp
      integrable_sinc
  calc μ.real {x | r < |x|}
  _ = μ.real {x | 2 < |2 * r⁻¹ * x|} := by
    congr 1 with x
    simp only [Set.mem_ofPred_eq, abs_mul, Nat.abs_ofNat]
    rw [abs_of_nonneg (a := r⁻¹) (by positivity), mul_assoc, ← inv_mul_lt_iff₀ (by positivity),
      inv_mul_cancel₀ (by positivity), lt_inv_mul_iff₀ (by positivity), mul_one]
  _ = ∫ x in {x | 2 < |2 * r⁻¹ * x|}, 1 ∂μ := by simp
  _ = 2 * ∫ x in {x | 2 < |2 * r⁻¹ * x|}, 2⁻¹ ∂μ := by
    rw [← integral_const_mul]
    congr with _
    rw [mul_inv_cancel₀ (by positivity)]
  _ ≤ 2 * ∫ x in {x | 2 < |2 * r⁻¹ * x|}, 1 - sinc (2 * r⁻¹ * x) ∂μ := by
    gcongr (2 : ℝ) * ?_
    refine setIntegral_mono_on ?_
      ((integrable_const _).sub (integrable_sinc_const_mul _)).integrableOn ?_ fun x hx ↦ ?_
    · exact Integrable.integrableOn <| by fun_prop
    · exact MeasurableSet.preimage measurableSet_Ioi (by fun_prop)
    · have hx_ne : 2 * r⁻¹ * x ≠ 0 := by
        intro hx0
        simp only [hx0, Set.mem_ofPred_eq, abs_zero] at hx
        linarith
      rw [le_sub_iff_add_le, ← le_sub_iff_add_le']
      norm_num
      rw [one_div]
      refine (sinc_le_inv_abs hx_ne).trans ?_
      exact (inv_le_inv₀ (by positivity) (by positivity)).mpr (le_of_lt hx)
  _ ≤ 2 * ∫ x, 1 - sinc (2 * r⁻¹ * x) ∂μ := by
    grw [setIntegral_le_integral (by fun_prop) <| ae_of_all _ fun x ↦ ?_]
    simp only [Pi.zero_apply, sub_nonneg]
    exact sinc_le_one (2 * r⁻¹ * x)
  _ ≤ 2 * ‖∫ x, 1 - sinc (2 * r⁻¹ * x) ∂μ‖ := by
    gcongr
    exact Real.le_norm_self _
  _ = 2⁻¹ * r *
      ‖2 * (r : ℂ)⁻¹ + 2 * r⁻¹ - 2 * (2 * r⁻¹) * ∫ x, sinc (2 * r⁻¹ * x) ∂μ‖ := 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
  _ = 2⁻¹ * r * ‖∫ t in (-2 * r⁻¹)..(2 * r⁻¹), 1 - charFun μ t‖ := by
    rw [intervalIntegral.integral_sub intervalIntegrable_const intervalIntegrable_charFun, neg_mul,
      integral_charFun_Icc (by positivity)]
    simp

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

Goal state before:
pp: case h
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
g : E →C_c ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ (fun x ↦ g x) ≤ fun x ↦ ‖g.toBoundedContinuousFunction‖

Tactic:
· intro x
          apply le_of_abs_le
          exact g.toBoundedContinuousFunction.norm_coe_le_norm x

Goal state after: