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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : 0 ≤ z
⊢ Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)

pp: case neg
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : z < 0
⊢ Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)

Tactic:
· unfold Tendsto
    lift z to ℕ using hz
    simpa using! h z

Goal state after:
case neg
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : z < 0
⊢ Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), f =O[l] fun a ↦ k a ^ z
z : ℤ
⊢ Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)

Tactic:
suffices (fun a : α => k a ^ z * f a) =O[l] fun a : α => (k a)⁻¹ from
      IsBigO.trans_tendsto this hk.inv_tendsto_atTop
    refine ((isBigO_refl (fun a => k a ^ z) l).mul (h (-(z + 1)))).trans ?_
    refine .of_bound' <| hk0.mono fun a ha0 => ?_
    simp [← zpow_add₀ ha0]

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

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
⊢ (linearGrowthInf fun n ↦ ↑(v n)) * linearGrowthInf u ≤ linearGrowthInf (u ∘ v)

Tactic:
have uv_0 : 0 ≤ linearGrowthInf (u ∘ v) := by
    rw [← linearGrowthInf_const zero_ne_bot zero_ne_top]
    exact linearGrowthInf_eventually_monotone (hv.eventually hu)
  apply EReal.mul_le_of_forall_lt_of_nonneg (linearGrowthInf_natCast_nonneg v) uv_0
  refine fun a ⟨_, a_v⟩ b ⟨b_0, b_u⟩ ↦ Eventually.le_linearGrowthInf ?_
  have b_uv := eventually_map.1 ((eventually_mul_le b_u).filter_mono hv)
  filter_upwards [b_uv, eventually_lt_of_lt_liminf a_v, eventually_gt_atTop 0]
    with n b_uvn a_vn n_0
  replace a_vn := ((lt_div_iff (Nat.cast_pos'.2 n_0) (natCast_ne_top n)).1 a_vn).le
  rw [comp_apply, mul_comm a b, mul_assoc b a]
  exact b_uvn.trans' <| by gcongr

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

Goal state before:
pp: α : 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 : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
c : ι
hc : c ∈ u
h : ¬Disjoint (B a) (B c)
⊢ False

Tactic:
not_disjoint_iff_nonempty_inter

Goal state after:
α : 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 : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
c : ι
hc : c ∈ u
h : (B a ∩ B c).Nonempty
⊢ False
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: case neg.inr
α : 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, Disjoint (B c) (B d)
H' : b ∈ u
⊢ ∃ c_1 ∈ insert a' u, (B c ∩ B c_1).Nonempty ∧ δ c ≤ τ * δ c_1

Tactic:
· rw [← not_disjoint_iff_nonempty_inter] at hcb
        exact (hcb (H _ H')).elim

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

Goal state before:
pp: u : ℕ → EReal
m : ℕ
h : Monotone u
hm : m ≠ 0
⊢ Tendsto (fun n ↦ ↑(m * n) / ↑n) atTop (𝓝 ↑m)

Tactic:
refine tendsto_nhds_of_eventually_eq ((eventually_gt_atTop 0).mono fun x hx ↦ ?_)

Goal state after:
u : ℕ → EReal
m : ℕ
h : Monotone u
hm : m ≠ 0
x : ℕ
hx : 0 < x
⊢ ↑(m * x) / ↑x = ↑m
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
t : Set ι
x : ι → α
r : ι → ℝ
R : ℝ
hr : ∀ a ∈ t, r a ≤ R
τ : ℝ
hτ : 3 < τ
h✝ : t.Nonempty
t' : Set ι := {a | a ∈ t ∧ 0 < r a}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint fun a ↦ ball (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
A : ∀ a ∈ t', ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)
a : ι
ha : a ∈ t
h'a : r a ≤ 0
b : ι
rb : b ∈ t ∧ 0 < r b
c : ι
cu : c ∈ u
right✝ : ball (x b) (r b) ⊆ ball (x c) (τ * r c)
⊢ ball (x a) (r a) ⊆ ball (x c) (τ * r c)

Tactic:
simp only [ball_eq_empty.2 h'a, empty_subset]

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

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋃ n, s n)))
d_Inter :
  ∀ (s : ℕ → Set α),
    (∀ (n : ℕ), MeasurableSet (s n)) →
      (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋂ n, s n)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this✝ : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun n m ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
f_subset_f : ∀ {a b c d : ℕ}, a ≤ b → c ≤ d → f a d ⊆ f b c
f_succ : ∀ (n m : ℕ), n ≤ m → f n (m + 1) = f n m ∩ e (m + 1)
n m : ℕ
h : m ≤ n
this : γ - (1 / 2) ^ m < d (e m)
⊢ γ - 2 * (1 / 2) ^ m + (1 / 2) ^ m ≤ d (f m m)

Tactic:
simp_rw [f, Nat.Ico_succ_singleton, Finset.inf_singleton]

Goal state after:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋃ n, s n)))
d_Inter :
  ∀ (s : ℕ → Set α),
    (∀ (n : ℕ), MeasurableSet (s n)) →
      (∀ (n m : ℕ), n ≤ m → s m ⊆ s n) → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋂ n, s n)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this✝ : ∀ (n : ℕ), ∃ s, MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun n m ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
f_subset_f : ∀ {a b c d : ℕ}, a ≤ b → c ≤ d → f a d ⊆ f b c
f_succ : ∀ (n m : ℕ), n ≤ m → f n (m + 1) = f n m ∩ e (m + 1)
n m : ℕ
h : m ≤ n
this : γ - (1 / 2) ^ m < d (e m)
⊢ γ - 2 * (1 / 2) ^ m + (1 / 2) ^ m ≤ d (e m)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ Measurable (μ.rnDeriv ν)

Tactic:
rw [rnDeriv_of_not_haveLebesgueDecomposition h]

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ Measurable 0
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ⟂ₘ ν
h : ¬μ.HaveLebesgueDecomposition ν
⊢ μ.rnDeriv ν =ᵐ[ν] 0

Tactic:
rw [rnDeriv_of_not_haveLebesgueDecomposition h]

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}
x : α
hx : x ∈ {x | ∃ᶠ (x : Set α) in v.filterAt x, μ x = 0}
ε : ℝ
εpos : ε > 0
⊢ ∃ t ∈ v.setsAt x ∩ f x, t ⊆ closedBall x ε

Tactic:
simp only [frequently_filterAt_iff, gt_iff_lt, mem_ofPred_eq] at hx

Goal state after:
α : 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}
x : α
ε : ℝ
εpos : ε > 0
hx : ∀ (ε : ℝ), 0 < ε → ∃ t ∈ v.setsAt x, t ⊆ closedBall x ε ∧ μ t = 0
⊢ ∃ t ∈ v.setsAt x ∩ f x, t ⊆ closedBall x ε
Module: Mathlib.Order.Monotone.Extension

Goal state before:
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:
not_disjoint_iff_nonempty_inter

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 : (Iic x ∩ s).Nonempty
hy : ¬Disjoint (Iic y) s
⊢ sSup (f '' (Iic x ∩ s)) ≤ sSup (f '' (Iic y ∩ s))
Module: Mathlib.MeasureTheory.Covering.OneDim

Goal state before:
pp: case refine_2
x : ℝ
⊢ ∀ ε > 0, ∀ᶠ (i : ℝ) in 𝓝[<] x, Icc i x ⊆ Metric.closedBall x ε

Tactic:
· intro ε εpos
    filter_upwards [Icc_mem_nhdsLT <| show x - ε < x by linarith] with y hy
    rw [closedBall_eq_Icc]
    exact Icc_subset_Icc hy.1 (by linarith)

Goal state after:
Module: Mathlib.Analysis.Calculus.Monotone

Goal state before:
pp: case h1
f : StieltjesFunction ℝ
x : ℝ
hx : Tendsto (fun a ↦ f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 : Tendsto (fun y ↦ (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L2 : Tendsto (fun y ↦ (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
⊢ Tendsto (fun y ↦ y + 1 * (y - x) ^ 2) (𝓝[<] x) (𝓝 x)

Tactic:
apply Tendsto.mono_left _ nhdsWithin_le_nhds

Goal state after:
f : StieltjesFunction ℝ
x : ℝ
hx : Tendsto (fun a ↦ f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 : Tendsto (fun y ↦ (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L2 : Tendsto (fun y ↦ (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
⊢ Tendsto (fun y ↦ y + 1 * (y - x) ^ 2) (𝓝 x) (𝓝 x)
Module: Mathlib.Analysis.Calculus.Monotone

Goal state before:
pp: case h1
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧
    Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : ↑hf.stieltjesFunction x = f x
⊢ Tendsto (fun y ↦ y + -1 * (y - x) ^ 2) (𝓝[>] x) (𝓝 x)

Tactic:
apply Tendsto.mono_left _ nhdsWithin_le_nhds

Goal state after:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧
    Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : ↑hf.stieltjesFunction x = f x
⊢ Tendsto (fun y ↦ y + -1 * (y - x) ^ 2) (𝓝 x) (𝓝 x)
Module: Mathlib.Analysis.Calculus.Monotone

Goal state before:
pp: case h1
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧
    Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : ↑hf.stieltjesFunction x = f x
L1 : Tendsto (fun y ↦ (f y - f x) / (y - x)) (𝓝[>] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
⊢ Tendsto (fun y ↦ y + -1 * (y - x) ^ 2) (𝓝[<] x) (𝓝 x)

Tactic:
apply Tendsto.mono_left _ nhdsWithin_le_nhds

Goal state after:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧
    Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : ↑hf.stieltjesFunction x = f x
L1 : Tendsto (fun y ↦ (f y - f x) / (y - x)) (𝓝[>] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
⊢ Tendsto (fun y ↦ y + -1 * (y - x) ^ 2) (𝓝 x) (𝓝 x)
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α✝ : Type u_1
inst✝³ : LinearOrder α✝
E✝ : Type u_2
inst✝² : PseudoEMetricSpace E✝
f✝ : α✝ → E✝
s✝ : Set α✝
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
h : variationOnFromTo f s a b = 0
h' : a ≤ b
⊢ edist (f a) (f b) ≤ eVariationOn f (s ∩ Icc a b)

Tactic:
apply eVariationOn.edist_le

Goal state after:
case hx
α✝ : Type u_1
inst✝³ : LinearOrder α✝
E✝ : Type u_2
inst✝² : PseudoEMetricSpace E✝
f✝ : α✝ → E✝
s✝ : Set α✝
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
h : variationOnFromTo f s a b = 0
h' : a ≤ b
⊢ a ∈ s ∩ Icc a b

case hy
α✝ : Type u_1
inst✝³ : LinearOrder α✝
E✝ : Type u_2
inst✝² : PseudoEMetricSpace E✝
f✝ : α✝ → E✝
s✝ : Set α✝
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
h : variationOnFromTo f s a b = 0
h' : a ≤ b
⊢ b ∈ s ∩ Icc a b
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
b : α
bs : b ∈ s
⊢ AntitoneOn (fun a ↦ variationOnFromTo f s a b) s

Tactic:
rintro a as c cs ac
  dsimp only
  rw [← variationOnFromTo.add hf as cs bs]
  exact le_add_of_nonneg_left (variationOnFromTo.nonneg_of_le f s ac)

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

Goal state before:
pp: case hx
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
as : a ∈ s
bs : b ∈ s
cs : c ∈ s
bc : b ≤ c
⊢ b ∈ s ∩ Icc b c

pp: case hy
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
as : a ∈ s
bs : b ∈ s
cs : c ∈ s
bc : b ≤ c
⊢ c ∈ s ∩ Icc b c

Tactic:
exacts [⟨bs, le_rfl, bc⟩, ⟨cs, bc, le_rfl⟩]

Goal state after:
Module: Mathlib.Analysis.BoundedVariation

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
f g : α → ℝ
C D : ℝ≥0∞
s : Set α
hf : ∀ x ∈ s, ‖f x‖ₑ ≤ C
hg : ∀ x ∈ s, ‖g x‖ₑ ≤ D
⊢ eVariationOn (f * g) s ≤ C * eVariationOn g s + D * eVariationOn f s

Tactic:
by
  simpa using eVariationOn_smul_le hf hg

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

Goal state before:
pp: α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
hs : MeasurableSet s
this : IsLocallyFiniteMeasure (μ.restrict s)
x : α
hx : Tendsto (fun a ↦ (μ.restrict s) a / μ a) (v.filterAt x) (𝓝 ((μ.restrict s).rnDeriv μ x))
h'x : (μ.restrict s).rnDeriv μ x = s.indicator 1 x
⊢ Tendsto (fun a ↦ μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 (s.indicator 1 x))

Tactic:
simpa only [h'x, restrict_apply' hs, inter_comm] using hx

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

Goal state before:
pp: α : 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
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)

Tactic:
let A := MeasureTheory.Measure.finiteSpanningSetsInOpen' μ

Goal state after:
α : 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} :=
  μ.finiteSpanningSetsInOpen'
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: case pos
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 0 a = 0

pp: case neg
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 0 a = 0

Tactic:
· exact cfc_apply (0 : R → R) a ▸ map_zero (cfcHom ha)

Goal state after:
case neg
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 0 a = 0
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : LocallyBoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
hx : x ∈ s
h : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : y ∈ s ∩ Iio x
⊢ Tendsto (fun y ↦ eVariationOn f (s ∩ Icc y x)) (𝓝[s ∩ Iio x] x) (𝓝 (edist (f x) l))

Tactic:
have : 𝓝[s ∩ Iio x] x = 𝓝[(s ∩ Icc y x) ∩ Iio x] x := by
    rw [show (s ∩ Icc y x) ∩ Iio x = (s ∩ Iio x) ∩ Icc y x by grind, eq_comm]
    apply nhdsWithin_inter_of_mem' (nhdsWithin_mono _ inter_subset_right (Icc_mem_nhdsLT hy.2))

Goal state after:
case inr
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : LocallyBoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Iio x] x) (𝓝 l)
hx : x ∈ s
h : (𝓝[s ∩ Iio x] x).NeBot
y : α
hy : y ∈ s ∩ Iio x
this : 𝓝[s ∩ Iio x] x = 𝓝[s ∩ Icc y x ∩ Iio x] x
⊢ Tendsto (fun y ↦ eVariationOn f (s ∩ Icc y x)) (𝓝[s ∩ Iio x] x) (𝓝 (edist (f x) l))
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
ha : p a✝
hf : ContinuousOn f✝ (spectrum R a✝)
hg : ContinuousOn g (spectrum R a✝)
f : R → R
a : A
⊢ Commute (star (cfc f a)) (cfc f a)

Tactic:
by
    rw [Commute, SemiconjBy]
    by_cases h : ContinuousOn f (spectrum R a)
    · rw [← cfc_star, ← cfc_mul .., ← cfc_mul ..]
      congr! 2
      exact mul_comm _ _
    · simp [cfc_apply_of_not_continuousOn a h]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: a b : ℝ
h : a < b
⊢ Subalgebra.comap (compRightAlgHom ℝ ℝ ↑(iccHomeoI a b h).symm) (polynomialFunctions I) =
    polynomialFunctions (Set.Icc a b)

Tactic:
by
  ext f
  fconstructor
  · rintro ⟨p, ⟨-, w⟩⟩
    rw [DFunLike.ext_iff] at w
    dsimp at w
    let q := p.comp ((b - a)⁻¹ • Polynomial.X + Polynomial.C (-a * (b - a)⁻¹))
    refine ⟨q, ⟨?_, ?_⟩⟩
    · simp
    · ext x
      simp only [q, neg_mul, map_neg, map_mul, AlgHom.coe_toRingHom,
        Polynomial.eval_X, Polynomial.eval_neg, Polynomial.eval_C, Polynomial.eval_smul,
        smul_eq_mul, Polynomial.eval_mul, Polynomial.eval_add,
        Polynomial.eval_comp, Polynomial.toContinuousMapOnAlgHom_apply,
        Polynomial.toContinuousMapOn_apply, Polynomial.toContinuousMap_apply]
      convert! w ⟨_, _⟩
      · ext
        simp only [iccHomeoI_symm_apply_coe]
        replace h : b - a ≠ 0 := sub_ne_zero_of_ne h.ne.symm
        field
      · rw [mul_comm (b - a)⁻¹, ← neg_mul, ← add_mul, ← sub_eq_add_neg]
        have w₁ : 0 < (b - a)⁻¹ := inv_pos.mpr (sub_pos.mpr h)
        have w₂ : 0 ≤ (x : ℝ) - a := sub_nonneg.mpr x.2.1
        have w₃ : (x : ℝ) - a ≤ b - a := sub_le_sub_right x.2.2 a
        fconstructor
        · exact mul_nonneg w₂ (le_of_lt w₁)
        · rw [← div_eq_mul_inv, div_le_one (sub_pos.mpr h)]
          exact w₃
  · rintro ⟨p, ⟨-, rfl⟩⟩
    let q := p.comp ((b - a) • Polynomial.X + Polynomial.C a)
    refine ⟨q, ⟨?_, ?_⟩⟩
    · simp
    · ext x
      simp [q, mul_comm]

Goal state after: