mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
⊢ derivWithin f s x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(Submodule.span 𝕜 (f '' t))

Tactic:
by_cases H : UniqueDiffWithinAt 𝕜 s x

Goal state after:
case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin f s x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(Submodule.span 𝕜 (f '' t))

case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin f s x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(Submodule.span 𝕜 (f '' t))
Module: Mathlib.Analysis.Calculus.FDeriv.Mul

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
𝕜' : Type u_5
inst✝⁴ : NormedRing 𝕜'
inst✝³ : NormedAlgebra 𝕜 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : IsBoundedSMul 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
c' : E →L[𝕜] 𝕜'
hc : HasFDerivAt c c' x
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (c • f) (c x • f' + c'.smulRight (f x)) x

Tactic:
by
  -- `by exact` to solve unification issues.
  exact (isBoundedBilinearMap_smul.hasFDerivAt (𝕜 := 𝕜) (c x, f x)).comp x <| hc.prodMk hf

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

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m ↦ z ^ m • a (m + n)) t

Tactic:
by_cases h : z = 0

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : z = 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m ↦ z ^ m • a (m + n)) t

case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m ↦ z ^ m • a (m + n)) t
Module: Mathlib.Analysis.Calculus.Deriv.Inv

Goal state before:
pp: 𝕜 : 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
⊢ 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:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x
  · exact (hc.hasDerivWithinAt.div hd.hasDerivWithinAt hx).derivWithin hsx
  · simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
x : E
hg : ∀ i ∈ u, HasFDerivWithinAt (g i) (g' i) s x
⊢ HasFDerivWithinAt (fun x ↦ ∏ i ∈ u, g i x) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) •> g' i) s x

Tactic:
by
  simpa [← Finset.prod_attach u] using .congr_fderiv
    (hasFDerivAt_finsetProd.comp_hasFDerivWithinAt x <|
      hasFDerivWithinAt_pi.mpr fun i ↦ hg (Subtype.val i) i.prop :)
    (by ext; simp [Finset.prod_erase_attach (g · x), ← u.sum_attach])

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
g : ℝ → E
fdiff : DifferentiableOn ℝ f (Icc a b)
gdiff : DifferentiableOn ℝ g (Icc a b)
hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)
hi : f a = g a
⊢ ∀ y ∈ Icc a b, f y = g y

Tactic:
have A : ∀ y ∈ Ico a b, HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y := fun y hy =>
    (fdiff y (mem_Icc_of_Ico hy)).hasDerivWithinAt.mono_of_mem_nhdsWithin
    (Icc_mem_nhdsGE_of_mem hy)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
g : ℝ → E
fdiff : DifferentiableOn ℝ f (Icc a b)
gdiff : DifferentiableOn ℝ g (Icc a b)
hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)
hi : f a = g a
A : ∀ y ∈ Ico a b, HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y
⊢ ∀ y ∈ Icc a b, f y = g y
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: case succ
𝕜 : 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
c : F
s : Set E
n : ℕ
hn : n + 1 ≠ 0
⊢ iteratedFDerivWithin 𝕜 (n + 1) (fun x ↦ c) s = 0

Tactic:
exact iteratedFDerivWithin_succ_const n c

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

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
f : E → F
x : E
n : ℕ∞ω
g : F →L[𝕜] G
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (fun x ↦ ((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 (fun x ↦ E) F G) g) (p x i)) u

Tactic:
apply AnalyticOnNhd.comp_analyticOn _ (h'p i) (Set.mapsTo_univ _ _)

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
f : E → F
x : E
n : ℕ∞ω
g : F →L[𝕜] G
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u
i : ℕ
⊢ AnalyticOnNhd 𝕜 (⇑((ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 (fun x ↦ E) F G) g)) univ
Module: Mathlib.Analysis.Calculus.MeanValue

Goal state before:
pp: 𝕜 : Type u_3
G : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : 𝕜 → G
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (deriv f) 0 s
x : 𝕜
hx : x ∈ s
⊢ fderiv 𝕜 f x = 0 x

Tactic:
ext; simp [← toSpanSingleton_deriv, hf' hx]

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

Goal state before:
pp: case refine_1
𝕜 : 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
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
a : E
hgc : ContinuousAt g a
hf : HasFDerivAt f f' (g a)
hh : HasFDerivAt h h' a
hcomp : f ∘ g =ᶠ[𝓝 a] h
hf'symm : Function.LeftInverse ⇑f'symm ⇑f'
⊢ Tendsto (Prod.map g g) (𝓝 a ×ˢ pure a) (𝓝 (g a) ×ˢ pure (g a))

pp: case refine_2
𝕜 : 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
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
a : E
hgc : ContinuousAt g a
hf : HasFDerivAt f f' (g a)
hh : HasFDerivAt h h' a
hcomp : f ∘ g =ᶠ[𝓝 a] h
hf'symm : Function.LeftInverse ⇑f'symm ⇑f'
⊢ Prod.map (f ∘ g) (f ∘ g) =ᶠ[𝓝 a ×ˢ pure a] Prod.map h h

Tactic:
· exact hgc.tendsto.prodMap (by simp)

Goal state after:
case refine_2
𝕜 : 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
f' : F →L[𝕜] G
h' : E →L[𝕜] G
f'symm : G →L[𝕜] F
a : E
hgc : ContinuousAt g a
hf : HasFDerivAt f f' (g a)
hh : HasFDerivAt h h' a
hcomp : f ∘ g =ᶠ[𝓝 a] h
hf'symm : Function.LeftInverse ⇑f'symm ⇑f'
⊢ Prod.map (f ∘ g) (f ∘ g) =ᶠ[𝓝 a ×ˢ pure a] Prod.map h h
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs

Goal state before:
pp: 𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
h : AnalyticAt 𝕜 f x
⊢ HasFPowerSeriesAt f (FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial) x

Tactic:
obtain ⟨p, hp⟩ := h

Goal state after:
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
hp : HasFPowerSeriesAt f p x
⊢ HasFPowerSeriesAt f (FormalMultilinearSeries.ofScalars 𝕜 fun n ↦ iteratedDeriv n f x / ↑n.factorial) x
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case mpr
𝕜 : 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✝ : ℕ∞ω
n : ℕ∞
⊢ ContDiff 𝕜 (↑n) f → ContDiffOn 𝕜 (↑n) f univ

Tactic:
· rintro ⟨p, hp⟩ x _ m hm
      exact ⟨univ, Filter.univ_sets _, p,
        (hp.hasFTaylorSeriesUpToOn univ).of_le (mod_cast hm)⟩

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

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : DivisionRing 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
x : 𝔸
n : ℕ
⊢ ((expSeries 𝕂 𝔸 n) fun x_1 ↦ x) = x ^ n / ↑n !

Tactic:
div_eq_mul_inv,

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : DivisionRing 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
x : 𝔸
n : ℕ
⊢ ((expSeries 𝕂 𝔸 n) fun x_1 ↦ x) = x ^ n * (↑n !)⁻¹
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : CompleteSpace 𝔸
inst✝¹ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
inst✝ : Invertible (exp x)
⊢ ⅟(exp x) = exp (-x)

Tactic:
let := invertibleExpOfMemBall hx; convert! (rfl : ⅟(exp x) = _)

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

Goal state before:
pp: case neg.emb.refine_2.inl.inr
𝕜 : 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✝
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
j : Fin (c.partSize (c.index 0))
hj : j ≠ 0
⊢ c.emb (c.index 0) j = cases 0 (succ ∘ fun j ↦ (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯) (Fin.cast ⋯ ⟨↑j, ⋯⟩)

Tactic:
· let j' := Fin.pred (j.cast B.symm) (by simpa using hj)
              have : j = (succ j').cast B := by simp [j']
              simp only [this, val_cast, val_succ, cast_mk, cases_succ', comp_apply, succ_mk,
                succ_pred]
              rfl

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
f g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑n) f s x
hg : ContDiffWithinAt 𝕜 (↑n) g s x
⊢ iteratedDerivWithin n (f - g) s x = iteratedDerivWithin n f s x - iteratedDerivWithin n g s x

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, Pi.neg_def, iteratedDerivWithin_add hx h hf hg.neg,
    iteratedDerivWithin_fun_neg]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
s : Set 𝕜
f : 𝕜 → F
c x : 𝕜
⊢ iteratedDerivWithin n (fun z ↦ f (z + c)) s x = iteratedDerivWithin n f (c +ᵥ s) (x + c)

Tactic:
simp [iteratedDerivWithin, ← iteratedFDerivWithin_comp_add_right n c x]

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

Goal state before:
pp: case refine_3
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
n : ℕ∞ω
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
L : (m : ℕ) → ((i : ι) → E [×m]→L[𝕜] F' i) ≃ₗᵢ[𝕜] E [×m]→L[𝕜] (i : ι) → F' i :=
  fun m ↦ ContinuousMultilinearMap.piₗᵢ 𝕜 fun _i ↦ E
h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
⊢ ∀ (m : ℕ),
    ↑m < n →
      ∀ x ∈ s,
        HasFDerivWithinAt (fun x ↦ ContinuousMultilinearMap.pi fun i ↦ p' i x m)
          (ContinuousMultilinearMap.pi fun i ↦ p' i x m.succ).curryLeft s x

pp: case refine_4
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
n : ℕ∞ω
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
L : (m : ℕ) → ((i : ι) → E [×m]→L[𝕜] F' i) ≃ₗᵢ[𝕜] E [×m]→L[𝕜] (i : ι) → F' i :=
  fun m ↦ ContinuousMultilinearMap.piₗᵢ 𝕜 fun _i ↦ E
h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x ↦ ContinuousMultilinearMap.pi fun i ↦ p' i x m) s

Tactic:
· intro m hm x hx
    exact (L m).hasFDerivAt.comp_hasFDerivWithinAt x <|
      hasFDerivWithinAt_pi.2 fun i => (h i).fderivWithin m hm x hx

Goal state after:
case refine_4
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
n : ℕ∞ω
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
L : (m : ℕ) → ((i : ι) → E [×m]→L[𝕜] F' i) ≃ₗᵢ[𝕜] E [×m]→L[𝕜] (i : ι) → F' i :=
  fun m ↦ ContinuousMultilinearMap.piₗᵢ 𝕜 fun _i ↦ E
h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x ↦ ContinuousMultilinearMap.pi fun i ↦ p' i x m) s
Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv

Goal state before:
pp: n : ℕ
⊢ deriv^[n + 1] cexp = cexp

Tactic:
by rw [iterate_succ_apply, deriv_exp, iter_deriv_exp n]

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

Goal state before:
pp: n : ℕ
⊢ deriv^[n + 1] rexp = rexp

Tactic:
by rw [iterate_succ_apply, deriv_exp, iter_deriv_exp n]

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
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑f.symm a)
n : ℕ
IH : ContDiffAt 𝕜 (↑↑n) (↑f) (↑f.symm a) → ContDiffAt 𝕜 (↑↑n) (↑f.symm) a
hf : ContDiffAt 𝕜 (↑↑n.succ) (↑f) (↑f.symm a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑f.symm a)
u : Set E
hu : u ∈ 𝓝 (↑f.symm a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑f.symm a) = ↑f₀'
h_deriv₁ : ContDiffAt 𝕜 (↑n) inverse (f' (↑f.symm a))
⊢ n ≤ n.succ

Tactic:
exact Nat.le_succ n

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), ↑(f x) ∂μ = ∞
hc : c = 0
⊢ ∃ g,
    (∀ (x : α), (piecewise s hs (const α c) (const α 0)) x ≤ g x) ∧
      LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ + ε

Tactic:
refine ⟨fun _ => 0, ?_, lowerSemicontinuous_const, ?_⟩
      · classical
        simp only [hc, Set.indicator_zero', Pi.zero_apply, SimpleFunc.const_zero, imp_true_iff,
          SimpleFunc.coe_zero, Set.piecewise_eq_indicator,
          SimpleFunc.coe_piecewise, le_zero_iff]
      · simp only [lintegral_const, zero_mul, zero_le, ENNReal.coe_zero]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t ↦ (AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t)) (y - x)) I t
⊢ ∃ t ∈ Ioo 0 1, (f' (g t)) (y - x) = (f (g 1) - f (g 0)) / (1 - 0)

Tactic:
refine exists_hasDerivAt_eq_slope (f ∘ g) _ (by simp) ?_ ?_

Goal state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t ↦ (AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t)) (y - x)) I t
⊢ ContinuousOn (f ∘ g) (Icc 0 1)

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t ↦ (AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t)) (y - x)) I t
⊢ ∀ x_1 ∈ Ioo 0 1, HasDerivAt (f ∘ g) ((f' (g x_1)) (y - x)) x_1
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
⊢ ∃ z ∈ segment ℝ x y, f y - f x = (f' z) (y - x)

Tactic:
set g : ℝ → E := fun t => AffineMap.lineMap x y t
  set I := Icc (0 : ℝ) 1
  have hsub : Ioo (0 : ℝ) 1 ⊆ I := Ioo_subset_Icc_self
  have hmaps : MapsTo g I s := hs.mapsTo_lineMap xs ys
  -- The one-variable function `f ∘ g` has derivative `f' (g t) (y - x)` at each `t ∈ I`
  have hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) (f' (g t) (y - x)) I t := fun t ht =>
    (hf _ (hmaps ht)).comp_hasDerivWithinAt t AffineMap.hasDerivWithinAt_lineMap hmaps
  -- apply 1-variable mean value theorem to pullback
  have hMVT : ∃ t ∈ Ioo (0 : ℝ) 1, f' (g t) (y - x) = (f (g 1) - f (g 0)) / (1 - 0) := by
    refine exists_hasDerivAt_eq_slope (f ∘ g) _ (by simp) ?_ ?_
    · exact fun t Ht => (hfg t Ht).continuousWithinAt
    · exact fun t Ht => (hfg t <| hsub Ht).hasDerivAt (Icc_mem_nhds Ht.1 Ht.2)
  -- reinterpret on domain
  rcases hMVT with ⟨t, Ht, hMVT'⟩
  rw [segment_eq_image_lineMap, exists_mem_image]
  refine ⟨t, hsub Ht, ?_⟩
  simpa [g] using hMVT'.symm

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
hx : x = 0
⊢ 0 = 0⁻¹

Tactic:
inv_zero

Goal state after:
x : ℝ
hx : x = 0
⊢ 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x ↦ -x ^ n / (1 - x)
y : ℝ
hy : y ∈ Set.Ioo (-1) 1
this : HasDerivAt F (∑ i ∈ Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)) y
⊢ ∑ i ∈ Finset.range n, y ^ i + -1 / (1 - y) = ∑ i ∈ Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y)

Tactic:
congr with i
        rw [Nat.cast_succ, mul_div_cancel_left₀ _ (Nat.cast_add_one_pos i).ne']

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

Goal state before:
pp: case refine_1
𝕜 : 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
K : Set (E →L[𝕜] F)
x : E
hx : x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
p : ℕ
hp : p ≥ n
q : ℕ
hq : q ≥ n
⊢ x ∈ A f (fderiv 𝕜 f x) ((1 / 2) ^ p) ((1 / 2) ^ e)

Tactic:
· refine hR _ ⟨by positivity, lt_of_le_of_lt ?_ hn⟩
      exact pow_le_pow_of_le_one (by norm_num) (by norm_num) (by assumption)

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

Goal state before:
pp: case refine_2
𝕜 : 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
K : Set (E →L[𝕜] F)
x : E
hx : x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
p : ℕ
hp : p ≥ n
q : ℕ
hq : q ≥ n
⊢ x ∈ A f (fderiv 𝕜 f x) ((1 / 2) ^ q) ((1 / 2) ^ e)

Tactic:
· refine hR _ ⟨by positivity, lt_of_le_of_lt ?_ hn⟩
      exact pow_le_pow_of_le_one (by norm_num) (by norm_num) (by assumption)

Goal state after:
Module: Mathlib.Analysis.RCLike.Extend

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
F : Type u_2
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
f : StrongDual 𝕜 F
⊢ extendRCLike ((fun f ↦ reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f) f) = f

Tactic:
by ext; apply RCLike.ext <;> simp [extendRCLike_apply]

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

Goal state before:
pp: E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
⊢ x ∈ closure[inst✝¹] s

Tactic:
have : ∀ᶠ r : ℝ in 𝓝[<] 1, r • x ∈ s := by
    filter_upwards [Ico_mem_nhdsLT one_pos] with r ⟨hr₀, hr₁⟩
    apply setOfPred_gauge_lt_one_subset_self hc hs₀ ha
    rw [mem_ofPred_eq, gauge_smul_of_nonneg hr₀]
    exact mul_lt_one_of_nonneg_of_lt_one_left hr₀ hr₁ h

Goal state after:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
this : ∀ᶠ (r : ℝ) in 𝓝[<] 1, r • x ∈ s
⊢ x ∈ closure[inst✝¹] s