Theorem: NontrivialHolomorphicAt.comp (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 ℂ
inst✝ : T2Space U
f : T → U
g : S → T
z : S
fn : NontrivialHolomorphicAt f (g z)
gn : NontrivialHolomorphicAt g z
⊢ NontrivialHolomorphicAt (fun z => f (g z)) z
Tactic:
use fn.holomorphicAt.comp gn.holomorphicAt
State after:
case nonconst
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 ℂ
inst✝ : T2Space U
f : T → U
g : S → T
z : S
fn : NontrivialHolomorphicAt f (g z)
gn : NontrivialHolomorphicAt g z
⊢ ∃ᶠ (w : S) in 𝓝 z, f (g w) ≠ f (g z)

State before:
case nonconst
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 ℂ
inst✝ : T2Space U
f : T → U
g : S → T
z : S
fn : NontrivialHolomorphicAt f (g z)
gn : NontrivialHolomorphicAt g z
⊢ ∃ᶠ (w : S) in 𝓝 z, f (g w) ≠ f (g z)
Tactic:
convert gn.nonconst.and_eventually (gn.holomorphicAt.continuousAt.eventually fn.eventually_ne)
State after:
case h.e'_2.h.a
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 ℂ
inst✝ : T2Space U
f : T → U
g : S → T
z : S
fn : NontrivialHolomorphicAt f (g z)
gn : NontrivialHolomorphicAt g z
x✝ : S
⊢ f (g x✝) ≠ f (g z) ↔ g x✝ ≠ g z ∧ (g x✝ ≠ g z → f (g x✝) ≠ f (g z))

State before:
case h.e'_2.h.a
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 ℂ
inst✝ : T2Space U
f : T → U
g : S → T
z : S
fn : NontrivialHolomorphicAt f (g z)
gn : NontrivialHolomorphicAt g z
x✝ : S
⊢ f (g x✝) ≠ f (g z) ↔ g x✝ ≠ g z ∧ (g x✝ ≠ g z → f (g x✝) ≠ f (g z))
Tactic:
tauto
State after:
no goals