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

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → E
hf : AEStronglyMeasurable f μ
⊢ ∫ (x : Ω), (f ∘ X) x ∂P = ∫ (x : Ω), f (X x) ∂P

pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → E
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable f (map X P)

Tactic:
Function.comp_def

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → E
hf : AEStronglyMeasurable f μ
⊢ ∫ (x : Ω), (fun x ↦ f (X x)) x ∂P = ∫ (x : Ω), f (X x) ∂P

Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → E
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable f (map X P)
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: case e'_5
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝³ : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝² : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X Y : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst✝¹ : TopologicalSpace E
inst✝ : OpensMeasurableSpace E
T : Ω' → E
hXY : ∀ (i : ι), X i =ᵐ[μ i] Y i
hZT : Z =ᵐ[μ'] T
h : TendstoInDistribution X l Z μ μ'
⊢ ⟨Measure.map T μ', ⋯⟩ = ⟨Measure.map T μ', ⋯⟩

Tactic:
rfl

Goal state after:
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✝ : BorelSpace γ
h : IdentDistrib f g μ ν
hf : Integrable f μ
⊢ Integrable g ν

Tactic:
by
  rw [← memLp_one_iff_integrable] at hf ⊢
  exact h.memLp_snd hf

Goal state after:
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: case e'_3
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g μ ν
⊢ eVar[g; ν] = ∫⁻ (x : β), ↑‖g x - ∫ (x : β), g x ∂ν‖₊ ^ 2 ∂ν

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g μ ν
⊢ eVar[g; ν].toReal = Var[g; ν]

Tactic:
rfl

Goal state after:
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 μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
⊢ x ∈ {x | ⟨C, ⋯⟩ ≤ ‖f i x‖₊} ↔ x ∈ {x | C ≤ ‖f i x‖}

Tactic:
simp_rw [← norm_toNNReal]

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 μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
⊢ x ∈ {x | ⟨C, ⋯⟩ ≤ ‖f i x‖.toNNReal} ↔ x ∈ {x | C ≤ ‖f i x‖}
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : ¬s.Nonempty
⊢ (fun i ↦ if s.Nonempty then sInf ((fun f ↦ ↑f i) '' s) else m) i ≤
    (fun i ↦ if s.Nonempty then sInf ((fun f ↦ ↑f i) '' s) else m) j

pp: case pos
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : s.Nonempty
⊢ (fun i ↦ if s.Nonempty then sInf ((fun f ↦ ↑f i) '' s) else m) i ≤
    (fun i ↦ if s.Nonempty then sInf ((fun f ↦ ↑f i) '' s) else m) j

Tactic:
· simp only [h_nonempty, if_false, le_refl]

Goal state after:
case pos
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
h_nonempty : s.Nonempty
⊢ (fun i ↦ if s.Nonempty then sInf ((fun f ↦ ↑f i) '' s) else m) i ≤
    (fun i ↦ if s.Nonempty then sInf ((fun f ↦ ↑f i) '' s) else m) j
Module: Mathlib.MeasureTheory.Function.Intersectivity

Goal state before:
pp: α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : μ (⋂ n ∈ u, s n) = 0
⊢ x ∈ M ((⋂ n ∈ u, s n).indicator 1)

Tactic:
mem_ofPred,

Goal state after:
α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : μ (⋂ n ∈ u, s n) = 0
⊢ eLpNormEssSup ((⋂ n ∈ u, s n).indicator 1) μ < ↑‖(⋂ n ∈ u, s n).indicator 1 x‖₊
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
h_nonempty : ¬s.Nonempty
⊢ (if s.Nonempty then sInf ((fun f ↦ ↑f i) '' s) else m) ≤ m

pp: case pos
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
h_nonempty : s.Nonempty
⊢ (if s.Nonempty then sInf ((fun f ↦ ↑f i) '' s) else m) ≤ m

Tactic:
· simp only [h_nonempty, if_false, le_refl]

Goal state after:
case pos
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
h_nonempty : s.Nonempty
⊢ (if s.Nonempty then sInf ((fun f ↦ ↑f i) '' s) else m) ≤ m
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this : TopologicalSpace ι := Preorder.topology ι
i : ι
hi : ¬(𝓝[>] i).NeBot
⊢ ↑𝓕 i ≤ m

Tactic:
exact 𝓕.le i

Goal state after:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝³ : (i : ι) → TopologicalSpace (β i)
inst✝² : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝¹ : ∀ (i : ι), BorelSpace (β i)
inst✝ : Preorder ι
u : (i : ι) → Ω → β i
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ ⨆ x, MeasurableSpace.comap (u ↑x) (mβ ↑x) = ⨆ a, MeasurableSpace.comap (u ↑a) inferInstance

Tactic:
rfl

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic

Goal state before:
pp: case mk.mk
M : Type u_1
α : Type u_3
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableConstSMul M α
c : Mᵈᵐᵃ
val✝¹ : α →ₘ[μ] E
a✝¹ : { f // AEStronglyMeasurable f μ }
property✝¹ : Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝¹ ∈ Lp E p μ
val✝ : α →ₘ[μ] E
a✝ : { f // AEStronglyMeasurable f μ }
property✝ : Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝ ∈ Lp E p μ
⊢ c • (⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝¹, property✝¹⟩ + ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝, property✝⟩) =
    c • ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝¹, property✝¹⟩ + c • ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝, property✝⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic

Goal state before:
pp: case mk
M : Type u_1
α : Type u_3
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableConstSMul M α
c : Mᵈᵐᵃ
val✝ : α →ₘ[μ] E
a✝ : { f // AEStronglyMeasurable f μ }
property✝ : Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝ ∈ Lp E p μ
⊢ c • -⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝, property✝⟩ = -(c • ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝, property✝⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic

Goal state before:
pp: case mk.mk
M : Type u_1
α : Type u_3
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableConstSMul M α
c : Mᵈᵐᵃ
val✝¹ : α →ₘ[μ] E
a✝¹ : { f // AEStronglyMeasurable f μ }
property✝¹ : Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝¹ ∈ Lp E p μ
val✝ : α →ₘ[μ] E
a✝ : { f // AEStronglyMeasurable f μ }
property✝ : Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝ ∈ Lp E p μ
⊢ c • (⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝¹, property✝¹⟩ - ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝, property✝⟩) =
    c • ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝¹, property✝¹⟩ - c • ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝, property✝⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic

Goal state before:
pp: case mk.mk
M : Type u_1
N : Type u_2
α : Type u_3
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableConstSMul M α
a✝² : Mᵈᵐᵃ
val✝¹ : α →ₘ[μ] E
a✝¹ : { f // AEStronglyMeasurable f μ }
property✝¹ : Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝¹ ∈ Lp E p μ
val✝ : α →ₘ[μ] E
a✝ : { f // AEStronglyMeasurable f μ }
property✝ : Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝ ∈ Lp E p μ
⊢ a✝² • (⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝¹, property✝¹⟩ + ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝, property✝⟩) =
    a✝² • ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝¹, property✝¹⟩ +
      a✝² • ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝, property✝⟩

Tactic:
rfl

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 : ℕ ≃ ι
n : ℕ
i : ι
hi : ∃ m < n, i = e m
⊢ hi.choose < n + 1

Tactic:
grind

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

Goal state before:
pp: case neg
ι : 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
n : ℕ
b : Fin (n + 1)
hb : ¬↑b < n
⊢ Fin.last n = b

Tactic:
grind

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
g : G
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
inst✝¹ : BorelSpace G
μ : Measure G
inst✝ : μ.IsHaarMeasure
ν : Measure G := haar
int_f_ne_zero : ∀ (μ₀ : Measure G) [μ₀.IsHaarMeasure], ∫ (x : G), f x ∂μ₀ ≠ 0
t : ∫ (x : G), f (x * g) ∂ν = ∫ (x : G), f (x * g) ∂ν.haarScalarFactor μ • μ
r : ↑(ν.haarScalarFactor μ) / ↑(ν.haarScalarFactor μ) = 1
this✝ : MeasurableSpace G := borel G
⊢ ↑(modularCharacterFun g) = ↑((map (fun x ↦ x * g) ν).haarScalarFactor ν)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : μ Eg < ∞
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : μ Ef < ∞
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : μ E < ∞
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (μ E < ∞)
hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
n : ℕ
hn : n ≥ N
hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ
hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3
hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ
⊢ eLpNorm (Eᶜ.indicator g) p μ ≤ eLpNorm (Efᶜ.indicator (Egᶜ.indicator g)) p μ

Tactic:
by
        unfold E; rw [compl_union, ← indicator_indicator]

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 α
inst✝⁵ : TopologicalSpace β✝
inst✝⁴ : Zero β✝
γ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : Zero γ
β : Type u_6
inst✝¹ : PseudoMetricSpace β
inst✝ : Zero β
f : α →C_c β
this : IsCompact (Set.range ⇑f)
C : ℝ
hC : ∀ ⦃x : β⦄, x ∈ Set.range ⇑f → ∀ ⦃y : β⦄, y ∈ Set.range ⇑f → dist x y ≤ C
⊢ ∀ (x y : α), dist (f x) (f y) ≤ C

Tactic:
grind

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
G : Type u_5
inst✝² : FunLike G α β
inst✝¹ : ContinuousMapClass G α β
inst✝ : CompactSpace α
⊢ ∀ (f : G), HasCompactSupport ⇑f

Tactic:
intro f
    exact HasCompactSupport.of_compactSpace f

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 α
Λ : (α →C_c ℝ) →ₚ[ℝ] ℝ
f g : α →C_c ℝ≥0
⊢ NNReal.mk (Λ f.toReal + Λ g.toReal) ⋯ = NNReal.mk (Λ f.toReal) ⋯ + NNReal.mk (Λ g.toReal) ⋯

Tactic:
rfl

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 α
Λ : (α →C_c ℝ) →ₚ[ℝ] ℝ
a : ℝ≥0
f : α →C_c ℝ≥0
⊢ NNReal.mk (↑a * Λ f.toReal) ⋯ = a * NNReal.mk (Λ f.toReal) ⋯

Tactic:
rfl

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

Goal state before:
pp: case e_a
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
x : ℝ
hx : 0 < x
⊢ x * x ^ q * rexp (-x ^ p) = x ^ (q + 1) * rexp (-x ^ p)

Tactic:
rpow_add hx,

Goal state after:
case e_a
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
x : ℝ
hx : 0 < x
⊢ x * x ^ q * rexp (-x ^ p) = x ^ q * x ^ 1 * rexp (-x ^ p)
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e_a
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x : ℝ
hx : 0 < x
⊢ x * x ^ q * rexp (-b * x ^ p) = x ^ (q + 1) * rexp (-b * x ^ p)

Tactic:
rpow_add hx,

Goal state after:
case e_a
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x : ℝ
hx : 0 < x
⊢ x * x ^ q * rexp (-b * x ^ p) = x ^ q * x ^ 1 * rexp (-b * x ^ p)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue

Goal state before:
pp: a✝ b✝ : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
a b : ℝ
hf : ContinuousOn f [[a, b]]
hg : IntervalIntegrable g μ a b
hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), 0 ≤ g x
h : ¬a = b
hab : a < b
s : Set ℝ := Ι a b
hs : s = Ioc a b
hs' : s ⊆ [[a, b]]
hs_conn : IsConnected s
⊢ IntervalIntegrable (fun x ↦ f x * g x) μ a b

Tactic:
exact hg.continuousOn_smul hf

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
⊢ Monotone ⇑Λ

Tactic:
intro f₁ f₂ h
  obtain ⟨g, hg⟩ := CompactlySupportedContinuousMap.exists_add_of_le h
  rw [← hg]
  simp

Goal state after:
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
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), 0 ≤ f x ∧ f x ≤ 1
V : Set X
hV : tsupport ⇑f ⊆ V
⊢ ENNReal.ofReal (Λ f) ≤ (rieszMeasure Λ) (tsupport ⇑f)

Tactic:
have := Content.measure_eq_content_of_regular (rieszContent (toNNRealLinear Λ))
    (contentRegular_rieszContent (toNNRealLinear Λ)) (⟨tsupport f, f.hasCompactSupport⟩)

Goal state after:
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 ℝ
hf : ∀ (x : X), 0 ≤ f x ∧ f x ≤ 1
V : Set X
hV : tsupport ⇑f ⊆ V
this :
  (rieszContent (toNNRealLinear Λ)).measure ↑{ carrier := tsupport ⇑f, isCompact' := ⋯ } =
    (rieszContent (toNNRealLinear Λ)) { carrier := tsupport ⇑f, isCompact' := ⋯ }
⊢ ENNReal.ofReal (Λ f) ≤ (rieszMeasure Λ) (tsupport ⇑f)
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)
n m : Fin N
h : n < m
⊢ a ≤ a

Tactic:
rfl

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)
n m : Fin N
h : n < m
⊢ ε ≤ ε

Tactic:
rfl

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ : (⇑(MeasurableEquiv.funUnique (Fin 1) ℝ).symm ⁻¹' Icc 0 fun x ↦ 2 * π) = Icc 0 (2 * π)
θ : Fin 1 → ℝ
i : Fin 1
⊢ torusMap c R θ 0 = circleMap (c 0) (R 0) (θ 0)

Tactic:
rfl

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

Goal state before:
pp: X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : T2Space X
inst✝⁴ : LocallyCompactSpace X
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
μ ν : Measure X
inst✝¹ : μ.Regular
inst✝ : ν.Regular
hμν : ∀ (f : X →C_c ℝ≥0), ∫ (x : X), ↑(f x) ∂μ = ∫ (x : X), ↑(f x) ∂ν
f : X →C_c ℝ
⊢ ∫ (x : X), ↑(f.nnrealPart x) ∂ν - ∫ (x : X), ↑((-f).nnrealPart x) ∂ν =
    ∫ (a : X), ↑(f a).toNNReal ∂ν - ∫ (a : X), ↑(-f a).toNNReal ∂ν

Tactic:
rfl

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f g : α → α
s : Set α
hs : MeasurableSet s
⊢ g ⁻¹' s = s

Tactic:
hs.2.2

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → α
s : Set α
hs : MeasurableSet s
⊢ s = s
Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
f : α → α
g : α → β
⊢ (∀ ⦃t : Set β⦄, MeasurableSet t → MeasurableSet (g ⁻¹' t)) ↔
    ∀ (x : Set β), MeasurableSet x → MeasurableSet (g ⁻¹' x) ∧ g ∘ f ⁻¹' x = g ⁻¹' x

Tactic:
rfl

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

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyRegularSpace Y
f : X → Y
hf : IsInducing f
x : X
K : Set Y
hK : IsClosed[inst✝¹] K
hxK : f x ∉ K
g : Y → ↑I
hcf : Continuous[inst✝¹, _] g
egfx : g (f x) = 0
hgK : EqOn g 1 K
⊢ 1 = 1 ∘ f

Tactic:
rfl

Goal state after:
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
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := ⋯
K : Set X := ⋯
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < 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 → ℝ := ⋯
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
⊢ μ ↑(V n) ≠ ∞

Tactic:
rw [← lt_top_iff_ne_top]
            apply lt_of_le_of_lt (hV n).2.2
            rw [WithTop.add_lt_top]
            exact ⟨WithTop.lt_top_iff_ne_top.mpr (hE' n), ENNReal.ofReal_lt_top⟩

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
⊢ ↑((fun x ↦ ⟨diracProba x, ⋯⟩) x) = diracProba x

Tactic:
rfl

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

Goal state before:
pp: ι : 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) ε) ⊆ u

Tactic:
by rwa [← ball_pi _ εpos]

Goal state after: