Theorem: Har.on1 (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)
z0r : z0 ∈ closedBall c0 r
⊢ AnalyticOn ℂ (fun z1 => f (z0, z1)) (closedBall c1 r)
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 : ℝ
h : Har f (closedBall (c0, c1) r)
z0r : z0 ∈ closedBall c0 r
z1 : ℂ
z1s : z1 ∈ closedBall c1 r
⊢ AnalyticAt ℂ (fun z1 => f (z0, z1)) 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 : ℝ
h : Har f (closedBall (c0, c1) r)
z0r : z0 ∈ closedBall c0 r
z1 : ℂ
z1s : z1 ∈ closedBall c1 r
⊢ AnalyticAt ℂ (fun z1 => f (z0, z1)) z1
Tactic:
apply h.fa1 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)
z0r : z0 ∈ closedBall c0 r
z1 : ℂ
z1s : z1 ∈ closedBall c1 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)
z0r : z0 ∈ closedBall c0 r
z1 : ℂ
z1s : z1 ∈ closedBall c1 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)
z0r : z0 ∈ closedBall c0 r
z1 : ℂ
z1s : z1 ∈ closedBall c1 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)
z0r : z0 ∈ closedBall c0 r
z1 : ℂ
z1s : z1 ∈ closedBall c1 r
⊢ (z0, z1) ∈ closedBall c0 r ×ˢ closedBall c1 r
Tactic:
simp only [Set.prod_mk_mem_set_prod_eq, Metric.mem_closedBall] 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 : ℝ
h : Har f (closedBall (c0, c1) r)
z0r : z0 ∈ closedBall c0 r
z1 : ℂ
z1s : dist z1 c1 ≤ 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)
z0r : z0 ∈ closedBall c0 r
z1 : ℂ
z1s : dist z1 c1 ≤ r
⊢ dist z0 c0 ≤ r ∧ dist z1 c1 ≤ r
Tactic:
exact ⟨z0r, z1s⟩
State after:
no goals