mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case mpr.inr.refine_1
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
F : Filter γ
inst✝ : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ C, ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ L, LipschitzWith L f) → Tendsto (fun i ↦ ∫ (ω : Ω), f ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), f ω ∂↑μ))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun n ω ↦ ↑((thickenedIndicator ⋯ s) ω)
key₁ : Tendsto (fun n ↦ ∫ (ω : Ω), fs n ω ∂↑μ) atTop (𝓝 ((↑μ).real s))
room₁ : (↑μ).real s < (↑μ).real s + ε / 2
M : ℕ
hM : ∀ (b : ℕ), M ≤ b → ∫ (ω : Ω), fs b ω ∂↑μ < (↑μ).real s + ε / 2
x y : Ω
⊢ dist (fs M x) (fs M y) ≤ 1

Tactic:
simp only [Real.dist_eq, abs_le]
    have h1 x : fs M x ≤ 1 := thickenedIndicator_le_one _ _ _
    have h2 x : 0 ≤ fs M x := by simp [fs]
    grind

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
inst✝ : HasPDF X ℙ μ
⊢ ∫⁻ (x : E), pdf X ℙ μ x ∂μ = ℙ Set.univ

Tactic:
rw [← setLIntegral_univ, ← map_eq_setLIntegral_pdf X ℙ μ MeasurableSet.univ,
    map_apply_of_aemeasurable (HasPDF.aemeasurable X ℙ μ) MeasurableSet.univ, Set.preimage_univ]

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case inr
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS
πTβ : Set (Set ((i : ↥T) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
hπT_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πT
s : Set ((i : ↥S) → β ↑i)
sets_s : (i : ↥S) → Set (β ↑i)
hs2 : univ.pi sets_s = s
t : Set ((i : ↥T) → β ↑i)
sets_t : (i : ↥T) → Set (β ↑i)
ht2 : univ.pi sets_t = t
hs1 : ∀ (i : ↥S), MeasurableSet (sets_s i)
ht1 : ∀ (i : ↥T), MeasurableSet (sets_t i)
⊢ ∀ᵐ (a : α) ∂μ,
    (η a) ((fun a i ↦ f (↑i) a) ⁻¹' s ∩ (fun a i ↦ f (↑i) a) ⁻¹' t) =
      (η a) ((fun a i ↦ f (↑i) a) ⁻¹' s) * (η a) ((fun a i ↦ f (↑i) a) ⁻¹' t)

Tactic:
rw [← hs2, ← ht2]

Goal state after:
case inr
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS
πTβ : Set (Set ((i : ↥T) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
hπT_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πT
s : Set ((i : ↥S) → β ↑i)
sets_s : (i : ↥S) → Set (β ↑i)
hs2 : univ.pi sets_s = s
t : Set ((i : ↥T) → β ↑i)
sets_t : (i : ↥T) → Set (β ↑i)
ht2 : univ.pi sets_t = t
hs1 : ∀ (i : ↥S), MeasurableSet (sets_s i)
ht1 : ∀ (i : ↥T), MeasurableSet (sets_t i)
⊢ ∀ᵐ (a : α) ∂μ,
    (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_s ∩ (fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_t) =
      (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_s) * (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_t)
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case refine_2
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
F : Filter γ
inst✝ : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ C, ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ L, LipschitzWith L f) → Tendsto (fun i ↦ ∫ (ω : Ω), f ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), f ω ∂↑μ))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun n ω ↦ ↑((thickenedIndicator ⋯ s) ω)
key₁ : Tendsto (fun n ↦ ∫ (ω : Ω), fs n ω ∂↑μ) atTop (𝓝 ((↑μ).real s))
room₁ : (↑μ).real s < (↑μ).real s + ε / 2
M : ℕ
hM : ∀ (b : ℕ), M ≤ b → ∫ (ω : Ω), fs b ω ∂↑μ < (↑μ).real s + ε / 2
key₂ : Tendsto (fun i ↦ ∫ (ω : Ω), fs M ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), fs M ω ∂↑μ))
room₂ : ∫ (a : Ω), fs M a ∂↑μ < ∫ (a : Ω), fs M a ∂↑μ + ε / 2
x : γ
hx : ∫ (ω : Ω), fs M ω ∂↑(μs x) ≤ ∫ (a : Ω), fs M a ∂↑μ + ε / 2
⊢ s.indicator 1 ≤ fs M

Tactic:
have h : _ ≤ fs M :=
        indicator_le_thickenedIndicator (δ := (1 : ℝ) / (M + 1)) (by positivity) s
      simpa using! h

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
⊢ ¬MemLp X 2 μ → ∞ ≤ eVar[X; μ]

Tactic:
top_le_iff

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
⊢ ¬MemLp X 2 μ → eVar[X; μ] = ∞
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
⊢ cov[X, Y; μ] = cov[Y, X; μ]

Tactic:
simp_rw [covariance]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
⊢ ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ =
    ∫ (ω : Ω), (Y ω - ∫ (x : Ω), Y x ∂μ) * (X ω - ∫ (x : Ω), X x ∂μ) ∂μ
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : Integrable X μ
c : ℝ
⊢ cov[fun ω ↦ X ω + c, Y; μ] = cov[X, Y; μ]

Tactic:
simp_rw [covariance]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : Integrable X μ
c : ℝ
⊢ ∫ (ω : Ω), (X ω + c - ∫ (x : Ω), X x + c ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ =
    ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) * (Y ω - ∫ (x : Ω), Y x ∂μ) ∂μ
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hY : Integrable Y μ
c : ℝ
⊢ cov[X, fun ω ↦ Y ω + c; μ] = cov[X, Y; μ]

Tactic:
exact covariance_add_const_right hY c

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
hX : AEMeasurable X (Measure.map Y μ)
hY : AEMeasurable Y μ
⊢ AEStronglyMeasurable (fun ω ↦ X ω - ∫ (x : Ω), X x ∂Measure.map Y μ) (Measure.map Y μ)

Tactic:
exact AEMeasurable.aestronglyMeasurable (by fun_prop)

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
⊢ eVar[X; μ] = ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ - ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2)

Tactic:
by_cases hℒ : MemLp X 2 μ
  · rw [← ofReal_variance hℒ, variance_eq_sub hℒ, ENNReal.ofReal_sub _ (sq_nonneg _)]
    congr
    simp_rw [← enorm_pow, enorm]
    rw [lintegral_coe_eq_integral]
    · simp
    · simpa using hℒ.abs.integrable_sq
  · symm
    rw [evariance_eq_top hX hℒ, ENNReal.sub_eq_top_iff]
    refine ⟨?_, ENNReal.ofReal_ne_top⟩
    rw [MemLp, not_and] at hℒ
    specialize hℒ hX
    simp only [eLpNorm_eq_lintegral_rpow_enorm_toReal two_ne_zero ENNReal.ofNat_ne_top, not_lt,
      top_le_iff, ENNReal.toReal_ofNat, one_div, ENNReal.rpow_eq_top_iff, inv_lt_zero, inv_pos,
      and_true, or_iff_not_imp_left, not_and_or, zero_lt_two] at hℒ
    exact mod_cast hℒ fun _ => zero_le_two

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

Goal state before:
pp: case neg.inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ s, X i =ᵐ[μ] 0
j : ι
hj1 : j ∈ s
hj2 : ¬X j =ᵐ[μ] 0
h' : s.Nontrivial
k : ι
hk1 : k ∈ s
hk2 : k ≠ j
this : IsProbabilityMeasure μ
i : ι
hi : i ∈ s
⊢ ∑ j ∈ s, cov[X i, X j; μ] = Var[X i; μ]

Tactic:
rw [← covariance_self (hs i hi).aemeasurable]

Goal state after:
case neg.inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ s, X i =ᵐ[μ] 0
j : ι
hj1 : j ∈ s
hj2 : ¬X j =ᵐ[μ] 0
h' : s.Nontrivial
k : ι
hk1 : k ∈ s
hk2 : k ≠ j
this : IsProbabilityMeasure μ
i : ι
hi : i ∈ s
⊢ ∑ j ∈ s, cov[X i, X j; μ] = cov[X i, X i; μ]
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable id (Measure.map f μ)

Tactic:
aestronglyMeasurable_iff_aemeasurable_separable

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
⊢ AEMeasurable id (Measure.map f μ) ∧ ∃ t, IsSeparable t ∧ ∀ᵐ (x : γ) ∂Measure.map f μ, id x ∈ t
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: ι : Type u_1
E : Type u_2
Ω' : Type u_3
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁴ : IsProbabilityMeasure μ'
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst✝³ : PseudoEMetricSpace E
inst✝² : BorelSpace E
inst✝¹ : l.IsCountablyGenerated
inst✝ : l.NeBot
X : ι → Ω' → E
h : TendstoInMeasure μ' X l Z
hX : ∀ (i : ι), AEMeasurable (X i) μ'
hZ : AEMeasurable Z μ'
ns : ℕ → ι
hns : Tendsto ns atTop l
ms : ℕ → ℕ
hms1 : Tendsto ms atTop atTop
hms2 : ∀ᵐ (x : Ω') ∂μ', Tendsto (fun i ↦ (X ∘ ns) (ms i) x) atTop (𝓝 (Z x))
⊢ TendstoInDistribution (fun n ↦ X (ns (ms n))) atTop Z (fun n ↦ μ') μ'

Tactic:
exact tendstoInDistribution_of_ae_tendsto (by fun_prop) hZ hms2

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst✝¹ : MeasurableSpace Z
inst✝ : MeasurableSingletonClass Z
hg : Measurable g
x₁ x₂ : X
h : f x₁ = f x₂
⊢ g x₁ ∈ {g x₂}

Tactic:
obtain ⟨s, -, hs⟩ := hg (measurableSet_singleton (g x₂))

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst✝¹ : MeasurableSpace Z
inst✝ : MeasurableSingletonClass Z
hg : Measurable g
x₁ x₂ : X
h : f x₁ = f x₂
s : Set Y
hs : f ⁻¹' s = g ⁻¹' {g x₂}
⊢ g x₁ ∈ {g x₂}
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:

Tactic:
eLpNorm (indicator sᶜᶜ (f i + g i)) p μ
      = eLpNorm (indicator s (f i) + indicator s (g i)) p μ := by rw [compl_compl, indicator_add']
    _ ≤ ε := le_of_lt <|
      hη _ _ ((hf_meas i).indicator hsm) ((hg_meas i).indicator hsm)
        (η_cast ▸ hfs i) (η_cast ▸ hgs i)

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

Goal state before:
pp: case refine_2
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
⊢ HasCompactSupport fun x ↦ f (x * g)

Tactic:
· have j : (fun x ↦ f (x * g)) = (f ∘ (Homeomorph.mulRight g)) := rfl
      rw [j]
      exact HasCompactSupport.comp_homeomorph f_comp _

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

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

Tactic:
apply_rules [ContinuousOn.pow, ContinuousOn.div, continuousOn_const]

Goal state after:
case hg
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun w ↦ circleMap z R w.2 - w.1) (closedBall z r ×ˢ univ)

case h₀
R r : ℝ
hr : r < R
z : ℂ
⊢ ∀ x ∈ closedBall z r ×ˢ univ, circleMap z R x.2 - x.1 ≠ 0
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.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : TopologicalSpace α
δ : Type u_5
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : Zero δ
f : γ →C_c δ
g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : β
hx : x ∈ tsupport (⇑f ∘ ⇑g)
o : Set γ
⊢ IsOpen o → g x ∈ o → (o ∩ Function.support f.toFun).Nonempty

Tactic:
ho

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : TopologicalSpace α
δ : Type u_5
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : Zero δ
f : γ →C_c δ
g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : β
hx : x ∈ tsupport (⇑f ∘ ⇑g)
o : Set γ
ho : IsOpen o
⊢ g x ∈ o → (o ∩ Function.support f.toFun).Nonempty
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ) →ₚ[ℝ] ℝ
f g : α →C_c ℝ≥0
⊢ NNReal.mk (Λ (toRealLinearMap (f + g))) ⋯ = NNReal.mk (Λ (toRealLinearMap f)) ⋯ + NNReal.mk (Λ (toRealLinearMap g)) ⋯

Tactic:
by simp; rfl

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 : E
ω : E → E →L[𝕜] F
γ : Path a b
⊢ ∫ᶜ (x : E) in γ.symm, ω x = -∫ᶜ (x : E) in γ, ω x

Tactic:
simp [curveIntegral, curveIntegralFun_symm]

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 C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x | deriv f x ≠ 0}
⊢ ‖f b - f a‖ ≤ C * volume.real {x | x ∈ Ioo a b ∧ deriv f x ≠ 0}

Tactic:
have hsm : MeasurableSet s := by measurability

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C : ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hnorm : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ C
s : Set ℝ := toMeasurable volume {x | deriv f x ≠ 0}
hsm : MeasurableSet s
⊢ ‖f b - f a‖ ≤ C * volume.real {x | x ∈ Ioo a b ∧ deriv f x ≠ 0}
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue

Goal state before:
pp: case neg.inr
a b : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
this :
  ∀ {a b : ℝ},
    ContinuousOn f [[a, b]] →
      IntervalIntegrable g μ a b →
        (∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x) →
          ¬a = b → a < b → ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
hab : ¬a < b
⊢ ∃ c ∈ [[a, b]], ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
simp only [not_lt] at hab
    obtain ⟨c, c_in_uIcc, that⟩ :=
      this (by rwa [uIcc_comm]) hg.symm (by rwa [uIoc_comm]) (by lia) (lt_of_le_of_ne' hab h)
    exact ⟨c, by rwa [uIcc_comm], by simpa [integral_symm b a]⟩

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‖
⊢ ∃ ε > 0, ∀ y ∈ ball a ε, ‖f y - f a‖ ≤ C * ‖‖y - a‖ ^ (r + 1)‖

Tactic:
refine ⟨ε, hε₀, fun y hy ↦ ?_⟩

Goal state after:
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 ε
⊢ ‖f y - f a‖ ≤ C * ‖‖y - a‖ ^ (r + 1)‖
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f₁ : X →C_c ℝ≥0
⊢ ∀ ⦃b : X →C_c ℝ≥0⦄, f₁ ≤ b → Λ f₁ ≤ Λ b

Tactic:
f₂

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f₁ f₂ : X →C_c ℝ≥0
⊢ f₁ ≤ f₂ → Λ f₁ ≤ Λ f₂
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: case refine_1
α : Type u
s : Set (Set α)
t✝ : Set α
ht✝ : t✝ ∈ generateMeasurableRec s (ω_ 1)
t : Set α
ht : t ∈ s
⊢ ∃ i, ∃ (_ : i < ω_ 1), t ∈ generateMeasurableRec s i

Tactic:
exact ⟨0, omega_pos 1, self_subset_generateMeasurableRec s 0 ht⟩

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 μ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (charFun μ)

Tactic:
refine contDiff_zero.1 (contDiff_charFun ?_)

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 μ
⊢ MemLp id (↑0) μ
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: case h.right.right
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⋯
x : X
I' : Finset ι
V U : ↥I' → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : ↥I' → X → ↑I
hfs : ∀ (i : ↥I'), Continuous[t ↑i, _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I'), EqOn (fs i) 1 (U i)ᶜ
⊢ EqOn (I'.attach.sup fs) 1 (⋂ i, V i)ᶜ

Tactic:
simp only [EqOn, Pi.one_apply, show (1 : ↥I) = ⊤ from rfl] at hfsU ⊢
    conv => equals ∀ x i, x ∈ (V i)ᶜ → ∃ b, fs b x = ⊤ => simp [Finset.sup_eq_top_iff]
    intro x i hxi
    specialize hfsU i (by tauto_set)
    exists i

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

Goal state before:
pp: case a
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
hμs : ∃ δ > 0, μ (thickening δ s) ≠ ∞
hνs : ∃ δ > 0, ν (thickening δ s) ≠ ∞
⊢ μ s ≤ ν s

pp: case a
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
hμs : ∃ δ > 0, μ (thickening δ s) ≠ ∞
hνs : ∃ δ > 0, ν (thickening δ s) ≠ ∞
⊢ ν s ≤ μ s

Tactic:
· exact measure_le_measure_closure_of_levyProkhorovEDist_eq_zero
      hLP s_closed.measurableSet hνs |>.trans <|
      le_of_eq (congr_arg _ s_closed.closure_eq)

Goal state after:
case a
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
hμs : ∃ δ > 0, μ (thickening δ s) ≠ ∞
hνs : ∃ δ > 0, ν (thickening δ s) ≠ ∞
⊢ ν s ≤ μ s
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ ε : ℝ≥0∞
B : Set Ω
h : 1 - μ (thickening ε.toReal B) ≤ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + ε
ε_gt : δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ
almost :
  1 - μ (thickening ε.toReal B) + μ (thickening ε.toReal B) ≤
    ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + ε + μ (thickening ε.toReal B)
⊢ 1 - ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) ≤ μ (thickening ε.toReal B) + ε

Tactic:
tsub_add_cancel_of_le prob_le_one,

Goal state after:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ ε : ℝ≥0∞
B : Set Ω
h : 1 - μ (thickening ε.toReal B) ≤ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + ε
ε_gt : δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ
almost : 1 ≤ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + ε + μ (thickening ε.toReal B)
⊢ 1 - ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) ≤ μ (thickening ε.toReal B) + ε