mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
i : ι
ne : c.Nonempty
⊢ find c ne i ∈ c

Tactic:
by
  rw [find]
  split_ifs with h
  exacts [h.choose_spec.1, ne.some_mem]

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : FiberBundle F V
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
u : Set M
s : (x : M) → V x
ψ : M → 𝕜
hψ : ContMDiffOn I 𝓘(𝕜, 𝕜) n ψ u
ht : IsOpen u
ht' : tsupport ψ ⊆ u
hs : ContMDiffOn I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, s x⟩) u
⊢ ContMDiff I (I.prod 𝓘(𝕜, F)) n fun x ↦ ⟨x, (ψ • s) x⟩

Tactic:
apply contMDiff_of_contMDiffOn_union_of_isOpen (hψ.smul_section hs) ?_ ?_ ht
      (isOpen_compl_iff.mpr <| isClosed_tsupport ψ)
  · apply ((contMDiff_zeroSection _ _).contMDiffOn (s := (tsupport ψ)ᶜ)).congr
    intro y hy
    simp [image_eq_zero_of_notMem_tsupport hy, zeroSection]
  · exact Set.compl_subset_iff_union.mp <| Set.compl_subset_compl.mpr ht'

Goal state after:
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := ⋯.toFinset
hs : ↑s = {i | (f i) x ≠ 0}
A : (support fun i ↦ f.toPOUFun i x) ⊆ ↑s
B : (mulSupport fun i ↦ 1 - (f i) x) ⊆ ↑s
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
⊢ ∑ᶠ (i : ι), f.toPOUFun i x = 1 - ∏ᶠ (i : ι), (1 - (f i) x)

Tactic:
finsum_eq_sum_of_support_subset _ A,

Goal state after:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := ⋯.toFinset
hs : ↑s = {i | (f i) x ≠ 0}
A : (support fun i ↦ f.toPOUFun i x) ⊆ ↑s
B : (mulSupport fun i ↦ 1 - (f i) x) ⊆ ↑s
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
⊢ ∑ i ∈ s, f.toPOUFun i x = 1 - ∏ᶠ (i : ι), (1 - (f i) x)
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
H : Type uH
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : IsManifold I ∞ M
n : ℕ∞
inst✝² : T2Space M
inst✝¹ : NormalSpace M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst✝⁶] s
ht : IsClosed[inst✝⁶] t
hd : Disjoint s t
u : Set M
u_op : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hut : closure[inst✝⁶] u ⊆ tᶜ
⊢ ∃ f, (∀ᶠ (x : M) in 𝓝ˢ s, f x = 0) ∧ (∀ᶠ (x : M) in 𝓝ˢ t, f x = 1) ∧ ∀ (x : M), f x ∈ Icc 0 1

Tactic:
obtain ⟨v, v_op, htv, hvu⟩ := normal_exists_closure_subset ht isClosed_closure.isOpen_compl
    (subset_compl_comm.mp hut)

Goal state after:
E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
H : Type uH
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : IsManifold I ∞ M
n : ℕ∞
inst✝² : T2Space M
inst✝¹ : NormalSpace M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst✝⁶] s
ht : IsClosed[inst✝⁶] t
hd : Disjoint s t
u : Set M
u_op : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hut : closure[inst✝⁶] u ⊆ tᶜ
v : Set M
v_op : IsOpen[inst✝⁶] v
htv : t ⊆ v
hvu : closure[inst✝⁶] v ⊆ (closure[inst✝⁶] u)ᶜ
⊢ ∃ f, (∀ᶠ (x : M) in 𝓝ˢ s, f x = 0) ∧ (∀ᶠ (x : M) in 𝓝ˢ t, f x = 1) ∧ ∀ (x : M), f x ∈ Icc 0 1
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: E : Type uE
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℝ E
H : Type uH
inst✝¹⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹³ : TopologicalSpace M
inst✝¹² : ChartedSpace H M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : IsManifold I ∞ M
inst✝⁹ : SigmaCompactSpace M
inst✝⁸ : T2Space M
n : ℕ∞
F_fiber : Type u_1
inst✝⁷ : NormedAddCommGroup F_fiber
inst✝⁶ : NormedSpace ℝ F_fiber
V : M → Type u_2
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : (x : M) → Module ℝ (V x)
inst✝² : TopologicalSpace (TotalSpace F_fiber V)
inst✝¹ : FiberBundle F_fiber V
inst✝ : VectorBundle ℝ F_fiber V
t : (x : M) → Set (V x)
ht_conv : ∀ (x : M), Convex ℝ (t x)
W : M → Set M
h_nhds : ∀ (x₀ : M), W x₀ ∈ 𝓝 x₀
s_loc : M → (x : M) → V x
s_smooth : ∀ (x₀ : M), ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) (↑n) (fun x ↦ ⟨x, s_loc x₀ x⟩) (W x₀)
h_mem_t : ∀ (x₀ y : M), y ∈ W x₀ → s_loc x₀ y ∈ t y
U : M → Set M := fun x ↦ interior (W x)
hU_covers_univ : univ ⊆ ⋃ x, U x
ρ : SmoothPartitionOfUnity M I M
hρU : ρ.IsSubordinate U
s : (x : M) → V x := fun x ↦ ∑ᶠ (j : M), (ρ j) x • s_loc j x
this : ∀ (j : M), ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) ↑n fun x ↦ ⟨x, (ρ j) x • s_loc j x⟩
hs : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) ↑n fun x ↦ ⟨x, s x⟩
x j : M
⊢ (ρ j) x ≠ 0 → s_loc j x ∈ t x

Tactic:
h_ρjx_ne_zero

Goal state after:
E : Type uE
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℝ E
H : Type uH
inst✝¹⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹³ : TopologicalSpace M
inst✝¹² : ChartedSpace H M
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : IsManifold I ∞ M
inst✝⁹ : SigmaCompactSpace M
inst✝⁸ : T2Space M
n : ℕ∞
F_fiber : Type u_1
inst✝⁷ : NormedAddCommGroup F_fiber
inst✝⁶ : NormedSpace ℝ F_fiber
V : M → Type u_2
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : (x : M) → Module ℝ (V x)
inst✝² : TopologicalSpace (TotalSpace F_fiber V)
inst✝¹ : FiberBundle F_fiber V
inst✝ : VectorBundle ℝ F_fiber V
t : (x : M) → Set (V x)
ht_conv : ∀ (x : M), Convex ℝ (t x)
W : M → Set M
h_nhds : ∀ (x₀ : M), W x₀ ∈ 𝓝 x₀
s_loc : M → (x : M) → V x
s_smooth : ∀ (x₀ : M), ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) (↑n) (fun x ↦ ⟨x, s_loc x₀ x⟩) (W x₀)
h_mem_t : ∀ (x₀ y : M), y ∈ W x₀ → s_loc x₀ y ∈ t y
U : M → Set M := fun x ↦ interior (W x)
hU_covers_univ : univ ⊆ ⋃ x, U x
ρ : SmoothPartitionOfUnity M I M
hρU : ρ.IsSubordinate U
s : (x : M) → V x := fun x ↦ ∑ᶠ (j : M), (ρ j) x • s_loc j x
this : ∀ (j : M), ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) ↑n fun x ↦ ⟨x, (ρ j) x • s_loc j x⟩
hs : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) ↑n fun x ↦ ⟨x, s x⟩
x j : M
h_ρjx_ne_zero : (ρ j) x ≠ 0
⊢ s_loc j x ∈ t x
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ 0 ≤ ∫ (x : α) in s, -f x ∂μ

Tactic:
integral_neg,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ 0 ≤ -∫ (a : α) in s, f a ∂μ
Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : ℕ → E := fun n ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
W : ∀ (n : ℕ), ∃ d_1, d_1 ≠ 0 ∧ ‖d_1 • d n‖ < 1 ∧ 1 / ‖r‖ ≤ ‖d_1 • d n‖ ∧ ‖d_1‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty

Tactic:
choose c c_ne c_le le_c hc using W

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : ℕ → E := fun n ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
Module: Mathlib.Analysis.Calculus.TangentCone.Seq

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
⊢ ∃ d, x + d ∈ s ∧ ‖d‖ < (1 / (2 * ‖c‖)) ^ n

Tactic:
Metric.mem_closure_iff

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : ∀ ε > 0, ∃ b ∈ s, dist x b < ε
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
⊢ ∃ d, x + d ∈ s ∧ ‖d‖ < (1 / (2 * ‖c‖)) ^ n
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: case refine_1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
ι : Type u_3
s : Finset ι
a : ι → ℝ
v : ι → E
g : E → ℝ
g_smooth : ContDiff ℝ (↑⊤) g
g_comp : HasCompactSupport g
A : ∀ i ∈ s, Integrable (fun x ↦ g x • (a i • fun x ↦ lineDeriv ℝ f x (v i)) x) μ
i : ι
_hi : i ∈ s
L : StrongDual ℝ E → ℝ := fun f ↦ f (v i)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun x ↦ (L ∘ fderiv ℝ g) x * f x

Tactic:
exact ((g_smooth.continuous_fderiv (by simp)).clm_apply continuous_const).mul
      hf.continuous

Goal state after:
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
f : ℝ → X
a b c d : ℝ
hf : AbsolutelyContinuousOnInterval f a b
habcd : uIcc c d ⊆ uIcc a b
⊢ AbsolutelyContinuousOnInterval f c d

Tactic:
by
  simp only [AbsolutelyContinuousOnInterval, Tendsto] at *
  refine le_trans (Filter.map_mono ?_) hf
  gcongr; exact disjWithin_mono habcd

Goal state after:
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
hg :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
⊢ ∀ᶠ (t : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter ⊓ 𝓟 (disjWithin a b),
    ∑ i ∈ Finset.range t.1, dist ((f • g) (t.2 i).1) ((f • g) (t.2 i).2) ≤
      C * ∑ i ∈ Finset.range t.1, dist (g (t.2 i).1) (g (t.2 i).2) +
        D * ∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2)

Tactic:
rw [eventually_inf_principal]

Goal state after:
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
hg :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
⊢ ∀ᶠ (x : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter,
    x ∈ disjWithin a b →
      ∑ i ∈ Finset.range x.1, dist ((f • g) (x.2 i).1) ((f • g) (x.2 i).2) ≤
        C * ∑ i ∈ Finset.range x.1, dist (g (x.2 i).1) (g (x.2 i).2) +
          D * ∑ i ∈ Finset.range x.1, dist (f (x.2 i).1) (f (x.2 i).2)
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
⊢ AbsolutelyContinuousOnInterval f a b

Tactic:
by
  rw [absolutelyContinuousOnInterval_iff]
  intro ε hε
  refine ⟨ε / (K + 1), by positivity, fun (n, I) hnI₁ hnI₂ ↦ ?_⟩
  calc
    _ ≤ ∑ i ∈ Finset.range n, K * dist (I i).1 (I i).2 := by
      apply Finset.sum_le_sum
      intro i hi
      have := hfK (hnI₁.left i hi).left (hnI₁.left i hi).right
      apply ENNReal.toReal_mono (Ne.symm (not_eq_of_beq_eq_false rfl)) at this
      rwa [ENNReal.toReal_mul, ← dist_edist, ← dist_edist] at this
    _ = K * ∑ i ∈ Finset.range n, dist (I i).1 (I i).2 := by symm; exact Finset.mul_sum _ _ _
    _ ≤ K * (ε / (K + 1)) := by gcongr
    _ < (K + 1) * (ε / (K + 1)) := by gcongr; linarith
    _ = ε := by field

Goal state after:
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case right
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n + 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
hd : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) [[x₀, x]]
x' : ℝ
h1 : x' ∈ uIoo x₀ x
h2 :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
⊢ iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / ↑(n + 1)! =
    iteratedDeriv (n + 1) f x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!

Tactic:
iteratedDeriv_eq_iteratedFDeriv,

Goal state after:
case right
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n + 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
hd : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) [[x₀, x]]
x' : ℝ
h1 : x' ∈ uIoo x₀ x
h2 :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
⊢ iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / ↑(n + 1)! =
    ((iteratedFDeriv ℝ (n + 1) f x') fun x ↦ 1) * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a C x : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx : x ∈ Icc a a
hC : ∀ y ∈ Icc a a, ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C
⊢ ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !

Tactic:
Icc_self,

Goal state after:
case inl
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a C x : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
hx : x ∈ {a}
hC : ∀ y ∈ Icc a a, ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C
⊢ ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
v : E
hv : v ∈ ball 0 r
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : w ∈ sphere 0 1
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
⊢ (↑C + ‖L‖ + 1) * δ * ρ = ε * ‖v‖

Tactic:
hδ,

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
v : E
hv : v ∈ ball 0 r
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : w ∈ sphere 0 1
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
⊢ ε * ρ = ε * ‖v‖
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
C : ℝ≥0
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : FiniteDimensional ℝ F
inst✝ : μ.IsAddHaarMeasure
f : E → F
h : LipschitzWith C f
⊢ ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x

Tactic:
rw [← lipschitzOnWith_univ] at h
  simpa [differentiableWithinAt_univ] using h.ae_differentiableWithinAt_of_mem

Goal state after:
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case inr.zero
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this : x₀ ≠ x
hf : ∫ (t : ℝ) in x₀..x, deriv (fun t ↦ f t) t = f x - f x₀
⊢ ∫ (t : ℝ) in x₀..x, deriv (fun t ↦ f t) t = ∫ (t : ℝ) in x₀..x, derivWithin f [[x₀, x]] t

Tactic:
refine intervalIntegral.integral_congr_uIoo fun _ ⟨h1, h2⟩ => ?_

Goal state after:
case inr.zero
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this : x₀ ≠ x
hf : ∫ (t : ℝ) in x₀..x, deriv (fun t ↦ f t) t = f x - f x₀
x✝¹ : ℝ
x✝ : x✝¹ ∈ uIoo x₀ x
h1 : min x₀ x < x✝¹
h2 : x✝¹ < max x₀ x
⊢ deriv (fun t ↦ f t) x✝¹ = derivWithin f [[x₀, x]] x✝¹
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case e'_3
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this✝ : x₀ ≠ x
n : ℕ
ih :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
hf :
  ∀ k ≤ n + 1,
    let u := fun t ↦ (x - t) ^ k / ↑k !;
    let v := fun t ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
this :
  let u := fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!;
  let v := fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t;
  ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
⊢ ∫ (t : ℝ) in x₀..x, ((x - t) ^ (n + 1) / ((↑n + 1) * ↑n !)) • iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] t =
    ∫ (t : ℝ) in x₀..x,
      (fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!) t • deriv (fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) t

Tactic:
refine intervalIntegral.integral_congr_uIoo fun _ ⟨h1, h2⟩ => ?_

Goal state after:
case e'_3
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this✝ : x₀ ≠ x
n : ℕ
ih :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
hf :
  ∀ k ≤ n + 1,
    let u := fun t ↦ (x - t) ^ k / ↑k !;
    let v := fun t ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
this :
  let u := fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!;
  let v := fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t;
  ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
x✝¹ : ℝ
x✝ : x✝¹ ∈ uIoo x₀ x
h1 : min x₀ x < x✝¹
h2 : x✝¹ < max x₀ x
⊢ ((x - x✝¹) ^ (n + 1) / ((↑n + 1) * ↑n !)) • iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] x✝¹ =
    (fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!) x✝¹ • deriv (fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) x✝¹
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ √(x ^ 2 + y ^ 2) < (2 * √(1 + s ^ 2) + 1) * (1 - √((1 - x) ^ 2 + y ^ 2))

Tactic:
have H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2 := by
    calc √((1 - x) ^ 2 + y ^ 2)
      _ ≤ √((1 - x) ^ 2 + (s * x) ^ 2) := sqrt_le_sqrt <| by rw [← sq_abs y]; gcongr
      _ = √(1 - 2 * x + (1 + s ^ 2) * x * x) := by congr 1; ring
      _ ≤ √(1 - 2 * x + (1 + s ^ 2) * (1 / (1 + s ^ 2)) * x) := by gcongr
      _ = √(1 - x) := by congr 1; field
      _ ≤ 1 - x / 2 := by
        simp_rw [sub_eq_add_neg, ← neg_div]
        refine sqrt_one_add_le <| neg_le_neg_iff.mpr (hx₁.trans_le ?_).le
        rw [div_le_one (by positivity)]
        exact le_add_of_nonneg_right <| sq_nonneg s

Goal state after:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ √(x ^ 2 + y ^ 2) < (2 * √(1 + s ^ 2) + 1) * (1 - √((1 - x) ^ 2 + y ^ 2))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: case hg
f g : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ IntervalIntegrable (fun x ↦ deriv f x * g x) volume a b

Tactic:
exact hf.intervalIntegrable_deriv.mul_continuousOn hg.continuousOn

Goal state after:
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: case hg
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
k :
  Tendsto (fun n ↦ (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
⊢ Tendsto (fun n ↦ z ^ n / (z - 1) + (0 / (z - 1) + -1 / (z - 1))) atTop (𝓝 (0 / (z - 1) + -1 / (z - 1)))

Tactic:
apply Tendsto.add (Tendsto.div_const (tendsto_pow_atTop_nhds_zero_of_norm_lt_one hz) (z - 1))

Goal state after:
case hg
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := ⋯
k :
  Tendsto (fun n ↦ (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
⊢ Tendsto (fun x ↦ 0 / (z - 1) + -1 / (z - 1)) atTop (𝓝 (-1 / (z - 1)))