Theorem: SuperAtC.ga_of_fa (Ray/Dynamics/BottcherNear.lean)

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
⊢ AnalyticOn ℂ (g2 f d) t
Tactic:
refine Pair.hartogs o ?_ ?_
State after:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
⊢ ∀ (c0 c1 : ℂ), (c0, c1) ∈ t → AnalyticAt ℂ (fun z0 => g2 f d (z0, c1)) c0

case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
⊢ ∀ (c0 c1 : ℂ), (c0, c1) ∈ t → AnalyticAt ℂ (fun z1 => g2 f d (c0, z1)) c1

State before:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
⊢ ∀ (c0 c1 : ℂ), (c0, c1) ∈ t → AnalyticAt ℂ (fun z0 => g2 f d (z0, c1)) c0
Tactic:
intro c z m
State after:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun z0 => g2 f d (z0, z)) c

State before:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun z0 => g2 f d (z0, z)) c
Tactic:
simp only [g2, g]
State after:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun z0 => if z = 0 then 1 else f z0 z / z ^ d) c

State before:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun z0 => if z = 0 then 1 else f z0 z / z ^ d) c
Tactic:
by_cases zero : z = 0
State after:
case pos
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : z = 0
⊢ AnalyticAt ℂ (fun z0 => if z = 0 then 1 else f z0 z / z ^ d) c

case neg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : ¬z = 0
⊢ AnalyticAt ℂ (fun z0 => if z = 0 then 1 else f z0 z / z ^ d) c

State before:
case pos
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : z = 0
⊢ AnalyticAt ℂ (fun z0 => if z = 0 then 1 else f z0 z / z ^ d) c
Tactic:
simp only [zero, eq_self_iff_true, if_true]
State after:
case pos
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : z = 0
⊢ AnalyticAt ℂ (fun z0 => 1) c

State before:
case pos
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : z = 0
⊢ AnalyticAt ℂ (fun z0 => 1) c
Tactic:
exact analyticAt_const
State after:
no goals

State before:
case neg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : ¬z = 0
⊢ AnalyticAt ℂ (fun z0 => if z = 0 then 1 else f z0 z / z ^ d) c
Tactic:
simp only [zero, if_false]
State after:
case neg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : ¬z = 0
⊢ AnalyticAt ℂ (fun z0 => f z0 z / z ^ d) c

State before:
case neg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : ¬z = 0
⊢ AnalyticAt ℂ (fun z0 => f z0 z / z ^ d) c
Tactic:
refine AnalyticAt.div ?_ analyticAt_const (pow_ne_zero _ zero)
State after:
case neg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : ¬z = 0
⊢ AnalyticAt ℂ (fun z0 => f z0 z) c

State before:
case neg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : ¬z = 0
⊢ AnalyticAt ℂ (fun z0 => f z0 z) c
Tactic:
refine (fa _ ?_).comp₂ (analyticAt_id _ _) analyticAt_const
State after:
case neg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : ¬z = 0
⊢ (c, z) ∈ t

State before:
case neg
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
zero : ¬z = 0
⊢ (c, z) ∈ t
Tactic:
exact m
State after:
no goals

State before:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
⊢ ∀ (c0 c1 : ℂ), (c0, c1) ∈ t → AnalyticAt ℂ (fun z1 => g2 f d (c0, z1)) c1
Tactic:
intro c z m
State after:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun z1 => g2 f d (c, z1)) z

State before:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun z1 => g2 f d (c, z1)) z
Tactic:
apply (s.s (tc m)).ga_of_fa
State after:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (f (c, z).1) z

State before:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (f (c, z).1) z
Tactic:
refine (fa _ ?_).comp₂ analyticAt_const (analyticAt_id _ _)
State after:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
⊢ (c, id z) ∈ t

State before:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s : SuperAtC f d u
t : Set (ℂ × ℂ)
o : IsOpen t
fa : AnalyticOn ℂ (uncurry f) t
tc : ∀ {p : ℂ × ℂ}, p ∈ t → p.1 ∈ u
c z : ℂ
m : (c, z) ∈ t
⊢ (c, id z) ∈ t
Tactic:
exact m
State after:
no goals