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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁷ : AddCommGroup E
inst✝¹⁶ : UniformSpace E
inst✝¹⁵ : IsUniformAddGroup E
inst✝¹⁴ : AddCommGroup F
inst✝¹³ : UniformSpace F
inst✝¹² : IsUniformAddGroup F
inst✝¹¹ : T0Space F
inst✝¹⁰ : AddCommMonoid Eₗ
inst✝⁹ : UniformSpace Eₗ
inst✝⁸ : ContinuousAdd Eₗ
inst✝⁷ : Semiring 𝕜
inst✝⁶ : Semiring 𝕜₂
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : Module 𝕜 Eₗ
inst✝² : ContinuousConstSMul 𝕜 Eₗ
inst✝¹ : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst✝ : CompleteSpace F
e : E →L[𝕜] Eₗ
h_dense : DenseRange ⇑e
h_e : IsUniformInducing ⇑e
x : E
⊢ (f.extend e) (e x) = f x

Tactic:
simp only [extend, h_dense, h_e, and_self, ↓reduceDIte, coe_mk', LinearMap.coe_mk, AddHom.coe_mk]
  exact IsDenseInducing.extend_eq (h_e.isDenseInducing h_dense) f.cont _

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
y : F
⊢ ∑ z ∈ {y}, μ.real (⇑(const α y) ⁻¹' {z}) • z = μ.real Set.univ • y

Tactic:
simp [Set.preimage]

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝² : MeasurableSpace G := borel G
this✝¹ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this✝ : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n ↦ approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp (⇑(x n)) p μ
h_toLp : ∀ (n : ℕ), ↑↑(MemLp.toLp ⇑(x n) ⋯) =ᵐ[μ] ⇑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
hx_tendsto : Tendsto (fun n ↦ eLpNorm (⇑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
this : Tendsto (fun b ↦ dist ↑((x b).toLp ⋯) ↑g) atTop (𝓝 0)
⊢ Tendsto (fun b ↦ dist (coeSimpleFuncNonnegToLpNonneg p μ G ⟨(x b).toLp ⋯, ⋯⟩) g) atTop (𝓝 0)

Tactic:
Subtype.dist_eq

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝² : MeasurableSpace G := borel G
this✝¹ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this✝ : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n ↦ approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp (⇑(x n)) p μ
h_toLp : ∀ (n : ℕ), ↑↑(MemLp.toLp ⇑(x n) ⋯) =ᵐ[μ] ⇑(x n)
hx_nonneg_Lp : ∀ (n : ℕ), 0 ≤ (x n).toLp ⋯
hx_tendsto : Tendsto (fun n ↦ eLpNorm (⇑(x n) - ↑↑↑g) p μ) atTop (𝓝 0)
this : Tendsto (fun b ↦ dist ↑((x b).toLp ⋯) ↑g) atTop (𝓝 0)
⊢ Tendsto (fun b ↦ dist ↑(coeSimpleFuncNonnegToLpNonneg p μ G ⟨(x b).toLp ⋯, ⋯⟩) ↑g) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
⊢ (setToFun μ (weightedSMul μ) ⋯ fun a ↦ f a + g a) = setToFun μ (weightedSMul μ) ⋯ f + setToFun μ (weightedSMul μ) ⋯ g

Tactic:
exact setToFun_add (dominatedFinMeasAdditive_weightedSMul μ) hf hg

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

Goal state before:
pp: case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ s.indicator (Function.const α x) ⁻¹' {x} = s

Tactic:
indicator_preimage,

Goal state after:
case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ s.ite (Function.const α x ⁻¹' {x}) (0 ⁻¹' {x}) = s
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
huv : Tendsto (u / v) l (𝓝 1)
h : ∃ᶠ (t : α) in l, (u / v) t = 0
⊢ False

Tactic:
simpa using tendsto_nhds_unique_of_frequently_eq (b := 0) huv tendsto_const_nhds h

Goal state after:
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : Type u_3
inst✝ : NormedField β
l : Filter α
L : List ι
f g : ι → α → β
h : ∀ i ∈ L, f i ~[l] g i
⊢ (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) L).prod) ~[l] fun x ↦ (List.map (fun x_1 ↦ g x_1 x) L).prod

Tactic:
induction L with

Goal state after:
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
u v t w : α → ℝ
l : Filter α
hu : 0 ≤ v
hw : 0 ≤ w
htu : u ~[l] v
hvw : t ~[l] w
⊢ u + t ~[l] v + w

Tactic:
simp only [IsEquivalent, add_sub_add_comm]

Goal state after:
α : Type u_1
u v t w : α → ℝ
l : Filter α
hu : 0 ≤ v
hw : 0 ≤ w
htu : u ~[l] v
hvw : t ~[l] w
⊢ (u - v + (t - w)) =o[l] (v + w)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
hf'_nonneg : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), 0 ≤ f' n x
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
⊢ 0 ≤ᵐ[μ] fun x ↦ (F - f 0) x

Tactic:
filter_upwards [h_tendsto, h_mono] with x hx_tendsto hx_mono

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
hf'_nonneg : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), 0 ≤ f' n x
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
x : α
hx_tendsto : Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
hx_mono : Monotone fun n ↦ f n x
⊢ 0 x ≤ (F - f 0) x
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case refine_2.refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : 0 ≤ᵐ[μ] fun x ↦ (F - f 0) x
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
⊢ ∀ (n : ℕ), AEMeasurable (fun a ↦ ENNReal.ofReal (f' n a)) μ

pp: case refine_2.refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : 0 ≤ᵐ[μ] fun x ↦ (F - f 0) x
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
⊢ ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ ENNReal.ofReal (f' n x)

pp: case refine_2.refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : 0 ≤ᵐ[μ] fun x ↦ (F - f 0) x
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal (f' n x)) atTop (𝓝 (ENNReal.ofReal ((F - f 0) x)))

Tactic:
· exact fun n ↦ ((hf n).sub (hf 0)).aemeasurable.ennreal_ofReal

Goal state after:
case refine_2.refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : 0 ≤ᵐ[μ] fun x ↦ (F - f 0) x
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
⊢ ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ ENNReal.ofReal (f' n x)

case refine_2.refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : 0 ≤ᵐ[μ] fun x ↦ (F - f 0) x
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal (f' n x)) atTop (𝓝 (ENNReal.ofReal ((F - f 0) x)))
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → P (s.indicator fun x ↦ c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Integrable f μ → Integrable g μ → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → Integrable f μ → P f → P g
⊢ ∀ ⦃f : α → E⦄, Integrable f μ → P f

Tactic:
simp only [← memLp_one_iff_integrable] at *
  exact MemLp.induction one_ne_top (motive := P) h_ind h_add h_closed h_ae

Goal state after:
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: case h
R : Type u_1
inst✝ : NonUnitalSeminormedRing R
s t : Set R
hs : ∃ C, ∀ ⦃x : R⦄, x ∈ s → ∀ ⦃y : R⦄, y ∈ s → dist x y ≤ C
ht : ∃ C, ∀ ⦃x : R⦄, x ∈ t → ∀ ⦃y : R⦄, y ∈ t → dist x y ≤ C
Af : ℝ
hAf : s ⊆ Metric.closedBall 0 Af
Ag : ℝ
hAg : t ⊆ Metric.closedBall 0 Ag
z : R
hz : z ∈ s * t
w : R
hw : w ∈ s * t
x₁ : R
hx₁ : x₁ ∈ s
y₁ : R
hy₁ : y₁ ∈ t
z_eq : x₁ * y₁ = z
x₂ : R
hx₂ : x₂ ∈ s
y₂ : R
hy₂ : y₂ ∈ t
w_eq : x₂ * y₂ = w
⊢ dist z w ≤ 2 * Af * Ag

Tactic:
rw [← w_eq, ← z_eq, dist_eq_norm]

Goal state after:
case h
R : Type u_1
inst✝ : NonUnitalSeminormedRing R
s t : Set R
hs : ∃ C, ∀ ⦃x : R⦄, x ∈ s → ∀ ⦃y : R⦄, y ∈ s → dist x y ≤ C
ht : ∃ C, ∀ ⦃x : R⦄, x ∈ t → ∀ ⦃y : R⦄, y ∈ t → dist x y ≤ C
Af : ℝ
hAf : s ⊆ Metric.closedBall 0 Af
Ag : ℝ
hAg : t ⊆ Metric.closedBall 0 Ag
z : R
hz : z ∈ s * t
w : R
hw : w ∈ s * t
x₁ : R
hx₁ : x₁ ∈ s
y₁ : R
hy₁ : y₁ ∈ t
z_eq : x₁ * y₁ = z
x₂ : R
hx₂ : x₂ ∈ s
y₂ : R
hy₂ : y₂ ∈ t
w_eq : x₂ * y₂ = w
⊢ ‖x₁ * y₁ - x₂ * y₂‖ ≤ 2 * Af * Ag
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
⊢ IsInducing (⇑UniformFun.ofFun ∘ DFunLike.coe)

Tactic:
by
  rw [isInducing_iff_nhds]
  refine fun f => eq_of_forall_le_iff fun l => ?_
  rw [← tendsto_iff_comap, ← tendsto_id', tendsto_iff_tendstoUniformly,
    UniformFun.tendsto_iff_tendstoUniformly]
  simp [comp_def]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), ‖u (v i)‖₊ ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := ↑v.equivFunL
⊢ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M = Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊

Tactic:
by simp only [smul_mul_assoc, mul_right_comm]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
h : Nonempty α
⊢ ‖f‖ = sInf {C | ∀ (x : α), ‖f x‖ ≤ C}

Tactic:
obtain ⟨a⟩ := h

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
a : α
⊢ ‖f‖ = sInf {C | ∀ (x : α), ‖f x‖ ≤ C}
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : u =O[atTop] fun n ↦ ↑(n ^ k)
⊢ Summable fun n ↦ ‖u n * r ^ n‖

Tactic:
rcases exists_between hr with ⟨r', hrr', h⟩

Goal state after:
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : u =O[atTop] fun n ↦ ↑(n ^ k)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
⊢ Summable fun n ↦ ‖u n * r ^ n‖
Module: Mathlib.Topology.ContinuousMap.Compact

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁸ : TopologicalSpace α
inst✝⁷ : CompactSpace α
inst✝⁶ : PseudoMetricSpace β
inst✝⁵ : SeminormedAddCommGroup E
f✝ g : C(α, β)
C : ℝ
R : Type u_4
inst✝⁴ : Zero R
inst✝³ : Zero β
inst✝² : PseudoMetricSpace R
inst✝¹ : SMul R β
inst✝ : IsBoundedSMul R β
r₁ r₂ : R
f : C(α, β)
⊢ dist (r₁ • f) (r₂ • f) ≤ dist r₁ r₂ * dist f 0

Tactic:
by
    simpa only [← dist_mkOfCompact] using! dist_pair_smul r₁ r₂ (mkOfCompact f)

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

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : r = 0
⊢ eLpNorm f 1 μ ≤ 2 * μ univ * ↑r

pp: case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
⊢ eLpNorm f 1 μ ≤ 2 * μ univ * ↑r

Tactic:
· suffices f =ᵐ[μ] 0 by
      rw [eLpNorm_congr_ae this, eLpNorm_zero, hr, ENNReal.coe_zero, mul_zero]
    rw [hr] at hf
    norm_cast at hf
    have hnegf : ∫ x, -f x ∂μ = 0 := by
      rw [integral_neg, neg_eq_zero]
      exact le_antisymm (integral_nonpos_of_ae hf) hfint'
    have := (integral_eq_zero_iff_of_nonneg_ae ?_ hfint.neg).1 hnegf
    · filter_upwards [this] with ω hω
      rwa [Pi.neg_apply, Pi.zero_apply, neg_eq_zero] at hω
    · filter_upwards [hf] with ω hω
      rwa [Pi.zero_apply, Pi.neg_apply, Right.nonneg_neg_iff]

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
⊢ eLpNorm f 1 μ ≤ 2 * μ univ * ↑r
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
h_le : infEDist y E * (↑δ.toNNReal)⁻¹ ≤ 1
⊢ infEDist y E * (↑δ.toNNReal)⁻¹ - infEDist x E * (↑δ.toNNReal)⁻¹ ≤ (↑δ.toNNReal)⁻¹ * edist x y

Tactic:
by
      rw [← ENNReal.sub_mul (by simp [δ_pos]), mul_comm, edist_comm]
      gcongr
      simp only [tsub_le_iff_right]
      exact infEDist_le_edist_add_infEDist

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : Integrable f (μ + μ')
⊢ μ ≤ 1 • (μ + μ')

Tactic:
rw [one_smul]

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : Integrable f (μ + μ')
⊢ μ ≤ μ + μ'
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ' T C
f : α → E
hf : Integrable f (μ + μ')
⊢ μ' ≤ 1 • (μ + μ')

Tactic:
rw [one_smul]

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ' T C
f : α → E
hf : Integrable f (μ + μ')
⊢ μ' ≤ μ + μ'
Module: Mathlib.MeasureTheory.Integral.Marginal

Goal state before:
pp: δ : Type u_1
X : δ → Type u_3
inst✝² : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f g : ((i : δ) → X i) → ℝ≥0∞
hst : s ⊆ t
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ
⊢ ∫⋯∫⁻_t, f ∂μ = ∫⋯∫⁻_t, g ∂μ

Tactic:
by
  rw [← union_sdiff_of_subset hst, lmarginal_union' μ f hf disjoint_sdiff,
    lmarginal_union' μ g hg disjoint_sdiff, hfg]

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
f : α → β
a : α
⊢ β

Tactic:
haveI : Nonempty β := ⟨f a⟩
  letI : TopologicalSpace α := Preorder.topology α
  exact if 𝓝[<] a = ⊥ ∨ ¬∃ y, Tendsto f (𝓝[<] a) (𝓝 y) then f a else limUnder (𝓝[<] a) f

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] x).NeBot
⊢ leftLim f x ≤ f y

Tactic:
leftLim_eq_sSup hf

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] x).NeBot
⊢ sSup (f '' Iio x) ≤ f y
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] y).NeBot
⊢ f x ≤ leftLim f y

Tactic:
leftLim_eq_sSup hf

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] y).NeBot
⊢ f x ≤ sSup (f '' Iio y)
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set X
μ : Measure X
hs : ∀ᵐ (x : X) ∂μ, x ∈ s
f : X → E
⊢ ∫ (x : X), f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
rw [← setIntegral_univ, ← setIntegral_congr_set]

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set X
μ : Measure X
hs : ∀ᵐ (x : X) ∂μ, x ∈ s
f : X → E
⊢ s =ᵐ[μ] univ
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case inr
R : Type u_1
inst✝⁶ : LinearOrder R
inst✝⁵ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁴ : OrderTopology R
inst✝³ : CompactIccSpace R
inst✝² : MeasurableSpace R
inst✝¹ : BorelSpace R
inst✝ : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ i, t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), f.length (t i) < ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
hR : Nonempty R
⊢ ∃ s, t i ⊆ s ∧ MeasurableSet s ∧ f.outer s ≤ f.length (t i) + ofReal ↑(ε' i)

Tactic:
have hl :=
        ENNReal.lt_add_right ((ENNReal.le_tsum i).trans_lt h).ne (ENNReal.coe_pos.2 (ε'0 i)).ne'

Goal state after:
case inr
R : Type u_1
inst✝⁶ : LinearOrder R
inst✝⁵ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁴ : OrderTopology R
inst✝³ : CompactIccSpace R
inst✝² : MeasurableSpace R
inst✝¹ : BorelSpace R
inst✝ : DenselyOrdered R
s : Set R
t : ℕ → Set R
ht : s ⊆ ⋃ i, t i
ε : ℝ≥0
ε0 : 0 < ε
h : ∑' (i : ℕ), f.length (t i) < ∞
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
hR : Nonempty R
hl : f.length (t i) < f.length (t i) + ↑(ε' i)
⊢ ∃ s, t i ⊆ s ∧ MeasurableSet s ∧ f.outer s ≤ f.length (t i) + ofReal ↑(ε' i)
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s : Set X
μ : Measure X
inst✝ : CompleteSpace E
c : E
⊢ ∫ (x : X) in s, c ∂μ = μ.real s • c

Tactic:
rw [integral_const, measureReal_restrict_apply_univ]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
h1t : ∅ ∈ {t | ↑K ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V}
g : G
hg : g ∈ interior ↑K
⊢ False

Tactic:
change g ∈ (∅ : Set G)

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
h1t : ∅ ∈ {t | ↑K ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V}
g : G
hg : g ∈ interior ↑K
⊢ g ∈ ∅
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a : R
⊢ f.measure {a} = ofReal (↑f a - leftLim (↑f) a)

Tactic:
by_cases ha : IsBot a

Goal state after:
case pos
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a : R
ha : IsBot a
⊢ f.measure {a} = ofReal (↑f a - leftLim (↑f) a)

case neg
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a : R
ha : ¬IsBot a
⊢ f.measure {a} = ofReal (↑f a - leftLim (↑f) a)
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁸ : LinearOrder R
inst✝⁷ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁶ : OrderTopology R
inst✝⁵ : CompactIccSpace R
inst✝⁴ : MeasurableSpace R
inst✝³ : BorelSpace R
inst✝² : SecondCountableTopology R
inst✝¹ : DenselyOrdered R
inst✝ : Nonempty R
hf : Tendsto (↑f) atBot atBot
⊢ f.measure univ = ∞

Tactic:
inhabit R
  rw [← top_le_iff, ← f.measure_Iio_of_tendsto_atBot_atBot hf default]
  exact measure_mono (subset_univ _)

Goal state after: