mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
u : γ → δ
h : IdentDistrib f g μ ν
hu : AEMeasurable u (Measure.map f μ)
⊢ Measure.map (u ∘ f) μ = Measure.map (u ∘ g) ν

Tactic:
rw [← AEMeasurable.map_map_of_aemeasurable hu h.aemeasurable_fst, ←
        AEMeasurable.map_map_of_aemeasurable _ h.aemeasurable_snd, h.map_eq]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
u : γ → δ
h : IdentDistrib f g μ ν
hu : AEMeasurable u (Measure.map f μ)
⊢ AEMeasurable u (Measure.map g ν)
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : Type u_3
β' : Type u_4
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
h :
  ∀ {φ : β → ℝ} {ψ : β' → ℝ},
    Measurable φ →
      Measurable ψ →
        Integrable (φ ∘ f) μ →
          Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
⊢ μ (f ⁻¹' A ∩ g ⁻¹' B) = μ (f ⁻¹' A) * μ (g ⁻¹' B)

Tactic:
specialize
    h (measurable_one.indicator hA) (measurable_one.indicator hB)
      ((integrable_const 1).indicator (hfm.comp measurable_id hA))
      ((integrable_const 1).indicator (hgm.comp measurable_id hB))

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : Type u_3
β' : Type u_4
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
A : Set β
hA : MeasurableSet A
B : Set β'
h : integral μ (A.indicator 1 ∘ f * B.indicator 1 ∘ g) = integral μ (A.indicator 1 ∘ f) * integral μ (B.indicator 1 ∘ g)
hB : MeasurableSet B
⊢ μ (f ⁻¹' A ∩ g ⁻¹' B) = μ (f ⁻¹' A) * μ (g ⁻¹' B)
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case hfm
Ω : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (f i) (Measure.map (X i) μ)
this : IsProbabilityMeasure μ
⊢ AEStronglyMeasurable (fun x ↦ ∏ i, f i (x i)) (Measure.map (fun ω x ↦ X x ω) μ)

Tactic:
hX.map_fun_eq_pi_map mX

Goal state after:
case hfm
Ω : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (f i) (Measure.map (X i) μ)
this : IsProbabilityMeasure μ
⊢ AEStronglyMeasurable (fun x ↦ ∏ i, f i (x i)) (Measure.pi fun i ↦ Measure.map (X i) μ)
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : 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 : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
h : IndepFun (fun a i ↦ AEMeasurable.mk (f ↑i) ⋯ a) (fun a i ↦ AEMeasurable.mk (f ↑i) ⋯ a) κ μ
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ↥S), f ↑i =ᵐ[κ a] AEMeasurable.mk (f ↑i) ⋯
a : α
ha : ∀ (i : ↥S), f ↑i =ᵐ[κ a] AEMeasurable.mk (f ↑i) ⋯
b : Ω
hb : ∀ (i : ↥S), f (↑i) b = AEMeasurable.mk (f ↑i) ⋯ b
⊢ (fun i ↦ AEMeasurable.mk (f ↑i) ⋯ b) = fun i ↦ f (↑i) b

Tactic:
ext i

Goal state after:
α : 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 : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
h : IndepFun (fun a i ↦ AEMeasurable.mk (f ↑i) ⋯ a) (fun a i ↦ AEMeasurable.mk (f ↑i) ⋯ a) κ μ
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ↥S), f ↑i =ᵐ[κ a] AEMeasurable.mk (f ↑i) ⋯
a : α
ha : ∀ (i : ↥S), f ↑i =ᵐ[κ a] AEMeasurable.mk (f ↑i) ⋯
b : Ω
hb : ∀ (i : ↥S), f (↑i) b = AEMeasurable.mk (f ↑i) ⋯ b
i : ↥S
⊢ AEMeasurable.mk (f ↑i) ⋯ b = f (↑i) b
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
⊢ UniformIntegrable f p μ

Tactic:
have hfmeas : ∀ i, AEStronglyMeasurable (f i) μ := fun i =>
    (hf i).aestronglyMeasurable_iff.2 hℒp.1

Goal state after:
α : Type u_1
inst✝⁴ : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
⊢ UniformIntegrable f p μ
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : 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 : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
h : IndepFun (fun a i ↦ AEMeasurable.mk (f ↑i) ⋯ a) (fun a i ↦ AEMeasurable.mk (f ↑i) ⋯ a) κ μ
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ↥T), f ↑i =ᵐ[κ a] AEMeasurable.mk (f ↑i) ⋯
a : α
ha : ∀ (i : ↥T), f ↑i =ᵐ[κ a] AEMeasurable.mk (f ↑i) ⋯
b : Ω
hb : ∀ (i : ↥T), f (↑i) b = AEMeasurable.mk (f ↑i) ⋯ b
⊢ (fun i ↦ AEMeasurable.mk (f ↑i) ⋯ b) = fun i ↦ f (↑i) b

Tactic:
ext i

Goal state after:
α : 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 : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
h : IndepFun (fun a i ↦ AEMeasurable.mk (f ↑i) ⋯ a) (fun a i ↦ AEMeasurable.mk (f ↑i) ⋯ a) κ μ
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ↥T), f ↑i =ᵐ[κ a] AEMeasurable.mk (f ↑i) ⋯
a : α
ha : ∀ (i : ↥T), f ↑i =ᵐ[κ a] AEMeasurable.mk (f ↑i) ⋯
b : Ω
hb : ∀ (i : ↥T), f (↑i) b = AEMeasurable.mk (f ↑i) ⋯ b
i : ↥T
⊢ AEMeasurable.mk (f ↑i) ⋯ b = f (↑i) b
Module: Mathlib.MeasureTheory.Group.FoelnerFilter

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
s t : Set X
ht : MeasurableSet t
hdisj : Disjoint s t
i : ι
hi : MeasurableSet (F i)
⊢ μ ((s ∪ t) ∩ F i) / μ (F i) = μ (s ∩ F i) / μ (F i) + μ (t ∩ F i) / μ (F i)

Tactic:
union_inter_distrib_right,

Goal state after:
G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
s t : Set X
ht : MeasurableSet t
hdisj : Disjoint s t
i : ι
hi : MeasurableSet (F i)
⊢ μ (s ∩ F i ∪ t ∩ F i) / μ (F i) = μ (s ∩ F i) / μ (F i) + μ (t ∩ F i) / μ (F i)
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ ∫ (x : ℝ) in Ioi 0, x ^ q * rexp (-x ^ p) =
    ∫ (x : ℝ) in Ioi 0, (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x))

Tactic:
rw [← integral_comp_rpow_Ioi _ (one_div_ne_zero (ne_of_gt hp)),
        abs_eq_self.mpr (le_of_lt (one_div_pos.mpr hp))]

Goal state after:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ ∫ (x : ℝ) in Ioi 0, (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-(x ^ (1 / p)) ^ p)) =
    ∫ (x : ℝ) in Ioi 0, (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x))
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : AddMonoid β
inst✝¹ : StarAddMonoid β
inst✝ : ContinuousStar β
f : α →C_c β
⊢ IsCompact (closure (Function.support fun x ↦ star (f x)))

Tactic:
have support_star : (Function.support fun (x : α) => star (f x)) = Function.support f := by
          ext x
          simp only [Function.mem_support, ne_eq, star_eq_zero]

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : AddMonoid β
inst✝¹ : StarAddMonoid β
inst✝ : ContinuousStar β
f : α →C_c β
support_star : (Function.support fun x ↦ star (f x)) = Function.support ⇑f
⊢ IsCompact (closure (Function.support fun x ↦ star (f x)))
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 ↑ε ⋯)
α : ℝ≥0
hα : 1 < α
K' : Set X := ⇑f ⁻¹' Ici α⁻¹
⊢ b.toNNReal ≤ Λ (α • f)

Tactic:
have hKK' : ↑K ⊆ interior K' :=
    subset_interior_iff.2 ⟨f ⁻¹' Ioi α⁻¹, isOpen_Ioi.preimage f.1.2,
      fun x hx ↦ (inv_lt_one_of_one_lt₀ hα).trans_le (hfleoneonK x hx),
      preimage_mono Ioi_subset_Ici_self⟩

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 < α
K' : Set X := ⇑f ⁻¹' Ici α⁻¹
hKK' : ↑K ⊆ interior K'
⊢ b.toNNReal ≤ Λ (α • f)
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
⊢ generateMeasurableRec s i ⊆ {t | GenerateMeasurable s t}

Tactic:
by
  apply WellFoundedLT.induction i
  exact fun i IH t ht => generateMeasurableRec_induction .basic .empty
    (fun u _ ⟨j, hj, hj'⟩ => .compl _ (IH j hj hj')) (fun f H => .iUnion _ fun n => (H n).1) 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 μ
n : ℕ∞
hint : ∀ (k : ℕ), MemLp id (↑k) μ
k : ℕ
hk : ↑k ≤ n
⊢ Integrable (fun v ↦ ‖v‖ ^ k) μ

Tactic:
refine MemLp.integrable_norm_pow' ((hint k).mono_exponent (by simp_all))

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

Goal state before:
pp: case pos
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 : Fin N → X →C_c ℝ
hg :
  (∀ (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)
n : Fin N
hn : n ∈ Finset.univ
x : X
hx : x ∈ tsupport ⇑(g n)
⊢ (g n • f) x ≤ ((y n + ε') • g n) x

Tactic:
rw [smul_eq_mul, mul_comm]
      apply mul_le_mul_of_nonneg_right ?_ (hg.2.2.1 n x).1
      exact le_of_lt <| (hV n).2.1 x <| mem_of_subset_of_mem (hg.1 n) hx

Goal state after:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: case a
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
x : X
⊢ ∀ (s : Set X), x ∈ s → IsOpen[inst✝¹] s → ∃ i, stoneCechUnit x ∈ i ∧ IsOpen i ∧ stoneCechUnit ⁻¹' i ⊆ s

Tactic:
intro U

Goal state after:
case a
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
x : X
U : Set X
⊢ x ∈ U → IsOpen[inst✝¹] U → ∃ 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ᶜ
R : Set ↑I := range f
⊢ lift.{u, 0} #↑R < lift.{0, u} 𝔠

Tactic:
simpa [R] using mk_range_le_lift.trans_lt (lift_strictMono hX)

Goal state after:
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
x : X
μ : ↑(range diracProba)
h : ↑μ = diracProba x
⊢ diracProbaInverse μ = x

Tactic:
by
  apply injective_diracProba (X := X)
  simp only [← h]
  exact (mem_range.mp μ.prop).choose_spec

Goal state after:
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_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 (0 + 0))
n : ℕ
⊢ dist (μs n) ν + εs n ∈ Ioi 0

Tactic:
rw [mem_Ioi]

Goal state after:
Ω : 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_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 (0 + 0))
n : ℕ
⊢ 0 < dist (μs n) ν + εs n
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case a
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 ∂ν
K : Set X
hK : IsCompact K
⊢ ν K ≤ μ K

Tactic:
· 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: case refine_2
Ω : 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
⊢ levyProkhorovEDist ↑(Ps n) ↑P < ENNReal.ofReal (dist (μs n) ν + εs n)

Tactic:
ENNReal.ofReal_add (by positivity) (by positivity),

Goal state after:
case refine_2
Ω : 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
⊢ levyProkhorovEDist ↑(Ps n) ↑P < ENNReal.ofReal (dist (μs n) ν) + ENNReal.ofReal (εs n)
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

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
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
hcontdiff : ContDiffOn ℝ 2 (fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2) (Icc 0 1)
⊢ ∫ᶜ (x : E) in γ₁, ω x + ∫ᶜ (x : E) in φ.evalAt 1, ω x = ∫ᶜ (x : E) in γ₂, ω x + ∫ᶜ (x : E) in φ.evalAt 0, ω x

Tactic:
by
  simp only [← curveIntegral_restrictScalars (𝕜 := 𝕜) (𝕝 := ℝ)]
  set e := ContinuousLinearMap.restrictScalarsL 𝕜 E F ℝ ℝ
  exact φ.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt_off_countable_real hs hφt
    (dω := fun x ↦ e ∘L dω x)
    (fun a ha b hb hs ↦ e.hasFDerivAt.comp_hasFDerivWithinAt _ (hω a ha b hb hs))
    (e.continuous.comp_continuousOn hωc) hdω_symm hcontdiff

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

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
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω : ∀ a ∈ s, ∀ x ∈ tangentConeAt ℝ s a, ∀ y ∈ tangentConeAt ℝ s a, ((dω a) x) y = ((dω a) y) x
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
φ : (↑(Path.segment a b)).Homotopy ↑(Path.segment a c) :=
  ContinuousMap.Homotopy.affine ↑(Path.segment a b) ↑(Path.segment a c)
x : ↑I × ↑I
⊢ φ x ∈ s

Tactic:
simp [φ, ha, hb, hc, hs.lineMap_mem]

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

Goal state before:
pp: E : Type u_1
mE : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : ProperSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h : Tendsto (fun r ↦ limsup (fun n ↦ (μ n) {x | r < ‖x‖}) atTop) atTop (𝓝 0)
⊢ IsTightMeasureSet (Set.range μ)

Tactic:
simp_rw [isTightMeasureSet_iff_tendsto_measure_norm_gt, iSup_range]
  refine Nat.tendsto_iSup_of_tendsto_limsup (fun n ↦ ?_) h (fun n u v huv ↦ by gcongr)
  have h_tight : IsTightMeasureSet {μ n} := isTightMeasureSet_singleton
  rw [isTightMeasureSet_iff_tendsto_measure_norm_gt] at h_tight
  simpa using h_tight

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

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
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
s : Set E
ω : E → E →L[𝕜] F
inst✝ : CompleteSpace F
hs : Convex ℝ s
hso : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hω : DifferentiableOn ℝ ω s
hdω : ∀ a ∈ s, ∀ (x y : E), ((fderiv ℝ ω a) x) y = ((fderiv ℝ ω a) y) x
⊢ ∃ f, ∀ a ∈ s, HasFDerivAt f (ω a) a

Tactic:
by
  obtain ⟨f, hf⟩ : ∃ f, ∀ a ∈ s, HasFDerivWithinAt f (ω a) s a := by
    refine hs.exists_forall_hasFDerivWithinAt_of_fderivWithin_symmetric hω fun a ha x _ y _ ↦ ?_
    rw [fderivWithin_eq_fderiv, hdω a ha]
    exacts [hso.uniqueDiffOn a ha, hω.differentiableAt (hso.mem_nhds ha)]
  exact ⟨f, fun a ha ↦ (hf a ha).hasFDerivAt (hso.mem_nhds ha)⟩

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

Goal state before:
pp: E : Type u_1
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsFiniteMeasure (μ i)
y : E
h : Tendsto (fun r ↦ limsup (fun n ↦ (μ n) {x | r < ‖⟪(↑‖y‖)⁻¹ • y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
hy : ¬y = 0
⊢ Tendsto (fun r ↦ limsup (fun n ↦ (μ n) {x | ‖y‖⁻¹ * r < ‖⟪(↑‖y‖)⁻¹ • y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)

Tactic:
exact h.comp <| (tendsto_const_mul_atTop_of_pos (by positivity)).mpr tendsto_id

Goal state after: