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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
hs : ↑s = analyticOrderAt (fun x ↦ g x - g z₀) z₀
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
⊢ ∃ g_1, AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z

Tactic:
Eq.comm,

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ⊤
hf' : ¬analyticOrderAt f (g z₀) = ⊤
r s : ℕ
hs : analyticOrderAt (fun x ↦ g x - g z₀) z₀ = ↑s
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F (g z₀)
hFne : F (g z₀) ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 (g z₀), f z = (z - g z₀) ^ r • F z
⊢ ∃ g_1, AnalyticAt 𝕜 g_1 z₀ ∧ g_1 z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f ∘ g) z = (z - z₀) ^ (r * s) • g_1 z
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : ¬EventuallyConst g (𝓝 z₀)
hf' : ¬analyticOrderAt f (g z₀) = ⊤
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (fun x ↦ g x - g z₀) z₀

Tactic:
rw [eventuallyConst_iff_analyticOrderAt_sub_eq_top] at hg_nc
    obtain ⟨r, hr⟩ := ENat.ne_top_iff_exists.mp hf'
    obtain ⟨s, hs⟩ := ENat.ne_top_iff_exists.mp hg_nc
    rw [← hr, ← hs, ← ENat.natCast_mul, (hf.comp hg).analyticOrderAt_eq_natCast]
    rw [Eq.comm, hf.analyticOrderAt_eq_natCast] at hr
    rcases hr with ⟨F, hFa, hFne, hfF⟩
    rw [Eq.comm, AnalyticAt.analyticOrderAt_eq_natCast (by fun_prop)] at hs
    rcases hs with ⟨G, hGa, hGne, hgG⟩
    -- Now write `f ∘ g` locally as the product of `(z - z₀) ^ (r * s)` and the
    -- non-vanishing analytic function `fun z ↦ (G z) ^ r • F (g z)`.
    refine ⟨fun z ↦ (G z) ^ r • F (g z), by fun_prop, by aesop, ?_⟩
    filter_upwards [EventuallyEq.comp_tendsto hfF hg.continuousAt, hgG] with z hfz hgz
    simp only [hfz, Function.comp_def, hgz, smul_eq_mul, mul_pow, mul_smul, mul_comm r s, pow_mul]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | analyticOrderAt f ↑u = ⊤}
x✝¹ : Set ↑U
x✝ : ↑U
| analyticOrderAt f ↑x✝ = ⊤

Tactic:
analyticOrderAt_eq_top,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : z ∈ {u | analyticOrderAt f ↑u = ⊤}
x✝¹ : Set ↑U
x✝ : ↑U
| ∀ᶠ (z : 𝕜) in 𝓝 ↑x✝, f z = 0
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case right
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : analyticOrderAt f ↑z = ⊤
⊢ ∃ x ⊆ {x | ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑x ∈ t},
    IsOpen[instTopologicalSpaceSubtype] x ∧ z ∈ x

Tactic:
analyticOrderAt_eq_top,

Goal state after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : AnalyticOnNhd 𝕜 f U
z : ↑U
hz : ∀ᶠ (z : 𝕜) in 𝓝 ↑z, f z = 0
⊢ ∃ x ⊆ {x | ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑x ∈ t},
    IsOpen[instTopologicalSpaceSubtype] x ∧ z ∈ x
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ p ∈ (B ∩ s) ×ˢ (B ∩ s), ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
u v : E
uv_in : (u, v) ∈ closure[instTopologicalSpaceProd] ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt (f - ⇑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
v_in : v ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (fun y ↦ ‖f y.2 - f y.1 - (f' y.2 - f' y.1)‖) (𝓝[s ×ˢ s] (u, v)) (𝓝 ‖f v - f u - (f' v - f' u)‖)

Tactic:
rw [nhdsWithin_prod_eq]

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ p ∈ (B ∩ s) ×ˢ (B ∩ s), ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
u v : E
uv_in : (u, v) ∈ closure[instTopologicalSpaceProd] ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt (f - ⇑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
v_in : v ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (fun y ↦ ‖f y.2 - f y.1 - (f' y.2 - f' y.1)‖) (𝓝[s] u ×ˢ 𝓝[s] v) (𝓝 ‖f v - f u - (f' v - f' u)‖)
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
y : ℝ
⊢ HasDerivAt f (g y) y

Tactic:
by
  rcases eq_or_ne y x with (rfl | hne)
  · exact hasDerivAt_of_hasDerivAt_of_ne f_diff hf hg
  · exact f_diff y hne

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

Goal state before:
pp: case a.h
𝕜 : 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
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < p.radius
a : ℝ
ha : a ∈ Set.Ioo 0 1
H : ∀ᶠ (n : ℕ) in atTop, |‖p n‖ * ↑r ^ n| ≤ a ^ n
⊢ ∀ᶠ (n : ℕ) in atTop, ↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))

Tactic:
· rw [← eventually_map]
      refine
        H.mp ((eventually_gt_atTop 0).mono fun n hn₀ hn => (this _ hn₀).2 (NNReal.coe_le_coe.1 ?_))
      push_cast
      exact (le_abs_self _).trans (hn.trans (pow_le_one₀ ha.1.le ha.2.le))

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

Goal state before:
pp: case convert_2
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
⊢ Set.EqOn (⇑Complex.reCLM ∘ (fun x ↦ 1 / (1 - x) ^ ↑a) ∘ ⇑Complex.ofRealCLM) (fun x ↦ 1 / (1 - x) ^ a)
    (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ))

Tactic:
intro x hx
    have : |x| < 1 := by simpa [enorm_eq_nnnorm] using! hx
    have : 0 ≤ 1 - x := by grind
    simp [-Complex.inv_re, ← Complex.ofReal_one, ← Complex.ofReal_sub, ← Complex.ofReal_cpow this]

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

Goal state before:
pp: f : ℝ → ℝ
f' x p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivWithinAt (fun y ↦ f y ^ p) (f' * p * f x ^ (p - 1)) s x

Tactic:
convert! (hasDerivAt_rpow_const hx).comp_hasDerivWithinAt x hf using 1

Goal state after:
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'
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: 𝕜 : 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
x : E
h : AnalyticOn 𝕜 f univ
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ (iteratedFDeriv 𝕜 n f x) (v ∘ ⇑σ) = (iteratedFDeriv 𝕜 n f x) v

Tactic:
by
  rw [← iteratedFDerivWithin_univ]
  exact h.iteratedFDerivWithin_comp_perm uniqueDiffOn_univ (mem_univ x) _ _

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

Goal state before:
pp: 𝕜 : 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
x : E
h : ContDiffAt 𝕜 ω f x
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ (iteratedFDeriv 𝕜 n f x) (v ∘ ⇑σ) = (iteratedFDeriv 𝕜 n f x) v

Tactic:
by
  rw [← iteratedFDerivWithin_univ]
  exact h.iteratedFDerivWithin_comp_perm uniqueDiffOn_univ (mem_univ x) _ _

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

Goal state before:
pp: case coe
a✝ : ℝ
⊢ (if Real.exp a✝ ≤ 0 then ⊥ else ↑(Real.log (Real.exp a✝))) = ↑a✝

Tactic:
if_neg (not_le.mpr (Real.exp_pos _)),

Goal state after:
case coe
a✝ : ℝ
⊢ ↑(Real.log (Real.exp a✝)) = ↑a✝
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : CommSemiring β
inst✝² : PartialOrder β
inst✝¹ : IsOrderedRing β
inst✝ : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
⊢ ∀ᶠ (b : α) in l, k b ^ z * f b ≤ k b ^ z * g' b

Tactic:
filter_upwards [hfg', hk] with x hx (hx' : 0 ≤ k x) using by gcongr

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : X
ε : ℝ
εpos : ε > 0
⊢ ∃ s ∈ v.setsAt x ∪ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}, s ⊆ closedBall x ε

Tactic:
rcases v.nontrivial x ε εpos with ⟨s, hs, h's⟩

Goal state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : X
ε : ℝ
εpos : ε > 0
s : Set X
hs : s ∈ v.setsAt x
h's : s ⊆ closedBall x ε
⊢ ∃ s ∈ v.setsAt x ∪ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}, s ⊆ closedBall x ε
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
⊢ expGrowthInf u ≤ expGrowthInf v

Tactic:
apply (expGrowthInf_eventually_monotone h).trans

Goal state after:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
⊢ (expGrowthInf fun x ↦ b * v x) ≤ expGrowthInf v
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case pos
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : u = ⊥
⊢ ⊥ ≤ (linearGrowthSup fun n ↦ ↑(v n)) * ⊥

Tactic:
exact bot_le

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

Goal state before:
pp: case pos
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
v_0 : 0 < linearGrowthInf fun n ↦ ↑(v n)
u_0 : u = ⊥
⊢ ⊥ ≤ linearGrowthSup (⊥ ∘ v)

Tactic:
exact bot_le

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

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : ¬IsFiniteMeasure μ
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν

Tactic:
rw [not_isFiniteMeasure_iff] at hμ

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : μ univ = ∞
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    μ univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ (x : α), f x ∂ν
Module: Mathlib.MeasureTheory.Measure.Sub

Goal state before:
pp: case a.refine_1
α : 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
⊢ μ ≤ ν' + ν + ⊤.restrict sᶜ

Tactic:
Measure.le_iff

Goal state after:
case a.refine_1
α : 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
⊢ ∀ (s_1 : Set α), MeasurableSet s_1 → μ s_1 ≤ (ν' + ν + ⊤.restrict sᶜ) s_1
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hξμ : ξ ≪ μ
hξν : ξ ≪ ν
⊢ ξ ≪ ν.withDensity (μ.rnDeriv ν)

Tactic:
by
  conv_rhs at hξμ => rw [μ.haveLebesgueDecomposition_add ν, add_comm]
  refine absolutelyContinuous_of_add_of_mutuallySingular hξμ ?_
  exact MutuallySingular.mono_ac (mutuallySingular_singularPart μ ν).symm hξν .rfl

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
⊢ ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ ∞

Tactic:
filter_upwards [Measure.rnDeriv_lt_top μ ν] with x hx using hx.ne

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 ν
s : Set α
hs : MeasurableSet s
h₁ : ∀ (t : Set α), MeasurableSet t → t ⊆ s → μ t ≤ ν t
h₂ : ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → ν t ≤ μ t
⊢ μ.restrict s ≤ ν.restrict s

Tactic:
Measure.le_iff

Goal state after:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : Set α
hs : MeasurableSet s
h₁ : ∀ (t : Set α), MeasurableSet t → t ⊆ s → μ t ≤ ν t
h₂ : ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → ν t ≤ μ t
⊢ ∀ (s_1 : Set α), MeasurableSet s_1 → (μ.restrict s) s_1 ≤ (ν.restrict s) s_1
Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : Set α
hs : MeasurableSet s
h₁ : ∀ (t : Set α), MeasurableSet t → t ⊆ s → μ t ≤ ν t
h₂ : ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → ν t ≤ μ t
⊢ ν.restrict sᶜ ≤ μ.restrict sᶜ

Tactic:
Measure.le_iff

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : Set α
hs : MeasurableSet s
h₁ : ∀ (t : Set α), MeasurableSet t → t ⊆ s → μ t ≤ ν t
h₂ : ∀ (t : Set α), MeasurableSet t → t ⊆ sᶜ → ν t ≤ μ t
⊢ ∀ (s_1 : Set α), MeasurableSet s_1 → (ν.restrict sᶜ) s_1 ≤ (μ.restrict sᶜ) s_1
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 μ
⊢ ν₁ + ν₂ = ν₁.singularPart μ + μ.withDensity (ν₁.rnDeriv μ) + ν₂

Tactic:
← ν₁.haveLebesgueDecomposition_add μ

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝⁴ : IsFiniteMeasure ν₁
inst✝³ : IsFiniteMeasure ν₂
inst✝² : ν₁.HaveLebesgueDecomposition μ
inst✝¹ : ν₂.HaveLebesgueDecomposition μ
inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ ν₁ + ν₂ = ν₁ + ν₂
Module: Mathlib.MeasureTheory.Covering.OneDim

Goal state before:
pp: x y : ℝ
hxy : x < y
⊢ dist x ((x + y) / 2) ≤ 1 * ((y - x) / 2)

Tactic:
rw [dist_comm, Real.dist_eq, abs_of_nonneg] <;> linarith

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

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

Tactic:
filter_upwards [Icc_mem_nhdsGT <| show x < x + ε by linarith] with y hy

Goal state after:
x ε : ℝ
εpos : ε > 0
y : ℝ
hy : y ∈ Icc x (x + ε)
⊢ Icc x y ⊆ Metric.closedBall x ε
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case inr
α : 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
ba : b ≤ a
⊢ variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ uIcc a b → ∀ ⦃y : α⦄, y ∈ s ∩ uIcc a b → edist (f x) (f y) = 0

Tactic:
rw [uIcc_of_ge ba]

Goal state after:
case inr
α : 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
ba : b ≤ a
⊢ variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ Icc b a → ∀ ⦃y : α⦄, y ∈ s ∩ Icc b a → edist (f x) (f y) = 0
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
n : ℕ
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
⊢ ∃ p,
    ↑p.snd p.fst = u n ∧
      ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) =
        ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i))

Tactic:
induction n with
      | zero => exact ⟨⟨0, ⟨u, by grind [StrictMonoOn], fun i hi ↦ u_mem _⟩⟩, by simp⟩
      | succ n ih =>
        rcases ih with ⟨⟨m, v, v_mono, v_mem⟩, hv, h'v⟩
        simp only [Finset.sum_range_succ, Sigma.exists, Subtype.exists, mem_Iic, exists_and_left,
          exists_prop]
        rcases (u_mono (Nat.le_add_right n 1)).eq_or_lt with hn | hn
        · simp only [← hn, edist_self, add_zero]
          exact ⟨m, v, hv, ⟨v_mono, v_mem⟩, h'v⟩
        · refine ⟨m + 1, fun i ↦ if i ≤ m then v i else u (n + 1), by simp,
            by grind [StrictMonoOn], ?_⟩
          simp only [h'v, ← hv, Order.add_one_le_iff, Finset.sum_range_succ, lt_self_iff_false,
            ↓reduceIte, le_refl]
          congr 1
          exact Finset.sum_congr rfl (by grind)

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

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

Tactic:
calc
    f b - f c ≤ |f c - f b| := by grw [le_abs_self (f b - f c), abs_sub_comm (f b) (f c)]
    _ ≤ variationOnFromTo f s a c - variationOnFromTo f s a b := abs_sub_le_sub_of_le hf as bs cs bc

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 μ
⊢ ν₁ + ν₂ = ν₁.singularPart μ + μ.withDensity (ν₁.rnDeriv μ) + ν₂

Tactic:
← ν₁.haveLebesgueDecomposition_add μ

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝² : SigmaFinite ν₁
inst✝¹ : SigmaFinite ν₂
inst✝ : SigmaFinite μ
⊢ ν₁ + ν₂ = ν₁ + ν₂
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case inr
α : Type u_1
inst✝² : LinearOrder α
E : Type u_3
inst✝¹ : PseudoMetricSpace E
inst✝ : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
this✝¹ : TopologicalSpace α := Preorder.topology α
this✝ : OrderTopology α
hb : (𝓝[<] b).NeBot
this :
  Tendsto f (𝓝[univ ∩ Iio b] b) (𝓝 (Function.leftLim f b)) →
    Tendsto (variationOnFromTo f univ a) (𝓝[univ ∩ Iio b] b)
      (𝓝 (variationOnFromTo f univ a b - dist (f b) (Function.leftLim f b)))
⊢ Tendsto (variationOnFromTo f univ a) (𝓝[<] b) (𝓝 (variationOnFromTo f univ a b - dist (f b) (Function.leftLim f b)))

Tactic:
simp only [univ_inter] at this

Goal state after:
case inr
α : Type u_1
inst✝² : LinearOrder α
E : Type u_3
inst✝¹ : PseudoMetricSpace E
inst✝ : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
this✝¹ : TopologicalSpace α := Preorder.topology α
this✝ : OrderTopology α
hb : (𝓝[<] b).NeBot
this :
  Tendsto f (𝓝[<] b) (𝓝 (Function.leftLim f b)) →
    Tendsto (variationOnFromTo f univ a) (𝓝[<] b) (𝓝 (variationOnFromTo f univ a b - dist (f b) (Function.leftLim f b)))
⊢ Tendsto (variationOnFromTo f univ a) (𝓝[<] b) (𝓝 (variationOnFromTo f univ a b - dist (f b) (Function.leftLim f b)))
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case inr
α : Type u_1
inst✝² : LinearOrder α
E : Type u_3
inst✝¹ : PseudoMetricSpace E
inst✝ : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
this✝¹ : TopologicalSpace α := Preorder.topology α
this✝ : OrderTopology α
hb : (𝓝[>] b).NeBot
this :
  Tendsto f (𝓝[univ ∩ Ioi b] b) (𝓝 (Function.rightLim f b)) →
    Tendsto (variationOnFromTo f univ a) (𝓝[univ ∩ Ioi b] b)
      (𝓝 (variationOnFromTo f univ a b + dist (f b) (Function.rightLim f b)))
⊢ Tendsto (variationOnFromTo f univ a) (𝓝[>] b) (𝓝 (variationOnFromTo f univ a b + dist (f b) (Function.rightLim f b)))

Tactic:
simp only [univ_inter] at this

Goal state after:
case inr
α : Type u_1
inst✝² : LinearOrder α
E : Type u_3
inst✝¹ : PseudoMetricSpace E
inst✝ : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
this✝¹ : TopologicalSpace α := Preorder.topology α
this✝ : OrderTopology α
hb : (𝓝[>] b).NeBot
this :
  Tendsto f (𝓝[>] b) (𝓝 (Function.rightLim f b)) →
    Tendsto (variationOnFromTo f univ a) (𝓝[>] b)
      (𝓝 (variationOnFromTo f univ a b + dist (f b) (Function.rightLim f b)))
⊢ Tendsto (variationOnFromTo f univ a) (𝓝[>] b) (𝓝 (variationOnFromTo f univ a b + dist (f b) (Function.rightLim f b)))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun i ↦ if i < N then u i else if i = N then x else u (i - 1)
i : ℕ
hi : i + 1 = N
A : i < N
⊢ w i ≤ w (i + 1)

Tactic:
have := Nat.find_min exists_N A

Goal state after:
case inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun i ↦ if i < N then u i else if i = N then x else u (i - 1)
i : ℕ
hi : i + 1 = N
A : i < N
this : ¬(i ≤ n ∧ x < u i)
⊢ w i ≤ w (i + 1)
Module: Mathlib.Analysis.BoundedVariation

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
h : LocallyBoundedVariationOn f univ
⊢ ∀ᵐ (x : ℝ), DifferentiableAt ℝ f x

Tactic:
by
  filter_upwards [h.ae_differentiableWithinAt_of_mem] with x hx
  rw [differentiableWithinAt_univ] at hx
  exact hx (mem_univ _)

Goal state after: