Theorem: AnalyticAt.leading_approx (Ray/Analytic/Analytic.lean)

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
fa : AnalyticAt 𝕜 f c
⊢ (fun z => f z - (z - c) ^ orderAt f c • leadingCoeff f c) =o[𝓝 c] fun z => (z - c) ^ orderAt f c
Tactic:
rcases fa with ⟨p, fp⟩
State after:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
⊢ (fun z => f z - (z - c) ^ orderAt f c • leadingCoeff f c) =o[𝓝 c] fun z => (z - c) ^ orderAt f c

State before:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
⊢ (fun z => f z - (z - c) ^ orderAt f c • leadingCoeff f c) =o[𝓝 c] fun z => (z - c) ^ orderAt f c
Tactic:
generalize ha : leadingCoeff f c = a
State after:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
⊢ (fun z => f z - (z - c) ^ orderAt f c • a) =o[𝓝 c] fun z => (z - c) ^ orderAt f c

State before:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
⊢ (fun z => f z - (z - c) ^ orderAt f c • a) =o[𝓝 c] fun z => (z - c) ^ orderAt f c
Tactic:
generalize hd : orderAt f c = d
State after:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
⊢ (fun z => f z - (z - c) ^ d • a) =o[𝓝 c] fun z => (z - c) ^ d

State before:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
⊢ (fun z => f z - (z - c) ^ d • a) =o[𝓝 c] fun z => (z - c) ^ d
Tactic:
have ha' : (Function.swap dslope c)^[d] f c = a := by rw [← ha, ← hd, leadingCoeff]
State after:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
⊢ (fun z => f z - (z - c) ^ d • a) =o[𝓝 c] fun z => (z - c) ^ d

State before:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
⊢ (fun z => f z - (z - c) ^ d • a) =o[𝓝 c] fun z => (z - c) ^ d
Tactic:
have e := fp.eq_pow_order_mul_iterate_dslope
State after:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ p.order • (Function.swap dslope c)^[p.order] f z
⊢ (fun z => f z - (z - c) ^ d • a) =o[𝓝 c] fun z => (z - c) ^ d

State before:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ p.order • (Function.swap dslope c)^[p.order] f z
⊢ (fun z => f z - (z - c) ^ d • a) =o[𝓝 c] fun z => (z - c) ^ d
Tactic:
simp_rw [← fp.orderAt_unique, hd] at e
State after:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
⊢ (fun z => f z - (z - c) ^ d • a) =o[𝓝 c] fun z => (z - c) ^ d

State before:
case intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
⊢ (fun z => f z - (z - c) ^ d • a) =o[𝓝 c] fun z => (z - c) ^ d
Tactic:
apply Asymptotics.IsLittleO.of_isBigOWith
State after:
case intro.a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
⊢ ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → Asymptotics.IsBigOWith c_1 (𝓝 c) (fun z => f z - (z - c) ^ d • a) fun z => (z - c) ^ d

State before:
case intro.a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
⊢ ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → Asymptotics.IsBigOWith c_1 (𝓝 c) (fun z => f z - (z - c) ^ d • a) fun z => (z - c) ^ d
Tactic:
intro k kp
State after:
case intro.a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
⊢ Asymptotics.IsBigOWith k (𝓝 c) (fun z => f z - (z - c) ^ d • a) fun z => (z - c) ^ d

State before:
case intro.a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
⊢ Asymptotics.IsBigOWith k (𝓝 c) (fun z => f z - (z - c) ^ d • a) fun z => (z - c) ^ d
Tactic:
rw [Asymptotics.isBigOWith_iff]
State after:
case intro.a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖

State before:
case intro.a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖
Tactic:
apply e.mp
State after:
case intro.a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, f x = (x - c) ^ d • (Function.swap dslope c)^[d] f x → ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖

State before:
case intro.a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, f x = (x - c) ^ d • (Function.swap dslope c)^[d] f x → ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖
Tactic:
have dc : ContinuousAt ((Function.swap dslope c)^[d] f) c :=
  (fp.has_fpower_series_iterate_dslope_fslope d).analyticAt.continuousAt
State after:
case intro.a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, f x = (x - c) ^ d • (Function.swap dslope c)^[d] f x → ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖

State before:
case intro.a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, f x = (x - c) ^ d • (Function.swap dslope c)^[d] f x → ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖
Tactic:
rcases Metric.continuousAt_iff.mp dc k kp with ⟨r, rp, rh⟩
State after:
case intro.a.intro.intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
rh : ∀ {x : 𝕜}, dist x c < r → dist ((Function.swap dslope c)^[d] f x) ((Function.swap dslope c)^[d] f c) < k
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, f x = (x - c) ^ d • (Function.swap dslope c)^[d] f x → ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖

State before:
case intro.a.intro.intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
rh : ∀ {x : 𝕜}, dist x c < r → dist ((Function.swap dslope c)^[d] f x) ((Function.swap dslope c)^[d] f c) < k
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, f x = (x - c) ^ d • (Function.swap dslope c)^[d] f x → ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖
Tactic:
rw [ha'] at rh
State after:
case intro.a.intro.intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
rh : ∀ {x : 𝕜}, dist x c < r → dist ((Function.swap dslope c)^[d] f x) a < k
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, f x = (x - c) ^ d • (Function.swap dslope c)^[d] f x → ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖

State before:
case intro.a.intro.intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
rh : ∀ {x : 𝕜}, dist x c < r → dist ((Function.swap dslope c)^[d] f x) a < k
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, f x = (x - c) ^ d • (Function.swap dslope c)^[d] f x → ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖
Tactic:
generalize hg : (Function.swap dslope c)^[d] f = g
State after:
case intro.a.intro.intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
rh : ∀ {x : 𝕜}, dist x c < r → dist ((Function.swap dslope c)^[d] f x) a < k
g : 𝕜 → E
hg : (Function.swap dslope c)^[d] f = g
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, f x = (x - c) ^ d • g x → ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖

State before:
case intro.a.intro.intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
rh : ∀ {x : 𝕜}, dist x c < r → dist ((Function.swap dslope c)^[d] f x) a < k
g : 𝕜 → E
hg : (Function.swap dslope c)^[d] f = g
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, f x = (x - c) ^ d • g x → ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖
Tactic:
rw [hg] at rh
State after:
case intro.a.intro.intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
g : 𝕜 → E
rh : ∀ {x : 𝕜}, dist x c < r → dist (g x) a < k
hg : (Function.swap dslope c)^[d] f = g
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, f x = (x - c) ^ d • g x → ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖

State before:
case intro.a.intro.intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
g : 𝕜 → E
rh : ∀ {x : 𝕜}, dist x c < r → dist (g x) a < k
hg : (Function.swap dslope c)^[d] f = g
⊢ ∀ᶠ (x : 𝕜) in 𝓝 c, f x = (x - c) ^ d • g x → ‖f x - (x - c) ^ d • a‖ ≤ k * ‖(x - c) ^ d‖
Tactic:
rw [Metric.eventually_nhds_iff]
State after:
case intro.a.intro.intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
g : 𝕜 → E
rh : ∀ {x : 𝕜}, dist x c < r → dist (g x) a < k
hg : (Function.swap dslope c)^[d] f = g
⊢ ∃ ε > 0, ∀ ⦃y : 𝕜⦄, dist y c < ε → f y = (y - c) ^ d • g y → ‖f y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖

State before:
case intro.a.intro.intro
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
g : 𝕜 → E
rh : ∀ {x : 𝕜}, dist x c < r → dist (g x) a < k
hg : (Function.swap dslope c)^[d] f = g
⊢ ∃ ε > 0, ∀ ⦃y : 𝕜⦄, dist y c < ε → f y = (y - c) ^ d • g y → ‖f y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖
Tactic:
use r, rp
State after:
case right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
g : 𝕜 → E
rh : ∀ {x : 𝕜}, dist x c < r → dist (g x) a < k
hg : (Function.swap dslope c)^[d] f = g
⊢ ∀ ⦃y : 𝕜⦄, dist y c < r → f y = (y - c) ^ d • g y → ‖f y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖

State before:
case right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
g : 𝕜 → E
rh : ∀ {x : 𝕜}, dist x c < r → dist (g x) a < k
hg : (Function.swap dslope c)^[d] f = g
⊢ ∀ ⦃y : 𝕜⦄, dist y c < r → f y = (y - c) ^ d • g y → ‖f y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖
Tactic:
intro y yr fe
State after:
case right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
g : 𝕜 → E
rh : ∀ {x : 𝕜}, dist x c < r → dist (g x) a < k
hg : (Function.swap dslope c)^[d] f = g
y : 𝕜
yr : dist y c < r
fe : f y = (y - c) ^ d • g y
⊢ ‖f y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖

State before:
case right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
g : 𝕜 → E
rh : ∀ {x : 𝕜}, dist x c < r → dist (g x) a < k
hg : (Function.swap dslope c)^[d] f = g
y : 𝕜
yr : dist y c < r
fe : f y = (y - c) ^ d • g y
⊢ ‖f y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖
Tactic:
rw [fe]
State after:
case right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
g : 𝕜 → E
rh : ∀ {x : 𝕜}, dist x c < r → dist (g x) a < k
hg : (Function.swap dslope c)^[d] f = g
y : 𝕜
yr : dist y c < r
fe : f y = (y - c) ^ d • g y
⊢ ‖(y - c) ^ d • g y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖

State before:
case right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
g : 𝕜 → E
rh : ∀ {x : 𝕜}, dist x c < r → dist (g x) a < k
hg : (Function.swap dslope c)^[d] f = g
y : 𝕜
yr : dist y c < r
fe : f y = (y - c) ^ d • g y
⊢ ‖(y - c) ^ d • g y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖
Tactic:
specialize rh yr
State after:
case right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
g : 𝕜 → E
hg : (Function.swap dslope c)^[d] f = g
y : 𝕜
yr : dist y c < r
fe : f y = (y - c) ^ d • g y
rh : dist (g y) a < k
⊢ ‖(y - c) ^ d • g y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖

State before:
case right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
g : 𝕜 → E
hg : (Function.swap dslope c)^[d] f = g
y : 𝕜
yr : dist y c < r
fe : f y = (y - c) ^ d • g y
rh : dist (g y) a < k
⊢ ‖(y - c) ^ d • g y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖
Tactic:
rw [dist_eq_norm] at rh
State after:
case right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
g : 𝕜 → E
hg : (Function.swap dslope c)^[d] f = g
y : 𝕜
yr : dist y c < r
fe : f y = (y - c) ^ d • g y
rh : ‖g y - a‖ < k
⊢ ‖(y - c) ^ d • g y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖

State before:
case right
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
g : 𝕜 → E
hg : (Function.swap dslope c)^[d] f = g
y : 𝕜
yr : dist y c < r
fe : f y = (y - c) ^ d • g y
rh : ‖g y - a‖ < k
⊢ ‖(y - c) ^ d • g y - (y - c) ^ d • a‖ ≤ k * ‖(y - c) ^ d‖
Tactic:
calc ‖(y - c) ^ d • g y - (y - c) ^ d • a‖
  _ = ‖(y - c) ^ d‖ * ‖g y - a‖ := by rw [←smul_sub, norm_smul]
  _ ≤ ‖(y - c) ^ d‖ * k := mul_le_mul_of_nonneg_left rh.le (norm_nonneg _)
  _ = k * ‖(y - c) ^ d‖ := by rw [mul_comm]
State after:
no goals

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
⊢ (Function.swap dslope c)^[d] f c = a
Tactic:
rw [← ha, ← hd, leadingCoeff]
State after:
no goals

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
g : 𝕜 → E
hg : (Function.swap dslope c)^[d] f = g
y : 𝕜
yr : dist y c < r
fe : f y = (y - c) ^ d • g y
rh : ‖g y - a‖ < k
⊢ ‖(y - c) ^ d • g y - (y - c) ^ d • a‖ = ‖(y - c) ^ d‖ * ‖g y - a‖
Tactic:
rw [←smul_sub, norm_smul]
State after:
no goals

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
a : E
ha : leadingCoeff f c = a
d : ℕ
hd : orderAt f c = d
ha' : (Function.swap dslope c)^[d] f c = a
e : ∀ᶠ (z : 𝕜) in 𝓝 c, f z = (z - c) ^ d • (Function.swap dslope c)^[d] f z
k : ℝ
kp : 0 < k
dc : ContinuousAt ((Function.swap dslope c)^[d] f) c
r : ℝ
rp : r > 0
g : 𝕜 → E
hg : (Function.swap dslope c)^[d] f = g
y : 𝕜
yr : dist y c < r
fe : f y = (y - c) ^ d • g y
rh : ‖g y - a‖ < k
⊢ ‖(y - c) ^ d‖ * k = k * ‖(y - c) ^ d‖
Tactic:
rw [mul_comm]
State after:
no goals