Theorem: nontrivialHolomorphicAt_id (Ray/AnalyticManifold/Nontrivial.lean)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
s : Set ℂ
z : S
⊢ NontrivialHolomorphicAt (fun w => w) z
Tactic:
use holomorphicAt_id
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

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]
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

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
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

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⟩
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

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
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

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
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

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]
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

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⟩
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

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
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

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
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

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
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

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
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

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
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

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)]
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

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]
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

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]
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)

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
State after:
no goals

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]
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)

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
State after:
no goals

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]
State after:
no goals

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]
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

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
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

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]
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

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]
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

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
State after:
no goals