internlm/Lean-Github huggingface dataset:
Theorem: eq_of_pow_eq
Proof state before:
case refine_2
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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
x : X
m : x ∈ t
⊢ q x ^ d / p x ^ d = 1
Tactic:
rw [div_eq_one_iff_eq]
Proof state after:
case refine_2
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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
x : X
m : x ∈ t
⊢ q x ^ d = p x ^ d

case refine_2
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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
x : X
m : x ∈ t
⊢ p x ^ d ≠ 0
Theorem: eq_of_pow_eq
Proof state before:
case refine_2
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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
x : X
m : x ∈ t
⊢ q x ^ d = p x ^ d
Tactic:
exact (pqd _ m).symm
Proof state after:
no goals
Theorem: eq_of_pow_eq
Proof state before:
case refine_2
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 ℂ
p q : X → ℂ
t : Set X
d : ℕ
pc : ContinuousOn p t
qc : ContinuousOn q t
tc : IsPreconnected t
dp : d > 0
pq : ∃ x ∈ t, p x = q x
p0 : ∀ x ∈ t, p x ≠ 0
pqd : ∀ x ∈ t, p x ^ d = q x ^ d
r : X → ℂ
hr : (fun x => q x / p x) = r
rc : ContinuousOn r t
x : X
m : x ∈ t
⊢ p x ^ d ≠ 0
Tactic:
exact pow_ne_zero _ (p0 _ m)
Proof state after:
no goals
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
X : Type
inst✝⁷ : TopologicalSpace X
S : Type
inst✝⁶ : TopologicalSpace S
inst✝⁵ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝⁴ : TopologicalSpace T
inst✝³ : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝² : TopologicalSpace U
inst✝¹ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
inst✝ : T2Space T
f g : S → T
z : S
fa : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f z
ga : HolomorphicAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) g z
⊢ (∀ᶠ (w : S) in 𝓝 z, f w = g w) ∨ ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
Tactic:
simp only [holomorphicAt_iff, Function.comp] at fa ga
Proof state after:
X : Type
inst✝⁷ : TopologicalSpace X
S : Type
inst✝⁶ : TopologicalSpace S
inst✝⁵ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝⁴ : TopologicalSpace T
inst✝³ : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝² : TopologicalSpace U
inst✝¹ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
inst✝ : T2Space T
f g : S → T
z : S
fa :
  ContinuousAt f z ∧
    AnalyticAt ℂ (fun x => ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm x)))
      (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z)
ga :
  ContinuousAt g z ∧
    AnalyticAt ℂ (fun x => ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm x)))
      (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ (∀ᶠ (w : S) in 𝓝 z, f w = g w) ∨ ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
X : Type
inst✝⁷ : TopologicalSpace X
S : Type
inst✝⁶ : TopologicalSpace S
inst✝⁵ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝⁴ : TopologicalSpace T
inst✝³ : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝² : TopologicalSpace U
inst✝¹ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s : Set ℂ
inst✝ : T2Space T
f g : S → T
z : S
fa :
  ContinuousAt f z ∧
    AnalyticAt ℂ (fun x => ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm x)))
      (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z)
ga :
  ContinuousAt g z ∧
    AnalyticAt ℂ (fun x => ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm x)))
      (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ (∀ᶠ (w : S) in 𝓝 z, f w = g w) ∨ ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
Tactic:
rcases fa with ⟨fc, fa⟩
Proof state after:
case 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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
ga :
  ContinuousAt g z ∧
    AnalyticAt ℂ (fun x => ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm x)))
      (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z)
fc : ContinuousAt f z
fa :
  AnalyticAt ℂ (fun x => ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm x)))
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ (∀ᶠ (w : S) in 𝓝 z, f w = g w) ∨ ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case 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 ℂ
inst✝ : T2Space T
f g : S → T
z : S
ga :
  ContinuousAt g z ∧
    AnalyticAt ℂ (fun x => ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (g z)) (g (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm x)))
      (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z)
fc : ContinuousAt f z
fa :
  AnalyticAt ℂ (fun x => ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (f (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z).symm x)))
    (↑(_root_.extChartAt 𝓘(ℂ, ℂ) z) z)
⊢ (∀ᶠ (w : S) in 𝓝 z, f w = g w) ∨ ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
Tactic:
rcases ga with ⟨gc, ga⟩
Proof state after:
case 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 ℂ
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)
⊢ (∀ᶠ (w : S) in 𝓝 z, f w = g w) ∨ ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case 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 ℂ
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)
⊢ (∀ᶠ (w : S) in 𝓝 z, f w = g w) ∨ ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
Tactic:
by_cases fg : f z ≠ g z
Proof state after:
case pos
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
⊢ (∀ᶠ (w : S) in 𝓝 z, f w = g w) ∨ ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w

case neg
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
⊢ (∀ᶠ (w : S) in 𝓝 z, f w = g w) ∨ ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg
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
⊢ (∀ᶠ (w : S) in 𝓝 z, f w = g w) ∨ ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
Tactic:
simp only [not_not] at fg
Proof state after:
case neg
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
⊢ (∀ᶠ (w : S) in 𝓝 z, f w = g w) ∨ ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case neg
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
⊢ (∀ᶠ (w : S) in 𝓝 z, f w = g w) ∨ ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
Tactic:
cases' fa.eventually_eq_or_eventually_ne ga with e e
Proof state after:
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

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
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case pos
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
⊢ (∀ᶠ (w : S) in 𝓝 z, f w = g w) ∨ ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
Tactic:
right
Proof state after:
case pos.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
⊢ ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case pos.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
⊢ ∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
Tactic:
contrapose fg
Proof state after:
case pos.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 : ¬∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
⊢ ¬f z ≠ g z
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case pos.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 : ¬∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
⊢ ¬f z ≠ g z
Tactic:
simp only [not_not]
Proof state after:
case pos.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 : ¬∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
⊢ f z = g z
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case pos.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 : ¬∀ᶠ (w : S) in 𝓝[≠] z, f w ≠ g w
⊢ f z = g z
Tactic:
simp only [Filter.not_eventually, not_not] at fg
Proof state after:
case pos.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 : ∃ᶠ (x : S) in 𝓝[≠] z, f x = g x
⊢ f z = g z
Theorem: HolomorphicAt.eventually_eq_or_eventually_ne
Proof state before:
case pos.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 : ∃ᶠ (x : S) in 𝓝[≠] z, f x = g x
⊢ f z = g z
Tactic:
exact tendsto_nhds_unique_of_frequently_eq fc gc (fg.filter_mono nhdsWithin_le_nhds)
Proof state after:
no goals