mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case e'_9
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y ↦ ↑(-y) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x
⊢ (r + 1) * ↑(-x) ^ r * cexp (↑π * I * r) = -(-(r + 1) * ↑(-x) ^ r) * cexp (↑π * I * r)

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case e'_9
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y ↦ ↑y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x)
⊢ -(r + 1) * ↑(-x) ^ r = -1 * ((r + 1) * ↑(-x) ^ r)

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
y : ℂ
⊢ r = r + 1 - 1

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
this : Tendsto g (𝓝[<] x) (𝓝 (g x))
y : ℝ
hy : y ∈ Iio x
⊢ y ∈ {x | (fun x ↦ g x = (fun x ↦ deriv f x) x) x}

Tactic:
exact (f_diff y (ne_of_lt hy)).deriv.symm

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case inr.convert_5
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y ↦ y) 1 ↑(-x)

Tactic:
exact hasDerivAt_id ((-x : ℝ) : ℂ)

Goal state after:
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n))
    B
this✝ :
  iteratedDerivWithin (n + 1) (fun x ↦ (1 + x) ^ a) B = derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B
this :
  Set.EqOn (derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B)
    (derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B) B
z : ℂ
hz : z ∈ B
⊢ a - (↑n + 1) = a - ↑n - 1

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
k : ℕ
ih : HasFPowerSeriesWithinOnBall (iteratedFDerivWithin 𝕜 k f s) (p.iteratedFDerivSeries k) s x r
⊢ HasFPowerSeriesWithinOnBall (iteratedFDerivWithin 𝕜 (k + 1) f s) (p.iteratedFDerivSeries (k + 1)) s x r

Tactic:
iteratedFDerivWithin_succ_eq_comp_left

Goal state after:
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
k : ℕ
ih : HasFPowerSeriesWithinOnBall (iteratedFDerivWithin 𝕜 k f s) (p.iteratedFDerivSeries k) s x r
⊢ HasFPowerSeriesWithinOnBall
    (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm ∘ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 k f s) s)
    (p.iteratedFDerivSeries (k + 1)) s x r
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case e'_12.e_a.e_a
p : ℝ × ℝ
hp : p.1 < 0
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_8✝ : instAddCommGroup = normedCommRing.toCommRing.toAddCommGroup
e_9✝ : Semiring.toModule ≍ (NormedAlgebra.toNormedSpace ℝ).toModule
⊢ p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π =
    rexp (log p.1 * p.2) * -sin (p.2 * π) * π + p.1 ^ p.2 * log p.1

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case e'_12.e_a.e_a
p : ℝ × ℝ
hp : p.1 < 0
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_8✝ : instAddCommGroup = normedCommRing.toCommRing.toAddCommGroup
e_9✝ : Semiring.toModule ≍ (NormedAlgebra.toNormedSpace ℝ).toModule
⊢ p.2 * (p.1 ^ p.2 * p.1⁻¹) = p.1 ^ p.2 * p.2 * p.1⁻¹

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_10
a b : ℂ
n✝ : ℕ
⊢ a * ↑n✝ + b = b - a + a * (↑n✝ + 1)

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: f g : ℝ → ℝ
f' g' x : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h : 0 < f x
⊢ f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x) =
    g x * f x ^ (g x - 1) * f' + f x ^ g x * Real.log (f x) * g'

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case e'_9
f : ℝ → ℝ
f' x p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ f' * p * f x ^ (p - 1) = p * f x ^ (p - 1) * f'

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: c : ℂ
t : ℝ
ht : 0 < t
⊢ deriv (fun x ↦ ‖↑x ^ c‖) t = c.re * t ^ (c.re - 1)

Tactic:
rw [EventuallyEq.deriv_eq (f := fun x ↦ x ^ c.re)]
  · rw [Real.deriv_rpow_const t]
  · filter_upwards [eventually_gt_nhds ht] with x hx
    rw [Complex.norm_cpow_eq_rpow_re_of_pos hx]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: f : ℝ → ℝ
f' x : ℝ
s : Set ℝ
a : ℝ
ha : 0 < a
hf : HasDerivWithinAt f f' s x
⊢ Real.log a * f' * a ^ f x = 0 * f x * a ^ (f x - 1) + f' * a ^ f x * Real.log a

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: r : ℝ
hr : r ≠ 0
⊢ HasFPowerSeriesOnBall (fun x ↦ 1 / (r - x) ^ 2)
    (FormalMultilinearSeries.ofScalars ℝ fun n ↦ (r ^ (n + 2))⁻¹ * (↑n + 1)) 0 ‖r‖ₑ

Tactic:
simpa [add_comm 1] using one_div_sub_pow_hasFPowerSeriesOnBall_zero 1 hr

Goal state after:
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_10
a b : ℝ
n✝ : ℕ
⊢ a * ↑n✝ + b = b - a + a * (↑n✝ + 1)

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: x a : ℝ
ha : 0 < a
⊢ deriv (fun x ↦ a ^ x) x = log a * a ^ x

Tactic:
deriv_const_rpow ha differentiableAt_fun_id,

Goal state after:
x a : ℝ
ha : 0 < a
⊢ log a * deriv (fun x ↦ x) x * a ^ x = log a * a ^ x
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
⊢ linearGrowthSup (u ⊔ v) = max (linearGrowthSup u) (linearGrowthSup v)

Tactic:
rw [linearGrowthSup, linearGrowthSup, linearGrowthSup, ← limsup_max]
  refine limsup_congr (Eventually.of_forall fun n ↦ ?_)
  exact (monotone_div_right_of_nonneg n.cast_nonneg').map_max

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), f =O[l] fun a ↦ k a ^ z

Tactic:
refine (superpolynomialDecay_iff_zpow_tendsto_zero f hk).trans ?_

Goal state after:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ (∀ (z : ℤ), Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)) ↔ ∀ (z : ℤ), f =O[l] fun a ↦ k a ^ z
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case neg.inr
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : ¬u = ⊥
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
u_b : b > linearGrowthInf u
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
v_a' : (linearGrowthSup fun n ↦ ↑(v n)) < a'
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
⊢ ∃ᶠ (n : ℕ) in atTop, (u ∘ v) n ≤ a * b * ↑n

Tactic:
replace v_a' : ∀ᶠ n : ℕ in atTop, v n ≤ a' * n := by
    filter_upwards [eventually_lt_of_limsup_lt v_a', eventually_gt_atTop 0] with n vn_a' n_0
    rw [mul_comm]
    exact (div_le_iff_le_mul (Nat.cast_pos'.2 n_0) (natCast_ne_top n)).1 vn_a'.le

Goal state after:
case neg.inr
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : ¬u = ⊥
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
u_b : b > linearGrowthInf u
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, ↑(v n) ≤ a' * ↑n
⊢ ∃ᶠ (n : ℕ) in atTop, (u ∘ v) n ≤ a * b * ↑n
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: case a
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ u n + v n ≤ max (u n) (v n) + max (u n) (v n)

Tactic:
exact add_le_add (le_max_left (u n) (v n)) (le_max_right (u n) (v n))

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hf_meas : AEMeasurable f μ
⊢ AEFinStronglyMeasurable f μ

Tactic:
refine ⟨hf_meas.mk f, ENNReal.finStronglyMeasurable_of_measurable ?_ hf_meas.measurable_mk,
    hf_meas.ae_eq_mk⟩

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hf_meas : AEMeasurable f μ
⊢ ∫⁻ (x : α), AEMeasurable.mk f hf_meas x ∂μ ≠ ∞
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: case inl
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
hμ : μ = 0
⊢ Measure.real 0 univ • 0 = 0

Tactic:
smul_zero

Goal state after:
case inl
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
hμ : μ = 0
⊢ 0 = 0
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ∞
htμ : μ t ≠ ∞
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
this✝ : Fact (μ s < ∞)
this : Fact (μ t < ∞)
⊢ ⨍ (x : α), f x ∂(μ.restrict s + μ.restrict t) =
    (μ.real s / (μ.real s + μ.real t)) • ⨍ (x : α) in s, f x ∂μ +
      (μ.real t / (μ.real s + μ.real t)) • ⨍ (x : α) in t, f x ∂μ

Tactic:
average_add_measure hfs hft,

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ∞
htμ : μ t ≠ ∞
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
this✝ : Fact (μ s < ∞)
this : Fact (μ t < ∞)
⊢ ((μ.restrict s).real univ / ((μ.restrict s).real univ + (μ.restrict t).real univ)) • ⨍ (x : α) in s, f x ∂μ +
      ((μ.restrict t).real univ / ((μ.restrict s).real univ + (μ.restrict t).real univ)) • ⨍ (x : α) in t, f x ∂μ =
    (μ.real s / (μ.real s + μ.real t)) • ⨍ (x : α) in s, f x ∂μ +
      (μ.real t / (μ.real s + μ.real t)) • ⨍ (x : α) in t, f x ∂μ
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν
h : ν.withDensity (μ.rnDeriv ν) = 0
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
exact mutuallySingular_singularPart μ ν

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
exact mutuallySingular_singularPart μ ν

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ 0 = r • 0

pp: case neg.hnc
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ ¬(r • μ).HaveLebesgueDecomposition ν

Tactic:
smul_zero

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ 0 = 0

case neg.hnc
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ ¬(r • μ).HaveLebesgueDecomposition ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
this :
  ν.singularPart (r • μ) + (r • μ).withDensity (ν.rnDeriv (r • μ)) =
    ν.singularPart (r • μ) + r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)
⊢ (↑r • μ).withDensity (ν.rnDeriv (↑r • μ)) = ↑r⁻¹ • (↑r • μ).withDensity (ν.rnDeriv μ)

Tactic:
rwa [add_right_inj] at this

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝⁴ : IsFiniteMeasure ν₁
inst✝³ : IsFiniteMeasure ν₂
inst✝² : ν₁.HaveLebesgueDecomposition μ
inst✝¹ : ν₂.HaveLebesgueDecomposition μ
inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ
this :
  (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
⊢ μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)

Tactic:
rwa [add_right_inj] at this

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

Goal state before:
pp: α : 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))
x : α
hx : x ∈ s
this : IsGreatest (Iic x ∩ s) x
⊢ f x = sSup (f '' (Iic x ∩ s))

Tactic:
((h.mono inter_subset_right).map_isGreatest this).csSup_eq

Goal state after:
α : 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))
x : α
hx : x ∈ s
this : IsGreatest (Iic x ∩ s) x
⊢ f x = f x
Module: Mathlib.Analysis.Calculus.Monotone

Goal state before:
pp: f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] x
hf : Tendsto (fun y ↦ (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y ↦ y + c * (y - x) ^ 2) l l
⊢ Tendsto (fun y ↦ (f (y + c * (y - x) ^ 2) - d) / (y - x)) l (𝓝 a)

Tactic:
have L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1) := by
    have : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 (1 + c * (x - x))) := by
      apply Tendsto.mono_left _ (hl.trans nhdsWithin_le_nhds)
      exact ((tendsto_id.sub_const x).const_mul c).const_add 1
    simp only [_root_.sub_self, add_zero, mul_zero] at this
    apply Tendsto.congr' (Eventually.filter_mono hl _) this
    filter_upwards [self_mem_nhdsWithin] with y hy
    field [sub_ne_zero.2 hy]
  have Z := (hf.comp h').mul L
  rw [mul_one] at Z
  apply Tendsto.congr' _ Z
  have : ∀ᶠ y in l, y + c * (y - x) ^ 2 ≠ x := by apply Tendsto.mono_right h' hl self_mem_nhdsWithin
  filter_upwards [this] with y hy
  simp [field]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
⊢ ∃ p, Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2

Tactic:
have hξm : Measurable ξ := by
      convert! Measurable.iSup fun n ↦ (iSup_mem_measurableLE _ hf₁ n).1
      simp [hξ]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
⊢ ∃ p, Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
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
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
⊢ variationOnFromTo f s a b - variationOnFromTo f s a c = variationOnFromTo f s c b

Tactic:
rw [← variationOnFromTo.add hf ha hc hb, add_sub_cancel_left]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
this :
  ν.singularPart (r • μ) + (r • μ).withDensity (ν.rnDeriv (r • μ)) =
    ν.singularPart (r • μ) + r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)
⊢ (↑r • μ).withDensity (ν.rnDeriv (↑r • μ)) = ↑r⁻¹ • (↑r • μ).withDensity (ν.rnDeriv μ)

Tactic:
rwa [add_right_inj] at this

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
ι : Type u_3
F : ι → α → E
p : Filter ι
f : α → E
s : Set α
Ffs : ∀ x ∈ s, Tendsto (fun i ↦ F i x) p (𝓝 (f x))
v : ℝ≥0∞
hv : v < eVariationOn f s
⊢ ∀ᶠ (n : ι) in p, v < eVariationOn (F n) s

Tactic:
by
  obtain ⟨⟨n, ⟨u, um, us⟩⟩, hlt⟩ :
    ∃ p : ℕ × { u : ℕ → α // Monotone u ∧ ∀ i, u i ∈ s },
      v < ∑ i ∈ Finset.range p.1, edist (f ((p.2 : ℕ → α) (i + 1))) (f ((p.2 : ℕ → α) i)) :=
    lt_iSup_iff.mp hv
  have : Tendsto (fun j => ∑ i ∈ Finset.range n, edist (F j (u (i + 1))) (F j (u i))) p
      (𝓝 (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))) := by
    apply tendsto_finsetSum
    exact fun i _ => Tendsto.edist (Ffs (u i.succ) (us i.succ)) (Ffs (u i) (us i))
  exact (this.eventually_const_lt hlt).mono fun i h => h.trans_le (sum_le um us)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[singleton '' s] E
⊢ ∀ x ∈ s, Tendsto (fun i ↦ id i x) (𝓝 f) (𝓝 (f x))

Tactic:
simpa only [UniformOnFun.tendsto_iff_tendstoUniformlyOn, mem_image, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, tendstoUniformlyOn_singleton_iff_tendsto] using! @tendsto_id _ (𝓝 f)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝² : SigmaFinite ν₁
inst✝¹ : SigmaFinite ν₂
inst✝ : SigmaFinite μ
this :
  (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
⊢ μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)

Tactic:
rwa [add_right_inj] at this

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

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

Tactic:
ring

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

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

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.BoundedVariation

Goal state before:
pp: α : Type u_2
inst✝⁶ : LinearOrder α
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set α
f : α → E
g : α → F
C D : ℝ≥0∞
hf : ∀ x ∈ s, ‖f x‖ₑ ≤ C
hg : ∀ x ∈ s, ‖g x‖ₑ ≤ D
B : E →L[ℝ] F →L[ℝ] G
n : ℕ
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
⊢ (‖B‖ₑ * ∑ i ∈ Finset.range n, ‖f (u (i + 1)) - f (u i)‖ₑ) * D +
      ‖B‖ₑ * C * ∑ i ∈ Finset.range n, ‖g (u (i + 1)) - g (u i)‖ₑ =
    ‖B‖ₑ * D * ∑ i ∈ Finset.range n, ‖f (u (i + 1)) - f (u i)‖ₑ +
      ‖B‖ₑ * C * ∑ i ∈ Finset.range n, ‖g (u (i + 1)) - g (u i)‖ₑ

Tactic:
ring

Goal state after:
Module: Mathlib.Analysis.BoundedVariation

Goal state before:
pp: α : Type u_2
inst✝⁶ : LinearOrder α
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set α
f : α → E
g : α → F
C D : ℝ≥0∞
hf : ∀ x ∈ s, ‖f x‖ₑ ≤ C
hg : ∀ x ∈ s, ‖g x‖ₑ ≤ D
B : E →L[ℝ] F →L[ℝ] G
n : ℕ
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
⊢ ‖B‖ₑ * D * eVariationOn f s + ‖B‖ₑ * C * eVariationOn g s = ‖B‖ₑ * (C * eVariationOn g s + D * eVariationOn f s)

Tactic:
ring

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

Goal state before:
pp: case neg.inl
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
hfg : Set.EqOn f g (spectrum R a)
h : ¬(p a ∧ ContinuousOn g (spectrum R a))
ha : ¬p a
⊢ cfc f a = cfc g a

Tactic:
simp [cfc_apply_of_not_predicate a ha]

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

Goal state before:
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
f g : R → R
a : A
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : ¬p a
⊢ cfc (fun x ↦ f x * g x) a = cfc f a * cfc g a

Tactic:
simp [cfc_apply_of_not_predicate a ha]

Goal state after: