mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: case inr
𝕜 : 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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M'
⊢ writtenInExtChartAt I I (Sum.inr x) Sum.swap =ᶠ[𝓝[range ↑I] ↑I (↑(chartAt H (Sum.inr x)) (Sum.inr x))] id

Tactic:
let t := I.symm ⁻¹' (chartAt H x).target ∩ range I

Goal state after:
case inr
𝕜 : 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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M'
t : Set E := ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
⊢ writtenInExtChartAt I I (Sum.inr x) Sum.swap =ᶠ[𝓝[range ↑I] ↑I (↑(chartAt H (Sum.inr x)) (Sum.inr x))] id
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹¹ : NormedAddCommGroup E'
inst✝¹⁰ : NormedSpace 𝕜 E'
H : Type u_4
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_7
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
p : TangentBundle I H := ⟨↑I.symm 0, 0⟩
⊢ Continuous[instTopologicalSpaceModelProd H E, _] (TotalSpace.toProd H E).invFun

Tactic:
have : Continuous (chartAt (ModelProd H E) p).symm := by
        rw [← continuousOn_univ]
        convert! (chartAt (ModelProd H E) p).symm.continuousOn
        simp only [mfld_simps]

Goal state after:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹¹ : NormedAddCommGroup E'
inst✝¹⁰ : NormedSpace 𝕜 E'
H : Type u_4
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_7
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
p : TangentBundle I H := ⟨↑I.symm 0, 0⟩
this : Continuous[instTopologicalSpaceModelProd H E, _] ↑(chartAt (ModelProd H E) p).symm
⊢ Continuous[instTopologicalSpaceModelProd H E, _] (TotalSpace.toProd H E).invFun
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

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
s : Set M
z : M
F' : Type u_21
inst✝¹ : NormedField F'
inst✝ : NormedAlgebra 𝕜 F'
p : M → F'
p' : TangentSpace I z →L[𝕜] F'
hp : HasMFDerivAt[s] p z p'
hp_ne : p z ≠ 0
x✝ : TangentSpace I z
⊢ (p z ^ 2)⁻¹ * p' x✝ = (p z)⁻¹ * p' x✝ * (p z)⁻¹

Tactic:
ring_nf

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
⊢ u ∪ (tsupport ψ)ᶜ = Set.univ

Tactic:
· exact Set.compl_subset_iff_union.mp <| Set.compl_subset_compl.mpr ht'

Goal state after:
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: case hx
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
hx : x ∈ s
⊢ 1 - (f (f.ind x hx)) x = 0

pp: case hf
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
hx : x ∈ s
⊢ HasFiniteMulSupport fun i ↦ 1 - (f i) x

Tactic:
· simp only [f.ind_apply x hx, sub_self]

Goal state after:
case hf
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
x : X
hx : x ∈ s
⊢ HasFiniteMulSupport fun i ↦ 1 - (f i) x
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp

Goal state before:
pp: α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ FinStronglyMeasurable f μ

Tactic:
by
  borelize G
  have : SeparableSpace (Set.range f ∪ {0} : Set G) :=
    hf_meas.separableSpace_range_union_singleton
  let fs := SimpleFunc.approxOn f hf_meas.measurable (Set.range f ∪ {0}) 0 (by simp)
  refine ⟨fs, ?_, ?_⟩
  · have h_fs_Lp : ∀ n, MemLp (fs n) p μ :=
      SimpleFunc.memLp_approxOn_range hf_meas.measurable hf
    exact fun n => (fs n).measure_support_lt_top_of_memLp (h_fs_Lp n) hp_ne_zero hp_ne_top
  · intro x
    apply SimpleFunc.tendsto_approxOn
    apply subset_closure
    simp

Goal state after:
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: case refine_1
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
s : Set M
U : M → Set M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed[inst✝⁴] s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
hB : ∀ x ∈ s, (𝓝 x).HasBasis (fun f ↦ tsupport ↑f ⊆ U x) fun f ↦ support ↑f
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ a, support ↑(f a)
hfin : LocallyFinite fun a ↦ support ↑(f a)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport ↑(f a) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed[inst✝⁴] (V i)
hVf : ∀ (i : ι), V i ⊆ support ↑(f i)
r : ι → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι), V i ⊆ (chartAt H (c i)).source ∩ ↑(extChartAt I (c i)) ⁻¹' Metric.ball (↑(extChartAt I (c i)) (c i)) (r i)
⊢ LocallyFinite fun i ↦ support ↑((f i).updateRIn (r i) ⋯)

Tactic:
simpa only [SmoothBumpFunction.support_updateRIn]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ∞
⊢ ∫ (x : α) in s, f x ∂μ ≤ ∫ (x : α) in s, b ∂μ

Tactic:
refine setIntegral_mono_ae_restrict hf.integrableOn (integrableOn_const mus.ne) ?_

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ∞
⊢ f ≤ᵐ[μ.restrict s] fun x ↦ b
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: case neg
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 : ℕ∞
s : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∉ s
c : M
Hx : x ∉ tsupport ⇑(f c)
this : x ∉ support ⇑(f c)
⊢ (f c) x * g c (↑(chartAt H c) x) = 0

Tactic:
notMem_support

Goal state after:
case neg
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 : ℕ∞
s : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∉ s
c : M
Hx : x ∉ tsupport ⇑(f c)
this : (f c) x = 0
⊢ (f c) x * g c (↑(chartAt H c) x) = 0
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : AEFinStronglyMeasurable f μ
⊢ f =ᵐ[μ] 0

Tactic:
by
  let t := hf.sigmaFiniteSet
  suffices f =ᵐ[μ.restrict t] 0 from
    ae_of_ae_restrict_of_ae_restrict_compl _ this hf.ae_eq_zero_compl
  have : SigmaFinite (μ.restrict t) := hf.sigmaFinite_restrict
  refine ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite ?_ ?_
  · intro s hs hμs
    rw [IntegrableOn, Measure.restrict_restrict hs]
    rw [Measure.restrict_apply hs] at hμs
    exact hf_int_finite _ (hs.inter hf.measurableSet) hμs
  · intro s hs hμs
    rw [Measure.restrict_restrict hs]
    rw [Measure.restrict_apply hs] at hμs
    exact hf_zero _ (hs.inter hf.measurableSet) hμs

Goal state after:
Module: Mathlib.Analysis.Calculus.TangentCone.Seq

Goal state before:
pp: case mp.inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x y : E
hy₀ : y ≠ 0
c : ℕ → 𝕜
d : ℕ → E
hds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hd₀' : ∀ᶠ (n : ℕ) in atTop, d n ≠ 0
hd₀ : Tendsto (fun x ↦ ‖d x‖) atTop (𝓝 0)
hcd : Tendsto (fun x ↦ ‖c x‖ / ‖d x‖⁻¹) atTop (𝓝 ‖y‖)
⊢ Tendsto (fun x ↦ ‖d x‖⁻¹) atTop (𝓝[>] 0)⁻¹

Tactic:
← Filter.comap_inv,

Goal state after:
case mp.inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x y : E
hy₀ : y ≠ 0
c : ℕ → 𝕜
d : ℕ → E
hds : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s
hd₀' : ∀ᶠ (n : ℕ) in atTop, d n ≠ 0
hd₀ : Tendsto (fun x ↦ ‖d x‖) atTop (𝓝 0)
hcd : Tendsto (fun x ↦ ‖c x‖ / ‖d x‖⁻¹) atTop (𝓝 ‖y‖)
⊢ Tendsto (fun x ↦ ‖d x‖⁻¹) atTop (comap Inv.inv (𝓝[>] 0))
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
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) μ
S1 : ∫ (x : E), lineDeriv ℝ f x (∑ i ∈ s, a i • v i) * g x ∂μ = ∑ i ∈ s, a i * ∫ (x : E), lineDeriv ℝ f x (v i) * g x ∂μ
⊢ ∫ (x : E), g x * lineDeriv ℝ f x (∑ i ∈ s, a i • v i) ∂μ =
    ∑ x ∈ s, ∫ (a_1 : E), a x * (g a_1 * lineDeriv ℝ f a_1 (v x)) ∂μ

Tactic:
integral_const_mul,

Goal state after:
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) μ
S1 : ∫ (x : E), lineDeriv ℝ f x (∑ i ∈ s, a i • v i) * g x ∂μ = ∑ i ∈ s, a i * ∫ (x : E), lineDeriv ℝ f x (v i) * g x ∂μ
⊢ ∫ (x : E), g x * lineDeriv ℝ f x (∑ i ∈ s, a i • v i) ∂μ = ∑ x ∈ s, a x * ∫ (a : E), g a * lineDeriv ℝ f a (v x) ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : ℝ → ℝ := fun x ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
G : ℝ → ℝ → ℝ := fun c x ↦ slope g x (x + c)
G_integrable : ∀ (n : ℕ), Integrable (G (↑n)⁻¹) (volume.restrict (Icc a b))
n : ℕ
⊢ ∫ (x : ℝ) in Icc a b, G (↑n)⁻¹ x ≤ g b - g a

Tactic:
integral_Icc_eq_integral_Ioc,

Goal state after:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : ℝ → ℝ := fun x ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
G : ℝ → ℝ → ℝ := fun c x ↦ slope g x (x + c)
G_integrable : ∀ (n : ℕ), Integrable (G (↑n)⁻¹) (volume.restrict (Icc a b))
n : ℕ
⊢ ∫ (t : ℝ) in Ioc a b, G (↑n)⁻¹ t ≤ g b - g a
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:
pp: case right
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (uIcc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
hG'₀ : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤
integrable_f_deriv : Integrable (deriv f) (volume.restrict (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ}, x ∈ Ioo a b → 0 ≤ deriv f x
ebound : ∫ (x : ℝ) in Icc a b, ‖deriv f x‖ ∂volume ≤ f b - f a
⊢ ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a

Tactic:
integral_Icc_eq_integral_Ioc,

Goal state after:
case right
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (uIcc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
hG'₀ : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤
integrable_f_deriv : Integrable (deriv f) (volume.restrict (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ}, x ∈ Ioo a b → 0 ≤ deriv f x
ebound : ∫ (t : ℝ) in Ioc a b, ‖deriv f t‖ ∂volume ≤ f b - f a
⊢ ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ x : ℝ
⊢ (PolynomialModule.eval x) (taylorWithin f n s x₀) +
      (PolynomialModule.eval x)
        ((PolynomialModule.comp (Polynomial.X - Polynomial.C x₀))
          (PolynomialModule.single ℝ (n + 1) (taylorCoeffWithin f (n + 1) s x₀))) =
    (PolynomialModule.eval x) (taylorWithin f n s x₀) +
      (((↑n + 1) * ↑n !)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀

Tactic:
PolynomialModule.comp_eval

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ x : ℝ
⊢ (PolynomialModule.eval x) (taylorWithin f n s x₀) +
      (PolynomialModule.eval (Polynomial.eval x (Polynomial.X - Polynomial.C x₀)))
        (PolynomialModule.single ℝ (n + 1) (taylorCoeffWithin f (n + 1) s x₀)) =
    (PolynomialModule.eval x) (taylorWithin f n s x₀) +
      (((↑n + 1) * ↑n !)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: t x : ℝ
n : ℕ
⊢ HasDerivAt (fun y ↦ (-y + x) ^ (n + 1)) (-(↑n + 1) * (-t + x) ^ n) t

Tactic:
← neg_one_mul,

Goal state after:
t x : ℝ
n : ℕ
⊢ HasDerivAt (fun y ↦ (-y + x) ^ (n + 1)) (-1 * (↑n + 1) * (-t + x) ^ n) t
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: t x : ℝ
n : ℕ
⊢ HasDerivAt (fun y ↦ (-y + x) ^ (n + 1)) (-1 * (↑n + 1) * (-t + x) ^ n) t

Tactic:
mul_comm (-1 : ℝ),

Goal state after:
t x : ℝ
n : ℕ
⊢ HasDerivAt (fun y ↦ (-y + x) ^ (n + 1)) ((↑n + 1) * -1 * (-t + x) ^ n) t
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: t x : ℝ
n : ℕ
⊢ HasDerivAt (fun y ↦ (-y + x) ^ (n + 1)) ((↑n + 1) * (-1 * (-t + x) ^ n)) t

Tactic:
mul_comm (-1 : ℝ),

Goal state after:
t x : ℝ
n : ℕ
⊢ HasDerivAt (fun y ↦ (-y + x) ^ (n + 1)) ((↑n + 1) * ((-t + x) ^ n * -1)) t
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: f : ℝ → ℝ
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hf : ContDiffOn ℝ (↑n) f s
x : ℝ
⊢ (f x - taylorWithinEval f n s x₀ x) / (x - x₀) ^ n = ((x - x₀) ^ n)⁻¹ • (f x - taylorWithinEval f n s x₀ x)

Tactic:
simp [div_eq_inv_mul]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ray

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y

Tactic:
by
  rw [inv_smul_eq_iff₀, smul_comm, eq_comm, inv_smul_eq_iff₀, sameRay_iff_norm_smul_eq] <;>
    rwa [norm_ne_zero_iff]

Goal state after:
Module: Mathlib.Analysis.Convex.StrictConvexSpace

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ ‖a • x + b • y‖ ≠ 1
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
hne : x ≠ y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hne' : ‖a • x + b • y‖ ≠ 1
⊢ ([x -[ℝ] y] \ sphere 0 1).Nonempty

Tactic:
exact ⟨_, ⟨a, b, ha, hb, hab, rfl⟩, mt mem_sphere_zero_iff_norm.1 hne'⟩

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Convex

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
ε : ℝ
hε : 0 < ε
x : F
hx : ‖x‖ = 1
y : F
hy : ‖y‖ = 1
hxy : ε ≤ ‖x - y‖
⊢ 2 * (1 * 1 + 1 * 1) - ‖x - y‖ ^ 2 ≤ 4 - ε ^ 2

Tactic:
ring_nf

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
ε : ℝ
hε : 0 < ε
x : F
hx : ‖x‖ = 1
y : F
hy : ‖y‖ = 1
hxy : ε ≤ ‖x - y‖
⊢ 4 - ‖x - y‖ ^ 2 ≤ 4 - ε ^ 2
Module: Mathlib.Analysis.Convex.Uniform

Goal state before:
pp: case inl
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : UniformConvexSpace E
ε : ℝ
inst✝ : NormedSpace ℝ E
hε : 0 < ε
r : ℝ
hr : r ≤ 0
⊢ ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ r → ∀ ⦃y : E⦄, ‖y‖ ≤ r → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 * r - δ

Tactic:
exact ⟨1, one_pos, fun x hx y hy h => (hε.not_ge <|
      h.trans <| (norm_sub_le _ _).trans <| add_nonpos (hx.trans hr) (hy.trans hr)).elim⟩

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: ⊢ ContinuousOn (fun x ↦ √x * log x) (Ioi 1)

pp: x : ℝ
hx : x ∈ Ioi 1
⊢ deriv^[2] (fun x ↦ √x * log x) x < 0

Tactic:
· exact continuous_sqrt.continuousOn.mul
      (continuousOn_log.mono fun x hx => ne_of_gt (zero_lt_one.trans hx))

Goal state after:
x : ℝ
hx : x ∈ Ioi 1
⊢ deriv^[2] (fun x ↦ √x * log x) x < 0
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: ⊢ StrictConcaveOn ℝ (Icc 0 π) sin

Tactic:
apply strictConcaveOn_of_deriv2_neg (convex_Icc _ _) continuousOn_sin fun x hx => ?_

Goal state after:
x : ℝ
hx : x ∈ interior (Icc 0 π)
⊢ deriv^[2] sin x < 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: θ : ℂ
⊢ cexp (θ * I - -θ * I) = -1 ↔ cexp (2 * θ * I) = -1

Tactic:
ring_nf

Goal state after:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: case neg
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : f w - f x < deriv f a * (w - x)
hb : f y - f w < deriv f b * (y - w)
⊢ f y - f x < deriv f b * (y - x)

Tactic:
have : deriv f a * (w - x) < deriv f b * (w - x) := by
      apply mul_lt_mul _ le_rfl (sub_pos.2 hxw) _
      · exact hf'_mono ⟨hxa, haw.trans hwy⟩ ⟨hxw.trans hwb, hby⟩ (haw.trans hwb)
      · rw [← hw]
        exact (hf'_mono ⟨hxw, hwy⟩ ⟨hxw.trans hwb, hby⟩ hwb).le

Goal state after:
case neg
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : f w - f x < deriv f a * (w - x)
hb : f y - f w < deriv f b * (y - w)
this : deriv f a * (w - x) < deriv f b * (w - x)
⊢ f y - f x < deriv f b * (y - x)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case a
n : ℕ
a b : ℂ
x : ℕ
hx : x ∈ Finset.range n
⊢ -2 * sin (a / 2) * sin (a * ↑x + b) =
    -2 * sin ((a * (↑x + 1 - 1 / 2) + b + -(a * (↑x - 1 / 2) + b)) / 2) *
      sin ((a * (↑x + 1 - 1 / 2) + b - -(a * (↑x - 1 / 2) + b)) / 2)

Tactic:
ring_nf

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: n : ℕ
a b : ℂ
⊢ -2 * sin ((a * (↑n - 1 / 2) + b + (a * (↑0 - 1 / 2) + b)) / 2) *
      sin ((a * (↑n - 1 / 2) + b - (a * (↑0 - 1 / 2) + b)) / 2) =
    -2 * sin (↑n * a / 2) * sin ((↑n - 1) * a / 2 + b)

Tactic:
ring_nf

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case a
n : ℕ
a b : ℂ
x : ℕ
hx : x ∈ Finset.range n
⊢ 2 * sin (a / 2) * cos (a * ↑x + b) =
    2 * sin ((a * (↑x + 1 - 1 / 2) + b - (a * (↑x - 1 / 2) + b)) / 2) *
      cos ((a * (↑x + 1 - 1 / 2) + b + (a * (↑x - 1 / 2) + b)) / 2)

Tactic:
ring_nf

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: n : ℕ
a b : ℂ
⊢ 2 * sin ((a * (↑n - 1 / 2) + b - (a * (↑0 - 1 / 2) + b)) / 2) *
      cos ((a * (↑n - 1 / 2) + b + (a * (↑0 - 1 / 2) + b)) / 2) =
    2 * sin (↑n * a / 2) * cos ((↑n - 1) * a / 2 + b)

Tactic:
ring_nf

Goal state after:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
this : EqOn (deriv f) f' (interior D)
⊢ ConvexOn ℝ D f

Tactic:
refine convexOn_of_deriv2_nonneg hD hf (fun x hx ↦ (hf' _ hx).differentiableWithinAt) ?_ ?_

Goal state after:
case refine_1
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
this : EqOn (deriv f) f' (interior D)
⊢ DifferentiableOn ℝ (deriv f) (interior D)

case refine_2
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
this : EqOn (deriv f) f' (interior D)
⊢ ∀ x ∈ interior D, 0 ≤ deriv^[2] f x