mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : 𝐤X → Y
⊢ Continuous[instTopologicalSpace, inst✝] f ↔
    ∀ (K : Set X), IsCompact K → ContinuousOn (f ∘ ⇑(CompactCoherentification.mk X)) K

Tactic:
[

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : 𝐤X → Y
⊢ Continuous[instTopologicalSpace, inst✝] f ↔
    ∀ (K : Set X), IsCompact K → ContinuousOn (f ∘ ⇑(CompactCoherentification.mk X)) K
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : ∀ (K : Set X), IsCompact K → ContinuousOn f K
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] (CompactCoherentification.map f)

Tactic:
[

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : ∀ (K : Set X), IsCompact K → ContinuousOn f K
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] (CompactCoherentification.map f)
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
A : Set X
hA : IsCompact A
f : X → Y
⊢ ContinuousOn (⇑(CompactCoherentification.mk Y) ∘ f) A ↔ ContinuousOn f A

Tactic:
[

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
A : Set X
hA : IsCompact A
f : X → Y
⊢ ContinuousOn (⇑(CompactCoherentification.mk Y) ∘ f) A ↔ ContinuousOn f A
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup F
inst✝⁷ : SeminormedAddCommGroup G
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NontriviallyNormedField 𝕜₃
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₂] F
g : E →SL[σ₁₃] G
h : ∀ (x : E), ‖f x‖ = ‖g x‖
x : E
⊢ ‖g x‖ ≤ ‖g‖ * ‖x‖

Tactic:
exact le_opNorm _ _

Goal state after:
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f✝ f : C(α, β)
l : Filter C(α, β)
⊢ l ≤ 𝓝 f ↔ l ≤ 𝓝 f

Tactic:
[

Goal state after:
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f✝ f : C(α, β)
l : Filter C(α, β)
⊢ l ≤ 𝓝 f ↔ l ≤ 𝓝 f
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝³ : TopologicalSpace α
inst✝² : UniformSpace β
δ₁ : Type u_1
δ₂ : Type u_2
inst✝¹ : TopologicalSpace δ₁
inst✝ : TopologicalSpace δ₂
φ₁ : C(δ₁, α)
φ₂ : C(δ₂, α)
h_proper₁ : IsProperMap ⇑φ₁
h_proper₂ : IsProperMap ⇑φ₂
h_cover : range ⇑φ₁ ∪ range ⇑φ₂ = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗₁ : Set (Set δ₁) := {K | IsCompact K}
𝔗₂ : Set (Set δ₂) := {K | IsCompact K}
h_image₁ : MapsTo (fun x ↦ ⇑φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ ⇑φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ ⇑φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ ⇑φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover' : ∀ S ∈ 𝔖, S ⊆ range ⇑φ₁ ∪ range ⇑φ₂
⊢ inferInstance =
    UniformSpace.comap (fun x ↦ x.comp φ₁) inferInstance ⊓ UniformSpace.comap (fun x ↦ x.comp φ₂) inferInstance

Tactic:
[

Goal state after:
α : Type u₁
β : Type u₂
inst✝³ : TopologicalSpace α
inst✝² : UniformSpace β
δ₁ : Type u_1
δ₂ : Type u_2
inst✝¹ : TopologicalSpace δ₁
inst✝ : TopologicalSpace δ₂
φ₁ : C(δ₁, α)
φ₂ : C(δ₂, α)
h_proper₁ : IsProperMap ⇑φ₁
h_proper₂ : IsProperMap ⇑φ₂
h_cover : range ⇑φ₁ ∪ range ⇑φ₂ = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗₁ : Set (Set δ₁) := {K | IsCompact K}
𝔗₂ : Set (Set δ₂) := {K | IsCompact K}
h_image₁ : MapsTo (fun x ↦ ⇑φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ ⇑φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ ⇑φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ ⇑φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover' : ∀ S ∈ 𝔖, S ⊆ range ⇑φ₁ ∪ range ⇑φ₂
⊢ inferInstance =
    UniformSpace.comap (fun x ↦ x.comp φ₁) inferInstance ⊓ UniformSpace.comap (fun x ↦ x.comp φ₂) inferInstance
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i ↦ range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun i ↦ {K | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun x ↦ ⇑(φ i) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ ⇑(φ i) ⁻¹' x) 𝔖 (𝔗 i)
S : Set α
hS : S ∈ 𝔖
⊢ (⋃ i ∈ {i | (range ⇑(φ i) ∩ S).Nonempty}, range ⇑(φ i)) ∩ S = S

Tactic:
[

Goal state after:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i ↦ range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun i ↦ {K | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun x ↦ ⇑(φ i) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ ⇑(φ i) ⁻¹' x) 𝔖 (𝔗 i)
S : Set α
hS : S ∈ 𝔖
⊢ (⋃ i ∈ {i | (range ⇑(φ i) ∩ S).Nonempty}, range ⇑(φ i)) ∩ S = S
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i ↦ range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun i ↦ {K | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun x ↦ ⇑(φ i) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ ⇑(φ i) ⁻¹' x) 𝔖 (𝔗 i)
h_cover' : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range ⇑(φ i)
⊢ inferInstance = ⨅ i, UniformSpace.comap (fun x ↦ x.comp (φ i)) inferInstance

Tactic:
[

Goal state after:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i ↦ range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun i ↦ {K | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun x ↦ ⇑(φ i) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ ⇑(φ i) ⁻¹' x) 𝔖 (𝔗 i)
h_cover' : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range ⇑(φ i)
⊢ inferInstance = ⨅ i, UniformSpace.comap (fun x ↦ x.comp (φ i)) inferInstance
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case pos
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : a = 0
⊢ limsup (fun x ↦ a * u x) f = a * limsup u f

Tactic:
[

Goal state after:
case pos
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : a = 0
⊢ limsup (fun x ↦ a * u x) f = a * limsup u f
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case pos
α : Type u_1
f : Filter α
inst✝ : f.NeBot
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : a = 0
⊢ liminf (fun x ↦ a * u x) f = a * liminf u f

Tactic:
[

Goal state after:
case pos
α : Type u_1
f : Filter α
inst✝ : f.NeBot
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : a = 0
⊢ liminf (fun x ↦ a * u x) f = a * liminf u f
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
⊢ ∑ x, μ (X ⁻¹' {x}) * μ[E | X ⁻¹' {x}] = ∑ x, μ (X ⁻¹' {x} ∩ E)

Tactic:
[

Goal state after:
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
⊢ ∑ x, μ (X ⁻¹' {x}) * μ[E | X ⁻¹' {x}] = ∑ x, μ (X ⁻¹' {x} ∩ E)
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
this : ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E = E
⊢ μ (⋃ b ∈ Finset.univ, X ⁻¹' {b} ∩ E) = μ E

pp: Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
this : ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E = E
⊢ (↑Finset.univ).PairwiseDisjoint fun x ↦ X ⁻¹' {x} ∩ E

Tactic:
this

Goal state after:
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
this : ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E = E
⊢ μ E = μ E

Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
this : ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E = E
⊢ (↑Finset.univ).PairwiseDisjoint fun x ↦ X ⁻¹' {x} ∩ E
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: case intro
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), ⋃ n, s i n = univ
val✝ : Encodable (ι → ℕ)
e : ℕ → ι → ℕ := fun n ↦ (decode n).getD default
⊢ (⋃ n, univ.pi fun i ↦ s i (e n i)) = univ

Tactic:
[

Goal state after:
case intro
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
s : (i : ι) → ℕ → Set (α i)
h1s : ∀ (i : ι) (n : ℕ), s i n ∈ C i
h2s : ∀ (i : ι), ⋃ n, s i n = univ
val✝ : Encodable (ι → ℕ)
e : ℕ → ι → ℕ := fun n ↦ (decode n).getD default
⊢ (⋃ n, univ.pi fun i ↦ s i (e n i)) = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
⊢ MeasurableSet ((fun b ↦ b i) ⁻¹' s)

Tactic:
[

Goal state after:
case intro.a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
⊢ MeasurableSet ((fun b ↦ b i) ⁻¹' s)
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
⊢ x✝ ∈ univ.pi (update (fun i' ↦ iUnion (t i')) i (⋃ x, s)) ↔ x✝ ∈ univ.pi fun k ↦ ⋃ j, update (fun i' ↦ t i' j) i s k

Tactic:
[

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set (α i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
⊢ x✝ ∈ univ.pi (update (fun i' ↦ iUnion (t i')) i (⋃ x, s)) ↔ x✝ ∈ univ.pi fun k ↦ ⋃ j, update (fun i' ↦ t i' j) i s k
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : ConditionallyCompleteLattice β
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : Module R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
f : α → β
⊢ essSup f (c • μ) = essSup f μ

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : ConditionallyCompleteLattice β
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : Module R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
f : α → β
⊢ essSup f (c • μ) = essSup f μ
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : ConditionallyCompleteLattice β
c : ℝ≥0∞
hc : c ≠ 0
f : α → β
⊢ essSup f (c • μ) = essSup f μ

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : ConditionallyCompleteLattice β
c : ℝ≥0∞
hc : c ≠ 0
f : α → β
⊢ essSup f (c • μ) = essSup f μ
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : ConditionallyCompleteLinearOrder β
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology β
inst✝ : OrderTopology β
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) f
⊢ μ {y | essSup f μ < f y} = 0

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : ConditionallyCompleteLinearOrder β
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology β
inst✝ : OrderTopology β
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) f
⊢ μ {y | essSup f μ < f y} = 0
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : ConditionallyCompleteLinearOrder β
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology β
inst✝ : OrderTopology β
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) (ae μ) f
⊢ μ {y | f y < essInf f μ} = 0

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : ConditionallyCompleteLinearOrder β
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology β
inst✝ : OrderTopology β
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) (ae μ) f
⊢ μ {y | f y < essInf f μ} = 0
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case inr.inl
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : univ.pi s = ∅
⊢ piPremeasure m (univ.pi s) = ∏ i, (m i) (s i)

pp: case inr.inr
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : (univ.pi s).Nonempty
⊢ piPremeasure m (univ.pi s) = ∏ i, (m i) (s i)

Tactic:
· rcases univ_pi_eq_empty_iff.mp h with ⟨i, hi⟩
    have : ∃ i, m i (s i) = 0 := ⟨i, by simp [hi]⟩
    simpa [h, Finset.card_univ, zero_pow Fintype.card_ne_zero, @eq_comm _ (0 : ℝ≥0∞),
      Finset.prod_eq_zero_iff, piPremeasure]

Goal state after:
case inr.inr
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h✝ : Nonempty ι
h : (univ.pi s).Nonempty
⊢ piPremeasure m (univ.pi s) = ∏ i, (m i) (s i)
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : Preorder ι
f : ι → α → ℝ≥0∞
⊢ essSup (fun x ↦ liminf (fun n ↦ f n x) atTop) μ ≤ liminf (fun n ↦ essSup (fun x ↦ f n x) μ) atTop

Tactic:
[

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : Preorder ι
f : ι → α → ℝ≥0∞
⊢ essSup (fun x ↦ liminf (fun n ↦ f n x) atTop) μ ≤ liminf (fun n ↦ essSup (fun x ↦ f n x) μ) atTop
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Defs

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
inst✝ : ENorm ε
μ : Measure α
f : α → ε
⊢ eLpNorm f 1 μ = ∫⁻ (x : α), ‖f x‖ₑ ∂μ

Tactic:
[

Goal state after:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
inst✝ : ENorm ε
μ : Measure α
f : α → ε
⊢ eLpNorm f 1 μ = ∫⁻ (x : α), ‖f x‖ₑ ∂μ
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯
b' : β := Classical.choose h
this : const α b = mk (Function.const α b') ⋯
⊢ Function.const α b' x = b

Tactic:
[

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯
b' : β := Classical.choose h
this : const α b = mk (Function.const α b') ⋯
⊢ Function.const α b' x = b
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯
b' : β := Classical.choose h
this : b = b'
⊢ b' = b

Tactic:
this

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯
b' : β := Classical.choose h
this : b = b'
⊢ b' = b'
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
μ ν : Measure α
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : TopologicalSpace β
inst✝⁵ : TopologicalSpace γ
𝕜 : Type u_5
𝕜' : Type u_6
inst✝⁴ : SMul 𝕜 γ
inst✝³ : ContinuousConstSMul 𝕜 γ
inst✝² : SMul 𝕜' γ
inst✝¹ : ContinuousConstSMul 𝕜' γ
inst✝ : SMulCommClass 𝕜 𝕜' γ
a : 𝕜
b : 𝕜'
f✝ : α →ₘ[μ] γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ a • b • mk f hf = b • a • mk f hf

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
μ ν : Measure α
inst✝⁷ : TopologicalSpace δ
inst✝⁶ : TopologicalSpace β
inst✝⁵ : TopologicalSpace γ
𝕜 : Type u_5
𝕜' : Type u_6
inst✝⁴ : SMul 𝕜 γ
inst✝³ : ContinuousConstSMul 𝕜 γ
inst✝² : SMul 𝕜' γ
inst✝¹ : ContinuousConstSMul 𝕜' γ
inst✝ : SMulCommClass 𝕜 𝕜' γ
a : 𝕜
b : 𝕜'
f✝ : α →ₘ[μ] γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ a • b • mk f hf = b • a • mk f hf
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁹ : MeasurableSpace α
μ ν : Measure α
inst✝⁸ : TopologicalSpace δ
inst✝⁷ : TopologicalSpace β
inst✝⁶ : TopologicalSpace γ
𝕜 : Type u_5
𝕜' : Type u_6
inst✝⁵ : SMul 𝕜 γ
inst✝⁴ : ContinuousConstSMul 𝕜 γ
inst✝³ : SMul 𝕜' γ
inst✝² : ContinuousConstSMul 𝕜' γ
inst✝¹ : SMul 𝕜 𝕜'
inst✝ : IsScalarTower 𝕜 𝕜' γ
a : 𝕜
b : 𝕜'
f✝ : α →ₘ[μ] γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ (a • b) • mk f hf = a • b • mk f hf

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁹ : MeasurableSpace α
μ ν : Measure α
inst✝⁸ : TopologicalSpace δ
inst✝⁷ : TopologicalSpace β
inst✝⁶ : TopologicalSpace γ
𝕜 : Type u_5
𝕜' : Type u_6
inst✝⁵ : SMul 𝕜 γ
inst✝⁴ : ContinuousConstSMul 𝕜 γ
inst✝³ : SMul 𝕜' γ
inst✝² : ContinuousConstSMul 𝕜' γ
inst✝¹ : SMul 𝕜 𝕜'
inst✝ : IsScalarTower 𝕜 𝕜' γ
a : 𝕜
b : 𝕜'
f✝ : α →ₘ[μ] γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ (a • b) • mk f hf = a • b • mk f hf
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁹ : MeasurableSpace α
μ ν : Measure α
inst✝⁸ : TopologicalSpace δ
inst✝⁷ : TopologicalSpace β
inst✝⁶ : TopologicalSpace γ
𝕜 : Type u_5
𝕜' : Type u_6
inst✝⁵ : SMul 𝕜 γ
inst✝⁴ : ContinuousConstSMul 𝕜 γ
inst✝³ : SMul 𝕜' γ
inst✝² : ContinuousConstSMul 𝕜' γ
inst✝¹ : SMul 𝕜ᵐᵒᵖ γ
inst✝ : IsCentralScalar 𝕜 γ
a : 𝕜
f✝ : α →ₘ[μ] γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ MulOpposite.op a • mk f hf = a • mk f hf

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁹ : MeasurableSpace α
μ ν : Measure α
inst✝⁸ : TopologicalSpace δ
inst✝⁷ : TopologicalSpace β
inst✝⁶ : TopologicalSpace γ
𝕜 : Type u_5
𝕜' : Type u_6
inst✝⁵ : SMul 𝕜 γ
inst✝⁴ : ContinuousConstSMul 𝕜 γ
inst✝³ : SMul 𝕜' γ
inst✝² : ContinuousConstSMul 𝕜' γ
inst✝¹ : SMul 𝕜ᵐᵒᵖ γ
inst✝ : IsCentralScalar 𝕜 γ
a : 𝕜
f✝ : α →ₘ[μ] γ
f : α → γ
hf : AEStronglyMeasurable f μ
⊢ MulOpposite.op a • mk f hf = a • mk f hf
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
hf : Measurable fun x ↦ rexp (f x)
this : f = fun x ↦ log (rexp (f x))
⊢ Measurable f

Tactic:
this

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
hf : Measurable fun x ↦ rexp (f x)
this : f = fun x ↦ log (rexp (f x))
⊢ Measurable fun x ↦ log (rexp (f x))
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ piPremeasure (fun i ↦ (μ i).toOuterMeasure) (t ∩ (fun b ↦ b i) ⁻¹' s) +
      piPremeasure (fun i ↦ (μ i).toOuterMeasure) (t \ (fun b ↦ b i) ⁻¹' s) ≤
    piPremeasure (fun i ↦ (μ i).toOuterMeasure) t

Tactic:
[

Goal state after:
ι : Type u_1
α : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
i : ι
s : Set (α i)
hs : MeasurableSet s
t : Set ((a : ι) → α a)
⊢ piPremeasure (fun i ↦ (μ i).toOuterMeasure) (t ∩ (fun b ↦ b i) ⁻¹' s) +
      piPremeasure (fun i ↦ (μ i).toOuterMeasure) (t \ (fun b ↦ b i) ⁻¹' s) ≤
    piPremeasure (fun i ↦ (μ i).toOuterMeasure) t
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable (fun x ↦ rexp (f x)) μ
this : f = fun x ↦ log (rexp (f x))
⊢ AEMeasurable f μ

Tactic:
this

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
hf : AEMeasurable (fun x ↦ rexp (f x)) μ
this : f = fun x ↦ log (rexp (f x))
⊢ AEMeasurable (fun x ↦ log (rexp (f x))) μ
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝⁴ : TopologicalSpace β
inst✝³ : Lattice β
inst✝² : TopologicalLattice β
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
f : α →ₘ[μ] β
⊢ ↑|f| =ᵐ[μ] fun x ↦ |↑f x|

Tactic:
[

Goal state after:
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝⁴ : TopologicalSpace β
inst✝³ : Lattice β
inst✝² : TopologicalLattice β
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
f : α →ₘ[μ] β
⊢ ↑|f| =ᵐ[μ] fun x ↦ |↑f x|
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: case refine_1
⊢ Measurable fun p ↦ ↑p.1 ^ p.2

Tactic:
[

Goal state after:
case refine_1
⊢ Measurable fun p ↦ ↑p.1 ^ p.2
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: case refine_2
⊢ Measurable fun x ↦ ∞ ^ x

Tactic:
[

Goal state after:
case refine_2
⊢ Measurable fun x ↦ ∞ ^ x
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
this : Encodable ι
⊢ ∏ i, (μ i) (s i) ≤ (Measure.pi μ) (univ.pi s)

Tactic:
[

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), MeasurableSet (s i)
this : Encodable ι
⊢ ∏ i, (μ i) (s i) ≤ (Measure.pi μ) (univ.pi s)