internlm/Lean-Github huggingface dataset:
Theorem: nontrivialHolomorphicAt_id
Proof state before:
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
Tactic:
rw [← (PartialEquiv.injOn _).ne_iff ((extChartAt I z).map_target au.1) (mem_extChartAt_source I z)]
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) (↑(extChartAt 𝓘(ℂ, ℂ) z).symm a) ≠ ↑(extChartAt 𝓘(ℂ, ℂ) z) z
Theorem: nontrivialHolomorphicAt_id
Proof state before:
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) (↑(extChartAt 𝓘(ℂ, ℂ) z).symm a) ≠ ↑(extChartAt 𝓘(ℂ, ℂ) z) z
Tactic:
rw [PartialEquiv.right_inv _ au.1, ← ha]
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) z + ↑r / 2 ≠ ↑(extChartAt 𝓘(ℂ, ℂ) z) z
Theorem: nontrivialHolomorphicAt_id
Proof state before:
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) z + ↑r / 2 ≠ ↑(extChartAt 𝓘(ℂ, ℂ) z) z
Tactic:
simp only [Ne, add_right_eq_self, div_eq_zero_iff, Complex.ofReal_eq_zero, bit0_eq_zero,
  one_ne_zero, or_false_iff, rp.ne', not_false_iff]
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
⊢ ¬(False ∨ 2 = 0)
Theorem: nontrivialHolomorphicAt_id
Proof state before:
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
⊢ ¬(False ∨ 2 = 0)
Tactic:
norm_num
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
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
⊢ IsOpen u
Tactic:
rw [← hu]
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 ℂ
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
⊢ IsOpen ((extChartAt 𝓘(ℂ, ℂ) z).target ∩ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm ⁻¹' t)
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
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
⊢ IsOpen ((extChartAt 𝓘(ℂ, ℂ) z).target ∩ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm ⁻¹' t)
Tactic:
exact (continuousOn_extChartAt_symm I z).isOpen_inter_preimage (isOpen_extChartAt_target _ _) ot
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
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
⊢ ↑(extChartAt 𝓘(ℂ, ℂ) z) z ∈ u
Tactic:
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:
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
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
⊢ a ∈ u
Tactic:
rw [← ha]
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 ℂ
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
⊢ ↑(extChartAt 𝓘(ℂ, ℂ) z) z + ↑r / 2 ∈ u
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
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
⊢ ↑(extChartAt 𝓘(ℂ, ℂ) z) z + ↑r / 2 ∈ u
Tactic:
apply ru
Proof state after:
case 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 ℂ
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
⊢ ↑(extChartAt 𝓘(ℂ, ℂ) z) z + ↑r / 2 ∈ ball (↑(extChartAt 𝓘(ℂ, ℂ) z) z) r
Theorem: nontrivialHolomorphicAt_id
Proof state before:
case 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 ℂ
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
⊢ ↑(extChartAt 𝓘(ℂ, ℂ) z) z + ↑r / 2 ∈ ball (↑(extChartAt 𝓘(ℂ, ℂ) z) z) r
Tactic:
simp only [Metric.mem_ball, Complex.dist_eq, add_sub_cancel_left]
Proof state after:
case 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 ℂ
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
⊢ Complex.abs (↑r / 2) < r
Theorem: nontrivialHolomorphicAt_id
Proof state before:
case 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 ℂ
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
⊢ Complex.abs (↑r / 2) < r
Tactic:
simp only [map_div₀, Complex.abs_ofReal, abs_of_pos rp, Complex.abs_two]
Proof state after:
case 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 ℂ
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
⊢ r / 2 < r
Theorem: nontrivialHolomorphicAt_id
Proof state before:
case 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 ℂ
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
⊢ r / 2 < r
Tactic:
exact half_lt_self rp
Proof state after:
no goals
Theorem: nontrivialHolomorphicAt_of_order
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 : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : orderAt f z ≠ 0
⊢ NontrivialHolomorphicAt f z
Tactic:
use fa.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 : Set ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : orderAt f z ≠ 0
⊢ ∃ᶠ (w : ℂ) in 𝓝 z, f w ≠ f z
Theorem: nontrivialHolomorphicAt_of_order
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : orderAt f z ≠ 0
⊢ ∃ᶠ (w : ℂ) in 𝓝 z, f w ≠ f z
Tactic:
contrapose h
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ¬∃ᶠ (w : ℂ) in 𝓝 z, f w ≠ f z
⊢ ¬orderAt f z ≠ 0
Theorem: nontrivialHolomorphicAt_of_order
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ¬∃ᶠ (w : ℂ) in 𝓝 z, f w ≠ f z
⊢ ¬orderAt f z ≠ 0
Tactic:
simp only [Filter.not_frequently, not_not] at h ⊢
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
⊢ orderAt f z = 0
Theorem: nontrivialHolomorphicAt_of_order
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
⊢ orderAt f z = 0
Tactic:
have fp : HasFPowerSeriesAt f (constFormalMultilinearSeries ℂ ℂ (f z)) z :=
  hasFPowerSeriesAt_const.congr (Filter.EventuallyEq.symm h)
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
fp : HasFPowerSeriesAt f (constFormalMultilinearSeries ℂ ℂ (f z)) z
⊢ orderAt f z = 0
Theorem: nontrivialHolomorphicAt_of_order
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
fp : HasFPowerSeriesAt f (constFormalMultilinearSeries ℂ ℂ (f z)) z
⊢ orderAt f z = 0
Tactic:
simp only [fp.orderAt_unique]
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
fp : HasFPowerSeriesAt f (constFormalMultilinearSeries ℂ ℂ (f z)) z
⊢ (constFormalMultilinearSeries ℂ ℂ (f z)).order = 0
Theorem: nontrivialHolomorphicAt_of_order
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
fp : HasFPowerSeriesAt f (constFormalMultilinearSeries ℂ ℂ (f z)) z
⊢ (constFormalMultilinearSeries ℂ ℂ (f z)).order = 0
Tactic:
by_contra p0
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
fp : HasFPowerSeriesAt f (constFormalMultilinearSeries ℂ ℂ (f z)) z
p0 : ¬(constFormalMultilinearSeries ℂ ℂ (f z)).order = 0
⊢ False
Theorem: nontrivialHolomorphicAt_of_order
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
fp : HasFPowerSeriesAt f (constFormalMultilinearSeries ℂ ℂ (f z)) z
p0 : ¬(constFormalMultilinearSeries ℂ ℂ (f z)).order = 0
⊢ False
Tactic:
have b := FormalMultilinearSeries.apply_order_ne_zero' p0
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 ℂ
f : ℂ → ℂ
z : ℂ
fa : AnalyticAt ℂ f z
h : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
fp : HasFPowerSeriesAt f (constFormalMultilinearSeries ℂ ℂ (f z)) z
p0 : ¬(constFormalMultilinearSeries ℂ ℂ (f z)).order = 0
b : constFormalMultilinearSeries ℂ ℂ (f z) (constFormalMultilinearSeries ℂ ℂ (f z)).order ≠ 0
⊢ False