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

Goal state before:

Tactic:
μ s ≤ μ (s ∩ o ∪ oᶜ) := by
        conv_lhs => rw [← inter_union_compl s o]
        gcongr
        apply inter_subset_right
      _ ≤ μ (s ∩ o) + μ oᶜ := measure_union_le _ _
      _ = μ (s ∩ o) := by rw [μo, add_zero]
      _ = (ε : ℝ≥0∞)⁻¹ * (ε • μ) (s ∩ o) := by
        simp only [coe_nnreal_smul_apply, ← mul_assoc, mul_comm _ (ε : ℝ≥0∞)]
        rw [ENNReal.mul_inv_cancel (ENNReal.coe_pos.2 εpos).ne' ENNReal.coe_ne_top, one_mul]
      _ ≤ (ε : ℝ≥0∞)⁻¹ * ρ (s ∩ o) := by
        gcongr _ * ?_
        refine v.measure_le_of_frequently_le ρ smul_absolutelyContinuous _ ?_
        intro x hx
        rw [hs] at hx
        simp only [mem_inter_iff, not_lt, not_eventually, mem_ofPred_eq] at hx
        exact hx.1
      _ ≤ (ε : ℝ≥0∞)⁻¹ * ρ o := by gcongr; apply inter_subset_right
      _ = 0 := by rw [ρo, mul_zero]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.DensityTheorem

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[>] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ∈ (vitaliFamily μ K).setsAt x

Tactic:
filter_upwards [xmem, δlim self_mem_nhdsWithin] with j hj h'j

Goal state after:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[>] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
j : ι
hj : x ∈ closedBall (w j) (K * δ j)
h'j : j ∈ δ ⁻¹' Ioi 0
⊢ closedBall (w j) (δ j) ∈ (vitaliFamily μ K).setsAt x
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 ξ
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (a : α) in A, ⨆ i, ⨆ i_1, ⨆ (_ : i_1 ≤ i), f i_1 a ∂ν ≤ μ A

Tactic:
lintegral_iSup (fun n ↦ (iSup_mem_measurableLE _ hf₁ n).1) (iSup_monotone _)

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 ξ
A : Set α
hA : MeasurableSet A
⊢ ⨆ n, ∫⁻ (a : α) in A, ⨆ k, ⨆ (_ : k ≤ n), f k a ∂ν ≤ μ A
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = ∞}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : ρ o < ∞
s : Set α := {x | v.limRatioMeas hρ x = ∞} ∩ o
ρs : ρ s ≠ ∞
q : ℝ≥0
hq : 1 ≤ q
y : α
hy : y ∈ s
⊢ y ∈ {x | ↑q < v.limRatioMeas hρ x}

Tactic:
have : v.limRatioMeas hρ y = ∞ := hy.1

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = ∞}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : ρ o < ∞
s : Set α := {x | v.limRatioMeas hρ x = ∞} ∩ o
ρs : ρ s ≠ ∞
q : ℝ≥0
hq : 1 ≤ q
y : α
hy : y ∈ s
this : v.limRatioMeas hρ y = ∞
⊢ y ∈ {x | ↑q < v.limRatioMeas hρ x}
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))) (g (u (i + 1)))‖ₑ +
      ∑ i ∈ Finset.range n, ‖(B (f (u i))) (g (u (i + 1)) - g (u i))‖ₑ ≤
    ∑ i ∈ Finset.range n, ‖B‖ₑ * ‖f (u (i + 1)) - f (u i)‖ₑ * ‖g (u (i + 1))‖ₑ +
      ∑ i ∈ Finset.range n, ‖B‖ₑ * ‖f (u i)‖ₑ * ‖g (u (i + 1)) - g (u i)‖ₑ

Tactic:
gcongr with i hi i hi

Goal state after:
case h
α : 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 : ℕ
hi : i ∈ Finset.range n
⊢ ‖(B (f (u (i + 1)) - f (u i))) (g (u (i + 1)))‖ₑ ≤ ‖B‖ₑ * ‖f (u (i + 1)) - f (u i)‖ₑ * ‖g (u (i + 1))‖ₑ

case h
α : 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 : ℕ
hi : i ∈ Finset.range n
⊢ ‖(B (f (u i))) (g (u (i + 1)) - g (u i))‖ₑ ≤ ‖B‖ₑ * ‖f (u i)‖ₑ * ‖g (u (i + 1)) - g (u i)‖ₑ
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)‖ₑ * ‖g (u (i + 1))‖ₑ +
      ∑ i ∈ Finset.range n, ‖B‖ₑ * ‖f (u i)‖ₑ * ‖g (u (i + 1)) - g (u i)‖ₑ ≤
    ∑ 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)‖ₑ

Tactic:
gcongr with i hi i hi

Goal state after:
case h₂
α : 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 : ℕ
hi : i ∈ Finset.range n
⊢ ‖g (u (i + 1))‖ₑ ≤ D

case h₂
α : 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 : ℕ
hi : i ∈ Finset.range n
⊢ ‖f (u i)‖ₑ ≤ 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ρ : ρ ≪ μ
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)
⊢ ν (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) ≤ (↑t ^ 2 • ρ) (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))

Tactic:
simp only [ν, I, M, withDensity_apply]

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)
⊢ ∫⁻ (a : α) in s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)), v.limRatioMeas hρ a ∂μ ≤
    (↑t ^ 2 • ρ) (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))
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 α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hb : b ∈ s
A : IsGreatest (s ∩ Icc a b) b
B : IsLeast (s ∩ Icc b c) b
⊢ eVariationOn f (s ∩ Icc a b) + eVariationOn f (s ∩ Icc b c) = eVariationOn f (s ∩ Icc a c)

Tactic:
rw [← eVariationOn.union f A B, ← inter_union_distrib_left, Icc_union_Icc_eq_Icc hab hbc]

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
a : A
f : R → R
ha : p a
hf : ContinuousOn f (spectrum R a)
⊢ cfc f a = (cfcL ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ }

Tactic:
by
  rw [cfc_def, dif_pos ⟨ha, hf⟩, cfcL_apply]

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

Goal state before:
pp: case neg.inl
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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (spectrum R a)) (ha : p a),
    P ((cfcHom ha) { toFun := (spectrum R a).domRestrict f, continuous_toFun := ⋯ })
h : ¬p a
⊢ P (cfc f a)

Tactic:
rwa [cfc_apply_of_not_predicate _ h]

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

Goal state before:
pp: case neg
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
f g : R → R
a : A
h : ∀ x ∈ spectrum R a, f x ≤ g x
hf : ContinuousOn f (spectrum R a)
hg : ContinuousOn g (spectrum R a)
ha : ¬p a
⊢ cfc f a ≤ cfc g a

Tactic:
· simp only [cfc_apply_of_not_predicate _ ha, le_rfl]

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

Goal state before:
pp: case neg
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
P : A → Prop
a : A
f : R → R
h₀ : P 0
haf :
  ∀ (hf : ContinuousOn f (σₙ R a)) (h0 : { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯ } 0 = 0) (ha : p a),
    P ((cfcₙHom ha) { toFun := (σₙ R a).domRestrict f, continuous_toFun := ⋯, map_zero' := h0 })
h : ¬(ContinuousOn f (σₙ R a) ∧ f 0 = 0 ∧ p a)
⊢ P (cfcₙ f a)

Tactic:
· simp only [not_and_or] at h
    obtain (h | h | h) := h
    · rwa [cfcₙ_apply_of_not_continuousOn _ h]
    · rwa [cfcₙ_apply_of_not_map_zero _ h]
    · rwa [cfcₙ_apply_of_not_predicate _ h]

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

Goal state before:
pp: 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)
⊢ cfcₙ f a = cfcₙ g a

Tactic:
by
  by_cases h : p a ∧ ContinuousOn g (σₙ R a) ∧ g 0 = 0
  · rw [cfcₙ_apply f a (h.2.1.congr hfg) (hfg (quasispectrum.zero_mem R a) ▸ h.2.2) h.1,
      cfcₙ_apply g a h.2.1 h.2.2 h.1]
    congr 3
    exact Set.domRestrict_eq_iff.mpr hfg
  · simp only [not_and_or] at h
    obtain (ha | hg | h0) := h
    · simp [cfcₙ_apply_of_not_predicate a ha]
    · rw [cfcₙ_apply_of_not_continuousOn a hg, cfcₙ_apply_of_not_continuousOn]
      exact fun hf ↦ hg (hf.congr hfg.symm)
    · rw [cfcₙ_apply_of_not_map_zero a h0, cfcₙ_apply_of_not_map_zero]
      exact fun hf ↦ h0 (hfg (quasispectrum.zero_mem R a) ▸ hf)

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
hE : Nonempty E
f : α → E
s : Set α
hf : BoundedVariationOn f s
⊢ ∃ l, Tendsto f (𝓟 s ⊓ atTop) (𝓝 l)

Tactic:
rcases eq_empty_or_nonempty s with rfl | hs
  · simp
  · exact hf.exists_tendsto_left_of_filter _
      (fun y hy ↦ inter_mem_inf (mem_principal_self s) (Ici_mem_atTop _)) hs

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n ν : ℕ
⊢ Polynomial.map f (bernsteinPolynomial R n ν) = bernsteinPolynomial S n ν

Tactic:
simp [bernsteinPolynomial]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν = 0
⊢ Polynomial.eval 0 (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) = 1

Tactic:
subst h

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ Polynomial.eval 0 (↑(n.choose 0) * X ^ 0 * (1 - X) ^ (n - 0)) = 1
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν = n
⊢ Polynomial.eval 1 (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν)) = 1

Tactic:
subst h

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
ν : ℕ
⊢ Polynomial.eval 1 (↑(ν.choose ν) * X ^ ν * (1 - X) ^ (ν - ν)) = 1
Module: Mathlib.RingTheory.Polynomial.Bernstein

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
ν : ℕ
⊢ Polynomial.derivative (bernsteinPolynomial R 0 (ν + 1)) =
    ↑0 * (bernsteinPolynomial R (0 - 1) ν - bernsteinPolynomial R (0 - 1) (ν + 1))

Tactic:
simp [bernsteinPolynomial]

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

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

Tactic:
simp [eval_at_0]

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

Goal state before:
pp: case pos.zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
h : 0 ≤ n
⊢ eval 0 ((⇑derivative)^[0] (bernsteinPolynomial R n 0)) = eval (↑(n - (0 - 1))) (ascPochhammer R 0)

Tactic:
simp [eval_at_0]

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
⊢ ↑f ⊔ ↑g ∈ A.topologicalClosure

Tactic:
rw [sup_eq_half_smul_add_add_abs_sub' ℝ]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : CompactSpace ↑s
p : C(↑s, 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)
frequently : ∀ (f : C(↑s, 𝕜)), (∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g) → p f
f : C(↑s, 𝕜)
⊢ p f

Tactic:
by
  refine f.induction_on const id star_id add mul fun h f ↦ frequently f ?_
  have := polynomialFunctions.starClosure_topologicalClosure s ▸ mem_top (x := f)
  rw [← SetLike.mem_coe, topologicalClosure_coe, mem_closure_iff_frequently] at this
  exact this.mp <| .of_forall h

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

Goal state before:
pp: F : Type u_2
S : Type u_3
K : Type u_4
A : Type u_5
inst✝¹³ : CommRing K
inst✝¹² : Ring A
inst✝¹¹ : Algebra K A
inst✝¹⁰ : TopologicalSpace K
inst✝⁹ : T1Space K
inst✝⁸ : TopologicalSpace A
inst✝⁷ : ContinuousSub A
inst✝⁶ : ContinuousSMul K A
inst✝⁵ : FunLike F A K
inst✝⁴ : AlgHomClass F K A K
inst✝³ : SetLike S A
inst✝² : OneMemClass S A
inst✝¹ : AddSubgroupClass S A
inst✝ : SMulMemClass S K A
φ : F
hφ : Continuous[inst✝⁸, inst✝¹⁰] ⇑φ
s : S
x : A
hxs : (𝓝 x ⊓ 𝓟 ↑s).NeBot
hxφ : φ x = 0
this : Tendsto (fun y ↦ y - φ y • 1) (𝓝 x ⊓ 𝓟 ↑s) (𝓝 x)
g : A
hg : g ∈ ↑s
⊢ g - φ g • 1 ∈ ↑(RingHom.ker φ)

Tactic:
simp [RingHom.mem_ker]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
s : Set α
x : α
inst✝ : TopologicalSpace β
⊢ UpperHemicontinuousWithinAt f s x ↔ ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝[s] x

Tactic:
by
  simp_rw [upperHemicontinuousWithinAt_iff]
  rw [hasBasis_nhdsSet (f x) |>.forall_iff ?h₁, hasBasis_nhdsSet (f x) |>.forall_iff ?h₂]
  case h₂ =>
    intro s t hst
    gcongr
  case h₁ =>
    intro s t hst
    gcongr
  refine forall₂_congr fun u ⟨hu, hfu⟩ ↦ ?_
  simp [hu.mem_nhdsSet, eventually_iff, Iic]

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
inst✝ : TopologicalSpace β
| (∀ (x : α), ∀ u ∈ 𝓝ˢ (f x), f ⁻¹' Iic u ∈ 𝓝 x) ↔ ∀ (u : Set β), IsOpen[inst✝] u → ∀ x ∈ f ⁻¹' Iic u, f ⁻¹' Iic u ∈ 𝓝 x

Tactic:
enter [1, x]
    rw [hasBasis_nhdsSet (f x) |>.forall_iff fun s t hst ↦ by gcongr]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → Set β
inst✝ : TopologicalSpace β
x : α
| ∀ (i : Set β), IsOpen[inst✝] i ∧ f x ⊆ i → f ⁻¹' Iic i ∈ 𝓝 x
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case left
α : Type u_1
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x✝¹ : Set α × Set α
s t : Set α
x✝ : (s, t) ∈ hausdorffEntourage V
hst : s ⊆ V.preimage t
hts : t ⊆ V.image s
⊢ closure[inst✝.toTopologicalSpace] s ⊆ SetRel.preimage U (closure[inst✝.toTopologicalSpace] t)

pp: case right
α : Type u_1
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x✝¹ : Set α × Set α
s t : Set α
x✝ : (s, t) ∈ hausdorffEntourage V
hst : s ⊆ V.preimage t
hts : t ⊆ V.image s
⊢ closure[inst✝.toTopologicalSpace] t ⊆ SetRel.image U (closure[inst✝.toTopologicalSpace] s)

Tactic:
· grw [closure_subset_preimage hV s, hst, ← subset_closure, ← hVU, SetRel.preimage_comp]

Goal state after:
case right
α : Type u_1
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
x✝¹ : Set α × Set α
s t : Set α
x✝ : (s, t) ∈ hausdorffEntourage V
hst : s ⊆ V.preimage t
hts : t ⊆ V.image s
⊢ closure[inst✝.toTopologicalSpace] t ⊆ SetRel.image U (closure[inst✝.toTopologicalSpace] s)
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x✝ :
  (∀ (U : Set β), IsOpen[inst✝] U → IsOpen[inst✝¹] (f ⁻¹' 𝒫 U)) ∧
    ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[inst✝¹] (f ⁻¹' 𝒫 F)
h₁ : ∀ (U : Set β), IsOpen[inst✝] U → IsOpen[inst✝¹] (f ⁻¹' 𝒫 U)
h₂ : ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[inst✝¹] (f ⁻¹' 𝒫 F)
U : Set β
hU : U ∈ {V | IsOpen[inst✝] V}
⊢ IsOpen[inst✝¹] (f ⁻¹' {s | (s ∩ U).Nonempty})

Tactic:
preimage_ofPred_eq,

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x✝ :
  (∀ (U : Set β), IsOpen[inst✝] U → IsOpen[inst✝¹] (f ⁻¹' 𝒫 U)) ∧
    ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[inst✝¹] (f ⁻¹' 𝒫 F)
h₁ : ∀ (U : Set β), IsOpen[inst✝] U → IsOpen[inst✝¹] (f ⁻¹' 𝒫 U)
h₂ : ∀ (F : Set β), IsClosed[inst✝] F → IsClosed[inst✝¹] (f ⁻¹' 𝒫 F)
U : Set β
hU : U ∈ {V | IsOpen[inst✝] V}
⊢ IsOpen[inst✝¹] {a | (f a ∩ U).Nonempty}
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ inst✝ =
    generateFrom
      ((fun x ↦ (fun x ↦ {x}) ⁻¹' {t | t ⊆ x}) '' {U | IsOpen[inst✝] U} ∪
        (fun x ↦ (fun x ↦ {x}) ⁻¹' {s | (s ∩ x).Nonempty}) '' {U | IsOpen[inst✝] U})

Tactic:
preimage_ofPred_eq,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ inst✝ =
    generateFrom
      ((fun a ↦ {a_1 | {a_1} ⊆ a}) '' {U | IsOpen[inst✝] U} ∪
        (fun a ↦ {a_1 | ({a_1} ∩ a).Nonempty}) '' {U | IsOpen[inst✝] U})
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
⊢ U ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] U → {a | s ⊆ U.preimage a} ∩ {a | a ⊆ U.image s} ∈ 𝓝 s

Tactic:
⟨hU₁, hU₂⟩

Goal state after:
α : Type u_1
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsOpen[instTopologicalSpaceProd] U
⊢ {a | s ⊆ U.preimage a} ∩ {a | a ⊆ U.image s} ∈ 𝓝 s
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ (∀ (U : Set α), IsOpen[inst✝] U → IsOpen[instTopologicalSpaceProd] ((fun x ↦ x.1 ∪ x.2) ⁻¹' {t | t ⊆ U})) ∧
    ∀ (F : Set α), IsClosed[inst✝] F → IsClosed[instTopologicalSpaceProd] ((fun x ↦ x.1 ∪ x.2) ⁻¹' {t | t ⊆ F})

Tactic:
preimage_ofPred_eq,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ (∀ (U : Set α), IsOpen[inst✝] U → IsOpen[instTopologicalSpaceProd] {a | a.1 ∪ a.2 ⊆ U}) ∧
    ∀ (F : Set α), IsClosed[inst✝] F → IsClosed[instTopologicalSpaceProd] {a | a.1 ∪ a.2 ⊆ F}