Theorem: HolomorphicAt.eventually_eq_or_eventually_ne (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 ℂ
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
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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
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
Tactic:
specialize h ((PartialEquiv.injOn _).ne xm (mem_extChartAt_source _ _) xz)
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 𝓘(ℂ, ℂ) (f z)) (f x) ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (g x)
⊢ f x ≠ g x

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
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 𝓘(ℂ, ℂ) (f z)) (f x) ≠ ↑(_root_.extChartAt 𝓘(ℂ, ℂ) (f z)) (g x)
⊢ f x ≠ g x
Tactic:
rwa [← (PartialEquiv.injOn _).ne_iff fm gm]
State after:
no goals