mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: case inr.refine_2
α : 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
vnonempty : v.Nonempty
a : ι
hav : a ∈ v
R0a : R0 / 2 < r a
b : ι
bu : b ∈ u
⊢ (B b ∩ ball x (R x)).Nonempty → B b ⊆ closedBall x (8 * R0)

Tactic:
hbx

Goal state after:
case inr.refine_2
α : 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
vnonempty : v.Nonempty
a : ι
hav : a ∈ v
R0a : R0 / 2 < r a
b : ι
bu : b ∈ u
hbx : (B b ∩ ball x (R x)).Nonempty
⊢ B b ⊆ closedBall x (8 * R0)
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
hμ : μ ≠ 0
hint : ∫⁻ (a : α), f a ∂μ ≠ ∞
hN : μ N = 0
this : 0 < μ ({x | ⨍⁻ (a : α), f a ∂μ ≤ f x} \ N)
x : α
hx : x ∈ {x | ⨍⁻ (a : α), f a ∂μ ≤ f x}
hxN : x ∉ N
⊢ ∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x

Tactic:
exact ⟨x, hxN, hx⟩

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : AEMeasurable f μ
hN : μ N = 0
this : 0 < μ ({x | f x ≤ ⨍⁻ (a : α), f a ∂μ} \ N)
x : α
hx : x ∈ {x | f x ≤ ⨍⁻ (a : α), f a ∂μ}
hxN : x ∉ N
⊢ ∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ

Tactic:
exact ⟨x, hxN, hx⟩

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
⊢ (r • μ).HaveLebesgueDecomposition ν

Tactic:
rw [ENNReal.smul_def]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
⊢ (↑r • μ).HaveLebesgueDecomposition ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
x✝ : MeasurableSet s
hνs : (μ.withDensity (ν.rnDeriv μ)) s = 0
t : Set α
left✝ : MeasurableSet t
ht1 : (ν.singularPart μ) t = 0
ht2 : μ tᶜ = 0
⊢ μ (s ∩ t) = 0 ∧ μ (s ∩ tᶜ) = 0

Tactic:
constructor

Goal state after:
case left
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
x✝ : MeasurableSet s
hνs : (μ.withDensity (ν.rnDeriv μ)) s = 0
t : Set α
left✝ : MeasurableSet t
ht1 : (ν.singularPart μ) t = 0
ht2 : μ tᶜ = 0
⊢ μ (s ∩ t) = 0

case right
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
x✝ : MeasurableSet s
hνs : (μ.withDensity (ν.rnDeriv μ)) s = 0
t : Set α
left✝ : MeasurableSet t
ht1 : (ν.singularPart μ) t = 0
ht2 : μ tᶜ = 0
⊢ μ (s ∩ tᶜ) = 0
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case left
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
x✝ : MeasurableSet s
hνs : (μ.withDensity (ν.rnDeriv μ)) s = 0
t : Set α
left✝ : MeasurableSet t
ht1 : (ν.singularPart μ) t = 0
ht2 : μ tᶜ = 0
⊢ (ν.singularPart μ) (s ∩ t) = 0 ∧ (μ.withDensity (ν.rnDeriv μ)) (s ∩ t) = 0

Tactic:
constructor

Goal state after:
case left.left
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
x✝ : MeasurableSet s
hνs : (μ.withDensity (ν.rnDeriv μ)) s = 0
t : Set α
left✝ : MeasurableSet t
ht1 : (ν.singularPart μ) t = 0
ht2 : μ tᶜ = 0
⊢ (ν.singularPart μ) (s ∩ t) = 0

case left.right
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
x✝ : MeasurableSet s
hνs : (μ.withDensity (ν.rnDeriv μ)) s = 0
t : Set α
left✝ : MeasurableSet t
ht1 : (ν.singularPart μ) t = 0
ht2 : μ tᶜ = 0
⊢ (μ.withDensity (ν.rnDeriv μ)) (s ∩ t) = 0
Module: Mathlib.MeasureTheory.Covering.DensityTheorem

Goal state before:
pp: case pos.inl
α : 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
⊢ closedBall y r ⊆ closedBall x ((K + 1) * r) ∧
    μ (closedBall x (3 * ((K + 1) * r))) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * μ (closedBall y r)

Tactic:
constructor

Goal state after:
case pos.inl.left
α : 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 : ℝ := ⋯
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ closedBall y r ⊆ closedBall x ((K + 1) * r)

case pos.inl.right
α : 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 : ℝ := ⋯
H : closedBall y r ⊆ closedBall x (R / 4)
hr : r ≤ R
⊢ μ (closedBall x (3 * ((K + 1) * r))) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * μ (closedBall y r)
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
⊢ HasDerivAt (↑f) (f.measure.rnDeriv volume x).toReal x

Tactic:
have L1 :
    Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[>] x) (𝓝 (rnDeriv f.measure volume x).toReal) := by
    apply Tendsto.congr' _
      ((ENNReal.tendsto_toReal h'x.ne).comp (hx.comp (Real.tendsto_Icc_vitaliFamily_right x)))
    filter_upwards [self_mem_nhdsWithin]
    rintro y (hxy : x < y)
    simp only [comp_apply, StieltjesFunction.measure_Icc, Real.volume_Icc, Classical.not_not.1 h''x]
    rw [← ENNReal.ofReal_div_of_pos (sub_pos.2 hxy), ENNReal.toReal_ofReal]
    exact div_nonneg (sub_nonneg.2 (f.mono hxy.le)) (sub_pos.2 hxy).le

Goal state after:
f : StieltjesFunction ℝ
x : ℝ
hx : Tendsto (fun a ↦ f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 : Tendsto (fun y ↦ (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
⊢ HasDerivAt (↑f) (f.measure.rnDeriv volume x).toReal x
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ k, ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ k, ⨆ (_ : k ≤ m), f k a)
⊢ ⨆ k, ⨆ (_ : k ≤ m + 1), f k a ≤ max (f m.succ a) (⨆ k, ⨆ (_ : k ≤ m), f k a) ∧
    max (f m.succ a) (⨆ k, ⨆ (_ : k ≤ m), f k a) ≤ ⨆ k, ⨆ (_ : k ≤ m + 1), f k a

Tactic:
constructor

Goal state after:
case left
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⋯
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := ⋯
hd : d = max (f m.succ a) (⨆ k, ⨆ (_ : k ≤ m), f k a)
⊢ ⨆ k, ⨆ (_ : k ≤ m + 1), f k a ≤ max (f m.succ a) (⨆ k, ⨆ (_ : k ≤ m), f k a)

case right
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⋯
hc : c = ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := ⋯
hd : d = max (f m.succ a) (⨆ k, ⨆ (_ : k ≤ m), f k a)
⊢ max (f m.succ a) (⨆ k, ⨆ (_ : k ≤ m), f k a) ≤ ⨆ k, ⨆ (_ : k ≤ m + 1), f k a
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 (ρ + μ)
⊢ ∃ a b,
    MeasurableSet a ∧ MeasurableSet b ∧ {x | v.limRatio ρ x < ↑p} ⊆ a ∧ {x | ↑q < v.limRatio ρ x} ⊆ b ∧ μ (a ∩ b) = 0

Tactic:
let u n := s ∩ {x | v.limRatio ρ x < p} ∩ o n

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
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
⊢ ∃ a b,
    MeasurableSet a ∧ MeasurableSet b ∧ {x | v.limRatio ρ x < ↑p} ⊆ a ∧ {x | ↑q < v.limRatio ρ x} ⊆ b ∧ μ (a ∩ b) = 0
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case zero
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
⊢ (fun x ↦ ⨆ k, ⨆ (_ : k ≤ 0), f k x) ∈ measurableLE μ ν

Tactic:
constructor

Goal state after:
case zero.left
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
⊢ Measurable fun x ↦ ⨆ k, ⨆ (_ : k ≤ 0), f k x

case zero.right
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
⊢ ∀ (A : Set α), MeasurableSet A → ∫⁻ (x : α) in A, (fun x ↦ ⨆ k, ⨆ (_ : k ≤ 0), f k x) x ∂μ ≤ ν A
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

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

Tactic:
· 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 a
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
⊢ eVariationOn f s ≤ ⨆ p, ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i))

pp: case a
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
⊢ ⨆ p, ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i)) ≤ eVariationOn f s

Tactic:
· apply iSup_le
    rintro ⟨n, u, u_mono, u_mem⟩
    have : ∃ p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s },
        (p.2 : ℕ → α) p.1 = u n ∧
        ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) =
        ∑ i ∈ Finset.range p.1, edist (f ((p.2 : ℕ → α) (i + 1))) (f ((p.2 : ℕ → α) i)) := by
      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)
    rcases this with ⟨p, -, hp⟩
    rw [hp]
    apply le_iSup _ p

Goal state after:
case a
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
⊢ ⨆ p, ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i)) ≤ eVariationOn f s
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 α
⊢ eVariationOn f s = 0 ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
⊢ eVariationOn f s = 0 → ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0

case mpr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
⊢ (∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0) → eVariationOn f s = 0
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
f : α → E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
hf : BoundedVariationOn f univ
a x : α
hx : ContinuousWithinAt f (Ici x) x
⊢ ContinuousWithinAt (variationOnFromTo f univ a) (Ici x) x

Tactic:
have : variationOnFromTo f univ a =
      fun y ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y := by
    ext y
    rw [variationOnFromTo.add hf.locallyBoundedVariationOn (mem_univ _) (mem_univ _) (mem_univ _)]
  rw [this]
  apply continuousWithinAt_const.add
  suffices H : ContinuousWithinAt (fun y ↦ (eVariationOn f (univ ∩ Icc x y)).toReal) (Ici x) x from
    H.congr_of_mem (fun y hy ↦ by grind [variationOnFromTo]) self_mem_Iic
  simp only [ContinuousWithinAt, Icc_self]
  rw [eVariationOn.subsingleton _ (by grind [Set.Subsingleton])]
  apply (ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp
  apply Tendsto.mono_left _ (nhdsWithin_mono _ (subset_univ _))
  exact hf.tendsto_eVariationOn_Icc_zero_right _ (by simpa using hx)

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
⊢ f = (fun x ↦ (variationOnFromTo f s c x + f x) / 2) - fun x ↦ (variationOnFromTo f s c x - f x) / 2

Tactic:
ext

Goal state after:
case inr.refine_3
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
x✝ : α
⊢ f x✝ = ((fun x ↦ (variationOnFromTo f s c x + f x) / 2) - fun x ↦ (variationOnFromTo f s c x - f x) / 2) x✝
Module: Mathlib.Topology.ContinuousMap.StarOrdered

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : PartialOrder R
inst✝⁶ : NonUnitalSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : TopologicalSpace R
inst✝² : ContinuousStar R
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousSqrt R
f g : C(α, R)
⊢ f ≤ g ↔ ∃ s, g = f + star s * s

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : PartialOrder R
inst✝⁶ : NonUnitalSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : TopologicalSpace R
inst✝² : ContinuousStar R
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousSqrt R
f g : C(α, R)
⊢ f ≤ g → ∃ s, g = f + star s * s

case mpr
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : PartialOrder R
inst✝⁶ : NonUnitalSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : TopologicalSpace R
inst✝² : ContinuousStar R
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousSqrt R
f g : C(α, R)
⊢ (∃ s, g = f + star s * s) → f ≤ g
Module: Mathlib.Topology.ContinuousMap.StarOrdered

Goal state before:
pp: case mpr
α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : PartialOrder R
inst✝⁶ : NonUnitalSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : TopologicalSpace R
inst✝² : ContinuousStar R
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousSqrt R
f g : C(α, R)
⊢ (∃ s, g = f + star s * s) → f ≤ g

Tactic:
rintro ⟨p, rfl⟩
    exact fun x ↦ le_add_of_nonneg_right (star_mul_self_nonneg (p x))

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

Goal state before:
pp: α : Type u_1
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : Zero α
R : Type u_2
inst✝⁸ : TopologicalSpace R
inst✝⁷ : CommSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : NoZeroDivisors R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : IsTopologicalSemiring R
inst✝¹ : ContinuousStar R
inst✝ : StarOrderedRing C(α, R)
f g : C(α, R)₀
⊢ f ≤ g ↔ ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), g = f + p

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : Zero α
R : Type u_2
inst✝⁸ : TopologicalSpace R
inst✝⁷ : CommSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : NoZeroDivisors R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : IsTopologicalSemiring R
inst✝¹ : ContinuousStar R
inst✝ : StarOrderedRing C(α, R)
f g : C(α, R)₀
⊢ f ≤ g → ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), g = f + p

case mpr
α : Type u_1
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : Zero α
R : Type u_2
inst✝⁸ : TopologicalSpace R
inst✝⁷ : CommSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : NoZeroDivisors R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : IsTopologicalSemiring R
inst✝¹ : ContinuousStar R
inst✝ : StarOrderedRing C(α, R)
f g : C(α, R)₀
⊢ (∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), g = f + p) → f ≤ g
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✝ : ℕ
a✝¹ : 0 < i✝
a✝ : i✝ < n
⊢ I 0 ≤ I i✝ ∧ I i✝ ≤ I n

Tactic:
constructor

Goal state after:
case left
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i✝ : ℕ
a✝¹ : 0 < i✝
a✝ : i✝ < n
⊢ I 0 ≤ I i✝

case right
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i✝ : ℕ
a✝¹ : 0 < i✝
a✝ : i✝ < n
⊢ I i✝ ≤ I n
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
s : Finset α
hne : s.Nonempty
this : 0 < s.card
u : ℕ → α := fun n ↦ (s.orderEmbOfFin ⋯) ⟨min n (s.card - 1), ⋯⟩
⊢ ↑s = u '' Iic (s.card - 1)

Tactic:
ext

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
s : Finset α
hne : s.Nonempty
this : 0 < s.card
u : ℕ → α := fun n ↦ (s.orderEmbOfFin ⋯) ⟨min n (s.card - 1), ⋯⟩
x✝ : α
⊢ x✝ ∈ ↑s ↔ x✝ ∈ u '' Iic (s.card - 1)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
s : Finset α
hne : s.Nonempty
this : 0 < s.card
u : ℕ → α := fun n ↦ (s.orderEmbOfFin ⋯) ⟨min n (s.card - 1), ⋯⟩
x✝ : α
⊢ (∃ y, (s.orderEmbOfFin ⋯) y = x✝) ↔ ∃ x ≤ s.card - 1, (s.orderEmbOfFin ⋯) ⟨min x (s.card - 1), ⋯⟩ = x✝

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
s : Finset α
hne : s.Nonempty
this : 0 < s.card
u : ℕ → α := ⋯
x✝ : α
⊢ (∃ y, (s.orderEmbOfFin ⋯) y = x✝) → ∃ x ≤ s.card - 1, (s.orderEmbOfFin ⋯) ⟨min x (s.card - 1), ⋯⟩ = x✝

case mpr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
s : Finset α
hne : s.Nonempty
this : 0 < s.card
u : ℕ → α := ⋯
x✝ : α
⊢ (∃ x ≤ s.card - 1, (s.orderEmbOfFin ⋯) ⟨min x (s.card - 1), ⋯⟩ = x✝) → ∃ y, (s.orderEmbOfFin ⋯) y = x✝
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case e'_3.a
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
⊢ φ '' t ∩ Icc (φ x) (φ y) ⊆ φ '' (t ∩ Icc x y)

Tactic:
rintro _ ⟨⟨u, us, rfl⟩, vφx, vφy⟩

Goal state after:
case e'_3.a
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
u : β
us : u ∈ t
vφx : φ x ≤ φ u
vφy : φ u ≤ φ y
⊢ φ u ∈ φ '' (t ∩ Icc x y)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case h₂
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this✝¹ : u (n + 1) ≤ a
hn : u (n + 1) = a
this✝ :
  Tendsto (fun y ↦ eVariationOn f (s ∩ Iio a) + edist (f a) (f y)) (𝓝[s ∩ Iio a] a)
    (𝓝 (eVariationOn f (s ∩ Iio a) + edist (f a) l))
this : s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a
y : α
hy : y ∈ s ∩ Ioo (u n) a
v : ℕ → α := fun i ↦ if i ≤ n then u i else if i = n + 1 then y else a
⊢ edist (f (u (n + 1))) (f (u n)) ≤ edist (f (v (n + (1 + 1)))) (f (v (n + 1))) + edist (f (v (n + 1))) (f (v n))

Tactic:
← edist_triangle

Goal state after:
case h₂
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
a : α
l : E
h : (𝓝[s ∩ Iio a] a).NeBot
ha : a ∈ s
h'f : Tendsto f (𝓝[s ∩ Iio a] a) (𝓝 l)
u : ℕ → α
n : ℕ
u_mono : StrictMonoOn u (Iic (n + 1))
u_mem : ∀ i ∈ Iic (n + 1), u i ∈ s ∩ Iic a
this✝¹ : u (n + 1) ≤ a
hn : u (n + 1) = a
this✝ :
  Tendsto (fun y ↦ eVariationOn f (s ∩ Iio a) + edist (f a) (f y)) (𝓝[s ∩ Iio a] a)
    (𝓝 (eVariationOn f (s ∩ Iio a) + edist (f a) l))
this : s ∩ Ioo (u n) a ∈ 𝓝[s ∩ Iio a] a
y : α
hy : y ∈ s ∩ Ioo (u n) a
v : ℕ → α := fun i ↦ if i ≤ n then u i else if i = n + 1 then y else a
⊢ edist (f (u (n + 1))) (f (u n)) ≤ edist (f (v (n + (1 + 1)))) (f (v n))