mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
U : Set 𝕜
⊢ MeromorphicOn (f ∘ fun x ↦ x + c) U ↔ MeromorphicOn f (U + {c})

Tactic:
refine ⟨fun h y hy ↦ ?_, fun h y hy ↦ ?_⟩

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
U : Set 𝕜
h : MeromorphicOn (f ∘ fun x ↦ x + c) U
y : 𝕜
hy : y ∈ U + {c}
⊢ MeromorphicAt f y

case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
U : Set 𝕜
h : MeromorphicOn f (U + {c})
y : 𝕜
hy : y ∈ U
⊢ MeromorphicAt (f ∘ fun x ↦ x + c) y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x : E
p : ℝ
m : ℕ
hf : ContDiffAt ℝ (↑m) f x
h : ↑m ≤ p
⊢ ContDiffAt ℝ (↑m) (fun x ↦ f x ^ p) x

Tactic:
← contDiffWithinAt_univ

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x : E
p : ℝ
m : ℕ
hf : ContDiffWithinAt ℝ (↑m) f Set.univ x
h : ↑m ≤ p
⊢ ContDiffWithinAt ℝ (↑m) (fun x ↦ f x ^ p) Set.univ x
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
x y : X
hx : x ∈ D
hy : y ∈ D
hne : x ≠ y
hsep : ENNReal.ofReal ↑D.packingRadius < ENNReal.ofReal (dist x y)
⊢ ↑D.packingRadius < dist x y

Tactic:
exact (ENNReal.ofReal_lt_ofReal_iff (h := dist_pos.mpr hne)).1 hsep

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

Goal state before:
pp: u : ℕ → EReal
h : 0 < linearGrowthInf u
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf u
⊢ Tendsto (fun x ↦ a * ↑x) atTop (𝓝 ⊤)

Tactic:
refine tendsto_nhds_top_iff_real.2 fun M ↦ eventually_atTop.2 ?_

Goal state after:
u : ℕ → EReal
h : 0 < linearGrowthInf u
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf u
M : ℝ
⊢ ∃ a_1, ∀ (b : ℕ), a_1 ≤ b → ↑M < a * ↑b
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
n : ℕ
⊢ u n / ↑n + v n / ↑n = (u n + v n) / ↑n

Tactic:
add_div_of_nonneg_right n.cast_nonneg'

Goal state after:
u v : ℕ → EReal
n : ℕ
⊢ u n / ↑n + v n / ↑n = u n / ↑n + v n / ↑n
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤
h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥
n : ℕ
⊢ u n / ↑n + v n / ↑n = (u n + v n) / ↑n

Tactic:
add_div_of_nonneg_right n.cast_nonneg'

Goal state after:
u v : ℕ → EReal
h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤
h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥
n : ℕ
⊢ u n / ↑n + v n / ↑n = u n / ↑n + v n / ↑n
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), ∀ s ∈ v.setsAt x ∪ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}, MeasurableSet s

Tactic:
rintro x s (hs | hs)
    exacts [v.measurableSet _ _ hs, hs.1]

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 : 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 ε

Tactic:
exact ⟨s, mem_union_left _ hs, h's⟩

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

Goal state before:
pp: u v : ℕ → ℝ≥0∞
n : ℕ
⊢ ((u n).log + (v n).log) / ↑n = (u n * v n).log / ↑n

Tactic:
log_mul_add

Goal state after:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ ((u n).log + (v n).log) / ↑n = ((u n).log + (v n).log) / ↑n
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthInf v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthInf v ≠ ⊥
n : ℕ
⊢ ((u n).log + (v n).log) / ↑n = (u n * v n).log / ↑n

Tactic:
log_mul_add

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

Goal state before:
pp: u v : ℕ → ℝ≥0∞
n : ℕ
⊢ (u n).log / ↑n + (v n).log / ↑n = ((u n).log + (v n).log) / ↑n

Tactic:
add_div_of_nonneg_right n.cast_nonneg'

Goal state after:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ (u n).log / ↑n + (v n).log / ↑n = (u n).log / ↑n + (v n).log / ↑n
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
n : ℕ
⊢ (u n).log / ↑n + (v n).log / ↑n = ((u n).log + (v n).log) / ↑n

Tactic:
add_div_of_nonneg_right n.cast_nonneg'

Goal state after:
u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
n : ℕ
⊢ (u n).log / ↑n + (v n).log / ↑n = (u n).log / ↑n + (v n).log / ↑n
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: case empty
α : Type u_1
u : α → ℕ → ℝ≥0∞
⊢ expGrowthSup (∑ x ∈ ∅, u x) = ⨆ x ∈ ∅, expGrowthSup (u x)

Tactic:
Finset.sum_empty,

Goal state after:
case empty
α : Type u_1
u : α → ℕ → ℝ≥0∞
⊢ expGrowthSup 0 = ⨆ x ∈ ∅, expGrowthSup (u x)
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ (μ univ)⁻¹ • ∫⁻ (a : α), f a ∂μ = (∫⁻ (x : α), f x ∂μ) / μ univ

Tactic:
ENNReal.div_eq_inv_mul,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ (μ univ)⁻¹ • ∫⁻ (a : α), f a ∂μ = (μ univ)⁻¹ * ∫⁻ (x : α), f x ∂μ
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → ℝ≥0∞
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ∞
htμ : μ t ≠ ∞
⊢ ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ [⨍⁻ (x : α) in s, f x ∂μ -[ℝ≥0∞] ⨍⁻ (x : α) in t, f x ∂μ]

Tactic:
by_cases hs₀ : μ s = 0
  · rw [← ae_eq_empty] at hs₀
    rw [restrict_congr_set (hs₀.union EventuallyEq.rfl), empty_union]
    exact right_mem_segment _ _ _
  · refine
      ⟨μ s / (μ s + μ t), μ t / (μ s + μ t), zero_le, zero_le, ?_, (laverage_union hd ht).symm⟩
    rw [← ENNReal.add_div,
      ENNReal.div_self (add_eq_zero.not.2 fun h => hs₀ h.1) (add_ne_top.2 ⟨hsμ, htμ⟩)]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : α → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), μ (closedBall x (20 * R x)) < ∞
t' : Set ι := {a | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
x✝ : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x
R0 : ℝ := sSup (r '' v)
R0_def : R0 = sSup (r '' v)
R0_bdd : BddAbove (r '' v)
H : R x ≤ R0
R0pos : 0 < R0
h : ¬v.Nonempty
⊢ False

Tactic:
nonempty_iff_ne_empty,

Goal state after:
α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : α → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), μ (closedBall x (20 * R x)) < ∞
t' : Set ι := {a | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
x✝ : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
Idist_v : ∀ a ∈ v, dist (c a) x ≤ r a + R x
R0 : ℝ := sSup (r '' v)
R0_def : R0 = sSup (r '' v)
R0_bdd : BddAbove (r '' v)
H : R x ≤ R0
R0pos : 0 < R0
h : ¬v ≠ ∅
⊢ False
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ Measurable (μ.rnDeriv ν)

Tactic:
by_cases h : HaveLebesgueDecomposition μ ν

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ.HaveLebesgueDecomposition ν
⊢ Measurable (μ.rnDeriv ν)

case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ Measurable (μ.rnDeriv ν)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

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

Tactic:
by_cases h : HaveLebesgueDecomposition μ ν

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ⟂ₘ ν

case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ⟂ₘ ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

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

Tactic:
have := h.haveLebesgueDecomposition

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
this : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν = μ
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: case refine_1
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (fun i ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (fun i ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I : ∀ᶠ (i : ι) in l, ∫ (y : α), g i y • (f y - c) ∂μ + (∫ (y : α), g i y ∂μ) • c = ∫ (y : α), g i y • f y ∂μ
this✝ : Tendsto (fun x ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
h''i : IntegrableOn f (a i) μ
hi_int : 0 < ∫ (y : α), g i y ∂μ
mu_ai : μ (a i) < ∞
this : ∀ x ∉ a i, ‖g i x‖ * ‖f x - c‖ = 0
⊢ Integrable (fun a_1 ↦ K / (μ.restrict (a i)).real univ * ‖f a_1 - c‖) (μ.restrict (a i))

Tactic:
apply (Integrable.sub h''i _).norm.const_mul

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (fun i ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (fun i ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I : ∀ᶠ (i : ι) in l, ∫ (y : α), g i y • (f y - c) ∂μ + (∫ (y : α), g i y ∂μ) • c = ∫ (y : α), g i y • f y ∂μ
this✝ : Tendsto (fun x ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
h''i : IntegrableOn f (a i) μ
hi_int : 0 < ∫ (y : α), g i y ∂μ
mu_ai : μ (a i) < ∞
this : ∀ x ∉ a i, ‖g i x‖ * ‖f x - c‖ = 0
⊢ Integrable (fun x ↦ c) (μ.restrict (a i))
Module: Mathlib.MeasureTheory.Covering.DensityTheorem

Goal state before:
pp: case h
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
⊢ 3 * (R / 4) + dist x y ≤ r

Tactic:
have A : y ∈ closedBall y r := mem_closedBall_self rpos.le

Goal state after:
case h
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
A : y ∈ closedBall y r
⊢ 3 * (R / 4) + dist x y ≤ r
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ρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0
hc : ↑c ∈ w
d : ℝ≥0
hd : ↑d ∈ w
hcd : ↑c < ↑d
x : α
h1x : ∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < ↑c
a✝ : ∃ᶠ (x : Set α) in v.filterAt x, ↑d < ρ x / μ x
a : Set α
ha : ρ a / μ a < ↑c
⊢ μ a ≠ 0 ∨ ↑c ≠ ∞

Tactic:
simp only [ENNReal.coe_ne_top, Ne, or_true, not_false_iff]

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ρ : ρ ≪ μ
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
m n : ℕ
I✝ : (ρ + μ) (u m) ≠ ∞
J : (ρ + μ) (w n) ≠ ∞
x : α
hx : x ∈ u m ∩ toMeasurable (ρ + μ) (w n)
L : Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))
I : ∀ᶠ (b : Set α) in v.filterAt x, ρ b / μ b < ↑p
a : Set α
ha : ρ a / μ a < ↑p
⊢ μ a ≠ 0 ∨ ↑p ≠ ∞

Tactic:
simp only [ENNReal.coe_ne_top, Ne, or_true, not_false_iff]

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

Goal state before:
pp: 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
this :
  Tendsto (fun y ↦ (↑hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[>] x)
    (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
y : ℝ
hy : y ∈ Ioi x
⊢ (↑hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x) ≤ (f y - f x) / (y - x)

Tactic:
rw [mem_Ioi, ← sub_pos] at hy

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
this :
  Tendsto (fun y ↦ (↑hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[>] x)
    (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
y : ℝ
hy : 0 < y - x
⊢ (↑hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x) ≤ (f y - f x) / (y - x)
Module: Mathlib.Analysis.Calculus.Monotone

Goal state before:
pp: 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
this :
  Tendsto (fun y ↦ (↑hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[>] x)
    (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
y : ℝ
hy : y ∈ Ioi x
⊢ (f y - f x) / (y - x) ≤ (↑hf.stieltjesFunction y - f x) / (y - x)

Tactic:
rw [mem_Ioi, ← sub_pos] at hy

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
this :
  Tendsto (fun y ↦ (↑hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[>] x)
    (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
y : ℝ
hy : 0 < y - x
⊢ (f y - f x) / (y - x) ≤ (↑hf.stieltjesFunction y - f x) / (y - x)
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ρ : ρ ≪ μ
⊢ AEMeasurable (v.limRatio ρ) μ

Tactic:
apply ENNReal.aemeasurable_of_exist_almost_disjoint_supersets _ _ fun p q hpq => ?_

Goal state after:
α : 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
⊢ ∃ u v_1,
    MeasurableSet u ∧
      MeasurableSet v_1 ∧ {x | v.limRatio ρ x < ↑p} ⊆ u ∧ {x | ↑q < v.limRatio ρ x} ⊆ v_1 ∧ μ (u ∩ v_1) = 0
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ρ : ρ ≪ μ
p : ℝ≥0
s : Set α
h : s ⊆ {x | v.limRatioMeas hρ x < ↑p}
t : Set α := {x | Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : μ tᶜ = 0
H : ρ (s ∩ t) ≤ (p • μ) (s ∩ t)
⊢ ρ s = ρ (s ∩ t ∪ s ∩ tᶜ)

Tactic:
rw [inter_union_compl]

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ρ : ρ ≪ μ
p : ℝ≥0
s : Set α
h : s ⊆ {x | v.limRatioMeas hρ x < ↑p}
t : Set α := {x | Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : μ tᶜ = 0
x : α
hx : x ∈ s ∩ t
I : ∀ᶠ (b : Set α) in v.filterAt x, ρ b / μ b < ↑p
a : Set α
ha : ρ a / μ a < ↑p
⊢ μ a ≠ 0 ∨ ↑p ≠ ∞

Tactic:
simp only [ENNReal.coe_ne_top, Ne, or_true, not_false_iff]

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ρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < v.limRatioMeas hρ x}
t : Set α := {x | Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : μ tᶜ = 0
H : (q • μ) (s ∩ t) ≤ ρ (s ∩ t)
⊢ (q • μ) s = (q • μ) (s ∩ t ∪ s ∩ tᶜ)

Tactic:
rw [inter_union_compl]

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
E : Type u_3
inst✝¹ : PseudoMetricSpace E
inst✝ : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
⊢ Function.leftLim (variationOnFromTo f univ a) b = variationOnFromTo f univ a b - dist (f b) (Function.leftLim f b)

Tactic:
let : TopologicalSpace α := Preorder.topology α

Goal state after:
α : 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 α
⊢ Function.leftLim (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: α : Type u_1
inst✝² : LinearOrder α
E : Type u_3
inst✝¹ : PseudoMetricSpace E
inst✝ : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
⊢ Function.rightLim (variationOnFromTo f univ a) b = variationOnFromTo f univ a b + dist (f b) (Function.rightLim f b)

Tactic:
let : TopologicalSpace α := Preorder.topology α

Goal state after:
α : 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 α
⊢ Function.rightLim (variationOnFromTo f univ a) b = variationOnFromTo f univ a b + dist (f b) (Function.rightLim f b)
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
h : LocallyBoundedVariationOn f ∅
⊢ ∃ p q,
    MonotoneOn p ∅ ∧ MonotoneOn q ∅ ∧ f = p - q ∧ ∀ x ∈ ∅, ∀ y ∈ ∅, p y - p x + (q y - q x) = variationOnFromTo f ∅ x y

Tactic:
refine ⟨f, 0, subsingleton_empty.monotoneOn _, subsingleton_empty.monotoneOn _,
      (sub_zero f).symm, fun x hx y hy ↦ by simp at hx⟩

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
⊢ ∑ i ∈ Finset.range n, edist ((B (f (u (i + 1)))) (g (u (i + 1)))) ((B (f (u i))) (g (u i))) ≤
    ∑ x ∈ Finset.range n,
      (edist ((B (f (u (x + 1)))) (g (u (x + 1)))) ((B (f (u x))) (g (u (x + 1)))) +
        edist ((B (f (u x))) (g (u (x + 1)))) ((B (f (u x))) (g (u x))))

Tactic:
gcongr with i hi

Goal state after:
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)))