mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : 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
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖
A : (fun z ↦ z - x) =O[𝓝[s] x] fun z ↦ f' (z - x)
⊢ Tendsto f (𝓝[s \ {x}] x) (𝓝[≠] f x)

Tactic:
have : (fun z ↦ f z - f x) ~[𝓝[s] x] fun z ↦ f' (z - x) := h.isLittleO.trans_isBigO A

Goal state after:
𝕜 : 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
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖
A : (fun z ↦ z - x) =O[𝓝[s] x] fun z ↦ f' (z - x)
this : (fun z ↦ f z - f x) ~[𝓝[s] x] fun z ↦ f' (z - x)
⊢ Tendsto f (𝓝[s \ {x}] x) (𝓝[≠] f x)
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f₁ f₂ : F [⋀^ι]→L[𝕜] G
⊢ (f₁ + f₂).fderivCompContinuousLinearMap g = f₁.fderivCompContinuousLinearMap g + f₂.fderivCompContinuousLinearMap g

Tactic:
ext; simp [Finset.sum_add_distrib]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ dist x x = 0

Tactic:
refine induction_on x ?_ ?_
  · refine isClosed_eq ?_ continuous_const
    exact Completion.continuous_dist continuous_id continuous_id
  · intro a
    rw [Completion.dist_eq, dist_self]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) ↔ ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s

Tactic:
by
  constructor
  · /- Start from an entourage `s`. It contains a closed entourage `t`. Its pullback in `α` is an
      entourage, so it contains an `ε`-neighborhood of the diagonal by definition of the entourages
      in metric spaces. Then `t` contains an `ε`-neighborhood of the diagonal in `Completion α`, as
      closed properties pass to the completion. -/
    intro hs
    rcases mem_uniformity_isClosed hs with ⟨t, ht, ⟨tclosed, ts⟩⟩
    have A : { x : α × α | (↑x.1, ↑x.2) ∈ t } ∈ uniformity α :=
      uniformContinuous_def.1 (uniformContinuous_coe α) t ht
    rcases mem_uniformity_dist.1 A with ⟨ε, εpos, hε⟩
    refine ⟨ε, εpos, @fun x y hxy ↦ ?_⟩
    have : ε ≤ dist x y ∨ (x, y) ∈ t := by
      refine induction_on₂ x y ?_ ?_
      · have : { x : Completion α × Completion α | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t } =
               { p : Completion α × Completion α | ε ≤ dist p.1 p.2 } ∪ t := by ext; simp
        rw [this]
        apply IsClosed.union _ tclosed
        exact isClosed_le continuous_const Completion.uniformContinuous_dist.continuous
      · intro x y
        rw [Completion.dist_eq]
        by_cases! h : ε ≤ dist x y
        · exact Or.inl h
        · have Z := hε h
          simp only [Set.mem_ofPred_eq] at Z
          exact Or.inr Z
    simp only [not_le.mpr hxy, false_or] at this
    exact ts this
  · /- Start from a set `s` containing an ε-neighborhood of the diagonal in `Completion α`. To show
        that it is an entourage, we use the fact that `dist` is uniformly continuous on
        `Completion α × Completion α` (this is a general property of the extension of uniformly
        continuous functions). Therefore, the preimage of the ε-neighborhood of the diagonal in ℝ
        is an entourage in `Completion α × Completion α`. Massaging this property, it follows that
        the ε-neighborhood of the diagonal is an entourage in `Completion α`, and therefore this is
        also the case of `s`. -/
    rintro ⟨ε, εpos, hε⟩
    let r : Set (ℝ × ℝ) := { p | dist p.1 p.2 < ε }
    have : r ∈ uniformity ℝ := Metric.dist_mem_uniformity εpos
    have T := uniformContinuous_def.1 (@Completion.uniformContinuous_dist α _) r this
    simp only [uniformity_prod_eq_prod, mem_prod_iff, Filter.mem_map] at T
    rcases T with ⟨t1, ht1, t2, ht2, ht⟩
    refine mem_of_superset ht1 ?_
    have A : ∀ a b : Completion α, (a, b) ∈ t1 → dist a b < ε := by
      intro a b hab
      have : ((a, b), (a, a)) ∈ t1 ×ˢ t2 := ⟨hab, refl_mem_uniformity ht2⟩
      exact lt_of_le_of_lt (le_abs_self _)
        (by simpa [r, Completion.dist_self, Real.dist_eq, Completion.dist_comm] using ht this)
    grind

Goal state after:
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 : Set E
f : E → F
n : ℕ
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s

Tactic:
intro x hx
  rw [← iteratedFDerivWithin_univ]
  exact iteratedFDerivWithin_congr_set (Filter.eventuallyEq_univ.mpr <| hs.mem_nhds hx) n

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

Goal state before:
pp: case succ
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
ih : ∀ (a : 𝕜), iteratedFDerivWithin 𝕜 n (fun x ↦ f (-x)) s a = (-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a)
a : 𝕜
⊢ iteratedFDerivWithin 𝕜 (n + 1) (fun x ↦ f (-x)) s a = (-1) ^ (n + 1) • iteratedFDerivWithin 𝕜 (n + 1) f (-s) (-a)

Tactic:
have ih' : iteratedFDerivWithin 𝕜 n (fun x => f (-x)) s
        = fun a ↦ (-1 : 𝕜) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a) := by
      ext b
      rw [ih b]

Goal state after:
case succ
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ
ih : ∀ (a : 𝕜), iteratedFDerivWithin 𝕜 n (fun x ↦ f (-x)) s a = (-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a)
a : 𝕜
ih' : iteratedFDerivWithin 𝕜 n (fun x ↦ f (-x)) s = fun a ↦ (-1) ^ n • iteratedFDerivWithin 𝕜 n f (-s) (-a)
⊢ iteratedFDerivWithin 𝕜 (n + 1) (fun x ↦ f (-x)) s a = (-1) ^ (n + 1) • iteratedFDerivWithin 𝕜 (n + 1) f (-s) (-a)
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : OpenPartialHomeomorph E F
a : F
i : E ≃L[𝕜] F
h0 : a ∈ f.target
h : AnalyticAt 𝕜 (↑f) (↑f.symm a)
h' : fderiv 𝕜 (↑f) (↑f.symm a) = ↑i
⊢ AnalyticAt 𝕜 (↑f.symm) a

Tactic:
have : a = f (f.symm a) := by simp [h0]
  rw [this]
  exact f.analyticAt_symm' (by simp [h0]) h h'

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

Goal state before:
pp: case inl.refine_2
𝕜 : 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
h : HasFiniteFPowerSeriesOnBall f p x 0 r
n : ℕ
a : Fin n → E
⊢ (continuousMultilinearCurryFin1 𝕜 E F) ((p.changeOriginSeries 1 n) a) = 0

Tactic:
rw [p.changeOriginSeries_finite_of_finite h.finite 1 (Nat.zero_le _)]

Goal state after:
case inl.refine_2
𝕜 : 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
h : HasFiniteFPowerSeriesOnBall f p x 0 r
n : ℕ
a : Fin n → E
⊢ (continuousMultilinearCurryFin1 𝕜 E F) (0 a) = 0
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case right
𝕜 : 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 ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
⊢ Function.Surjective fun x ↦ ⟨{x}ᶜ, ⋯⟩

Tactic:
intro ⟨s, hs⟩

Goal state after:
case right
𝕜 : 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 ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
inst✝ : DecidableEq ι
y : (i : ι) → E i
h✝ : Nonempty ι
s : Finset (Fin (1 + (Fintype.card ι - 1)))
hs : #s = Fintype.card ι - 1
⊢ ∃ a, (fun x ↦ ⟨{x}ᶜ, ⋯⟩) a = ⟨s, hs⟩
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝² : Field k
inst✝¹ : AddCommGroup E
inst✝ : Module k E
f : k → E
x y : k
⊢ slope (-f) x y = (-slope f) x y

Tactic:
exact slope_neg f x y

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

Goal state before:
pp: case fderiv
𝕜 : 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 ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x v : (i : ι) → E i
m : Fin n → (i : ι) → E i
⊢ ((f.iteratedFDeriv n.succ x).curryLeft v) m =
    ((∑ e,
          (f.iteratedFDerivComponent e.toEquivRange).linearDeriv ((Pi.compRightL 𝕜 E Subtype.val) x) ∘SL
            Pi.compRightL 𝕜 E Subtype.val)
        v)
      m

Tactic:
simp only [ContinuousMultilinearMap.iteratedFDeriv, curryLeft_apply, sum_apply,
      iteratedFDerivComponent_apply, Finset.univ_sigma_univ,
      Pi.compRightL_apply, _root_.sum_apply, ContinuousLinearMap.comp_apply, linearDeriv_apply,
      Finset.sum_sigma']

Goal state after:
case fderiv
𝕜 : 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 ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x v : (i : ι) → E i
m : Fin n → (i : ι) → E i
⊢ (∑ x_1, f fun j ↦ if h : j ∈ range ⇑x_1 then Fin.cons v m (x_1.toEquivRange.symm ⟨j, ⋯⟩) j else x j) =
    ∑ x_1,
      f fun j ↦
        if h : j ∈ range ⇑x_1.fst then m (x_1.fst.toEquivRange.symm ⟨j, h⟩) j
        else Function.update ((Pi.compRightL 𝕜 E Subtype.val) x) x_1.snd (v ↑x_1.snd) ⟨j, h⟩
Module: Mathlib.Analysis.Calculus.LogDeriv

Goal state before:
pp: case inr.inr
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hdf : DifferentiableAt 𝕜 f x
n : ℤ
hn : n ≠ 0
hf : f x ≠ 0
⊢ deriv ((fun x ↦ x ^ n) ∘ f) x / f x ^ n = ↑n * logDeriv f x

Tactic:
deriv_comp _ (differentiableAt_zpow.2 <| .inl hf) hdf,

Goal state after:
case inr.inr
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hdf : DifferentiableAt 𝕜 f x
n : ℤ
hn : n ≠ 0
hf : f x ≠ 0
⊢ deriv (fun x ↦ x ^ n) (f x) * deriv f x / f x ^ n = ↑n * logDeriv f x
Module: Mathlib.Analysis.Calculus.MeanValue

Goal state before:
pp: case ha
f : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
B B' : ℝ → ℝ
ha : f a ≤ B a
hB : ContinuousOn B (Icc a b)
hB' : ∀ x ∈ Ico a b, HasDerivWithinAt B (B' x) (Ici x) x
bound : ∀ x ∈ Ico a b, ∀ (r : ℝ), B' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
x : ℝ
hx : x ∈ Icc a b
r : ℝ
hr : r > 0
⊢ f a ≤ B a + r * (a - a)

Tactic:
rwa [sub_self, mul_zero, add_zero]

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
x : E
f' : E → E →L[𝕜] G
hs : Convex ℝ s
f : E → G
hder : ∀ᶠ (y : E) in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y
hcont : ContinuousWithinAt f' s x
K : ℝ≥0
hK : ‖f' x‖₊ < K
⊢ ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
by
  obtain ⟨ε, ε0, hε⟩ : ∃ ε > 0,
      ball x ε ∩ s ⊆ { y | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K } :=
    mem_nhdsWithin_iff.1 (hder.and <| hcont.nnnorm.eventually (gt_mem_nhds hK))
  rw [inter_comm] at hε
  refine ⟨s ∩ ball x ε, inter_mem_nhdsWithin _ (ball_mem_nhds _ ε0), ?_⟩
  exact
    (hs.inter (convex_ball _ _)).lipschitzOnWith_of_nnnorm_hasFDerivWithin_le
      (fun y hy => (hε hy).1.mono inter_subset_left) fun y hy => (hε hy).2.le

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

Goal state before:
pp: case h₁
𝕜 : 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
x : E
n : ℕ∞ω
f : E → F
g : E → G
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
hs : UniqueDiffOn 𝕜 s
ha : x ∈ s
i : ℕ
hi : ↑i ≤ n
x✝ : Fin i → E
⊢ ((ContinuousLinearMap.fst 𝕜 F G).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i (fun x ↦ (f x, g x)) s x))
      x✝ =
    ((ContinuousLinearMap.fst 𝕜 F G).compContinuousMultilinearMap
        ((iteratedFDerivWithin 𝕜 i f s x).prod (iteratedFDerivWithin 𝕜 i g s x)))
      x✝

Tactic:
rw [← ContinuousLinearMap.iteratedFDerivWithin_comp_left _ (hf.prodMk hg) hs ha hi]

Goal state after:
case h₁
𝕜 : 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
x : E
n : ℕ∞ω
f : E → F
g : E → G
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
hs : UniqueDiffOn 𝕜 s
ha : x ∈ s
i : ℕ
hi : ↑i ≤ n
x✝ : Fin i → E
⊢ (iteratedFDerivWithin 𝕜 i (⇑(ContinuousLinearMap.fst 𝕜 F G) ∘ fun x ↦ (f x, g x)) s x) x✝ =
    ((ContinuousLinearMap.fst 𝕜 F G).compContinuousMultilinearMap
        ((iteratedFDerivWithin 𝕜 i f s x).prod (iteratedFDerivWithin 𝕜 i g s x)))
      x✝
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: case h₂
𝕜 : 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
x : E
n : ℕ∞ω
f : E → F
g : E → G
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
hs : UniqueDiffOn 𝕜 s
ha : x ∈ s
i : ℕ
hi : ↑i ≤ n
x✝ : Fin i → E
⊢ ((ContinuousLinearMap.snd 𝕜 F G).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i (fun x ↦ (f x, g x)) s x))
      x✝ =
    ((ContinuousLinearMap.snd 𝕜 F G).compContinuousMultilinearMap
        ((iteratedFDerivWithin 𝕜 i f s x).prod (iteratedFDerivWithin 𝕜 i g s x)))
      x✝

Tactic:
rw [← ContinuousLinearMap.iteratedFDerivWithin_comp_left _ (hf.prodMk hg) hs ha hi]

Goal state after:
case h₂
𝕜 : 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
x : E
n : ℕ∞ω
f : E → F
g : E → G
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
hs : UniqueDiffOn 𝕜 s
ha : x ∈ s
i : ℕ
hi : ↑i ≤ n
x✝ : Fin i → E
⊢ (iteratedFDerivWithin 𝕜 i (⇑(ContinuousLinearMap.snd 𝕜 F G) ∘ fun x ↦ (f x, g x)) s x) x✝ =
    ((ContinuousLinearMap.snd 𝕜 F G).compContinuousMultilinearMap
        ((iteratedFDerivWithin 𝕜 i f s x).prod (iteratedFDerivWithin 𝕜 i g s x)))
      x✝
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 : ℕ∞ω
h : ContDiffWithinAt 𝕜 ω f s x
m : ℕ∞
hmn : ↑m ≤ ω
⊢ ContDiffWithinAt 𝕜 (↑m) f s x

Tactic:
intro k _
      obtain ⟨u, hu, p, hp, -⟩ := h
      exact ⟨u, hu, p, hp.of_le le_top⟩

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

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
s : Set E
n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hn : n ≠ ∞
x₀ : E
hf : ContDiffWithinAt 𝕜 (n + 1) (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 n g s x₀
hgt : t ∈ 𝓝[g '' s] g x₀
⊢ s ⊆ g ⁻¹' g '' s

Tactic:
subset_preimage_image

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

Goal state before:
pp: n : ℕ
c : OrderedFinpartition n
α : Type u_5
inst✝ : CommMonoid α
v : Fin n → α
⊢ ∏ x ∈ Finset.univ.sigma fun m ↦ Finset.univ, v (c.emb x.fst x.snd) = ∏ i, v i

Tactic:
exact Fintype.prod_equiv c.equivSigma _ _ (fun p ↦ rfl)

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

Goal state before:
pp: case refine_2
𝕜 : 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
n : ℕ∞ω
hn : n ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hus : u ⊆ insert x s
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
huf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) s x
hf' : ContDiffWithinAt 𝕜 n f' s x
⊢ ∃ u ∈ 𝓝[insert x s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 n f' u x

Tactic:
exact ⟨u, hu, f_an, f', fun y hy => (huf' y hy).insert'.mono hus, hf'.insert.mono hus⟩

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

Goal state before:
pp: 𝕜 : 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}
⊢ StrictMono fun m ↦
    have this := ⋯;
    (c.emb (Fin.cast this m.succ) ⟨c.partSize (Fin.cast ⋯ m.succ) - 1, ⋯⟩).pred ⋯

Tactic:
by
    intro i j hij
    simp only [pred_lt_pred_iff, Nat.succ_eq_add_one]
    apply c.parts_strictMono (cast_strictMono _ (strictMono_succ hij))

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

Goal state before:
pp: case mp
𝕜 : 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
x : E
n : ℕ
⊢ (∃ u ∈ 𝓝 x,
      (↑n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n) f' u x) →
    ∃ f', (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n) f' x

Tactic:
rintro ⟨u, H, -, f', h_fderiv, h_cont_diff⟩

Goal state after:
case mp
𝕜 : 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
x : E
n : ℕ
u : Set E
H : u ∈ 𝓝 x
f' : E → E →L[𝕜] F
h_fderiv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
h_cont_diff : ContDiffWithinAt 𝕜 (↑n) f' u x
⊢ ∃ f', (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n) f' x
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝔸 : Type u_2
inst✝² : Ring 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
⊢ exp 0 = 1

Tactic:
by
  rw [exp]
  split_ifs
  · simp_rw [expSeries_sum_eq, ← expSeries_apply_eq, expSeries_apply_zero, tsum_pi_single]
  · rfl

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

Goal state before:
pp: ⊢ AnalyticOnNhd ℝ rexp univ

Tactic:
Real.exp_eq_exp_ℝ

Goal state after:
⊢ AnalyticOnNhd ℝ NormedSpace.exp univ
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: case mpr
s : Set ℝ
a : ℝ
h : ∃ᶠ (x : ℝ) in map (fun x ↦ a + x) (𝓝 0), x ∈ Ioi a ∩ s
⊢ ∃ᶠ (t : ℝ) in 𝓝[>] 0, a + t • 1 ∈ s

Tactic:
frequently_map

Goal state after:
case mpr
s : Set ℝ
a : ℝ
h : ∃ᶠ (a_1 : ℝ) in 𝓝 0, a + a_1 ∈ Ioi a ∩ s
⊢ ∃ᶠ (t : ℝ) in 𝓝[>] 0, a + t • 1 ∈ s
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: s : Set ℝ
a : ℝ
⊢ 1 ∈ posTangentConeAt s a ↔ ∃ᶠ (x : ℝ) in 𝓝[>] a, x ∈ s

Tactic:
rw [one_mem_posTangentConeAt_iff_mem_closure, mem_closure_iff_frequently,
    frequently_nhdsWithin_iff, inter_comm]
  simp_rw [mem_inter_iff]

Goal state after:
Module: Mathlib.Topology.ExtendFrom

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst✝²] A
hf : ∀ x ∈ B, ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
⊢ IsClosed[inst✝¹] V' → φ ⁻¹' V' ∈ 𝓝[B] x

Tactic:
V'_closed

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure[inst✝²] A
hf : ∀ x ∈ B, ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed[inst✝¹] V'
⊢ φ ⁻¹' V' ∈ 𝓝[B] x
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : ℕ∞ω
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : E → 𝔸
hf : ContDiff 𝕜 n f
⊢ ContDiff 𝕜 n fun x ↦ f x ^ 0

Tactic:
by simpa using contDiff_const

Goal state after:
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
b : α
la : β
inst✝ : RegularSpace β
x : α
hf : ContinuousOn f (Ioo x b)
ha : Tendsto f (𝓝[>] x) (𝓝 la)
hab : x < b
x_in : x ∈ Ico x b
⊢ Tendsto f (𝓝[Ioo x b] x) (𝓝 la)

Tactic:
simpa [hab]

Goal state after:
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la : β
inst✝ : T2Space β
hab : a < b
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ Tendsto f (𝓝[Ioo a b] a) (𝓝 la)

Tactic:
simpa [hab]

Goal state after:
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
lb : β
inst✝ : T2Space β
hab : a < b
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
⊢ Tendsto f (𝓝[Ioo a b] b) (𝓝 lb)

Tactic:
simpa [hab]

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

Goal state before:
pp: f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff :
  ∀ᶠ (x : ℝ) in 𝓝[>] a,
    slope f a x ∈
      Ioo (derivWithin f (Ioi a) a - 1, derivWithin f (Ioi a) a + 1).1
        (derivWithin f (Ioi a) a - 1, derivWithin f (Ioi a) a + 1).2
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1

Tactic:
filter_upwards [hdiff] with z hz using hz.2

Goal state after: