Theorem: SuperAtC.superNearC' (Ray/Dynamics/BottcherNear.lean)

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
⊢ ∃ t ⊆ w, SuperNearC f d u t
Tactic:
set r := fun c : u ↦ choose (h _ c.mem)
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
⊢ ∃ t ⊆ w, SuperNearC f d u t

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
⊢ ∃ t ⊆ w, SuperNearC f d u t
Tactic:
set v := fun c : u ↦ ball (c : ℂ) (r c)
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
⊢ ∃ t ⊆ w, SuperNearC f d u t

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
⊢ ∃ t ⊆ w, SuperNearC f d u t
Tactic:
set t := fun c : u ↦ ball ((c : ℂ), (0 : ℂ)) (r c)
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
⊢ ∃ t ⊆ w, SuperNearC f d u t

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
⊢ ∃ t ⊆ w, SuperNearC f d u t
Tactic:
use⋃ c : u, t c
State after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
⊢ ⋃ c, t c ⊆ w ∧ SuperNearC f d u (⋃ c, t c)

State before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
e : u = ⋃ c, v c
⊢ ⋃ c, t c ⊆ w ∧ SuperNearC f d u (⋃ c, t c)
Tactic:
have tw : (⋃ c : u, t c) ⊆ w := by
  apply Set.iUnion_subset; intro i; rcases choose_spec (h _ i.mem) with ⟨_, _, rw, _⟩; exact rw
State after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
e : u = ⋃ c, v c
tw : ⋃ c, t c ⊆ w
⊢ ⋃ c, t c ⊆ w ∧ SuperNearC f d u (⋃ c, t c)

State before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
e : u = ⋃ c, v c
tw : ⋃ c, t c ⊆ w
⊢ ⋃ c, t c ⊆ w ∧ SuperNearC f d u (⋃ c, t c)
Tactic:
have si : ∀ c : u, SuperNearC f d (v c) (t c) := by
  intro i; rcases choose_spec (h _ i.mem) with ⟨_, _, _, s⟩; exact s
State after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
e : u = ⋃ c, v c
tw : ⋃ c, t c ⊆ w
si : ∀ (c : ↑u), SuperNearC f d (v c) (t c)
⊢ ⋃ c, t c ⊆ w ∧ SuperNearC f d u (⋃ c, t c)

State before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
e : u = ⋃ c, v c
tw : ⋃ c, t c ⊆ w
si : ∀ (c : ↑u), SuperNearC f d (v c) (t c)
⊢ ⋃ c, t c ⊆ w ∧ SuperNearC f d u (⋃ c, t c)
Tactic:
have s := SuperNearC.union si
State after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s✝ : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
e : u = ⋃ c, v c
tw : ⋃ c, t c ⊆ w
si : ∀ (c : ↑u), SuperNearC f d (v c) (t c)
s : SuperNearC f d (⋃ i, v i) (⋃ i, t i)
⊢ ⋃ c, t c ⊆ w ∧ SuperNearC f d u (⋃ c, t c)

State before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s✝ : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
e : u = ⋃ c, v c
tw : ⋃ c, t c ⊆ w
si : ∀ (c : ↑u), SuperNearC f d (v c) (t c)
s : SuperNearC f d (⋃ i, v i) (⋃ i, t i)
⊢ ⋃ c, t c ⊆ w ∧ SuperNearC f d u (⋃ c, t c)
Tactic:
rw [← e] at s
State after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s✝ : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
e : u = ⋃ c, v c
tw : ⋃ c, t c ⊆ w
si : ∀ (c : ↑u), SuperNearC f d (v c) (t c)
s : SuperNearC f d u (⋃ i, t i)
⊢ ⋃ c, t c ⊆ w ∧ SuperNearC f d u (⋃ c, t c)

State before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s✝ : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
e : u = ⋃ c, v c
tw : ⋃ c, t c ⊆ w
si : ∀ (c : ↑u), SuperNearC f d (v c) (t c)
s : SuperNearC f d u (⋃ i, t i)
⊢ ⋃ c, t c ⊆ w ∧ SuperNearC f d u (⋃ c, t c)
Tactic:
exact ⟨tw, s⟩
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
⊢ ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Tactic:
intro c m
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Tactic:
rcases(s.fa m).exists_ball_analyticOn with ⟨r0, r0p, fa⟩
State after:
case intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)

State before:
case intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Tactic:
rcases Metric.isOpen_iff.mp s.o c m with ⟨r1, r1p, rc⟩
State after:
case intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc : ball c r1 ⊆ u
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)

State before:
case intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc : ball c r1 ⊆ u
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Tactic:
set r2 := min r0 r1
State after:
case intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)

State before:
case intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Tactic:
have fa := fa.mono (Metric.ball_subset_ball (min_le_left r0 r1))
State after:
case intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)

State before:
case intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Tactic:
have rc : ball c r2 ⊆ u := le_trans (Metric.ball_subset_ball (by bound)) rc
State after:
case intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)

State before:
case intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Tactic:
have ga := s.ga_of_fa isOpen_ball fa
    (by intro p m; simp only [← ball_prod_same, Set.mem_prod] at m; exact rc m.1)
State after:
case intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)

State before:
case intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Tactic:
rcases Metric.isOpen_iff.mp wo (c, 0) (wc c m) with ⟨r3, r3p, rw⟩
State after:
case intro.intro.intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw : ball (c, 0) r3 ⊆ w
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)

State before:
case intro.intro.intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw : ball (c, 0) r3 ⊆ w
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Tactic:
rcases Metric.continuousAt_iff.mp (ga (c, 0) (mem_ball_self (by bound))).continuousAt
    (1 / 4) (by norm_num) with ⟨r4, r4p, gs⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Tactic:
set r := min (min r2 r3) (min r4 (1 / 2))
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Tactic:
have rp : 0 < r := by bound
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Tactic:
have rh : r ≤ 1 / 2 := le_trans (min_le_right _ _) (min_le_right _ _)
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Tactic:
have rr4 : r ≤ r4 := le_trans (min_le_right _ _) (min_le_left r4 _)
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Tactic:
have rc : ball c r ⊆ u := le_trans (Metric.ball_subset_ball (by bound)) rc
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Tactic:
have rw : ball (c, 0) r ⊆ w :=
  _root_.trans (Metric.ball_subset_ball (le_trans (min_le_left _ _) (min_le_right _ _))) rw
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
⊢ ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
Tactic:
use r, rp, rc, rw
State after:
case right
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
⊢ SuperNearC f d (ball c r) (ball (c, 0) r)

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
⊢ r2 ≤ r1
Tactic:
bound
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
⊢ ∀ {p : ℂ × ℂ}, p ∈ ball (c, 0) (min r0 r1) → p.1 ∈ u
Tactic:
intro p m
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
p : ℂ × ℂ
m : p ∈ ball (c, 0) (min r0 r1)
⊢ p.1 ∈ u

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
p : ℂ × ℂ
m : p ∈ ball (c, 0) (min r0 r1)
⊢ p.1 ∈ u
Tactic:
simp only [← ball_prod_same, Set.mem_prod] at m
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
p : ℂ × ℂ
m : p.1 ∈ ball c (min r0 r1) ∧ p.2 ∈ ball 0 (min r0 r1)
⊢ p.1 ∈ u

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
p : ℂ × ℂ
m : p.1 ∈ ball c (min r0 r1) ∧ p.2 ∈ ball 0 (min r0 r1)
⊢ p.1 ∈ u
Tactic:
exact rc m.1
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw : ball (c, 0) r3 ⊆ w
⊢ 0 < min r0 r1
Tactic:
bound
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw : ball (c, 0) r3 ⊆ w
⊢ 1 / 4 > 0
Tactic:
norm_num
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
⊢ 0 < r
Tactic:
bound
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
⊢ r ≤ r2
Tactic:
bound
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
⊢ ∀ {p : ℂ × ℂ}, p ∈ ball (c, 0) r → p.1 ∈ ball c r
Tactic:
intro p m
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
p : ℂ × ℂ
m : p ∈ ball (c, 0) r
⊢ p.1 ∈ ball c r

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
p : ℂ × ℂ
m : p ∈ ball (c, 0) r
⊢ p.1 ∈ ball c r
Tactic:
simp only [← ball_prod_same, Set.mem_prod] at m
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
p : ℂ × ℂ
m : p.1 ∈ ball c r ∧ p.2 ∈ ball 0 r
⊢ p.1 ∈ ball c r

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
p : ℂ × ℂ
m : p.1 ∈ ball c r ∧ p.2 ∈ ball 0 r
⊢ p.1 ∈ ball c r
Tactic:
exact Metric.ball_subset_ball (by linarith) m.1
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
p : ℂ × ℂ
m : p.1 ∈ ball c r ∧ p.2 ∈ ball 0 r
⊢ r ≤ r
Tactic:
linarith
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
⊢ ∀ {c_1 : ℂ}, c_1 ∈ ball c r → SuperNear (f c_1) d {z | (c_1, z) ∈ ball (c, 0) r}
Tactic:
intro c' m
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
⊢ SuperNear (f c') d {z | (c', z) ∈ ball (c, 0) r}

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
⊢ SuperNear (f c') d {z | (c', z) ∈ ball (c, 0) r}
Tactic:
simp only [← ball_prod_same, Set.mem_prod, m, true_and_iff]
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
⊢ SuperNear (f c') d {z | z ∈ ball 0 r}

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
⊢ SuperNear (f c') d {z | z ∈ ball 0 r}
Tactic:
apply (s.s (rc m)).super_on_ball rp rh
State after:
case fa
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
⊢ AnalyticOn ℂ (f c') (ball 0 r)

case gs
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
⊢ ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g (f c') d z - 1) < 1 / 4

State before:
case fa
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
⊢ AnalyticOn ℂ (f c') (ball 0 r)
Tactic:
apply fa.comp₂ analyticOn_const (analyticOn_id _)
State after:
case fa
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
⊢ ∀ x ∈ ball 0 r, (c', x) ∈ ball (c, 0) (min r0 r1)

State before:
case fa
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
⊢ ∀ x ∈ ball 0 r, (c', x) ∈ ball (c, 0) (min r0 r1)
Tactic:
intro z zm
State after:
case fa
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
z : ℂ
zm : z ∈ ball 0 r
⊢ (c', z) ∈ ball (c, 0) (min r0 r1)

State before:
case fa
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
z : ℂ
zm : z ∈ ball 0 r
⊢ (c', z) ∈ ball (c, 0) (min r0 r1)
Tactic:
apply Metric.ball_subset_ball (by bound : r ≤ r2)
State after:
case fa.a
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
z : ℂ
zm : z ∈ ball 0 r
⊢ (c', z) ∈ ball (c, 0) r

State before:
case fa.a
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
z : ℂ
zm : z ∈ ball 0 r
⊢ (c', z) ∈ ball (c, 0) r
Tactic:
simp only [← ball_prod_same, Set.mem_prod, m, true_and_iff]
State after:
case fa.a
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
z : ℂ
zm : z ∈ ball 0 r
⊢ z ∈ ball 0 r

State before:
case fa.a
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
z : ℂ
zm : z ∈ ball 0 r
⊢ z ∈ ball 0 r
Tactic:
exact zm
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
z : ℂ
zm : z ∈ ball 0 r
⊢ r ≤ r2
Tactic:
bound
State after:
no goals

State before:
case gs
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
gs : ∀ {x : ℂ × ℂ}, dist x (c, 0) < r4 → dist (g2 f d x) (g2 f d (c, 0)) < 1 / 4
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
⊢ ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g (f c') d z - 1) < 1 / 4
Tactic:
simp only [Complex.dist_eq, Prod.dist_eq, sub_zero, max_lt_iff, and_imp, g2, g0] at gs
State after:
case gs
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
gs : ∀ {x : ℂ × ℂ}, Complex.abs (x.1 - c) < r4 → Complex.abs x.2 < r4 → Complex.abs (g (f x.1) d x.2 - 1) < 1 / 4
⊢ ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g (f c') d z - 1) < 1 / 4

State before:
case gs
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
m : c' ∈ ball c r
gs : ∀ {x : ℂ × ℂ}, Complex.abs (x.1 - c) < r4 → Complex.abs x.2 < r4 → Complex.abs (g (f x.1) d x.2 - 1) < 1 / 4
⊢ ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g (f c') d z - 1) < 1 / 4
Tactic:
simp only [Metric.mem_ball, Complex.dist_eq] at m
State after:
case gs
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
gs : ∀ {x : ℂ × ℂ}, Complex.abs (x.1 - c) < r4 → Complex.abs x.2 < r4 → Complex.abs (g (f x.1) d x.2 - 1) < 1 / 4
m : Complex.abs (c' - c) < r
⊢ ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g (f c') d z - 1) < 1 / 4

State before:
case gs
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
gs : ∀ {x : ℂ × ℂ}, Complex.abs (x.1 - c) < r4 → Complex.abs x.2 < r4 → Complex.abs (g (f x.1) d x.2 - 1) < 1 / 4
m : Complex.abs (c' - c) < r
⊢ ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g (f c') d z - 1) < 1 / 4
Tactic:
intro z zr
State after:
case gs
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
gs : ∀ {x : ℂ × ℂ}, Complex.abs (x.1 - c) < r4 → Complex.abs x.2 < r4 → Complex.abs (g (f x.1) d x.2 - 1) < 1 / 4
m : Complex.abs (c' - c) < r
z : ℂ
zr : Complex.abs z < r
⊢ Complex.abs (g (f c') d z - 1) < 1 / 4

State before:
case gs
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
c : ℂ
m✝ : c ∈ u
r0 : ℝ
r0p : 0 < r0
fa✝ : AnalyticOn ℂ (uncurry f) (ball (c, 0) r0)
r1 : ℝ
r1p : r1 > 0
rc✝¹ : ball c r1 ⊆ u
r2 : ℝ := min r0 r1
fa : AnalyticOn ℂ (uncurry f) (ball (c, 0) (min r0 r1))
rc✝ : ball c r2 ⊆ u
ga : AnalyticOn ℂ (g2 f d) (ball (c, 0) (min r0 r1))
r3 : ℝ
r3p : r3 > 0
rw✝ : ball (c, 0) r3 ⊆ w
r4 : ℝ
r4p : r4 > 0
r : ℝ := min (min r2 r3) (min r4 (1 / 2))
rp : 0 < r
rh : r ≤ 1 / 2
rr4 : r ≤ r4
rc : ball c r ⊆ u
rw : ball (c, 0) r ⊆ w
c' : ℂ
gs : ∀ {x : ℂ × ℂ}, Complex.abs (x.1 - c) < r4 → Complex.abs x.2 < r4 → Complex.abs (g (f x.1) d x.2 - 1) < 1 / 4
m : Complex.abs (c' - c) < r
z : ℂ
zr : Complex.abs z < r
⊢ Complex.abs (g (f c') d z - 1) < 1 / 4
Tactic:
exact @gs ⟨c', z⟩ (lt_of_lt_of_le m rr4) (lt_of_lt_of_le zr rr4)
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
⊢ u = ⋃ c, v c
Tactic:
apply Set.ext
State after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
⊢ ∀ (x : ℂ), x ∈ u ↔ x ∈ ⋃ c, v c

State before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
⊢ ∀ (x : ℂ), x ∈ u ↔ x ∈ ⋃ c, v c
Tactic:
intro c
State after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
⊢ c ∈ u ↔ c ∈ ⋃ c, v c

State before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
⊢ c ∈ u ↔ c ∈ ⋃ c, v c
Tactic:
rw [Set.mem_iUnion]
State after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
⊢ c ∈ u ↔ ∃ i, c ∈ v i

State before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
⊢ c ∈ u ↔ ∃ i, c ∈ v i
Tactic:
constructor
State after:
case h.mp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
⊢ c ∈ u → ∃ i, c ∈ v i

case h.mpr
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
⊢ (∃ i, c ∈ v i) → c ∈ u

State before:
case h.mp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
⊢ c ∈ u → ∃ i, c ∈ v i
Tactic:
intro m
State after:
case h.mp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
m : c ∈ u
⊢ ∃ i, c ∈ v i

State before:
case h.mp
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
m : c ∈ u
⊢ ∃ i, c ∈ v i
Tactic:
use⟨c, m⟩
State after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
m : c ∈ u
⊢ c ∈ v ⟨c, m⟩

State before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
m : c ∈ u
⊢ c ∈ v ⟨c, m⟩
Tactic:
rcases choose_spec (h c m) with ⟨rp, _, _⟩
State after:
case h.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
m : c ∈ u
rp : choose ⋯ > 0
left✝ : ball c (choose ⋯) ⊆ u
right✝ : ball (c, 0) (choose ⋯) ⊆ w ∧ SuperNearC f d (ball c (choose ⋯)) (ball (c, 0) (choose ⋯))
⊢ c ∈ v ⟨c, m⟩

State before:
case h.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
m : c ∈ u
rp : choose ⋯ > 0
left✝ : ball c (choose ⋯) ⊆ u
right✝ : ball (c, 0) (choose ⋯) ⊆ w ∧ SuperNearC f d (ball c (choose ⋯)) (ball (c, 0) (choose ⋯))
⊢ c ∈ v ⟨c, m⟩
Tactic:
exact mem_ball_self rp
State after:
no goals

State before:
case h.mpr
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
⊢ (∃ i, c ∈ v i) → c ∈ u
Tactic:
intro m
State after:
case h.mpr
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
m : ∃ i, c ∈ v i
⊢ c ∈ u

State before:
case h.mpr
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
m : ∃ i, c ∈ v i
⊢ c ∈ u
Tactic:
rcases m with ⟨i, m⟩
State after:
case h.mpr.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
i : ↑u
m : c ∈ v i
⊢ c ∈ u

State before:
case h.mpr.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
i : ↑u
m : c ∈ v i
⊢ c ∈ u
Tactic:
rcases choose_spec (h _ i.mem) with ⟨_, us, _⟩
State after:
case h.mpr.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
i : ↑u
m : c ∈ v i
left✝ : choose ⋯ > 0
us : ball (↑i) (choose ⋯) ⊆ u
right✝ : ball (↑i, 0) (choose ⋯) ⊆ w ∧ SuperNearC f d (ball (↑i) (choose ⋯)) (ball (↑i, 0) (choose ⋯))
⊢ c ∈ u

State before:
case h.mpr.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
c : ℂ
i : ↑u
m : c ∈ v i
left✝ : choose ⋯ > 0
us : ball (↑i) (choose ⋯) ⊆ u
right✝ : ball (↑i, 0) (choose ⋯) ⊆ w ∧ SuperNearC f d (ball (↑i) (choose ⋯)) (ball (↑i, 0) (choose ⋯))
⊢ c ∈ u
Tactic:
exact us m
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
e : u = ⋃ c, v c
⊢ ⋃ c, t c ⊆ w
Tactic:
apply Set.iUnion_subset
State after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
e : u = ⋃ c, v c
⊢ ∀ (i : ↑u), t i ⊆ w

State before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
e : u = ⋃ c, v c
⊢ ∀ (i : ↑u), t i ⊆ w
Tactic:
intro i
State after:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
e : u = ⋃ c, v c
i : ↑u
⊢ t i ⊆ w

State before:
case h
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
e : u = ⋃ c, v c
i : ↑u
⊢ t i ⊆ w
Tactic:
rcases choose_spec (h _ i.mem) with ⟨_, _, rw, _⟩
State after:
case h.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
e : u = ⋃ c, v c
i : ↑u
left✝¹ : choose ⋯ > 0
left✝ : ball (↑i) (choose ⋯) ⊆ u
rw : ball (↑i, 0) (choose ⋯) ⊆ w
right✝ : SuperNearC f d (ball (↑i) (choose ⋯)) (ball (↑i, 0) (choose ⋯))
⊢ t i ⊆ w

State before:
case h.intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
e : u = ⋃ c, v c
i : ↑u
left✝¹ : choose ⋯ > 0
left✝ : ball (↑i) (choose ⋯) ⊆ u
rw : ball (↑i, 0) (choose ⋯) ⊆ w
right✝ : SuperNearC f d (ball (↑i) (choose ⋯)) (ball (↑i, 0) (choose ⋯))
⊢ t i ⊆ w
Tactic:
exact rw
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
e : u = ⋃ c, v c
tw : ⋃ c, t c ⊆ w
⊢ ∀ (c : ↑u), SuperNearC f d (v c) (t c)
Tactic:
intro i
State after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
e : u = ⋃ c, v c
tw : ⋃ c, t c ⊆ w
i : ↑u
⊢ SuperNearC f d (v i) (t i)

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
e : u = ⋃ c, v c
tw : ⋃ c, t c ⊆ w
i : ↑u
⊢ SuperNearC f d (v i) (t i)
Tactic:
rcases choose_spec (h _ i.mem) with ⟨_, _, _, s⟩
State after:
case intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s✝ : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
e : u = ⋃ c, v c
tw : ⋃ c, t c ⊆ w
i : ↑u
left✝² : choose ⋯ > 0
left✝¹ : ball (↑i) (choose ⋯) ⊆ u
left✝ : ball (↑i, 0) (choose ⋯) ⊆ w
s : SuperNearC f d (ball (↑i) (choose ⋯)) (ball (↑i, 0) (choose ⋯))
⊢ SuperNearC f d (v i) (t i)

State before:
case intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s✝ : SuperAtC f d u
w : Set (ℂ × ℂ)
wo : IsOpen w
wc : ∀ c ∈ u, (c, 0) ∈ w
h : ∀ c ∈ u, ∃ r > 0, ball c r ⊆ u ∧ ball (c, 0) r ⊆ w ∧ SuperNearC f d (ball c r) (ball (c, 0) r)
r : ↑u → ℝ := fun c => choose ⋯
v : ↑u → Set ℂ := fun c => ball (↑c) (r c)
t : ↑u → Set (ℂ × ℂ) := fun c => ball (↑c, 0) (r c)
e : u = ⋃ c, v c
tw : ⋃ c, t c ⊆ w
i : ↑u
left✝² : choose ⋯ > 0
left✝¹ : ball (↑i) (choose ⋯) ⊆ u
left✝ : ball (↑i, 0) (choose ⋯) ⊆ w
s : SuperNearC f d (ball (↑i) (choose ⋯)) (ball (↑i, 0) (choose ⋯))
⊢ SuperNearC f d (v i) (t i)
Tactic:
exact s
State after:
no goals