mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
s t : Set α
f : α → E
h : s =ᵐ[μ] t
⊢ ⨍ (x : α) in s, f x ∂μ = ⨍ (x : α) in t, f x ∂μ

Tactic:
by
  simp only [setAverage_eq, setIntegral_congr_set h, measureReal_congr h]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ (r • μ).withDensity (ν.rnDeriv (r • μ)) = (r • μ).withDensity (r⁻¹ • ν.rnDeriv μ)

pp: case hf
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ AEMeasurable (ν.rnDeriv (r • μ)) (r • μ)

pp: case hg
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ AEMeasurable (r⁻¹ • ν.rnDeriv μ) (r • μ)

pp: case hfi
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ∫⁻ (x : α), ν.rnDeriv (r • μ) x ∂r • μ ≠ ∞

Tactic:
rotate_left

Goal state after:
case hf
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ AEMeasurable (ν.rnDeriv (r • μ)) (r • μ)

case hg
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ AEMeasurable (r⁻¹ • ν.rnDeriv μ) (r • μ)

case hfi
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ ∫⁻ (x : α), ν.rnDeriv (r • μ) x ∂r • μ ≠ ∞

α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ (r • μ).withDensity (ν.rnDeriv (r • μ)) = (r • μ).withDensity (r⁻¹ • ν.rnDeriv μ)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
this :
  ν.singularPart (r • μ) + (r • μ).withDensity (ν.rnDeriv (r • μ)) =
    ν.singularPart (r • μ) + r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)
⊢ (↑r • μ).withDensity (ν.rnDeriv (↑r • μ)) = ↑r⁻¹ • (↑r • μ).withDensity (ν.rnDeriv μ)

Tactic:
add_right_inj

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
this : (r • μ).withDensity (ν.rnDeriv (r • μ)) = r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)
⊢ (↑r • μ).withDensity (ν.rnDeriv (↑r • μ)) = ↑r⁻¹ • (↑r • μ).withDensity (ν.rnDeriv μ)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝⁴ : IsFiniteMeasure ν₁
inst✝³ : IsFiniteMeasure ν₂
inst✝² : ν₁.HaveLebesgueDecomposition μ
inst✝¹ : ν₂.HaveLebesgueDecomposition μ
inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ
this :
  (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
⊢ μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)

Tactic:
add_right_inj

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝⁴ : IsFiniteMeasure ν₁
inst✝³ : IsFiniteMeasure ν₂
inst✝² : ν₁.HaveLebesgueDecomposition μ
inst✝¹ : ν₂.HaveLebesgueDecomposition μ
inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ
this : μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
⊢ μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
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}
⊢ ↑q * μ s ≤ ρ 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 : (q • μ) (s ∩ t) ≤ ρ (s ∩ t) by calc
    (q • μ) s = (q • μ) (s ∩ t ∪ s ∩ tᶜ) := by rw [inter_union_compl]
    _ ≤ (q • μ) (s ∩ t) + (q • μ) (s ∩ tᶜ) := measure_union_le _ _
    _ ≤ ρ (s ∩ t) + (q • μ) tᶜ := by gcongr; apply inter_subset_right
    _ = ρ (s ∩ t) := by simp [A]
    _ ≤ ρ s := by gcongr; apply inter_subset_left
  refine v.measure_le_of_frequently_le _ (.smul_left .rfl _) _ ?_
  intro x hx
  have I : ∀ᶠ a in v.filterAt x, (q : ℝ≥0∞) < ρ a / μ a := (tendsto_order.1 hx.2).1 _ (h hx.1)
  apply I.frequently.mono fun a ha => ?_
  rw [coe_nnreal_smul_apply]
  exact ENNReal.mul_le_of_le_div ha.le

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
s : Set α
E : Type u_3
inst✝² : PseudoMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
l : E
a b : α
ha : a ∈ s
hb : b ∈ s
hf : LocallyBoundedVariationOn f s
h'f : Tendsto f (𝓝[s ∩ Iio b] b) (𝓝 l)
⊢ Tendsto (variationOnFromTo f s a) (𝓝[s ∩ Iio b] b) (𝓝 (variationOnFromTo f s a b - dist (f b) l))

Tactic:
by
  suffices H : Tendsto (fun x ↦ variationOnFromTo f s a b - variationOnFromTo f s x b)
      (𝓝[s ∩ Iio b] b) (𝓝 (variationOnFromTo f s a b - dist (f b) l)) by
    apply Tendsto.congr' _ H
    filter_upwards [self_mem_nhdsWithin] with x hx
    rw [variationOnFromTo.sub_left hf ha hb hx.1]
  apply Tendsto.const_sub
  suffices H : Tendsto (fun x ↦ (eVariationOn f (s ∩ Icc x b)).toReal) (𝓝[s ∩ Iio b] b)
      (𝓝 (dist (f b) l)) by
    apply Tendsto.congr' _ H
    filter_upwards [self_mem_nhdsWithin] with x hx using by simp [variationOnFromTo, hx.2.le]
  rw [dist_edist]
  exact (ENNReal.tendsto_toReal (by simp)).comp (hf.tendsto_eVariationOn_Icc_left h'f hb)

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 α
hf : (f '' s).Subsingleton
x : α
xs : x ∈ s
y : α
ys : y ∈ s
⊢ edist (f x) (f y) = 0

Tactic:
rw [hf ⟨x, xs, rfl⟩ ⟨y, ys, rfl⟩, edist_self]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
this :
  ν.singularPart (r • μ) + (r • μ).withDensity (ν.rnDeriv (r • μ)) =
    ν.singularPart (r • μ) + r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)
⊢ (↑r • μ).withDensity (ν.rnDeriv (↑r • μ)) = ↑r⁻¹ • (↑r • μ).withDensity (ν.rnDeriv μ)

Tactic:
add_right_inj

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
this : (r • μ).withDensity (ν.rnDeriv (r • μ)) = r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)
⊢ (↑r • μ).withDensity (ν.rnDeriv (↑r • μ)) = ↑r⁻¹ • (↑r • μ).withDensity (ν.rnDeriv μ)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝² : SigmaFinite ν₁
inst✝¹ : SigmaFinite ν₂
inst✝ : SigmaFinite μ
this :
  (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
⊢ μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)

Tactic:
add_right_inj

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝² : SigmaFinite ν₁
inst✝¹ : SigmaFinite ν₂
inst✝ : SigmaFinite μ
this : μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
⊢ μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

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

Tactic:
let : TopologicalSpace α := Preorder.topology α
  have : OrderTopology α := ⟨rfl⟩
  rcases eq_or_neBot (𝓝[>] b) with hb | hb
  · simp [rightLim_eq_of_eq_bot _ hb]
  apply rightLim_eq_of_tendsto
  have := variationOnFromTo.tendsto_right (f := f) (l := f.rightLim b) (mem_univ a) (mem_univ b)
    hf.locallyBoundedVariationOn
  simp only [univ_inter] at this
  exact this (hf.tendsto_rightLim _)

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

Goal state before:
pp: case inr.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)
hw : Monotone w
Npos : N = 0
⊢ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ ∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j))

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)
hw : Monotone w
Npos : 0 < N
⊢ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ ∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j))

Tactic:
· calc
      (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i))) =
          ∑ i ∈ Finset.range n, edist (f (w (1 + i + 1))) (f (w (1 + i))) := by grind
      _ = ∑ i ∈ Finset.Ico 1 (n + 1), edist (f (w (i + 1))) (f (w i)) := by
        rw [Finset.range_eq_Ico]
        exact Finset.sum_Ico_add (fun i => edist (f (w (i + 1))) (f (w i))) 0 n 1
      _ ≤ ∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j)) := by
        rw [Finset.range_eq_Ico]
        gcongr
        exact zero_le_one

Goal state after:
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)
hw : Monotone w
Npos : 0 < N
⊢ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ ∑ j ∈ Finset.range (n + 1), edist (f (w (j + 1))) (f (w j))
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 μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
⊢ ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ = ∫⁻ (y : α), f y ∂μ

Tactic:
apply lintegral_congr_ae

Goal state after:
α : 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 ∂μ ≠ ∞
⊢ AEMeasurable.mk f hf =ᵐ[μ] f
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 α
⊢ ∫⁻ (y : α) in a, f y ∂μ = ∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ

Tactic:
apply lintegral_congr_ae

Goal state after:
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
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 : LocallyBoundedVariationOn f s
x y : αᵒᵈ
hx : x ∈ ⇑ofDual ⁻¹' s
hy : y ∈ ⇑ofDual ⁻¹' s
⊢ BoundedVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ Icc (toDual (ofDual x)) (toDual (ofDual y)))

Tactic:
Icc_toDual,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
x y : αᵒᵈ
hx : x ∈ ⇑ofDual ⁻¹' s
hy : y ∈ ⇑ofDual ⁻¹' s
⊢ BoundedVariationOn (f ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ ⇑ofDual ⁻¹' Icc (ofDual y) (ofDual x))
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: case e_a
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
I : Integrable (AEStronglyMeasurable.mk f ⋯) μ
x : α
hx :
  Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ ∂μ) / μ a)
    (v.filterAt x) (𝓝 0)
h'x : f x = AEStronglyMeasurable.mk f ⋯ x
a : Set α
⊢ ∫⁻ (y : α) in a, ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ ∂μ =
    ∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ

Tactic:
apply lintegral_congr_ae

Goal state after:
case e_a
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : Integrable f μ
I : Integrable (AEStronglyMeasurable.mk f ⋯) μ
x : α
hx :
  Tendsto (fun a ↦ (∫⁻ (y : α) in a, ‖AEStronglyMeasurable.mk f ⋯ y - AEStronglyMeasurable.mk f ⋯ x‖ₑ ∂μ) / μ a)
    (v.filterAt x) (𝓝 0)
h'x : f x = AEStronglyMeasurable.mk f ⋯ x
a : Set α
⊢ (fun a ↦ ‖AEStronglyMeasurable.mk f ⋯ a - AEStronglyMeasurable.mk f ⋯ x‖ₑ) =ᵐ[μ.restrict a] fun a ↦ ‖f a - f x‖ₑ
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
a : A
g : R → R
ha : p a
f : C(↑(spectrum R a), R)
⊢ (cfcHom ha) f = cfc (Function.extend Subtype.val (⇑f) g) a

Tactic:
by
  have h : f = (spectrum R a).domRestrict (Function.extend Subtype.val f g) := by
    ext; simp
  have hg : ContinuousOn (Function.extend Subtype.val f g) (spectrum R a) :=
    continuousOn_iff_continuous_domRestrict.mpr <| h ▸ map_continuous f
  rw [cfc_apply ..]
  congr!

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 α
f : α → E
a b : α
h : (𝓝[>] a).NeBot
h' : ContinuousWithinAt f (Ici a) a
hab : a < b
⊢ eVariationOn f (Ioc a b) = eVariationOn f (Icc a b)

Tactic:
have : (𝓝[Iic b ∩ Ioi a] a).NeBot := by
    convert h using 1
    exact nhdsWithin_inter_of_mem (mem_nhdsWithin_of_mem_nhds (Iic_mem_nhds hab))

Goal state after:
case inr
α : 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 (Ici a) a
hab : a < b
this : (𝓝[Iic b ∩ Ioi a] a).NeBot
⊢ eVariationOn f (Ioc a b) = eVariationOn f (Icc a b)
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 : α
A : Tendsto (fun y ↦ eVariationOn f (s ∩ Ico y x)) (𝓝[s ∩ Iio x] x) (𝓝 0)
a : α
ha : a ∈ s ∩ Ici x
⊢ 0 = eVariationOn f (s ∩ Ico a x)

Tactic:
by simp [show Ico a x = ∅ by grind]

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
inst✝ : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
⊢ cfc (g ∘ f) a = cfc g (cfc f a)

Tactic:
by
  have := hg.comp hf <| (spectrum R a).mapsTo_image f
  have sp_eq : spectrum R (cfcHom (show p a from ha) (ContinuousMap.mk _ hf.domRestrict)) =
      f '' (spectrum R a) := by
    rw [cfcHom_map_spectrum (by exact ha) _]
    ext
    simp
  rw [cfc_apply .., cfc_apply f a,
    cfc_apply _ _ (cfcHom_predicate (show p a from ha) _) (by convert! hg), ← cfcHom_comp _ _]
  swap
  · exact ContinuousMap.mk _ <| hf.domRestrict.codRestrict fun x ↦ by rw [sp_eq]; use x.1; simp
  · congr
  · exact fun _ ↦ rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹⁹ : Semifield R
inst✝¹⁸ : StarRing R
inst✝¹⁷ : MetricSpace R
inst✝¹⁶ : IsTopologicalSemiring R
inst✝¹⁵ : ContinuousStar R
inst✝¹⁴ : Field S
inst✝¹³ : StarRing S
inst✝¹² : MetricSpace S
inst✝¹¹ : IsTopologicalRing S
inst✝¹⁰ : ContinuousStar S
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : Module S A
inst✝⁶ : IsScalarTower S A A
inst✝⁵ : SMulCommClass S A A
inst✝⁴ : Algebra R S
inst✝³ : Module R A
inst✝² : IsScalarTower R S A
inst✝¹ : StarModule R S
inst✝ : ContinuousSMul R S
a : A
φ : C(↑(σₙ S a), S)₀ →⋆ₙₐ[S] A
f : C(S, R)
h : QuasispectrumRestricts a ⇑f
h_id : φ (ContinuousMapZero.id (σₙ S a)) = a
⊢ (nonUnitalStarAlgHom φ h) (ContinuousMapZero.id (σₙ R a)) = a

Tactic:
simp only [QuasispectrumRestricts.nonUnitalStarAlgHom_apply]

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹⁹ : Semifield R
inst✝¹⁸ : StarRing R
inst✝¹⁷ : MetricSpace R
inst✝¹⁶ : IsTopologicalSemiring R
inst✝¹⁵ : ContinuousStar R
inst✝¹⁴ : Field S
inst✝¹³ : StarRing S
inst✝¹² : MetricSpace S
inst✝¹¹ : IsTopologicalRing S
inst✝¹⁰ : ContinuousStar S
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : Module S A
inst✝⁶ : IsScalarTower S A A
inst✝⁵ : SMulCommClass S A A
inst✝⁴ : Algebra R S
inst✝³ : Module R A
inst✝² : IsScalarTower R S A
inst✝¹ : StarModule R S
inst✝ : ContinuousSMul R S
a : A
φ : C(↑(σₙ S a), S)₀ →⋆ₙₐ[S] A
f : C(S, R)
h : QuasispectrumRestricts a ⇑f
h_id : φ (ContinuousMapZero.id (σₙ S a)) = a
⊢ φ
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
        ((ContinuousMapZero.id (σₙ R a)).comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ })) =
    a
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 (toDual y) (toDual x))

Tactic:
Icc_toDual,

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 ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ ⇑ofDual ⁻¹' 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 (toDual y) (toDual x))

Tactic:
Icc_toDual,

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 ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ ⇑ofDual ⁻¹' 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 (toDual y) (toDual x))

Tactic:
Icc_toDual,

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 ∘ ⇑ofDual) (⇑ofDual ⁻¹' s ∩ ⇑ofDual ⁻¹' Icc x y)
Module: Mathlib.Topology.ContinuousMap.Polynomial

Goal state before:
pp: case e'_3
a b : ℝ
h : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h).symm x)
q : ℝ[X] := p.comp ((b - a)⁻¹ • X + Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
⊢ ↑x = (b - a) * ((b - a)⁻¹ * ↑x + -(a * (b - a)⁻¹)) + a

Tactic:
replace h : b - a ≠ 0 := sub_ne_zero_of_ne h.ne.symm

Goal state after:
case e'_3
a b : ℝ
h✝ : a < b
f : C(↑(Set.Icc a b), ℝ)
p : ℝ[X]
w : ∀ (x : ↑I), Polynomial.eval (↑x) p = f ((iccHomeoI a b h✝).symm x)
q : ℝ[X] := p.comp ((b - a)⁻¹ • X + Polynomial.C (-a * (b - a)⁻¹))
x : ↑(Set.Icc a b)
h : b - a ≠ 0
⊢ ↑x = (b - a) * ((b - a)⁻¹ * ↑x + -(a * (b - a)⁻¹)) + a
Module: Mathlib.Topology.ContinuousMap.Weierstrass

Goal state before:
pp: case h
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := ⋯
p : ℝ[X]
b : ‖p.toContinuousMapOn (Set.Icc a b✝) - f'‖ < ε
⊢ ∀ x ∈ Set.Icc a b✝, |Polynomial.eval x p - f x| < ε

Tactic:
rw [norm_lt_iff _ pos] at b

Goal state after:
case h
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := { toFun := fun x ↦ f ↑x, continuous_toFun := ⋯ }
p : ℝ[X]
b : ∀ (x : ↑(Set.Icc a b✝)), ‖(p.toContinuousMapOn (Set.Icc a b✝) - f') x‖ < ε
⊢ ∀ x ∈ Set.Icc a b✝, |Polynomial.eval x p - f x| < ε
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
⊢ (r • -f).toNNReal = r • (-f).toNNReal

Tactic:
toNNReal_smul

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
⊢ r • (-f).toNNReal = r • (-f).toNNReal