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

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
L : Filter (E × E)
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L
⊢ HasFDerivAtFilter f^[0] (f' ^ 0) L

Tactic:
exact hasFDerivAtFilter_id L

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

Goal state before:
pp: case e'_11
𝕜 : 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
iso : E ≃L[𝕜] F
f : G → E
x : G
f' : G →L[𝕜] E
H : HasStrictFDerivAt (⇑iso ∘ f) (↑iso ∘SL f') x
z : G
⊢ f z = iso.symm ((⇑iso ∘ f) z)

Tactic:
apply (iso.symm_apply_apply _).symm

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

Goal state before:
pp: case e'_12
𝕜 : 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
iso : E ≃L[𝕜] F
f : G → E
x : G
f' : G →L[𝕜] E
H : HasStrictFDerivAt (⇑iso ∘ f) (↑iso ∘SL f') x
z : G
⊢ f' z = (↑iso.symm ∘SL ↑iso ∘SL f') z

Tactic:
apply (iso.symm_apply_apply _).symm

Goal state after:
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
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
x : E
⊢ fderiv 𝕜 (fun x ↦ ↑L ∘SL f x) x = ↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘SL fderiv 𝕜 f x

Tactic:
change fderiv 𝕜 (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘ f) x = _
  rw [ContinuousLinearEquiv.comp_fderiv]

Goal state after:
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 ι
f : F [⋀^ι]→L[𝕜] G
g dg : E →L[𝕜] F
v : ι → E
a b : ι
heq : v a = v b
hne : a ≠ b
⊢ ∀ x ∈ {a, b}ᶜ, (f fun j ↦ (Function.update (fun x ↦ g) x dg j) (v j)) = 0

Tactic:
simp only [mem_compl, mem_insert, mem_singleton, not_or, and_imp]
        intro i hia hib
        apply f.map_eq_zero_of_eq _ _ hne
        simp [*, Ne.symm]

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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
m : ℕ
hm : ↑m < ↑n
x : E
hx : x ∈ s
⊢ ↑m.succ < ↑n.succ

Tactic:
rw [Nat.cast_lt] at hm ⊢

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
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
m : ℕ
hm : m < n
x : E
hx : x ∈ s
⊢ m.succ < n.succ
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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, (p x 0).curry0 = f x
Hfderiv_zero : ∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x
Htaylor : HasFTaylorSeriesUpToOn (↑n) (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑(m + 1) < ↑n.succ
⊢ ↑m < ↑n

Tactic:
rw [Nat.cast_lt] at hm ⊢

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
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, (p x 0).curry0 = f x
Hfderiv_zero : ∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x
Htaylor : HasFTaylorSeriesUpToOn (↑n) (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s
x : E
hx : x ∈ s
m : ℕ
hm : m + 1 < n.succ
⊢ m < n
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
f : E → F
m n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpTo n f p
hmn : m ≤ n
⊢ HasFTaylorSeriesUpTo m f p

Tactic:
rw [← hasFTaylorSeriesUpToOn_univ_iff] at h ⊢

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
m n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p univ
hmn : m ≤ n
⊢ HasFTaylorSeriesUpToOn m f p univ
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
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
⊢ ‖id (x, x) - (x, x)‖ = 0

Tactic:
_root_.id,

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
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
⊢ ‖(x, x) - (x, x)‖ = 0
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case 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
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
z : E
hz : z ∈ Metric.eball x r
⊢ (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1) = fderiv 𝕜 f z

Tactic:
rw [← h.fderiv_eq, add_sub_cancel]

Goal state after:
case 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
inst✝ : CompleteSpace F
h : HasFPowerSeriesOnBall f p x r
z : E
hz : z ∈ Metric.eball x r
⊢ ↑‖z - x‖₊ < r
Module: Mathlib.Analysis.Calculus.FDeriv.Pow

Goal state before:
pp: 𝕜 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
s : Set 𝔸
x : 𝔸
n : ℕ
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (fun x ↦ x ^ n) s x = ∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 𝔸 <• x ^ i

Tactic:
by
  rw [fderivWithin_fun_pow' hxs n differentiableAt_fun_id.differentiableWithinAt,
    fderivWithin_fun_id hxs]

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst✝¹ : NormedDivisionRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
u : 𝕜 → 𝕜'
v : 𝕜'
⊢ deriv (fun y ↦ u y * v) x = deriv u x * v

Tactic:
by_cases hu : DifferentiableAt 𝕜 u x
  · exact deriv_mul_const hu v
  · rw [deriv_zero_of_not_differentiableAt hu, zero_mul]
    rcases eq_or_ne v 0 with (rfl | hd)
    · simp only [mul_zero, deriv_const]
    · refine deriv_zero_of_not_differentiableAt (mt (fun H => ?_) hu)
      simpa only [mul_inv_cancel_right₀ hd] using H.mul_const v⁻¹

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

Goal state before:
pp: case 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∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
z : E
hz : z ∈ Metric.eball x r
⊢ (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1) = fderiv 𝕜 f z

Tactic:
rw [← h.fderiv_eq, add_sub_cancel]

Goal state after:
case 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∞
n : ℕ
f : E → F
x : E
h : HasFiniteFPowerSeriesOnBall f p x (n + 1) r
z : E
hz : z ∈ Metric.eball x r
⊢ ↑‖z - x‖₊ < r
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case inr.refine_3
𝕜 : 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 ι
i : ι
⊢ f (Function.update x i (y i)) =
    f fun i_1 ↦ Function.update (fun x_1 ↦ x) ((Fintype.equivFinOfCardEq ⋯) i) y ((Fintype.equivFinOfCardEq ⋯) i_1) i_1

Tactic:
Function.update_apply,

Goal state after:
case inr.refine_3
𝕜 : 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 ι
i : ι
⊢ f (Function.update x i (y i)) =
    f fun i_1 ↦ (if (Fintype.equivFinOfCardEq ⋯) i_1 = (Fintype.equivFinOfCardEq ⋯) i then y else x) i_1
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case pos
𝕜 : 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
e : Fin n.succ ↪ ι
k : ι
hke : k ∈ range ⇑e
⊢ (if h : k ∈ range ⇑e then Fin.cons v m (e.toEquivRange.symm ⟨k, ⋯⟩) k else x k) =
    if h : k ∈ range ⇑((Equiv.embeddingFinSucc n ι) e).fst then
      m (((Equiv.embeddingFinSucc n ι) e).fst.toEquivRange.symm ⟨k, h⟩) k
    else
      Function.update ((Pi.compRightL 𝕜 E Subtype.val) x) ((Equiv.embeddingFinSucc n ι) e).snd
        (v ↑((Equiv.embeddingFinSucc n ι) e).snd) ⟨k, h⟩

Tactic:
simp only [hke, ↓reduceDIte]
      split_ifs with hkf
      · simp only [← Equiv.succ_embeddingFinSucc_fst_symm_apply e hkf hke, Fin.cons_succ]
      · obtain rfl : k = e 0 := by
          rcases hke with ⟨j, rfl⟩
          simpa using hkf
        simp only [Function.Embedding.toEquivRange_symm_apply_self, Fin.cons_zero, Function.update,
          Pi.compRightL_apply]
        split_ifs with h
        · congr!
        · exfalso
          apply h
          simp_rw [← Equiv.embeddingFinSucc_snd e]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : Finite ι
x : ι → 𝔸
this : Fintype ι
a : ι
l : List ι
IH :
  HasStrictFDerivAt (fun x ↦ (List.map x l).prod)
    (∑ i, (List.map x (List.take (↑i) l)).prod •> (proj l[i] <• (List.map x (List.drop (↑i).succ l)).prod)) x
⊢ (proj a) x •> ∑ i, (List.map x (List.take (↑i) l)).prod •> (proj l[i] <• (List.map x (List.drop (↑i).succ l)).prod) +
      proj a <• (List.map x l).prod =
    ∑ i,
      (List.map x (List.take (↑i) (a :: l))).prod •>
        (proj (a :: l)[i] <• (List.map x (List.drop (↑i).succ (a :: l))).prod)

Tactic:
ext; simp [Fin.sum_univ_succ, Finset.mul_sum, mul_assoc, add_comm]

Goal state after:
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
⊢ (∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z) ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = g z

Tactic:
simpa [sub_eq_zero] using frequently_zero_iff_eventually_zero (hf.sub hg)

Goal state after:
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
⊢ (∀ᶠ (x : 𝕜) in codiscreteWithin U, (f - g) x ≠ 0) → ∀ᶠ (x : 𝕜) in codiscreteWithin U, f x ≠ g x

Tactic:
simp only [Pi.sub_apply, ne_eq, sub_eq_zero, imp_self]

Goal state after:
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
hs : s ∈ 𝓝[≠] f x
this : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s
h : ¬f ⁻¹' s ∈ 𝓝[≠] x
z : 𝕜
⊢ (f z ∈ s → False) ∧ f z ∈ insert (f x) s → f z = f x

Tactic:
⟨h₁z, h₂z⟩

Goal state after:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
s : Set E
hfx : AnalyticAt 𝕜 f x
hs : s ∈ 𝓝[≠] f x
this : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s
h : ¬f ⁻¹' s ∈ 𝓝[≠] x
z : 𝕜
h₁z : f z ∈ s → False
h₂z : f z ∈ insert (f x) s
⊢ f z = f x
Module: Mathlib.Analysis.Calculus.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℤ
⊢ logDeriv (fun x ↦ x ^ n) x = ↑n / x

Tactic:
rw [logDeriv_fun_zpow (by fun_prop), logDeriv_id', mul_one_div]

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

Goal state before:
pp: 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 x ≤ B x + r * (x - a)

Tactic:
apply image_le_of_liminf_slope_right_lt_deriv_boundary' hf bound
    · rwa [sub_self, mul_zero, add_zero]
    · exact hB.add (continuousOn_const.mul (continuousOn_id.sub continuousOn_const))
    · intro x hx
      exact (hB' x hx).add (((hasDerivWithinAt_id x (Ici x)).sub_const a).const_mul r)
    · intro x _ _
      rw [mul_one]
      exact (lt_add_iff_pos_right _).2 hr
    exact hx

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

Goal state before:
pp: 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
Hr : ∀ x ∈ Icc a b, ∀ r > 0, f x ≤ B x + r * (x - a)
x : ℝ
hx : x ∈ Icc a b
this : ContinuousWithinAt (fun r ↦ B x + r * (x - a)) (Ioi 0) 0
⊢ f x ≤ B x

Tactic:
convert! continuousWithinAt_const.closure_le _ this (Hr x hx) using 1

Goal state after:
case e'_4
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
Hr : ∀ x ∈ Icc a b, ∀ r > 0, f x ≤ B x + r * (x - a)
x : ℝ
hx : x ∈ Icc a b
this : ContinuousWithinAt (fun r ↦ B x + r * (x - a)) (Ioi 0) 0
⊢ B x = B x + 0 * (x - a)

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
Hr : ∀ x ∈ Icc a b, ∀ r > 0, f x ≤ B x + r * (x - a)
x : ℝ
hx : x ∈ Icc a b
this : ContinuousWithinAt (fun r ↦ B x + r * (x - a)) (Ioi 0) 0
⊢ 0 ∈ closure (Ioi 0)
Module: Mathlib.Analysis.Calculus.MeanValue

Goal state before:
pp: 𝕜 : Type u_3
G : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → G
hf : Differentiable 𝕜 f
hf' : ∀ (x : E), fderiv 𝕜 f x = 0
x y : E
⊢ f x = f y

Tactic:
by
  let : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
  let A : NormedSpace ℝ E := .restrictScalars ℝ 𝕜 E
  exact convex_univ.is_const_of_fderivWithin_eq_zero hf.differentiableOn
    (fun x _ => by rw [fderivWithin_univ]; exact hf' x) trivial trivial

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

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf' : f' =o[𝓝[s] x₀] fun x ↦ (x - x₀) ^ n
h : (fun x ↦ f x - f x₀) =o[𝓝[s] x₀] fun x ↦ ‖x - x₀‖ ^ (n + 1)
⊢ (fun x ↦ f x - f x₀) =o[𝓝[s] x₀] fun x ↦ (x - x₀) ^ (n + 1)

pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf' : f' =o[𝓝[s] x₀] fun x ↦ (x - x₀) ^ n
⊢ (fun x ↦ toSpanSingleton ℝ (f' x)) =o[𝓝[s] x₀] fun x ↦ ‖x - x₀‖ ^ n

Tactic:
· rw [Asymptotics.isLittleO_iff] at h ⊢
    simpa using h

Goal state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf' : f' =o[𝓝[s] x₀] fun x ↦ (x - x₀) ^ n
⊢ (fun x ↦ toSpanSingleton ℝ (f' x)) =o[𝓝[s] x₀] fun x ↦ ‖x - x₀‖ ^ n
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
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : UniqueDiffOn 𝕜 t
hmn : m + 1 ≤ n
hx₀ : x₀ ∈ s
hst : s ⊆ g ⁻¹' t
⊢ ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)

Tactic:
rw [insert_eq_self.mpr hx₀]

Goal state after:
𝕜 : 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
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
hg : ContDiffWithinAt 𝕜 m g s x₀
ht : UniqueDiffOn 𝕜 t
hmn : m + 1 ≤ n
hx₀ : x₀ ∈ s
hst : s ⊆ g ⁻¹' t
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
Module: Mathlib.Analysis.Calculus.ContDiff.Comp

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x₀ : E
m n : ℕ∞ω
i : ℕ
hf : ContDiffAt 𝕜 n f x₀
hmn : m + ↑i ≤ n
⊢ ContDiffAt 𝕜 m (iteratedFDeriv 𝕜 i f) x₀

Tactic:
rw [← iteratedFDerivWithin_univ, ← contDiffWithinAt_univ] at *
  exact hf.iteratedFDerivWithin_right uniqueDiffOn_univ hmn trivial

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 : ℕ∞), ContDiffOn 𝕜 (↑n) f s) ↔ ∀ (n : ℕ), ContDiffOn 𝕜 (↑n) f s

Tactic:
refine ⟨fun H n => H n, ?_⟩

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
s : Set E
f : E → F
⊢ (∀ (n : ℕ), ContDiffOn 𝕜 (↑n) f s) → ∀ (n : ℕ∞), ContDiffOn 𝕜 (↑n) f s
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
f : 𝕜 → F
n : ℕ
s t : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ EqOn (iteratedDerivWithin n f s) (iteratedDerivWithin n f t) (s ∩ t)

Tactic:
by
  intro r hr
  rw [iteratedDerivWithin_of_isOpen hs hr.1, iteratedDerivWithin_of_isOpen ht hr.2]

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
n : ℕ∞ω
m : ℕ
h : ContDiffWithinAt 𝕜 n f s x
hmn : ↑m < n
hs : UniqueDiffOn 𝕜 (insert x s)
this : ↑m + 1 ≠ ∞
u : Set E
uo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
t : Set E := insert x s ∩ u
hu : ContDiffOn 𝕜 (↑(m + 1)) f t
A : t =ᶠ[𝓝[≠] x] s
B : iteratedFDerivWithin 𝕜 m f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 m f t
C : DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f t) s x
⊢ DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) s x

Tactic:
exact C.congr_of_eventuallyEq (B.filter_mono inf_le_left) B.self_of_nhds

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

Goal state before:
pp: case pos
𝔸 : Type u_2
inst✝² : Ring 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
h✝ : Nonempty (Algebra ℚ 𝔸)
⊢ (∑' (n : ℕ), (expSeries ℚ 𝔸 n) fun x ↦ 0) = 1

Tactic:
expSeries_apply_zero,

Goal state after:
case pos
𝔸 : Type u_2
inst✝² : Ring 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
h✝ : Nonempty (Algebra ℚ 𝔸)
⊢ ∑' (n : ℕ), Pi.single 0 1 n = 1
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: case inr
𝔸 : Type u_2
inst✝⁵ : Ring 𝔸
inst✝⁴ : TopologicalSpace 𝔸
inst✝³ : IsTopologicalRing 𝔸
inst✝² : T2Space 𝔸
inst✝¹ : StarRing 𝔸
inst✝ : ContinuousStar 𝔸
x : 𝔸
val✝ : Algebra ℚ 𝔸
⊢ star (exp x) = exp (star x)

Tactic:
· simp_rw [exp_eq_tsum ℚ, ← star_pow, ← star_inv_natCast_smul, ← tsum_star]

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
⊢ HasFDerivAt exp (exp x • 1) x

Tactic:
hasFDerivAt_iff_isLittleO_nhds_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
⊢ (fun h ↦ exp (x + h) - exp x - (exp x • 1) h) =o[𝓝 0] fun h ↦ h