Theorem: RiemannSphere.holomorphic_inv (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
⊢ Holomorphic I I fun z => z⁻¹
Tactic:
rw [holomorphic_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
⊢ (Continuous fun z => z⁻¹) ∧
    ∀ (x : 𝕊), AnalyticAt ℂ (↑(extChartAt I x⁻¹) ∘ (fun z => z⁻¹) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
⊢ (Continuous fun z => z⁻¹) ∧
    ∀ (x : 𝕊), AnalyticAt ℂ (↑(extChartAt I x⁻¹) ∘ (fun z => z⁻¹) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)
Tactic:
use continuous_inv
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
⊢ ∀ (x : 𝕊), AnalyticAt ℂ (↑(extChartAt I x⁻¹) ∘ (fun z => z⁻¹) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)

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
⊢ ∀ (x : 𝕊), AnalyticAt ℂ (↑(extChartAt I x⁻¹) ∘ (fun z => z⁻¹) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x)
Tactic:
intro z
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
z : 𝕊
⊢ AnalyticAt ℂ (↑(extChartAt I z⁻¹) ∘ (fun z => z⁻¹) ∘ ↑(extChartAt I z).symm) (↑(extChartAt I z) z)

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
z : 𝕊
⊢ AnalyticAt ℂ (↑(extChartAt I z⁻¹) ∘ (fun z => z⁻¹) ∘ ↑(extChartAt I z).symm) (↑(extChartAt I z) z)
Tactic:
induction' z using OnePoint.rec with z
State after:
case right.h₁
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
⊢ AnalyticAt ℂ (↑(extChartAt I ∞⁻¹) ∘ (fun z => z⁻¹) ∘ ↑(extChartAt I ∞).symm) (↑(extChartAt I ∞) ∞)

case right.h₂
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (↑(extChartAt I (↑z)⁻¹) ∘ (fun z => z⁻¹) ∘ ↑(extChartAt I ↑z).symm) (↑(extChartAt I ↑z) ↑z)

State before:
case right.h₁
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
⊢ AnalyticAt ℂ (↑(extChartAt I ∞⁻¹) ∘ (fun z => z⁻¹) ∘ ↑(extChartAt I ∞).symm) (↑(extChartAt I ∞) ∞)
Tactic:
simp only [inv_inf, extChartAt_inf, ← coe_zero, extChartAt_coe, Function.comp,
  PartialEquiv.trans_apply, Equiv.toPartialEquiv_apply, invEquiv_apply, coePartialEquiv_symm_apply,
  toComplex_coe, PartialEquiv.coe_trans_symm, PartialEquiv.symm_symm, coePartialEquiv_apply,
  Equiv.toPartialEquiv_symm_apply, invEquiv_symm, inv_inv]
State after:
case right.h₁
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
⊢ AnalyticAt ℂ (fun x => x) 0

State before:
case right.h₁
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
⊢ AnalyticAt ℂ (fun x => x) 0
Tactic:
apply analyticAt_id
State after:
no goals

State before:
case right.h₂
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (↑(extChartAt I (↑z)⁻¹) ∘ (fun z => z⁻¹) ∘ ↑(extChartAt I ↑z).symm) (↑(extChartAt I ↑z) ↑z)
Tactic:
simp only [extChartAt_coe, PartialEquiv.symm_symm, Function.comp, coePartialEquiv_apply,
  coePartialEquiv_symm_apply, toComplex_coe]
State after:
case right.h₂
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (fun x => ↑(extChartAt I (↑z)⁻¹) (↑x)⁻¹) z

State before:
case right.h₂
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (fun x => ↑(extChartAt I (↑z)⁻¹) (↑x)⁻¹) 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
z : ℂ
z0 : z = 0
⊢ AnalyticAt ℂ (fun x => ↑(extChartAt I (↑z)⁻¹) (↑x)⁻¹) 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
z : ℂ
z0 : ¬z = 0
⊢ AnalyticAt ℂ (fun x => ↑(extChartAt I (↑z)⁻¹) (↑x)⁻¹) 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
z : ℂ
z0 : z = 0
⊢ AnalyticAt ℂ (fun x => ↑(extChartAt I (↑z)⁻¹) (↑x)⁻¹) z
Tactic:
simp only [z0, coe_zero, extChartAt_inf, PartialEquiv.trans_apply, coePartialEquiv_symm_apply,
  invEquiv_apply, Equiv.toPartialEquiv_apply, inv_zero', inv_inv, toComplex_coe]
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
z : ℂ
z0 : z = 0
⊢ AnalyticAt ℂ (fun x => x) 0

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
z : ℂ
z0 : z = 0
⊢ AnalyticAt ℂ (fun x => x) 0
Tactic:
apply analyticAt_id
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
z : ℂ
z0 : ¬z = 0
⊢ AnalyticAt ℂ (fun x => ↑(extChartAt I (↑z)⁻¹) (↑x)⁻¹) z
Tactic:
simp only [inv_coe z0, extChartAt_coe, coePartialEquiv_symm_apply]
State after:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
z0 : ¬z = 0
⊢ AnalyticAt ℂ (fun x => (↑x)⁻¹.toComplex) z

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
z : ℂ
z0 : ¬z = 0
⊢ AnalyticAt ℂ (fun x => (↑x)⁻¹.toComplex) z
Tactic:
refine ((analyticAt_id _ _).inv z0).congr ?_
State after:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
z0 : ¬z = 0
⊢ (𝓝 z).EventuallyEq (fun x => (id x)⁻¹) fun x => (↑x)⁻¹.toComplex

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
z : ℂ
z0 : ¬z = 0
⊢ (𝓝 z).EventuallyEq (fun x => (id x)⁻¹) fun x => (↑x)⁻¹.toComplex
Tactic:
refine (continuousAt_id.eventually_ne z0).mp (eventually_of_forall fun w w0 ↦ ?_)
State after:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
z0 : ¬z = 0
w : ℂ
w0 : id w ≠ 0
⊢ (fun x => (id x)⁻¹) w = (fun x => (↑x)⁻¹.toComplex) w

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
z : ℂ
z0 : ¬z = 0
w : ℂ
w0 : id w ≠ 0
⊢ (fun x => (id x)⁻¹) w = (fun x => (↑x)⁻¹.toComplex) w
Tactic:
rw [id] at w0
State after:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
z0 : ¬z = 0
w : ℂ
w0 : w ≠ 0
⊢ (fun x => (id x)⁻¹) w = (fun x => (↑x)⁻¹.toComplex) w

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
z : ℂ
z0 : ¬z = 0
w : ℂ
w0 : w ≠ 0
⊢ (fun x => (id x)⁻¹) w = (fun x => (↑x)⁻¹.toComplex) w
Tactic:
simp only [inv_coe w0, toComplex_coe, id]
State after:
no goals