mathlib-initiative/mathlib-tactics huggingface dataset:
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
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I (n + 1) M
i j : ↑(atlas H M)
h : (((↑i).extend I).symm ≫ (↑j).extend I).source ⊆ range ↑I
x : E
hx : x ∈ (((↑i).extend I).symm ≫ (↑j).extend I).source
⊢ ContDiffWithinAt 𝕜 n (fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I))
    (((↑i).extend I).symm ≫ (↑j).extend I).source x

Tactic:
refine (ContDiffWithinAt.fderivWithin_right ?_ I.uniqueDiffOn le_rfl
    <| h hx).mono h

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I (n + 1) M
i j : ↑(atlas H M)
h : (((↑i).extend I).symm ≫ (↑j).extend I).source ⊆ range ↑I
x : E
hx : x ∈ (((↑i).extend I).symm ≫ (↑j).extend I).source
⊢ ContDiffWithinAt 𝕜 (n + 1) (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I) x
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: case e'_24.e'_19
𝕜 : 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
E' : Type u_5
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝¹² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹¹ : TopologicalSpace M'
inst✝¹⁰ : ChartedSpace H' M'
F : Type u_11
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_12
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
F' : Type u_14
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_15
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
p : M × M'
f : M → N
g : M' → N'
df : TangentSpace I p.1 →L[𝕜] TangentSpace J (f p.1)
hf : HasMFDerivAt% f p.1 df
dg : TangentSpace I' p.2 →L[𝕜] TangentSpace J' (g p.2)
hg : HasMFDerivAt% g p.2 dg
⊢ mfderiv% f p.1 = df

Tactic:
exact hf.mfderiv

Goal state after:
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
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
x : TangentBundle I H
y : ModelProd H E
⊢ ∀ (a b : E) (x : H),
    ↑I x = a →
      ↑I
            ({ toFun := fun x ↦ (x.proj, x.snd), invFun := fun x ↦ ⟨x.1, x.2⟩, left_inv := ⋯, right_inv := ⋯ }
                ⟨(↑(I.prod (PartialEquiv.refl E)).symm (a, b)).1, (↑(I.prod (PartialEquiv.refl E)).symm (a, b)).2⟩).1 =
          a ∧
        ({ toFun := fun x ↦ (x.proj, x.snd), invFun := fun x ↦ ⟨x.1, x.2⟩, left_inv := ⋯, right_inv := ⋯ }
              ⟨(↑(I.prod (PartialEquiv.refl E)).symm (a, b)).1, (↑(I.prod (PartialEquiv.refl E)).symm (a, b)).2⟩).2 =
          b

Tactic:
rintro a b x rfl

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
x✝ : TangentBundle I H
y : ModelProd H E
b : E
x : H
⊢ ↑I
        ({ toFun := fun x ↦ (x.proj, x.snd), invFun := fun x ↦ ⟨x.1, x.2⟩, left_inv := ⋯, right_inv := ⋯ }
            ⟨(↑(I.prod (PartialEquiv.refl E)).symm (↑I x, b)).1,
              (↑(I.prod (PartialEquiv.refl E)).symm (↑I x, b)).2⟩).1 =
      ↑I x ∧
    ({ toFun := fun x ↦ (x.proj, x.snd), invFun := fun x ↦ ⟨x.1, x.2⟩, left_inv := ⋯, right_inv := ⋯ }
          ⟨(↑(I.prod (PartialEquiv.refl E)).symm (↑I x, b)).1, (↑(I.prod (PartialEquiv.refl E)).symm (↑I x, b)).2⟩).2 =
      b
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
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
x : ModelProd H E
y : TangentBundle I H
⊢ ∀ (a b : E) (x : H),
    ↑I x = a →
      ↑I
            ({ toFun := fun x ↦ (x.proj, x.snd), invFun := fun x ↦ ⟨x.1, x.2⟩, left_inv := ⋯, right_inv := ⋯ }
                ⟨(↑(I.prod (PartialEquiv.refl E)).symm (a, b)).1, (↑(I.prod (PartialEquiv.refl E)).symm (a, b)).2⟩).1 =
          a ∧
        ({ toFun := fun x ↦ (x.proj, x.snd), invFun := fun x ↦ ⟨x.1, x.2⟩, left_inv := ⋯, right_inv := ⋯ }
              ⟨(↑(I.prod (PartialEquiv.refl E)).symm (a, b)).1, (↑(I.prod (PartialEquiv.refl E)).symm (a, b)).2⟩).2 =
          b

Tactic:
rintro a b x rfl

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
x✝ : ModelProd H E
y : TangentBundle I H
b : E
x : H
⊢ ↑I
        ({ toFun := fun x ↦ (x.proj, x.snd), invFun := fun x ↦ ⟨x.1, x.2⟩, left_inv := ⋯, right_inv := ⋯ }
            ⟨(↑(I.prod (PartialEquiv.refl E)).symm (↑I x, b)).1,
              (↑(I.prod (PartialEquiv.refl E)).symm (↑I x, b)).2⟩).1 =
      ↑I x ∧
    ({ toFun := fun x ↦ (x.proj, x.snd), invFun := fun x ↦ ⟨x.1, x.2⟩, left_inv := ⋯, right_inv := ⋯ }
          ⟨(↑(I.prod (PartialEquiv.refl E)).symm (↑I x, b)).1, (↑(I.prod (PartialEquiv.refl E)).symm (↑I x, b)).2⟩).2 =
      b
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
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
⊢ ContMDiff I.tangent I.tangent n ⇑(tangentBundleModelSpaceHomeomorph I).symm

Tactic:
apply contMDiff_iff.2 ⟨Homeomorph.continuous _, fun x y ↦ ?_⟩
  apply contDiffOn_id.congr
  simp only [mfld_simps, mem_range, TotalSpace.toProd, Equiv.coe_fn_symm_mk, forall_exists_index,
    Prod.forall, Prod.mk.injEq]
  rintro a b x rfl
  simpa [PartialEquiv.prod] using ⟨rfl, rfl⟩

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential

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
inst✝ : IsManifold I 1 M
hs : UniqueMDiff[s]
x : M
⊢ UniqueMDiff[(extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s]

Tactic:
rw [← PartialEquiv.image_source_inter_eq', inter_comm, extChartAt_source]
  exact (hs.inter (chartAt H x).open_source).image_denseRange'
    (fun y hy ↦ hasMFDerivWithinAt_extChartAt hy.2)
    fun y hy ↦ ((mdifferentiable_chart _).mfderiv_surjective hy.2).denseRange

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential

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
F : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
Z : M → Type u_10
inst✝² : TopologicalSpace (TotalSpace F Z)
inst✝¹ : (b : M) → TopologicalSpace (Z b)
inst✝ : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueMDiffAt[s] p.proj
⊢ (trivializationAt F Z p.proj).baseSet ∈ nhds p.proj

Tactic:
exact (trivializationAt F Z p.proj).open_baseSet.mem_nhds
    (FiberBundle.mem_baseSet_trivializationAt' p.proj)

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

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
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
⊢ dist (↑(extChartAt I c) c) (↑(extChartAt I c) c) < f.rIn

Tactic:
by rw [dist_self]; exact f.rIn_pos

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case pos
ι : 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
h : ∃ v ∈ c, i ∈ v.carrier
⊢ i ∈ h.choose.carrier ↔ i ∈ chainSupCarrier c

pp: case neg
ι : 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
h : ¬∃ v ∈ c, i ∈ v.carrier
⊢ i ∈ ne.some.carrier ↔ i ∈ chainSupCarrier c

Tactic:
· have := h.choose_spec
    exact iff_of_true this.2 (mem_iUnion₂.2 ⟨_, this.1, this.2⟩)

Goal state after:
case neg
ι : 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
h : ¬∃ v ∈ c, i ∈ v.carrier
⊢ i ∈ ne.some.carrier ↔ i ∈ chainSupCarrier c
Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: ι : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
⊢ ParacompactSpace X

Tactic:
by
  refine ⟨fun α s ho hc ↦ ?_⟩
  choose i hi using iUnion_eq_univ_iff.1 hc
  have : ∀ x : X, (𝓝 x).HasBasis (fun t : Set X ↦ (x ∈ t ∧ IsOpen t) ∧ t ⊆ s (i x)) id :=
    fun x : X ↦ (nhds_basis_opens x).restrict_subset (IsOpen.mem_nhds (ho (i x)) (hi x))
  rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis this with
    ⟨β, c, t, hto, htc, htf⟩
  exact ⟨β, t, fun x ↦ (hto x).1.2, htc, htf, fun b ↦ ⟨i <| c b, (hto b).2⟩⟩

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_3
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i
C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun i
⊢ ∀ {i_1 : ι}, i_1 ∈ insert i v.carrier → closure (update v.toFun i vi i_1) ⊆ u i_1

Tactic:
rintro j (rfl | hj)
    · rwa [update_self, ← v.apply_eq hi]
    · rw [update_of_ne (ne_of_mem_of_not_mem hj hi)]
      exact v.closure_subset hj

Goal state after:
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 t : Set M
hs : IsOpen[inst✝⁵] s
ht : IsClosed[inst✝⁵] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑?m.68) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑?m.109) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∉ support f
⊢ 0 < f x + g x

Tactic:
have : 0 < g x := by
        apply lt_of_le_of_ne (g_pos x) (Ne.symm ?_)
        rw [← mem_support, g_supp]
        contrapose xs
        exact h.trans f_supp.symm.subset (by simpa using xs)

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 t : Set M
hs : IsOpen[inst✝⁵] s
ht : IsClosed[inst✝⁵] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑?m.68) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑?m.109) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∉ support f
this : 0 < g x
⊢ 0 < f x + g x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:
pp: 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
x : ℝ
hx : x ∈ Ioo a b
⊢ 0 ≤ deriv f x

Tactic:
rw [← derivWithin_of_mem_nhds (Icc_mem_nhds hx.left hx.right)]

Goal state after:
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
x : ℝ
hx : x ∈ Ioo a b
⊢ 0 ≤ derivWithin f (Icc a b) x
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
⊢ Tendsto ?m.10 (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)

Tactic:
simpa using! hf

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

Goal state before:
pp: F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ AbsolutelyContinuousOnInterval (f - g) a b

Tactic:
simpa [sub_eq_add_neg] using hf.add (hg.neg)

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

Goal state before:
pp: F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
α : M
hf : AbsolutelyContinuousOnInterval f a b
⊢ AbsolutelyContinuousOnInterval (fun x ↦ α • f x) a b

Tactic:
apply squeeze_zero (fun t ↦ ?_) (fun t ↦ ?_) (by simpa using hf.const_mul ‖α‖)
  · exact Finset.sum_nonneg (fun i hi ↦ by positivity)
  · simp [Finset.mul_sum, dist_smul₀]

Goal state after:
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 ⊆ s, q.Finite ∧ sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ

Tactic:
by
    have : sphere 0 1 ⊆ ⋃ y ∈ s, ball y δ := by
      apply hs.trans (fun z hz ↦ ?_)
      obtain ⟨y, ys, hy⟩ : ∃ y ∈ s, dist z y < δ := Metric.mem_closure_iff.1 hz δ δpos
      exact mem_biUnion ys hy
    exact (isCompact_sphere 0 1).elim_finite_subcover_image (fun y _hy ↦ isOpen_ball) this

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

Goal state before:
pp: case zero
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ : ℝ
⊢ taylorWithinEval f 0 s x₀ x₀ = f x₀

Tactic:
exact taylor_within_zero_eval _ _ _ _

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

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x₀ x : ℝ
s : Set ℝ
f : ℝ → E
n : ℕ
this :
  ∀ (i : ℕ) {c : ℝ} {c' : E}, HasDerivAt (fun x ↦ (c * (x - x₀) ^ i) • c') ((c * (↑i * (x - x₀) ^ (i - 1) * 1)) • c') x
⊢ ∑ i ∈ Finset.range (n + 1 + 1), ((↑i !)⁻¹ * (↑i * (x - x₀) ^ (i - 1) * 1)) • iteratedDerivWithin i f s x₀ =
    ∑ k ∈ Finset.range (n + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k (derivWithin f s) s x₀

Tactic:
Finset.sum_range_succ',

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x₀ x : ℝ
s : Set ℝ
f : ℝ → E
n : ℕ
this :
  ∀ (i : ℕ) {c : ℝ} {c' : E}, HasDerivAt (fun x ↦ (c * (x - x₀) ^ i) • c') ((c * (↑i * (x - x₀) ^ (i - 1) * 1)) • c') x
⊢ ∑ k ∈ Finset.range (n + 1),
        ((↑(k + 1)!)⁻¹ * (↑(k + 1) * (x - x₀) ^ (k + 1 - 1) * 1)) • iteratedDerivWithin (k + 1) f s x₀ +
      ((↑0!)⁻¹ * (↑0 * (x - x₀) ^ (0 - 1) * 1)) • iteratedDerivWithin 0 f s x₀ =
    ∑ k ∈ Finset.range (n + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k (derivWithin f s) s x₀
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 → ℝ
s : Set E
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzOnWith C f s
g : E → ℝ
g_lip : LipschitzWith C g
hg : EqOn f g s
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
filter_upwards [g_lip.ae_differentiableAt_of_real] with x hx xs

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
s : Set E
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzOnWith C f s
g : E → ℝ
g_lip : LipschitzWith C g
hg : EqOn f g s
x : E
hx : DifferentiableAt ℝ g x
xs : x ∈ s
⊢ DifferentiableWithinAt ℝ f s x
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
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : μ.IsAddHaarMeasure
ι : Type u_3
inst✝ : Fintype ι
f : E → ι → ℝ
s : Set E
hf : LipschitzOnWith C f s
A : ∀ (i : ι), LipschitzWith 1 fun x ↦ x i
i : ι
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ (fun x ↦ f x i) s x

Tactic:
by
    apply ae_differentiableWithinAt_of_mem_of_real
    exact LipschitzWith.comp_lipschitzOnWith (A i) hf

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

Goal state before:
pp: F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
x y : ℝ
x✝³ : a ≤ x
x✝² : x ≤ y
x✝¹ : y < x + δ
x✝ : y ≤ b
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone ↑p.2
hp₂ : ∀ (i : ℕ), ↑p.2 i ∈ Icc x y
⊢ ∑ i ∈ Finset.range p.1, dist (f (↑p.2 i)) (f (↑p.2 (i + 1))) < 1

Tactic:
apply hδ₂ (p.1, (fun i ↦ (p.2.val i, p.2.val (i + 1))))

Goal state after:
case a
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := ⋯
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
x y : ℝ
x✝³ : a ≤ x
x✝² : x ≤ y
x✝¹ : y < x + δ
x✝ : y ≤ b
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone ↑p.2
hp₂ : ∀ (i : ℕ), ↑p.2 i ∈ Icc x y
⊢ (p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))) ∈ disjWithin a b

case a
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := ⋯
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
x y : ℝ
x✝³ : a ≤ x
x✝² : x ≤ y
x✝¹ : y < x + δ
x✝ : y ≤ b
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone ↑p.2
hp₂ : ∀ (i : ℕ), ↑p.2 i ∈ Icc x y
⊢ ∑ i ∈ Finset.range (p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).1,
      dist ((p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).2 i).1 ((p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).2 i).2 <
    δ
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
g : ℂ → ℂ := fun z ↦ ∑' (n : ℕ), f n * z ^ n
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
⊢ ε / 4 / M * M = ε / 4

Tactic:
div_mul_cancel₀ _ (by linarith only [hM])

Goal state after:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
g : ℂ → ℂ := fun z ↦ ∑' (n : ℕ), f n * z ^ n
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
⊢ ε / 4 = ε / 4
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ 1 - x ^ 2 / 2 < cos x

Tactic:
by
  have := (sin_sq_lt_sq (by positivity)).trans_eq' (sin_sq_eq_half_sub (x / 2))
  ring_nf at this
  linarith

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

Goal state before:
pp: x : ℝ
⊢ arctan (-1) = -(π / 4)

Tactic:
rw [arctan_neg, arctan_one]

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

Goal state before:
pp: x : ℝ
⊢ 0 ≤ arctan x ↔ 0 ≤ x

Tactic:
by
  simpa only [arctan_zero] using arctan_le_arctan_iff (x := 0)

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

Goal state before:
pp: case inr.refine_2
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ ∀ b ∈ slope f y '' {y_1 | y_1 ∈ S ∧ y < y_1}, slope f x y ≤ b

Tactic:
rintro _ ⟨z, ⟨hzs, hyz : y < z⟩, rfl⟩

Goal state after:
case inr.refine_2
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
z : ℝ
hzs : z ∈ S
hyz : y < z
⊢ slope f x y ≤ slope f y z