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

Goal state before:
pp: case neg
α : 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, 0 < r a
t' : Set ι := {a | a ∈ t ∧ 0 < r a}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint fun a ↦ ball (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
A : ∀ a ∈ t', ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)
⊢ ∃ u ⊆ t, (u.PairwiseDisjoint fun a ↦ ball (x a) (r a)) ∧ ∀ a ∈ t, ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)

Tactic:
refine ⟨u, ut'.trans fun a ha => ha.1, u_disj, fun a ha => ?_⟩

Goal state after:
case neg
α : 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, 0 < r a
t' : Set ι := {a | a ∈ t ∧ 0 < r a}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint fun a ↦ ball (x a) (r a)
hu : ∀ a ∈ t', ∃ b ∈ u, (ball (x a) (r a) ∩ ball (x b) (r b)).Nonempty ∧ r a ≤ (τ - 1) / 2 * r b
A : ∀ a ∈ t', ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)
a : ι
ha : a ∈ t
⊢ ∃ b ∈ u, ball (x a) (r a) ⊆ ball (x b) (τ * r b)
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf' : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ ((∫⁻ (x : α), f x ∂μ) / μ univ).toReal = (μ.real univ)⁻¹ * ∫ (x : α), (f x).toReal ∂μ

Tactic:
toReal_div,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf' : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ (∫⁻ (x : α), f x ∂μ).toReal / (μ univ).toReal = (μ.real univ)⁻¹ * ∫ (x : α), (f x).toReal ∂μ
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)
⊢ BddAbove (r '' v)

Tactic:
refine ⟨1, fun r' hr' => ?_⟩

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)
r' : ℝ
hr' : r' ∈ r '' v
⊢ r' ≤ 1
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case refine_1
α : 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
⊢ ∀ (n : ℕ), AEMeasurable (⨆ k, ⨆ (_ : k ≤ n), f k) ν

pp: case refine_2
α : 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
⊢ ∀ᵐ (x : α) ∂ν, Monotone fun n ↦ (⨆ k, ⨆ (_ : k ≤ n), f k) x

pp: case refine_3
α : 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
⊢ ∀ᵐ (x : α) ∂ν,
    Filter.Tendsto (fun n ↦ (⨆ k, ⨆ (_ : k ≤ n), f k) x) Filter.atTop (nhds ((⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k) x))

Tactic:
· intro n
        refine Measurable.aemeasurable ?_
        convert! (iSup_mem_measurableLE _ hf₁ n).1
        simp

Goal state after:
case refine_2
α : 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
⊢ ∀ᵐ (x : α) ∂ν, Monotone fun n ↦ (⨆ k, ⨆ (_ : k ≤ n), f k) x

case refine_3
α : 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
⊢ ∀ᵐ (x : α) ∂ν,
    Filter.Tendsto (fun n ↦ (⨆ k, ⨆ (_ : k ≤ n), f k) x) Filter.atTop (nhds ((⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k) x))
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
⊢ variationOnFromTo f s a b - variationOnFromTo f s a c = variationOnFromTo f s c b

Tactic:
← variationOnFromTo.add hf ha hc hb,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
⊢ variationOnFromTo f s a c + variationOnFromTo f s c b - variationOnFromTo f s a c = variationOnFromTo f s c b
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
⊢ variationOnFromTo f s a b - variationOnFromTo f s c b = variationOnFromTo f s a c

Tactic:
← variationOnFromTo.add hf ha hc hb,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
⊢ variationOnFromTo f s a c + variationOnFromTo f s c b - variationOnFromTo f s c b = variationOnFromTo f s a c
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

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

Tactic:
intro x hx y hy hxy
    dsimp
    gcongr 1
    simpa using variationOnFromTo.add_self_monotoneOn h cs hx hy hxy

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

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

Tactic:
intro x hx y hy

Goal state after:
case inr.refine_4
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ (fun x ↦ (variationOnFromTo f s c x + f x) / 2) y - (fun x ↦ (variationOnFromTo f s c x + f x) / 2) x +
      ((fun x ↦ (variationOnFromTo f s c x - f x) / 2) y - (fun x ↦ (variationOnFromTo f s c x - f x) / 2) x) =
    variationOnFromTo f s x y
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))
M : MeasurableSet (s ∩ f ⁻¹' I)
⊢ ↑t ^ (n + 1) * μ (s ∩ f ⁻¹' I) = ↑t ^ 2 * (↑t ^ (n - 1) * μ (s ∩ f ⁻¹' I))

Tactic:
rw [← mul_assoc, ← ENNReal.zpow_add t_ne_zero ENNReal.coe_ne_top]

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)
⊢ ↑t ^ (n + 1) * μ (s ∩ f ⁻¹' I) = ↑t ^ (2 + (n - 1)) * μ (s ∩ f ⁻¹' I)
Module: Mathlib.Analysis.BoundedVariation

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
s : Set ℝ
h : LocallyBoundedVariationOn f s
A : V ≃L[ℝ] ↑(Module.Basis.ofVectorSpaceIndex ℝ V) → ℝ :=
  (Module.Basis.ofVectorSpace ℝ V).equivFun.toContinuousLinearEquiv
H : ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
x : ℝ
hx : x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
xs : x ∈ s
⊢ DifferentiableWithinAt ℝ f s x

Tactic:
exact (ContinuousLinearEquiv.comp_differentiableWithinAt_iff _).mp (hx xs)

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

Goal state before:
pp: 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✝

Tactic:
rintro ⟨i, hi, rfl⟩; use ⟨i, by omega⟩; congr; omega

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

Goal state before:
pp: case refine_2
α : 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)
b : α
hb : b ∈ s ∩ Iio a
this : Nonempty ((n : ℕ) × { u // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iio a })
⊢ eVariationOn f (s ∩ Iio a) + edist (f a) l ≤ eVariationOn f (s ∩ Iic a)

Tactic:
rw [eVariationOn_eq_strictMonoOn, ENNReal.iSup_add]

Goal state after:
case refine_2
α : 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)
b : α
hb : b ∈ s ∩ Iio a
this : Nonempty ((n : ℕ) × { u // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s ∩ Iio a })
⊢ ⨆ i, ∑ i_1 ∈ Finset.range i.fst, edist (f (↑i.snd (i_1 + 1))) (f (↑i.snd i_1)) + edist (f a) l ≤
    eVariationOn f (s ∩ Iic a)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:

Tactic:
∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x))
    _ = ∑ i ∈ Finset.range n, edist (f (v (i + 1))) (f (v i)) := by grind [Finset.sum_congr]
    _ ≤ eVariationOn f (s ∩ Icc (u 0) (u n)) :=
      sum_le_of_monotoneOn_Iic (by grind [MonotoneOn]) (by grind)

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x y : α
⊢ eVariationOn f (s ∩ Ioc x y) = eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' (s ∩ Ioc x y))

Tactic:
comp_ofDual

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x y : α
⊢ eVariationOn f (s ∩ Ioc x y) = eVariationOn f (s ∩ Ioc x y)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : BoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Ioi x] x) (𝓝 l)
hx : x ∈ s
y : α
⊢ eVariationOn f (s ∩ Icc x y) = eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' (s ∩ Icc x y))

Tactic:
comp_ofDual

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : BoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Ioi x] x) (𝓝 l)
hx : x ∈ s
y : α
⊢ eVariationOn f (s ∩ Icc x y) = eVariationOn f (s ∩ Icc x y)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : LocallyBoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Ioi x] x) (𝓝 l)
hx : x ∈ s
y : α
⊢ eVariationOn f (s ∩ Icc x y) = eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' (s ∩ Icc x y))

Tactic:
comp_ofDual

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
l : E
hf : LocallyBoundedVariationOn f s
x : α
h'f : Tendsto f (𝓝[s ∩ Ioi x] x) (𝓝 l)
hx : x ∈ s
y : α
⊢ eVariationOn f (s ∩ Icc x y) = eVariationOn f (s ∩ Icc x y)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Ici x) x
y : α
⊢ eVariationOn f (s ∩ Icc x y) = eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' (s ∩ Icc x y))

Tactic:
comp_ofDual

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
s : Set α
hf : BoundedVariationOn f s
x : α
h : ContinuousWithinAt f (s ∩ Ici x) x
y : α
⊢ eVariationOn f (s ∩ Icc x y) = eVariationOn f (s ∩ Icc x y)
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✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : MetricSpace R
inst✝¹⁰ : IsTopologicalSemiring R
inst✝⁹ : ContinuousStar R
inst✝⁸ : ContinuousSqrt R
inst✝⁷ : StarOrderedRing R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ IsStrictlyPositive (cfc f a) ↔ ∀ x ∈ spectrum R a, 0 < f x

Tactic:
rw [cfc_apply .., cfcHom_isStrictlyPositive_iff]

Goal state after:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁴ : CommSemiring R
inst✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : MetricSpace R
inst✝¹⁰ : IsTopologicalSemiring R
inst✝⁹ : ContinuousStar R
inst✝⁸ : ContinuousSqrt R
inst✝⁷ : StarOrderedRing R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : ContinuousOn f (spectrum R a)
ha : p a
⊢ (∀ (x : ↑(spectrum R a)), 0 < { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ } x) ↔
    ∀ x ∈ spectrum R a, 0 < f x
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Goal state before:
pp: case neg.inr.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
hfg : Set.EqOn f g (σₙ R a)
h0 : ¬g 0 = 0
⊢ cfcₙ f a = 0

Tactic:
cfcₙ_apply_of_not_map_zero

Goal state after:
case neg.inr.inr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
hfg : Set.EqOn f g (σₙ R a)
h0 : ¬g 0 = 0
⊢ 0 = 0

case neg.inr.inr.hf
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
hfg : Set.EqOn f g (σₙ R a)
h0 : ¬g 0 = 0
⊢ ¬f 0 = 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 α
hf : BoundedVariationOn f s
y : α
⊢ eVariationOn f (s ∩ Iic y) = eVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' (s ∩ Iic y))

Tactic:
comp_ofDual

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
y : α
⊢ eVariationOn f (s ∩ Iic y) = eVariationOn f (s ∩ Iic y)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
C : ℝ
hf : MonotoneOn f s
h : ∀ x ∈ s, |f x| ≤ C
⊢ ∀ (a b : α), a ∈ s → b ∈ s → a ≤ b → eVariationOn f (s ∩ Set.Icc a b) ≤ ENNReal.ofReal (2 * C)

Tactic:
intro a b as bs hab

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
C : ℝ
hf : MonotoneOn f s
h : ∀ x ∈ s, |f x| ≤ C
a b : α
as : a ∈ s
bs : b ∈ s
hab : a ≤ b
⊢ eVariationOn f (s ∩ Set.Icc a b) ≤ ENNReal.ofReal (2 * C)
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: case refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : X → X → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), (g x y) x = f x
w₂ : ∀ (x y : X), (g x y) y = f y
U : X → X → Set X := fun x y ↦ {z | f z - ε < (g x y) z}
x y : X
⊢ f y - ε < f y

Tactic:
exact sub_lt_self _ pos

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν +
        (1 - (2 * n) • X) * ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν +
      n ^ 2 • X ^ 2 * ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν
⊢ ∑ ν ∈ Finset.range (n + 1), (n • X - ↑ν) ^ 2 * bernsteinPolynomial R n ν = n • X * (1 - X)

Tactic:
conv at p =>
    rhs
    rw [sum, sum_smul, sum_mul_smul, ← natCast_mul]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
p :
  ∑ x ∈ Finset.range (n + 1),
      (↑(x * (x - 1)) + (1 - ↑(2 * n) * X) * ↑x + ↑(n ^ 2) * X ^ 2) * bernsteinPolynomial R n x =
    ↑(n * (n - 1)) * X ^ 2 + (1 - (2 * n) • X) * n • X + n ^ 2 • X ^ 2 * 1
⊢ ∑ ν ∈ Finset.range (n + 1), (n • X - ↑ν) ^ 2 * bernsteinPolynomial R n ν = n • X * (1 - X)
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : C(X, ℝ)
⊢ f ∈ A.topologicalClosure

Tactic:
by
  rw [subalgebra_topologicalClosure_eq_top_of_separatesPoints A w]
  simp

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

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key : (↑I).range ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure
f : C(X, 𝕜)
f_re : C(X, ℝ) := { toFun := ⇑re, continuous_toFun := ⋯ }.comp f
f_im : C(X, ℝ) := { toFun := ⇑im, continuous_toFun := ⋯ }.comp f
h_f_re : I f_re ∈ A.topologicalClosure
h_f_im : I f_im ∈ A.topologicalClosure
this : I f_re + RCLike.I • I f_im ∈ A.topologicalClosure.toSubalgebra
⊢ f ∈ A.topologicalClosure

Tactic:
StarSubalgebra.mem_toSubalgebra

Goal state after:
𝕜 : Type u_1
X : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : StarSubalgebra 𝕜 C(X, 𝕜)
hA : A.SeparatesPoints
I : C(X, ℝ) →L[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM
key : (↑I).range ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure
f : C(X, 𝕜)
f_re : C(X, ℝ) := { toFun := ⇑re, continuous_toFun := ⋯ }.comp f
f_im : C(X, ℝ) := { toFun := ⇑im, continuous_toFun := ⋯ }.comp f
h_f_re : I f_re ∈ A.topologicalClosure
h_f_im : I f_im ∈ A.topologicalClosure
this : I f_re + RCLike.I • I f_im ∈ A.topologicalClosure
⊢ f ∈ A.topologicalClosure