mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: case refine_3
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
h_le :
  ∀ (n : ι),
    |∫ (ω : E), F ω ∂Measure.map (Y n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'| ≤
      ↑L * (ε / 2) + M * μ''.real {ω | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |∫ (ω : E), F ω ∂Measure.map (X n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'|
⊢ Tendsto (fun n ↦ |∫ (ω : E), F ω ∂Measure.map (X n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'|) l (𝓝 0)

Tactic:
replace hXZ := hXZ.tendsto

Goal state after:
case refine_3
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ✝ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
h_le :
  ∀ (n : ι),
    |∫ (ω : E), F ω ∂Measure.map (Y n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'| ≤
      ↑L * (ε / 2) + M * μ''.real {ω | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |∫ (ω : E), F ω ∂Measure.map (X n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'|
hXZ : Tendsto (fun n ↦ ⟨Measure.map (X n) μ'', ⋯⟩) l (𝓝 ⟨Measure.map Z μ', ⋯⟩)
⊢ Tendsto (fun n ↦ |∫ (ω : E), F ω ∂Measure.map (X n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'|) l (𝓝 0)
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
h_le :
  ∀ (n : ι),
    |∫ (ω : E), F ω ∂Measure.map (Y n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'| ≤
      ↑L * (ε / 2) + M * μ''.real {ω | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |∫ (ω : E), F ω ∂Measure.map (X n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'|
h_tendsto :
  Tendsto
    (fun n ↦
      ↑L * (ε / 2) + M * μ''.real {ω | ε / 2 ≤ ‖Y n ω - X n ω‖} +
        |∫ (ω : E), F ω ∂Measure.map (X n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'|)
    l (𝓝 (↑L * ε / 2))
⊢ 0 < ↑L * ε

Tactic:
positivity

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : BorelSpace X
inst✝⁸ : R1Space X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
inst✝⁴ : R1Space Y
μ : Measure X
ν : Measure Y
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure ν
E : Type u_3
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
hp₀ : p ≠ 0
f : ↥(simpleFunc E p ν)
⊢ Continuous[_, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] fun y ↦
    (compMeasurePreserving ⇑↑(↑f, y).2 ⋯) (↑f, y).1

Tactic:
induction f using Lp.simpleFunc.induction hp₀ hp with

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst✝¹ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst✝ : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Infinite ι
e : ℕ ≃ ι
g : (n : ℕ) → ι → Fin (n + 1) := fun n i ↦ if hi : ∃ m < n, i = e m then ⟨hi.choose, ⋯⟩ else Fin.last n
sg : ∀ (n : ℕ), Function.Surjective (g n)
G : (n : ℕ) → IndexedPartition fun k ↦ ⋃ i ∈ g n ⁻¹' {k}, s i
x : α
y : ℕ
hy : e y = hs.index x
b : ℕ
hb : y + 1 ≤ b
this : y = ↑⟨y, ⋯⟩
⊢ x ∈ ⋃ i ∈ g b ⁻¹' {⟨y, ⋯⟩}, s i

Tactic:
have : ∃ m < b, hs.index x = e m := ⟨y, ⟨by lia, hy.symm⟩⟩

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst✝¹ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst✝ : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Infinite ι
e : ℕ ≃ ι
g : (n : ℕ) → ι → Fin (n + 1) := fun n i ↦ if hi : ∃ m < n, i = e m then ⟨hi.choose, ⋯⟩ else Fin.last n
sg : ∀ (n : ℕ), Function.Surjective (g n)
G : (n : ℕ) → IndexedPartition fun k ↦ ⋃ i ∈ g n ⁻¹' {k}, s i
x : α
y : ℕ
hy : e y = hs.index x
b : ℕ
hb : y + 1 ≤ b
this✝ : y = ↑⟨y, ⋯⟩
this : ∃ m < b, hs.index x = e m
⊢ x ∈ ⋃ i ∈ g b ⁻¹' {⟨y, ⋯⟩}, s i
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : Finite ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
n : ℕ
hn : Nonempty (ι ≃ Fin n)
⊢ ∃ s, μ s ≠ ∞ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
set g : Fin n → α → β := f ∘ hn.some.symm

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : Finite ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
n : ℕ
hn : Nonempty (ι ≃ Fin n)
g : Fin n → α → β := f ∘ ⇑hn.some.symm
⊢ ∃ s, μ s ≠ ∞ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers

Goal state before:
pp: E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯.choose
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun n ↦ (1 + u n) • K
Z : ℕ → Set E := fun n ↦ ↑(S n) ∩ (↑L \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
⊢ 0 ≤ 1 + ↑(u n)

Tactic:
positivity

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

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : 0 ≤ a
x : α
⊢ max (a * f x) 0 = a * max (f x) 0

Tactic:
rcases le_total 0 (f x) with hfx | hfx

Goal state after:
case inl
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : 0 ≤ a
x : α
hfx : 0 ≤ f x
⊢ max (a * f x) 0 = a * max (f x) 0

case inr
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : 0 ≤ a
x : α
hfx : f x ≤ 0
⊢ max (a * f x) 0 = a * max (f x) 0
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : a ≤ 0
x : α
⊢ max (a * f x) 0 = max (-a) 0 * max (-f x) 0

Tactic:
rcases le_total 0 (f x) with hfx | hfx

Goal state after:
case inl
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : a ≤ 0
x : α
hfx : 0 ≤ f x
⊢ max (a * f x) 0 = max (-a) 0 * max (-f x) 0

case inr
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : a ≤ 0
x : α
hfx : f x ≤ 0
⊢ max (a * f x) 0 = max (-a) 0 * max (-f x) 0
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case hx
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 < b

Tactic:
positivity

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

Goal state before:
pp: p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ p ≠ 0

Tactic:
positivity

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

Goal state before:
pp: case hx
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b

Tactic:
positivity

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

Goal state before:
pp: p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 0 ≤ b ^ p⁻¹

Tactic:
positivity

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

Goal state before:
pp: p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ 0 < b ^ p⁻¹

Tactic:
positivity

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

Goal state before:
pp: case hx
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ 0 < b

Tactic:
positivity

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

Goal state before:
pp: case hx
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ 0 ≤ b

Tactic:
positivity

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

Goal state before:
pp: p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ 0 < p

Tactic:
positivity

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 c : E
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
⊢ 0 ≤ 1 / 2

Tactic:
positivity

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‖
y : E
hy : y ∈ ball a ε
⊢ 0 ≤ ‖y - a‖ ^ (r + 1)

Tactic:
positivity

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‖
y : E
hy : y ∈ ball a ε
⊢ 0 ≤ ‖y - a‖

Tactic:
positivity

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‖
y : E
hy : y ∈ ball a ε
⊢ r + 1 ≠ 0

Tactic:
positivity

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‖
y : E
hy : y ∈ ball a ε
hsub : closedBall a ‖y - a‖ ⊆ ball a ε
z : E
hz : z ∈ closedBall a ‖y - a‖
⊢ 0 ≤ ‖z - a‖ ^ r

Tactic:
positivity

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

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
h_f_int : IntervalIntegrable f volume a (a + ↑N * h)
k✝ : ℕ
hk✝ : k✝ < N
h_pos : 0 ≤ h
k : ℕ
hk : ↑k ≤ ↑N
⊢ 0 ≤ ↑k * h

Tactic:
positivity

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : Disjoint s₀ s₁
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
⊢ x ∈ ⋃ j, if j = 0 then s₀ᶜ else s₁ᶜ

Tactic:
rw [mem_iUnion]

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : Disjoint s₀ s₁
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
⊢ ∃ i, x ∈ if i = 0 then s₀ᶜ else s₁ᶜ
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
⊢ 0 < h

Tactic:
positivity

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
k : ℕ
hk : k < N
⊢ 0 ≤ ↑k * h

Tactic:
positivity

Goal state after:
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₁ K₂ : Compacts X
disj : Disjoint ↑K₁ ↑K₂
b : ℝ≥0
f : X →C_c ℝ≥0
hf : f ∈ {f | ∀ x ∈ K₁ ⊔ K₂, 1 ≤ f x}
Λf_eq_b : Λ f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, x ∈ support ⇑f
hsubsuppf : ↑K₁ ∪ ↑K₂ ⊆ tsupport ⇑f
g₁ g₂ : X →C_c ℝ≥0
hg₁ : EqOn (⇑g₁) 1 K₁.carrier
hg₂ : EqOn (⇑g₂) 1 K₂.carrier
sum_g : EqOn (⇑(g₁ + g₂)) 1 (tsupport f.toFun)
f_eq_sum : f = g₁ * f + g₂ * f
aux₁ : ∀ x ∈ K₁, 1 ≤ (g₁ * f) x
⊢ ∀ x ∈ K₂, 1 ≤ (g₂ * f) x

Tactic:
intro x x_in_K₂

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint ↑K₁ ↑K₂
b : ℝ≥0
f : X →C_c ℝ≥0
hf : f ∈ {f | ∀ x ∈ K₁ ⊔ K₂, 1 ≤ f x}
Λf_eq_b : Λ f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, x ∈ support ⇑f
hsubsuppf : ↑K₁ ∪ ↑K₂ ⊆ tsupport ⇑f
g₁ g₂ : X →C_c ℝ≥0
hg₁ : EqOn (⇑g₁) 1 K₁.carrier
hg₂ : EqOn (⇑g₂) 1 K₂.carrier
sum_g : EqOn (⇑(g₁ + g₂)) 1 (tsupport f.toFun)
f_eq_sum : f = g₁ * f + g₂ * f
aux₁ : ∀ x ∈ K₁, 1 ≤ (g₁ * f) x
x : X
x_in_K₂ : x ∈ K₂
⊢ 1 ≤ (g₂ * f) x
Module: Mathlib.MeasureTheory.Integral.TorusIntegral

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
C : ℝ
hf : ∀ (θ : Fin n → ℝ), ‖f (torusMap c R θ)‖ ≤ C
θ : Fin n → ℝ
x✝ : θ ∈ Icc 0 fun x ↦ 2 * π
⊢ 0 ≤ ∏ i, |R i|

Tactic:
positivity

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
z : ℝ
n : ℕ
hn : n < N
x✝¹ : a + ↑n * ε < z
x✝ : z ≤ a + ↑(n + 1) * ε
⊢ z ≤ a + ε * (↑↑⟨n, hn⟩ + 1)

Tactic:
by simp_all [mul_comm ε _]

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

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x ↦ ℝ) i).symm
hem : MeasurePreserving (⇑e) volume volume
heπ : (⇑e ⁻¹' Icc 0 fun x ↦ 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x ↦ 2 * π
⊢ ∫ (x : ℝ × (Fin n → ℝ)) in Icc 0 (2 * π) ×ˢ Icc 0 fun x ↦ 2 * π,
      (∏ i, ↑(R i) * cexp (↑(e x i) * I) * I) • f (torusMap c R (e x)) ∂volume =
    ∮ (x : ℂ) in C(c i, R i), ∯ (y : Fin n → ℂ) in T(c ∘ i.succAbove, R ∘ i.succAbove), f (i.insertNth x y)

Tactic:
Measure.volume_eq_prod,

Goal state after:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x ↦ ℝ) i).symm
hem : MeasurePreserving (⇑e) volume volume
heπ : (⇑e ⁻¹' Icc 0 fun x ↦ 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x ↦ 2 * π
⊢ ∫ (x : ℝ × (Fin n → ℝ)) in Icc 0 (2 * π) ×ˢ Icc 0 fun x ↦ 2 * π,
      (∏ i, ↑(R i) * cexp (↑(e x i) * I) * I) • f (torusMap c R (e x)) ∂volume.prod volume =
    ∮ (x : ℂ) in C(c i, R i), ∯ (y : Fin n → ℂ) in T(c ∘ i.succAbove, R ∘ i.succAbove), f (i.insertNth x y)
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ max (#↑s) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
⊢ Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (max (#↑s) 2 ^ ℵ₀)

Tactic:
rw [lift_power, lift_aleph0]
      rw [← Ordinal.lift_le.{u}, lift_omega, Ordinal.lift_one, ← ord_aleph] at hi
      have H := card_le_of_le_ord hi
      rw [← Ordinal.lift_card] at H
      apply H.trans <| aleph_one_le_continuum.trans <| power_le_power_right _
      rw [lift_max, Cardinal.lift_ofNat]
      exact le_max_right _ _

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

Goal state before:
pp: W : Type u_1
inst✝¹¹ : AddCommGroup W
inst✝¹⁰ : Module ℝ W
inst✝⁹ : TopologicalSpace W
e : AddChar ℝ Circle
V : Type u_2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module ℝ V
inst✝⁶ : PseudoEMetricSpace V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : CompleteSpace V
inst✝² : SecondCountableTopology V
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
he' : e ≠ 1
hL' : ∀ (v : V), v ≠ 0 → L v ≠ 0
hL : Continuous fun p ↦ (L p.1) p.2
P P' : Measure V
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
h : ∀ (w : W), ∫ (v : V), (char he hL w) v ∂P = ∫ (v : V), (char he hL w) v ∂P'
g✝ : V →ᵇ ℂ
w : AddMonoidAlgebra ℂ W
hw : ⇑g✝ = fun x ↦ w.coeff.sum fun a z ↦ z * ↑(e ((L x) a))
⊢ ∫ (x : V), (fun x ↦ w.coeff.sum fun a z ↦ z * ↑(e ((L x) a))) x ∂P =
    ∫ (x : V), (fun x ↦ w.coeff.sum fun a z ↦ z * ↑(e ((L x) a))) x ∂P'

Tactic:
have hsum (P : Measure V) [IsFiniteMeasure P] :
      ∫ v, w.coeff.sum (fun a z ↦ z * e (L v a)) ∂P =
        w.coeff.sum (fun a z ↦ ∫ v, z * e (L v a) ∂P) :=
    integral_finsetSum _ fun a ha ↦ ((char he hL a).integrable P).const_mul  _

Goal state after:
W : Type u_1
inst✝¹¹ : AddCommGroup W
inst✝¹⁰ : Module ℝ W
inst✝⁹ : TopologicalSpace W
e : AddChar ℝ Circle
V : Type u_2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module ℝ V
inst✝⁶ : PseudoEMetricSpace V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : CompleteSpace V
inst✝² : SecondCountableTopology V
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
he' : e ≠ 1
hL' : ∀ (v : V), v ≠ 0 → L v ≠ 0
hL : Continuous fun p ↦ (L p.1) p.2
P P' : Measure V
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
h : ∀ (w : W), ∫ (v : V), (char he hL w) v ∂P = ∫ (v : V), (char he hL w) v ∂P'
g✝ : V →ᵇ ℂ
w : AddMonoidAlgebra ℂ W
hw : ⇑g✝ = fun x ↦ w.coeff.sum fun a z ↦ z * ↑(e ((L x) a))
hsum :
  ∀ (P : Measure V) [IsFiniteMeasure P],
    ∫ (v : V), w.coeff.sum fun a z ↦ z * ↑(e ((L v) a)) ∂P = w.coeff.sum fun a z ↦ ∫ (v : V), z * ↑(e ((L v) a)) ∂P
⊢ ∫ (x : V), (fun x ↦ w.coeff.sum fun a z ↦ z * ↑(e ((L x) a))) x ∂P =
    ∫ (x : V), (fun x ↦ w.coeff.sum fun a z ↦ z * ↑(e ((L x) a))) x ∂P'
Module: Mathlib.MeasureTheory.Measure.DiracProba

Goal state before:
pp: X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhds : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
⊢ interior U ∈ 𝓝 x

Tactic:
simpa only [interior_mem_nhds] using U_nhds

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

Goal state before:
pp: p : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ p)
ι : 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 ℝ (PiLp p E)
⊢ ∫ (v : WithLp p ((i : ι) → E i)), cexp (↑(L v) * I) ∂Measure.map (toLp p) (Measure.pi μ) =
    ∫ (x : (i : ι) → E i),
      cexp
        (∑ x_1,
          ↑((L ∘SL ↑(PiLp.continuousLinearEquiv p ℝ E).symm ∘SL ContinuousLinearMap.single ℝ E x_1) (x x_1)) *
            I) ∂Measure.pi μ

Tactic:
← Finset.sum_mul,

Goal state after:
p : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ p)
ι : 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 ℝ (PiLp p E)
⊢ ∫ (v : WithLp p ((i : ι) → E i)), cexp (↑(L v) * I) ∂Measure.map (toLp p) (Measure.pi μ) =
    ∫ (x : (i : ι) → E i),
      cexp
        ((∑ i, ↑((L ∘SL ↑(PiLp.continuousLinearEquiv p ℝ E).symm ∘SL ContinuousLinearMap.single ℝ E i) (x i))) *
          I) ∂Measure.pi μ
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    0 < ε →
      ε < ∞ →
        MeasurableSet B → μ B ≤ ν (thickening (δ + ε).toReal B) + δ + ε ∧ ν B ≤ μ (thickening (δ + ε).toReal B) + δ + ε
ε : ℝ≥0
hε : 0 < ε
a✝ : δ < ∞
ε_top : ¬↑ε = ∞
B : Set Ω
B_mble : MeasurableSet B
⊢ 0 < ↑ε

Tactic:
positivity

Goal state after: