Theorem: Har.on0 (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 : ℝ
h : Har f (closedBall (c0, c1) r)
z1r : z1 ∈ closedBall c1 r
⊢ AnalyticOn ℂ (fun z0 => f (z0, z1)) (closedBall c0 r)
Tactic:
intro z0 z0s
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 : ℝ
h : Har f (closedBall (c0, c1) r)
z1r : z1 ∈ closedBall c1 r
z0 : ℂ
z0s : z0 ∈ closedBall c0 r
⊢ AnalyticAt ℂ (fun z0 => f (z0, z1)) z0

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 : ℝ
h : Har f (closedBall (c0, c1) r)
z1r : z1 ∈ closedBall c1 r
z0 : ℂ
z0s : z0 ∈ closedBall c0 r
⊢ AnalyticAt ℂ (fun z0 => f (z0, z1)) z0
Tactic:
apply h.fa0 z0 z1
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 : ℝ
h : Har f (closedBall (c0, c1) r)
z1r : z1 ∈ closedBall c1 r
z0 : ℂ
z0s : z0 ∈ closedBall c0 r
⊢ (z0, z1) ∈ closedBall (c0, c1) 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 : ℝ
h : Har f (closedBall (c0, c1) r)
z1r : z1 ∈ closedBall c1 r
z0 : ℂ
z0s : z0 ∈ closedBall c0 r
⊢ (z0, z1) ∈ closedBall (c0, c1) r
Tactic:
rw [← closedBall_prod_same]
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 : ℝ
h : Har f (closedBall (c0, c1) r)
z1r : z1 ∈ closedBall c1 r
z0 : ℂ
z0s : z0 ∈ closedBall c0 r
⊢ (z0, z1) ∈ closedBall c0 r ×ˢ closedBall c1 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 : ℝ
h : Har f (closedBall (c0, c1) r)
z1r : z1 ∈ closedBall c1 r
z0 : ℂ
z0s : z0 ∈ closedBall c0 r
⊢ (z0, z1) ∈ closedBall c0 r ×ˢ closedBall c1 r
Tactic:
simp only [Set.prod_mk_mem_set_prod_eq, Metric.mem_closedBall] at z0s ⊢
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 : ℝ
h : Har f (closedBall (c0, c1) r)
z1r : z1 ∈ closedBall c1 r
z0 : ℂ
z0s : dist z0 c0 ≤ r
⊢ dist z0 c0 ≤ r ∧ dist z1 c1 ≤ 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 : ℝ
h : Har f (closedBall (c0, c1) r)
z1r : z1 ∈ closedBall c1 r
z0 : ℂ
z0s : dist z0 c0 ≤ r
⊢ dist z0 c0 ≤ r ∧ dist z1 c1 ≤ r
Tactic:
exact ⟨z0s, z1r⟩
State after:
no goals