Theorem: differentiable_iff_analytic2 (Ray/Analytic/Holomorphic.lean)

State before:
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
⊢ DifferentiableOn ℂ f s ↔ AnalyticOn ℂ f s
Tactic:
constructor
State after:
case mp
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
⊢ DifferentiableOn ℂ f s → AnalyticOn ℂ f s

case mpr
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
⊢ AnalyticOn ℂ f s → DifferentiableOn ℂ f s

State before:
case mp
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
⊢ DifferentiableOn ℂ f s → AnalyticOn ℂ f s
Tactic:
intro d
State after:
case mp
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
⊢ AnalyticOn ℂ f s

State before:
case mp
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
⊢ AnalyticOn ℂ f s
Tactic:
apply osgood o d.continuousOn
State after:
case mp.fa0
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
⊢ ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0

case mp.fa1
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
⊢ ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1

State before:
case mp.fa0
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
⊢ ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
Tactic:
intro z0 z1 zs
State after:
case mp.fa0
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
⊢ AnalyticAt ℂ (fun z0 => f (z0, z1)) z0

State before:
case mp.fa0
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
⊢ AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
Tactic:
rcases Metric.isOpen_iff.mp o (z0, z1) zs with ⟨r, rp, rs⟩
State after:
case mp.fa0.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ AnalyticAt ℂ (fun z0 => f (z0, z1)) z0

State before:
case mp.fa0.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
Tactic:
have d0 : DifferentiableOn ℂ (fun z0 ↦ f (z0, z1)) (ball z0 r) := by
  apply DifferentiableOn.comp d
  exact DifferentiableOn.prod differentiableOn_id (differentiableOn_const _)
  intro z0 z0s; apply rs; simp at z0s ⊢; assumption
State after:
case mp.fa0.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
d0 : DifferentiableOn ℂ (fun z0 => f (z0, z1)) (ball z0 r)
⊢ AnalyticAt ℂ (fun z0 => f (z0, z1)) z0

State before:
case mp.fa0.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
d0 : DifferentiableOn ℂ (fun z0 => f (z0, z1)) (ball z0 r)
⊢ AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
Tactic:
exact (analyticOn_iff_differentiableOn isOpen_ball).mpr d0 z0 (Metric.mem_ball_self rp)
State after:
no goals

State before:
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ DifferentiableOn ℂ (fun z0 => f (z0, z1)) (ball z0 r)
Tactic:
apply DifferentiableOn.comp d
State after:
case hf
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ DifferentiableOn ℂ (fun z0 => (z0, z1)) (ball z0 r)

case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ Set.MapsTo (fun z0 => (z0, z1)) (ball z0 r) s

State before:
case hf
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ DifferentiableOn ℂ (fun z0 => (z0, z1)) (ball z0 r)

case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ Set.MapsTo (fun z0 => (z0, z1)) (ball z0 r) s
Tactic:
exact DifferentiableOn.prod differentiableOn_id (differentiableOn_const _)
State after:
case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ Set.MapsTo (fun z0 => (z0, z1)) (ball z0 r) s

State before:
case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ Set.MapsTo (fun z0 => (z0, z1)) (ball z0 r) s
Tactic:
intro z0 z0s
State after:
case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0✝ z1 : ℂ
zs : (z0✝, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0✝, z1) r ⊆ s
z0 : ℂ
z0s : z0 ∈ ball z0✝ r
⊢ (fun z0 => (z0, z1)) z0 ∈ s

State before:
case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0✝ z1 : ℂ
zs : (z0✝, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0✝, z1) r ⊆ s
z0 : ℂ
z0s : z0 ∈ ball z0✝ r
⊢ (fun z0 => (z0, z1)) z0 ∈ s
Tactic:
apply rs
State after:
case st.a
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0✝ z1 : ℂ
zs : (z0✝, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0✝, z1) r ⊆ s
z0 : ℂ
z0s : z0 ∈ ball z0✝ r
⊢ (fun z0 => (z0, z1)) z0 ∈ ball (z0✝, z1) r

State before:
case st.a
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0✝ z1 : ℂ
zs : (z0✝, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0✝, z1) r ⊆ s
z0 : ℂ
z0s : z0 ∈ ball z0✝ r
⊢ (fun z0 => (z0, z1)) z0 ∈ ball (z0✝, z1) r
Tactic:
simp at z0s ⊢
State after:
case st.a
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0✝ z1 : ℂ
zs : (z0✝, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0✝, z1) r ⊆ s
z0 : ℂ
z0s : dist z0 z0✝ < r
⊢ dist z0 z0✝ < r

State before:
case st.a
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0✝ z1 : ℂ
zs : (z0✝, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0✝, z1) r ⊆ s
z0 : ℂ
z0s : dist z0 z0✝ < r
⊢ dist z0 z0✝ < r
Tactic:
assumption
State after:
no goals

State before:
case mp.fa1
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
⊢ ∀ (z0 z1 : ℂ), (z0, z1) ∈ s → AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
Tactic:
intro z0 z1 zs
State after:
case mp.fa1
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
⊢ AnalyticAt ℂ (fun z1 => f (z0, z1)) z1

State before:
case mp.fa1
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
⊢ AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
Tactic:
rcases Metric.isOpen_iff.mp o (z0, z1) zs with ⟨r, rp, rs⟩
State after:
case mp.fa1.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ AnalyticAt ℂ (fun z1 => f (z0, z1)) z1

State before:
case mp.fa1.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
Tactic:
have d1 : DifferentiableOn ℂ (fun z1 ↦ f (z0, z1)) (ball z1 r) := by
  apply DifferentiableOn.comp d
  exact DifferentiableOn.prod (differentiableOn_const _) differentiableOn_id
  intro z1 z1s; apply rs; simp at z1s ⊢; assumption
State after:
case mp.fa1.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
d1 : DifferentiableOn ℂ (fun z1 => f (z0, z1)) (ball z1 r)
⊢ AnalyticAt ℂ (fun z1 => f (z0, z1)) z1

State before:
case mp.fa1.intro.intro
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
d1 : DifferentiableOn ℂ (fun z1 => f (z0, z1)) (ball z1 r)
⊢ AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
Tactic:
exact (analyticOn_iff_differentiableOn isOpen_ball).mpr d1 z1 (Metric.mem_ball_self rp)
State after:
no goals

State before:
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ DifferentiableOn ℂ (fun z1 => f (z0, z1)) (ball z1 r)
Tactic:
apply DifferentiableOn.comp d
State after:
case hf
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ DifferentiableOn ℂ (fun z1 => (z0, z1)) (ball z1 r)

case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ Set.MapsTo (fun z1 => (z0, z1)) (ball z1 r) s

State before:
case hf
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ DifferentiableOn ℂ (fun z1 => (z0, z1)) (ball z1 r)

case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ Set.MapsTo (fun z1 => (z0, z1)) (ball z1 r) s
Tactic:
exact DifferentiableOn.prod (differentiableOn_const _) differentiableOn_id
State after:
case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ Set.MapsTo (fun z1 => (z0, z1)) (ball z1 r) s

State before:
case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1 : ℂ
zs : (z0, z1) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1) r ⊆ s
⊢ Set.MapsTo (fun z1 => (z0, z1)) (ball z1 r) s
Tactic:
intro z1 z1s
State after:
case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1✝ : ℂ
zs : (z0, z1✝) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1✝) r ⊆ s
z1 : ℂ
z1s : z1 ∈ ball z1✝ r
⊢ (fun z1 => (z0, z1)) z1 ∈ s

State before:
case st
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1✝ : ℂ
zs : (z0, z1✝) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1✝) r ⊆ s
z1 : ℂ
z1s : z1 ∈ ball z1✝ r
⊢ (fun z1 => (z0, z1)) z1 ∈ s
Tactic:
apply rs
State after:
case st.a
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1✝ : ℂ
zs : (z0, z1✝) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1✝) r ⊆ s
z1 : ℂ
z1s : z1 ∈ ball z1✝ r
⊢ (fun z1 => (z0, z1)) z1 ∈ ball (z0, z1✝) r

State before:
case st.a
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1✝ : ℂ
zs : (z0, z1✝) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1✝) r ⊆ s
z1 : ℂ
z1s : z1 ∈ ball z1✝ r
⊢ (fun z1 => (z0, z1)) z1 ∈ ball (z0, z1✝) r
Tactic:
simp at z1s ⊢
State after:
case st.a
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1✝ : ℂ
zs : (z0, z1✝) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1✝) r ⊆ s
z1 : ℂ
z1s : dist z1 z1✝ < r
⊢ dist z1 z1✝ < r

State before:
case st.a
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
d : DifferentiableOn ℂ f s
z0 z1✝ : ℂ
zs : (z0, z1✝) ∈ s
r : ℝ
rp : r > 0
rs : ball (z0, z1✝) r ⊆ s
z1 : ℂ
z1s : dist z1 z1✝ < r
⊢ dist z1 z1✝ < r
Tactic:
assumption
State after:
no goals

State before:
case mpr
E✝ : Type
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace ℂ E✝
inst✝⁶ : CompleteSpace E✝
F : Type
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
E : Type
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
o : IsOpen s
⊢ AnalyticOn ℂ f s → DifferentiableOn ℂ f s
Tactic:
exact fun a ↦ a.differentiableOn
State after:
no goals