Theorem: NontrivialHolomorphicAt.pow_iff (Ray/AnalyticManifold/Nontrivial.lean)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : S → ℂ
z : S
d : ℕ
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d0 : 0 < d
⊢ NontrivialHolomorphicAt (fun z => f z ^ d) z ↔ NontrivialHolomorphicAt f z
Tactic:
refine ⟨?_, (nontrivialHolomorphicAtPow d0).comp⟩
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : S → ℂ
z : S
d : ℕ
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d0 : 0 < d
⊢ NontrivialHolomorphicAt (fun z => f z ^ d) z → NontrivialHolomorphicAt f z

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : S → ℂ
z : S
d : ℕ
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d0 : 0 < d
⊢ NontrivialHolomorphicAt (fun z => f z ^ d) z → NontrivialHolomorphicAt f z
Tactic:
have pa : HolomorphicAt I I (fun z ↦ z ^ d) (f z) := HolomorphicAt.pow holomorphicAt_id
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : S → ℂ
z : S
d : ℕ
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d0 : 0 < d
pa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun z => z ^ d) (f z)
⊢ NontrivialHolomorphicAt (fun z => f z ^ d) z → NontrivialHolomorphicAt f z

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : S → ℂ
z : S
d : ℕ
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d0 : 0 < d
pa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun z => z ^ d) (f z)
⊢ NontrivialHolomorphicAt (fun z => f z ^ d) z → NontrivialHolomorphicAt f z
Tactic:
intro h
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : S → ℂ
z : S
d : ℕ
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d0 : 0 < d
pa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun z => z ^ d) (f z)
h : NontrivialHolomorphicAt (fun z => f z ^ d) z
⊢ NontrivialHolomorphicAt f z

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : S → ℂ
z : S
d : ℕ
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d0 : 0 < d
pa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun z => z ^ d) (f z)
h : NontrivialHolomorphicAt (fun z => f z ^ d) z
⊢ NontrivialHolomorphicAt f z
Tactic:
refine (NontrivialHolomorphicAt.anti ?_ pa fa).2
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : S → ℂ
z : S
d : ℕ
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d0 : 0 < d
pa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun z => z ^ d) (f z)
h : NontrivialHolomorphicAt (fun z => f z ^ d) z
⊢ NontrivialHolomorphicAt (fun z => f z ^ d) z

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
f : S → ℂ
z : S
d : ℕ
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d0 : 0 < d
pa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (fun z => z ^ d) (f z)
h : NontrivialHolomorphicAt (fun z => f z ^ d) z
⊢ NontrivialHolomorphicAt (fun z => f z ^ d) z
Tactic:
exact h
State after:
no goals