Theorem: term_prod_analytic (Ray/Dynamics/BottcherNear.lean)

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 ?_ ?_
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

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
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

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
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals