Theorem: on_subdisk (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)
rp : r > 0
ep : e > 0
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
set re := min r e
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball 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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
have esub : closedBall c0 re ⊆ closedBall c0 r :=
  Metric.closedBall_subset_closedBall (min_le_left _ _)
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball 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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
generalize hS : (fun b : ℕ ↦
  {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1, z1 ∈ closedBall c1 r → ‖f (z0, z1)‖ ≤ b}) = 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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball 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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
have hU : (interior (⋃ b, S b)).Nonempty := by
  refine Set.nonempty_of_mem
      (mem_interior.mpr ⟨ball c0 re, ?_, Metric.isOpen_ball, Metric.mem_ball_self (lt_min rp ep)⟩)
  rw [Set.subset_def]; intro z0 z0s; rw [Set.mem_iUnion]
  have z0s' := esub (mem_open_closed z0s)
  rcases (isCompact_closedBall _ _).bddAbove_image (h.on1 z0s').continuousOn.norm with ⟨b, fb⟩
  simp only [mem_upperBounds, Set.forall_mem_image] at fb
  use Nat.ceil b; rw [← hS]; simp only [Set.mem_setOf]
  refine ⟨mem_open_closed z0s, ?_⟩
  simp only [Metric.mem_closedBall] at fb ⊢; intro z1 z1r
  exact _root_.trans (fb z1r) (Nat.le_ceil _)
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball 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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
rcases NonemptyInterior.nonempty_interior_of_iUnion_of_closed hc hU with ⟨b, bi⟩
State after:
case 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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
bi : (interior (S b)).Nonempty
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)

State before:
case 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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
bi : (interior (S b)).Nonempty
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
rcases bi with ⟨c0', c0's⟩
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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)

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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
⊢ ∃ c0', ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
use c0'
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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
⊢ ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)

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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
⊢ ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
rcases mem_interior.mp c0's with ⟨s', s's, so, c0s'⟩
State after:
case h.intro.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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
⊢ ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)

State before:
case h.intro.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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
⊢ ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
rcases Metric.isOpen_iff.mp so c0' c0s' with ⟨t, tp, ts⟩
State after:
case h.intro.intro.intro.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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
⊢ ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)

State before:
case h.intro.intro.intro.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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
⊢ ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
have tr : ball c0' t ⊆ closedBall c0 re := by
  rw [Set.subset_def]; intro z0 z0t
  have z0b := _root_.trans ts s's z0t
  rw [← hS] at z0b; simp only [Set.setOf_and, Set.setOf_mem_eq, Set.mem_inter_iff] at z0b
  exact z0b.left
State after:
case h.intro.intro.intro.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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
⊢ ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)

State before:
case h.intro.intro.intro.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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
⊢ ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
have c0e : c0' ∈ closedBall c0 e :=
  _root_.trans tr (Metric.closedBall_subset_closedBall (min_le_right _ _))
    (Metric.mem_ball_self tp)
State after:
case h.intro.intro.intro.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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
⊢ ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)

State before:
case h.intro.intro.intro.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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
⊢ ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
have fb : ∀ z, z ∈ ball c0' t ×ˢ ball c1 r → ‖f z‖ ≤ b := by
  intro z zs; rw [Set.mem_prod] at zs
  have zb := _root_.trans ts s's zs.left
  rw [← hS] at zb
  simp only [Metric.mem_ball, Metric.mem_closedBall, le_min_iff, Set.mem_setOf_eq] at zb zs
  have zb' := zb.right z.snd zs.right.le
  simp only [Prod.mk.eta] at zb'; exact zb'
State after:
case h.intro.intro.intro.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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
fb : ∀ z ∈ ball c0' t ×ˢ ball c1 r, ‖f z‖ ≤ ↑b
⊢ ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)

State before:
case h.intro.intro.intro.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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
fb : ∀ z ∈ ball c0' t ×ˢ ball c1 r, ‖f z‖ ≤ ↑b
⊢ ∃ t > 0, c0' ∈ closedBall c0 e ∧ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
use t, tp, c0e
State after:
case right
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
fb : ∀ z ∈ ball c0' t ×ˢ ball c1 r, ‖f z‖ ≤ ↑b
⊢ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)

State before:
case right
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
fb : ∀ z ∈ ball c0' t ×ˢ ball c1 r, ‖f z‖ ≤ ↑b
⊢ AnalyticOn ℂ f (ball c0' t ×ˢ ball c1 r)
Tactic:
refine of_bounded (h.mono ?_) (IsOpen.prod isOpen_ball isOpen_ball) fb
State after:
case right
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
fb : ∀ z ∈ ball c0' t ×ˢ ball c1 r, ‖f z‖ ≤ ↑b
⊢ ball c0' t ×ˢ ball c1 r ⊆ closedBall (c0, c1) r

State before:
case right
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
fb : ∀ z ∈ ball c0' t ×ˢ ball c1 r, ‖f z‖ ≤ ↑b
⊢ ball c0' t ×ˢ ball c1 r ⊆ closedBall (c0, c1) r
Tactic:
rw [← closedBall_prod_same]
State after:
case right
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
fb : ∀ z ∈ ball c0' t ×ˢ ball c1 r, ‖f z‖ ≤ ↑b
⊢ ball c0' t ×ˢ ball c1 r ⊆ closedBall c0 r ×ˢ closedBall c1 r

State before:
case right
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
fb : ∀ z ∈ ball c0' t ×ˢ ball c1 r, ‖f z‖ ≤ ↑b
⊢ ball c0' t ×ˢ ball c1 r ⊆ closedBall c0 r ×ˢ closedBall c1 r
Tactic:
exact Set.prod_mono (_root_.trans tr esub) Metric.ball_subset_closedBall
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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
⊢ ∀ (b : ℕ), IsClosed (S b)
Tactic:
intro b
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
⊢ IsClosed (S b)

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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
⊢ IsClosed (S b)
Tactic:
rw [← hS]
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
⊢ IsClosed ((fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) b)

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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
⊢ IsClosed ((fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) b)
Tactic:
simp only [← forall_const_and_distrib]
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
⊢ IsClosed {z0 | ∀ (x : ℂ), z0 ∈ closedBall c0 re ∧ (x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ ↑b)}

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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
⊢ IsClosed {z0 | ∀ (x : ℂ), z0 ∈ closedBall c0 re ∧ (x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ ↑b)}
Tactic:
rw [Set.setOf_forall]
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
⊢ IsClosed (⋂ i, {x | x ∈ closedBall c0 re ∧ (i ∈ closedBall c1 r → ‖f (x, i)‖ ≤ ↑b)})

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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
⊢ IsClosed (⋂ i, {x | x ∈ closedBall c0 re ∧ (i ∈ closedBall c1 r → ‖f (x, i)‖ ≤ ↑b)})
Tactic:
apply isClosed_iInter
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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
⊢ ∀ (i : ℂ), IsClosed {x | x ∈ closedBall c0 re ∧ (i ∈ closedBall c1 r → ‖f (x, i)‖ ≤ ↑b)}

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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
⊢ ∀ (i : ℂ), IsClosed {x | x ∈ closedBall c0 re ∧ (i ∈ closedBall c1 r → ‖f (x, i)‖ ≤ ↑b)}
Tactic:
intro z1
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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
⊢ IsClosed {x | x ∈ closedBall c0 re ∧ (z1 ∈ closedBall c1 r → ‖f (x, z1)‖ ≤ ↑b)}

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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
⊢ IsClosed {x | x ∈ closedBall c0 re ∧ (z1 ∈ closedBall c1 r → ‖f (x, z1)‖ ≤ ↑b)}
Tactic:
by_cases z1r : z1 ∉ closedBall c1 r
State after:
case pos
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : z1 ∉ closedBall c1 r
⊢ IsClosed {x | x ∈ closedBall c0 re ∧ (z1 ∈ closedBall c1 r → ‖f (x, z1)‖ ≤ ↑b)}

case neg
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : ¬z1 ∉ closedBall c1 r
⊢ IsClosed {x | x ∈ closedBall c0 re ∧ (z1 ∈ closedBall c1 r → ‖f (x, z1)‖ ≤ ↑b)}

State before:
case pos
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : z1 ∉ closedBall c1 r
⊢ IsClosed {x | x ∈ closedBall c0 re ∧ (z1 ∈ closedBall c1 r → ‖f (x, z1)‖ ≤ ↑b)}
Tactic:
simp only [z1r, false_imp_iff, and_true_iff, Set.setOf_mem_eq, Metric.isClosed_ball]
State after:
no goals

State before:
case neg
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : ¬z1 ∉ closedBall c1 r
⊢ IsClosed {x | x ∈ closedBall c0 re ∧ (z1 ∈ closedBall c1 r → ‖f (x, z1)‖ ≤ ↑b)}
Tactic:
rw [Set.not_not_mem] at z1r
State after:
case neg
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : z1 ∈ closedBall c1 r
⊢ IsClosed {x | x ∈ closedBall c0 re ∧ (z1 ∈ closedBall c1 r → ‖f (x, z1)‖ ≤ ↑b)}

State before:
case neg
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : z1 ∈ closedBall c1 r
⊢ IsClosed {x | x ∈ closedBall c0 re ∧ (z1 ∈ closedBall c1 r → ‖f (x, z1)‖ ≤ ↑b)}
Tactic:
simp only [z1r, true_imp_iff]
State after:
case neg
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : z1 ∈ closedBall c1 r
⊢ IsClosed {x | x ∈ closedBall c0 re ∧ ‖f (x, z1)‖ ≤ ↑b}

State before:
case neg
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : z1 ∈ closedBall c1 r
⊢ IsClosed {x | x ∈ closedBall c0 re ∧ ‖f (x, z1)‖ ≤ ↑b}
Tactic:
refine ContinuousOn.isClosed_le Metric.isClosed_ball ?_ continuousOn_const
State after:
case neg
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : z1 ∈ closedBall c1 r
⊢ ContinuousOn (fun x => ‖f (x, z1)‖) (closedBall c0 re)

State before:
case neg
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : z1 ∈ closedBall c1 r
⊢ ContinuousOn (fun x => ‖f (x, z1)‖) (closedBall c0 re)
Tactic:
apply ContinuousOn.norm
State after:
case neg.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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : z1 ∈ closedBall c1 r
⊢ ContinuousOn (fun x => f (x, z1)) (closedBall c0 re)

State before:
case neg.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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
b : ℕ
z1 : ℂ
z1r : z1 ∈ closedBall c1 r
⊢ ContinuousOn (fun x => f (x, z1)) (closedBall c0 re)
Tactic:
exact ContinuousOn.mono (h.on0 z1r).continuousOn esub
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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
⊢ (interior (⋃ b, S b)).Nonempty
Tactic:
refine Set.nonempty_of_mem
    (mem_interior.mpr ⟨ball c0 re, ?_, Metric.isOpen_ball, Metric.mem_ball_self (lt_min rp ep)⟩)
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
⊢ ball c0 re ⊆ ⋃ b, S b

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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
⊢ ball c0 re ⊆ ⋃ b, S b
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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
⊢ ∀ x ∈ ball c0 re, x ∈ ⋃ b, S b

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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
⊢ ∀ x ∈ ball c0 re, x ∈ ⋃ b, S b
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
⊢ z0 ∈ ⋃ b, S b

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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
⊢ z0 ∈ ⋃ b, S b
Tactic:
rw [Set.mem_iUnion]
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
⊢ ∃ i, z0 ∈ S i

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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
⊢ ∃ i, z0 ∈ S i
Tactic:
have z0s' := esub (mem_open_closed 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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
⊢ ∃ i, z0 ∈ S i

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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
⊢ ∃ i, z0 ∈ S i
Tactic:
rcases (isCompact_closedBall _ _).bddAbove_image (h.on1 z0s').continuousOn.norm with ⟨b, fb⟩
State after:
case 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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : b ∈ upperBounds ((fun x => ‖f (z0, x)‖) '' closedBall c1 r)
⊢ ∃ i, z0 ∈ S i

State before:
case 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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : b ∈ upperBounds ((fun x => ‖f (z0, x)‖) '' closedBall c1 r)
⊢ ∃ i, z0 ∈ S i
Tactic:
simp only [mem_upperBounds, Set.forall_mem_image] at fb
State after:
case 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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ b
⊢ ∃ i, z0 ∈ S i

State before:
case 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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ b
⊢ ∃ i, z0 ∈ S i
Tactic:
use Nat.ceil b
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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ b
⊢ z0 ∈ S ⌈b⌉₊

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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ b
⊢ z0 ∈ S ⌈b⌉₊
Tactic:
rw [← hS]
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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ b
⊢ z0 ∈ (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) ⌈b⌉₊

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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ b
⊢ z0 ∈ (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) ⌈b⌉₊
Tactic:
simp only [Set.mem_setOf]
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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ b
⊢ z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑⌈b⌉₊

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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ b
⊢ z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑⌈b⌉₊
Tactic:
refine ⟨mem_open_closed z0s, ?_⟩
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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ b
⊢ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑⌈b⌉₊

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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, x ∈ closedBall c1 r → ‖f (z0, x)‖ ≤ b
⊢ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑⌈b⌉₊
Tactic:
simp only [Metric.mem_closedBall] at fb ⊢
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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, dist x c1 ≤ r → ‖f (z0, x)‖ ≤ b
⊢ ∀ (z1 : ℂ), dist z1 c1 ≤ r → ‖f (z0, z1)‖ ≤ ↑⌈b⌉₊

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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, dist x c1 ≤ r → ‖f (z0, x)‖ ≤ b
⊢ ∀ (z1 : ℂ), dist z1 c1 ≤ r → ‖f (z0, z1)‖ ≤ ↑⌈b⌉₊
Tactic:
intro z1 z1r
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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, dist x c1 ≤ r → ‖f (z0, x)‖ ≤ b
z1 : ℂ
z1r : dist z1 c1 ≤ r
⊢ ‖f (z0, z1)‖ ≤ ↑⌈b⌉₊

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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
z0 : ℂ
z0s : z0 ∈ ball c0 re
z0s' : z0 ∈ closedBall c0 r
b : ℝ
fb : ∀ ⦃x : ℂ⦄, dist x c1 ≤ r → ‖f (z0, x)‖ ≤ b
z1 : ℂ
z1r : dist z1 c1 ≤ r
⊢ ‖f (z0, z1)‖ ≤ ↑⌈b⌉₊
Tactic:
exact _root_.trans (fb z1r) (Nat.le_ceil _)
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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
⊢ ball c0' t ⊆ closedBall c0 re
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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
⊢ ∀ x ∈ ball c0' t, x ∈ closedBall c0 re

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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
⊢ ∀ x ∈ ball c0' t, x ∈ closedBall c0 re
Tactic:
intro z0 z0t
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
z0 : ℂ
z0t : z0 ∈ ball c0' t
⊢ z0 ∈ closedBall c0 re

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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
z0 : ℂ
z0t : z0 ∈ ball c0' t
⊢ z0 ∈ closedBall c0 re
Tactic:
have z0b := _root_.trans ts s's z0t
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
z0 : ℂ
z0t : z0 ∈ ball c0' t
z0b : z0 ∈ S b
⊢ z0 ∈ closedBall c0 re

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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
z0 : ℂ
z0t : z0 ∈ ball c0' t
z0b : z0 ∈ S b
⊢ z0 ∈ closedBall c0 re
Tactic:
rw [← hS] at z0b
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
z0 : ℂ
z0t : z0 ∈ ball c0' t
z0b : z0 ∈ (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) b
⊢ z0 ∈ closedBall c0 re

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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
z0 : ℂ
z0t : z0 ∈ ball c0' t
z0b : z0 ∈ (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) b
⊢ z0 ∈ closedBall c0 re
Tactic:
simp only [Set.setOf_and, Set.setOf_mem_eq, Set.mem_inter_iff] at z0b
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
z0 : ℂ
z0t : z0 ∈ ball c0' t
z0b : z0 ∈ closedBall c0 re ∧ z0 ∈ {a | ∀ z1 ∈ closedBall c1 r, ‖f (a, z1)‖ ≤ ↑b}
⊢ z0 ∈ closedBall c0 re

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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
z0 : ℂ
z0t : z0 ∈ ball c0' t
z0b : z0 ∈ closedBall c0 re ∧ z0 ∈ {a | ∀ z1 ∈ closedBall c1 r, ‖f (a, z1)‖ ≤ ↑b}
⊢ z0 ∈ closedBall c0 re
Tactic:
exact z0b.left
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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
⊢ ∀ z ∈ ball c0' t ×ˢ ball c1 r, ‖f z‖ ≤ ↑b
Tactic:
intro z zs
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zs : z ∈ ball c0' t ×ˢ ball c1 r
⊢ ‖f z‖ ≤ ↑b

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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zs : z ∈ ball c0' t ×ˢ ball c1 r
⊢ ‖f z‖ ≤ ↑b
Tactic:
rw [Set.mem_prod] at zs
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zs : z.1 ∈ ball c0' t ∧ z.2 ∈ ball c1 r
⊢ ‖f z‖ ≤ ↑b

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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zs : z.1 ∈ ball c0' t ∧ z.2 ∈ ball c1 r
⊢ ‖f z‖ ≤ ↑b
Tactic:
have zb := _root_.trans ts s's zs.left
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zs : z.1 ∈ ball c0' t ∧ z.2 ∈ ball c1 r
zb : z.1 ∈ S b
⊢ ‖f z‖ ≤ ↑b

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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zs : z.1 ∈ ball c0' t ∧ z.2 ∈ ball c1 r
zb : z.1 ∈ S b
⊢ ‖f z‖ ≤ ↑b
Tactic:
rw [← hS] at zb
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zs : z.1 ∈ ball c0' t ∧ z.2 ∈ ball c1 r
zb : z.1 ∈ (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) b
⊢ ‖f z‖ ≤ ↑b

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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zs : z.1 ∈ ball c0' t ∧ z.2 ∈ ball c1 r
zb : z.1 ∈ (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) b
⊢ ‖f z‖ ≤ ↑b
Tactic:
simp only [Metric.mem_ball, Metric.mem_closedBall, le_min_iff, Set.mem_setOf_eq] at zb zs
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zb : dist z.1 c0 ≤ re ∧ ∀ (z1 : ℂ), dist z1 c1 ≤ r → ‖f (z.1, z1)‖ ≤ ↑b
zs : dist z.1 c0' < t ∧ dist z.2 c1 < r
⊢ ‖f z‖ ≤ ↑b

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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zb : dist z.1 c0 ≤ re ∧ ∀ (z1 : ℂ), dist z1 c1 ≤ r → ‖f (z.1, z1)‖ ≤ ↑b
zs : dist z.1 c0' < t ∧ dist z.2 c1 < r
⊢ ‖f z‖ ≤ ↑b
Tactic:
have zb' := zb.right z.snd zs.right.le
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zb : dist z.1 c0 ≤ re ∧ ∀ (z1 : ℂ), dist z1 c1 ≤ r → ‖f (z.1, z1)‖ ≤ ↑b
zs : dist z.1 c0' < t ∧ dist z.2 c1 < r
zb' : ‖f (z.1, z.2)‖ ≤ ↑b
⊢ ‖f z‖ ≤ ↑b

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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zb : dist z.1 c0 ≤ re ∧ ∀ (z1 : ℂ), dist z1 c1 ≤ r → ‖f (z.1, z1)‖ ≤ ↑b
zs : dist z.1 c0' < t ∧ dist z.2 c1 < r
zb' : ‖f (z.1, z.2)‖ ≤ ↑b
⊢ ‖f z‖ ≤ ↑b
Tactic:
simp only [Prod.mk.eta] at zb'
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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zb : dist z.1 c0 ≤ re ∧ ∀ (z1 : ℂ), dist z1 c1 ≤ r → ‖f (z.1, z1)‖ ≤ ↑b
zs : dist z.1 c0' < t ∧ dist z.2 c1 < r
zb' : ‖f z‖ ≤ ↑b
⊢ ‖f z‖ ≤ ↑b

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)
rp : r > 0
ep : e > 0
re : ℝ := min r e
esub : closedBall c0 re ⊆ closedBall c0 r
S : ℕ → Set ℂ
hS : (fun b => {z0 | z0 ∈ closedBall c0 re ∧ ∀ z1 ∈ closedBall c1 r, ‖f (z0, z1)‖ ≤ ↑b}) = S
hc : ∀ (b : ℕ), IsClosed (S b)
hU : (interior (⋃ b, S b)).Nonempty
b : ℕ
c0' : ℂ
c0's : c0' ∈ interior (S b)
s' : Set ℂ
s's : s' ⊆ S b
so : IsOpen s'
c0s' : c0' ∈ s'
t : ℝ
tp : t > 0
ts : ball c0' t ⊆ s'
tr : ball c0' t ⊆ closedBall c0 re
c0e : c0' ∈ closedBall c0 e
z : ℂ × ℂ
zb : dist z.1 c0 ≤ re ∧ ∀ (z1 : ℂ), dist z1 c1 ≤ r → ‖f (z.1, z1)‖ ≤ ↑b
zs : dist z.1 c0' < t ∧ dist z.2 c1 < r
zb' : ‖f z‖ ≤ ↑b
⊢ ‖f z‖ ≤ ↑b
Tactic:
exact zb'
State after:
no goals