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 ν
h : ¬μ ⟂ₘ ν
⊢ ∃ ε, 0 < ε ∧ ∃ E, MeasurableSet E ∧ 0 < ν E ∧ ∀ (A : Set α), MeasurableSet A → ↑ε * ν (A ∩ E) ≤ μ (A ∩ E)

Tactic:
by
  -- for all `n : ℕ`, obtain the Hahn decomposition for `μ - (1 / n) ν`
  have h_decomp (n : ℕ) : ∃ s : Set α, MeasurableSet s
        ∧ (∀ t, MeasurableSet t → ((1 / (n + 1) : ℝ≥0) • ν) (t ∩ s) ≤ μ (t ∩ s))
        ∧ (∀ t, MeasurableSet t → μ (t ∩ sᶜ) ≤ ((1 / (n + 1) : ℝ≥0) • ν) (t ∩ sᶜ)) := by
    obtain ⟨s, hs, hs_le, hs_ge⟩ := hahn_decomposition μ ((1 / (n + 1) : ℝ≥0) • ν)
    refine ⟨s, hs, fun t ht ↦ ?_, fun t ht ↦ ?_⟩
    · exact hs_le (t ∩ s) (ht.inter hs) inter_subset_right
    · exact hs_ge (t ∩ sᶜ) (ht.inter hs.compl) inter_subset_right
  choose f hf₁ hf₂ hf₃ using h_decomp
  -- set `A` to be the intersection of all the negative parts of obtained Hahn decompositions
  -- and we show that `μ A = 0`
  let A := ⋂ n, (f n)ᶜ
  have hAmeas : MeasurableSet A := MeasurableSet.iInter fun n ↦ (hf₁ n).compl
  have hA₂ (n : ℕ) (t : Set α) (ht : MeasurableSet t) :
      μ (t ∩ A) ≤ ((1 / (n + 1) : ℝ≥0) • ν) (t ∩ A) := by
    specialize hf₃ n (t ∩ A) (ht.inter hAmeas)
    have : A ∩ (f n)ᶜ = A := inter_eq_left.mpr (iInter_subset _ n)
    rwa [inter_assoc, this] at hf₃
  have hA₃ (n : ℕ) : μ A ≤ (1 / (n + 1) : ℝ≥0) * ν A := by simpa using hA₂ n univ .univ
  have hμ : μ A = 0 := by
    lift μ A to ℝ≥0 using measure_ne_top _ _ with μA
    lift ν A to ℝ≥0 using measure_ne_top _ _ with νA
    rw [ENNReal.coe_eq_zero]
    by_cases! hb : 0 < νA
    · suffices ∀ b, 0 < b → μA ≤ b by
        by_contra h
        have h' := this (μA / 2) (half_pos (zero_lt_iff.2 h))
        rw [← @Classical.not_not (μA ≤ μA / 2)] at h'
        exact h' (not_le.2 (NNReal.half_lt_self h))
      intro c hc
      have : ∃ n : ℕ, 1 / (n + 1 : ℝ) < c * (νA : ℝ)⁻¹ := by
        refine exists_nat_one_div_lt ?_
        positivity
      rcases this with ⟨n, hn⟩
      have hb₁ : (0 : ℝ) < (νA : ℝ)⁻¹ := by rw [_root_.inv_pos]; exact hb
      have h' : 1 / (↑n + 1) * νA < c := by
        rw [← NNReal.coe_lt_coe, ← mul_lt_mul_iff_left₀ hb₁, NNReal.coe_mul, mul_assoc, ←
          NNReal.coe_inv, ← NNReal.coe_mul, mul_inv_cancel₀, ← NNReal.coe_mul, mul_one,
          NNReal.coe_inv]
        · exact hn
        · exact hb.ne'
      refine le_trans ?_ h'.le
      rw [← ENNReal.coe_le_coe, ENNReal.coe_mul]
      exact hA₃ n
    · rw [le_zero_iff] at hb
      simpa [hb] using hA₃ 0
  -- since `μ` and `ν` are not mutually singular, `μ A = 0` implies `ν Aᶜ > 0`
  rw [MutuallySingular] at h; push Not at h
  have := h _ hAmeas hμ
  simp_rw [A, compl_iInter, compl_compl] at this
  -- as `Aᶜ = ⋃ n, f n`, `ν Aᶜ > 0` implies there exists some `n` such that `ν (f n) > 0`
  obtain ⟨n, hn⟩ := exists_measure_pos_of_not_measure_iUnion_null this
  -- thus, choosing `f n` as the set `E` suffices
  exact ⟨1 / (n + 1), by simp, f n, hf₁ n, hn, hf₂ n⟩

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

Goal state before:
pp: case refine_1
α : 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
⊢ ∀ {a b : α}, a ∈ s → b ∈ s → variationOnFromTo f s a b + variationOnFromTo f s b a = 0

pp: case refine_2
α : 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
⊢ ∀ {a b c : α},
    a ≤ b →
      b ≤ c → a ∈ s → b ∈ s → c ∈ s → variationOnFromTo f s a c = variationOnFromTo f s a b + variationOnFromTo f s b c

Tactic:
· rintro x y _xs _ys
    simp only [variationOnFromTo.eq_neg_swap f s y x, add_neg_cancel]

Goal state after:
case refine_2
α : 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
⊢ ∀ {a b c : α},
    a ≤ b →
      b ≤ c → a ∈ s → b ∈ s → c ∈ s → variationOnFromTo f s a c = variationOnFromTo f s a b + variationOnFromTo f s b c
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}
⊢ ρ s ≤ ↑p * μ s

Tactic:
let t := {x : α | Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
  have A : μ tᶜ = 0 := v.ae_tendsto_limRatioMeas hρ
  suffices H : ρ (s ∩ t) ≤ (p • μ) (s ∩ t) by calc
    ρ s = ρ (s ∩ t ∪ s ∩ tᶜ) := by rw [inter_union_compl]
    _ ≤ ρ (s ∩ t) + ρ (s ∩ tᶜ) := measure_union_le _ _
    _ ≤ (p • μ) (s ∩ t) + ρ tᶜ := by gcongr; apply inter_subset_right
    _ ≤ p * μ (s ∩ t) := by simp [(hρ A)]
    _ ≤ p * μ s := by gcongr; apply inter_subset_left
  refine v.measure_le_of_frequently_le (p • μ) hρ _ fun x hx => ?_
  have I : ∀ᶠ b : Set α in v.filterAt x, ρ b / μ b < p := (tendsto_order.1 hx.2).2 _ (h hx.1)
  apply I.frequently.mono fun a ha => ?_
  rw [coe_nnreal_smul_apply]
  refine (ENNReal.div_le_iff_le_mul ?_ (Or.inr (bot_le.trans_lt ha).ne')).1 ha.le
  simp only [ENNReal.coe_ne_top, Ne, or_true, not_false_iff]

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
s : Set α
n : ℕ
u : ℕ → α
hu : Monotone u
hus : ∀ (i : ℕ), u i ∈ s
⊢ ∀ i ≤ n, u i ∈ s ∩ Icc (u 0) (u n)

Tactic:
grind [Monotone]

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
s : Set α
n : ℕ
u : ℕ → α
hu : Monotone u
hus : ∀ (i : ℕ), u i ∈ s
⊢ (u 0, u n) ∈ {p | p.1 ∈ s ∧ p.2 ∈ s ∧ p.1 ≤ p.2}

Tactic:
grind [Monotone]

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
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : u n ≤ x
v : ℕ → α := fun i ↦ if i ≤ n then u i else x
⊢ Monotone v

Tactic:
grind [Monotone]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ
⊢ μ + (ν - ξ) = μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ

Tactic:
rw [restrict_add_restrict_compl hs, add_assoc, restrict_add_restrict_compl hs]

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

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

Tactic:
grind [Monotone]

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

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

Tactic:
grind [Monotone]

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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ (μ.withDensity (v.limRatioMeas hρ)) s ≤ ↑t ^ 2 * ρ s

Tactic:
have t_ne_zero' : t ≠ 0 := (zero_lt_one.trans ht).ne'

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
⊢ (μ.withDensity (v.limRatioMeas hρ)) s ≤ ↑t ^ 2 * ρ s
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, ‖B‖ₑ * ‖f (u (i + 1)) - f (u i)‖ₑ * D +
      ∑ i ∈ Finset.range n, ‖B‖ₑ * C * ‖g (u (i + 1)) - g (u i)‖ₑ =
    ‖B‖ₑ * D * ∑ i ∈ Finset.range n, ‖f (u (i + 1)) - f (u i)‖ₑ +
      ‖B‖ₑ * C * ∑ i ∈ Finset.range n, ‖g (u (i + 1)) - g (u i)‖ₑ

Tactic:
simp only [← sum_mul, ← mul_sum]
    ring

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

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

Tactic:
congr 1
          · grind [Finset.sum_congr]
          · have A : N - 1 + 1 = N := Nat.succ_pred_eq_of_pos Npos
            have : Finset.Ico (N - 1) N = {N - 1} := by rw [← Nat.Ico_succ_singleton, A]
            simp only [this, A, Finset.sum_singleton]

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)₀
⊢ (∀ (x : α), f x ≤ g x) → ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), g = f + p

Tactic:
← ContinuousMap.coe_coe,

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)₀
⊢ (∀ (x : α), ↑f x ≤ g x) → ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), g = f + p
Module: Mathlib.Topology.ContinuousMap.StarOrdered

Goal state before:
pp: case mp.add_left
α : 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✝ p : C(α, R)
p_mem : p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
hp' : ∀ (f g : C(α, R)₀), ↑g = ↑f + p → ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), g = f + p
f g : C(α, R)₀
s : C(α, R)
hp : ↑g = ↑f + ((fun s ↦ star s * s) s + p)
⊢ ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), g = f + p

Tactic:
simp only at *

Goal state after:
case mp.add_left
α : 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✝ p : C(α, R)
p_mem : p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
hp' : ∀ (f g : C(α, R)₀), ↑g = ↑f + p → ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), g = f + p
f g : C(α, R)₀
s : C(α, R)
hp : ↑g = ↑f + (star s * s + p)
⊢ ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), g = f + p
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
⊢ ρ s ≤ ↑t * (μ.withDensity (v.limRatioMeas hρ)) s

Tactic:
have t_ne_zero' : t ≠ 0 := (zero_lt_one.trans ht).ne'

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
⊢ ρ s ≤ ↑t * (μ.withDensity (v.limRatioMeas hρ)) 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 t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this✝ : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
m : ℕ
v : ℕ → α
hv : Monotone v
vt : ∀ (i : ℕ), v i ∈ t
w : ℕ → α := fun i ↦ if i ≤ n then u i else v (i - (n + 1))
⊢ Monotone w

Tactic:
grind [Monotone]

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

Goal state before:
pp: case hE
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
L : Filter α
hL : ∀ y ∈ s, s ∩ Ici y ∈ L
x₀ : α
hx₀ : x₀ ∈ s
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : δ < ε
H : ∃ᶠ (x : α) in L, ε ≤ eVariationOn f (s ∩ Ici x)
y : α → α
y_mem : ∀ y_1 ∈ s, y y_1 ∈ s ∩ Ici y_1
le_y : ∀ y_1 ∈ s, δ ≤ eVariationOn f (s ∩ Icc y_1 (y y_1))
v : ℕ → α := ⋯
I : ∀ (n : ℕ), v n ∈ s
n : ℕ
⊢ Monotone v

Tactic:
apply monotone_nat_of_le_succ (fun n ↦ ?_)
        simp only [Function.iterate_succ', Function.comp_apply, v]
        exact (y_mem _ (I n)).2

Goal state after:
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✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
f : R → R
⊢ cfc f 1 = (algebraMap R A) (f 1)

Tactic:
simpa using cfc_algebraMap (A := A) 1 f

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁴ : CommRing R
inst✝¹³ : PartialOrder R
inst✝¹² : StarRing R
inst✝¹¹ : MetricSpace R
inst✝¹⁰ : IsTopologicalRing 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 g : C(↑(spectrum R a), R)
⊢ (cfcHom ha) f ≤ (cfcHom ha) g ↔ f ≤ g

Tactic:
by
  rw [← sub_nonneg, ← map_sub, cfcHom_nonneg_iff, sub_nonneg]

Goal state after:
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 : R → R
a : A
h0 : ¬f 0 = 0
⊢ cfcₙ (fun x ↦ star (f x)) a = star (cfcₙ f a)

Tactic:
rw [cfcₙ_apply_of_not_map_zero a h0, cfcₙ_apply_of_not_map_zero, star_zero]

Goal state after:
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 : R → R
a : A
h0 : ¬f 0 = 0
⊢ ¬star (f 0) = 0
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n ν k : ℕ
⊢ k < ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n ν)) = 0

Tactic:
rcases ν with - | ν

Goal state after:
case zero
R : Type u_1
inst✝ : CommRing R
n k : ℕ
⊢ k < 0 → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n 0)) = 0

case succ
R : Type u_1
inst✝ : CommRing R
n k ν : ℕ
⊢ k < ν + 1 → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
n k ν : ℕ
⊢ k ≤ ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0

Tactic:
induction k generalizing n ν with
    | zero => simp [eval_at_0]
    | succ k ih =>
      simp only [derivative_succ, Function.comp_apply,
        Function.iterate_succ, Polynomial.iterate_derivative_sub,
        Polynomial.iterate_derivative_natCast_mul, Polynomial.eval_mul, Polynomial.eval_natCast,
        Polynomial.eval_sub]
      intro h
      apply mul_eq_zero_of_right
      rw [ih _ _ (Nat.le_of_succ_le h), sub_zero]
      convert! ih _ _ (Nat.pred_le_pred h)
      exact (Nat.succ_pred_eq_of_pos (k.succ_pos.trans_le h)).symm

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

Goal state before:
pp: n k : ℕ
h : k ≤ n + 1
⊢ LinearIndependent ℚ fun ν ↦ bernsteinPolynomial ℚ n ↑ν

Tactic:
by
  induction k with
  | zero => apply linearIndependent_empty_type
  | succ k ih =>
    apply linearIndependent_finSucc'.mpr
    fconstructor
    · exact ih (le_of_lt h)
    · -- The actual work!
      -- We show that the (n-k)-th derivative at 1 doesn't vanish,
      -- but vanishes for everything in the span.
      clear ih
      simp only [add_le_add_iff_right] at h
      simp only [Fin.val_last, Fin.init_def]
      dsimp
      apply notMem_span_of_apply_notMem_span_image (@Polynomial.derivative ℚ _ ^ (n - k))
      -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to change `span_image` into `span_image _`
      simp only [not_exists, not_and, Submodule.mem_map, Submodule.span_image _]
      intro p m
      apply_fun Polynomial.eval (1 : ℚ)
      simp only [Module.End.pow_apply]
      -- The right-hand side is nonzero,
      -- so it will suffice to show the left-hand side is always zero.
      suffices (Polynomial.derivative^[n - k] p).eval 1 = 0 by
        rw [this]
        exact (iterate_derivative_at_1_ne_zero ℚ n k h).symm
      refine span_induction ?_ ?_ ?_ ?_ m
      · simp only [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]
        rintro ⟨a, w⟩; simp only
        rw [iterate_derivative_at_1_eq_zero_of_lt ℚ n ((tsub_lt_tsub_iff_left_of_le h).mpr w)]
      · simp
      · intro x y _ _ hx hy; simp [hx, hy]
      · intro a x _ h; simp [h]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := fun i ↦ bif i then X else 1 - X
k : ℕ
⊢ (k + 1) • bernsteinPolynomial R n (k + 1) =
    ↑(k + 1) * X ^ (k + 1 - 1) * (1 - X) ^ (n - (k + 1)) * ↑(n.choose (k + 1)) * X

Tactic:
rw [bernsteinPolynomial]
        simp only [← natCast_mul, Nat.add_succ_sub_one, add_zero, pow_succ]
        push_cast
        ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: n ν : ℕ
x : ↑I
⊢ (bernstein n ν) x = ↑(n.choose ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)

Tactic:
dsimp [bernstein, Polynomial.toContinuousMapOn, Polynomial.toContinuousMap, bernsteinPolynomial]
  simp

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

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
x : MvPolynomial Bool R := MvPolynomial.X true
y : MvPolynomial Bool R := MvPolynomial.X false
pderiv_true_x : (pderiv true) x = 1
pderiv_true_y : (pderiv true) y = 0
e : Bool → R[X] := fun i ↦ bif i then X else 1 - X
k : ℕ
⊢ ((k + 1 + 1) * (k + 1 + 1 - 1)) • bernsteinPolynomial R n (k + 1 + 1) =
    ↑(n.choose (k + 1 + 1)) *
        ((1 - X) ^ (n - (k + 1 + 1)) * (↑(k + 1 + 1) * (↑(k + 1 + 1 - 1) * X ^ (k + 1 + 1 - 1 - 1)))) *
      X ^ 2

Tactic:
rw [bernsteinPolynomial]
        simp only [← natCast_mul, Nat.add_succ_sub_one, add_zero, pow_succ]
        push_cast
        ring

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 : ↥A
g : ℝ[X]
⊢ (g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (↑f).attachBound = ↑((Polynomial.aeval f) g)

Tactic:
ext
  simp only [Polynomial.aeval_subalgebra_coe, Polynomial.aeval_continuousMap_apply]
  simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Bernstein

Goal state before:
pp: E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
f : C(↑I, E)
this✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : U ∈ 𝓝 0
hUc : Convex ℝ U
C : ℝ
hC : ∀ (x y : ↑I), gauge U (f x - f y) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ : ∀ (x y : ↑I), dist x y < δ → gauge U (f x - f y) < 1 / 2
nhds_zero : Tendsto (fun n ↦ C / δ ^ 2 / ↑n) atTop (𝓝 0)
n : ℕ
nh : C / δ ^ 2 / ↑n < 1 / 2
hn₀ : n ≠ 0
x : ↑I
S : Finset (Fin (n + 1)) := {k | dist k/ₙ x < δ}
⊢ C * ∑ k, (↑x - ↑k/ₙ) ^ 2 / δ ^ 2 * (bernstein n ↑k) x = (C * ∑ k, (↑x - ↑k/ₙ) ^ 2 * (bernstein n ↑k) x) / δ ^ 2

Tactic:
simp only [← mul_div_right_comm, ← mul_div_assoc, ← Finset.sum_div]

Goal state after: