internlm/Lean-Github huggingface dataset:
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inl
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:
left
Proof state after:
case neg.inl.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.inl.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.inl.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.inl.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:
replace e := (continuousAt_extChartAt I z).eventually e
Proof state after:
case neg.inl.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 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))) =
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))
⊢ ∀ᶠ (w : S) in 𝓝 z, f w = g w
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inl.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 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))) =
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))
⊢ ∀ᶠ (w : S) in 𝓝 z, f w = g w
Tactic:
replace e := Filter.EventuallyEq.fun_comp e (_root_.extChartAt I (f z)).symm
Proof state after:
case neg.inl.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).EventuallyEq
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm ∘ fun x =>
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))))
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm ∘ fun x =>
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))))
⊢ ∀ᶠ (w : S) in 𝓝 z, f w = g w
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inl.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).EventuallyEq
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm ∘ fun x =>
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))))
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm ∘ fun x =>
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))))
⊢ ∀ᶠ (w : S) in 𝓝 z, f w = g w
Tactic:
apply e.congr
Proof state after:
case neg.inl.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).EventuallyEq
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm ∘ fun x =>
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))))
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm ∘ fun x =>
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))))
⊢ ∀ᶠ (x : S) in 𝓝 z,
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm ∘ fun x =>
            ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z))
              (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))))
          x =
        (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm ∘ fun x =>
            ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z))
              (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))))
          x ↔
      f x = g x
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inl.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).EventuallyEq
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm ∘ fun x =>
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))))
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm ∘ fun x =>
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))))
⊢ ∀ᶠ (x : S) in 𝓝 z,
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm ∘ fun x =>
            ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z))
              (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))))
          x =
        (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm ∘ fun x =>
            ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z))
              (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))))
          x ↔
      f x = g x
Tactic:
simp only [Function.comp]
Proof state after:
case neg.inl.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).EventuallyEq
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm ∘ fun x =>
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))))
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm ∘ fun x =>
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))))
⊢ ∀ᶠ (x : S) in 𝓝 z,
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z))
            (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) =
        ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z))
            (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) ↔
      f x = g x
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inl.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).EventuallyEq
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm ∘ fun x =>
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))))
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm ∘ fun x =>
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x))))
⊢ ∀ᶠ (x : S) in 𝓝 z,
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z))
            (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) =
        ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z))
            (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) ↔
      f x = g x
Tactic:
clear e
Proof state after:
case neg.inl.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) in 𝓝 z,
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z))
            (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) =
        ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z))
            (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) ↔
      f x = g x
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inl.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) in 𝓝 z,
    ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z))
            (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) =
        ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
          (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z))
            (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) ↔
      f x = g x
Tactic:
apply (fc.eventually_mem (extChartAt_source_mem_nhds I (f z))).mp
Proof state after:
case neg.inl.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) in 𝓝 z,
    f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source →
      (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
            (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z))
              (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) =
          ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
            (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z))
              (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) ↔
        f x = g x)
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inl.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) in 𝓝 z,
    f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source →
      (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
            (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z))
              (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) =
          ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
            (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z))
              (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) ↔
        f x = g x)
Tactic:
apply (gc.eventually_mem (extChartAt_source_mem_nhds I (g z))).mp
Proof state after:
case neg.inl.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) in 𝓝 z,
    g x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (g z)).source →
      f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source →
        (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
              (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z))
                (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) =
            ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
              (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z))
                (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) ↔
          f x = g x)
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inl.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) in 𝓝 z,
    g x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (g z)).source →
      f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source →
        (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
              (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z))
                (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) =
            ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
              (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z))
                (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) ↔
          f x = g x)
Tactic:
refine eventually_nhds_iff.mpr ⟨(_root_.extChartAt I z).source,
  fun x m gm fm ↦ ?_, isOpen_extChartAt_source _ _, mem_extChartAt_source I z⟩
Proof state after:
case neg.inl.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
m : x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) z).source
gm : g x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (g z)).source
fm : f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source
⊢ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
        (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z))
          (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) =
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
        (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z))
          (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) ↔
    f x = g x
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inl.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
m : x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) z).source
gm : g x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (g z)).source
fm : f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source
⊢ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
        (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z))
          (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) =
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
        (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z))
          (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) ↔
    f x = g x
Tactic:
rw [← fg] at gm
Proof state after:
case neg.inl.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
m : x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) z).source
gm : g x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source
fm : f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source
⊢ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
        (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z))
          (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) =
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
        (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z))
          (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) ↔
    f x = g x
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg.inl.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
m : x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) z).source
gm : g x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source
fm : f x ∈ (_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).source
⊢ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
        (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z))
          (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) =
      ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)).symm
        (↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z))
          (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) x)))) ↔
    f x = g x
Tactic:
simp only [← fg, PartialEquiv.left_inv _ m, PartialEquiv.left_inv _ fm,
  PartialEquiv.left_inv _ gm]
Proof state after:
no goals