internlm/Lean-Github huggingface dataset:
Theorem: lemma1
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
p : Filter ι
F : ι → α → β
f : α → β
inst✝ : UniformSpace β
hF : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 β)
⊢ Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓟 (f '' s) ×ˢ 𝓝ᵘ (f '' s))
Tactic:
refine tendsto_prod_iff'.mpr ⟨lemma2, ?h⟩
Proof state after:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
p : Filter ι
F : ι → α → β
f : α → β
inst✝ : UniformSpace β
hF : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 β)
⊢ Tendsto (fun n => (f n.2, F n.1 n.2).2) (p ×ˢ 𝓟 s) (𝓝ᵘ (f '' s))
Theorem: lemma1
Proof state before:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
p : Filter ι
F : ι → α → β
f : α → β
inst✝ : UniformSpace β
hF : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 β)
⊢ Tendsto (fun n => (f n.2, F n.1 n.2).2) (p ×ˢ 𝓟 s) (𝓝ᵘ (f '' s))
Tactic:
exact lemma0.comp (tendsto_inf.mpr ⟨hF, tendsto_comap_iff.mpr lemma2⟩)
Proof state after:
no goals
Theorem: HasFPowerSeriesAt.eventually_differentiable_at
Proof state before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
f : ℂ → E
z₀ : ℂ
hp : HasFPowerSeriesAt f p z₀
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, DifferentiableAt ℂ f z
Tactic:
obtain ⟨r, hp⟩ := hp
Proof state after:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
f : ℂ → E
z₀ : ℂ
r : ENNReal
hp : HasFPowerSeriesOnBall f p z₀ r
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, DifferentiableAt ℂ f z
Theorem: HasFPowerSeriesAt.eventually_differentiable_at
Proof state before:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
f : ℂ → E
z₀ : ℂ
r : ENNReal
hp : HasFPowerSeriesOnBall f p z₀ r
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, DifferentiableAt ℂ f z
Tactic:
exact hp.differentiableOn.eventually_differentiableAt (EMetric.ball_mem_nhds _ hp.r_pos)
Proof state after:
no goals
Theorem: circleIntegral.integral_add
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
c : ℂ
R : ℝ
hf : CircleIntegrable f c R
hg : CircleIntegrable g c R
⊢ (∮ (z : ℂ) in C(c, R), f z + g z) = (∮ (z : ℂ) in C(c, R), f z) + ∮ (z : ℂ) in C(c, R), g z
Tactic:
simp only [circleIntegral, smul_add, intervalIntegral.integral_add hf.out hg.out]
Proof state after:
no goals
Theorem: circle_integral_sub_center_inv_smul
Proof state before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f g : ℂ → E
r : ℝ
U : Set ℂ
c : ℂ
v : E
hr : 0 < r
⊢ (∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • v) = (2 * ↑π * I) • v
Tactic:
simp [circleIntegral.integral_sub_inv_of_mem_ball (mem_ball_self hr)]
Proof state after:
no goals
Theorem: DifferentiableOn.iterate_dslope
Proof state before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
hf : DifferentiableOn ℂ f U
hU : IsOpen U
hc : c ∈ U
⊢ DifferentiableOn ℂ ((swap dslope c)^[n] f) U
Tactic:
induction n generalizing f
Proof state after:
case zero
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
hU : IsOpen U
hc : c ∈ U
f : ℂ → E
hf : DifferentiableOn ℂ f U
⊢ DifferentiableOn ℂ ((swap dslope c)^[zero] f) U

case succ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
hU : IsOpen U
hc : c ∈ U
n✝ : ℕ
n_ih✝ : ∀ {f : ℂ → E}, DifferentiableOn ℂ f U → DifferentiableOn ℂ ((swap dslope c)^[n✝] f) U
f : ℂ → E
hf : DifferentiableOn ℂ f U
⊢ DifferentiableOn ℂ ((swap dslope c)^[succ n✝] f) U
Theorem: DifferentiableOn.iterate_dslope
Proof state before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
hU : IsOpen U
hc : c ∈ U
f : ℂ → E
hf : DifferentiableOn ℂ f U
⊢ DifferentiableOn ℂ ((swap dslope c)^[zero] f) U
Tactic:
case zero => exact hf
Proof state after:
no goals
Theorem: DifferentiableOn.iterate_dslope
Proof state before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
hU : IsOpen U
hc : c ∈ U
n✝ : ℕ
n_ih : ∀ {f : ℂ → E}, DifferentiableOn ℂ f U → DifferentiableOn ℂ ((swap dslope c)^[n✝] f) U
f : ℂ → E
hf : DifferentiableOn ℂ f U
⊢ DifferentiableOn ℂ ((swap dslope c)^[succ n✝] f) U
Tactic:
case succ n_ih => exact n_ih ((differentiableOn_dslope (hU.mem_nhds hc)).mpr hf)
Proof state after:
no goals
Theorem: DifferentiableOn.iterate_dslope
Proof state before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
hU : IsOpen U
hc : c ∈ U
f : ℂ → E
hf : DifferentiableOn ℂ f U
⊢ DifferentiableOn ℂ ((swap dslope c)^[zero] f) U
Tactic:
exact hf
Proof state after:
no goals
Theorem: DifferentiableOn.iterate_dslope
Proof state before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
hU : IsOpen U
hc : c ∈ U
n✝ : ℕ
n_ih : ∀ {f : ℂ → E}, DifferentiableOn ℂ f U → DifferentiableOn ℂ ((swap dslope c)^[n✝] f) U
f : ℂ → E
hf : DifferentiableOn ℂ f U
⊢ DifferentiableOn ℂ ((swap dslope c)^[succ n✝] f) U
Tactic:
exact n_ih ((differentiableOn_dslope (hU.mem_nhds hc)).mpr hf)
Proof state after:
no goals
Theorem: HasFPowerSeriesAt.dslope_order_eventually_ne_zero
Proof state before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, (swap dslope z₀)^[FormalMultilinearSeries.order p] f z ≠ 0
Tactic:
refine ContinuousAt.eventually_ne ?h (hp.iterate_dslope_fslope_ne_zero h)
Proof state after:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ ContinuousAt (fun z => (swap dslope z₀)^[FormalMultilinearSeries.order p] f z) z₀
Theorem: HasFPowerSeriesAt.dslope_order_eventually_ne_zero
Proof state before:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ ContinuousAt (fun z => (swap dslope z₀)^[FormalMultilinearSeries.order p] f z) z₀
Tactic:
obtain ⟨r, hf⟩ := hp
Proof state after:
case h.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
h : p ≠ 0
r : ENNReal
hf : HasFPowerSeriesOnBall f p z₀ r
⊢ ContinuousAt (fun z => (swap dslope z₀)^[FormalMultilinearSeries.order p] f z) z₀
Theorem: HasFPowerSeriesAt.dslope_order_eventually_ne_zero
Proof state before:
case h.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
h : p ≠ 0
r : ENNReal
hf : HasFPowerSeriesOnBall f p z₀ r
⊢ ContinuousAt (fun z => (swap dslope z₀)^[FormalMultilinearSeries.order p] f z) z₀
Tactic:
have hr : 0 < r := hf.r_pos
Proof state after:
case h.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
h : p ≠ 0
r : ENNReal
hf : HasFPowerSeriesOnBall f p z₀ r
hr : 0 < r
⊢ ContinuousAt (fun z => (swap dslope z₀)^[FormalMultilinearSeries.order p] f z) z₀
Theorem: HasFPowerSeriesAt.dslope_order_eventually_ne_zero
Proof state before:
case h.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
h : p ≠ 0
r : ENNReal
hf : HasFPowerSeriesOnBall f p z₀ r
hr : 0 < r
⊢ ContinuousAt (fun z => (swap dslope z₀)^[FormalMultilinearSeries.order p] f z) z₀
Tactic:
refine ContinuousOn.continuousAt ?h1 (EMetric.ball_mem_nhds _ hr)
Proof state after:
case h1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
h : p ≠ 0
r : ENNReal
hf : HasFPowerSeriesOnBall f p z₀ r
hr : 0 < r
⊢ ContinuousOn (fun z => (swap dslope z₀)^[FormalMultilinearSeries.order p] f z) (EMetric.ball z₀ r)
Theorem: HasFPowerSeriesAt.dslope_order_eventually_ne_zero
Proof state before:
case h1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
h : p ≠ 0
r : ENNReal
hf : HasFPowerSeriesOnBall f p z₀ r
hr : 0 < r
⊢ ContinuousOn (fun z => (swap dslope z₀)^[FormalMultilinearSeries.order p] f z) (EMetric.ball z₀ r)
Tactic:
have hh : DifferentiableOn ℂ (iterate (swap dslope z₀) p.order f) (EMetric.ball z₀ r) :=
  DifferentiableOn.iterate_dslope hf.differentiableOn EMetric.isOpen_ball (EMetric.mem_ball_self hr)
Proof state after:
case h1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
h : p ≠ 0
r : ENNReal
hf : HasFPowerSeriesOnBall f p z₀ r
hr : 0 < r
hh : DifferentiableOn ℂ ((swap dslope z₀)^[FormalMultilinearSeries.order p] f) (EMetric.ball z₀ r)
⊢ ContinuousOn (fun z => (swap dslope z₀)^[FormalMultilinearSeries.order p] f z) (EMetric.ball z₀ r)
Theorem: HasFPowerSeriesAt.dslope_order_eventually_ne_zero
Proof state before:
case h1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
p : FormalMultilinearSeries ℂ ℂ E
U : Set ℂ
z₀ c : ℂ
n : ℕ
h : p ≠ 0
r : ENNReal
hf : HasFPowerSeriesOnBall f p z₀ r
hr : 0 < r
hh : DifferentiableOn ℂ ((swap dslope z₀)^[FormalMultilinearSeries.order p] f) (EMetric.ball z₀ r)
⊢ ContinuousOn (fun z => (swap dslope z₀)^[FormalMultilinearSeries.order p] f z) (EMetric.ball z₀ r)
Tactic:
exact hh.continuousOn
Proof state after:
no goals
Theorem: deriv_div_self_eq_div_add_deriv_div_self
Proof state before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ n * g w
hz : z ≠ z₀
⊢ deriv f z / f z = ↑n / (z - z₀) + deriv g z / g z
Tactic:
have h1 : DifferentiableAt ℂ (λ y => (y - z₀) ^ n) z :=
  ((differentiable_id'.sub_const z₀).pow n).differentiableAt
Proof state after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ n * g w
hz : z ≠ z₀
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ n) z
⊢ deriv f z / f z = ↑n / (z - z₀) + deriv g z / g z
Theorem: deriv_div_self_eq_div_add_deriv_div_self
Proof state before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ n * g w
hz : z ≠ z₀
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ n) z
⊢ deriv f z / f z = ↑n / (z - z₀) + deriv g z / g z
Tactic:
have h4 : DifferentiableAt ℂ (λ y => y - z₀) z := (differentiable_id'.sub_const z₀).differentiableAt
Proof state after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ n * g w
hz : z ≠ z₀
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ n) z
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
⊢ deriv f z / f z = ↑n / (z - z₀) + deriv g z / g z
Theorem: deriv_div_self_eq_div_add_deriv_div_self
Proof state before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ n * g w
hz : z ≠ z₀
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ n) z
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
⊢ deriv f z / f z = ↑n / (z - z₀) + deriv g z / g z
Tactic:
have h5 : deriv (fun y => y - z₀) z = 1 := by simp only [deriv_sub_const, deriv_id'']
Proof state after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ n * g w
hz : z ≠ z₀
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ n) z
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
⊢ deriv f z / f z = ↑n / (z - z₀) + deriv g z / g z
Theorem: deriv_div_self_eq_div_add_deriv_div_self
Proof state before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ n * g w
hz : z ≠ z₀
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ n) z
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
⊢ deriv f z / f z = ↑n / (z - z₀) + deriv g z / g z
Tactic:
simp [hfg.deriv_eq, hfg.self_of_nhds, deriv_mul h1 hg, _root_.add_div, deriv_pow'' n h4, deriv_sub_const, h5]
Proof state after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ n * g w
hz : z ≠ z₀
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ n) z
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
⊢ ↑n * (z - z₀) ^ (n - 1) * g z / ((z - z₀) ^ n * g z) + (z - z₀) ^ n * deriv g z / ((z - z₀) ^ n * g z) =
    ↑n / (z - z₀) + deriv g z / g z
Theorem: deriv_div_self_eq_div_add_deriv_div_self
Proof state before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ n * g w
hz : z ≠ z₀
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ n) z
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
⊢ ↑n * (z - z₀) ^ (n - 1) * g z / ((z - z₀) ^ n * g z) + (z - z₀) ^ n * deriv g z / ((z - z₀) ^ n * g z) =
    ↑n / (z - z₀) + deriv g z / g z
Tactic:
cases n
Proof state after:
case zero
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hz : z ≠ z₀
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ zero * g w
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ zero) z
⊢ ↑zero * (z - z₀) ^ (zero - 1) * g z / ((z - z₀) ^ zero * g z) +
      (z - z₀) ^ zero * deriv g z / ((z - z₀) ^ zero * g z) =
    ↑zero / (z - z₀) + deriv g z / g z

case succ
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hz : z ≠ z₀
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
n✝ : ℕ
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ succ n✝ * g w
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ succ n✝) z
⊢ ↑(succ n✝) * (z - z₀) ^ (succ n✝ - 1) * g z / ((z - z₀) ^ succ n✝ * g z) +
      (z - z₀) ^ succ n✝ * deriv g z / ((z - z₀) ^ succ n✝ * g z) =
    ↑(succ n✝) / (z - z₀) + deriv g z / g z
Theorem: deriv_div_self_eq_div_add_deriv_div_self
Proof state before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hz : z ≠ z₀
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ zero * g w
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ zero) z
⊢ ↑zero * (z - z₀) ^ (zero - 1) * g z / ((z - z₀) ^ zero * g z) +
      (z - z₀) ^ zero * deriv g z / ((z - z₀) ^ zero * g z) =
    ↑zero / (z - z₀) + deriv g z / g z
Tactic:
case zero => simp
Proof state after:
no goals
Theorem: deriv_div_self_eq_div_add_deriv_div_self
Proof state before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hz : z ≠ z₀
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
n : ℕ
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ succ n * g w
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ succ n) z
⊢ ↑(succ n) * (z - z₀) ^ (succ n - 1) * g z / ((z - z₀) ^ succ n * g z) +
      (z - z₀) ^ succ n * deriv g z / ((z - z₀) ^ succ n * g z) =
    ↑(succ n) / (z - z₀) + deriv g z / g z
Tactic:
case succ n =>
  field_simp [_root_.pow_succ, sub_ne_zero.mpr hz]
  ring
Proof state after:
no goals
Theorem: deriv_div_self_eq_div_add_deriv_div_self
Proof state before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ n * g w
hz : z ≠ z₀
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ n) z
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
⊢ deriv (fun y => y - z₀) z = 1
Tactic:
simp only [deriv_sub_const, deriv_id'']
Proof state after:
no goals
Theorem: deriv_div_self_eq_div_add_deriv_div_self
Proof state before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hz : z ≠ z₀
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ zero * g w
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ zero) z
⊢ ↑zero * (z - z₀) ^ (zero - 1) * g z / ((z - z₀) ^ zero * g z) +
      (z - z₀) ^ zero * deriv g z / ((z - z₀) ^ zero * g z) =
    ↑zero / (z - z₀) + deriv g z / g z
Tactic:
simp
Proof state after:
no goals
Theorem: deriv_div_self_eq_div_add_deriv_div_self
Proof state before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hz : z ≠ z₀
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
n : ℕ
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ succ n * g w
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ succ n) z
⊢ ↑(succ n) * (z - z₀) ^ (succ n - 1) * g z / ((z - z₀) ^ succ n * g z) +
      (z - z₀) ^ succ n * deriv g z / ((z - z₀) ^ succ n * g z) =
    ↑(succ n) / (z - z₀) + deriv g z / g z
Tactic:
field_simp [_root_.pow_succ, sub_ne_zero.mpr hz]
Proof state after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hz : z ≠ z₀
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
n : ℕ
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ succ n * g w
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ succ n) z
⊢ ((↑n + 1) * (z - z₀) ^ n * g z + (z - z₀) * (z - z₀) ^ n * deriv g z) * ((z - z₀) * g z) =
    ((↑n + 1) * g z + deriv g z * (z - z₀)) * ((z - z₀) * (z - z₀) ^ n * g z)
Theorem: deriv_div_self_eq_div_add_deriv_div_self
Proof state before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hz : z ≠ z₀
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
n : ℕ
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ succ n * g w
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ succ n) z
⊢ ((↑n + 1) * (z - z₀) ^ n * g z + (z - z₀) * (z - z₀) ^ n * deriv g z) * ((z - z₀) * g z) =
    ((↑n + 1) * g z + deriv g z * (z - z₀)) * ((z - z₀) * (z - z₀) ^ n * g z)
Tactic:
ring
Proof state after:
no goals
Theorem: eventually_deriv_div_self_eq
Proof state before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ let g := (swap dslope z₀)^[FormalMultilinearSeries.order p] f;
  ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
Tactic:
intro g
Proof state after:
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
Theorem: eventually_deriv_div_self_eq
Proof state before:
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
Tactic:
obtain ⟨r, h2⟩ := hp.has_fpower_series_iterate_dslope_fslope p.order
Proof state after:
case intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
r : ENNReal
h2 :
  HasFPowerSeriesOnBall ((swap dslope z₀)^[FormalMultilinearSeries.order p] f)
    (FormalMultilinearSeries.fslope^[FormalMultilinearSeries.order p] p) z₀ r
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
Theorem: eventually_deriv_div_self_eq
Proof state before:
case intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
r : ENNReal
h2 :
  HasFPowerSeriesOnBall ((swap dslope z₀)^[FormalMultilinearSeries.order p] f)
    (FormalMultilinearSeries.fslope^[FormalMultilinearSeries.order p] p) z₀ r
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
Tactic:
have lh1 := h2.differentiableOn.eventually_differentiableAt (EMetric.ball_mem_nhds _ h2.r_pos)
Proof state after:
case intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
r : ENNReal
h2 :
  HasFPowerSeriesOnBall ((swap dslope z₀)^[FormalMultilinearSeries.order p] f)
    (FormalMultilinearSeries.fslope^[FormalMultilinearSeries.order p] p) z₀ r
lh1 : ∀ᶠ (y : ℂ) in 𝓝 z₀, DifferentiableAt ℂ ((swap dslope z₀)^[FormalMultilinearSeries.order p] f) y
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
Theorem: eventually_deriv_div_self_eq
Proof state before:
case intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
r : ENNReal
h2 :
  HasFPowerSeriesOnBall ((swap dslope z₀)^[FormalMultilinearSeries.order p] f)
    (FormalMultilinearSeries.fslope^[FormalMultilinearSeries.order p] p) z₀ r
lh1 : ∀ᶠ (y : ℂ) in 𝓝 z₀, DifferentiableAt ℂ ((swap dslope z₀)^[FormalMultilinearSeries.order p] f) y
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
Tactic:
have lh2 := hp.dslope_order_eventually_ne_zero h
Proof state after:
case intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
r : ENNReal
h2 :
  HasFPowerSeriesOnBall ((swap dslope z₀)^[FormalMultilinearSeries.order p] f)
    (FormalMultilinearSeries.fslope^[FormalMultilinearSeries.order p] p) z₀ r
lh1 : ∀ᶠ (y : ℂ) in 𝓝 z₀, DifferentiableAt ℂ ((swap dslope z₀)^[FormalMultilinearSeries.order p] f) y
lh2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, (swap dslope z₀)^[FormalMultilinearSeries.order p] f z ≠ 0
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z