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

Goal state before:
pp: case inr.const
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
c : E
s : Set α
hs : MeasurableSet s
⊢ ∀ (δ : ℝ≥0∞),
    δ ≠ 0 →
      MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p μ →
        ∃ g, eLpNorm (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) - g) p μ ≤ δ ∧ P g

Tactic:
ε

Goal state after:
case inr.const
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε✝ : ℝ≥0∞
hε : ε✝ ≠ 0
hp_pos : p ≠ 0
c : E
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
⊢ ε ≠ 0 →
    MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p μ →
      ∃ g, eLpNorm (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) - g) p μ ≤ ε ∧ P g
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case 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
⊢ ∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ ≠ ∞

pp: case 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) ∂μ)
⊢ Tendsto (fun n ↦ (∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ).toReal) atTop
    (𝓝 (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ).toReal)

Tactic:
· rw [← ofReal_integral_eq_lintegral_ofReal (hF.sub (hf 0)) hF_ge]
    finiteness

Goal state after:
case 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) ∂μ)
⊢ Tendsto (fun n ↦ (∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ).toReal) atTop
    (𝓝 (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ).toReal)
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹⁴ : Ring S
inst✝¹³ : Ring R
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module R V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module R W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : Module S W
inst✝⁴ : SMulCommClass R S W
inst✝³ : ContinuousConstSMul S W
inst✝² : AddTorsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalAddTorsor Q
f : V →ᴬ[R] Q
x : V
⊢ f.contLinear x +ᵥ Function.const V (f 0) x = f x

Tactic:
Function.const_apply,

Goal state after:
R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹⁴ : Ring S
inst✝¹³ : Ring R
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module R V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module R W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : Module S W
inst✝⁴ : SMulCommClass R S W
inst✝³ : ContinuousConstSMul S W
inst✝² : AddTorsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalAddTorsor Q
f : V →ᴬ[R] Q
x : V
⊢ f.contLinear x +ᵥ f 0 = f x
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))

Tactic:
let F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))
Module: Mathlib.Topology.Instances.Matrix

Goal state before:
pp: X : Type u_1
n : Type u_5
R : Type u_8
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace R
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : IsTopologicalRing R
A : X → Matrix n n R
hA : Continuous A
⊢ Continuous fun x ↦ (A x).det

Tactic:
Matrix.det_apply

Goal state after:
X : Type u_1
n : Type u_5
R : Type u_8
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace R
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : IsTopologicalRing R
A : X → Matrix n n R
hA : Continuous A
⊢ Continuous fun x ↦ ∑ σ, Equiv.Perm.sign σ • ∏ i, A x (σ i) i
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)
h_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f' i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone fun i ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
h1 : (fun i ↦ f i a) = fun i ↦ (f' i a).toReal + f 0 a
⊢ 0 ≤ F a - f 0 a

Tactic:
simp [ha_bound 0]

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

Goal state before:
pp: case e_f
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSingletonClass X
μ : Measure X
inst✝ : Countable X
hf : Integrable f (Measure.sum fun a ↦ μ {a} • Measure.dirac a)
a : X
⊢ ∫ (x : X), f x ∂μ {a} • Measure.dirac a = (Measure.sum fun a ↦ μ {a} • Measure.dirac a).real {a} • f a

Tactic:
rw [integral_smul_measure, integral_dirac, Measure.sum_smul_dirac, measureReal_def]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f g : ↥(Lp H 1 μ)
⊢ dist f g = ∫ (a : α), dist (↑↑f a) (↑↑g a) ∂μ

Tactic:
simp only [dist_eq_norm, L1.norm_eq_integral_norm]
  exact integral_congr_ae <| (Lp.coeFn_sub _ _).fun_comp norm

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

Goal state before:
pp: case inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
h✝ : IsEmpty α
⊢ dist f g = sSup ∅

Tactic:
Real.sSup_empty,

Goal state after:
case inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
h✝ : IsEmpty α
⊢ dist f g = 0
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x ↦ ‖f x‖ₑ) * fun x ↦ ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q) ≠ ∞

Tactic:
refine ENNReal.mul_ne_top ?_ ?_

Goal state after:
case refine_1.refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x ↦ ‖f x‖ₑ) * fun x ↦ ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) ≠ ∞

case refine_1.refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x ↦ ‖f x‖ₑ) * fun x ↦ ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q) ≠ ∞
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case neg
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
⊢ ∀ ε > 0, ∃ δ > 0, ∀ (a : ↥(Lp G 1 μ)), dist a f < δ → dist (Integrable.toL1 ↑↑a ⋯) (Integrable.toL1 ↑↑f ⋯) < ε

Tactic:
ε

Goal state after:
case neg
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
⊢ ε > 0 → ∃ δ > 0, ∀ (a : ↥(Lp G 1 μ)), dist a f < δ → dist (Integrable.toL1 ↑↑a ⋯) (Integrable.toL1 ↑↑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 : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
x : (i : δ) → X i
e : ((i : ↥s) → X ↑i) × ((i : ↥t) → X ↑i) ≃ᵐ ((i : ↥(s ∪ t)) → X ↑i) := ⋯
⊢ Measurable fun z ↦ f (updateFinset x (s ∪ t) ((MeasurableEquiv.piFinsetUnion X hst) z))

Tactic:
exact hf.comp <| measurable_updateFinset.comp e.measurable

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
⊢ leftLim (rightLim f) a = leftLim f a

Tactic:
by
  obtain ⟨b, hb⟩ : (Iio a).Nonempty := Filter.nonempty_of_mem (self_mem_nhdsWithin (a := a))
  apply leftLim_eq_of_tendsto
  apply (closed_nhds_basis (f.leftLim a)).tendsto_right_iff.2
  rintro s ⟨s_mem, s_closed⟩
  obtain ⟨u, au, hu⟩ : ∃ u, u < a ∧ Ioo u a ⊆ {x | f x ∈ s} := by
    have := (closed_nhds_basis (f.leftLim a)).tendsto_right_iff.1 h s ⟨s_mem, s_closed⟩
    simpa using (mem_nhdsLT_iff_exists_Ioo_subset' hb).1 this
  filter_upwards [Ioo_mem_nhdsLT au] with c hc
  rcases eq_or_neBot (𝓝[>] c) with h'c | h'c
  · simpa [h'c, rightLim_eq_of_eq_bot] using hu hc
  by_cases! h''c : ¬ ∃ y, Tendsto f (𝓝[>] c) (𝓝 y)
  · simpa [rightLim_eq_of_not_tendsto _ h''c] using hu hc
  apply s_closed.mem_of_tendsto (tendsto_rightLim_of_tendsto h''c)
  filter_upwards [Ioo_mem_nhdsGT_of_mem ⟨hc.1.le, hc.2⟩] with d hd using hu hd

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : T3Space β
inst✝ : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
s : Set β
s_mem : s ∈ 𝓝 b
s_closed : IsClosed[inst✝⁴] s
u : α
hu : ∀ (b : α), u ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s
a : α
ha : u < a
⊢ g a ∈ id s

Tactic:
apply s_closed.mem_of_mapClusterPt (hu a ha.le).1

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : T3Space β
inst✝ : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
s : Set β
s_mem : s ∈ 𝓝 b
s_closed : IsClosed[inst✝⁴] s
u : α
hu : ∀ (b : α), u ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s
a : α
ha : u < a
⊢ ∀ᶠ (x : α) in 𝓝 a, f x ∈ s
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
f : R → ℝ
hf : Monotone f
⊢ ∀ (x : R), ContinuousWithinAt (rightLim f) (Ici x) x

Tactic:
intro x s hs
    change ∀ᶠ y in 𝓝[≥] x, rightLim f y ∈ s
    obtain ⟨l, u, hlu, lus⟩ : ∃ l u : ℝ, rightLim f x ∈ Ioo l u ∧ Ioo l u ⊆ s :=
      mem_nhds_iff_exists_Ioo_subset.1 hs
    by_cases! hx : ∀ y, y ≤ x
    · filter_upwards [self_mem_nhdsWithin] with y (hy : x ≤ y)
      rw [show y = x by exact le_antisymm (hx y) hy]
      exact lus hlu
    rcases hx with ⟨y₀, hy₀⟩
    obtain ⟨y, xy, h'y⟩ : ∃ (y : R), x < y ∧ Ioo x y ⊆ f ⁻¹' Ioo l u :=
      (mem_nhdsGT_iff_exists_Ioo_subset' hy₀).1 (hf.tendsto_rightLim x (Ioo_mem_nhds hlu.1 hlu.2))
    filter_upwards [Ico_mem_nhdsGE xy] with z hz
    apply lus
    refine ⟨hlu.1.trans_le (hf.rightLim hz.1), ?_⟩
    rcases hz.1.eq_or_lt with rfl | h''z
    · exact hlu.2
    rcases Filter.eq_or_neBot (𝓝[>] z) with h'z | h'z
    · rw [rightLim_eq_of_eq_bot _ h'z]
      have : z ∈ Ioo x y := ⟨h''z, hz.2⟩
      exact (h'y this).2
    · obtain ⟨a, za, ay⟩ : ∃ a : R, z < a ∧ a < y := Filter.nonempty_of_mem (Ioo_mem_nhdsGT hz.2)
      calc
        rightLim f z ≤ f a := hf.rightLim_le za
        _ < u := (h'y ⟨hz.1.trans_lt za, ay⟩).2

Goal state after:
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
a : R
c d : ℕ → R
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R), Icc a b ⊆ ⋃ i ∈ ↑t, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : R
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Iotop (c x) (d x)
is : i ∈ s
bcd : b ∈ Ioc (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ofReal (↑f (d i) - ↑f (c i)) + ofReal (↑f (c i) - ↑f a)

pp: case a
R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a : R
c d : ℕ → R
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R), Icc a b ⊆ ⋃ i ∈ ↑t, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : R
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Iotop (c x) (d x)
is : i ∈ s
bcd : b ∈ Ioc (c i) (d i)
⊢ Icc a (c i) ⊆ ⋃ i_1 ∈ ↑(s.erase i), Iotop (c i_1) (d i_1)

Tactic:
← ENNReal.ofReal_add_le

Goal state after:
case inr
R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a : R
c d : ℕ → R
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R), Icc a b ⊆ ⋃ i ∈ ↑t, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : R
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Iotop (c x) (d x)
is : i ∈ s
bcd : b ∈ Ioc (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ofReal (↑f (d i) - ↑f (c i) + (↑f (c i) - ↑f a))

case a
R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a : R
c d : ℕ → R
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R), Icc a b ⊆ ⋃ i ∈ ↑t, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : R
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Iotop (c x) (d x)
is : i ∈ s
bcd : b ∈ Ioc (c i) (d i)
⊢ Icc a (c i) ⊆ ⋃ i_1 ∈ ↑(s.erase i), Iotop (c i_1) (d i_1)
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
f : X → E
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
⊢ ∀ᵐ (x : X) ∂μ.restrict t, AEStronglyMeasurable.mk f hf x = 0 x

Tactic:
ae_restrict_iff (hf.stronglyMeasurable_mk.measurableSet_eq_fun stronglyMeasurable_zero)

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
⊢ ∀ᵐ (x : X) ∂μ, x ∈ t → AEStronglyMeasurable.mk f hf x = 0 x
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
inst✝¹ : MulAction H β
inst✝ : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : β → α
hf : QuasiMeasurePreserving f ν μ
e : G → H
he : Bijective e
hef : ∀ (g : G), Semiconj f (fun x ↦ e g • x) fun x ↦ g • x
x : β
x✝ : ∃ g, g • f x ∈ s
g : G
hg : g • f x ∈ s
⊢ f (e g • x) ∈ s

Tactic:
hef g x

Goal state after:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
inst✝¹ : MulAction H β
inst✝ : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : β → α
hf : QuasiMeasurePreserving f ν μ
e : G → H
he : Bijective e
hef : ∀ (g : G), Semiconj f (fun x ↦ e g • x) fun x ↦ g • x
x : β
x✝ : ∃ g, g • f x ∈ s
g : G
hg : g • f x ∈ s
⊢ (fun x ↦ g • x) (f x) ∈ s
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
ha : ¬IsBot a
b : R
hb : b < a
u : ℕ → R
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
x : R
hx : x ∈ {a}
⊢ x ∈ ⋂ n, Ioc (u n) a

Tactic:
by simp [mem_singleton_iff.1 hx, u_lt_a]

Goal state after:
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
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : μ s < ∞
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
⊢ ‖∫ (x : X) in s, f x ∂μ‖ ≤ C * μ.real s

Tactic:
by
  by_cases hfm : AEStronglyMeasurable f (μ.restrict s)
  · apply norm_setIntegral_le_of_norm_le_const_ae hs
    have A : ∀ᵐ x : X ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C := by
      filter_upwards [hC, hfm.ae_mem_imp_eq_mk] with _ h1 h2 h3
      rw [← h2 h3]
      exact h1 h3
    have B : MeasurableSet {x | ‖hfm.mk f x‖ ≤ C} :=
      hfm.stronglyMeasurable_mk.norm.measurable measurableSet_Iic
    filter_upwards [hfm.ae_eq_mk, (ae_restrict_iff B).2 A] with _ h1 _
    rwa [h1]
  · rw [integral_non_aestronglyMeasurable hfm]
    have : ∃ᵐ (x : X) ∂μ, x ∈ s := by
      apply frequently_ae_mem_iff.mpr
      contrapose hfm
      simp [Measure.restrict_eq_zero.mpr hfm]
    rcases (this.and_eventually hC).exists with ⟨x, hx, h'x⟩
    have : 0 ≤ C := (norm_nonneg _).trans (h'x hx)
    simp only [norm_zero, ge_iff_le]
    positivity

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

Goal state before:
pp: case hf
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x ↦ R) {x | R < f x} μ
⊢ ∀ᵐ (x : X) ∂μ, x ∈ {x | R < f x} → 0 ≤ f x - R

Tactic:
exact Eventually.of_forall fun x hx => sub_nonneg.2 <| le_of_lt hx

Goal state after:
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
f : X → E
μ : Measure X
inst✝¹ : PartialOrder X
x y : X
inst✝ : NullSingletonClass μ
⊢ ∫ (t : X) in Icc x y, f t ∂μ = ∫ (t : X) in Ioo x y, f t ∂μ

Tactic:
rw [integral_Icc_eq_integral_Ico, integral_Ico_eq_integral_Ioo]

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
U : Set G
hU : (interior U).Nonempty
⊢ prehaar (↑K₀) U ∈ haarProduct ↑K₀

Tactic:
rintro ⟨K, hK⟩ _

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K : Set G
hK : IsCompact K
a✝ : { carrier := K, isCompact' := hK } ∈ univ
⊢ prehaar (↑K₀) U { carrier := K, isCompact' := hK } ∈
    (fun K ↦ Icc 0 ↑(index ↑K ↑K₀)) { carrier := K, isCompact' := hK }
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
⊢ normSq x * t * t + re ⟪x, y⟫ * t + re ⟪y, x⟫ * t + normSq y =
    normSq x * t * t + re ⟪x, y⟫ * t + re ⟪x, y⟫ * t + normSq y

Tactic:
rw [inner_re_symm]

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
⊢ chaar K₀ K₀.toCompacts = 1

Tactic:
by
  let eval : (Compacts G → ℝ) → ℝ := fun f => f K₀.toCompacts
  have : Continuous eval := continuous_apply _
  change chaar K₀ ∈ eval ⁻¹' {(1 : ℝ)}
  apply mem_of_subset_of_mem _ (chaar_mem_clPrehaar K₀ ⊤)
  unfold clPrehaar; rw [IsClosed.closure_subset_iff]
  · rintro _ ⟨U, ⟨_, h2U, h3U⟩, rfl⟩; apply prehaar_self
    rw [h2U.interior_eq]; exact ⟨1, h3U⟩
  · apply continuous_iff_isClosed.mp this; exact isClosed_singleton

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

Goal state before:
pp: case inl
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
f g : StieltjesFunction R
a b : R
h : a ≤ b
ha : 𝓝[<] a = ⊥
⊢ leftLim (↑(f + g)) a = leftLim (↑f) a + leftLim (↑g) a

Tactic:
simp [leftLim_eq_of_eq_bot _ ha]

Goal state after: