internlm/Lean-Github huggingface dataset:
Theorem: leadingCoeff_const_smul
Proof state before:
case zero.h
𝕜 : 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 a : 𝕜
a0 : ¬a = 0
x✝ : 𝕜
⊢ (Function.swap dslope c)^[0] (fun z => a • f z) x✝ = (a • (Function.swap dslope c)^[0] f) x✝

case succ
𝕜 : 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 a : 𝕜
a0 : ¬a = 0
n : ℕ
h : ((Function.swap dslope c)^[n] fun z => a • f z) = a • (Function.swap dslope c)^[n] f
⊢ ((Function.swap dslope c)^[n + 1] fun z => a • f z) = a • (Function.swap dslope c)^[n + 1] f
Tactic:
simp only [Function.iterate_zero_apply, Pi.smul_apply]
Proof state after:
case succ
𝕜 : 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 a : 𝕜
a0 : ¬a = 0
n : ℕ
h : ((Function.swap dslope c)^[n] fun z => a • f z) = a • (Function.swap dslope c)^[n] f
⊢ ((Function.swap dslope c)^[n + 1] fun z => a • f z) = a • (Function.swap dslope c)^[n + 1] f
Theorem: leadingCoeff_const_smul
Proof state before:
case succ
𝕜 : 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 a : 𝕜
a0 : ¬a = 0
n : ℕ
h : ((Function.swap dslope c)^[n] fun z => a • f z) = a • (Function.swap dslope c)^[n] f
⊢ ((Function.swap dslope c)^[n + 1] fun z => a • f z) = a • (Function.swap dslope c)^[n + 1] f
Tactic:
generalize hg : (Function.swap dslope c)^[n] f = g
Proof state after:
case succ
𝕜 : 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 a : 𝕜
a0 : ¬a = 0
n : ℕ
h : ((Function.swap dslope c)^[n] fun z => a • f z) = a • (Function.swap dslope c)^[n] f
g : 𝕜 → E
hg : (Function.swap dslope c)^[n] f = g
⊢ ((Function.swap dslope c)^[n + 1] fun z => a • f z) = a • (Function.swap dslope c)^[n + 1] f
Theorem: leadingCoeff_const_smul
Proof state before:
case succ
𝕜 : 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 a : 𝕜
a0 : ¬a = 0
n : ℕ
h : ((Function.swap dslope c)^[n] fun z => a • f z) = a • (Function.swap dslope c)^[n] f
g : 𝕜 → E
hg : (Function.swap dslope c)^[n] f = g
⊢ ((Function.swap dslope c)^[n + 1] fun z => a • f z) = a • (Function.swap dslope c)^[n + 1] f
Tactic:
simp only [Function.iterate_succ_apply', h, hg]
Proof state after:
case succ
𝕜 : 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 a : 𝕜
a0 : ¬a = 0
n : ℕ
h : ((Function.swap dslope c)^[n] fun z => a • f z) = a • (Function.swap dslope c)^[n] f
g : 𝕜 → E
hg : (Function.swap dslope c)^[n] f = g
⊢ Function.swap dslope c (a • g) = a • Function.swap dslope c g
Theorem: leadingCoeff_const_smul
Proof state before:
case succ
𝕜 : 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 a : 𝕜
a0 : ¬a = 0
n : ℕ
h : ((Function.swap dslope c)^[n] fun z => a • f z) = a • (Function.swap dslope c)^[n] f
g : 𝕜 → E
hg : (Function.swap dslope c)^[n] f = g
⊢ Function.swap dslope c (a • g) = a • Function.swap dslope c g
Tactic:
funext x
Proof state after:
case succ.h
𝕜 : 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 a : 𝕜
a0 : ¬a = 0
n : ℕ
h : ((Function.swap dslope c)^[n] fun z => a • f z) = a • (Function.swap dslope c)^[n] f
g : 𝕜 → E
hg : (Function.swap dslope c)^[n] f = g
x : 𝕜
⊢ Function.swap dslope c (a • g) x = (a • Function.swap dslope c g) x
Theorem: leadingCoeff_const_smul
Proof state before:
case succ.h
𝕜 : 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 a : 𝕜
a0 : ¬a = 0
n : ℕ
h : ((Function.swap dslope c)^[n] fun z => a • f z) = a • (Function.swap dslope c)^[n] f
g : 𝕜 → E
hg : (Function.swap dslope c)^[n] f = g
x : 𝕜
⊢ Function.swap dslope c (a • g) x = (a • Function.swap dslope c g) x
Tactic:
simp only [Function.swap]
Proof state after:
case succ.h
𝕜 : 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 a : 𝕜
a0 : ¬a = 0
n : ℕ
h : ((Function.swap dslope c)^[n] fun z => a • f z) = a • (Function.swap dslope c)^[n] f
g : 𝕜 → E
hg : (Function.swap dslope c)^[n] f = g
x : 𝕜
⊢ dslope (a • g) c x = (a • dslope g c) x
Theorem: leadingCoeff_const_smul
Proof state before:
case succ.h
𝕜 : 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 a : 𝕜
a0 : ¬a = 0
n : ℕ
h : ((Function.swap dslope c)^[n] fun z => a • f z) = a • (Function.swap dslope c)^[n] f
g : 𝕜 → E
hg : (Function.swap dslope c)^[n] f = g
x : 𝕜
⊢ dslope (a • g) c x = (a • dslope g c) x
Tactic:
by_cases cx : x = c
Proof state after:
case pos
𝕜 : 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 a : 𝕜
a0 : ¬a = 0
n : ℕ
h : ((Function.swap dslope c)^[n] fun z => a • f z) = a • (Function.swap dslope c)^[n] f
g : 𝕜 → E
hg : (Function.swap dslope c)^[n] f = g
x : 𝕜
cx : x = c
⊢ dslope (a • g) c x = (a • dslope g c) x

case neg
𝕜 : 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 a : 𝕜
a0 : ¬a = 0
n : ℕ
h : ((Function.swap dslope c)^[n] fun z => a • f z) = a • (Function.swap dslope c)^[n] f
g : 𝕜 → E
hg : (Function.swap dslope c)^[n] f = g
x : 𝕜
cx : ¬x = c
⊢ dslope (a • g) c x = (a • dslope g c) x
Theorem: leadingCoeff_const_smul
Proof state before:
case pos
𝕜 : 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 a : 𝕜
a0 : ¬a = 0
n : ℕ
h : ((Function.swap dslope c)^[n] fun z => a • f z) = a • (Function.swap dslope c)^[n] f
g : 𝕜 → E
hg : (Function.swap dslope c)^[n] f = g
x : 𝕜
cx : x = c
⊢ dslope (a • g) c x = (a • dslope g c) x

case neg
𝕜 : 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 a : 𝕜
a0 : ¬a = 0
n : ℕ
h : ((Function.swap dslope c)^[n] fun z => a • f z) = a • (Function.swap dslope c)^[n] f
g : 𝕜 → E
hg : (Function.swap dslope c)^[n] f = g
x : 𝕜
cx : ¬x = c
⊢ dslope (a • g) c x = (a • dslope g c) x
Tactic:
simp only [cx, dslope_same, Pi.smul_apply, Pi.smul_def, deriv_const_smul']
Proof state after:
case neg
𝕜 : 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 a : 𝕜
a0 : ¬a = 0
n : ℕ
h : ((Function.swap dslope c)^[n] fun z => a • f z) = a • (Function.swap dslope c)^[n] f
g : 𝕜 → E
hg : (Function.swap dslope c)^[n] f = g
x : 𝕜
cx : ¬x = c
⊢ dslope (a • g) c x = (a • dslope g c) x
Theorem: leadingCoeff_const_smul
Proof state before:
case neg
𝕜 : 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 a : 𝕜
a0 : ¬a = 0
n : ℕ
h : ((Function.swap dslope c)^[n] fun z => a • f z) = a • (Function.swap dslope c)^[n] f
g : 𝕜 → E
hg : (Function.swap dslope c)^[n] f = g
x : 𝕜
cx : ¬x = c
⊢ dslope (a • g) c x = (a • dslope g c) x
Tactic:
simp only [dslope_of_ne _ cx, Pi.smul_apply, slope, vsub_eq_sub, ← smul_sub, smul_comm _ a]
Proof state after:
no goals
Theorem: leadingCoeff_ne_zero
Proof 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
o0 : orderAt f c ≠ 0
⊢ leadingCoeff f c ≠ 0
Tactic:
rcases fa with ⟨p, fp⟩
Proof 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 : 𝕜
o0 : orderAt f c ≠ 0
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
⊢ leadingCoeff f c ≠ 0
Theorem: leadingCoeff_ne_zero
Proof 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 : 𝕜
o0 : orderAt f c ≠ 0
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
⊢ leadingCoeff f c ≠ 0
Tactic:
simp only [fp.orderAt_unique, leadingCoeff] at o0 ⊢
Proof 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
o0 : p.order ≠ 0
⊢ (Function.swap dslope c)^[p.order] f c ≠ 0
Theorem: leadingCoeff_ne_zero
Proof 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
o0 : p.order ≠ 0
⊢ (Function.swap dslope c)^[p.order] f c ≠ 0
Tactic:
exact fp.iterate_dslope_fslope_ne_zero (FormalMultilinearSeries.ne_zero_of_order_ne_zero o0)
Proof state after:
no goals
Theorem: SuperAt.d0
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
⊢ d ≠ 0
Tactic:
have h := s.d2
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
h : 2 ≤ d
⊢ d ≠ 0
Theorem: SuperAt.d0
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
h : 2 ≤ d
⊢ d ≠ 0
Tactic:
omega
Proof state after:
no goals
Theorem: SuperAt.dr2
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
⊢ 2 ≤ ↑2
Tactic:
norm_num
Proof state after:
no goals
Theorem: g0
Proof state before:
f✝ : ℂ → ℂ
d✝ : ℕ
z : ℂ
t : Set ℂ
f : ℂ → ℂ
d : ℕ
⊢ g f d 0 = 1
Tactic:
simp only [g, eq_self_iff_true, if_true]
Proof state after:
no goals
Theorem: SuperAt.approx
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
⊢ (fun z => f z - z ^ d) =o[𝓝 0] fun z => z ^ d
Tactic:
have a := s.fa0.leading_approx
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
a : (fun z => f z - (z - 0) ^ orderAt f 0 • leadingCoeff f 0) =o[𝓝 0] fun z => (z - 0) ^ orderAt f 0
⊢ (fun z => f z - z ^ d) =o[𝓝 0] fun z => z ^ d
Theorem: SuperAt.approx
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
a : (fun z => f z - (z - 0) ^ orderAt f 0 • leadingCoeff f 0) =o[𝓝 0] fun z => (z - 0) ^ orderAt f 0
⊢ (fun z => f z - z ^ d) =o[𝓝 0] fun z => z ^ d
Tactic:
simp only [s.fd, s.fc, sub_zero, Pi.one_apply, Algebra.id.smul_eq_mul, mul_one] at a
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
a : (fun z => f z - z ^ d) =o[𝓝 0] fun z => z ^ d
⊢ (fun z => f z - z ^ d) =o[𝓝 0] fun z => z ^ d
Theorem: SuperAt.approx
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
a : (fun z => f z - z ^ d) =o[𝓝 0] fun z => z ^ d
⊢ (fun z => f z - z ^ d) =o[𝓝 0] fun z => z ^ d
Tactic:
exact a
Proof state after:
no goals
Theorem: SuperAt.f0
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
⊢ orderAt f 0 > 0
Tactic:
simp [s.fd, s.dp]
Proof state after:
no goals
Theorem: SuperAt.fg
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
z : ℂ
⊢ f z = z ^ d * g f d z
Tactic:
by_cases z0 : z = 0
Proof state after:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
z : ℂ
z0 : z = 0
⊢ f z = z ^ d * g f d z

case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
z : ℂ
z0 : ¬z = 0
⊢ f z = z ^ d * g f d z
Theorem: SuperAt.fg
Proof state before:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
z : ℂ
z0 : z = 0
⊢ f z = z ^ d * g f d z
Tactic:
simp only [z0, zero_pow s.d0, s.f0, MulZeroClass.zero_mul]
Proof state after:
no goals
Theorem: SuperAt.fg
Proof state before:
case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
z : ℂ
z0 : ¬z = 0
⊢ f z = z ^ d * g f d z
Tactic:
simp only [g, z0, if_false]
Proof state after:
case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
z : ℂ
z0 : ¬z = 0
⊢ f z = z ^ d * (f z / z ^ d)
Theorem: SuperAt.fg
Proof state before:
case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
z : ℂ
z0 : ¬z = 0
⊢ f z = z ^ d * (f z / z ^ d)
Tactic:
field_simp [z0]
Proof state after:
no goals
Theorem: SuperAt.ga_of_fa
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
c : ℂ
fa : AnalyticAt ℂ f c
⊢ AnalyticAt ℂ (g f d) c
Tactic:
rcases fa.exists_ball_analyticOn with ⟨r, rp, fa⟩
Proof state after:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
fa : AnalyticOn ℂ f (ball c r)
⊢ AnalyticAt ℂ (g f d) c
Theorem: SuperAt.ga_of_fa
Proof state before:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
fa : AnalyticOn ℂ f (ball c r)
⊢ AnalyticAt ℂ (g f d) c
Tactic:
have o : IsOpen (ball c r) := isOpen_ball
Proof state after:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
fa : AnalyticOn ℂ f (ball c r)
o : IsOpen (ball c r)
⊢ AnalyticAt ℂ (g f d) c
Theorem: SuperAt.ga_of_fa
Proof state before:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
fa : AnalyticOn ℂ f (ball c r)
o : IsOpen (ball c r)
⊢ AnalyticAt ℂ (g f d) c
Tactic:
generalize ht : ball c r = t
Proof state after:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
fa : AnalyticOn ℂ f (ball c r)
o : IsOpen (ball c r)
t : Set ℂ
ht : ball c r = t
⊢ AnalyticAt ℂ (g f d) c
Theorem: SuperAt.ga_of_fa
Proof state before:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
fa : AnalyticOn ℂ f (ball c r)
o : IsOpen (ball c r)
t : Set ℂ
ht : ball c r = t
⊢ AnalyticAt ℂ (g f d) c
Tactic:
rw [ht] at fa o
Proof state after:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
⊢ AnalyticAt ℂ (g f d) c
Theorem: SuperAt.ga_of_fa
Proof state before:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
⊢ AnalyticAt ℂ (g f d) c
Tactic:
suffices h : AnalyticOn ℂ (g f d) t by rw [← ht] at h; exact h _ (mem_ball_self rp)
Proof state after:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
⊢ AnalyticOn ℂ (g f d) t
Theorem: SuperAt.ga_of_fa
Proof state before:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
⊢ AnalyticOn ℂ (g f d) t
Tactic:
have ga : DifferentiableOn ℂ (g f d) (t \ {0}) := by
  have e : ∀ z : ℂ, z ∈ t \ {0} → g f d z = f z / z ^ d := by
    intro z zs; simp only [Set.mem_diff, Set.mem_singleton_iff] at zs
    simp only [g, zs.2, if_false]
  rw [differentiableOn_congr e]
  apply DifferentiableOn.div (fa.mono (Set.diff_subset _ _)).differentiableOn
  exact (Differentiable.pow differentiable_id _).differentiableOn
  intro z zs; exact pow_ne_zero _ (Set.mem_diff_singleton.mp zs).2
Proof state after:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
⊢ AnalyticOn ℂ (g f d) t
Theorem: SuperAt.ga_of_fa
Proof state before:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
⊢ AnalyticOn ℂ (g f d) t
Tactic:
rw [analyticOn_iff_differentiableOn o]
Proof state after:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
⊢ DifferentiableOn ℂ (g f d) t
Theorem: SuperAt.ga_of_fa
Proof state before:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
⊢ DifferentiableOn ℂ (g f d) t
Tactic:
by_cases t0 : (0 : ℂ) ∉ t
Proof state after:
case pos
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : 0 ∉ t
⊢ DifferentiableOn ℂ (g f d) t

case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : ¬0 ∉ t
⊢ DifferentiableOn ℂ (g f d) t
Theorem: SuperAt.ga_of_fa
Proof state before:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : ¬0 ∉ t
⊢ DifferentiableOn ℂ (g f d) t
Tactic:
simp only [Set.not_not_mem] at t0
Proof state after:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t✝ : Set ℂ
s : SuperAt f d
c : ℂ
fa✝ : AnalyticAt ℂ f c
r : ℝ
rp : 0 < r
t : Set ℂ
o : IsOpen t
fa : AnalyticOn ℂ f t
ht : ball c r = t
ga : DifferentiableOn ℂ (g f d) (t \ {0})
t0 : 0 ∈ t
⊢ DifferentiableOn ℂ (g f d) t