Theorem: Pair.hartogs (Ray/Hartogs/Hartogs.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
⊢ AnalyticOn ℂ f s
Tactic:
have h : Har f s := ⟨fa0, fa1⟩
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
⊢ AnalyticOn ℂ f s

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
⊢ AnalyticOn ℂ f s
Tactic:
intro c cs
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
⊢ AnalyticAt ℂ f c

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
⊢ AnalyticAt ℂ f c
Tactic:
rcases Metric.isOpen_iff.mp so c cs with ⟨r, rp, rs⟩
State after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
⊢ AnalyticAt ℂ f c

State before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
⊢ AnalyticAt ℂ f c
Tactic:
rcases exists_between rp with ⟨t, tp, tr⟩
State after:
case intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
⊢ AnalyticAt ℂ f c

State before:
case intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
⊢ AnalyticAt ℂ f c
Tactic:
have bs : closedBall (c.1, c.2) t ⊆ s := by
  refine _root_.trans ?_ rs; simp only [fst_snd_eq]; exact Metric.closedBall_subset_ball tr
State after:
case intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
⊢ AnalyticAt ℂ f c

State before:
case intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
⊢ AnalyticAt ℂ f c
Tactic:
rcases to_uneven (h.mono bs) tp with ⟨c0', r0, r1, us, c0s, u⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
⊢ AnalyticAt ℂ f c

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
⊢ AnalyticAt ℂ f c
Tactic:
have cr : abs (c.1 - c0') < r1 := by
  simp only [Complex.dist_eq, Metric.mem_ball] at c0s; exact c0s
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
⊢ AnalyticAt ℂ f c

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
⊢ AnalyticAt ℂ f c
Tactic:
rcases exists_between cr with ⟨v, vc, vr⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
⊢ AnalyticAt ℂ f c

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
⊢ AnalyticAt ℂ f c
Tactic:
rcases uneven_bounded u (lt_of_le_of_lt (Complex.abs.nonneg _) vc) vr with ⟨b, _, fb⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ AnalyticAt ℂ f c

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ AnalyticAt ℂ f c
Tactic:
have fa := of_bounded (h.mono ?_) Metric.isOpen_ball fb
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
fa : AnalyticOn ℂ f (ball (c0', c.2) v)
⊢ AnalyticAt ℂ f c

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ ball (c0', c.2) v ⊆ s

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
⊢ closedBall (c.1, c.2) t ⊆ s
Tactic:
refine _root_.trans ?_ rs
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
⊢ closedBall (c.1, c.2) t ⊆ ball c r

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
⊢ closedBall (c.1, c.2) t ⊆ ball c r
Tactic:
simp only [fst_snd_eq]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
⊢ closedBall c t ⊆ ball c r

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
⊢ closedBall c t ⊆ ball c r
Tactic:
exact Metric.closedBall_subset_ball tr
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
⊢ Complex.abs (c.1 - c0') < r1
Tactic:
simp only [Complex.dist_eq, Metric.mem_ball] at c0s
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
u : Uneven f c0' c.2 r0 r1
c0s : Complex.abs (c.1 - c0') < r1
⊢ Complex.abs (c.1 - c0') < r1

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
u : Uneven f c0' c.2 r0 r1
c0s : Complex.abs (c.1 - c0') < r1
⊢ Complex.abs (c.1 - c0') < r1
Tactic:
exact c0s
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
fa : AnalyticOn ℂ f (ball (c0', c.2) v)
⊢ AnalyticAt ℂ f c
Tactic:
apply fa
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
fa : AnalyticOn ℂ f (ball (c0', c.2) v)
⊢ c ∈ ball (c0', c.2) v

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
fa : AnalyticOn ℂ f (ball (c0', c.2) v)
⊢ c ∈ ball (c0', c.2) v
Tactic:
simp only [Metric.mem_ball, Prod.dist_eq, Complex.dist_eq, dist_self, ge_iff_le, apply_nonneg,
  max_eq_left, vc]
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ ball (c0', c.2) v ⊆ s
Tactic:
refine _root_.trans ?_ bs
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ ball (c0', c.2) v ⊆ closedBall (c.1, c.2) t

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ ball (c0', c.2) v ⊆ closedBall (c.1, c.2) t
Tactic:
simp_rw [← ball_prod_same, ← closedBall_prod_same, Set.prod_subset_prod_iff]
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ ball c0' v ⊆ closedBall c.1 t ∧ ball c.2 v ⊆ closedBall c.2 t ∨ ball c0' v = ∅ ∨ ball c.2 v = ∅

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ ball c0' v ⊆ closedBall c.1 t ∧ ball c.2 v ⊆ closedBall c.2 t ∨ ball c0' v = ∅ ∨ ball c.2 v = ∅
Tactic:
apply Or.inl
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ ball c0' v ⊆ closedBall c.1 t ∧ ball c.2 v ⊆ closedBall c.2 t

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ ball c0' v ⊆ closedBall c.1 t ∧ ball c.2 v ⊆ closedBall c.2 t
Tactic:
use _root_.trans (Metric.ball_subset_ball vr.le) us
State after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ ball c.2 v ⊆ closedBall c.2 t

State before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ ball c.2 v ⊆ closedBall c.2 t
Tactic:
have r1t := le_of_ball_subset_closedBall u.r1p.le tp.le us
State after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
r1t : r1 ≤ t
⊢ ball c.2 v ⊆ closedBall c.2 t

State before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
r1t : r1 ≤ t
⊢ ball c.2 v ⊆ closedBall c.2 t
Tactic:
exact _root_.trans Metric.ball_subset_closedBall
    (Metric.closedBall_subset_closedBall (_root_.trans vr.le r1t))
State after:
no goals