internlm/Lean-Github huggingface dataset:
Theorem: NontrivialHolomorphicAt.on_preconnected
Proof 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 T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
a : T
n : ∀ᶠ (x : S) in 𝓝 w, f x = a
ha : f w = a
c : ∀ w ∈ s, f w = a
⊢ ∀ x ∈ s, f x = f z
Tactic:
intro x m
Proof 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 ℂ
inst✝ : T2Space T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
a : T
n : ∀ᶠ (x : S) in 𝓝 w, f x = a
ha : f w = a
c : ∀ w ∈ s, f w = a
x : S
m : x ∈ s
⊢ f x = f z
Theorem: NontrivialHolomorphicAt.on_preconnected
Proof 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 T
f : S → T
s : Set S
z : S
fa : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f s
zs : z ∈ s
o : IsOpen s
p : IsPreconnected s
w : S
ws : w ∈ s
a : T
n : ∀ᶠ (x : S) in 𝓝 w, f x = a
ha : f w = a
c : ∀ w ∈ s, f w = a
x : S
m : x ∈ s
⊢ f x = f z
Tactic:
rw [c _ m, c _ zs]
Proof state after:
no goals
Theorem: NontrivialHolomorphicAt.eventually
Proof 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 T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
⊢ ∀ᶠ (w : S) in 𝓝 z, NontrivialHolomorphicAt f w
Tactic:
have lc : LocallyConnectedSpace S := ChartedSpace.locallyConnectedSpace ℂ _
Proof 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 ℂ
inst✝ : T2Space T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
lc : LocallyConnectedSpace S
⊢ ∀ᶠ (w : S) in 𝓝 z, NontrivialHolomorphicAt f w
Theorem: NontrivialHolomorphicAt.eventually
Proof 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 T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
lc : LocallyConnectedSpace S
⊢ ∀ᶠ (w : S) in 𝓝 z, NontrivialHolomorphicAt f w
Tactic:
rcases eventually_nhds_iff.mp n.holomorphicAt.eventually with ⟨s, fa, os, zs⟩
Proof state after:
case intro.intro.intro
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 T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
lc : LocallyConnectedSpace S
s : Set S
fa : ∀ x ∈ s, HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f x
os : IsOpen s
zs : z ∈ s
⊢ ∀ᶠ (w : S) in 𝓝 z, NontrivialHolomorphicAt f w
Theorem: NontrivialHolomorphicAt.eventually
Proof state before:
case intro.intro.intro
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 T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
lc : LocallyConnectedSpace S
s : Set S
fa : ∀ x ∈ s, HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f x
os : IsOpen s
zs : z ∈ s
⊢ ∀ᶠ (w : S) in 𝓝 z, NontrivialHolomorphicAt f w
Tactic:
rcases locallyConnectedSpace_iff_open_connected_subsets.mp lc z s (os.mem_nhds zs) with
  ⟨t, ts, ot, zt, ct⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
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 T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
lc : LocallyConnectedSpace S
s : Set S
fa : ∀ x ∈ s, HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f x
os : IsOpen s
zs : z ∈ s
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
ct : IsConnected t
⊢ ∀ᶠ (w : S) in 𝓝 z, NontrivialHolomorphicAt f w
Theorem: NontrivialHolomorphicAt.eventually
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
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 T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
lc : LocallyConnectedSpace S
s : Set S
fa : ∀ x ∈ s, HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f x
os : IsOpen s
zs : z ∈ s
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
ct : IsConnected t
⊢ ∀ᶠ (w : S) in 𝓝 z, NontrivialHolomorphicAt f w
Tactic:
rw [eventually_nhds_iff]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
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 T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
lc : LocallyConnectedSpace S
s : Set S
fa : ∀ x ∈ s, HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f x
os : IsOpen s
zs : z ∈ s
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
ct : IsConnected t
⊢ ∃ t, (∀ x ∈ t, NontrivialHolomorphicAt f x) ∧ IsOpen t ∧ z ∈ t
Theorem: NontrivialHolomorphicAt.eventually
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
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 T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
lc : LocallyConnectedSpace S
s : Set S
fa : ∀ x ∈ s, HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f x
os : IsOpen s
zs : z ∈ s
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
ct : IsConnected t
⊢ ∃ t, (∀ x ∈ t, NontrivialHolomorphicAt f x) ∧ IsOpen t ∧ z ∈ t
Tactic:
refine ⟨t, ?_, ot, zt⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
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 T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
lc : LocallyConnectedSpace S
s : Set S
fa : ∀ x ∈ s, HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f x
os : IsOpen s
zs : z ∈ s
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
ct : IsConnected t
⊢ ∀ x ∈ t, NontrivialHolomorphicAt f x
Theorem: NontrivialHolomorphicAt.eventually
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
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 T
f : S → T
z : S
n : NontrivialHolomorphicAt f z
lc : LocallyConnectedSpace S
s : Set S
fa : ∀ x ∈ s, HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f x
os : IsOpen s
zs : z ∈ s
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
ct : IsConnected t
⊢ ∀ x ∈ t, NontrivialHolomorphicAt f x
Tactic:
exact n.on_preconnected (HolomorphicOn.mono fa ts) zt ot ct.isPreconnected
Proof state after:
no goals
Theorem: nontrivialHolomorphicAt_of_mfderiv_ne_zero
Proof 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 → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d : mfderiv 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z ≠ 0
⊢ NontrivialHolomorphicAt f z
Tactic:
refine ⟨fa, ?_⟩
Proof 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 → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d : mfderiv 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z ≠ 0
⊢ ∃ᶠ (w : S) in 𝓝 z, f w ≠ f z
Theorem: nontrivialHolomorphicAt_of_mfderiv_ne_zero
Proof 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 → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d : mfderiv 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z ≠ 0
⊢ ∃ᶠ (w : S) in 𝓝 z, f w ≠ f z
Tactic:
contrapose d
Proof 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 → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d : ¬∃ᶠ (w : S) in 𝓝 z, f w ≠ f z
⊢ ¬mfderiv 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z ≠ 0
Theorem: nontrivialHolomorphicAt_of_mfderiv_ne_zero
Proof 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 → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d : ¬∃ᶠ (w : S) in 𝓝 z, f w ≠ f z
⊢ ¬mfderiv 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z ≠ 0
Tactic:
simp only [Filter.not_frequently, not_not] at d ⊢
Proof 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 → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d : ∀ᶠ (x : S) in 𝓝 z, f x = f z
⊢ mfderiv 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z = 0
Theorem: nontrivialHolomorphicAt_of_mfderiv_ne_zero
Proof 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 → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d : ∀ᶠ (x : S) in 𝓝 z, f x = f z
⊢ mfderiv 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z = 0
Tactic:
generalize ha : f z = a
Proof 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 → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d : ∀ᶠ (x : S) in 𝓝 z, f x = f z
a : T
ha : f z = a
⊢ mfderiv 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z = 0
Theorem: nontrivialHolomorphicAt_of_mfderiv_ne_zero
Proof 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 → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
d : ∀ᶠ (x : S) in 𝓝 z, f x = f z
a : T
ha : f z = a
⊢ mfderiv 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z = 0
Tactic:
rw [ha] at d
Proof 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 → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
a : T
d : ∀ᶠ (x : S) in 𝓝 z, f x = a
ha : f z = a
⊢ mfderiv 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z = 0
Theorem: nontrivialHolomorphicAt_of_mfderiv_ne_zero
Proof 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 → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
a : T
d : ∀ᶠ (x : S) in 𝓝 z, f x = a
ha : f z = a
⊢ mfderiv 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z = 0
Tactic:
apply HasMFDerivAt.mfderiv
Proof state after:
case h
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 → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
a : T
d : ∀ᶠ (x : S) in 𝓝 z, f x = a
ha : f z = a
⊢ HasMFDerivAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z 0
Theorem: nontrivialHolomorphicAt_of_mfderiv_ne_zero
Proof state before:
case h
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 → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
a : T
d : ∀ᶠ (x : S) in 𝓝 z, f x = a
ha : f z = a
⊢ HasMFDerivAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z 0
Tactic:
exact (hasMFDerivAt_const I I a _).congr_of_eventuallyEq d
Proof state after:
no goals
Theorem: NontrivialHolomorphicAt.comp
Proof 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
Proof 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)
Theorem: NontrivialHolomorphicAt.comp
Proof 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)
Proof 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))
Theorem: NontrivialHolomorphicAt.comp
Proof 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
Proof state after:
no goals
Theorem: NontrivialHolomorphicAt.anti
Proof 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 : T → U
g : S → T
z : S
h : NontrivialHolomorphicAt (fun z => f (g z)) z
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
⊢ NontrivialHolomorphicAt f (g z) ∧ NontrivialHolomorphicAt g z
Tactic:
replace h := h.nonconst
Proof 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 : T → U
g : S → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
h : ∃ᶠ (w : S) in 𝓝 z, f (g w) ≠ f (g z)
⊢ NontrivialHolomorphicAt f (g z) ∧ NontrivialHolomorphicAt g z
Theorem: NontrivialHolomorphicAt.anti
Proof 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 : T → U
g : S → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
h : ∃ᶠ (w : S) in 𝓝 z, f (g w) ≠ f (g z)
⊢ NontrivialHolomorphicAt f (g z) ∧ NontrivialHolomorphicAt g z
Tactic:
refine ⟨⟨fa, ?_⟩, ⟨ga, ?_⟩⟩
Proof state after:
case refine_1
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 : T → U
g : S → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
h : ∃ᶠ (w : S) in 𝓝 z, f (g w) ≠ f (g z)
⊢ ∃ᶠ (w : T) in 𝓝 (g z), f w ≠ f (g z)

case refine_2
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 : T → U
g : S → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
h : ∃ᶠ (w : S) in 𝓝 z, f (g w) ≠ f (g z)
⊢ ∃ᶠ (w : S) in 𝓝 z, g w ≠ g z
Theorem: NontrivialHolomorphicAt.anti
Proof state before:
case refine_1
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 : T → U
g : S → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
h : ∃ᶠ (w : S) in 𝓝 z, f (g w) ≠ f (g z)
⊢ ∃ᶠ (w : T) in 𝓝 (g z), f w ≠ f (g z)
Tactic:
contrapose h
Proof state after:
case refine_1
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 : T → U
g : S → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
h : ¬∃ᶠ (w : T) in 𝓝 (g z), f w ≠ f (g z)
⊢ ¬∃ᶠ (w : S) in 𝓝 z, f (g w) ≠ f (g z)