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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) ↔ ∃ i, s ∈ 𝓟 {p | dist p.1 p.2 < ↑i}

pp: case h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ Directed (fun x1 x2 ↦ x1 ≥ x2) fun ε ↦ 𝓟 {p | dist p.1 p.2 < ↑ε}

Tactic:
· simp [Completion.mem_uniformity_dist, subset_def]

Goal state after:
case h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ Directed (fun x1 x2 ↦ x1 ≥ x2) fun ε ↦ 𝓟 {p | dist p.1 p.2 < ↑ε}
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case neg
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
h :
  HasFTaylorSeriesUpToOn (↑n) f p s ∧
    (∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y n) (p x n.succ).curryLeft s x) ∧ ContinuousOn (fun x ↦ p x (n + 1)) s
m : ℕ
hm : ↑m ≤ ↑n + 1
h' : ¬m ≤ n
⊢ ContinuousOn (fun x ↦ p x m) s

Tactic:
· have : m = n + 1 := le_antisymm (mod_cast hm) (not_le.1 h')
        rw [this]
        exact h.2.2

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: case zero
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
m : Fin (0 + 1) → E
⊢ ((continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm
        (fderivWithin 𝕜 (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s x))
      m =
    (fderivWithin 𝕜 f s x) (m (last 0))

Tactic:
LinearIsometryEquiv.comp_fderivWithin _ (hs x hx)

Goal state after:
case zero
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
m : Fin (0 + 1) → E
⊢ ((continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm
        (↑↑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘SL fderivWithin 𝕜 f s x))
      m =
    (fderivWithin 𝕜 f s x) (m (last 0))
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
n : ℕ
⊢ iteratedFDerivWithin 𝕜 n f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f t

Tactic:
induction n with
  | zero => exact h.mono fun y hy => DFunLike.ext _ _ fun _ => hy
  | succ n ihn =>
    have : fderivWithin 𝕜 _ t =ᶠ[𝓝[s] x] fderivWithin 𝕜 _ t := ihn.fderivWithin' ht
    refine this.mono fun y hy => ?_
    simp only [iteratedFDerivWithin_succ_eq_comp_left, hy, (· ∘ ·)]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy✝ : y ∈ insert x s ∩ Metric.eball x r
Z : DifferentiableWithinAt 𝕜 f (insert y s) y
hy : y ≠ x
⊢ DifferentiableWithinAt 𝕜 f (insert x s ∩ Metric.eball x r) y

Tactic:
· apply (Z.mono (subset_insert _ _)).mono_of_mem_nhdsWithin
    suffices s ∈ 𝓝[insert x s] y from nhdsWithin_mono _ inter_subset_left this
    rw [nhdsWithin_insert_of_ne hy]
    exact self_mem_nhdsWithin

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∉ tsupport u
⊢ HasDerivAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x

Tactic:
have hx : x ∉ tsupport fun x ↦ B (u x) (v x) :=
      mt (closure_mono (fun x ↦ mt fun h ↦ by simp [h]) ·) hxu

Goal state after:
case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : x ∈ tsupport v → HasDerivAt u u' x
hv : x ∈ tsupport u → HasDerivAt v v' x
hxu : x ∉ tsupport u
hx : x ∉ tsupport fun x ↦ (B (u x)) (v x)
⊢ HasDerivAt (fun x ↦ (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
𝕜' : Type u_2
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivAt c c' x
hf : HasDerivAt f f' x
⊢ HasDerivAt (c • f) (c x • f' + c' • f x) x

Tactic:
by
  rw [← hasDerivWithinAt_univ] at *
  exact hc.smul hf

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Pow

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
h : UniqueDiffWithinAt 𝕜 s x
n : ℕ
⊢ derivWithin (fun x ↦ x ^ n) s x = ↑n * x ^ (n - 1)

Tactic:
derivWithin_fun_pow (differentiableWithinAt_fun_id) n,

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
h : UniqueDiffWithinAt 𝕜 s x
n : ℕ
⊢ ↑n * x ^ (n - 1) * derivWithin (fun x ↦ x) s x = ↑n * x ^ (n - 1)
Module: Mathlib.Analysis.Calculus.DiffContOnCl

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
h : DiffContOnCl 𝕜 f (ball x r)
hr : r ≠ 0
⊢ ContinuousOn f (closedBall x r)

Tactic:
rw [← closure_ball x hr]
    exact h.continuousOn

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a : k
⊢ slope f a a = 0

Tactic:
rw [slope, sub_self, inv_zero, zero_smul]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : Fintype ι
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : DecidableEq ι
x : G
f : G → ContinuousMultilinearMap 𝕜 E F
g : (i : ι) → G → E i
f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
g' : (i : ι) → G →L[𝕜] E i
hf : HasFDerivAt f f' x
hg : ∀ (i : ι), HasFDerivAt (g i) (g' i) x
⊢ HasFDerivAt (fun x ↦ (f x) fun x_1 ↦ g x_1 x)
    ((apply 𝕜 E F fun x_1 ↦ g x_1 x) ∘SL f' + ∑ i, (f x).toContinuousLinearMap (fun x_1 ↦ g x_1 x) i ∘SL g' i) x

Tactic:
simp only [← hasFDerivWithinAt_univ] at *

Goal state after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : Fintype ι
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : DecidableEq ι
x : G
f : G → ContinuousMultilinearMap 𝕜 E F
g : (i : ι) → G → E i
f' : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
g' : (i : ι) → G →L[𝕜] E i
hf : HasFDerivWithinAt f f' univ x
hg : ∀ (i : ι), HasFDerivWithinAt (g i) (g' i) univ x
⊢ HasFDerivWithinAt (fun x ↦ (f x) fun x_1 ↦ g x_1 x)
    ((apply 𝕜 E F fun x_1 ↦ g x_1 x) ∘SL f' + ∑ i, (f x).toContinuousLinearMap (fun x_1 ↦ g x_1 x) i ∘SL g' i) univ x
Module: Mathlib.Analysis.Calculus.Deriv.Inv

Goal state before:
pp: case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hx : d x ≠ 0
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x ↦ c x / d x) s x = (derivWithin c s x * d x - c x * derivWithin d s x) / d x ^ 2

Tactic:
exact (hc.hasDerivWithinAt.div hd.hasDerivWithinAt hx).derivWithin hsx

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.ZPow

Goal state before:
pp: case inl
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x ↦ x ^ m) (↑m * x ^ (m - 1)) x
hm : m < 0
⊢ HasStrictDerivAt (fun x ↦ x ^ m) (↑m * x ^ (m - 1)) x

pp: case inr.inl
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x ↦ x ^ m) (↑m * x ^ (m - 1)) x
hm : m = 0
⊢ HasStrictDerivAt (fun x ↦ x ^ m) (↑m * x ^ (m - 1)) x

pp: case inr.inr
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x ↦ x ^ m) (↑m * x ^ (m - 1)) x
hm : 0 < m
⊢ HasStrictDerivAt (fun x ↦ x ^ m) (↑m * x ^ (m - 1)) x

Tactic:
· have hx : x ≠ 0 := h.resolve_right hm.not_ge
    have := (hasStrictDerivAt_inv ?_).scomp _ (this (-m) (neg_pos.2 hm)) <;>
      [skip; exact zpow_ne_zero _ hx]
    simp only [Function.comp_def, zpow_neg, inv_inv, smul_eq_mul] at this
    convert! this using 1
    rw [sq, mul_inv, inv_inv, Int.cast_neg, neg_mul, neg_mul_neg, ← zpow_add₀ hx, mul_assoc, ←
      zpow_add₀ hx]
    congr
    abel

Goal state after:
case inr.inl
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x ↦ x ^ m) (↑m * x ^ (m - 1)) x
hm : m = 0
⊢ HasStrictDerivAt (fun x ↦ x ^ m) (↑m * x ^ (m - 1)) x

case inr.inr
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m
this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x ↦ x ^ m) (↑m * x ^ (m - 1)) x
hm : 0 < m
⊢ HasStrictDerivAt (fun x ↦ x ^ m) (↑m * x ^ (m - 1)) x
Module: Mathlib.Analysis.Calculus.Deriv.ZPow

Goal state before:
pp: case neg
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk : (deriv^[k] fun x ↦ (c * x + d)⁻¹) = fun x ↦ (-1) ^ k * ↑k ! * c ^ k * (c * x + d) ^ (-1 - ↑k)
z : 𝕜
hd : ¬c = 0
this : deriv (fun x ↦ (c * (x + d / c)) ^ (-1 - ↑k)) z = deriv (fun x ↦ (c * x) ^ (-1 - ↑k)) (z + d / c)
h0 : (fun x ↦ (c * (x + d / c)) ^ (-1 - ↑k)) = fun x ↦ (c * x + d) ^ (-1 - ↑k)
⊢ (-1) ^ k * ↑k ! * c ^ k * deriv (fun x ↦ (c * x + d) ^ (-1 - ↑k)) z =
    (-1) ^ (1 + k) * ↑((1 + k) * k !) * c ^ (1 + k) * (c * z + d) ^ (-1 - (1 + ↑k))

Tactic:
rw [h0, deriv_comp_mul_left c (fun x ↦ (x) ^ (-1 - k : ℤ)) (z + d / c)] at this

Goal state after:
case neg
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk : (deriv^[k] fun x ↦ (c * x + d)⁻¹) = fun x ↦ (-1) ^ k * ↑k ! * c ^ k * (c * x + d) ^ (-1 - ↑k)
z : 𝕜
hd : ¬c = 0
this : deriv (fun x ↦ (c * x + d) ^ (-1 - ↑k)) z = c • deriv (fun x ↦ x ^ (-1 - ↑k)) (c * (z + d / c))
h0 : (fun x ↦ (c * (x + d / c)) ^ (-1 - ↑k)) = fun x ↦ (c * x + d) ^ (-1 - ↑k)
⊢ (-1) ^ k * ↑k ! * c ^ k * deriv (fun x ↦ (c * x + d) ^ (-1 - ↑k)) z =
    (-1) ^ (1 + k) * ↑((1 + k) * k !) * c ^ (1 + k) * (c * z + d) ^ (-1 - (1 + ↑k))
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: case zero_eq
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →ᴬ[𝕜] E
A : (m : ℕ) → (E [×m]→L[𝕜] F) → G [×m]→L[𝕜] F := ⋯
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
⊢ ∀ x ∈ ⇑g ⁻¹' s, ((p (g x) 0).compContinuousLinearMap fun x ↦ g.contLinear).curry0 = (f ∘ ⇑g) x

Tactic:
intro x hx
    simp only [(hf.zero_eq (g x) hx).symm, Function.comp_apply]
    change (p (g x) 0 fun _ : Fin 0 => g.contLinear 0) = p (g x) 0 0
    rw [map_zero]
    rfl

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
a : E
hg : ContinuousAt g a
hf : HasFDerivAt f f' (g a)
hf' : Topology.IsEmbedding ⇑f'
hh : HasFDerivAt h (f' ∘SL g') a
hcomp : f ∘ g =ᶠ[𝓝 a] h
⊢ HasFDerivAt g g' a

Tactic:
refine HasFDerivAtFilter.of_comp_of_isEmbedding ?_ hf hf' hh ?_
  · exact hg.tendsto.prodMap (by simp)
  · exact hcomp.prodMap hcomp.self_of_nhds

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
m n : ℕ∞ω
hm : m ≤ n
h' : m = ∞ → n = ω
h : ContDiffWithinAt 𝕜 n f s x
⊢ ∃ u, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u ∧ x ∈ u ∧ ContDiffOn 𝕜 m f (insert x s ∩ u)

Tactic:
rcases eq_or_ne n ω with rfl | hn
  · obtain ⟨t, ht, p, hp, h'p⟩ := h
    rcases mem_nhdsWithin.1 ht with ⟨u, huo, hxu, hut⟩
    rw [inter_comm] at hut
    refine ⟨u, huo, hxu, ?_⟩
    suffices ContDiffOn 𝕜 ω f (insert x s ∩ u) from this.of_le le_top
    intro y hy
    refine ⟨insert x s ∩ u, ?_, p, hp.mono hut, fun i ↦ (h'p i).mono hut⟩
    simp only [insert_eq_of_mem, hy, self_mem_nhdsWithin]
  · match m with
    | ω => simp [hn] at hm
    | ∞ => exact (hn (h' rfl)).elim
    | (m : ℕ) =>
      rcases contDiffWithinAt_nat.1 (h.of_le hm) with ⟨t, ht, p, hp⟩
      rcases mem_nhdsWithin.1 ht with ⟨u, huo, hxu, hut⟩
      rw [inter_comm] at hut
      exact ⟨u, huo, hxu, (hp.mono hut).contDiffOn⟩

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ ‖iteratedFDerivWithin 𝕜 n f s x‖ = ‖iteratedDerivWithin n f s x‖

Tactic:
rw [iteratedDerivWithin_eq_equiv_comp, Function.comp_apply, LinearIsometryEquiv.norm_map]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 (↑n) f s ↔
    (∀ m ≤ n, ContinuousOn (fun x ↦ iteratedFDerivWithin 𝕜 m f s x) s) ∧
      ∀ m < n, DifferentiableOn 𝕜 (fun x ↦ iteratedFDerivWithin 𝕜 m f s x) s

Tactic:
rw [← WithTop.coe_natCast, contDiffOn_iff_continuousOn_differentiableOn hs]
  simp

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case e'_3.inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
j : Fin c.length
hij : c.index 0 < j
A : 1 < c.partSize (c.index 0)
⊢ 1 ≤ ↑(c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩)

Tactic:
rw [Order.one_le_iff_pos]

Goal state after:
case e'_3.inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
j : Fin c.length
hij : c.index 0 < j
A : 1 < c.partSize (c.index 0)
⊢ 0 < ↑(c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩)
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case e'_4.inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i : Fin c.length
hij : i < c.index 0
A : 1 < c.partSize (c.index 0)
⊢ 1 ≤ ↑(c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩)

Tactic:
rw [Order.one_le_iff_pos]

Goal state after:
case e'_4.inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i : Fin c.length
hij : i < c.index 0
A : 1 < c.partSize (c.index 0)
⊢ 0 < ↑(c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩)
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
m : ℕ
x : E
h : ContDiffAt 𝕜 n f x
hmn : ↑m < n
⊢ DifferentiableAt 𝕜 (iteratedFDeriv 𝕜 m f) x

Tactic:
← differentiableWithinAt_univ

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
m : ℕ
x : E
h : ContDiffAt 𝕜 n f x
hmn : ↑m < n
⊢ DifferentiableWithinAt 𝕜 (iteratedFDeriv 𝕜 m f) univ x
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: case inl
𝔸 : Type u_2
inst✝³ : Ring 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x : 𝔸
h : IsEmpty (Algebra ℚ 𝔸)
⊢ exp (MulOpposite.op x) = MulOpposite.op (exp x)

pp: case inr
𝔸 : Type u_2
inst✝³ : Ring 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x : 𝔸
val✝ : Algebra ℚ 𝔸
⊢ exp (MulOpposite.op x) = MulOpposite.op (exp x)

Tactic:
· have : IsEmpty (Algebra ℚ 𝔸ᵐᵒᵖ) := ⟨fun _ => h.elim <| (RingEquiv.opOp 𝔸).algebra ℚ⟩
    simp

Goal state after:
case inr
𝔸 : Type u_2
inst✝³ : Ring 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x : 𝔸
val✝ : Algebra ℚ 𝔸
⊢ exp (MulOpposite.op x) = MulOpposite.op (exp x)
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝔸 : Type u_1
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra ℚ 𝔸
inst✝² : CompleteSpace 𝔸
inst✝¹ : StarRing 𝔸
inst✝ : ContinuousStar 𝔸
x : 𝔸
h : x ∈ skewAdjoint 𝔸
⊢ exp (-x + x) = 1 ∧ exp x * exp (-x) = 1

Tactic:
← exp_add_of_commute (Commute.refl x).neg_right,

Goal state after:
𝔸 : Type u_1
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra ℚ 𝔸
inst✝² : CompleteSpace 𝔸
inst✝¹ : StarRing 𝔸
inst✝ : ContinuousStar 𝔸
x : 𝔸
h : x ∈ skewAdjoint 𝔸
⊢ exp (-x + x) = 1 ∧ exp (x + -x) = 1
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝔸 : Type u_1
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra ℚ 𝔸
inst✝² : CompleteSpace 𝔸
inst✝¹ : StarRing 𝔸
inst✝ : ContinuousStar 𝔸
x : 𝔸
h : x ∈ skewAdjoint 𝔸
⊢ exp 0 = 1 ∧ exp 0 = 1

Tactic:
exp_zero,

Goal state after:
𝔸 : Type u_1
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra ℚ 𝔸
inst✝² : CompleteSpace 𝔸
inst✝¹ : StarRing 𝔸
inst✝ : ContinuousStar 𝔸
x : 𝔸
h : x ∈ skewAdjoint 𝔸
⊢ 1 = 1 ∧ 1 = 1
Module: Mathlib.Topology.MetricSpace.CauSeqFilter

Goal state before:
pp: β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → f.lim ∈ s → ↑f ⁻¹' s ∈ atTop

Tactic:
os

Goal state after:
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ f.lim ∈ s → ↑f ⁻¹' s ∈ atTop
Module: Mathlib.Topology.MetricSpace.CauSeqFilter

Goal state before:
pp: β : Type v
inst✝ : NormedField β
f : CauSeq β norm
⊢ CauchySeq ↑f

Tactic:
refine cauchy_iff.2 ⟨by infer_instance, fun s hs => ?_⟩
  rcases mem_uniformity_dist.1 hs with ⟨ε, ⟨hε, hεs⟩⟩
  obtain ⟨N, hN⟩ := CauSeq.cauchy₂ f hε
  exists { n | n ≥ N }.image f
  simp only [mem_atTop_sets, mem_map]
  constructor
  · exists N
    intro b hb
    exists b
  · rintro ⟨a, b⟩ ⟨⟨a', ⟨ha'1, ha'2⟩⟩, ⟨b', ⟨hb'1, hb'2⟩⟩⟩
    dsimp at ha'1 ha'2 hb'1 hb'2
    rw [← ha'2, ← hb'2]
    apply hεs
    rw [dist_eq_norm]
    apply hN <;> assumption

Goal state after:
Module: Mathlib.Topology.MetricSpace.CauSeqFilter

Goal state before:
pp: β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
ε : ℝ
εpos : ε > 0
N : ℕ
hN : ∀ j ≥ N, ‖↑(⟨u, C⟩ - CauSeq.const norm (CauSeq.lim ⟨u, C⟩)) j‖ < ε
⊢ ∀ n ≥ N, dist (u n) (CauSeq.lim ⟨u, C⟩) < ε

Tactic:
simpa [dist_eq_norm] using hN

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
a✝ : 𝔸
hh : a✝ ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ exp x * (exp (0 + a✝) - exp 0 - (ContinuousLinearMap.id 𝕂 𝔸) a✝) =
    exp x * exp a✝ - exp x - exp x • (ContinuousLinearMap.id 𝕂 𝔸) a✝

Tactic:
exp_zero,

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
this : ∀ᶠ (h : 𝔸) in 𝓝 0, h ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
a✝ : 𝔸
hh : a✝ ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ exp x * (exp (0 + a✝) - 1 - (ContinuousLinearMap.id 𝕂 𝔸) a✝) =
    exp x * exp a✝ - exp x - exp x • (ContinuousLinearMap.id 𝕂 𝔸) a✝