internlm/Lean-Github huggingface dataset:
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inr
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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
fa :
  AnalyticAt ℂ (fun x => ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm x)))
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z)
gc : ContinuousAt g z
ga :
  AnalyticAt ℂ (fun x => ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm x)))
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z)
fg : f z = g z
e :
  ∀ᶠ (z_1 : ℂ) in 𝓝[≠] ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z,
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm z_1)) ≠
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm z_1))
⊢ (∀ᶠ (w : S) in 𝓝 z, f w = g w) ∨ ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
Tactic:
right
Proof state after:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
fa :
  AnalyticAt ℂ (fun x => ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm x)))
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z)
gc : ContinuousAt g z
ga :
  AnalyticAt ℂ (fun x => ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm x)))
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z)
fg : f z = g z
e :
  ∀ᶠ (z_1 : ℂ) in 𝓝[≠] ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z,
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm z_1)) ≠
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm z_1))
⊢ ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
fa :
  AnalyticAt ℂ (fun x => ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm x)))
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z)
gc : ContinuousAt g z
ga :
  AnalyticAt ℂ (fun x => ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm x)))
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z)
fg : f z = g z
e :
  ∀ᶠ (z_1 : ℂ) in 𝓝[≠] ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z,
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm z_1)) ≠
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm z_1))
⊢ ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
Tactic:
clear fa ga
Proof state after:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
e :
  ∀ᶠ (z_1 : ℂ) in 𝓝[≠] ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z,
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm z_1)) ≠
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm z_1))
⊢ ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
e :
  ∀ᶠ (z_1 : ℂ) in 𝓝[≠] ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z,
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm z_1)) ≠
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm z_1))
⊢ ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
Tactic:
simp only [eventually_nhdsWithin_iff, Set.mem_compl_singleton_iff] at e ⊢
Proof state after:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
e :
  ∀ᶠ (x : ℂ) in 𝓝 (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z),
    x ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z →
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm x)) ≠
        ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm x))
⊢ ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ g x
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
e :
  ∀ᶠ (x : ℂ) in 𝓝 (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z),
    x ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z →
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm x)) ≠
        ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm x))
⊢ ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ g x
Tactic:
replace e := (continuousAt_extChartAt I z).eventually e
Proof state after:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
e :
  ∀ᶠ (x : S) in 𝓝 z,
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z →
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))) ≠
        ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))
⊢ ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ g x
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
e :
  ∀ᶠ (x : S) in 𝓝 z,
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z →
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))) ≠
        ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))
⊢ ∀ᶠ (x : S) in 𝓝 z, x ≠ z → f x ≠ g x
Tactic:
apply (fc.eventually_mem ((extChartAt_source_mem_nhds I (f z)))).mp
Proof state after:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
e :
  ∀ᶠ (x : S) in 𝓝 z,
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z →
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))) ≠
        ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))
⊢ ∀ᶠ (x : S) in 𝓝 z, f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source → x ≠ z → f x ≠ g x
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
e :
  ∀ᶠ (x : S) in 𝓝 z,
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z →
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))) ≠
        ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))
⊢ ∀ᶠ (x : S) in 𝓝 z, f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source → x ≠ z → f x ≠ g x
Tactic:
apply (gc.eventually_mem ((extChartAt_source_mem_nhds I (g z)))).mp
Proof state after:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
e :
  ∀ᶠ (x : S) in 𝓝 z,
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z →
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))) ≠
        ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))
⊢ ∀ᶠ (x : S) in 𝓝 z,
    g x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (g z)).source → f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source → x ≠ z → f x ≠ g x
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
e :
  ∀ᶠ (x : S) in 𝓝 z,
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z →
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))) ≠
        ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))
⊢ ∀ᶠ (x : S) in 𝓝 z,
    g x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (g z)).source → f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source → x ≠ z → f x ≠ g x
Tactic:
apply ((isOpen_extChartAt_source I z).eventually_mem (mem_extChartAt_source I z)).mp
Proof state after:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
e :
  ∀ᶠ (x : S) in 𝓝 z,
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z →
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))) ≠
        ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))
⊢ ∀ᶠ (x : S) in 𝓝 z,
    x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) z).source →
      g x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (g z)).source →
        f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source → x ≠ z → f x ≠ g x
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
e :
  ∀ᶠ (x : S) in 𝓝 z,
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z →
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))) ≠
        ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))
⊢ ∀ᶠ (x : S) in 𝓝 z,
    x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) z).source →
      g x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (g z)).source →
        f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source → x ≠ z → f x ≠ g x
Tactic:
refine e.mp (eventually_of_forall ?_)
Proof state after:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
e :
  ∀ᶠ (x : S) in 𝓝 z,
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z →
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))) ≠
        ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))
⊢ ∀ (x : S),
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z →
        ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z))
            (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))) ≠
          ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z))
            (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) →
      x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) z).source →
        g x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (g z)).source →
          f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source → x ≠ z → f x ≠ g x
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
e :
  ∀ᶠ (x : S) in 𝓝 z,
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z →
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))) ≠
        ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))
⊢ ∀ (x : S),
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z →
        ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z))
            (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))) ≠
          ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z))
            (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) →
      x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) z).source →
        g x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (g z)).source →
          f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source → x ≠ z → f x ≠ g x
Tactic:
clear e
Proof state after:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
⊢ ∀ (x : S),
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z →
        ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z))
            (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))) ≠
          ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z))
            (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) →
      x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) z).source →
        g x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (g z)).source →
          f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source → x ≠ z → f x ≠ g x
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
⊢ ∀ (x : S),
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z →
        ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z))
            (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))) ≠
          ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z))
            (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) →
      x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) z).source →
        g x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (g z)).source →
          f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source → x ≠ z → f x ≠ g x
Tactic:
intro x h xm gm fm xz
Proof state after:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
x : S
h :
  ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z →
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))) ≠
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))
xm : x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) z).source
gm : g x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (g z)).source
fm : f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source
xz : x ≠ z
⊢ f x ≠ g x
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
x : S
h :
  ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z →
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))) ≠
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))
xm : x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) z).source
gm : g x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (g z)).source
fm : f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source
xz : x ≠ z
⊢ f x ≠ g x
Tactic:
rw [← fg] at gm
Proof state after:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
x : S
h :
  ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z →
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))) ≠
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))
xm : x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) z).source
gm : g x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source
fm : f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source
xz : x ≠ z
⊢ f x ≠ g x
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
x : S
h :
  ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z →
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))) ≠
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))
xm : x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) z).source
gm : g x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source
fm : f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source
xz : x ≠ z
⊢ f x ≠ g x
Tactic:
simp only [← fg, PartialEquiv.left_inv _ xm] at h
Proof state after:
case neg.inr.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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
fc : ContinuousAt f z
gc : ContinuousAt g z
fg : f z = g z
x : S
xm : x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) z).source
gm : g x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source
fm : f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source
xz : x ≠ z
h :
  ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z →
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f x) ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (g x)
⊢ f x ≠ g x