mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A, ξ a ∂ν ≤ μ A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ν E
hE₃ : ∀ (A : Set α), MeasurableSet A → ↑ε * ν (A ∩ E) ≤ (μ - ν.withDensity ξ) (A ∩ E)
hε₂ : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν ≤ μ (A ∩ E)
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (a : α) in A, ξ a ∂ν + ↑ε * ν (A ∩ E) = ↑ε * ν (A ∩ E) + ∫⁻ (a : α) in A, ξ a ∂ν

Tactic:
add_comm

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A, ξ a ∂ν ≤ μ A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ν E
hE₃ : ∀ (A : Set α), MeasurableSet A → ↑ε * ν (A ∩ E) ≤ (μ - ν.withDensity ξ) (A ∩ E)
hε₂ : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν ≤ μ (A ∩ E)
A : Set α
hA : MeasurableSet A
⊢ ↑ε * ν (A ∩ E) + ∫⁻ (a : α) in A, ξ a ∂ν = ↑ε * ν (A ∩ E) + ∫⁻ (a : α) in A, ξ 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 α
a : α
⊢ variationOnFromTo f s a a = 0

Tactic:
by
  dsimp only [variationOnFromTo]
  rw [if_pos le_rfl, Icc_self, eVariationOn.subsingleton, ENNReal.toReal_zero]
  exact fun x hx y hy => hx.2.trans hy.2.symm

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)
⊢ ρ (s ∩ t) + (q • μ) tᶜ = ρ (s ∩ t)

Tactic:
by simp [A]

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

Goal state before:
pp: case inl
α : 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
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)

Tactic:
variationOnFromTo.eq_of_le _ _ h,

Goal state after:
case inl
α : 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
⊢ (eVariationOn (f ∘ φ) (t ∩ Icc x y)).toReal = variationOnFromTo f (φ '' t) (φ 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 : ℤ
⊢ ν (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))

Tactic:
let I := Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))

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))
⊢ ν (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))
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)
p : C(α, R)
f g : C(α, R)₀
hp : ↑g = ↑f + 0
⊢ g = f + 0

Tactic:
by ext x; congrm($(hp) x)

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

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

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

Tactic:
· rw [le_def, ← ContinuousMap.coe_coe, ← ContinuousMap.coe_coe g, ← ContinuousMap.le_def,
        StarOrderedRing.le_iff]
      rintro ⟨p, hp_mem, hp⟩
      induction hp_mem using AddSubmonoid.closure_induction_left generalizing f g with
      | zero => exact ⟨0, zero_mem _, by ext x; congrm($(hp) x)⟩
      | add_left s s_mem p p_mem hp' =>
        obtain ⟨s, rfl⟩ := s_mem
        simp only at *
        have h₀ : (star s * s + p) 0 = 0 := by simpa using congr($(hp) 0).symm
        rw [← add_assoc] at hp
        have p'₀ : 0 ≤ p 0 := by rw [← StarOrderedRing.nonneg_iff] at p_mem; exact p_mem 0
        have s₉ : (star s * s) 0 = 0 := le_antisymm ((le_add_of_nonneg_right p'₀).trans_eq h₀)
          (star_mul_self_nonneg (s 0))
        have s₀' : s 0 = 0 := by aesop
        let s' : C(α, R)₀ := ⟨s, s₀'⟩
        obtain ⟨p', hp'_mem, rfl⟩ := hp' (f + star s' * s') g hp
        refine ⟨star s' * s' + p', ?_, by rw [add_assoc]⟩
        exact add_mem (AddSubmonoid.subset_closure ⟨s', rfl⟩) hp'_mem

Goal state after:
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.MeasureTheory.Covering.Differentiation

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

Tactic:
let I := Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))

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

Goal state before:
pp: case refine_2
α : 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
⊢ ρ s ≤ (μ.withDensity (v.limRatioMeas hρ)) s

Tactic:
· have :
      Tendsto (fun t : ℝ≥0 => (t : ℝ≥0∞) * μ.withDensity (v.limRatioMeas hρ) s) (𝓝[>] 1)
        (𝓝 ((1 : ℝ≥0∞) * μ.withDensity (v.limRatioMeas hρ) s)) := by
      refine ENNReal.Tendsto.mul_const (ENNReal.tendsto_coe.2 nhdsWithin_le_nhds) ?_
      simp only [true_or, Ne, not_false_iff, one_ne_zero]
    simp only [one_mul] at this
    refine ge_of_tendsto this ?_
    filter_upwards [self_mem_nhdsWithin] with _ ht
    exact v.le_mul_withDensity hρ hs ht

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
a b : α
hab : a ≤ b
⊢ ∀ (i : (n : ℕ) × { u // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ {a, b} }),
    ∑ i_1 ∈ Finset.range i.fst, edist (f (↑i.snd (i_1 + 1))) (f (↑i.snd i_1)) ≤ edist (f a) (f b)

Tactic:
rintro ⟨n, u, hmono, hi⟩

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
a b : α
hab : a ≤ b
n : ℕ
u : ℕ → α
hmono : StrictMonoOn u (Iic n)
hi : ∀ i ∈ Iic n, u i ∈ {a, b}
⊢ ∑ i ∈ Finset.range ⟨n, ⟨u, ⋯⟩⟩.fst, edist (f (↑⟨n, ⟨u, ⋯⟩⟩.snd (i + 1))) (f (↑⟨n, ⟨u, ⋯⟩⟩.snd i)) ≤ edist (f a) (f b)
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 α
⊢ BoundedVariationOn f ↑s

Tactic:
obtain rfl | hne := s.eq_empty_or_nonempty

Goal state after:
case inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
⊢ BoundedVariationOn f ↑∅

case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
s : Finset α
hne : s.Nonempty
⊢ BoundedVariationOn f ↑s
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: case e_a
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ∞
x : α
hx : Tendsto (fun a ↦ (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / μ a) (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
a : Set α
⊢ f =ᵐ[μ.restrict a] AEMeasurable.mk f hf

Tactic:
exact ae_restrict_of_ae hf.ae_eq_mk

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

Goal state before:
pp: case inr
α : Type u_1
inst✝⁴ : LinearOrder α
E : Type u_2
inst✝³ : PseudoEMetricSpace E
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : α → E
a b : α
h' : ContinuousWithinAt f (Ici a) a
hab : a < b
this : (𝓝[>] a).NeBot
⊢ eVariationOn f (Ioc a b) = eVariationOn f (Icc a b)

Tactic:
exact eVariationOn_Ioc_eq_Icc_of_continuousWithinAt' h'

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
a b : α
h : (𝓝[<] a).NeBot
h' : ContinuousWithinAt f (Iic a) a
⊢ eVariationOn (f ∘ ⇑ofDual) (Ioc (toDual a) (toDual b)) = eVariationOn (f ∘ ⇑ofDual) (Icc (toDual a) (toDual b))

Tactic:
exact eVariationOn_Ioc_eq_Icc_of_continuousWithinAt' h'

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✝¹ : CompleteSpace E
inst✝ : DenselyOrdered α
f : α → E
a : α
hf : BoundedVariationOn f univ
this✝¹ : TopologicalSpace α := Preorder.topology α
this✝ : OrderTopology α
ha : ¬IsBot a
this : (𝓝[<] a).NeBot
⊢ (𝓝[univ ∩ Iio a] a).NeBot

Tactic:
simpa

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 g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this✝ : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
this : ∀ᶠ (b : ℕ → E) in Filter.pi fun i ↦ 𝓝 (g (u i)), c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)
I : Set ℕ
I_fin : I.Finite
t : ℕ → Set E
t_mem : ∀ (i : ℕ), t i ∈ 𝓝 (g (u i))
ht : I.pi t ⊆ {b | c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)}
⊢ ∀ i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}, ∀ᶠ (x : ℕ → α) in 𝓝 u, x i.1 < x i.2

Tactic:
intro i hi

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f g : α → E
s : Set α
hg : ∀ x ∈ s, MapClusterPt (g x) (𝓝[s] x) f
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
this✝ : Nonempty α
c : ℝ≥0∞
hc : c < ∑ x ∈ Finset.range n, edist (g (u (x + 1))) (g (u x))
this : ∀ᶠ (b : ℕ → E) in Filter.pi fun i ↦ 𝓝 (g (u i)), c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)
I : Set ℕ
I_fin : I.Finite
t : ℕ → Set E
t_mem : ∀ (i : ℕ), t i ∈ 𝓝 (g (u i))
ht : I.pi t ⊆ {b | c < ∑ i ∈ Finset.range n, edist (b (i + 1)) (b i)}
i : ℕ × ℕ
hi : i ∈ {i ∈ Finset.Iic n ×ˢ Finset.Iic n | i.1 < i.2}
⊢ ∀ᶠ (x : ℕ → α) in 𝓝 u, x i.1 < x i.2
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
a : A
ha : p a
f : C(↑(spectrum R a), R)
⊢ IsStrictlyPositive ((cfcHom ha) f) ↔ ∀ (x : ↑(spectrum R a)), 0 < f x

Tactic:
refine ⟨fun hf x => hf.spectrum_pos <| cfcHom_map_spectrum (R := R) ha _ ▸ Set.mem_range_self x,
    fun h => ⟨cfcHom_nonneg_iff _ |>.mpr fun x => le_of_lt (h x), ?_⟩⟩

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
a : A
ha : p a
f : C(↑(spectrum R a), R)
h : ∀ (x : ↑(spectrum R a)), 0 < f x
⊢ IsUnit ((cfcHom ha) f)
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := ⋯
y : MvPolynomial Bool R := ⋯
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := ⋯
⊢ ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν =
    (MvPolynomial.aeval e) ((pderiv true) ((pderiv true) ((x + y) ^ n))) * X ^ 2

Tactic:
have w : ∀ k : ℕ, (k * (k - 1)) • bernsteinPolynomial R n k =
        (n.choose k : R[X]) * ((1 - Polynomial.X) ^ (n - k) *
          ((k : R[X]) * ((↑(k - 1) : R[X]) * Polynomial.X ^ (k - 1 - 1)))) * Polynomial.X ^ 2 := by
      rintro (_ | _ | k)
      · simp
      · simp
      · rw [bernsteinPolynomial]
        simp only [← natCast_mul, Nat.add_succ_sub_one, add_zero, pow_succ]
        push_cast
        ring
    rw [add_pow, map_sum (pderiv true), map_sum (pderiv true), map_sum (MvPolynomial.aeval e),
      Finset.sum_mul]
    -- Step inside the sum:
    refine Finset.sum_congr rfl fun k _ => (w k).trans ?_
    simp only [x, y, e, pderiv_true_x, pderiv_true_y, smul_eq_mul, nsmul_eq_mul,
      Bool.cond_true, Bool.cond_false, add_zero, zero_add, mul_zero, mul_one,
      MvPolynomial.aeval_X,
      Derivation.leibniz_pow, Derivation.leibniz, Derivation.map_natCast, map_natCast, map_pow,
      map_mul]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
⊢ 2⁻¹ • (↑f + ↑g - |↑g - ↑f|) ∈ A.topologicalClosure

Tactic:
refine
    A.topologicalClosure.smul_mem
      (A.topologicalClosure.sub_mem
        (A.topologicalClosure.add_mem (A.le_topologicalClosure f.property)
          (A.le_topologicalClosure g.property))
        ?_)
      _

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
⊢ |↑g - ↑f| ∈ A.topologicalClosure
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: case neg
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
r✝ : ℝ
f : C(X, ℝ)₀
r : ℝ≥0
hr : 0 < ↑r
⊢ r • φ (-f).toNNReal + -(r • φ f.toNNReal) = -(r • φ f.toNNReal) + r • φ (-f).toNNReal

Tactic:
add_comm

Goal state after:
case neg
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
r✝ : ℝ
f : C(X, ℝ)₀
r : ℝ≥0
hr : 0 < ↑r
⊢ -(r • φ f.toNNReal) + r • φ (-f).toNNReal = -(r • φ f.toNNReal) + r • φ (-f).toNNReal
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
f g : C(X, ℝ)₀
this :
  φ (f + g).toNNReal + φ (-f).toNNReal + φ (-g).toNNReal - (φ (-(f + g)).toNNReal + φ f.toNNReal + φ g.toNNReal) = 0
⊢ φ (f + g).toNNReal - φ (-(f + g)).toNNReal - (φ f.toNNReal - φ (-f).toNNReal + (φ g.toNNReal - φ (-g).toNNReal)) = 0

Tactic:
← this

Goal state after:
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
f g : C(X, ℝ)₀
this :
  φ (f + g).toNNReal + φ (-f).toNNReal + φ (-g).toNNReal - (φ (-(f + g)).toNNReal + φ f.toNNReal + φ g.toNNReal) = 0
⊢ φ (f + g).toNNReal - φ (-(f + g)).toNNReal - (φ f.toNNReal - φ (-f).toNNReal + (φ g.toNNReal - φ (-g).toNNReal)) =
    φ (f + g).toNNReal + φ (-f).toNNReal + φ (-g).toNNReal - (φ (-(f + g)).toNNReal + φ f.toNNReal + φ g.toNNReal)
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
f g : C(X, ℝ)₀
this :
  φ (f * g).toNNReal + φ (-f).toNNReal * φ g.toNNReal + φ f.toNNReal * φ (-g).toNNReal -
      (φ (-(f * g)).toNNReal + φ f.toNNReal * φ g.toNNReal + φ (-f).toNNReal * φ (-g).toNNReal) =
    0
⊢ φ (f * g).toNNReal - φ (-(f * g)).toNNReal -
      (φ f.toNNReal * φ g.toNNReal - φ (-f).toNNReal * φ g.toNNReal -
        (φ f.toNNReal * φ (-g).toNNReal - φ (-f).toNNReal * φ (-g).toNNReal)) =
    0

Tactic:
← this

Goal state after:
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Zero X
A : Type u_2
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module ℝ A
inst✝¹ : TopologicalSpace A
inst✝ : IsSemitopologicalRing A
φ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
f g : C(X, ℝ)₀
this :
  φ (f * g).toNNReal + φ (-f).toNNReal * φ g.toNNReal + φ f.toNNReal * φ (-g).toNNReal -
      (φ (-(f * g)).toNNReal + φ f.toNNReal * φ g.toNNReal + φ (-f).toNNReal * φ (-g).toNNReal) =
    0
⊢ φ (f * g).toNNReal - φ (-(f * g)).toNNReal -
      (φ f.toNNReal * φ g.toNNReal - φ (-f).toNNReal * φ g.toNNReal -
        (φ f.toNNReal * φ (-g).toNNReal - φ (-f).toNNReal * φ (-g).toNNReal)) =
    φ (f * g).toNNReal + φ (-f).toNNReal * φ g.toNNReal + φ f.toNNReal * φ (-g).toNNReal -
      (φ (-(f * g)).toNNReal + φ f.toNNReal * φ g.toNNReal + φ (-f).toNNReal * φ (-g).toNNReal)
Module: Mathlib.Analysis.CStarAlgebra.Unitization

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : DenselyNormedField 𝕜
inst✝⁸ : NonUnitalNormedRing E
inst✝⁷ : StarRing E
inst✝⁶ : CStarRing E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : IsScalarTower 𝕜 E E
inst✝³ : SMulCommClass 𝕜 E E
inst✝² : StarRing 𝕜
inst✝¹ : StarModule 𝕜 E
inst✝ : CStarRing 𝕜
x✝ x : Unitization 𝕜 E
h : ¬(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2 = 0
this : ‖((splitMul 𝕜 E) x).2‖ * ‖((splitMul 𝕜 E) x).2‖ ≤ ‖((splitMul 𝕜 E) x⋆).2‖ * ‖((splitMul 𝕜 E) x).2‖
⊢ ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2‖ ≤
    ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1⋆ + (mul 𝕜 E) x.toProd.2⋆‖

Tactic:
← Ne,

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : DenselyNormedField 𝕜
inst✝⁸ : NonUnitalNormedRing E
inst✝⁷ : StarRing E
inst✝⁶ : CStarRing E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : IsScalarTower 𝕜 E E
inst✝³ : SMulCommClass 𝕜 E E
inst✝² : StarRing 𝕜
inst✝¹ : StarModule 𝕜 E
inst✝ : CStarRing 𝕜
x✝ x : Unitization 𝕜 E
h : (algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2 ≠ 0
this : ‖((splitMul 𝕜 E) x).2‖ * ‖((splitMul 𝕜 E) x).2‖ ≤ ‖((splitMul 𝕜 E) x⋆).2‖ * ‖((splitMul 𝕜 E) x).2‖
⊢ ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1 + (mul 𝕜 E) x.toProd.2‖ ≤
    ‖(algebraMap 𝕜 (E →L[𝕜] E)) x.toProd.1⋆ + (mul 𝕜 E) x.toProd.2⋆‖