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

Goal state before:
pp: case refine_1
𝕜 : 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
H' : DifferentiableWithinAt 𝕜 f s x
I : (𝓝[(s ∩ t) \ {x}] x).NeBot
this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))
y : 𝕜
hy : y ∈ (s ∩ t) \ {x}
⊢ f y ∈ f '' t

Tactic:
exact mem_image_of_mem _ hy.1.2

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

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hx : AccPt x (𝓟 s)
hd : HasDerivWithinAt g g' s x
hg : MonotoneOn g s
this✝ : (𝓝[s \ {x}] x).NeBot
h'g : MonotoneOn g (insert x s)
this : Tendsto (slope g x) (𝓝[s \ {x}] x) (𝓝 g')
y : 𝕜
hy : y ∈ s ∧ ¬y = x
⊢ y ∈ insert x s

Tactic:
by simp [hy]

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
L : Filter 𝕜
L' : Filter 𝕜'
hg : HasDerivAtFilter g₁ g₁' (L' ×ˢ pure y)
hh : HasDerivAtFilter h h' (L ×ˢ pure x)
hy : y = h x
hL : Tendsto h L L'
⊢ Tendsto h (pure x) (pure y)

Tactic:
by simp [hy]

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

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x ↦ x⁻¹) s x = -(x ^ 2)⁻¹

Tactic:
rw [DifferentiableAt.derivWithin (differentiableAt_inv x_ne_zero) hxs]

Goal state after:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ deriv Inv.inv x = -(x ^ 2)⁻¹
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 : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hx : c x ≠ 0
⊢ derivWithin (fun x ↦ (c x)⁻¹) s x = -derivWithin c s x / c x ^ 2

Tactic:
by
  by_cases hsx : UniqueDiffWithinAt 𝕜 s x
  · exact (hc.hasDerivWithinAt.inv hx).derivWithin hsx
  · simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
L' : Filter 𝕜'
L'' : Filter E
hh₂ : HasDerivAtFilter h₂ h₂' (L' ×ˢ pure y)
hf : HasFDerivAtFilter f f' (L'' ×ˢ pure x)
hL : Tendsto f L'' L'
hy : y = f x
⊢ Tendsto f (pure x) (pure y)

Tactic:
by simp [hy]

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
L : Filter 𝕜
L' : Filter 𝕜'
hh₂ : HasDerivAtFilter h₂ h₂' (L' ×ˢ pure y)
hh : HasDerivAtFilter h h' (L ×ˢ pure x)
hL : Tendsto h L L'
hy : y = h x
⊢ Tendsto h (pure x) (pure y)

Tactic:
by simp [hy]

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
s : Set 𝕜
x : 𝕜
⊢ derivWithin (fun x ↦ f (c • x)) s x = c • derivWithin f (c • s) (c • x)

Tactic:
← derivWithin_const_smul_field,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : 𝕜 → E
s : Set 𝕜
x : 𝕜
⊢ derivWithin (fun x ↦ f (c • x)) s x = derivWithin (c • f) (c • s) (c • x)
Module: Mathlib.Analysis.Calculus.Deriv.Shift

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
s : Set 𝕜
x : 𝕜
⊢ derivWithin (fun x ↦ f (a - x)) s x = -derivWithin f (a +ᵥ -s) (a - x)

Tactic:
simp only [sub_eq_add_neg]

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
s : Set 𝕜
x : 𝕜
⊢ derivWithin (fun x ↦ f (a + -x)) s x = -derivWithin f (a +ᵥ -s) (a + -x)
Module: Mathlib.Analysis.Calculus.Deriv.ZPow

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

Tactic:
exact zpow_ne_zero _ hx

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

Goal state before:
pp: f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
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, f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x ↦ (f x, B x)) (Icc a b)
⊢ Icc a b ⊆ {x | f x ≤ B x}

Tactic:
have : IsClosed s := by
    simp only [s, inter_comm]
    exact A.preimage_isClosed_of_isClosed isClosed_Icc OrderClosedTopology.isClosed_le'

Goal state after:
f f' : ℝ → ℝ
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
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, f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x ↦ (f x, B x)) (Icc a b)
this : IsClosed s
⊢ Icc a b ⊆ {x | f x ≤ B x}
Module: Mathlib.Analysis.Calculus.MeanValue

Goal state before:
pp: case inr
f 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, f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x ↦ (f x, B x)) (Icc a b)
this✝ : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hf' : ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
hfr : f' x < r
hrB : r < B' x
HB : ∀ᶠ (z : ℝ) in 𝓝[>] x, r < slope B x z
z : ℝ
hfz : slope f x z < r
hzB : r < slope B x z
hz : z ∈ Ioc x y
this : (f z - f x) / (z - x) ≤ (B z - B x) / (z - x)
⊢ z ∈ {x | f x ≤ B x}

Tactic:
div_le_div_iff_of_pos_right (sub_pos.2 hz.1),

Goal state after:
case inr
f 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, f x = B x → f' x < B' x
s : Set ℝ := {x | f x ≤ B x} ∩ Icc a b
A : ContinuousOn (fun x ↦ (f x, B x)) (Icc a b)
this✝ : IsClosed s
x : ℝ
hxB✝ : f x ≤ B x
xab : x ∈ Ico a b
y : ℝ
hy : y ∈ Ioi x
hxB : f x = B x
r : ℝ
hf' : ∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
hfr : f' x < r
hrB : r < B' x
HB : ∀ᶠ (z : ℝ) in 𝓝[>] x, r < slope B x z
z : ℝ
hfz : slope f x z < r
hzB : r < slope B x z
hz : z ∈ Ioc x y
this : f z - f x ≤ B z - B x
⊢ z ∈ {x | f x ≤ B x}
Module: Mathlib.Analysis.Calculus.MeanValue

Goal state before:
pp: 𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt f (f' y) y
hcont : ContinuousAt f' x
⊢ HasStrictFDerivAt f (f' x) x

Tactic:
hasStrictFDerivAt_iff_isLittleO,

Goal state after:
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt f (f' y) y
hcont : ContinuousAt f' x
⊢ (fun p ↦ f p.1 - f p.2 - (f' x) (p.1 - p.2)) =o[𝓝 (x, x)] fun p ↦ p.1 - p.2
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
g : G ≃ₗᵢ[𝕜] E
f : E → F
x : G
i : ℕ
⊢ ‖iteratedFDeriv 𝕜 i (f ∘ ⇑g) x‖ = ‖iteratedFDeriv 𝕜 i f (g x)‖

Tactic:
simp only [← iteratedFDerivWithin_univ]
  apply g.norm_iteratedFDerivWithin_comp_right f uniqueDiffOn_univ (mem_univ (g x)) i

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

Goal state before:
pp: case mp.refine_1
𝕜 : 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
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hn : ω ≠ ∞
h'n : ω + 1 ≠ ∞
h : ContDiffWithinAt 𝕜 (ω + 1) f s x
Hp : HasFTaylorSeriesUpToOn (ω + 1) f p u
H'p : ω + 1 = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u
⊢ AnalyticOn 𝕜 f u

Tactic:
exact Hp.analyticOn (H'p rfl 0)

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
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
hf : ContDiffAt 𝕜 n (uncurry f) (x₀, g x₀)
hg : ContDiffAt 𝕜 m g x₀
hmn : m + 1 ≤ n
⊢ ContDiffAt 𝕜 m (fun x ↦ fderiv 𝕜 (f x) (g x)) x₀

Tactic:
simp_rw [← fderivWithin_univ]
  refine (ContDiffWithinAt.fderivWithin hf.contDiffWithinAt hg.contDiffWithinAt uniqueDiffOn_univ
    hmn (mem_univ x₀) ?_).contDiffAt univ_mem
  rw [preimage_univ]

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

Goal state before:
pp: case inr
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 ≠ 0
⊢ 1 < Nat.card ↑(range (c.emb (c.index 0)))

Tactic:
· apply one_lt_two.trans_le
    have : {c.emb (c.index 0) 0,
        c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, Nat.sub_one_lt_of_lt (c.partSize_pos _)⟩}
          ⊆ range (c.emb (c.index 0)) := by simp [insert_subset]
    simp only [emb_zero] at this
    convert! Nat.card_mono Subtype.finite this
    simp only [Nat.card_eq_fintype_card, Fintype.card_ofFinset, toFinset_singleton]
    apply (Finset.card_pair ?_).symm
    exact ((Fin.zero_le _).trans_lt (c.parts_strictMono ((pos_iff_ne_zero' (c.index 0)).mpr h))).ne

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

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
n : ℕ
IH : ∀ {x : 𝕜}, iteratedDerivWithin n f s x = (fun g ↦ derivWithin g s)^[n] f x
x : 𝕜
⊢ iteratedDerivWithin (n + 1) f s x = (fun g ↦ derivWithin g s)^[n + 1] f x

Tactic:
iteratedDerivWithin_succ,

Goal state after:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n✝ : ℕ
f : 𝕜 → F
s : Set 𝕜
n : ℕ
IH : ∀ {x : 𝕜}, iteratedDerivWithin n f s x = (fun g ↦ derivWithin g s)^[n] f x
x : 𝕜
⊢ derivWithin (iteratedDerivWithin n f s) s x = (fun g ↦ derivWithin g s)^[n + 1] f 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
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
hu : ContDiffOn 𝕜 (↑(m + 1)) f (insert x s ∩ u)
⊢ DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) s x

Tactic:
set t := insert x s ∩ u

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
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
⊢ DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) s x
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i : Fin c.length
j : Fin (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)
h : ¬i = c.index 0
⊢ Fin n

Tactic:
refine Fin.pred (c.emb i (Fin.cast ?_ j)) ?_
      · simp [h]
      · conv_rhs => rw [← c.emb_invEmbedding 0]
        exact c.emb_ne_emb_of_ne h

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
f : E → F
n : ℕ∞
⊢ ContDiff 𝕜 (↑n) f ↔ ∀ (m : ℕ), ↑m ≤ n → ContDiff 𝕜 (↑m) f

Tactic:
by
  simp_rw [← contDiffOn_univ]; exact contDiffOn_iff_forall_nat_le

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
f : E → F
⊢ ContDiff 𝕜 ∞ f ↔ Differentiable 𝕜 f ∧ ContDiff 𝕜 ∞ (fderiv 𝕜 f)

Tactic:
rw [← ENat.coe_top_add_one, contDiff_succ_iff_fderiv]
  simp

Goal state after:
Module: Mathlib.Analysis.Complex.RealDeriv

Goal state before:
pp: e : ℂ → ℂ
z : ℝ
n : WithTop ℕ∞
h : ContDiffAt ℂ n e ↑z
⊢ ContDiffAt ℝ n (fun x ↦ (e ↑x).re) z

Tactic:
have A : ContDiffAt ℝ n ((↑) : ℝ → ℂ) z := ofRealCLM.contDiff.contDiffAt

Goal state after:
e : ℂ → ℂ
z : ℝ
n : WithTop ℕ∞
h : ContDiffAt ℂ n e ↑z
A : ContDiffAt ℝ n ofReal z
⊢ ContDiffAt ℝ n (fun x ↦ (e ↑x).re) z
Module: Mathlib.Analysis.Complex.RealDeriv

Goal state before:
pp: f : ℂ → ℂ
f' x : ℂ
h : HasDerivAt f f' x
⊢ HasFDerivAt f (f' • 1) x

Tactic:
simpa only [Complex.restrictScalars_toSpanSingleton] using h.hasFDerivAt.restrictScalars ℝ

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

Goal state before:
pp: case inr
𝔸 : Type u_2
inst✝³ : Ring 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x : 𝔸
val✝ : Algebra ℚ 𝔸
⊢ (fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) (MulOpposite.op x) = MulOpposite.op (exp x)

Tactic:
exp_eq_tsum ℚ

Goal state after:
case inr
𝔸 : Type u_2
inst✝³ : Ring 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x : 𝔸
val✝ : Algebra ℚ 𝔸
⊢ (fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) (MulOpposite.op x) = MulOpposite.op ((fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) x)
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝔸 : Type u_2
inst✝¹⁰ : Ring 𝔸
inst✝⁹ : TopologicalSpace 𝔸
inst✝⁸ : IsTopologicalRing 𝔸
R : Type u_3
S : Type u_4
inst✝⁷ : Monoid R
inst✝⁶ : SMul ℚ R
inst✝⁵ : MulAction R 𝔸
inst✝⁴ : Algebra ℚ 𝔸
inst✝³ : IsScalarTower ℚ R 𝔸
inst✝² : SetLike S 𝔸
inst✝¹ : SubsemiringClass S 𝔸
inst✝ : SMulMemClass S R 𝔸
s : S
h_closed : IsClosed[inst✝⁹] ↑s
x : 𝔸
h : x ∈ s
this : SMulMemClass S ℚ 𝔸
⊢ exp x ∈ s

Tactic:
exp_eq_tsum ℚ

Goal state after:
𝔸 : Type u_2
inst✝¹⁰ : Ring 𝔸
inst✝⁹ : TopologicalSpace 𝔸
inst✝⁸ : IsTopologicalRing 𝔸
R : Type u_3
S : Type u_4
inst✝⁷ : Monoid R
inst✝⁶ : SMul ℚ R
inst✝⁵ : MulAction R 𝔸
inst✝⁴ : Algebra ℚ 𝔸
inst✝³ : IsScalarTower ℚ R 𝔸
inst✝² : SetLike S 𝔸
inst✝¹ : SubsemiringClass S 𝔸
inst✝ : SMulMemClass S R 𝔸
s : S
h_closed : IsClosed[inst✝⁹] ↑s
x : 𝔸
h : x ∈ s
this : SMulMemClass S ℚ 𝔸
⊢ (fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) x ∈ s
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case pos.partSize
𝕜 : 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}
A : c.length - 1 + 1 = c.length
⊢ { length := c.length - 1 + 1, partSize := cons 1 fun i ↦ c.partSize (Fin.cast ⋯ i.succ), partSize_pos := ⋯,
        emb := fun i ↦
          cases (motive := fun x ↦ Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) x) → Fin (n + 1)) (fun x ↦ 0)
            (fun m ↦ succ ∘ fun j ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯) i,
        emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ }.partSize ≍
    c.partSize

Tactic:
refine (Fin.heq_fun_iff A).mpr (fun i ↦ ?_)
        induction i using Fin.induction with
        | zero => change 1 = c.partSize 0; simp [c.partSize_eq_one_of_range_emb_eq_singleton h]
        | succ i => simp only [cons_succ, val_succ]; rfl

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

Goal state before:
pp: case inr
𝔸 : Type u_2
inst✝³ : Ring 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x y : 𝔸
h : Commute x y
val✝ : Algebra ℚ 𝔸
⊢ Commute x (exp y)

Tactic:
exp_eq_tsum ℚ

Goal state after:
case inr
𝔸 : Type u_2
inst✝³ : Ring 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x y : 𝔸
h : Commute x y
val✝ : Algebra ℚ 𝔸
⊢ Commute x ((fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) y)
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝔸 : Type u_1
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
x a b : 𝔸
h : SemiconjBy x a b
⊢ SemiconjBy x (exp a) (exp b)

Tactic:
exp_eq_tsum ℚ

Goal state after:
𝔸 : Type u_1
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
x a b : 𝔸
h : SemiconjBy x a b
⊢ SemiconjBy x ((fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) a) ((fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) b)
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
s : Set 𝕜
𝕝 : Type u_4
inst✝³ : DivisionSemiring 𝕝
inst✝² : Module 𝕝 F
inst✝¹ : SMulCommClass 𝕜 𝕝 F
inst✝ : ContinuousConstSMul 𝕝 F
c : 𝕝
n : ℕ
IH : ∀ {x : 𝕜} (f : 𝕜 → F), iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x
x : 𝕜
f : 𝕜 → F
⊢ iteratedDerivWithin (n + 1) (c • f) s x = c • iteratedDerivWithin (n + 1) f s x

Tactic:
iteratedDerivWithin_succ,

Goal state after:
case succ
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
s : Set 𝕜
𝕝 : Type u_4
inst✝³ : DivisionSemiring 𝕝
inst✝² : Module 𝕝 F
inst✝¹ : SMulCommClass 𝕜 𝕝 F
inst✝ : ContinuousConstSMul 𝕝 F
c : 𝕝
n : ℕ
IH : ∀ {x : 𝕜} (f : 𝕜 → F), iteratedDerivWithin n (c • f) s x = c • iteratedDerivWithin n f s x
x : 𝕜
f : 𝕜 → F
⊢ derivWithin (iteratedDerivWithin n (c • f) s) s x = c • derivWithin (iteratedDerivWithin n f s) s x
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
s : Set 𝕜
𝕜' : Type u_6
inst✝¹ : NormedDivisionRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
d : 𝕜'
n : ℕ
IH : ∀ {x : 𝕜} (f : 𝕜 → 𝕜'), iteratedDerivWithin n (fun z ↦ f z * d) s x = iteratedDerivWithin n f s x * d
x : 𝕜
f : 𝕜 → 𝕜'
⊢ iteratedDerivWithin (n + 1) (fun z ↦ f z * d) s x = iteratedDerivWithin (n + 1) f s x * d

Tactic:
iteratedDerivWithin_succ,

Goal state after:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
s : Set 𝕜
𝕜' : Type u_6
inst✝¹ : NormedDivisionRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
d : 𝕜'
n : ℕ
IH : ∀ {x : 𝕜} (f : 𝕜 → 𝕜'), iteratedDerivWithin n (fun z ↦ f z * d) s x = iteratedDerivWithin n f s x * d
x : 𝕜
f : 𝕜 → 𝕜'
⊢ derivWithin (iteratedDerivWithin n (fun z ↦ f z * d) s) s x = derivWithin (iteratedDerivWithin n f s) s x * d
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
c : 𝕜
hs : Set.MapsTo (fun x ↦ c * x) s s
n : ℕ
ih :
  ∀ {x : 𝕜},
    x ∈ s →
      ContDiffOn 𝕜 (↑n) f s → iteratedDerivWithin n (fun x ↦ f (c * x)) s x = c ^ n • iteratedDerivWithin n f s (c * x)
x : 𝕜
hx : x ∈ s
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hcx : c * x ∈ s
h₀ : Set.EqOn (iteratedDerivWithin n (fun x ↦ f (c * x)) s) (fun x ↦ c ^ n • iteratedDerivWithin n f s (c * x)) s
h₁ : DifferentiableWithinAt 𝕜 (iteratedDerivWithin n f s) s (c * x)
h₂ : DifferentiableWithinAt 𝕜 (fun x ↦ iteratedDerivWithin n f s (c * x)) s x
⊢ iteratedDerivWithin (n + 1) (fun x ↦ f (c * x)) s x = c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)

Tactic:
iteratedDerivWithin_succ,

Goal state after:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
c : 𝕜
hs : Set.MapsTo (fun x ↦ c * x) s s
n : ℕ
ih :
  ∀ {x : 𝕜},
    x ∈ s →
      ContDiffOn 𝕜 (↑n) f s → iteratedDerivWithin n (fun x ↦ f (c * x)) s x = c ^ n • iteratedDerivWithin n f s (c * x)
x : 𝕜
hx : x ∈ s
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hcx : c * x ∈ s
h₀ : Set.EqOn (iteratedDerivWithin n (fun x ↦ f (c * x)) s) (fun x ↦ c ^ n • iteratedDerivWithin n f s (c * x)) s
h₁ : DifferentiableWithinAt 𝕜 (iteratedDerivWithin n f s) s (c * x)
h₂ : DifferentiableWithinAt 𝕜 (fun x ↦ iteratedDerivWithin n f s (c * x)) s x
⊢ derivWithin (iteratedDerivWithin n (fun x ↦ f (c * x)) s) s x = c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)