internlm/Lean-Github huggingface dataset:
Theorem: SuperAtC.superNearC'
Proof 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
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)
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
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
⊢ ∀ (i : ↑u), t i ⊆ w
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
⊢ ∀ (i : ↑u), t i ⊆ w
Tactic:
intro i
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
i : ↑u
⊢ t i ⊆ w
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
i : ↑u
⊢ t i ⊆ w
Tactic:
rcases choose_spec (h _ i.mem) with ⟨_, _, rw, _⟩
Proof 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
Theorem: SuperAtC.superNearC'
Proof 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
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)
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
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)
e : u = ⋃ c, v c
tw : ⋃ c, t c ⊆ w
i : ↑u
⊢ SuperNearC f d (v i) (t i)
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)
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⟩
Proof 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)
Theorem: SuperAtC.superNearC'
Proof 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
Proof state after:
no goals
Theorem: SuperAtC.superNearC
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
⊢ ∃ t, SuperNearC f d u t
Tactic:
rcases s.superNearC' isOpen_univ fun _ _ ↦ Set.mem_univ _ with ⟨t, _, s⟩
Proof state after:
case intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s✝ : SuperAtC f d u
t : Set (ℂ × ℂ)
left✝ : t ⊆ univ
s : SuperNearC f d u t
⊢ ∃ t, SuperNearC f d u t
Theorem: SuperAtC.superNearC
Proof state before:
case intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s✝ : SuperAtC f d u
t : Set (ℂ × ℂ)
left✝ : t ⊆ univ
s : SuperNearC f d u t
⊢ ∃ t, SuperNearC f d u t
Tactic:
exact ⟨t, s⟩
Proof state after:
no goals
Theorem: iterates_analytic_c
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun c => (f c)^[n] z) c
Tactic:
induction' n with n nh
Proof state after:
case zero
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun c => (f c)^[0] z) c

case succ
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
n : ℕ
nh : AnalyticAt ℂ (fun c => (f c)^[n] z) c
⊢ AnalyticAt ℂ (fun c => (f c)^[n + 1] z) c
Theorem: iterates_analytic_c
Proof state before:
case zero
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun c => (f c)^[0] z) c
Tactic:
simp only [Function.iterate_zero, id]
Proof state after:
case zero
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun c => z) c
Theorem: iterates_analytic_c
Proof state before:
case zero
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun c => z) c
Tactic:
exact analyticAt_const
Proof state after:
no goals
Theorem: iterates_analytic_c
Proof state before:
case succ
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
n : ℕ
nh : AnalyticAt ℂ (fun c => (f c)^[n] z) c
⊢ AnalyticAt ℂ (fun c => (f c)^[n + 1] z) c
Tactic:
simp_rw [Function.iterate_succ']
Proof state after:
case succ
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
n : ℕ
nh : AnalyticAt ℂ (fun c => (f c)^[n] z) c
⊢ AnalyticAt ℂ (fun c => (f c ∘ (f c)^[n]) z) c
Theorem: iterates_analytic_c
Proof state before:
case succ
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
n : ℕ
nh : AnalyticAt ℂ (fun c => (f c)^[n] z) c
⊢ AnalyticAt ℂ (fun c => (f c ∘ (f c)^[n]) z) c
Tactic:
simp only [Function.comp_apply]
Proof state after:
case succ
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
n : ℕ
nh : AnalyticAt ℂ (fun c => (f c)^[n] z) c
⊢ AnalyticAt ℂ (fun c => f c ((f c)^[n] z)) c
Theorem: iterates_analytic_c
Proof state before:
case succ
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
n : ℕ
nh : AnalyticAt ℂ (fun c => (f c)^[n] z) c
⊢ AnalyticAt ℂ (fun c => f c ((f c)^[n] z)) c
Tactic:
refine (s.fa _ ?_).comp ((analyticAt_id _ _).prod nh)
Proof state after:
case succ
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
n : ℕ
nh : AnalyticAt ℂ (fun c => (f c)^[n] z) c
⊢ (id c, (f c)^[n] z) ∈ t
Theorem: iterates_analytic_c
Proof state before:
case succ
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
n : ℕ
nh : AnalyticAt ℂ (fun c => (f c)^[n] z) c
⊢ (id c, (f c)^[n] z) ∈ t
Tactic:
exact (s.ts m).mapsTo n m
Proof state after:
no goals
Theorem: term_analytic_c
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun c => term (f c) d n z) c
Tactic:
refine AnalyticAt.cpow ?_ analyticAt_const ?_
Proof state after:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun c => g (f c) d ((f c)^[n] z)) c

case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
⊢ g (f c) d ((f c)^[n] z) ∈ Complex.slitPlane
Theorem: term_analytic_c
Proof state before:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun c => g (f c) d ((f c)^[n] z)) c
Tactic:
have e : (fun c ↦ g (f c) d ((f c)^[n] z)) = fun c ↦ g2 f d (c, (f c)^[n] z) := rfl
Proof state after:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
e : (fun c => g (f c) d ((f c)^[n] z)) = fun c => g2 f d (c, (f c)^[n] z)
⊢ AnalyticAt ℂ (fun c => g (f c) d ((f c)^[n] z)) c
Theorem: term_analytic_c
Proof state before:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
e : (fun c => g (f c) d ((f c)^[n] z)) = fun c => g2 f d (c, (f c)^[n] z)
⊢ AnalyticAt ℂ (fun c => g (f c) d ((f c)^[n] z)) c
Tactic:
rw [e]
Proof state after:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
e : (fun c => g (f c) d ((f c)^[n] z)) = fun c => g2 f d (c, (f c)^[n] z)
⊢ AnalyticAt ℂ (fun c => g2 f d (c, (f c)^[n] z)) c
Theorem: term_analytic_c
Proof state before:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
e : (fun c => g (f c) d ((f c)^[n] z)) = fun c => g2 f d (c, (f c)^[n] z)
⊢ AnalyticAt ℂ (fun c => g2 f d (c, (f c)^[n] z)) c
Tactic:
refine (s.ga _ ?_).comp ?_
Proof state after:
case refine_1.refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
e : (fun c => g (f c) d ((f c)^[n] z)) = fun c => g2 f d (c, (f c)^[n] z)
⊢ (c, (f c)^[n] z) ∈ t

case refine_1.refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
e : (fun c => g (f c) d ((f c)^[n] z)) = fun c => g2 f d (c, (f c)^[n] z)
⊢ AnalyticAt ℂ (fun c => (c, (f c)^[n] z)) c
Theorem: term_analytic_c
Proof state before:
case refine_1.refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
e : (fun c => g (f c) d ((f c)^[n] z)) = fun c => g2 f d (c, (f c)^[n] z)
⊢ (c, (f c)^[n] z) ∈ t
Tactic:
exact (s.ts m).mapsTo n m
Proof state after:
no goals
Theorem: term_analytic_c
Proof state before:
case refine_1.refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
e : (fun c => g (f c) d ((f c)^[n] z)) = fun c => g2 f d (c, (f c)^[n] z)
⊢ AnalyticAt ℂ (fun c => (c, (f c)^[n] z)) c
Tactic:
apply (analyticAt_id _ _).prod (iterates_analytic_c s n m)
Proof state after:
no goals
Theorem: term_analytic_c
Proof state before:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
⊢ g (f c) d ((f c)^[n] z) ∈ Complex.slitPlane
Tactic:
refine mem_slitPlane_of_near_one ?_
Proof state after:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
⊢ Complex.abs (g (f c) d ((f c)^[n] z) - 1) < 1
Theorem: term_analytic_c
Proof state before:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
⊢ Complex.abs (g (f c) d ((f c)^[n] z) - 1) < 1
Tactic:
exact lt_of_le_of_lt ((s.ts m).gs ((s.ts m).mapsTo n m)) (by norm_num)
Proof state after:
no goals
Theorem: term_analytic_c
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
⊢ 1 / 4 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: term_prod_analytic_c
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun c => ∏' (n : ℕ), term (f c) d n z) c
Tactic:
have c12 : (1 / 2 : ℝ) ≤ 1 / 2 := by norm_num
Proof state after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
⊢ AnalyticAt ℂ (fun c => ∏' (n : ℕ), term (f c) d n z) c
Theorem: term_prod_analytic_c
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
⊢ AnalyticAt ℂ (fun c => ∏' (n : ℕ), term (f c) d n z) c
Tactic:
have a0 : 0 ≤ (1 / 2 : ℝ) := by norm_num
Proof state after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
⊢ AnalyticAt ℂ (fun c => ∏' (n : ℕ), term (f c) d n z) c
Theorem: term_prod_analytic_c
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
⊢ AnalyticAt ℂ (fun c => ∏' (n : ℕ), term (f c) d n z) c
Tactic:
set t' := {c | (c, z) ∈ t}
Proof state after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
t' : Set ℂ := {c | (c, z) ∈ t}
⊢ AnalyticAt ℂ (fun c => ∏' (n : ℕ), term (f c) d n z) c
Theorem: term_prod_analytic_c
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
t' : Set ℂ := {c | (c, z) ∈ t}
⊢ AnalyticAt ℂ (fun c => ∏' (n : ℕ), term (f c) d n z) c
Tactic:
have o' : IsOpen t' := s.o.preimage (by continuity)
Proof state after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
t' : Set ℂ := {c | (c, z) ∈ t}
o' : IsOpen t'
⊢ AnalyticAt ℂ (fun c => ∏' (n : ℕ), term (f c) d n z) c
Theorem: term_prod_analytic_c
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
t' : Set ℂ := {c | (c, z) ∈ t}
o' : IsOpen t'
⊢ AnalyticAt ℂ (fun c => ∏' (n : ℕ), term (f c) d n z) c
Tactic:
refine (fast_products_converge' o' c12 a0 (by linarith) ?_
  fun n c m ↦ term_converges (s.ts m) n m).2.1 _ m
Proof state after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
t' : Set ℂ := {c | (c, z) ∈ t}
o' : IsOpen t'
⊢ ∀ (n : ℕ), AnalyticOn ℂ (fun c => term (f (c, z).1) d n z) t'
Theorem: term_prod_analytic_c
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
t' : Set ℂ := {c | (c, z) ∈ t}
o' : IsOpen t'
⊢ ∀ (n : ℕ), AnalyticOn ℂ (fun c => term (f (c, z).1) d n z) t'
Tactic:
exact fun n c m ↦ term_analytic_c s n m
Proof state after:
no goals
Theorem: term_prod_analytic_c
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
⊢ 1 / 2 ≤ 1 / 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: term_prod_analytic_c
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
⊢ 0 ≤ 1 / 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: term_prod_analytic_c
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
t' : Set ℂ := {c | (c, z) ∈ t}
⊢ Continuous fun c => (c, z)
Tactic:
continuity
Proof state after:
no goals
Theorem: term_prod_analytic_c
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
t' : Set ℂ := {c | (c, z) ∈ t}
o' : IsOpen t'
⊢ 1 / 2 < 1
Tactic:
linarith
Proof state after:
no goals
Theorem: term_prod_analytic
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
⊢ AnalyticOn ℂ (fun p => ∏' (n : ℕ), term (f p.1) d n p.2) t
Tactic:
refine Pair.hartogs s.o ?_ ?_
Proof state after:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
⊢ ∀ (c0 c1 : ℂ), (c0, c1) ∈ t → AnalyticAt ℂ (fun z0 => ∏' (n : ℕ), term (f (z0, c1).1) d n (z0, c1).2) c0

case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
⊢ ∀ (c0 c1 : ℂ), (c0, c1) ∈ t → AnalyticAt ℂ (fun z1 => ∏' (n : ℕ), term (f (c0, z1).1) d n (c0, z1).2) c1
Theorem: term_prod_analytic
Proof state before:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
⊢ ∀ (c0 c1 : ℂ), (c0, c1) ∈ t → AnalyticAt ℂ (fun z0 => ∏' (n : ℕ), term (f (z0, c1).1) d n (z0, c1).2) c0
Tactic:
intro c z m
Proof state after:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun z0 => ∏' (n : ℕ), term (f (z0, z).1) d n (z0, z).2) c
Theorem: term_prod_analytic
Proof state before:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun z0 => ∏' (n : ℕ), term (f (z0, z).1) d n (z0, z).2) c
Tactic:
simp only
Proof state after:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun z0 => ∏' (n : ℕ), term (f z0) d n z) c
Theorem: term_prod_analytic
Proof state before:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun z0 => ∏' (n : ℕ), term (f z0) d n z) c
Tactic:
exact term_prod_analytic_c s m
Proof state after:
no goals
Theorem: term_prod_analytic
Proof state before:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
⊢ ∀ (c0 c1 : ℂ), (c0, c1) ∈ t → AnalyticAt ℂ (fun z1 => ∏' (n : ℕ), term (f (c0, z1).1) d n (c0, z1).2) c1
Tactic:
intro c z m
Proof state after:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun z1 => ∏' (n : ℕ), term (f (c, z1).1) d n (c, z1).2) z
Theorem: term_prod_analytic
Proof state before:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun z1 => ∏' (n : ℕ), term (f (c, z1).1) d n (c, z1).2) z
Tactic:
simp only
Proof state after:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun z1 => ∏' (n : ℕ), term (f c) d n z1) z
Theorem: term_prod_analytic
Proof state before:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun z1 => ∏' (n : ℕ), term (f c) d n z1) z
Tactic:
exact term_prod_analytic_z (s.ts m) _ m
Proof state after:
no goals
Theorem: df_ne_zero
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
⊢ ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), deriv (f p.1) p.2 = 0 ↔ p.2 = 0
Tactic:
have df : ∀ e z, (e, z) ∈ t →
    deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z := by
  intro e z m; apply HasDerivAt.deriv
  have fg : f e = fun z ↦ z ^ d * g (f e) d z := by funext; rw [(s.ts m).fg]
  nth_rw 1 [fg]
  apply HasDerivAt.mul; apply hasDerivAt_pow
  rw [hasDerivAt_deriv_iff]; exact ((s.ts m).ga _ m).differentiableAt
Proof state after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
⊢ ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), deriv (f p.1) p.2 = 0 ↔ p.2 = 0
Theorem: df_ne_zero
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
small : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), Complex.abs (p.2 * deriv (g (f p.1) d) p.2) < Complex.abs (↑d * g (f p.1) d p.2)
⊢ ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), deriv (f p.1) p.2 = 0 ↔ p.2 = 0
Tactic:
apply small.mp
Proof state after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
small : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), Complex.abs (p.2 * deriv (g (f p.1) d) p.2) < Complex.abs (↑d * g (f p.1) d p.2)
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0),
    Complex.abs (x.2 * deriv (g (f x.1) d) x.2) < Complex.abs (↑d * g (f x.1) d x.2) → (deriv (f x.1) x.2 = 0 ↔ x.2 = 0)
Theorem: df_ne_zero
Proof state before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
small : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), Complex.abs (p.2 * deriv (g (f p.1) d) p.2) < Complex.abs (↑d * g (f p.1) d p.2)
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0),
    Complex.abs (x.2 * deriv (g (f x.1) d) x.2) < Complex.abs (↑d * g (f x.1) d x.2) → (deriv (f x.1) x.2 = 0 ↔ x.2 = 0)
Tactic:
apply (s.o.eventually_mem (s.s m).t0).mp
Proof state after:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c : ℂ
m : c ∈ u
df : ∀ (e z : ℂ), (e, z) ∈ t → deriv (f e) z = ↑d * z ^ (d - 1) * g (f e) d z + z ^ d * deriv (g (f e) d) z
small : ∀ᶠ (p : ℂ × ℂ) in 𝓝 (c, 0), Complex.abs (p.2 * deriv (g (f p.1) d) p.2) < Complex.abs (↑d * g (f p.1) d p.2)
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (c, 0),
    x ∈ t →
      Complex.abs (x.2 * deriv (g (f x.1) d) x.2) < Complex.abs (↑d * g (f x.1) d x.2) →
        (deriv (f x.1) x.2 = 0 ↔ x.2 = 0)