Theorem: unevenSeries_analytic (Ray/Hartogs/Hartogs.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
⊢ AnalyticOn ℂ (fun z1 => unevenSeries u z1 n) (ball c1 r1)
Tactic:
intro z1 z1s
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Tactic:
rcases u.a (c0, z1) (Set.mk_mem_prod (Metric.mem_ball_self u.r0p) z1s) with ⟨p, r, hp⟩
State after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1

State before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Tactic:
have pa := (p.hasFPowerSeriesOnBall_changeOrigin n (lt_of_lt_of_le hp.r_pos hp.r_le)).analyticAt
State after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1

State before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Tactic:
set g := fun w1 ↦ ((0 : ℂ), w1 - z1)
State after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1

State before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Tactic:
have ga : AnalyticOn ℂ g univ := by
  rw [analyticOn_univ_iff_differentiable]
  exact (differentiable_const _).prod (differentiable_id.sub (differentiable_const _))
State after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ga : AnalyticOn ℂ g univ
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1

State before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ga : AnalyticOn ℂ g univ
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Tactic:
have g0 : 0 = g z1 := by
  simp only [Prod.ext_iff, Prod.fst_zero, Prod.snd_zero, sub_self, and_self_iff]
State after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ga : AnalyticOn ℂ g univ
g0 : 0 = g z1
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1

State before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ga : AnalyticOn ℂ g univ
g0 : 0 = g z1
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Tactic:
rw [g0] at pa
State after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) (g z1)
ga : AnalyticOn ℂ g univ
g0 : 0 = g z1
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1

State before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) (g z1)
ga : AnalyticOn ℂ g univ
g0 : 0 = g z1
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Tactic:
have ta := pa.comp (ga z1 (Set.mem_univ _))
State after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) (g z1)
ga : AnalyticOn ℂ g univ
g0 : 0 = g z1
ta : AnalyticAt ℂ ((fun x => p.changeOrigin x n) ∘ g) z1
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1

State before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) (g z1)
ga : AnalyticOn ℂ g univ
g0 : 0 = g z1
ta : AnalyticAt ℂ ((fun x => p.changeOrigin x n) ∘ g) z1
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Tactic:
simp_rw [Function.comp] at ta
State after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) (g z1)
ga : AnalyticOn ℂ g univ
g0 : 0 = g z1
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1

State before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) (g z1)
ga : AnalyticOn ℂ g univ
g0 : 0 = g z1
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Tactic:
clear pa ga g0
State after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1

State before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
pu : ∀ᶠ (w1 : ℂ) in 𝓝 z1, unevenSeries u w1 n = (p.changeOrigin (g w1)).along0 n
⊢ AnalyticAt ℂ (fun z1 => unevenSeries u z1 n) z1
Tactic:
rw [analyticAt_congr pu]
State after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
pu : ∀ᶠ (w1 : ℂ) in 𝓝 z1, unevenSeries u w1 n = (p.changeOrigin (g w1)).along0 n
⊢ AnalyticAt ℂ (fun x => (p.changeOrigin (g x)).along0 n) z1

State before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
pu : ∀ᶠ (w1 : ℂ) in 𝓝 z1, unevenSeries u w1 n = (p.changeOrigin (g w1)).along0 n
⊢ AnalyticAt ℂ (fun x => (p.changeOrigin (g x)).along0 n) z1
Tactic:
exact (Along0.analyticAt _).comp ta
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
⊢ AnalyticOn ℂ g univ
Tactic:
rw [analyticOn_univ_iff_differentiable]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
⊢ Differentiable ℂ g

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
⊢ Differentiable ℂ g
Tactic:
exact (differentiable_const _).prod (differentiable_id.sub (differentiable_const _))
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
pa : AnalyticAt ℂ (fun x => p.changeOrigin x n) 0
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ga : AnalyticOn ℂ g univ
⊢ 0 = g z1
Tactic:
simp only [Prod.ext_iff, Prod.fst_zero, Prod.snd_zero, sub_self, and_self_iff]
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
⊢ ∀ᶠ (w1 : ℂ) in 𝓝 z1, unevenSeries u w1 n = (p.changeOrigin (g w1)).along0 n
Tactic:
rw [eventually_nhds_iff]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t
Tactic:
set s' := r1 - dist z1 c1
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t
Tactic:
set s := min r (ENNReal.ofReal s')
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t
Tactic:
have s'p : s' > 0 := by simp only [Metric.mem_ball] at z1s; bound
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t
Tactic:
have sp : s > 0 := by bound
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t
Tactic:
have sr : s ≤ r := by bound
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t
Tactic:
have sb : EMetric.ball z1 s ⊆ ball c1 r1 := by
  rw [Set.subset_def]; intro x xs
  simp only [Metric.mem_ball, EMetric.mem_ball, lt_min_iff, edist_lt_ofReal, s] at xs z1s ⊢
  calc dist x c1
    _ ≤ dist x z1 + dist z1 c1 := by bound
    _ < s' + dist z1 c1 := (add_lt_add_right xs.right _)
    _ = r1 - dist z1 c1 + dist z1 c1 := rfl
    _ = r1 := by ring_nf
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
⊢ ∃ t, (∀ x ∈ t, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧ IsOpen t ∧ z1 ∈ t
Tactic:
use EMetric.ball z1 s
State after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
⊢ (∀ x ∈ EMetric.ball z1 s, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧
    IsOpen (EMetric.ball z1 s) ∧ z1 ∈ EMetric.ball z1 s

State before:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
⊢ (∀ x ∈ EMetric.ball z1 s, unevenSeries u x n = (p.changeOrigin (g x)).along0 n) ∧
    IsOpen (EMetric.ball z1 s) ∧ z1 ∈ EMetric.ball z1 s
Tactic:
refine ⟨?_, EMetric.isOpen_ball, EMetric.mem_ball_self sp⟩
State after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
⊢ ∀ x ∈ EMetric.ball z1 s, unevenSeries u x n = (p.changeOrigin (g x)).along0 n

State before:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
⊢ ∀ x ∈ EMetric.ball z1 s, unevenSeries u x n = (p.changeOrigin (g x)).along0 n
Tactic:
intro w1 w1s
State after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1✝ : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
⊢ unevenSeries u w1 n = (p.changeOrigin (g w1)).along0 n

State before:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1✝ : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
⊢ unevenSeries u w1 n = (p.changeOrigin (g w1)).along0 n
Tactic:
have p0 : HasFPowerSeriesAt (fun z0 ↦ f (z0, w1)) (unevenSeries u w1) c0 := by
  have w1c : w1 ∈ closedBall c1 r1 := mem_open_closed (sb w1s)
  refine (Uneven.has_series u u.r1p (le_refl _) w1c).hasFPowerSeriesAt
State after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1✝ : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
⊢ unevenSeries u w1 n = (p.changeOrigin (g w1)).along0 n

State before:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1✝ : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
p1 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (p.changeOrigin (g w1)).along0 c0
⊢ unevenSeries u w1 n = (p.changeOrigin (g w1)).along0 n
Tactic:
rw [HasFPowerSeriesAt.eq_formalMultilinearSeries p0 p1]
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
⊢ s' > 0
Tactic:
simp only [Metric.mem_ball] at z1s
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
z1s : dist z1 c1 < r1
⊢ s' > 0

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
z1s : dist z1 c1 < r1
⊢ s' > 0
Tactic:
bound
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
⊢ s > 0
Tactic:
bound
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
⊢ s ≤ r
Tactic:
bound
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
⊢ EMetric.ball z1 s ⊆ ball c1 r1
Tactic:
rw [Set.subset_def]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
⊢ ∀ x ∈ EMetric.ball z1 s, x ∈ ball c1 r1

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
⊢ ∀ x ∈ EMetric.ball z1 s, x ∈ ball c1 r1
Tactic:
intro x xs
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
x : ℂ
xs : x ∈ EMetric.ball z1 s
⊢ x ∈ ball c1 r1

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
x : ℂ
xs : x ∈ EMetric.ball z1 s
⊢ x ∈ ball c1 r1
Tactic:
simp only [Metric.mem_ball, EMetric.mem_ball, lt_min_iff, edist_lt_ofReal, s] at xs z1s ⊢
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
x : ℂ
xs : edist x z1 < r ∧ dist x z1 < s'
z1s : dist z1 c1 < r1
⊢ dist x c1 < r1

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
x : ℂ
xs : edist x z1 < r ∧ dist x z1 < s'
z1s : dist z1 c1 < r1
⊢ dist x c1 < r1
Tactic:
calc dist x c1
  _ ≤ dist x z1 + dist z1 c1 := by bound
  _ < s' + dist z1 c1 := (add_lt_add_right xs.right _)
  _ = r1 - dist z1 c1 + dist z1 c1 := rfl
  _ = r1 := by ring_nf
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
x : ℂ
xs : edist x z1 < r ∧ dist x z1 < s'
z1s : dist z1 c1 < r1
⊢ dist x c1 ≤ dist x z1 + dist z1 c1
Tactic:
bound
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
x : ℂ
xs : edist x z1 < r ∧ dist x z1 < s'
z1s : dist z1 c1 < r1
⊢ r1 - dist z1 c1 + dist z1 c1 = r1
Tactic:
ring_nf
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1✝ : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
⊢ HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
Tactic:
have w1c : w1 ∈ closedBall c1 r1 := mem_open_closed (sb w1s)
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1✝ : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
w1c : w1 ∈ closedBall c1 r1
⊢ HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1✝ : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
w1c : w1 ∈ closedBall c1 r1
⊢ HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
Tactic:
refine (Uneven.has_series u u.r1p (le_refl _) w1c).hasFPowerSeriesAt
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1✝ : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
⊢ HasFPowerSeriesAt (fun z0 => f (z0, w1)) (p.changeOrigin (g w1)).along0 c0
Tactic:
have wz : ↑‖((0 : ℂ), w1 - z1)‖₊ < r := by
  simp only [EMetric.mem_ball, edist_dist, Complex.dist_eq] at w1s
  simp only [Prod.nnnorm_def', nnnorm_zero, max_eq_right, zero_le', ← edist_eq_coe_nnnorm,
    edist_dist, Complex.dist_eq, sub_zero]
  exact lt_of_lt_of_le w1s sr
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1✝ : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
wz : ↑‖(0, w1 - z1)‖₊ < r
⊢ HasFPowerSeriesAt (fun z0 => f (z0, w1)) (p.changeOrigin (g w1)).along0 c0

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1✝ : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
wz : ↑‖(0, w1 - z1)‖₊ < r
⊢ HasFPowerSeriesAt (fun z0 => f (z0, w1)) (p.changeOrigin (g w1)).along0 c0
Tactic:
convert (hp.changeOrigin wz).hasFPowerSeriesAt.along0
State after:
case h.e'_9.h.h.e'_1.h.e'_4
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1✝ : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
wz : ↑‖(0, w1 - z1)‖₊ < r
x✝ : ℂ
⊢ w1 = (c0, z1).2 + (0, w1 - z1).2

case h.e'_11
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1✝ : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
wz : ↑‖(0, w1 - z1)‖₊ < r
⊢ c0 = (c0, z1).1 + (0, w1 - z1).1

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1✝ : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
⊢ ↑‖(0, w1 - z1)‖₊ < r
Tactic:
simp only [EMetric.mem_ball, edist_dist, Complex.dist_eq] at w1s
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1✝ : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
w1s : ENNReal.ofReal (Complex.abs (w1 - z1)) < s
⊢ ↑‖(0, w1 - z1)‖₊ < r

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1✝ : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
w1s : ENNReal.ofReal (Complex.abs (w1 - z1)) < s
⊢ ↑‖(0, w1 - z1)‖₊ < r
Tactic:
simp only [Prod.nnnorm_def', nnnorm_zero, max_eq_right, zero_le', ← edist_eq_coe_nnnorm,
  edist_dist, Complex.dist_eq, sub_zero]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1✝ : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
w1s : ENNReal.ofReal (Complex.abs (w1 - z1)) < s
⊢ ENNReal.ofReal (Complex.abs (w1 - z1)) < r

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1✝ : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
w1s : ENNReal.ofReal (Complex.abs (w1 - z1)) < s
⊢ ENNReal.ofReal (Complex.abs (w1 - z1)) < r
Tactic:
exact lt_of_lt_of_le w1s sr
State after:
no goals

State before:
case h.e'_9.h.h.e'_1.h.e'_4
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1✝ : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
wz : ↑‖(0, w1 - z1)‖₊ < r
x✝ : ℂ
⊢ w1 = (c0, z1).2 + (0, w1 - z1).2
Tactic:
simp only [add_sub_cancel]
State after:
no goals

State before:
case h.e'_11
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1✝ : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
wz : ↑‖(0, w1 - z1)‖₊ < r
⊢ c0 = (c0, z1).1 + (0, w1 - z1).1
Tactic:
simp only [add_sub_cancel, add_zero]
State after:
no goals