mathlib-initiative/mathlib-tactics huggingface dataset:
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
x : E
r : ℝ≥0∞
y : E
F : Type (max u v)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
h : HasFPowerSeriesOnBall f p x r
⊢ ((p 0) fun x ↦ y) = (p 0) fun x ↦ y

Tactic:
]

Goal state after:
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
t : Set 𝕜
h : Dense t
⊢ range (derivWithin f univ) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(Submodule.span 𝕜 (f '' t))

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
h : Dense t
⊢ range (derivWithin f univ) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(Submodule.span 𝕜 (f '' t))
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
n : ℕ
ih :
  ∀ {F : Type (max u v)} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r → (n ! • (p n) fun x ↦ y) = (iteratedFDeriv 𝕜 n f x) fun x ↦ y
F : Type (max u v)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
h : HasFPowerSeriesOnBall f p x r
⊢ ((iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x) fun x ↦ y) y =
    ((iteratedFDeriv 𝕜 n (fun y ↦ fderiv 𝕜 f y) x) (Fin.init fun x ↦ y)) y

Tactic:
]

Goal state after:
case succ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
n : ℕ
ih :
  ∀ {F : Type (max u v)} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r → (n ! • (p n) fun x ↦ y) = (iteratedFDeriv 𝕜 n f x) fun x ↦ y
F : Type (max u v)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
h : HasFPowerSeriesOnBall f p x r
⊢ ((iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x) fun x ↦ y) y =
    ((iteratedFDeriv 𝕜 n (fun y ↦ fderiv 𝕜 f y) x) (Fin.init fun x ↦ y)) y
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
n : ℕ
ih :
  ∀ {F : Type (max u v)} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r → (n ! • (p n) fun x ↦ y) = (iteratedFDeriv 𝕜 n f x) fun x ↦ y
F : Type (max u v)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
h : HasFPowerSeriesOnBall f p x r
⊢ ((n + 1)! • (p (n + 1)) fun x ↦ y) = (iteratedFDeriv 𝕜 (n + 1) f x) fun x ↦ y

Tactic:
· rw [factorial_succ, mul_comm, mul_smul, ← derivSeries_apply_diag,
      ← _root_.smul_apply, ih h.fderiv, iteratedFDeriv_succ_apply_right]
    rfl

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

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SeparableSpace 𝕜
f : 𝕜 → F
s t : Set 𝕜
ts : t ⊆ s
t_count : t.Countable
ht : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SeparableSpace 𝕜
f : 𝕜 → F
s t : Set 𝕜
ts : t ⊆ s
t_count : t.Countable
ht : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
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
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
y : E
inst✝ : CompleteSpace F
⊢ ((p 0) fun x ↦ y) = (p 0) fun x ↦ y

Tactic:
]

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

Goal state before:
pp: case succ
𝕜 : 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
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
y : E
inst✝ : CompleteSpace F
n✝ : ℕ
⊢ ((iteratedFDeriv 𝕜 n✝ (fderiv 𝕜 f) x) fun x ↦ y) y =
    ((iteratedFDeriv 𝕜 n✝ (fun y ↦ fderiv 𝕜 f y) x) (Fin.init fun x ↦ y)) y

Tactic:
]

Goal state after:
case succ
𝕜 : 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
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
y : E
inst✝ : CompleteSpace F
n✝ : ℕ
⊢ ((iteratedFDeriv 𝕜 n✝ (fderiv 𝕜 f) x) fun x ↦ y) y =
    ((iteratedFDeriv 𝕜 n✝ (fun y ↦ fderiv 𝕜 f y) x) (Fin.init fun x ↦ y)) y
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SeparableSpace 𝕜
f : 𝕜 → F
⊢ IsSeparable (range (derivWithin f univ))

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SeparableSpace 𝕜
f : 𝕜 → F
⊢ IsSeparable (range (derivWithin f univ))
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: 𝕜 : Type u
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : DecidableEq 𝕜
f : 𝕜 → 𝕜
c a : 𝕜
hf : HasDerivAt f a c
⊢ ContinuousAt (Function.update (slope f c) c a) c

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : DecidableEq 𝕜
f : 𝕜 → 𝕜
c a : 𝕜
hf : HasDerivAt f a c
⊢ ContinuousAt (Function.update (slope f c) c a) c
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
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
inst✝¹ : CompleteSpace F
inst✝ : CharZero 𝕜
y : E
hy : y ∈ Metric.eball 0 r
n : ℕ
⊢ ((↑n !)⁻¹ • (iteratedFDeriv 𝕜 n f x) fun x ↦ y) = (p n) fun x ↦ y

Tactic:
← h.factorial_smul y n,

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
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
inst✝¹ : CompleteSpace F
inst✝ : CharZero 𝕜
y : E
hy : y ∈ Metric.eball 0 r
n : ℕ
⊢ ((↑n !)⁻¹ • n ! • (p n) fun x ↦ y) = (p n) fun x ↦ y
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
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
inst✝¹ : CompleteSpace F
inst✝ : CharZero 𝕜
y : E
hy : y ∈ Metric.eball 0 r
n : ℕ
⊢ ((p n) fun x ↦ y) = (p n) fun x ↦ y

Tactic:
]

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

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hd : HasDerivWithinAt g g' univ x
hg : Monotone g
⊢ 0 ≤ g'

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hd : HasDerivWithinAt g g' univ x
hg : Monotone g
⊢ 0 ≤ g'
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : Monotone g
⊢ 0 ≤ derivWithin g univ x

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : Monotone g
⊢ 0 ≤ derivWithin g univ x
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hd : HasDerivWithinAt g g' univ x
hg : Antitone g
⊢ g' ≤ 0

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
g' : 𝕜
hd : HasDerivWithinAt g g' univ x
hg : Antitone g
⊢ g' ≤ 0
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : Antitone g
⊢ derivWithin g univ x ≤ 0

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : Antitone g
⊢ derivWithin g univ x ≤ 0
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
C :
  {x_1 | (fun z ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[s] x ∧
    {x_1 | (fun z ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[{x}] x
⊢ ∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r

Tactic:
]

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
s : Set ℝ
x r : ℝ
hf : HasDerivWithinAt f f' s x
hr : ‖f'‖ < r
hr₀ : 0 < r
A : ∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
B : ∀ᶠ (z : ℝ) in 𝓝[{x}] x, ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r
C :
  {x_1 | (fun z ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[s] x ∧
    {x_1 | (fun z ↦ ‖(z - x)⁻¹ • (f z - f x)‖ ∈ Iio r) x_1} ∈ 𝓝[{x}] x
⊢ ∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r
Module: Mathlib.Analysis.Calculus.DSlope

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : 𝕜
f : 𝕜 → E
h : b ≠ a
⊢ f b = f b

Tactic:
]

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

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
x r : ℝ
hf : HasDerivWithinAt f f' (Ici x) x
hr : ‖f'‖ < r
this : ∃ᶠ (x_1 : ℝ) in 𝓝[>] x, ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r
z : ℝ
hxz : x < z
hz : (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
⊢ (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r

Tactic:
]

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
x r : ℝ
hf : HasDerivWithinAt f f' (Ici x) x
hr : ‖f'‖ < r
this : ∃ᶠ (x_1 : ℝ) in 𝓝[>] x, ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r
z : ℝ
hxz : x < z
hz : (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
⊢ (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
Module: Mathlib.Analysis.Calculus.DSlope

Goal state before:
pp: case succ
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : 𝕜
n : ℕ
ih : ∀ {f : 𝕜 → E}, (∀ k < n, (swap dslope a)^[k] f a = 0) → (b - a) ^ n • (swap dslope a)^[n] f b = f b
f : 𝕜 → E
hf : ∀ k < n + 1, (swap dslope a)^[k] f a = 0
⊢ f b = f b

Tactic:
]

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

Goal state before:
pp: s t : Set ℝ
⊢ re ⁻¹' interior s ∩ im ⁻¹' interior t = re ⁻¹' interior s ∩ im ⁻¹' interior t

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

Goal state before:
pp: r θ : ℝ
⊢ (starRingEnd ℂ) (circleMap 0 r θ) = circleMap 0 r (-θ)

Tactic:
by
  simp [circleMap_zero, ← exp_conj]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

Goal state before:
pp: a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_dist : |a - b| < 2 * π
h : ∃ n, ↑a * I = ↑b * I + ↑n * (2 * ↑π * I)
⊢ a = b

Tactic:
]

Goal state after:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
h_dist : |a - b| < 2 * π
h : ∃ n, ↑a * I = ↑b * I + ↑n * (2 * ↑π * I)
⊢ a = b
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

Goal state before:
pp: a b R : ℝ
c : ℂ
h_R : R ≠ 0
x✝ : |a - b| ≤ 2 * π
x₁✝ : ℝ
left✝¹ : min a b < x₁✝
right✝¹ : x₁✝ ≤ max a b
x₂✝ : ℝ
left✝ : min a b < x₂✝
right✝ : x₂✝ ≤ max a b
h : circleMap c R x₁✝ = circleMap c R x₂✝
⊢ -(2 * π) < x₁✝ - x₂✝ ∧ x₁✝ - x₂✝ < 2 * π

Tactic:
]

Goal state after:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
x✝ : |a - b| ≤ 2 * π
x₁✝ : ℝ
left✝¹ : min a b < x₁✝
right✝¹ : x₁✝ ≤ max a b
x₂✝ : ℝ
left✝ : min a b < x₂✝
right✝ : x₂✝ ≤ max a b
h : circleMap c R x₁✝ = circleMap c R x₂✝
⊢ -(2 * π) < x₁✝ - x₂✝ ∧ x₁✝ - x₂✝ < 2 * π
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

Goal state before:
pp: a b R : ℝ
c : ℂ
h_R : R ≠ 0
x✝ : b - a ≤ 2 * π
x₁✝ : ℝ
left✝¹ : a ≤ x₁✝
right✝¹ : x₁✝ < b
x₂✝ : ℝ
left✝ : a ≤ x₂✝
right✝ : x₂✝ < b
h : circleMap c R x₁✝ = circleMap c R x₂✝
⊢ -(2 * π) < x₁✝ - x₂✝ ∧ x₁✝ - x₂✝ < 2 * π

Tactic:
]

Goal state after:
a b R : ℝ
c : ℂ
h_R : R ≠ 0
x✝ : b - a ≤ 2 * π
x₁✝ : ℝ
left✝¹ : a ≤ x₁✝
right✝¹ : x₁✝ < b
x₂✝ : ℝ
left✝ : a ≤ x₂✝
right✝ : x₂✝ < b
h : circleMap c R x₁✝ = circleMap c R x₂✝
⊢ -(2 * π) < x₁✝ - x₂✝ ∧ x₁✝ - x₂✝ < 2 * π
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
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' s' (h x)
hh : HasDerivAt h h' x
hs : ∀ (x : 𝕜), h x ∈ s'
hy : y = h x
⊢ HasDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
]

Goal state after:
𝕜 : 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
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' s' (h x)
hh : HasDerivAt h h' x
hs : ∀ (x : 𝕜), h x ∈ s'
hy : y = h x
⊢ HasDerivAt (g₁ ∘ h) (h' • g₁') x
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' t' (h x)
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s t'
hy : y = h x
⊢ HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivWithinAt g₁ g₁' t' (h x)
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s t'
hy : y = h x
⊢ HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x
Module: Mathlib.Analysis.Calculus.Deriv.Inv

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
⊢ Tendsto (fun p ↦ (x * x)⁻¹ - (p.1 * p.2)⁻¹) (𝓝 (x, x)) (𝓝 ((x * x)⁻¹ - (x * x)⁻¹))

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
⊢ Tendsto (fun p ↦ (x * x)⁻¹ - (p.1 * p.2)⁻¹) (𝓝 (x, x)) (𝓝 ((x * x)⁻¹ - (x * x)⁻¹))
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 : 𝕜'
hg : HasDerivAt g₁ g₁' (h x)
hh : HasDerivAt h h' x
hy : y = h x
⊢ HasDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
]

Goal state after:
𝕜 : 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 : 𝕜'
hg : HasDerivAt g₁ g₁' (h x)
hh : HasDerivAt h h' x
hy : y = h x
⊢ HasDerivAt (g₁ ∘ h) (h' • g₁') x
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 : 𝕜'
hg : HasStrictDerivAt g₁ g₁' (h x)
hh : HasStrictDerivAt h h' x
hy : y = h x
⊢ HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
]

Goal state after:
𝕜 : 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 : 𝕜'
hg : HasStrictDerivAt g₁ g₁' (h x)
hh : HasStrictDerivAt h h' x
hy : y = h x
⊢ HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivAt g₁ g₁' (h x)
hh : HasDerivWithinAt h h' s x
hy : y = h x
⊢ HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivAt g₁ g₁' (h x)
hh : HasDerivWithinAt h h' s x
hy : y = h x
⊢ HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ (fslope^[p.order] p 0) 1 ≠ 0

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ (fslope^[p.order] p 0) 1 ≠ 0
Module: Mathlib.Analysis.Calculus.Deriv.Inv

Goal state before:
pp: case inl
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
⊢ 0 = -(0 ^ 2)⁻¹

Tactic:
]

Goal state after:
case inl
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
⊢ 0 = -(0 ^ 2)⁻¹
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
⊢ deriv Inv.inv x = -(x ^ 2)⁻¹

Tactic:
]

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 : 𝕜
⊢ toSpanSingleton 𝕜 (-(x ^ 2)⁻¹) = toSpanSingleton 𝕜 (-(x ^ 2)⁻¹)

Tactic:
]

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
⊢ fderiv 𝕜 Inv.inv x = toSpanSingleton 𝕜 (-(x ^ 2)⁻¹)

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 Inv.inv x = toSpanSingleton 𝕜 (-(x ^ 2)⁻¹)
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 : HasDerivWithinAt c c' univ x
hx : c x ≠ 0
⊢ HasDerivWithinAt c⁻¹ (-c' / c x ^ 2) univ x

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' univ x
hx : c x ≠ 0
⊢ HasDerivWithinAt c⁻¹ (-c' / c x ^ 2) univ x
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableWithinAt 𝕜' g₁ t' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s t'
hy : y = h x
⊢ derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)

Tactic:
]

Goal state after:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableWithinAt 𝕜' g₁ t' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s t'
hy : y = h x
⊢ derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
z : 𝕜
k : ℕ
hk : k < p.order
⊢ 0 = 0

Tactic:
]

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
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝 z₀, x ∈ {z₀}ᶜ → f x ≠ 0

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝 z₀, x ∈ {z₀}ᶜ → f x ≠ 0