mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
a : EReal
x✝¹ : a ∈ Set.Ioo 0 (linearGrowthInf fun n ↦ ↑(v n))
b : EReal
x✝ : b ∈ Set.Ioo 0 (linearGrowthInf u)
left✝ : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b_0 : 0 < b
b_u : b < linearGrowthInf u
b_uv : ∀ᶠ (a : ℕ) in atTop, b * ↑(v a) ≤ u (v a)
n : ℕ
⊢ b * ↑(v n) ≤ u (v n) → a < ↑(v n) / ↑n → 0 < n → a * b * ↑n ≤ (u ∘ v) n

Tactic:
b_uvn

Goal state after:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
a : EReal
x✝¹ : a ∈ Set.Ioo 0 (linearGrowthInf fun n ↦ ↑(v n))
b : EReal
x✝ : b ∈ Set.Ioo 0 (linearGrowthInf u)
left✝ : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b_0 : 0 < b
b_u : b < linearGrowthInf u
b_uv : ∀ᶠ (a : ℕ) in atTop, b * ↑(v a) ≤ u (v a)
n : ℕ
b_uvn : b * ↑(v n) ≤ u (v n)
⊢ a < ↑(v n) / ↑n → 0 < n → a * b * ↑n ≤ (u ∘ v) n
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case inr
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Tendsto v atTop atTop
m : ℕ
hum : ¬u m = ⊥ m
um_uvn : ∀ᶠ (n : ℕ) in atTop, u m ≤ (u ∘ v) n
hum' : u m ≠ ⊤
⊢ 0 ≤ linearGrowthInf fun x ↦ u m

Tactic:
rw [linearGrowthInf_const hum hum']

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this : Encodable ↑s
p q : β
H : ¬(p ∈ s ∧ q ∈ s ∧ p < q)
⊢ ∃ u v,
    MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ (p ∈ s → q ∈ s → p < q → μ (u ∩ v) = 0)

Tactic:
refine
        ⟨univ, univ, MeasurableSet.univ, MeasurableSet.univ, subset_univ _, subset_univ _,
          fun ps qs pq => ?_⟩
      exact (H ⟨ps, qs, pq⟩).elim

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x ↦ ⨅ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q
⊢ ∑' (p : ↑s) (x : ↑(s ∩ Ioi ↑p)), 0 = 0

Tactic:
simp only [tsum_zero]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : a' ∉ u
c : ι
ct : c ∈ t
b : ι
ba'u : b ∈ insert a' u
hcb : (B c ∩ B b).Nonempty
H : ∀ d ∈ u, B c ∩ B d = ∅
⊢ ∃ c_1 ∈ insert a' u, (B c ∩ B c_1).Nonempty ∧ δ c ≤ τ * δ c_1

Tactic:
· -- Otherwise, `c` belongs to `A`. The element of `u ∪ {a'}` that it intersects has to be `a'`.
      -- Moreover, `δ c` is smaller than the maximum `m` of `δ` over `A`, which is `≤ δ a' / τ`
      -- thanks to the good choice of `a'`. This is the desired inequality.
      simp only [← disjoint_iff_inter_eq_empty] at H
      rcases mem_insert_iff.1 ba'u with (rfl | H')
      · refine ⟨b, mem_insert _ _, hcb, ?_⟩
        calc
          δ c ≤ m := le_csSup bddA (mem_image_of_mem _ ⟨ct, H⟩)
          _ = τ * (m / τ) := by field
          _ ≤ τ * δ b := by gcongr
      · rw [← not_disjoint_iff_nonempty_inter] at hcb
        exact (hcb (H _ H')).elim

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
ε N : ℝ≥0
p : ℕ
εpos : 0 < ε
s : Set α := {x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p
s_lt_top : μ s < ∞
⊢ ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ + 0

Tactic:
rw [add_zero, ← Measure.restrict_toMeasurable s_lt_top.ne]
          refine h _ (measurableSet_toMeasurable ..) ?_
          rwa [measure_toMeasurable]

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

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure (μ.restrict s)
hμ0 : μ s = 0
⊢ ∫⁻ (x : α) in univ, f x ∂((μ.restrict s) univ)⁻¹ • μ.restrict s ≤ essSup f μ

Tactic:
exact le_of_eq_of_le (setLIntegral_measure_zero univ f <| by simp [hμ0]) zero_le

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
⊢ f =ᵐ[μ] g

Tactic:
have A : f ≤ᵐ[μ] g :=
    ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ hf fun s hs h's => le_of_eq (h s hs h's)
  have B : g ≤ᵐ[μ] f :=
    ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ hg fun s hs h's => ge_of_eq (h s hs h's)
  filter_upwards [A, B] with x using le_antisymm

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst✝ : IsProbabilityMeasure μ
hf : Integrable f μ
hN : μ N = 0
⊢ ∃ x ∉ N, f x ≤ ∫ (a : α), f a ∂μ

Tactic:
simpa only [average_eq_integral] using
    exists_notMem_null_le_average (IsProbabilityMeasure.ne_zero μ) hf hN

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

Goal state before:
pp: case a.refine_1.refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
t : Set α
h_meas_t : MeasurableSet t
h_mu_le_add_top : μ ≤ ν' + ν + ⊤
⊢ μ (t ∩ sᶜ) ≤ (ν' + ν + ⊤) (t ∩ sᶜ)

Tactic:
exact Measure.le_iff'.1 h_mu_le_add_top _

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a}
hs : s = {x | ∃ᶠ (x : Set α) in v.filterAt x, μ x = 0}
f : α → Set (Set α) := fun x ↦ {a | μ a = 0}
h : v.FineSubfamilyOn f s
⊢ ∑' (x : ↑h.index), 0 = 0

Tactic:
simp only [tsum_zero]

Goal state after:
Module: Mathlib.Order.Monotone.Extension

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
hy : Disjoint (Iic y) s
⊢ sSup (f '' (Iic x ∩ s)) ≤ a

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
hy : ¬Disjoint (Iic y) s
⊢ sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))

Tactic:
· exact (hx <| hy.mono_left <| Iic_subset_Iic.2 hxy).elim

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
hgs : EqOn f g s
x y : α
hxy : x ≤ y
hx : ¬Disjoint (Iic x) s
hy : ¬Disjoint (Iic y) s
⊢ sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f f' : α → E
s : Set α
h : ∀ ⦃x : α⦄, x ∈ s → edist (f x) (f' x) = 0
⊢ eVariationOn f s = eVariationOn f' s

Tactic:
dsimp only [eVariationOn]
  congr 1 with p : 1
  congr 1 with i : 1
  rw [edist_congr_right (h <| p.snd.prop.2 (i + 1)), edist_congr_left (h <| p.snd.prop.2 i)]

Goal state after:
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
s : Set α
E : Type u_3
inst✝² : PseudoMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
l : E
a b : α
ha : a ∈ s
hb : b ∈ s
hf : LocallyBoundedVariationOn f s
h'f : Tendsto f (𝓝[s ∩ Ioi b] b) (𝓝 l)
H :
  Tendsto (fun x ↦ variationOnFromTo f s a b + variationOnFromTo f s b x) (𝓝[s ∩ Ioi b] b)
    (𝓝 (variationOnFromTo f s a b + dist (f b) l))
⊢ Tendsto (variationOnFromTo f s a) (𝓝[s ∩ Ioi b] b) (𝓝 (variationOnFromTo f s a b + dist (f b) l))

Tactic:
apply Tendsto.congr' _ H
    filter_upwards [self_mem_nhdsWithin] with x hx
    rw [variationOnFromTo.add hf ha hb hx.1]

Goal state after:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
s : Set α
h : BoundedVariationOn f s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ dist (f x) (f y) ≤ (eVariationOn f s).toReal

Tactic:
rw [← ENNReal.ofReal_le_ofReal_iff ENNReal.toReal_nonneg, ENNReal.ofReal_toReal h, ← edist_dist]
  exact edist_le f hx hy

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
⊢ μ + (ν - ξ) = μ + ν - ξ

Tactic:
have h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ =
      μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ := by
    rw [restrict_sub_eq_restrict_sub_restrict hs.compl, h.restrict_compl_nullSet]
    simp

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ
⊢ μ + (ν - ξ) = μ + ν - ξ
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
f : α → E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
hf : BoundedVariationOn f univ
a x : α
hx : ContinuousWithinAt f (Ici x) x
this : variationOnFromTo f univ a = fun y ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y
⊢ Tendsto (fun y ↦ eVariationOn f (univ ∩ Icc x y)) (𝓝[univ] x) (𝓝 0)

Tactic:
exact hf.tendsto_eVariationOn_Icc_zero_right _ (by simpa using hx)

Goal state after:
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
⊢ MonotoneOn (fun x ↦ (variationOnFromTo f s c x + f x) / 2) s

Tactic:
intro x hx y hy hxy

Goal state after:
case inr.refine_1
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ (fun x ↦ (variationOnFromTo f s c x + f x) / 2) x ≤ (fun x ↦ (variationOnFromTo f s c x + f x) / 2) y
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case inr.refine_2
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
⊢ MonotoneOn (fun x ↦ (variationOnFromTo f s c x - f x) / 2) s

Tactic:
intro x hx y hy hxy

Goal state after:
case inr.refine_2
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ (fun x ↦ (variationOnFromTo f s c x - f x) / 2) x ≤ (fun x ↦ (variationOnFromTo f s c x - f x) / 2) y
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
⊢ BoundedVariationOn f ↑∅

Tactic:
simp [BoundedVariationOn]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: case hf
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K} := ⋯
t : Set E
t_count : t.Countable
ht : range f ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
n : ℕ
c : E
hi✝ : c ∈ t
⊢ Measurable fun y ↦ ‖f y - (A.set n).indicator (fun x ↦ c) y‖ₑ

pp: case h'f
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K} := ⋯
t : Set E
t_count : t.Countable
ht : range f ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
n : ℕ
c : E
hi✝ : c ∈ t
⊢ ∫⁻ (y : α), ‖f y - (A.set n).indicator (fun x ↦ c) y‖ₑ ∂μ ≠ ∞

Tactic:
· refine (h'f.sub ?_).enorm
      exact stronglyMeasurable_const.indicator (IsOpen.measurableSet (A.set_mem n))

Goal state after:
case h'f
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
h'f : StronglyMeasurable f
A : μ.FiniteSpanningSetsIn {K | IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K} := ⋯
t : Set E
t_count : t.Countable
ht : range f ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
n : ℕ
c : E
hi✝ : c ∈ t
⊢ ∫⁻ (y : α), ‖f y - (A.set n).indicator (fun x ↦ c) y‖ₑ ∂μ ≠ ∞
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case e'_3.a.inr
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
u : β
us : u ∈ t
vφx : φ x ≤ φ u
vφy : φ u ≤ φ y
ux : u ≤ x
⊢ φ u ∈ φ '' (t ∩ Icc x y)

Tactic:
← le_antisymm vφx (hφ us hx ux)

Goal state after:
case e'_3.a.inr
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
u : β
us : u ∈ t
vφx : φ x ≤ φ u
vφy : φ u ≤ φ y
ux : u ≤ x
⊢ φ x ∈ φ '' (t ∩ Icc x y)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f g : R → R
a : A
h : cfc f a = cfc g a
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : p a
⊢ Set.EqOn f g (spectrum R a)

Tactic:
rw [cfc_apply f a, cfc_apply g a] at h

Goal state after:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f g : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : p a
h :
  (cfcHom ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ } =
    (cfcHom ha) { toFun := (spectrum R a).domRestrict g, continuous_toFun := ⋯ }
⊢ Set.EqOn f g (spectrum R a)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝¹⁹ : Semifield R
inst✝¹⁸ : StarRing R
inst✝¹⁷ : MetricSpace R
inst✝¹⁶ : IsTopologicalSemiring R
inst✝¹⁵ : ContinuousStar R
inst✝¹⁴ : Semifield S
inst✝¹³ : StarRing S
inst✝¹² : MetricSpace S
inst✝¹¹ : IsTopologicalSemiring S
inst✝¹⁰ : ContinuousStar S
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : Algebra S A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : IsScalarTower R S A
inst✝³ : StarModule R S
inst✝² : ContinuousSMul R S
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousFunctionalCalculus S A q
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
⊢ ∀ (f_1 : C(↑(spectrum R a), R)), p ((starAlgHom (cfcHom ⋯) ⋯) f_1)

Tactic:
intro g

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝¹⁹ : Semifield R
inst✝¹⁸ : StarRing R
inst✝¹⁷ : MetricSpace R
inst✝¹⁶ : IsTopologicalSemiring R
inst✝¹⁵ : ContinuousStar R
inst✝¹⁴ : Semifield S
inst✝¹³ : StarRing S
inst✝¹² : MetricSpace S
inst✝¹¹ : IsTopologicalSemiring S
inst✝¹⁰ : ContinuousStar S
inst✝⁹ : Ring A
inst✝⁸ : StarRing A
inst✝⁷ : Algebra S A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : IsScalarTower R S A
inst✝³ : StarModule R S
inst✝² : ContinuousSMul R S
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousFunctionalCalculus S A q
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
g : C(↑(spectrum R a), R)
⊢ p ((starAlgHom (cfcHom ⋯) ⋯) g)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
a : A
ha : p a
⊢ cfc (fun x ↦ Polynomial.eval x X) a = a

Tactic:
simpa using! cfc_id R a

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²³ : Semifield R
inst✝²² : StarRing R
inst✝²¹ : MetricSpace R
inst✝²⁰ : IsTopologicalSemiring R
inst✝¹⁹ : ContinuousStar R
inst✝¹⁸ : Field S
inst✝¹⁷ : StarRing S
inst✝¹⁶ : MetricSpace S
inst✝¹⁵ : IsTopologicalRing S
inst✝¹⁴ : ContinuousStar S
inst✝¹³ : NonUnitalRing A
inst✝¹² : StarRing A
inst✝¹¹ : Module S A
inst✝¹⁰ : IsScalarTower S A A
inst✝⁹ : SMulCommClass S A A
inst✝⁸ : Algebra R S
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus S A q
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
⊢ ∀ (f_1 : C(↑(σₙ R a), R)₀), p ((nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯) f_1)

Tactic:
intro g

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²³ : Semifield R
inst✝²² : StarRing R
inst✝²¹ : MetricSpace R
inst✝²⁰ : IsTopologicalSemiring R
inst✝¹⁹ : ContinuousStar R
inst✝¹⁸ : Field S
inst✝¹⁷ : StarRing S
inst✝¹⁶ : MetricSpace S
inst✝¹⁵ : IsTopologicalRing S
inst✝¹⁴ : ContinuousStar S
inst✝¹³ : NonUnitalRing A
inst✝¹² : StarRing A
inst✝¹¹ : Module S A
inst✝¹⁰ : IsScalarTower S A A
inst✝⁹ : SMulCommClass S A A
inst✝⁸ : Algebra R S
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus S A q
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
g : C(↑(σₙ R a), R)₀
⊢ p ((nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯) g)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommRing R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : ContinuousFunctionalCalculus R A p
f : R → R
a : A
h : ¬(p a ∧ ContinuousOn f (spectrum R a))
⊢ cfc (fun x ↦ -f x) a = -cfc f a

Tactic:
· obtain (ha | hf) := not_and_or.mp h
    · simp [cfc_apply_of_not_predicate a ha]
    · rw [cfc_apply_of_not_continuousOn a hf, cfc_apply_of_not_continuousOn, neg_zero]
      exact fun hf_neg ↦ hf <| by simpa using hf_neg.fun_neg

Goal state after:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝⁵ : LinearOrder α
E : Type u_2
inst✝⁴ : PseudoEMetricSpace E
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : CompleteSpace E
inst✝ : T3Space E
f : α → E
hf : BoundedVariationOn f univ
x : α
⊢ ContinuousWithinAt (Function.leftLim f) (Iic x) x

Tactic:
have : Tendsto f.leftLim (𝓝[<] x) (𝓝 (f.leftLim.leftLim x)) := hf.leftLim.tendsto_leftLim x

Goal state after:
α : Type u_1
inst✝⁵ : LinearOrder α
E : Type u_2
inst✝⁴ : PseudoEMetricSpace E
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : CompleteSpace E
inst✝ : T3Space E
f : α → E
hf : BoundedVariationOn f univ
x : α
this : Tendsto (Function.leftLim f) (𝓝[<] x) (𝓝 (Function.leftLim (Function.leftLim f) x))
⊢ ContinuousWithinAt (Function.leftLim f) (Iic x) x
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
C : ℝ
hf : MonotoneOn f s
h : ∀ x ∈ s, |f x| ≤ C
⊢ BoundedVariationOn f s

Tactic:
by
  suffices eVariationOn f s ≤ .ofReal (2 * C) from
    ne_of_lt (this.trans_lt (by simp [mul_lt_top]))
  rw [eVariationOn.eq_biSup_inter_Icc]
  simp only [mem_ofPred_eq, iSup_le_iff, and_imp, Prod.forall]
  intro a b as bs hab
  grw [hf.eVariationOn_eq as bs]
  exact ofReal_mono (by grind)

Goal state after:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: a b : ℝ
⊢ BoundedVariationOn id (Set.Icc a b)

Tactic:
simp [BoundedVariationOn]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n ν k : ℕ
⊢ k < n - ν → eval 1 ((⇑derivative)^[k] (bernsteinPolynomial R n ν)) = 0

Tactic:
intro w

Goal state after:
R : Type u_1
inst✝ : CommRing R
n ν k : ℕ
w : k < n - ν
⊢ eval 1 ((⇑derivative)^[k] (bernsteinPolynomial R n ν)) = 0