internlm/Lean-Github huggingface dataset:
Theorem: SuperNearC.union
Proof state before:
case intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u✝¹ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u✝ : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝¹ : ∀ (i : I), SuperNearC f d (u✝ i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝² : c ∈ ⋃ i, u✝ i
i : I
m✝¹ : c ∈ u✝ i
s✝ : SuperNear (f c) d {z | (c, z) ∈ t i}
z : ℂ
m✝ : z ∈ {z | (c, z) ∈ tu}
u : Set ℂ
m : z ∈ u
us : u ⊆ {z | (c, z) ∈ tu}
s : SuperNear (f c) d u
⊢ f c z ∈ {z | (c, z) ∈ tu}
Tactic:
exact us (s.ft m)
Proof state after:
no goals
Theorem: SuperNearC.union
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝ : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝ : c ∈ ⋃ i, u i
i : I
m : c ∈ u i
s : SuperNear (f c) d {z | (c, z) ∈ t i}
⊢ ∀ {z : ℂ}, z ≠ 0 → z ∈ {z | (c, z) ∈ tu} → Complex.abs (f c z / z ^ d - 1) ≤ 1 / 4
Tactic:
intro z z0 m
Proof state after:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝ : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝¹ : c ∈ ⋃ i, u i
i : I
m✝ : c ∈ u i
s : SuperNear (f c) d {z | (c, z) ∈ t i}
z : ℂ
z0 : z ≠ 0
m : z ∈ {z | (c, z) ∈ tu}
⊢ Complex.abs (f c z / z ^ d - 1) ≤ 1 / 4
Theorem: SuperNearC.union
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u✝ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝ : ∀ (i : I), SuperNearC f d (u i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝¹ : c ∈ ⋃ i, u i
i : I
m✝ : c ∈ u i
s : SuperNear (f c) d {z | (c, z) ∈ t i}
z : ℂ
z0 : z ≠ 0
m : z ∈ {z | (c, z) ∈ tu}
⊢ Complex.abs (f c z / z ^ d - 1) ≤ 1 / 4
Tactic:
rcases sm m with ⟨u, m, _, s⟩
Proof state after:
case intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u✝¹ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u✝ : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝¹ : ∀ (i : I), SuperNearC f d (u✝ i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝² : c ∈ ⋃ i, u✝ i
i : I
m✝¹ : c ∈ u✝ i
s✝ : SuperNear (f c) d {z | (c, z) ∈ t i}
z : ℂ
z0 : z ≠ 0
m✝ : z ∈ {z | (c, z) ∈ tu}
u : Set ℂ
m : z ∈ u
left✝ : u ⊆ {z | (c, z) ∈ tu}
s : SuperNear (f c) d u
⊢ Complex.abs (f c z / z ^ d - 1) ≤ 1 / 4
Theorem: SuperNearC.union
Proof state before:
case intro.intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u✝¹ : Set ℂ
t✝ : Set (ℂ × ℂ)
I : Type
u✝ : I → Set ℂ
t : I → Set (ℂ × ℂ)
s✝¹ : ∀ (i : I), SuperNearC f d (u✝ i) (t i)
tu : Set (ℂ × ℂ) := ⋃ i, t i
o : IsOpen tu
sm : ∀ {c z : ℂ}, (c, z) ∈ tu → ∃ u, z ∈ u ∧ u ⊆ {z | (c, z) ∈ tu} ∧ SuperNear (f c) d u
c : ℂ
m✝² : c ∈ ⋃ i, u✝ i
i : I
m✝¹ : c ∈ u✝ i
s✝ : SuperNear (f c) d {z | (c, z) ∈ t i}
z : ℂ
z0 : z ≠ 0
m✝ : z ∈ {z | (c, z) ∈ tu}
u : Set ℂ
m : z ∈ u
left✝ : u ⊆ {z | (c, z) ∈ tu}
s : SuperNear (f c) d u
⊢ Complex.abs (f c z / z ^ d - 1) ≤ 1 / 4
Tactic:
exact s.gs' z0 m
Proof state after:
no goals
Theorem: SuperAtC.superNearC'
Proof 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)
Proof 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
Theorem: SuperAtC.superNearC'
Proof 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)
Proof 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
Theorem: SuperAtC.superNearC'
Proof 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)
Proof 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
Theorem: SuperAtC.superNearC'
Proof 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
Proof 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)
Theorem: SuperAtC.superNearC'
Proof 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
Proof 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)
Theorem: SuperAtC.superNearC'
Proof 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
Proof 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)
Theorem: SuperAtC.superNearC'
Proof 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
Proof 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)
Theorem: SuperAtC.superNearC'
Proof 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
Proof 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)
Theorem: SuperAtC.superNearC'
Proof 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⟩
Proof state after:
no goals
Theorem: SuperAtC.superNearC'
Proof 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
Proof 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)
Theorem: SuperAtC.superNearC'
Proof 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⟩
Proof 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)
Theorem: SuperAtC.superNearC'
Proof 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⟩
Proof 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)
Theorem: SuperAtC.superNearC'
Proof 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
Proof 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)
Theorem: SuperAtC.superNearC'
Proof 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))
Proof 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)
Theorem: SuperAtC.superNearC'
Proof 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
Proof 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)
Theorem: SuperAtC.superNearC'
Proof 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)
Proof 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)
Theorem: SuperAtC.superNearC'
Proof 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⟩
Proof 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)
Theorem: SuperAtC.superNearC'
Proof 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⟩
Proof 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)
Theorem: SuperAtC.superNearC'
Proof 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))
Proof 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)
Theorem: SuperAtC.superNearC'
Proof 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
Proof 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)