mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NontrivialTopology E
f : E →SL[σ₁₂] F
a : ℝ
hf : ∀ (x : E), ‖f x‖ = a * ‖x‖
x : E
hx : 0 < ‖x‖
ha : 0 ≤ a
⊢ a ≤ ‖f‖

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NontrivialTopology E
f : E →SL[σ₁₂] F
a : ℝ
hf : ∀ (x : E), ‖f x‖ = a * ‖x‖
x : E
hx : 0 < ‖x‖
ha : 0 ≤ a
⊢ a ≤ ‖f‖
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : NontriviallyNormedField 𝕜₃
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup F
inst✝⁷ : SeminormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜₂ F
inst✝⁴ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomIsometric σ₁₂
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : RingHomIsometric σ₁₃
h : F →SL[σ₂₃] G
f : E →SL[σ₁₂] F
⊢ ‖h ∘SL f‖ₑ ≤ ‖h‖ₑ * ‖f‖ₑ

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : NontriviallyNormedField 𝕜₃
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup F
inst✝⁷ : SeminormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜₂ F
inst✝⁴ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomIsometric σ₁₂
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : RingHomIsometric σ₁₃
h : F →SL[σ₂₃] G
f : E →SL[σ₁₂] F
⊢ ‖h ∘SL f‖₊ ≤ ‖h‖₊ * ‖f‖₊
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
⊢ ∃ x, r * ‖x‖₊ < ‖f x‖₊

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
⊢ ∃ x, r * ‖x‖₊ < ‖f x‖₊
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
F : Type u_7
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑q
⊢ ∃ C, 0 < C ∧ ∀ (x : F), q x ≤ C * ‖x‖

Tactic:
have hq' : Tendsto q (𝓝 0) (𝓝 0) := map_zero q ▸ hq.tendsto 0
  rcases NormedAddGroup.nhds_zero_basis_norm_lt.mem_iff.mp (hq' <| Iio_mem_nhds one_pos)
    with ⟨ε, ε_pos, hε⟩
  rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
  have : 0 < ‖c‖ / ε := by positivity
  refine ⟨‖c‖ / ε, this, fun x ↦ ?_⟩
  by_cases hx : ‖x‖ = 0
  · rw [hx, mul_zero]
    exact le_of_eq (map_eq_zero_of_norm_eq_zero q hq hx)
  · refine (normSeminorm 𝕜 F).bound_of_shell q ε_pos hc (fun x hle hlt ↦ ?_) hx
    refine (le_of_lt <| show q x < _ from hε hlt).trans ?_
    rwa [← div_le_iff₀' this, one_div_div]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ
hr : r < ‖f‖
hr₀ : r < 0
⊢ ‖0‖ < 1 ∧ r < ‖f 0‖

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ
hr : r < ‖f‖
hr₀ : r < 0
⊢ r < 0
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : DenselyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
r : ℝ≥0
hr✝ : r < ‖f‖₊
x : E
hlt : ‖x‖₊ < 1
hr : r < ‖f x‖₊
hx0 : 0 < ‖x‖₊
this : r < ‖x‖₊⁻¹ * ‖f x‖₊
⊢ ‖(algebraMap ℝ 𝕜) ‖x‖⁻¹ • x‖₊ = 1 ∧ r < ‖f ((algebraMap ℝ 𝕜) ‖x‖⁻¹ • x)‖₊

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : DenselyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
r : ℝ≥0
hr✝ : r < ‖f‖₊
x : E
hlt : ‖x‖₊ < 1
hr : r < ‖f x‖₊
hx0 : 0 < ‖x‖₊
this : r < ‖x‖₊⁻¹ * ‖f x‖₊
⊢ r < ‖x‖₊⁻¹ * ‖f x‖₊
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝ g✝ h✝ : α → β
inst✝² : Mul β
inst✝¹ : LE β
inst✝ : ExistsMulOfLE β
x y : l.Germ β
f g : α → β
h : f ≤ᶠ[l] g
c : (x : α) → f x ≤ g x → β
hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx
⊢ ∃ c, ↑g = ↑f * c

Tactic:
refine ⟨ofFun fun x ↦ if hx : f x ≤ g x then c x hx else f x, coe_eq.2 ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝ g✝ h✝ : α → β
inst✝² : Mul β
inst✝¹ : LE β
inst✝ : ExistsMulOfLE β
x y : l.Germ β
f g : α → β
h : f ≤ᶠ[l] g
c : (x : α) → f x ≤ g x → β
hc : ∀ (x : α) (hx : f x ≤ g x), g x = f x * c x hx
⊢ g =ᶠ[l] (fun f g x ↦ (fun x1 x2 ↦ x1 * x2) (f x) (g x)) f fun x ↦ if hx : f x ≤ g x then c x hx else f x
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 σ₂₃
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
⊢ ‖f.flip‖ ≤ ‖f‖

Tactic:
simpa using

Goal state after:
𝕜 : 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 σ₂₃
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
⊢ ‖f.flip‖ ≤ ‖f‖
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ ≪ μ[|univ]

Tactic:
rw [cond, restrict_univ]
  refine absolutelyContinuous_smul ?_
  simp [measure_ne_top]

Goal state after:
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
s : Set Ω
hms : MeasurableSet s
μ : Measure Ω
t : Set Ω
⊢ (μ s)⁻¹ • μ (t ∩ s) = (μ s)⁻¹ * μ (s ∩ t)

Tactic:
Set.inter_comm,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
s : Set Ω
hms : MeasurableSet s
μ : Measure Ω
t : Set Ω
⊢ (μ s)⁻¹ • μ (s ∩ t) = (μ s)⁻¹ * μ (s ∩ t)
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
ht : MeasurableSet t
μ : Measure Ω
⊢ (μ s)⁻¹ • μ (t ∩ s) = (μ s)⁻¹ * μ (s ∩ t)

Tactic:
Set.inter_comm,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
ht : MeasurableSet t
μ : Measure Ω
⊢ (μ s)⁻¹ • μ (s ∩ t) = (μ s)⁻¹ * μ (s ∩ t)
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case e'_3
f : Filter ℝ
hf : ¬IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
⊢ {a | ∀ᶠ (n : ℝ) in f, n ≤ a} = ∅

Tactic:
simpa using

Goal state after:
case e'_3
f : Filter ℝ
hf : ¬IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
⊢ ∀ (x : ℝ), ∃ᶠ (x_1 : ℝ) in f, x < x_1
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hs₀ : μ s ≠ 0
hs : μ s ≠ ∞
⊢ μ[s | s] = 1

Tactic:
simpa using

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hs₀ : μ s ≠ 0
hs : μ s ≠ ∞
⊢ (μ s)⁻¹ * μ s = 1
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case e'_3
f : Filter ℝ
hf : ¬IsBounded (fun x1 x2 ↦ x1 ≥ x2) f
⊢ {a | ∀ᶠ (n : ℝ) in f, a ≤ n} = ∅

Tactic:
simpa using

Goal state after:
case e'_3
f : Filter ℝ
hf : ¬IsBounded (fun x1 x2 ↦ x1 ≥ x2) f
⊢ ∀ (x : ℝ), ∃ᶠ (x_1 : ℝ) in f, x_1 < x
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ[t | s] = (μ s)⁻¹ * μ (t ∩ s)

Tactic:
Set.inter_comm,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ[t | s] = (μ s)⁻¹ * μ (s ∩ t)
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
inst✝ : f.NeBot
b : ℝ
hb : ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, ↑(u a_1) ≤ a) → b ≤ a
x : ℝ
x✝ : 0 ≤ x
⊢ (∀ᶠ (a : ι) in f, ↑(u a) ≤ ↑(NNReal.mk x x✝)) → ↑(NNReal.mk ↑b.toNNReal ⋯) ≤ ↑(NNReal.mk x x✝)

Tactic:
simpa using

Goal state after:
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
inst✝ : f.NeBot
b : ℝ
hb : ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, ↑(u a_1) ≤ a) → b ≤ a
x : ℝ
x✝ : 0 ≤ x
⊢ (∀ᶠ (a : ι) in f, ↑(u a) ≤ x) → b ≤ x
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case e'_2
f : Filter ℝ≥0
hf : ¬IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
⊢ {a | ∀ᶠ (n : ℝ≥0) in f, n ≤ a} = ∅

Tactic:
simpa using

Goal state after:
case e'_2
f : Filter ℝ≥0
hf : ¬IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
⊢ ∀ (x : ℝ≥0), ∃ᶠ (x_1 : ℝ≥0) in f, x < x_1
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case pos
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
c r : ℝ
hr : r < c
⊢ (∀ᶠ (a : ι) in f, r < ↑(u a)) ↔ 0 ≤ r → ∀ᶠ (a : ι) in f, r < ↑(u a)

Tactic:
simpa using

Goal state after:
case pos
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
c r : ℝ
hr : r < c
⊢ 0 ≤ r ∨ ∀ᶠ (a : ι) in f, r < ↑(u a)
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case pos
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf✝ : f.NeBot
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
c r : ℝ
hr : r < c
⊢ (∃ᶠ (a : ι) in f, r < ↑(u a)) ↔ 0 ≤ r → ∃ᶠ (a : ι) in f, r < ↑(u a)

Tactic:
simpa using

Goal state after:
case pos
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf✝ : f.NeBot
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
c r : ℝ
hr : r < c
⊢ 0 ≤ r ∨ ∃ᶠ (a : ι) in f, r < ↑(u a)
Module: Mathlib.Order.Filter.ENNReal

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

Tactic:
simpa using

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

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

Tactic:
simpa using

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

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

Tactic:
simpa using

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

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
⊢ limsup (fun x ↦ u x * a) f = a * limsup u f

Tactic:
simpa using

Goal state after:
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
⊢ limsup (fun x ↦ a * u x) f = a * limsup u f
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u v : α → ℝ≥0∞
⊢ limsup (u * v) f ≤ limsup (fun x ↦ limsup u f * v x) f

Tactic:
refine limsup_le_limsup ?_
      filter_upwards [@eventually_le_limsup _ f _ u] with x hx using mul_le_mul' hx le_rfl

Goal state after:
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > ↑r, ∀ᶠ (a : α) in f, u a < y
x : ℝ≥0
hx : some x > ↑r
⊢ ↑x > ↑r

Tactic:
simpa using

Goal state after:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > ↑r, ∀ᶠ (a : α) in f, u a < y
x : ℝ≥0
hx : some x > ↑r
⊢ r < x
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case inl
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > ↑r, ∀ᶠ (a : α) in f, u a < y
x : ℝ≥0
hx : some x > ↑r
a : α
ha : u a < ↑x
ha₀ : u a ≤ 0
⊢ ENNReal.ofReal (u a) < some x

Tactic:
simpa using

Goal state after:
case inl
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > ↑r, ∀ᶠ (a : α) in f, u a < y
x : ℝ≥0
hx : some x > ↑r
a : α
ha : u a < ↑x
ha₀ : u a ≤ 0
⊢ 0 < x
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > ↑r, ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y
x : ℝ
hx : x > ↑r
this : 0 < x
⊢ ENNReal.ofReal x > ↑r

Tactic:
simpa using

Goal state after:
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > ↑r, ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y
x : ℝ
hx : x > ↑r
this : 0 < x
⊢ ↑r < x
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
hf : f.NeBot
this✝ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
h : ∀ y > ENNReal.ofReal r, ∀ᶠ (a : α) in f, u a < y
x : ℝ
hx : x > r
this : 0 < x
⊢ ENNReal.ofReal x > ENNReal.ofReal r

Tactic:
simpa using

Goal state after:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
hf : f.NeBot
this✝ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
h : ∀ y > ENNReal.ofReal r, ∀ᶠ (a : α) in f, u a < y
x : ℝ
hx : x > r
this : 0 < x
⊢ r < x
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: case a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ univ.pi C
i : ι
⊢ MeasurableSet (eval i ⁻¹' s i)

Tactic:
apply @measurable_pi_apply _ _ (fun i => generateFrom (C i))

Goal state after:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ univ.pi C
i : ι
⊢ MeasurableSet (s i)
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
h : ∀ y > r, ∀ᶠ (a : α) in f, (u a).toReal < y
x : ℝ≥0
hx : some x > ENNReal.ofReal r
⊢ ↑x > r

Tactic:
simpa using

Goal state after:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
hf : f.NeBot
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
h : ∀ y > r, ∀ᶠ (a : α) in f, (u a).toReal < y
x : ℝ≥0
hx : some x > ENNReal.ofReal r
⊢ r < ↑x
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : #⋯.toFinset = #hsf.toFinset
⊢ ⋯.toFinset = hsf.toFinset

Tactic:
exact Finset.eq_of_subset_of_card_le (Set.Finite.toFinset_mono s.inter_subset_left) h.ge

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) f
r : ℝ≥0∞
⊢ r ≤ ⨅ a ∈ fun x ↦ (map f (ae μ)).sets {x_1 | (fun x_2 ↦ (fun x1 x2 ↦ x1 ≤ x2) x_2 x) x_1}, ↑a ↔
    r ≤ essSup (fun x ↦ ↑(f x)) μ

Tactic:
simp [essSup, limsup, limsSup, eventually_map, ENNReal.forall_ennreal]; rfl

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: δ : Type u_4
X : δ → Type u_5
inst✝¹ : (i : δ) → MeasurableSpace (X i)
l : List δ
μ : (i : δ) → Measure (X i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (X i)
⊢ (Measure.tprod l μ) (Set.tprod l s) = (List.map (fun i ↦ (μ i) (s i)) l).prod

Tactic:
induction l with
  | nil => simp
  | cons a l ih =>
    rw [tprod_cons, Set.tprod]
    simp only [foldr_cons, prod_cons, map_cons]
    rw [prod_prod, ih]

Goal state after:
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
t : ℝ
ht : t ≠ 0
hf : AEMeasurable (fun x ↦ rexp (t * f x)) μ
⊢ AEMeasurable f μ

Tactic:
simpa using

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
μ : Measure α
t : ℝ
ht : t ≠ 0
hf : AEMeasurable (fun x ↦ rexp (t * f x)) μ
⊢ AEMeasurable f μ
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
f : (i : ι) → α i
⊢ (Measure.pi μ) {f} = ∏ i, (μ i) {f i}

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
f : (i : ι) → α i
⊢ (Measure.pi μ) {f} = ∏ i, (μ i) {f i}
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
α : ι✝ → Type u_3
inst✝⁷ : Fintype ι✝
m : (i : ι✝) → OuterMeasure (α i)
inst✝⁶ : (i : ι✝) → MeasurableSpace (α i)
μ✝ : (i : ι✝) → Measure (α i)
inst✝⁵ : ∀ (i : ι✝), SigmaFinite (μ✝ i)
ι : Type u_4
inst✝⁴ : Fintype ι
X : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (X i)
inst✝² : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : ∀ (i : ι), IsUnifLocDoublingMeasure (μ i)
r : ℝ
hr :
  ∀ (i : ι) (x : X i),
    (μ i) (Metric.closedBall x (2 * r)) ≤
      ↑(IsUnifLocDoublingMeasure.doublingConstant (μ i)) * (μ i) (Metric.closedBall x r)
hr₀ : 0 < r
x : (i : ι) → X i
⊢ (Measure.pi μ) (Metric.closedBall x (2 * r)) ≤
    ↑(∏ i, IsUnifLocDoublingMeasure.doublingConstant (μ i)) * (Measure.pi μ) (Metric.closedBall x r)

Tactic:
simpa using

Goal state after:
ι✝ : Type u_1
ι' : Type u_2
α : ι✝ → Type u_3
inst✝⁷ : Fintype ι✝
m : (i : ι✝) → OuterMeasure (α i)
inst✝⁶ : (i : ι✝) → MeasurableSpace (α i)
μ✝ : (i : ι✝) → Measure (α i)
inst✝⁵ : ∀ (i : ι✝), SigmaFinite (μ✝ i)
ι : Type u_4
inst✝⁴ : Fintype ι
X : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (X i)
inst✝² : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : ∀ (i : ι), IsUnifLocDoublingMeasure (μ i)
r : ℝ
hr :
  ∀ (i : ι) (x : X i),
    (μ i) (Metric.closedBall x (2 * r)) ≤
      ↑(IsUnifLocDoublingMeasure.doublingConstant (μ i)) * (μ i) (Metric.closedBall x r)
hr₀ : 0 < r
x : (i : ι) → X i
⊢ ∏ i, (μ i) (Metric.closedBall (x i) (2 * r)) ≤
    (∏ i, ↑(IsUnifLocDoublingMeasure.doublingConstant (μ i))) * ∏ i, (μ i) (Metric.closedBall (x i) r)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : (fun a ↦ ‖g a‖ₑ ^ p) =ᵐ[μ] 0
x : α
hx : (fun a ↦ ‖g a‖ₑ ^ p) x = 0 x
⊢ ‖g x‖ₑ = 0

Tactic:
simpa using

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : (fun a ↦ ‖g a‖ₑ ^ p) =ᵐ[μ] 0
x : α
hx : (fun a ↦ ‖g a‖ₑ ^ p) x = 0 x
⊢ ‖g x‖ₑ = 0
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : eLpNorm' g p μ = 0
this✝ : ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = 0
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ

Tactic:
simpa using

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : eLpNorm' g p μ = 0
this✝ : ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = 0
⊢ eLpNorm' f p μ = 0
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case hfq
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hfp : eLpNorm f p μ < ∞
⊢ eLpNorm' f p.toReal μ < ∞

Tactic:
simpa using

Goal state after:
case hfq
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hfp : eLpNorm f p μ < ∞
⊢ eLpNorm' f p.toReal μ < ∞