internlm/Lean-Github huggingface dataset:
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 : T) in 𝓝 (g z), f w ≠ f (g z)
⊢ ¬∃ᶠ (w : S) in 𝓝 z, f (g w) ≠ f (g z)
Tactic:
simp only [Filter.not_frequently, not_not] at 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 : ∀ᶠ (x : T) in 𝓝 (g z), f x = f (g z)
⊢ ∀ᶠ (x : S) in 𝓝 z, f (g x) = f (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 : ∀ᶠ (x : T) in 𝓝 (g z), f x = f (g z)
⊢ ∀ᶠ (x : S) in 𝓝 z, f (g x) = f (g z)
Tactic:
exact (ga.continuousAt.eventually h).mp (eventually_of_forall fun _ h ↦ h)
Proof state after:
no goals
Theorem: NontrivialHolomorphicAt.anti
Proof state before:
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
Tactic:
contrapose h
Proof state after:
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, g w ≠ g z
⊢ ¬∃ᶠ (w : S) in 𝓝 z, f (g w) ≠ f (g z)
Theorem: NontrivialHolomorphicAt.anti
Proof state before:
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, g w ≠ g z
⊢ ¬∃ᶠ (w : S) in 𝓝 z, f (g w) ≠ f (g z)
Tactic:
simp only [Filter.not_frequently, not_not] at h ⊢
Proof state after:
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 : ∀ᶠ (x : S) in 𝓝 z, g x = g z
⊢ ∀ᶠ (x : S) in 𝓝 z, f (g x) = f (g z)
Theorem: NontrivialHolomorphicAt.anti
Proof state before:
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 : ∀ᶠ (x : S) in 𝓝 z, g x = g z
⊢ ∀ᶠ (x : S) in 𝓝 z, f (g x) = f (g z)
Tactic:
exact h.mp (eventually_of_forall fun x h ↦ by rw [h])
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
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (g z)
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
h✝ : ∀ᶠ (x : S) in 𝓝 z, g x = g z
x : S
h : g x = g z
⊢ f (g x) = f (g z)
Tactic:
rw [h]
Proof state after:
no goals
Theorem: nontrivialHolomorphicAt_id
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 ℂ
z : S
⊢ NontrivialHolomorphicAt (fun w => w) z
Tactic:
use holomorphicAt_id
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 ℂ
z : S
⊢ ∃ᶠ (w : S) in 𝓝 z, w ≠ z
Theorem: nontrivialHolomorphicAt_id
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 ℂ
z : S
⊢ ∃ᶠ (w : S) in 𝓝 z, w ≠ z
Tactic:
rw [Filter.frequently_iff]
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 ℂ
z : S
⊢ ∀ {U : Set S}, U ∈ 𝓝 z → ∃ x ∈ U, x ≠ z
Theorem: nontrivialHolomorphicAt_id
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 ℂ
z : S
⊢ ∀ {U : Set S}, U ∈ 𝓝 z → ∃ x ∈ U, x ≠ z
Tactic:
intro s sz
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 ℂ
z : S
s : Set S
sz : s ∈ 𝓝 z
⊢ ∃ x ∈ s, x ≠ z
Theorem: nontrivialHolomorphicAt_id
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 ℂ
z : S
s : Set S
sz : s ∈ 𝓝 z
⊢ ∃ x ∈ s, x ≠ z
Tactic:
rcases mem_nhds_iff.mp sz with ⟨t, ts, ot, zt⟩
Proof state after:
case nonconst.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 ℂ
z : S
s : Set S
sz : s ∈ 𝓝 z
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
⊢ ∃ x ∈ s, x ≠ z
Theorem: nontrivialHolomorphicAt_id
Proof state before:
case nonconst.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 ℂ
z : S
s : Set S
sz : s ∈ 𝓝 z
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
⊢ ∃ x ∈ s, x ≠ z
Tactic:
generalize hu : (extChartAt I z).target ∩ (extChartAt I z).symm ⁻¹' t = u
Proof state after:
case nonconst.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 ℂ
z : S
s : Set S
sz : s ∈ 𝓝 z
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
u : Set ℂ
hu : (extChartAt 𝓘(ℂ, ℂ) z).target ∩ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm ⁻¹' t = u
⊢ ∃ x ∈ s, x ≠ z
Theorem: nontrivialHolomorphicAt_id
Proof state before:
case nonconst.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 ℂ
z : S
s : Set S
sz : s ∈ 𝓝 z
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
u : Set ℂ
hu : (extChartAt 𝓘(ℂ, ℂ) z).target ∩ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm ⁻¹' t = u
⊢ ∃ x ∈ s, x ≠ z
Tactic:
have uo : IsOpen u := by
  rw [← hu]
  exact (continuousOn_extChartAt_symm I z).isOpen_inter_preimage (isOpen_extChartAt_target _ _) ot
Proof state after:
case nonconst.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 ℂ
z : S
s : Set S
sz : s ∈ 𝓝 z
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
u : Set ℂ
hu : (extChartAt 𝓘(ℂ, ℂ) z).target ∩ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm ⁻¹' t = u
uo : IsOpen u
⊢ ∃ x ∈ s, x ≠ z
Theorem: nontrivialHolomorphicAt_id
Proof state before:
case nonconst.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 ℂ
z : S
s : Set S
sz : s ∈ 𝓝 z
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
u : Set ℂ
hu : (extChartAt 𝓘(ℂ, ℂ) z).target ∩ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm ⁻¹' t = u
uo : IsOpen u
⊢ ∃ x ∈ s, x ≠ z
Tactic:
have zu : extChartAt I z z ∈ u := by
  simp only [mem_inter_iff, mem_extChartAt_target, true_and_iff, mem_preimage,
    PartialEquiv.left_inv _ (mem_extChartAt_source I z), zt, ← hu]
Proof state after:
case nonconst.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 ℂ
z : S
s : Set S
sz : s ∈ 𝓝 z
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
u : Set ℂ
hu : (extChartAt 𝓘(ℂ, ℂ) z).target ∩ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm ⁻¹' t = u
uo : IsOpen u
zu : ↑(extChartAt 𝓘(ℂ, ℂ) z) z ∈ u
⊢ ∃ x ∈ s, x ≠ z
Theorem: nontrivialHolomorphicAt_id
Proof state before:
case nonconst.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 ℂ
z : S
s : Set S
sz : s ∈ 𝓝 z
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
u : Set ℂ
hu : (extChartAt 𝓘(ℂ, ℂ) z).target ∩ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm ⁻¹' t = u
uo : IsOpen u
zu : ↑(extChartAt 𝓘(ℂ, ℂ) z) z ∈ u
⊢ ∃ x ∈ s, x ≠ z
Tactic:
rcases Metric.isOpen_iff.mp uo _ zu with ⟨r, rp, ru⟩
Proof state after:
case nonconst.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 ℂ
z : S
s : Set S
sz : s ∈ 𝓝 z
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
u : Set ℂ
hu : (extChartAt 𝓘(ℂ, ℂ) z).target ∩ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm ⁻¹' t = u
uo : IsOpen u
zu : ↑(extChartAt 𝓘(ℂ, ℂ) z) z ∈ u
r : ℝ
rp : r > 0
ru : ball (↑(extChartAt 𝓘(ℂ, ℂ) z) z) r ⊆ u
⊢ ∃ x ∈ s, x ≠ z
Theorem: nontrivialHolomorphicAt_id
Proof state before:
case nonconst.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 ℂ
z : S
s : Set S
sz : s ∈ 𝓝 z
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
u : Set ℂ
hu : (extChartAt 𝓘(ℂ, ℂ) z).target ∩ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm ⁻¹' t = u
uo : IsOpen u
zu : ↑(extChartAt 𝓘(ℂ, ℂ) z) z ∈ u
r : ℝ
rp : r > 0
ru : ball (↑(extChartAt 𝓘(ℂ, ℂ) z) z) r ⊆ u
⊢ ∃ x ∈ s, x ≠ z
Tactic:
generalize ha : extChartAt I z z + r / 2 = a
Proof state after:
case nonconst.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 ℂ
z : S
s : Set S
sz : s ∈ 𝓝 z
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
u : Set ℂ
hu : (extChartAt 𝓘(ℂ, ℂ) z).target ∩ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm ⁻¹' t = u
uo : IsOpen u
zu : ↑(extChartAt 𝓘(ℂ, ℂ) z) z ∈ u
r : ℝ
rp : r > 0
ru : ball (↑(extChartAt 𝓘(ℂ, ℂ) z) z) r ⊆ u
a : ℂ
ha : ↑(extChartAt 𝓘(ℂ, ℂ) z) z + ↑r / 2 = a
⊢ ∃ x ∈ s, x ≠ z
Theorem: nontrivialHolomorphicAt_id
Proof state before:
case nonconst.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 ℂ
z : S
s : Set S
sz : s ∈ 𝓝 z
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
u : Set ℂ
hu : (extChartAt 𝓘(ℂ, ℂ) z).target ∩ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm ⁻¹' t = u
uo : IsOpen u
zu : ↑(extChartAt 𝓘(ℂ, ℂ) z) z ∈ u
r : ℝ
rp : r > 0
ru : ball (↑(extChartAt 𝓘(ℂ, ℂ) z) z) r ⊆ u
a : ℂ
ha : ↑(extChartAt 𝓘(ℂ, ℂ) z) z + ↑r / 2 = a
⊢ ∃ x ∈ s, x ≠ z
Tactic:
have au : a ∈ u := by
  rw [← ha]; apply ru; simp only [Metric.mem_ball, Complex.dist_eq, add_sub_cancel_left]
  simp only [map_div₀, Complex.abs_ofReal, abs_of_pos rp, Complex.abs_two]; exact half_lt_self rp
Proof state after:
case nonconst.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 ℂ
z : S
s : Set S
sz : s ∈ 𝓝 z
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
u : Set ℂ
hu : (extChartAt 𝓘(ℂ, ℂ) z).target ∩ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm ⁻¹' t = u
uo : IsOpen u
zu : ↑(extChartAt 𝓘(ℂ, ℂ) z) z ∈ u
r : ℝ
rp : r > 0
ru : ball (↑(extChartAt 𝓘(ℂ, ℂ) z) z) r ⊆ u
a : ℂ
ha : ↑(extChartAt 𝓘(ℂ, ℂ) z) z + ↑r / 2 = a
au : a ∈ u
⊢ ∃ x ∈ s, x ≠ z
Theorem: nontrivialHolomorphicAt_id
Proof state before:
case nonconst.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 ℂ
z : S
s : Set S
sz : s ∈ 𝓝 z
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
u : Set ℂ
hu : (extChartAt 𝓘(ℂ, ℂ) z).target ∩ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm ⁻¹' t = u
uo : IsOpen u
zu : ↑(extChartAt 𝓘(ℂ, ℂ) z) z ∈ u
r : ℝ
rp : r > 0
ru : ball (↑(extChartAt 𝓘(ℂ, ℂ) z) z) r ⊆ u
a : ℂ
ha : ↑(extChartAt 𝓘(ℂ, ℂ) z) z + ↑r / 2 = a
au : a ∈ u
⊢ ∃ x ∈ s, x ≠ z
Tactic:
use (extChartAt I z).symm a
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 ℂ
z : S
s : Set S
sz : s ∈ 𝓝 z
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
u : Set ℂ
hu : (extChartAt 𝓘(ℂ, ℂ) z).target ∩ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm ⁻¹' t = u
uo : IsOpen u
zu : ↑(extChartAt 𝓘(ℂ, ℂ) z) z ∈ u
r : ℝ
rp : r > 0
ru : ball (↑(extChartAt 𝓘(ℂ, ℂ) z) z) r ⊆ u
a : ℂ
ha : ↑(extChartAt 𝓘(ℂ, ℂ) z) z + ↑r / 2 = a
au : a ∈ u
⊢ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm a ∈ s ∧ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm a ≠ z
Theorem: nontrivialHolomorphicAt_id
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 ℂ
z : S
s : Set S
sz : s ∈ 𝓝 z
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
u : Set ℂ
hu : (extChartAt 𝓘(ℂ, ℂ) z).target ∩ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm ⁻¹' t = u
uo : IsOpen u
zu : ↑(extChartAt 𝓘(ℂ, ℂ) z) z ∈ u
r : ℝ
rp : r > 0
ru : ball (↑(extChartAt 𝓘(ℂ, ℂ) z) z) r ⊆ u
a : ℂ
ha : ↑(extChartAt 𝓘(ℂ, ℂ) z) z + ↑r / 2 = a
au : a ∈ u
⊢ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm a ∈ s ∧ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm a ≠ z
Tactic:
rw [← hu] at au
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 ℂ
z : S
s : Set S
sz : s ∈ 𝓝 z
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
u : Set ℂ
hu : (extChartAt 𝓘(ℂ, ℂ) z).target ∩ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm ⁻¹' t = u
uo : IsOpen u
zu : ↑(extChartAt 𝓘(ℂ, ℂ) z) z ∈ u
r : ℝ
rp : r > 0
ru : ball (↑(extChartAt 𝓘(ℂ, ℂ) z) z) r ⊆ u
a : ℂ
ha : ↑(extChartAt 𝓘(ℂ, ℂ) z) z + ↑r / 2 = a
au : a ∈ (extChartAt 𝓘(ℂ, ℂ) z).target ∩ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm ⁻¹' t
⊢ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm a ∈ s ∧ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm a ≠ z
Theorem: nontrivialHolomorphicAt_id
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 ℂ
z : S
s : Set S
sz : s ∈ 𝓝 z
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
u : Set ℂ
hu : (extChartAt 𝓘(ℂ, ℂ) z).target ∩ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm ⁻¹' t = u
uo : IsOpen u
zu : ↑(extChartAt 𝓘(ℂ, ℂ) z) z ∈ u
r : ℝ
rp : r > 0
ru : ball (↑(extChartAt 𝓘(ℂ, ℂ) z) z) r ⊆ u
a : ℂ
ha : ↑(extChartAt 𝓘(ℂ, ℂ) z) z + ↑r / 2 = a
au : a ∈ (extChartAt 𝓘(ℂ, ℂ) z).target ∩ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm ⁻¹' t
⊢ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm a ∈ s ∧ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm a ≠ z
Tactic:
use ts au.2
Proof state after:
case right
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 ℂ
z : S
s : Set S
sz : s ∈ 𝓝 z
t : Set S
ts : t ⊆ s
ot : IsOpen t
zt : z ∈ t
u : Set ℂ
hu : (extChartAt 𝓘(ℂ, ℂ) z).target ∩ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm ⁻¹' t = u
uo : IsOpen u
zu : ↑(extChartAt 𝓘(ℂ, ℂ) z) z ∈ u
r : ℝ
rp : r > 0
ru : ball (↑(extChartAt 𝓘(ℂ, ℂ) z) z) r ⊆ u
a : ℂ
ha : ↑(extChartAt 𝓘(ℂ, ℂ) z) z + ↑r / 2 = a
au : a ∈ (extChartAt 𝓘(ℂ, ℂ) z).target ∩ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm ⁻¹' t
⊢ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm a ≠ z