internlm/Lean-Github huggingface dataset:
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
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 : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
ef : ∀ d ∈ ball c (min t r), ∀ w ∈ sphere z r, e / 2 ≤ ‖f d w - f d z‖
⊢ ball c (min t r) ×ˢ closedBall z r ⊆ closedBall c r ×ˢ closedBall z r
Tactic:
apply prod_mono_left
Proof state after:
case hs
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 : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
ef : ∀ d ∈ ball c (min t r), ∀ w ∈ sphere z r, e / 2 ≤ ‖f d w - f d z‖
⊢ ball c (min t r) ⊆ closedBall c r
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
Proof state before:
case hs
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 : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
ef : ∀ d ∈ ball c (min t r), ∀ w ∈ sphere z r, e / 2 ≤ ‖f d w - f d z‖
⊢ ball c (min t r) ⊆ closedBall c r
Tactic:
exact _root_.trans (Metric.ball_subset_ball (min_le_right _ _)) Metric.ball_subset_closedBall
Proof state after:
no goals
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
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 : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
ef : ∀ d ∈ ball c (min t r), ∀ w ∈ sphere z r, e / 2 ≤ ‖f d w - f d z‖
ss : ball c (min t r) ×ˢ closedBall z r ⊆ s
⊢ 0 < min t r
Tactic:
bound
Proof state after:
no goals
Theorem: NontrivialHolomorphicAt.inCharts
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 → T
z : S
n : NontrivialHolomorphicAt f z
⊢ NontrivialHolomorphicAt (fun w => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm w)))
    (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Tactic:
use n.holomorphicAt.2.holomorphicAt I I
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 → T
z : S
n : NontrivialHolomorphicAt f z
⊢ ∃ᶠ (w : ℂ) in 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) z) z),
    ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm w)) ≠
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z)))
Theorem: NontrivialHolomorphicAt.inCharts
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 → T
z : S
n : NontrivialHolomorphicAt f z
⊢ ∃ᶠ (w : ℂ) in 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) z) z),
    ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm w)) ≠
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z)))
Tactic:
have c := n.nonconst
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 → T
z : S
n : NontrivialHolomorphicAt f z
c : ∃ᶠ (w : S) in 𝓝 z, f w ≠ f z
⊢ ∃ᶠ (w : ℂ) in 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) z) z),
    ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm w)) ≠
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z)))
Theorem: NontrivialHolomorphicAt.inCharts
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 → T
z : S
n : NontrivialHolomorphicAt f z
c : ∃ᶠ (w : S) in 𝓝 z, f w ≠ f z
⊢ ∃ᶠ (w : ℂ) in 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) z) z),
    ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm w)) ≠
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z)))
Tactic:
contrapose c
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 → T
z : S
n : NontrivialHolomorphicAt f z
c :
  ¬∃ᶠ (w : ℂ) in 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) z) z),
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm w)) ≠
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z)))
⊢ ¬∃ᶠ (w : S) in 𝓝 z, f w ≠ f z
Theorem: NontrivialHolomorphicAt.inCharts
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 → T
z : S
n : NontrivialHolomorphicAt f z
c :
  ¬∃ᶠ (w : ℂ) in 𝓝 (↑(extChartAt 𝓘(ℂ, ℂ) z) z),
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm w)) ≠
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z)))
⊢ ¬∃ᶠ (w : S) in 𝓝 z, f w ≠ f z
Tactic:
simp only [Filter.not_frequently, not_not, ← extChartAt_map_nhds' I z,
  Filter.eventually_map] at c ⊢
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 → T
z : S
n : NontrivialHolomorphicAt f z
c :
  ∀ᶠ (a : S) in 𝓝 z,
    ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) a))) =
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z)))
⊢ ∀ᶠ (x : S) in 𝓝 z, f x = f z
Theorem: NontrivialHolomorphicAt.inCharts
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 → T
z : S
n : NontrivialHolomorphicAt f z
c :
  ∀ᶠ (a : S) in 𝓝 z,
    ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) a))) =
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z)))
⊢ ∀ᶠ (x : S) in 𝓝 z, f x = f z
Tactic:
apply c.mp
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 → T
z : S
n : NontrivialHolomorphicAt f z
c :
  ∀ᶠ (a : S) in 𝓝 z,
    ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) a))) =
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z)))
⊢ ∀ᶠ (x : S) in 𝓝 z,
    ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x))) =
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z))) →
      f x = f z
Theorem: NontrivialHolomorphicAt.inCharts
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 → T
z : S
n : NontrivialHolomorphicAt f z
c :
  ∀ᶠ (a : S) in 𝓝 z,
    ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) a))) =
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z)))
⊢ ∀ᶠ (x : S) in 𝓝 z,
    ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x))) =
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z))) →
      f x = f z
Tactic:
apply ((isOpen_extChartAt_source I z).eventually_mem (mem_extChartAt_source I z)).mp
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 → T
z : S
n : NontrivialHolomorphicAt f z
c :
  ∀ᶠ (a : S) in 𝓝 z,
    ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) a))) =
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z)))
⊢ ∀ᶠ (x : S) in 𝓝 z,
    x ∈ (extChartAt 𝓘(ℂ, ℂ) z).source →
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x))) =
          ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z))) →
        f x = f z
Theorem: NontrivialHolomorphicAt.inCharts
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 → T
z : S
n : NontrivialHolomorphicAt f z
c :
  ∀ᶠ (a : S) in 𝓝 z,
    ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) a))) =
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z)))
⊢ ∀ᶠ (x : S) in 𝓝 z,
    x ∈ (extChartAt 𝓘(ℂ, ℂ) z).source →
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x))) =
          ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z))) →
        f x = f z
Tactic:
apply (n.holomorphicAt.continuousAt.eventually_mem (extChartAt_source_mem_nhds I (f z))).mp
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 → T
z : S
n : NontrivialHolomorphicAt f z
c :
  ∀ᶠ (a : S) in 𝓝 z,
    ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) a))) =
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z)))
⊢ ∀ᶠ (x : S) in 𝓝 z,
    f x ∈ (extChartAt 𝓘(ℂ, ℂ) (f z)).source →
      x ∈ (extChartAt 𝓘(ℂ, ℂ) z).source →
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x))) =
            ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z))) →
          f x = f z
Theorem: NontrivialHolomorphicAt.inCharts
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 → T
z : S
n : NontrivialHolomorphicAt f z
c :
  ∀ᶠ (a : S) in 𝓝 z,
    ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) a))) =
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z)))
⊢ ∀ᶠ (x : S) in 𝓝 z,
    f x ∈ (extChartAt 𝓘(ℂ, ℂ) (f z)).source →
      x ∈ (extChartAt 𝓘(ℂ, ℂ) z).source →
        ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) x))) =
            ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z))) →
          f x = f z
Tactic:
refine eventually_of_forall fun w fm m fn ↦ ?_
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 → T
z : S
n : NontrivialHolomorphicAt f z
c :
  ∀ᶠ (a : S) in 𝓝 z,
    ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) a))) =
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z)))
w : S
fm : f w ∈ (extChartAt 𝓘(ℂ, ℂ) (f z)).source
m : w ∈ (extChartAt 𝓘(ℂ, ℂ) z).source
fn :
  ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) w))) =
    ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z)))
⊢ f w = f z
Theorem: NontrivialHolomorphicAt.inCharts
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 → T
z : S
n : NontrivialHolomorphicAt f z
c :
  ∀ᶠ (a : S) in 𝓝 z,
    ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) a))) =
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z)))
w : S
fm : f w ∈ (extChartAt 𝓘(ℂ, ℂ) (f z)).source
m : w ∈ (extChartAt 𝓘(ℂ, ℂ) z).source
fn :
  ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) w))) =
    ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z)))
⊢ f w = f z
Tactic:
rw [PartialEquiv.left_inv _ m, PartialEquiv.left_inv _ (mem_extChartAt_source I z)] at fn
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 → T
z : S
n : NontrivialHolomorphicAt f z
c :
  ∀ᶠ (a : S) in 𝓝 z,
    ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) a))) =
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z)))
w : S
fm : f w ∈ (extChartAt 𝓘(ℂ, ℂ) (f z)).source
m : w ∈ (extChartAt 𝓘(ℂ, ℂ) z).source
fn : ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f w) = ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f z)
⊢ f w = f z
Theorem: NontrivialHolomorphicAt.inCharts
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 → T
z : S
n : NontrivialHolomorphicAt f z
c :
  ∀ᶠ (a : S) in 𝓝 z,
    ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) a))) =
      ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm (↑(extChartAt 𝓘(ℂ, ℂ) z) z)))
w : S
fm : f w ∈ (extChartAt 𝓘(ℂ, ℂ) (f z)).source
m : w ∈ (extChartAt 𝓘(ℂ, ℂ) z).source
fn : ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f w) = ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f z)
⊢ f w = f z
Tactic:
exact ((PartialEquiv.injOn _).eq_iff fm (mem_extChartAt_source _ _)).mp fn
Proof state after:
no goals
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
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 → T
z : S
n : NontrivialHolomorphicAt f z
⊢ 𝓝 (f z) = Filter.map f (𝓝 z)
Tactic:
refine le_antisymm ?_ n.holomorphicAt.continuousAt
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 → T
z : S
n : NontrivialHolomorphicAt f z
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
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 → T
z : S
n : NontrivialHolomorphicAt f z
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Tactic:
generalize hg : (fun x ↦ extChartAt I (f z) (f ((extChartAt I z).symm x))) = g
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 → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Theorem: NontrivialHolomorphicAt.nhds_eq_map_nhds
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 → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)
Tactic:
have ga : AnalyticAt ℂ g (extChartAt I z z) := by rw [← hg]; exact n.holomorphicAt.2
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 → T
z : S
n : NontrivialHolomorphicAt f z
g : ℂ → ℂ
hg : (fun x => ↑(extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(extChartAt 𝓘(ℂ, ℂ) z).symm x))) = g
ga : AnalyticAt ℂ g (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ 𝓝 (f z) ≤ Filter.map f (𝓝 z)