mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case succ
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
⊢ (descPochhammer ℤ n).smeval a * deriv (fun x ↦ (1 + x) ^ (a - ↑n)) z =
    (descPochhammer ℤ (n + 1)).smeval a * (1 + z) ^ (a - (↑n + 1))

Tactic:
rw [_root_.deriv_cpow_const (by fun_prop), deriv_const_add_id, mul_one,
      show a - (n + 1) = a - n - 1 by ring, ← mul_assoc]

Goal state after:
case succ
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
⊢ (descPochhammer ℤ n).smeval a * (a - ↑n) * (1 + z) ^ (a - ↑n - 1) =
    (descPochhammer ℤ (n + 1)).smeval a * (1 + z) ^ (a - ↑n - 1)

case succ
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
⊢ 1 + z ∈ slitPlane
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: case zero
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : p (n + 0) = 0
x✝¹ : Fin n → E
x✝ : Fin 0 → E
this : p n = 0
⊢ ((p.iteratedFDerivSeries 0 n) x✝¹) x✝ = (0 x✝¹) x✝

Tactic:
simp [FormalMultilinearSeries.iteratedFDerivSeries, this]

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

Goal state before:
pp: w x : ℂ
hw : w ≠ x
⊢ HasFPowerSeriesOnBall (fun z ↦ 1 / (z - w) ^ 2 - 1 / w ^ 2)
    (FormalMultilinearSeries.ofScalars ℂ fun i ↦ (↑i + 1) * (w - x) ^ (-↑(i + 2)) - Nat.casesOn i (w ^ (-2)) 0) x
    ‖w - x‖ₑ

Tactic:
rw [← Pi.sub_def, ← Pi.sub_def, FormalMultilinearSeries.ofScalars_sub]
  refine .sub ?_ ?_
  · simpa only [sub_sub_sub_cancel_right, zero_add, sub_sq_comm w, zpow_neg, zpow_natCast, mul_comm]
      using (one_div_sub_sq_hasFPowerSeriesOnBall_zero
        (z := w - x) (by simp [sub_eq_zero, hw])).comp_sub x
  · convert! hasFPowerSeriesOnBall_const.mono _ le_top
    · ext (_ | _) <;> simp [zpow_ofNat]
    · simpa [sub_eq_zero]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: x : EReal
n : ℕ
⊢ (↑n * x).exp = x.exp ^ n

Tactic:
← log_eq_iff,

Goal state after:
x : EReal
n : ℕ
⊢ (↑n * x).exp.log = (x.exp ^ n).log
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: x : EReal
y : ℝ
⊢ (x * ↑y).exp = x.exp ^ y

Tactic:
← log_eq_iff,

Goal state after:
x : EReal
y : ℝ
⊢ (x * ↑y).exp.log = (x.exp ^ y).log
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ (∞ ^ y).log = ↑y * ∞.log

Tactic:
rw [ENNReal.top_rpow_of_pos y_pos, log_top, EReal.mul_top_of_pos]

Goal state after:
case inr.inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ 0 < ↑y
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
⊢ expGrowthInf u = linearGrowthInf (log ∘ u)

Tactic:
by
  rfl

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

Goal state before:
pp: u : ℕ → ℝ≥0∞
⊢ expGrowthSup u = linearGrowthSup (log ∘ u)

Tactic:
by
  rfl

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

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
u : ι → ℕ → EReal
⊢ linearGrowthSup (⨆ i, u i) = ⨆ i, linearGrowthSup (u i)

Tactic:
← iSup_univ,

Goal state after:
ι : Type u_1
inst✝ : Finite ι
u : ι → ℕ → EReal
⊢ linearGrowthSup (⨆ x ∈ Set.univ, u x) = ⨆ i, linearGrowthSup (u i)
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
h : expGrowthInf u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthInf u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
⊢ expGrowthInf (u * v) ≤ expGrowthInf u + expGrowthSup v

Tactic:
rw [mul_comm, add_comm]

Goal state after:
u v : ℕ → ℝ≥0∞
h : expGrowthInf u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthInf u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
⊢ expGrowthInf (v * u) ≤ expGrowthSup v + expGrowthInf u
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
⊢ expGrowthInf u + expGrowthSup v ≤ expGrowthSup (u * v)

Tactic:
rw [mul_comm, add_comm]

Goal state after:
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup v + expGrowthInf u ≤ expGrowthSup (v * u)
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
u : ι → ℕ → ℝ≥0∞
⊢ expGrowthSup (⨆ i, u i) = ⨆ i, expGrowthSup (u i)

Tactic:
← iSup_univ,

Goal state after:
ι : Type u_1
inst✝ : Finite ι
u : ι → ℕ → ℝ≥0∞
⊢ expGrowthSup (⨆ x ∈ Set.univ, u x) = ⨆ i, expGrowthSup (u i)
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
ht : ∀ a ∈ t, r a < 0
a : ι
ha : a ∈ t
b : ι
x✝¹ : b ∈ t
x✝ : a ≠ b
⊢ Function.onFun Disjoint (fun a ↦ closedBall (x a) (r a)) a b

Tactic:
simp only [closedBall_eq_empty.2 (ht a ha), empty_disjoint, Function.onFun]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : AEMeasurable f μ
⊢ 0 < μ {x | f x ≤ ⨍⁻ (a : α), f a ∂μ}

Tactic:
simpa using
    measure_le_setLAverage_pos (measure_univ_ne_zero.2 hμ) (measure_ne_top _ _) hf.restrict

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ
h_one : μ = μ.withDensity 1
| μ

Tactic:
h_one

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ
h_one : μ = μ.withDensity 1
| μ.withDensity 1
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst✝ : SigmaFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
⊢ ν.withDensity f = 0 + ν.withDensity f

Tactic:
rw [zero_add]

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
⊢ ∃ p, Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2

Tactic:
set ξ := ⨆ (n) (k) (_ : k ≤ n), f k with 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
⊢ ∃ p, Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
Module: Mathlib.Analysis.Calculus.Monotone

Goal state before:
pp: 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)
L3 :
  Tendsto (fun y ↦ (leftLim (↑f) (y + 1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[<] x)
    (𝓝 (f.measure.rnDeriv volume x).toReal)
⊢ Tendsto (fun y ↦ (↑f y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)

Tactic:
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' L3 L2

Goal state after:
case hgf
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)
L3 :
  Tendsto (fun y ↦ (leftLim (↑f) (y + 1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[<] x)
    (𝓝 (f.measure.rnDeriv volume x).toReal)
⊢ ∀ᶠ (b : ℝ) in 𝓝[<] x, (leftLim (↑f) (b + 1 * (b - x) ^ 2) - ↑f x) / (b - x) ≤ (↑f b - ↑f x) / (b - x)

case hfh
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)
L3 :
  Tendsto (fun y ↦ (leftLim (↑f) (y + 1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[<] x)
    (𝓝 (f.measure.rnDeriv volume x).toReal)
⊢ ∀ᶠ (b : ℝ) in 𝓝[<] x, (↑f b - ↑f x) / (b - x) ≤ (leftLim (↑f) b - ↑f x) / (b - x)
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: case refine_3
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n ↦ s ∩ {x | v.limRatio ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n ↦ s ∩ {x | ↑q < v.limRatio ρ x} ∩ o n
H : ∀ (m n : ℕ), μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ (⋃ n, toMeasurable (ρ + μ) (u n)) ∩ ⋃ n, toMeasurable (ρ + μ) (w n) ⊆
    toMeasurable μ sᶜ ∪ ⋃ m, ⋃ n, toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)

Tactic:
· simp_rw [iUnion_inter, inter_iUnion]; exact subset_union_right

Goal state after:
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 : α
ha : a ∈ s
hb : b ∈ s
h : variationOnFromTo f s a b = 0
⊢ edist (f a) (f b) = 0

Tactic:
wlog h' : a ≤ b
  · rw [edist_comm]
    apply this hf hb ha _ (le_of_not_ge h')
    rw [variationOnFromTo.eq_neg_swap, h, neg_zero]
  · rw [← nonpos_iff_eq_zero, ← ENNReal.ofReal_zero, ← h, variationOnFromTo.eq_of_le f s h',
      ENNReal.ofReal_toReal (hf a b ha hb)]
    apply eVariationOn.edist_le
    exacts [⟨ha, ⟨le_rfl, h'⟩⟩, ⟨hb, ⟨h', le_rfl⟩⟩]

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
h : eVariationOn f s = 0
x : α
xs : x ∈ s
y : α
ys : y ∈ s
⊢ edist (f x) (f y) = 0

Tactic:
rw [← nonpos_iff_eq_zero, ← h]

Goal state after:
case mp
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
h : eVariationOn f s = 0
x : α
xs : x ∈ s
y : α
ys : y ∈ s
⊢ edist (f x) (f y) ≤ eVariationOn f s
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

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

Tactic:
have hs : MeasurableSet s := h.measurableSet_nullSet

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
⊢ μ + (ν - ξ) = μ + ν - ξ
Module: Mathlib.Analysis.BoundedVariation

Goal state before:
pp: case h
α : 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
i : ℕ
hi : i ∈ Finset.range n
⊢ edist ((B (f (u (i + 1)))) (g (u (i + 1)))) ((B (f (u i))) (g (u i))) ≤
    edist ((B (f (u (i + 1)))) (g (u (i + 1)))) ((B (f (u i))) (g (u (i + 1)))) +
      edist ((B (f (u i))) (g (u (i + 1)))) ((B (f (u i))) (g (u i)))

Tactic:
apply edist_triangle

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 μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ν (s ∩ f ⁻¹' {0}) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' {0})
B : ν (s ∩ f ⁻¹' {∞}) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' {∞})
n : ℤ
I : Set ℝ≥0∞ := Ico (↑t ^ n) (↑t ^ (n + 1))
⊢ ν (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))

Tactic:
have M : MeasurableSet (s ∩ f ⁻¹' I) := hs.inter (f_meas measurableSet_Ico)

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ν (s ∩ f ⁻¹' {0}) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' {0})
B : ν (s ∩ f ⁻¹' {∞}) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' {∞})
n : ℤ
I : Set ℝ≥0∞ := Ico (↑t ^ n) (↑t ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
⊢ ν (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))
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 μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})
⊢ ρ s ≤ ↑t * (μ.withDensity (v.limRatioMeas hρ)) s

Tactic:
have B : ρ (s ∩ f ⁻¹' {∞}) ≤ (t • ν) (s ∩ f ⁻¹' {∞}) := by
    apply (hρ _).le.trans zero_le
    rw [← nonpos_iff_eq_zero]
    exact (measure_mono inter_subset_right).trans (v.measure_limRatioMeas_top hρ).le

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})
B : ρ (s ∩ f ⁻¹' {∞}) ≤ (t • ν) (s ∩ f ⁻¹' {∞})
⊢ ρ s ≤ ↑t * (μ.withDensity (v.limRatioMeas hρ)) s
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 μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})
B : ρ (s ∩ f ⁻¹' {∞}) ≤ (t • ν) (s ∩ f ⁻¹' {∞})
n : ℤ
I : Set ℝ≥0∞ := Ico (↑t ^ n) (↑t ^ (n + 1))
⊢ ρ (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) ≤ (t • ν) (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))

Tactic:
have M : MeasurableSet (s ∩ f ⁻¹' I) := hs.inter (f_meas measurableSet_Ico)

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})
B : ρ (s ∩ f ⁻¹' {∞}) ≤ (t • ν) (s ∩ f ⁻¹' {∞})
n : ℤ
I : Set ℝ≥0∞ := Ico (↑t ^ n) (↑t ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
⊢ ρ (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) ≤ (t • ν) (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case succ
α : Type u_1
inst✝¹ : LinearOrder α
E✝ : Type u_2
inst✝ : PseudoEMetricSpace E✝
f : α → E✝
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  (∀ (i : ℕ), 0 < i → i < n → E i ∈ s) →
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
⊢ ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E (n + 1)))

Tactic:
by_cases hn₀ : n = 0

Goal state after:
case pos
α : Type u_1
inst✝¹ : LinearOrder α
E✝ : Type u_2
inst✝ : PseudoEMetricSpace E✝
f : α → E✝
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  (∀ (i : ℕ), 0 < i → i < n → E i ∈ s) →
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : n = 0
⊢ ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E (n + 1)))

case neg
α : Type u_1
inst✝¹ : LinearOrder α
E✝ : Type u_2
inst✝ : PseudoEMetricSpace E✝
f : α → E✝
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  (∀ (i : ℕ), 0 < i → i < n → E i ∈ s) →
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
⊢ ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E (n + 1)))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n : ℕ
⊢ ∑ i ∈ Finset.range n, eVariationOn f (Icc (I i) (I (i + 1))) = eVariationOn f (Icc (I 0) (I n))

Tactic:
convert!
      sum f hI (s := Icc (I 0) (I n)) (n := n)
        (hn := by intros; rw [mem_Icc]; constructor <;> (apply hI; lia))
    with i hi
  · simp only [right_eq_inter]
    gcongr <;> (apply hI; rw [Finset.mem_range] at hi; lia)
  · simp

Goal state after:
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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a),
    P ((cfcHom ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ })
⊢ P (cfc f a)

Tactic:
by_cases h : p a ∧ ContinuousOn f (spectrum R a)
  · rw [cfc_apply f a h.1 h.2]
    exact haf h.2 h.1
  · simp only [not_and_or] at h
    obtain (h | h) := h
    · rwa [cfc_apply_of_not_predicate _ h]
    · rwa [cfc_apply_of_not_continuousOn _ h]

Goal state after:
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
S : Type u_3
inst✝⁴ : SMul S R
inst✝³ : ContinuousConstSMul S R
inst✝² : SMulZeroClass S A
inst✝¹ : IsScalarTower S R A
inst✝ : IsScalarTower S R (R → R)
s : S
a : A
ha : p a
⊢ cfc (fun x ↦ s • x) a = s • a

Tactic:
by
  rw [cfc_smul .., cfc_id' ..]

Goal state after:
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:
by
  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
⊢ CompactSpace ↑(σₙ R a)

Tactic:
have := NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum (R := S) a

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
this : CompactSpace ↑(σₙ S a)
⊢ CompactSpace ↑(σₙ R a)