mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq✝ : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
⊢ ∫⁻ (x : α), g x ∂μ < ∞

Tactic:
rw [← h_univ]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq✝ : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
⊢ ∫⁻ (x : α), f x ∂μ < ∞
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case neg.h0
α : Type u_1
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
this : r⁻¹ • μ.rnDeriv ν = ↑r⁻¹ • μ.rnDeriv ν
⊢ ↑r ≠ 0

pp: case neg.ht
α : Type u_1
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
this : r⁻¹ • μ.rnDeriv ν = ↑r⁻¹ • μ.rnDeriv ν
⊢ ↑r ≠ ∞

Tactic:
· simp [hr]

Goal state after:
case neg.ht
α : Type u_1
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
this : r⁻¹ • μ.rnDeriv ν = ↑r⁻¹ • μ.rnDeriv ν
⊢ ↑r ≠ ∞
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 α
inst✝ : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (fun i ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (fun i ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I : ∀ᶠ (i : ι) in l, ∫ (y : α), g i y • (f y - c) ∂μ + (∫ (y : α), g i y ∂μ) • c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (fun x ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
⊢ ∀ᶠ (n : ι) in l, ‖∫ (y : α), g n y • (f y - c) ∂μ‖ ≤ K * ⨍ (y : α) in a n, ‖f y - c‖ ∂μ

Tactic:
filter_upwards [g_supp, g_bound, f_int, (tendsto_order.1 hg).1 _ zero_lt_one]
      with i hi h'i h''i hi_int

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (fun i ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (fun i ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I : ∀ᶠ (i : ι) in l, ∫ (y : α), g i y • (f y - c) ∂μ + (∫ (y : α), g i y ∂μ) • c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (fun x ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
h''i : IntegrableOn f (a i) μ
hi_int : 0 < ∫ (y : α), g i y ∂μ
⊢ ‖∫ (y : α), g i y • (f y - c) ∂μ‖ ≤ K * ⨍ (y : α) in a i, ‖f y - c‖ ∂μ
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ (μ.singularPart ν).singularPart ν = μ.singularPart ν

Tactic:
Measure.singularPart_eq_self

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ.singularPart ν ⟂ₘ ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
n : ℕ
⊢ ∫⁻ (x : α) in spanningSets μ n, μ.rnDeriv ν x ∂ν ≠ ∞

Tactic:
refine (lintegral_rnDeriv_lt_top_of_measure_ne_top _ ?_).ne

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
n : ℕ
⊢ μ (spanningSets μ n) ≠ ∞
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a}
hs : s = {x | ∃ᶠ (x : Set α) in v.filterAt x, μ x = 0}
f : α → Set (Set α) := fun x ↦ {a | μ a = 0}
h : v.FineSubfamilyOn f s
⊢ ∑' (x : ↑h.index), μ (h.covering ↑x) = ∑' (x : ↑h.index), 0

Tactic:
congr; ext1 x; exact h.covering_mem x.2

Goal state after:
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 μ
⊢ ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + (ν₂.singularPart μ + μ.withDensity (ν₂.rnDeriv μ)))

Tactic:
← ν₂.haveLebesgueDecomposition_add μ,

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝⁴ : IsFiniteMeasure ν₁
inst✝³ : IsFiniteMeasure ν₂
inst✝² : ν₁.HaveLebesgueDecomposition μ
inst✝¹ : ν₂.HaveLebesgueDecomposition μ
inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + ν₂)
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 α
⊢ eVariationOn f s = ⨆ p, ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i))

Tactic:
by
  apply le_antisymm
  · apply iSup_le
    rintro ⟨n, u, u_mono, u_mem⟩
    have : ∃ p : (n : ℕ) × { u : ℕ → α // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s },
        (p.2 : ℕ → α) p.1 = u n ∧
        ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) =
        ∑ i ∈ Finset.range p.1, edist (f ((p.2 : ℕ → α) (i + 1))) (f ((p.2 : ℕ → α) i)) := by
      induction n with
      | zero => exact ⟨⟨0, ⟨u, by grind [StrictMonoOn], fun i hi ↦ u_mem _⟩⟩, by simp⟩
      | succ n ih =>
        rcases ih with ⟨⟨m, v, v_mono, v_mem⟩, hv, h'v⟩
        simp only [Finset.sum_range_succ, Sigma.exists, Subtype.exists, mem_Iic, exists_and_left,
          exists_prop]
        rcases (u_mono (Nat.le_add_right n 1)).eq_or_lt with hn | hn
        · simp only [← hn, edist_self, add_zero]
          exact ⟨m, v, hv, ⟨v_mono, v_mem⟩, h'v⟩
        · refine ⟨m + 1, fun i ↦ if i ≤ m then v i else u (n + 1), by simp,
            by grind [StrictMonoOn], ?_⟩
          simp only [h'v, ← hv, Order.add_one_le_iff, Finset.sum_range_succ, lt_self_iff_false,
            ↓reduceIte, le_refl]
          congr 1
          exact Finset.sum_congr rfl (by grind)
    rcases this with ⟨p, -, hp⟩
    rw [hp]
    apply le_iSup _ p
  · apply iSup_le
    rintro ⟨n, u, u_mono, u_mem⟩
    apply sum_le_of_monotoneOn_Iic (by grind [MonotoneOn, StrictMonoOn]) (by grind)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
hxy : y ≤ x
u : ℕ → α := fun n ↦ if n = 0 then y else x
hu : Monotone u
⊢ edist (f x) (f y) ≤ eVariationOn f s

Tactic:
have us : ∀ i, u i ∈ s := fun
  | 0 => hy
  | (_ + 1) => hx

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
hxy : y ≤ x
u : ℕ → α := fun n ↦ if n = 0 then y else x
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
⊢ edist (f x) (f y) ≤ eVariationOn f s
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

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

Tactic:
← ν₂.haveLebesgueDecomposition_add μ,

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝² : SigmaFinite ν₁
inst✝¹ : SigmaFinite ν₂
inst✝ : SigmaFinite μ
⊢ ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + ν₂)
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
hf : BoundedVariationOn f s
hg : BoundedVariationOn g s
B : E →L[ℝ] F →L[ℝ] G
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ‖f x‖ₑ + edist (f y) (f x) ≤ ‖f x‖ₑ + eVariationOn f s

Tactic:
eVariationOn.edist_le _ hy hx

Goal state after:
α : 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
hf : BoundedVariationOn f s
hg : BoundedVariationOn g s
B : E →L[ℝ] F →L[ℝ] G
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ‖f x‖ₑ + eVariationOn f s ≤ ‖f x‖ₑ + eVariationOn f 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
hf : BoundedVariationOn f s
hg : BoundedVariationOn g s
B : E →L[ℝ] F →L[ℝ] G
x : α
hx : x ∈ s
A : ∀ y ∈ s, ‖f y‖ₑ ≤ ‖f x‖ₑ + eVariationOn f s
y : α
hy : y ∈ s
⊢ ‖g x‖ₑ + edist (g y) (g x) ≤ ‖g x‖ₑ + eVariationOn g s

Tactic:
eVariationOn.edist_le _ hy hx

Goal state after:
α : 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
hf : BoundedVariationOn f s
hg : BoundedVariationOn g s
B : E →L[ℝ] F →L[ℝ] G
x : α
hx : x ∈ s
A : ∀ y ∈ s, ‖f y‖ₑ ≤ ‖f x‖ₑ + eVariationOn f s
y : α
hy : y ∈ s
⊢ ‖g x‖ₑ + eVariationOn g s ≤ ‖g x‖ₑ + eVariationOn g s
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 ↦ ?_)

Goal state after:
α : 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 : ℕ → α := fun n ↦ y^[n] x₀
I : ∀ (n : ℕ), v n ∈ s
n✝ n : ℕ
⊢ v n ≤ v (n + 1)
Module: Mathlib.Topology.Algebra.StarSubalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : StarRing R
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : StarRing A
inst✝¹⁰ : StarModule R A
inst✝⁹ : IsSemitopologicalSemiring A
inst✝⁸ : ContinuousStar A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
inst✝⁴ : StarRing B
inst✝³ : T2Space B
F : Type u_4
S : StarSubalgebra R A
inst✝² : FunLike F (↥S.topologicalClosure) B
inst✝¹ : AlgHomClass F R (↥S.topologicalClosure) B
inst✝ : StarHomClass F (↥S.topologicalClosure) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst✝⁷] ⇑φ
hψ : Continuous[instTopologicalSpaceSubtype, inst✝⁷] ⇑ψ
h : ∀ (x : ↥S), φ ((inclusion ⋯) x) = ψ ((inclusion ⋯) x)
⊢ φ = ψ

Tactic:
have : (φ : S.topologicalClosure →⋆ₐ[R] B) = (ψ : S.topologicalClosure →⋆ₐ[R] B) := by
    refine StarAlgHom.ext_topologicalClosure (R := R) (A := A) (B := B) hφ hψ (StarAlgHom.ext ?_)
    simpa only [StarAlgHom.coe_comp, StarAlgHom.coe_coe] using! h
  rw [DFunLike.ext'_iff, ← StarAlgHom.coe_coe]
  apply congrArg _ this

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

Tactic:
· 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: case succ
R : Type u_1
inst✝ : CommRing R
n k ν : ℕ
⊢ k < ν + 1 → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n (ν + 1))) = 0

Tactic:
Nat.lt_succ_iff

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

Goal state before:
pp: case pos.succ
R : Type u_1
inst✝ : CommRing R
ν : ℕ
ih :
  ∀ (n : ℕ), ν ≤ n → eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)
n : ℕ
h : ν + 1 ≤ n
h' : ν ≤ n - 1
⊢ ↑n * eval (↑(n - 1 - (ν - 1))) (ascPochhammer R ν) = ↑(n - (ν - 0)) * eval (↑(n - (ν - 0)) + 1) (ascPochhammer R ν)

Tactic:
obtain rfl | h'' := ν.eq_zero_or_pos

Goal state after:
case pos.succ.inl
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih :
  ∀ (n : ℕ), 0 ≤ n → eval 0 ((⇑derivative)^[0] (bernsteinPolynomial R n 0)) = eval (↑(n - (0 - 1))) (ascPochhammer R 0)
h : 0 + 1 ≤ n
h' : 0 ≤ n - 1
⊢ ↑n * eval (↑(n - 1 - (0 - 1))) (ascPochhammer R 0) = ↑(n - (0 - 0)) * eval (↑(n - (0 - 0)) + 1) (ascPochhammer R 0)

case pos.succ.inr
R : Type u_1
inst✝ : CommRing R
ν : ℕ
ih :
  ∀ (n : ℕ), ν ≤ n → eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) = eval (↑(n - (ν - 1))) (ascPochhammer R ν)
n : ℕ
h : ν + 1 ≤ n
h' : ν ≤ n - 1
h'' : ν > 0
⊢ ↑n * eval (↑(n - 1 - (ν - 1))) (ascPochhammer R ν) = ↑(n - (ν - 0)) * eval (↑(n - (ν - 0)) + 1) (ascPochhammer R ν)
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
this : ∀ i ∈ 𝓝 0, ∃ j, 0 < j ∧ ∀ (x y : ↑I), (x, y) ∈ {p | dist p.1 p.2 < j} → (f x, f y) ∈ {x | x.1 - x.2 ∈ id i}
⊢ ∃ δ > 0, ∀ (x y : ↑I), dist x y < δ → gauge U (f x - f y) < 1 / 2

Tactic:
exact this {z | gauge U z < 1 / 2} <| tendsto_gauge_nhds_zero hU₀
      |>.eventually_lt_const <| by positivity

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 ∈ A

Tactic:
polynomial_comp_attachBound

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
g : ℝ[X]
⊢ ↑((Polynomial.aeval f) g) ∈ A
Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : L.SeparatesPointsStrongly
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
⊢ ∃ x ∈ Metric.ball f ε, x ∈ L

Tactic:
simp only [Metric.mem_ball]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : L.SeparatesPointsStrongly
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
⊢ ∃ x, dist x f < ε ∧ x ∈ L
Module: Mathlib.Analysis.Normed.Algebra.Unitization

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : RegularNormedAlgebra 𝕜 A
⊢ LipschitzWith 2 ⇑(addEquiv 𝕜 A)

Tactic:
rw [← Real.toNNReal_ofNat]
  refine AddMonoidHomClass.lipschitz_of_bound (Unitization.addEquiv 𝕜 A) 2 fun x => ?_
  rw [norm_eq_sup, Prod.norm_def]
  refine max_le ?_ ?_
  · rw [mul_max_of_nonneg _ _ (zero_le_two : (0 : ℝ) ≤ 2)]
    exact le_max_of_le_left ((le_add_of_nonneg_left (norm_nonneg _)).trans_eq (two_mul _).symm)
  · nontriviality A
    rw [two_mul]
    calc
      ‖x.snd‖ = ‖mul 𝕜 A x.snd‖ :=
        .symm <| (isometry_mul 𝕜 A).norm_map_of_map_zero (map_zero _) _
      _ ≤ ‖algebraMap 𝕜 _ x.fst + mul 𝕜 A x.snd‖ + ‖x.fst‖ := by
        simpa only [add_comm _ (mul 𝕜 A x.snd), norm_algebraMap'] using
          norm_le_add_norm_add (mul 𝕜 A x.snd) (algebraMap 𝕜 _ x.fst)
      _ ≤ _ := add_le_add le_sup_right le_sup_left

Goal state after:
Module: Mathlib.Analysis.Real.Spectrum

Goal state before:
pp: A : Type u_1
inst✝³ : Ring A
inst✝² : PartialOrder A
inst✝¹ : Algebra ℝ A
inst✝ : NonnegSpectrumClass ℝ A
a : A
x : ℝ≥0
ha : 0 ≤ a
⊢ ↑x ∈ spectrum ℝ a ↔ x ∈ spectrum ℝ≥0 a

Tactic:
by
  simp [← (SpectrumRestricts.nnreal_of_nonneg ha).algebraMap_image, Set.mem_image,
    NNReal.algebraMap_eq_coe]

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : TopologicalSpace A
inst✝⁵ : T2Space A
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
s : Set 𝕜
hs : CompactSpace ↑s
h0 : Fact (0 ∈ s)
φ ψ : ContinuousMapZero (↑s) 𝕜 →⋆ₙₐ[𝕜] A
hφ : Continuous[_, inst✝⁶] ⇑φ
hψ : Continuous[_, inst✝⁶] ⇑ψ
h : φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s)
f : ContinuousMapZero (↑s) 𝕜
hf : f ∈ ↑(adjoin 𝕜 {ContinuousMapZero.id s})
⊢ φ f = ψ f

Tactic:
← NonUnitalStarAlgHom.mem_equalizer

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : TopologicalSpace A
inst✝⁵ : T2Space A
inst✝⁴ : NonUnitalRing A
inst✝³ : StarRing A
inst✝² : Module 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
s : Set 𝕜
hs : CompactSpace ↑s
h0 : Fact (0 ∈ s)
φ ψ : ContinuousMapZero (↑s) 𝕜 →⋆ₙₐ[𝕜] A
hφ : Continuous[_, inst✝⁶] ⇑φ
hψ : Continuous[_, inst✝⁶] ⇑ψ
h : φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s)
f : ContinuousMapZero (↑s) 𝕜
hf : f ∈ ↑(adjoin 𝕜 {ContinuousMapZero.id s})
⊢ f ∈ NonUnitalStarAlgHom.equalizer φ ψ
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ IsClopen {∅}

Tactic:
rw [← powerset_empty]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ IsClopen (𝒫 ∅)
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: case a.refine_2
α : Type u_1
U V : SetRel α α
s t : Set α
hst : s ⊆ (U ○ V).preimage t
hts : t ⊆ (U ○ V).image s
z : α
hz : z ∈ t
⊢ z ∈ V.image (U.image s ∩ V.preimage t)

Tactic:
obtain ⟨x, hx, y, hxy, hyz⟩ := hts hz

Goal state after:
case a.refine_2
α : Type u_1
U V : SetRel α α
s t : Set α
hst : s ⊆ (U ○ V).preimage t
hts : t ⊆ (U ○ V).image s
z : α
hz : z ∈ t
x : α
hx : x ∈ s
y : α
hxy : (x, y) ∈ U
hyz : (y, z) ∈ V
⊢ z ∈ V.image (U.image s ∩ V.preimage t)
Module: Mathlib.Topology.Semicontinuity.Hemicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → Set β
ι : Type u_3
F : ι → α → Set β
l : Filter ι
inst✝¹ : l.NeBot
inst✝ : UniformSpace β
htendsto : TendstoUniformly F f l
hF : ∀ (n : ι), LowerHemicontinuous (F n)
⊢ LowerHemicontinuous f

Tactic:
by
  rw [← lowerHemicontinuousOn_univ_iff]
  exact htendsto.tendstoUniformlyOn.lowerHemicontinuousOn (fun n ↦ (hF n).lowerHemicontinuousOn _)

Goal state after:
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}
⊢ IsClosed[inst✝¹] {a | f a ⊆ Uᶜ}

Tactic:
exact h₂ Uᶜ hU.isClosed_compl

Goal state after:
Module: Mathlib.Topology.UniformSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : T2Space α
inst✝ : CompleteSpace α
⊢ IsClosed (Set.range toCloseds)

Tactic:
convert! Closeds.isClosed_setOfPred_totallyBounded
    exact subset_antisymm
      (Set.range_subset_iff.mpr fun K => K.isCompact.totallyBounded)
      (fun K hK => ⟨⟨K, hK.isCompact_of_isClosed K.isClosed⟩, rfl⟩)

Goal state after:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: case pos
α : Type u_1
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : IsPreconnected s
t : Set α
hts : t ∈ s
ht : IsPreconnected t
hts' : t ⊆ ⋃₀ s
U V : Set α
hU : IsOpen[inst✝] U
hV : IsOpen[inst✝] V
hUV : ⋃₀ s ⊆ U ∪ V
ht' : t ⊆ U ∨ t ⊆ V
⊢ (⋃₀ s ∩ U).Nonempty → (⋃₀ s ∩ V).Nonempty → (⋃₀ s ∩ (U ∩ V)).Nonempty

pp: case neg
α : Type u_1
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : IsPreconnected s
t : Set α
hts : t ∈ s
ht : IsPreconnected t
hts' : t ⊆ ⋃₀ s
U V : Set α
hU : IsOpen[inst✝] U
hV : IsOpen[inst✝] V
hUV : ⋃₀ s ⊆ U ∪ V
ht' : ¬t ⊆ U ∧ ¬t ⊆ V
⊢ (⋃₀ s ∩ U).Nonempty → (⋃₀ s ∩ V).Nonempty → (⋃₀ s ∩ (U ∩ V)).Nonempty

Tactic:
· -- Consider the case when one of them covers `t`, say `U`.
    wlog htU : t ⊆ U generalizing U V
    · grind
    -- There is also some `u ∈ s` that intersects `V`.
    rintro - hV'
    rw [sUnion_eq_biUnion, iUnion₂_inter, nonempty_biUnion] at hV'
    obtain ⟨u, hus, huV⟩ := hV'
    -- Every set in `s` either is in `U` or intersects `V`.
    have : s ⊆ U.powerset ∪ {v | (v ∩ V).Nonempty} := by
      grind [=_ sdiff_subset_iff, =_ not_disjoint_iff_nonempty_inter]
    -- Since `s` connects `t` and `u`, there is some `v ∈ s` that is in `U` and intersects `V`.
    obtain ⟨v, hvs, hvU, hvV⟩ :=
      hs _ _ hU.powerset_vietoris (isOpen_inter_nonempty_of_isOpen hV) this
        ⟨t, hts, htU⟩ ⟨u, hus, huV⟩
    -- `U` intersects `V` within `v`, and therefore also within `⋃₀ s`.
    apply hvV.mono
    grind

Goal state after:
case neg
α : Type u_1
inst✝ : TopologicalSpace α
s : Set (Set α)
hs : IsPreconnected s
t : Set α
hts : t ∈ s
ht : IsPreconnected t
hts' : t ⊆ ⋃₀ s
U V : Set α
hU : IsOpen[inst✝] U
hV : IsOpen[inst✝] V
hUV : ⋃₀ s ⊆ U ∪ V
ht' : ¬t ⊆ U ∧ ¬t ⊆ V
⊢ (⋃₀ s ∩ U).Nonempty → (⋃₀ s ∩ V).Nonempty → (⋃₀ s ∩ (U ∩ V)).Nonempty