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

Goal state before:
pp: case ih
α : Type u
β : Type v
inst✝⁵ : PseudoMetricSpace α
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : Zero α
inst✝² : SMul M α
inst✝¹ : PseudoMetricSpace M
inst✝ : IsBoundedSMul M α
c₁ c₂ : M
x : α
⊢ dist (c₁ • ↑x) (c₂ • ↑x) ≤ dist c₁ c₂ * dist (↑x) 0

Tactic:
rw [← coe_smul, ← coe_smul, Completion.dist_eq, ← coe_zero, Completion.dist_eq]
      exact dist_pair_smul c₁ c₂ x

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
x : E
⊢ ftaylorSeriesWithin 𝕜 f (insert x s) = ftaylorSeriesWithin 𝕜 f s

Tactic:
ext y n : 2
  apply iteratedFDerivWithin_insert

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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hs : UniqueDiffOn 𝕜 s
x : E
hmn : ↑0 ≤ n
hx : x ∈ s
⊢ p x 0 = iteratedFDerivWithin 𝕜 0 f s x

Tactic:
h.zero_eq' 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
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
hs : UniqueDiffOn 𝕜 s
x : E
hmn : ↑0 ≤ n
hx : x ∈ s
⊢ (continuousMultilinearCurryFin0 𝕜 E F).symm (f x) = iteratedFDerivWithin 𝕜 0 f s x
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
x : E
n : ℕ
a : E
⊢ iteratedFDerivWithin 𝕜 n (fun z ↦ f (z - a)) s x = iteratedFDerivWithin 𝕜 n f (-a +ᵥ s) (x - a)

Tactic:
simp [iteratedFDerivWithin_comp_sub']

Goal state after:
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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinOnBall f p s x r
f' : E →L[𝕜] F
y : E
hy : ↑‖y‖₊ < r
h'y : x + y ∈ insert x s
hf' : HasFDerivWithinAt f f' (insert x s) (x + y)
hu : UniqueDiffOn 𝕜 (insert x s)
F' : Type v := UniformSpace.Completion F
a : F →L[𝕜] F' := UniformSpace.Completion.toComplL
b : (E →L[𝕜] F) →ₗᵢ[𝕜] E →L[𝕜] F' := UniformSpace.Completion.toComplₗᵢ.postcomp
⊢ HasSum (fun n ↦ (p.derivSeries n) fun x ↦ y) f'

Tactic:
← b.isEmbedding.hasSum_iff

Goal state after:
𝕜 : 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
h : HasFPowerSeriesWithinOnBall f p s x r
f' : E →L[𝕜] F
y : E
hy : ↑‖y‖₊ < r
h'y : x + y ∈ insert x s
hf' : HasFDerivWithinAt f f' (insert x s) (x + y)
hu : UniqueDiffOn 𝕜 (insert x s)
F' : Type v := UniformSpace.Completion F
a : F →L[𝕜] F' := UniformSpace.Completion.toComplL
b : (E →L[𝕜] F) →ₗᵢ[𝕜] E →L[𝕜] F' := UniformSpace.Completion.toComplₗᵢ.postcomp
⊢ HasSum (⇑b ∘ fun n ↦ (p.derivSeries n) fun x ↦ y) (b f')
Module: Mathlib.Analysis.Calculus.FDeriv.Pow

Goal state before:
pp: 𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedCommRing 𝔸
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
n : ℕ
⊢ ∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • f' = (n • f x ^ (n - 1)) • f'

Tactic:
simp_rw [op_smul_eq_smul, smul_smul, ← pow_add, ← Finset.sum_smul]
  rw [Finset.sum_eq_card_nsmul, Finset.card_range, smul_assoc]
  intro a ha
  congr
  exact add_tsub_cancel_of_le (Nat.le_pred_of_lt <| Finset.mem_range.1 ha)

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

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
⊢ AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 0 f s) s

Tactic:
iteratedFDerivWithin_zero_eq_comp

Goal state after:
case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
⊢ AnalyticOn 𝕜 (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s
Module: Mathlib.Analysis.Complex.ReImTopology

Goal state before:
pp: a : ℝ
⊢ interior {z | a ≤ z.re} = {z | a < z.re}

Tactic:
by
  simpa only [interior_Ici] using! interior_preimage_re (Ici a)

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

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ deriv (fun x ↦ x⁻¹) x = -(x ^ 2)⁻¹

Tactic:
rcases eq_or_ne x 0 with (rfl | hne)
  · rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_inv_iff.1 (not_not.2 rfl))]
    simp
  · exact (hasDerivAt_inv hne).deriv

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivAt c c' x
hx : c x ≠ 0
⊢ HasDerivAt c⁻¹ (-c' / c x ^ 2) x

Tactic:
rw [← hasDerivWithinAt_univ] at *
  exact hc.inv hx

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : 𝕜 → E
f' : E
s : Set 𝕜
x : 𝕜
⊢ HasDerivWithinAt (fun x ↦ f (c * x)) (c • f') s x ↔ HasDerivWithinAt f f' (c • s) (c * x)

Tactic:
simp only [hasDerivWithinAt_iff_hasFDerivWithinAt, ← smul_eq_mul,
    ← hasFDerivWithinAt_comp_smul_smul_iff, ContinuousLinearMap.toSpanSingleton_smul]

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

Goal state before:
pp: case inr
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
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' {f y})
h₂ : Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f ∘ Subtype.val)
h₃ : ¬f x = f y
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
ht' : Subtype.val ⁻¹' t = (f ∘ Subtype.val ⁻¹' {f y})ᶜ
⊢ False

Tactic:
have ht'' : ∀ a ∈ s, a ∈ t ↔ f a ≠ f y := by simpa [Set.ext_iff] using ht'

Goal state after:
case inr
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
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' {f y})
h₂ : Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f ∘ Subtype.val)
h₃ : ¬f x = f y
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
ht' : Subtype.val ⁻¹' t = (f ∘ Subtype.val ⁻¹' {f y})ᶜ
ht'' : ∀ a ∈ s, a ∈ t ↔ f a ≠ f y
⊢ False
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: case zero
𝕜 : 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
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
m : Fin 0 → E
⊢ (iteratedFDerivWithin 𝕜 0 (⇑g ∘ f) s x) m = ((↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 0 f s x)) m

Tactic:
simp only [iteratedFDerivWithin_zero_apply, comp_apply,
      ContinuousLinearMap.compContinuousMultilinearMap_coe, coe_coe]

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
f : E → G
s : Set E
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
this : ∀ᶠ (x : E) in 𝓝[s] x₀, [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
x : E
⊢ ([x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n) → ‖f x - f x₀‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖

Tactic:
⟨h_segment, h⟩

Goal state after:
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
f : E → G
s : Set E
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
c : ℝ
hc : 0 < c
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖x - x₀‖ ^ n
this : ∀ᶠ (x : E) in 𝓝[s] x₀, [x₀ -[ℝ] x] ⊆ s ∧ ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
x : E
h_segment : [x₀ -[ℝ] x] ⊆ s
h : ∀ y ∈ [x₀ -[ℝ] x], ‖f' y‖ ≤ c * ‖x - x₀‖ ^ n
⊢ ‖f x - f x₀‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: case fderivWithin
𝕜 : 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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ∞ω
hf : HasFTaylorSeriesUpToOn n f p s
g : E → G
q : E → FormalMultilinearSeries 𝕜 E G
hg : HasFTaylorSeriesUpToOn n g q s
L : (m : ℕ) → (E [×m]→L[𝕜] F) × (E [×m]→L[𝕜] G) ≃ₗᵢ[𝕜] E [×m]→L[𝕜] F × G :=
  fun m ↦ ContinuousMultilinearMap.prodL 𝕜 (fun x ↦ E) F G
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x ↦ (p x m).prod (q x m)) ((p x m.succ).prod (q x m.succ)).curryLeft s x

Tactic:
convert!
      (L m).hasFDerivAt.comp_hasFDerivWithinAt x
        ((hf.fderivWithin m hm x hx).prodMk (hg.fderivWithin m hm x hx))

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
h : HasDerivAt f f' x
hf' : f' ≠ 0
⊢ Tendsto f (𝓝[≠] x) (𝓝[≠] f x)

Tactic:
simpa only [compl_eq_univ_sdiff] using (hasDerivWithinAt_univ.2 h).tendsto_nhdsWithin_nhdsNE hf'

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y ∈ t
⊢ derivWithin f s x = 0

Tactic:
by
  by_cases hf : DifferentiableWithinAt 𝕜 f s x
  · contrapose! h
    exact hf.hasDerivWithinAt.eventually_notMem h t ht
  · exact derivWithin_zero_of_not_differentiableWithinAt hf

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

Goal state before:
pp: case refine_1.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 ≠ ∞
hf : ContDiffWithinAt 𝕜 (n + 1) f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
huf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
hf' : ContDiffWithinAt 𝕜 n f' u x
w : Set E
hw : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] w
hxw : x ∈ w
hwu : insert x s ∩ w ⊆ u
y : E
hy : y ∈ insert x s ∩ w
⊢ s ∩ w ∈ 𝓝[s] y

Tactic:
exact inter_mem_nhdsWithin _ (hw.mem_nhds hy.2)

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
s : Set E
f : E → F
n : ℕ∞ω
hn : n ≠ ∞
h : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
hf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
vu : v ∈ 𝓝[insert x u] x
v'u : v ⊆ insert x u
hv : ContDiffOn 𝕜 n f' v
xu : x ∈ u
⊢ ∃ u ∈ 𝓝[s] x, (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u

Tactic:
rw [insert_eq_of_mem xu] at vu v'u

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
s : Set E
f : E → F
n : ℕ∞ω
hn : n ≠ ∞
h : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
hf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
vu : v ∈ 𝓝[u] x
v'u : v ⊆ u
hv : ContDiffOn 𝕜 n f' v
xu : x ∈ u
⊢ ∃ u ∈ 𝓝[s] x, (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u
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
x : 𝕜
m : Fin n → 𝕜
⊢ (iteratedFDeriv 𝕜 n f x) m = (∏ i, m i) • iteratedDeriv n f x

Tactic:
by
  rw [iteratedDeriv_eq_iteratedFDeriv, ← ContinuousMultilinearMap.map_smul_univ]; simp

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : Algebra ℚ 𝔸
n : ℕ
c : Fin n → 𝔸
⊢ (expSeries 𝕂 𝔸 n) c = (expSeries ℚ 𝔸 n) c

Tactic:
simp [expSeries, inv_natCast_smul_eq 𝕂 ℚ]

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

Goal state before:
pp: case neg.e_6
𝕜 : 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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : ¬m = c.index j
⊢ update v j z ∘ c.emb m = v ∘ c.emb m

Tactic:
apply Function.update_comp_eq_of_notMem_range

Goal state after:
case neg.e_6
𝕜 : 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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : ¬m = c.index j
⊢ j ∉ range (c.emb m)
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: case zero
𝔸 : Type u_1
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
⊢ exp 0 = exp x ^ 0

Tactic:
pow_zero,

Goal state after:
case zero
𝔸 : Type u_1
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
⊢ exp 0 = 1
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: case zero
𝔸 : Type u_1
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
⊢ exp (0 • x) = exp x ^ 0

Tactic:
rw [zero_smul, pow_zero, exp_zero]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
x : E
n✝ : ℕ∞ω
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
n : ℕ∞
h : ∀ (i : ι), ContDiffWithinAt 𝕜 (↑n) (fun x ↦ Φ x i) s x
m : ℕ
hm : ↑m ≤ n
u : ι → Set E
hux : ∀ (i : ι), u i ∈ 𝓝[insert x s] x
p : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
hp : ∀ (i : ι), HasFTaylorSeriesUpToOn (↑m) (fun x ↦ Φ x i) (p i) (u i)
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) Φ p u

Tactic:
exact ⟨⋂ i, u i, Filter.iInter_mem.2 hux, _,
      hasFTaylorSeriesUpToOn_pi.2 fun i => (hp i).mono <| iInter_subset _ _⟩

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
i : ℕ
a : 𝕜
hf : ContDiff 𝕜 (↑i) f
⊢ (iteratedFDeriv 𝕜 i fun z ↦ f (a • z)) = fun x ↦ a ^ i • iteratedFDeriv 𝕜 i f (a • x)

Tactic:
by
  induction i with
  | zero => ext; simp
  | succ i hi =>
    ext v
    rw [iteratedFDeriv_succ_eq_comp_left, iteratedFDeriv_succ_eq_comp_left]
    simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, self_le_add_right, hf.of_le, hi,
      comp_apply, continuousMultilinearCurryLeftEquiv_symm_apply, smul_apply]
    rw [fderiv_fun_const_smul, fderiv_comp_smul, smul_smul, ← pow_succ]
    · simp
    rw [← Function.comp_def (g := (a • ·))]
    apply DifferentiableAt.comp
    · exact hf.contDiffAt.differentiableAt_iteratedFDeriv (Nat.cast_lt.2 i.lt_succ_self)
    · exact differentiableAt_id.const_smul _

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : ℕ∞ω
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f ↦ f ∘SL ↑e.symm
⊢ ContDiffAt 𝕜 n inverse ↑e

Tactic:
let O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (e.symm : F →L[𝕜] E).comp f

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : ℕ∞ω
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f ↦ f ∘SL ↑e.symm
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f ↦ ↑e.symm ∘SL f
⊢ ContDiffAt 𝕜 n inverse ↑e
Module: Mathlib.Topology.Order.Rolle

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a ≠ b
hfc✝ : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 l)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 l)
h : EqOn (extendFrom (uIoo a b) f) f (uIoo a b)
c : X
hc : c ∈ uIoo a b
hfc : IsExtrOn (extendFrom (uIoo a b) f) (uIcc a b) c
⊢ ∃ c ∈ uIoo a b, IsExtrOn f (uIoo a b) c

Tactic:
exact ⟨c, hc, (hfc.on_subset uIoo_subset_uIcc_self).congr h (h hc)⟩

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 : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
hcont_Ioc : ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z
⊢ False

Tactic:
have hcont : ContinuousOn f (Icc a b) := by
        intro z hz
        by_cases hz' : z = a
        · rw [hz']
          exact hcont_at_a.mono Icc_subset_Ici_self
        · exact hcont_Ioc z ⟨lt_of_le_of_ne hz.1 (Ne.symm hz'), hz.2⟩

Goal state after:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
hcont_Ioc : ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z
hcont : ContinuousOn f (Icc a b)
⊢ False
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 : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
hcontra : ∀ᶠ (x : ℝ) in 𝓝[>] a, False
⊢ False

Tactic:
simp [Filter.eventually_false_iff_eq_bot, ← notMem_closure_iff_nhdsWithin_eq_bot] at hcontra

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

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

Tactic:
rw [deriv_eqOn isOpen_interior hf' hx]; exact hf'₀ _ hx

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

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

Tactic:
rw [deriv_eqOn isOpen_interior hf' hx]; exact hf'₀ _ hx

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

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

Tactic:
rw [deriv_eqOn isOpen_interior hf' hx]; exact hf'₀ _ hx

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

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

Tactic:
rw [deriv_eqOn isOpen_interior hf' hx]; exact hf'₀ _ hx

Goal state after: