Theorem: RiemannSphere.holomorphicAt_fill_inf (Ray/AnalyticManifold/RiemannSphere.lean)

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ HolomorphicAt I I (fill f y) ∞
Tactic:
rw [holomorphicAt_iff]
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ContinuousAt (fill f y) ∞ ∧
    AnalyticAt ℂ (↑(extChartAt I (fill f y ∞)) ∘ fill f y ∘ ↑(extChartAt I ∞).symm) (↑(extChartAt I ∞) ∞)

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ContinuousAt (fill f y) ∞ ∧
    AnalyticAt ℂ (↑(extChartAt I (fill f y ∞)) ∘ fill f y ∘ ↑(extChartAt I ∞).symm) (↑(extChartAt I ∞) ∞)
Tactic:
use continuousAt_fill_inf fi
State after:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ AnalyticAt ℂ (↑(extChartAt I (fill f y ∞)) ∘ fill f y ∘ ↑(extChartAt I ∞).symm) (↑(extChartAt I ∞) ∞)

State before:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ AnalyticAt ℂ (↑(extChartAt I (fill f y ∞)) ∘ fill f y ∘ ↑(extChartAt I ∞).symm) (↑(extChartAt I ∞) ∞)
Tactic:
simp only [Function.comp, extChartAt, PartialHomeomorph.extend, fill, rec_inf,
  modelWithCornersSelf_partialEquiv, PartialEquiv.trans_refl, chartAt_inf,
  PartialHomeomorph.symm_toPartialEquiv, PartialEquiv.symm_symm, PartialHomeomorph.toFun_eq_coe,
  invCoePartialHomeomorph_apply, PartialHomeomorph.coe_coe_symm, invCoePartialHomeomorph_symm_apply,
  inv_inf, toComplex_zero]
State after:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ AnalyticAt ℂ (fun x => ↑(chartAt ℂ y) (OnePoint.rec y f (↑x)⁻¹)) 0

State before:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
e : (fun z => ↑(chartAt ℂ y) (OnePoint.rec y f (↑z)⁻¹)) = fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)
⊢ AnalyticAt ℂ (fun x => ↑(chartAt ℂ y) (OnePoint.rec y f (↑x)⁻¹)) 0
Tactic:
rw [e]
State after:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
e : (fun z => ↑(chartAt ℂ y) (OnePoint.rec y f (↑z)⁻¹)) = fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)
⊢ AnalyticAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) 0

State before:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
e : (fun z => ↑(chartAt ℂ y) (OnePoint.rec y f (↑z)⁻¹)) = fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)
⊢ AnalyticAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) 0
Tactic:
clear e
State after:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ AnalyticAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) 0

State before:
case right
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ AnalyticAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) 0
Tactic:
apply Complex.analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt
State after:
case right.hd
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) z

case right.hc
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ContinuousAt (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) 0

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ (fun z => ↑(chartAt ℂ y) (OnePoint.rec y f (↑z)⁻¹)) = fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)
Tactic:
funext z
State after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
⊢ ↑(chartAt ℂ y) (OnePoint.rec y f (↑z)⁻¹) = ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)

State before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
⊢ ↑(chartAt ℂ y) (OnePoint.rec y f (↑z)⁻¹) = ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)
Tactic:
by_cases z0 : z = 0
State after:
case pos
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
z0 : z = 0
⊢ ↑(chartAt ℂ y) (OnePoint.rec y f (↑z)⁻¹) = ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)

case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
z0 : ¬z = 0
⊢ ↑(chartAt ℂ y) (OnePoint.rec y f (↑z)⁻¹) = ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)

State before:
case pos
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
z0 : z = 0
⊢ ↑(chartAt ℂ y) (OnePoint.rec y f (↑z)⁻¹) = ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)
Tactic:
simp only [if_pos z0, z0, coe_zero, inv_zero', rec_inf, extChartAt, PartialHomeomorph.extend,
  modelWithCornersSelf_partialEquiv, PartialEquiv.trans_refl, PartialHomeomorph.toFun_eq_coe,
  if_true]
State after:
no goals

State before:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
z0 : ¬z = 0
⊢ ↑(chartAt ℂ y) (OnePoint.rec y f (↑z)⁻¹) = ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)
Tactic:
simp only [inv_coe z0, rec_coe, extChartAt, PartialHomeomorph.extend,
  modelWithCornersSelf_partialEquiv, PartialEquiv.trans_refl, z0, ite_false,
  PartialHomeomorph.toFun_eq_coe]
State after:
no goals

State before:
case right.hd
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) z
Tactic:
apply (inv_tendsto_atInf.eventually fa).mp
State after:
case right.hd
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ᶠ (x : ℂ) in 𝓝[≠] 0,
    HolomorphicAt I I f x⁻¹ → DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) x

State before:
case right.hd
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ᶠ (x : ℂ) in 𝓝[≠] 0,
    HolomorphicAt I I f x⁻¹ → DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) x
Tactic:
apply (inv_tendsto_atInf.eventually (fi.eventually
  ((isOpen_extChartAt_source I y).eventually_mem (mem_extChartAt_source I y)))).mp
State after:
case right.hd
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ᶠ (x : ℂ) in 𝓝[≠] 0,
    f x⁻¹ ∈ (extChartAt I y).source →
      HolomorphicAt I I f x⁻¹ → DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) x

State before:
case right.hd
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ᶠ (x : ℂ) in 𝓝[≠] 0,
    f x⁻¹ ∈ (extChartAt I y).source →
      HolomorphicAt I I f x⁻¹ → DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) x
Tactic:
apply eventually_nhdsWithin_of_forall
State after:
case right.hd.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ x ∈ {0}ᶜ,
    f x⁻¹ ∈ (extChartAt I y).source →
      HolomorphicAt I I f x⁻¹ → DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) x

State before:
case right.hd.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ x ∈ {0}ᶜ,
    f x⁻¹ ∈ (extChartAt I y).source →
      HolomorphicAt I I f x⁻¹ → DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) x
Tactic:
intro z z0 m fa
State after:
case right.hd.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
z0 : z ∈ {0}ᶜ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
⊢ DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) z

State before:
case right.hd.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
z0 : z ∈ {0}ᶜ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
⊢ DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) z
Tactic:
simp only [Set.mem_compl_iff, Set.mem_singleton_iff] at z0
State after:
case right.hd.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
⊢ DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) z

State before:
case right.hd.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
⊢ DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) z
Tactic:
have e : (fun z ↦ extChartAt I y (if z = 0 then y else f z⁻¹)) =ᶠ[𝓝 z]
    fun z ↦ extChartAt I y (f z⁻¹) := by
  refine (continuousAt_id.eventually_ne z0).mp (eventually_of_forall fun w w0 ↦ ?_)
  simp only [Ne, id_eq] at w0; simp only [w0, if_false]
State after:
case right.hd.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) z

State before:
case right.hd.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) z
Tactic:
refine DifferentiableAt.congr_of_eventuallyEq ?_ e
State after:
case right.hd.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (f z⁻¹)) z

State before:
case right.hd.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (f z⁻¹)) z
Tactic:
apply AnalyticAt.differentiableAt
State after:
case right.hd.h.a
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ AnalyticAt ℂ (fun z => ↑(extChartAt I y) (f z⁻¹)) z

State before:
case right.hd.h.a
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ AnalyticAt ℂ (fun z => ↑(extChartAt I y) (f z⁻¹)) z
Tactic:
apply HolomorphicAt.analyticAt I I
State after:
case right.hd.h.a
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ HolomorphicAt I I (fun z => ↑(extChartAt I y) (f z⁻¹)) z

State before:
case right.hd.h.a
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ HolomorphicAt I I (fun z => ↑(extChartAt I y) (f z⁻¹)) z
Tactic:
refine (HolomorphicAt.extChartAt ?_).comp ?_
State after:
case right.hd.h.a.refine_1
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ f z⁻¹ ∈ (extChartAt I y).source

case right.hd.h.a.refine_2
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ HolomorphicAt I I (fun z => f z⁻¹) z

State before:
case right.hd.h.a.refine_1
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ f z⁻¹ ∈ (extChartAt I y).source

case right.hd.h.a.refine_2
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ HolomorphicAt I I (fun z => f z⁻¹) z
Tactic:
exact m
State after:
case right.hd.h.a.refine_2
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ HolomorphicAt I I (fun z => f z⁻¹) z

State before:
case right.hd.h.a.refine_2
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ HolomorphicAt I I (fun z => f z⁻¹) z
Tactic:
exact fa.comp (holomorphicAt_id.inv z0)
State after:
no goals

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
⊢ (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
Tactic:
refine (continuousAt_id.eventually_ne z0).mp (eventually_of_forall fun w w0 ↦ ?_)
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
w : ℂ
w0 : id w ≠ 0
⊢ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) w = (fun z => ↑(extChartAt I y) (f z⁻¹)) w

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
w : ℂ
w0 : id w ≠ 0
⊢ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) w = (fun z => ↑(extChartAt I y) (f z⁻¹)) w
Tactic:
simp only [Ne, id_eq] at w0
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
w : ℂ
w0 : ¬w = 0
⊢ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) w = (fun z => ↑(extChartAt I y) (f z⁻¹)) w

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
w : ℂ
w0 : ¬w = 0
⊢ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) w = (fun z => ↑(extChartAt I y) (f z⁻¹)) w
Tactic:
simp only [w0, if_false]
State after:
no goals

State before:
case right.hc
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ContinuousAt (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) 0
Tactic:
refine (continuousAt_extChartAt' I ?_).comp ?_
State after:
case right.hc.refine_1
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ (if 0 = 0 then y else f 0⁻¹) ∈ (extChartAt I y).source

case right.hc.refine_2
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ContinuousAt (fun z => if z = 0 then y else f z⁻¹) 0

State before:
case right.hc.refine_1
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ (if 0 = 0 then y else f 0⁻¹) ∈ (extChartAt I y).source
Tactic:
simp only [eq_self_iff_true, if_pos, mem_extChartAt_source]
State after:
no goals

State before:
case right.hc.refine_2
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ContinuousAt (fun z => if z = 0 then y else f z⁻¹) 0
Tactic:
simp only [← continuousWithinAt_compl_self, ContinuousWithinAt]
State after:
case right.hc.refine_2
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ Tendsto (fun z => if z = 0 then y else f z⁻¹) (𝓝[≠] 0) (𝓝 (if True then y else f 0⁻¹))

State before:
case right.hc.refine_2
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ Tendsto (fun z => if z = 0 then y else f z⁻¹) (𝓝[≠] 0) (𝓝 (if True then y else f 0⁻¹))
Tactic:
apply tendsto_nhdsWithin_congr (f := fun z ↦ f z⁻¹)
State after:
case right.hc.refine_2.hfg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ x ∈ {0}ᶜ, f x⁻¹ = if x = 0 then y else f x⁻¹

case right.hc.refine_2.hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ Tendsto (fun z => f z⁻¹) (𝓝[≠] 0) (𝓝 (if True then y else f 0⁻¹))

State before:
case right.hc.refine_2.hfg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ x ∈ {0}ᶜ, f x⁻¹ = if x = 0 then y else f x⁻¹

case right.hc.refine_2.hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ Tendsto (fun z => f z⁻¹) (𝓝[≠] 0) (𝓝 (if True then y else f 0⁻¹))
Tactic:
intro z z0
State after:
case right.hc.refine_2.hfg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
z0 : z ∈ {0}ᶜ
⊢ f z⁻¹ = if z = 0 then y else f z⁻¹

case right.hc.refine_2.hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ Tendsto (fun z => f z⁻¹) (𝓝[≠] 0) (𝓝 (if True then y else f 0⁻¹))

State before:
case right.hc.refine_2.hfg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
z0 : z ∈ {0}ᶜ
⊢ f z⁻¹ = if z = 0 then y else f z⁻¹

case right.hc.refine_2.hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ Tendsto (fun z => f z⁻¹) (𝓝[≠] 0) (𝓝 (if True then y else f 0⁻¹))
Tactic:
simp only [Set.mem_compl_iff, Set.mem_singleton_iff] at z0
State after:
case right.hc.refine_2.hfg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
z0 : ¬z = 0
⊢ f z⁻¹ = if z = 0 then y else f z⁻¹

case right.hc.refine_2.hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ Tendsto (fun z => f z⁻¹) (𝓝[≠] 0) (𝓝 (if True then y else f 0⁻¹))

State before:
case right.hc.refine_2.hfg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
z0 : ¬z = 0
⊢ f z⁻¹ = if z = 0 then y else f z⁻¹

case right.hc.refine_2.hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ Tendsto (fun z => f z⁻¹) (𝓝[≠] 0) (𝓝 (if True then y else f 0⁻¹))
Tactic:
simp only [z0, if_false]
State after:
case right.hc.refine_2.hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ Tendsto (fun z => f z⁻¹) (𝓝[≠] 0) (𝓝 (if True then y else f 0⁻¹))

State before:
case right.hc.refine_2.hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ Tendsto (fun z => f z⁻¹) (𝓝[≠] 0) (𝓝 (if True then y else f 0⁻¹))
Tactic:
exact Filter.Tendsto.comp fi inv_tendsto_atInf
State after:
no goals