Theorem: NontrivialHolomorphicAt.inCharts (Ray/AnalyticManifold/OpenMapping.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 → 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
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)))

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

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

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

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

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

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

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 ↦ ?_
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

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

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