internlm/Lean-Github huggingface dataset:
Theorem: RiemannSphere.continuous_lift'
Proof 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✝ : ℂ
gc : Continuous (uncurry g)
gi : ∀ (x : X), Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
x : X
z : 𝕊
a✝ : (x, z) ∈ univ
⊢ ContinuousAt (uncurry (lift' g ∞)) (x, z)
Tactic:
induction z using OnePoint.rec
Proof state after:
case h.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 : ℂ
gc : Continuous (uncurry g)
gi : ∀ (x : X), Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
x : X
a✝ : (x, ∞) ∈ univ
⊢ ContinuousAt (uncurry (lift' g ∞)) (x, ∞)

case h.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 : ℂ
gc : Continuous (uncurry g)
gi : ∀ (x : X), Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
x : X
x✝ : ℂ
a✝ : (x, ↑x✝) ∈ univ
⊢ ContinuousAt (uncurry (lift' g ∞)) (x, ↑x✝)
Theorem: RiemannSphere.continuous_lift'
Proof state before:
case h.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 : ℂ
gc : Continuous (uncurry g)
gi : ∀ (x : X), Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
x : X
a✝ : (x, ∞) ∈ univ
⊢ ContinuousAt (uncurry (lift' g ∞)) (x, ∞)
Tactic:
exact continuousAt_lift_inf' (gi x)
Proof state after:
no goals
Theorem: RiemannSphere.continuous_lift'
Proof state before:
case h.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 : ℂ
gc : Continuous (uncurry g)
gi : ∀ (x : X), Tendsto (uncurry g) ((𝓝 x).prod atInf) atInf
x : X
x✝ : ℂ
a✝ : (x, ↑x✝) ∈ univ
⊢ ContinuousAt (uncurry (lift' g ∞)) (x, ↑x✝)
Tactic:
exact continuousAt_lift_coe' gc.continuousAt
Proof state after:
no goals
Theorem: RiemannSphere.continuousAt_lift_coe
Proof 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 : ℂ
fc : ContinuousAt f z
⊢ ContinuousAt (uncurry fun x => f) ((), z)
Tactic:
refine ContinuousAt.comp fc ?_
Proof 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 : ℂ
fc : ContinuousAt f z
⊢ ContinuousAt (fun a => a.2) ((), z)
Theorem: RiemannSphere.continuousAt_lift_coe
Proof 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 : ℂ
fc : ContinuousAt f z
⊢ ContinuousAt (fun a => a.2) ((), z)
Tactic:
exact continuousAt_snd
Proof state after:
no goals
Theorem: RiemannSphere.continuous_lift
Proof 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 : ℂ
fc : Continuous f
fi : Tendsto f atInf atInf
⊢ Continuous (lift f ∞)
Tactic:
rw [continuous_iff_continuousAt]
Proof 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 : ℂ
fc : Continuous f
fi : Tendsto f atInf atInf
⊢ ∀ (x : 𝕊), ContinuousAt (lift f ∞) x
Theorem: RiemannSphere.continuous_lift
Proof 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 : ℂ
fc : Continuous f
fi : Tendsto f atInf atInf
⊢ ∀ (x : 𝕊), ContinuousAt (lift f ∞) x
Tactic:
intro z
Proof 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✝ : ℂ
fc : Continuous f
fi : Tendsto f atInf atInf
z : 𝕊
⊢ ContinuousAt (lift f ∞) z
Theorem: RiemannSphere.continuous_lift
Proof 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✝ : ℂ
fc : Continuous f
fi : Tendsto f atInf atInf
z : 𝕊
⊢ ContinuousAt (lift f ∞) z
Tactic:
induction z using OnePoint.rec
Proof 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 : ℂ
fc : Continuous f
fi : Tendsto f atInf atInf
⊢ ContinuousAt (lift f ∞) ∞

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 : ℂ
fc : Continuous f
fi : Tendsto f atInf atInf
x✝ : ℂ
⊢ ContinuousAt (lift f ∞) ↑x✝
Theorem: RiemannSphere.continuous_lift
Proof 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 : ℂ
fc : Continuous f
fi : Tendsto f atInf atInf
⊢ ContinuousAt (lift f ∞) ∞
Tactic:
exact continuousAt_lift_inf fi
Proof state after:
no goals
Theorem: RiemannSphere.continuous_lift
Proof 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 : ℂ
fc : Continuous f
fi : Tendsto f atInf atInf
x✝ : ℂ
⊢ ContinuousAt (lift f ∞) ↑x✝
Tactic:
exact continuousAt_lift_coe fc.continuousAt
Proof state after:
no goals
Theorem: RiemannSphere.holomorphicAt_lift_coe
Proof 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 : ℂ
fa : AnalyticAt ℂ f z
⊢ HolomorphicAt I I (lift f y) ↑z
Tactic:
rw [lift_eq_fill]
Proof 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 : ℂ
fa : AnalyticAt ℂ f z
⊢ HolomorphicAt I I (fill (fun z => ↑(f z)) y) ↑z
Theorem: RiemannSphere.holomorphicAt_lift_coe
Proof 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 : ℂ
fa : AnalyticAt ℂ f z
⊢ HolomorphicAt I I (fill (fun z => ↑(f z)) y) ↑z
Tactic:
exact holomorphicAt_fill_coe ((holomorphic_coe _).comp (fa.holomorphicAt I I))
Proof state after:
no goals
Theorem: RiemannSphere.holomorphicAt_lift_inf
Proof 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 : ℂ
fa : ∀ᶠ (z : ℂ) in atInf, AnalyticAt ℂ f z
fi : Tendsto f atInf atInf
⊢ HolomorphicAt I I (lift f ∞) ∞
Tactic:
rw [lift_eq_fill]
Proof 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 : ℂ
fa : ∀ᶠ (z : ℂ) in atInf, AnalyticAt ℂ f z
fi : Tendsto f atInf atInf
⊢ HolomorphicAt I I (fill (fun z => ↑(f z)) ∞) ∞
Theorem: RiemannSphere.holomorphicAt_lift_inf
Proof 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 : ℂ
fa : ∀ᶠ (z : ℂ) in atInf, AnalyticAt ℂ f z
fi : Tendsto f atInf atInf
⊢ HolomorphicAt I I (fill (fun z => ↑(f z)) ∞) ∞
Tactic:
apply holomorphicAt_fill_inf
Proof state after:
case fa
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 : ℂ
fa : ∀ᶠ (z : ℂ) in atInf, AnalyticAt ℂ f z
fi : Tendsto f atInf atInf
⊢ ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I (fun z => ↑(f z)) z

case fi
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 : ℂ
fa : ∀ᶠ (z : ℂ) in atInf, AnalyticAt ℂ f z
fi : Tendsto f atInf atInf
⊢ Tendsto (fun z => ↑(f z)) atInf (𝓝 ∞)
Theorem: RiemannSphere.holomorphicAt_lift_inf
Proof state before:
case fa
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 : ℂ
fa : ∀ᶠ (z : ℂ) in atInf, AnalyticAt ℂ f z
fi : Tendsto f atInf atInf
⊢ ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I (fun z => ↑(f z)) z

case fi
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 : ℂ
fa : ∀ᶠ (z : ℂ) in atInf, AnalyticAt ℂ f z
fi : Tendsto f atInf atInf
⊢ Tendsto (fun z => ↑(f z)) atInf (𝓝 ∞)
Tactic:
exact fa.mp (eventually_of_forall fun z fa ↦ (holomorphic_coe _).comp (fa.holomorphicAt I I))
Proof state after:
case fi
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 : ℂ
fa : ∀ᶠ (z : ℂ) in atInf, AnalyticAt ℂ f z
fi : Tendsto f atInf atInf
⊢ Tendsto (fun z => ↑(f z)) atInf (𝓝 ∞)
Theorem: RiemannSphere.holomorphicAt_lift_inf
Proof state before:
case fi
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 : ℂ
fa : ∀ᶠ (z : ℂ) in atInf, AnalyticAt ℂ f z
fi : Tendsto f atInf atInf
⊢ Tendsto (fun z => ↑(f z)) atInf (𝓝 ∞)
Tactic:
exact coe_tendsto_inf.comp fi
Proof state after:
no goals
Theorem: RiemannSphere.holomorphic_lift
Proof 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 : ℂ
fa : AnalyticOn ℂ f univ
fi : Tendsto f atInf atInf
⊢ Holomorphic I I (lift f ∞)
Tactic:
intro z
Proof 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✝ : ℂ
fa : AnalyticOn ℂ f univ
fi : Tendsto f atInf atInf
z : 𝕊
⊢ HolomorphicAt I I (lift f ∞) z
Theorem: RiemannSphere.holomorphic_lift
Proof 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✝ : ℂ
fa : AnalyticOn ℂ f univ
fi : Tendsto f atInf atInf
z : 𝕊
⊢ HolomorphicAt I I (lift f ∞) z
Tactic:
induction z using OnePoint.rec
Proof 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 : ℂ
fa : AnalyticOn ℂ f univ
fi : Tendsto f atInf atInf
⊢ HolomorphicAt I I (lift f ∞) ∞

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 : ℂ
fa : AnalyticOn ℂ f univ
fi : Tendsto f atInf atInf
x✝ : ℂ
⊢ HolomorphicAt I I (lift f ∞) ↑x✝
Theorem: RiemannSphere.holomorphic_lift
Proof 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 : ℂ
fa : AnalyticOn ℂ f univ
fi : Tendsto f atInf atInf
⊢ HolomorphicAt I I (lift f ∞) ∞
Tactic:
exact holomorphicAt_lift_inf (eventually_of_forall fun z ↦ fa z (mem_univ _)) fi
Proof state after:
no goals
Theorem: RiemannSphere.holomorphic_lift
Proof 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 : ℂ
fa : AnalyticOn ℂ f univ
fi : Tendsto f atInf atInf
x✝ : ℂ
⊢ HolomorphicAt I I (lift f ∞) ↑x✝
Tactic:
exact holomorphicAt_lift_coe (fa _ (mem_univ _))
Proof state after:
no goals
Theorem: RiemannSphere.holomorphicLift'
Proof 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 : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
⊢ Holomorphic (I.prod I) I (uncurry (lift' f ∞))
Tactic:
apply osgoodManifold (continuous_lift' fa.continuous fi)
Proof state after:
case f0
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 : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
⊢ ∀ (x : ℂ) (y : 𝕊), HolomorphicAt I I (fun x => uncurry (lift' f ∞) (x, y)) x

case f1
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 : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
⊢ ∀ (x : ℂ) (y : 𝕊), HolomorphicAt I I (fun y => uncurry (lift' f ∞) (x, y)) y
Theorem: RiemannSphere.holomorphicLift'
Proof state before:
case f0
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 : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
⊢ ∀ (x : ℂ) (y : 𝕊), HolomorphicAt I I (fun x => uncurry (lift' f ∞) (x, y)) x
Tactic:
intro x z
Proof state after:
case f0
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 : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
x : ℂ
z : 𝕊
⊢ HolomorphicAt I I (fun x => uncurry (lift' f ∞) (x, z)) x
Theorem: RiemannSphere.holomorphicLift'
Proof state before:
case f0
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 : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
x : ℂ
z : 𝕊
⊢ HolomorphicAt I I (fun x => uncurry (lift' f ∞) (x, z)) x
Tactic:
induction z using OnePoint.rec
Proof state after:
case f0.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 : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
x : ℂ
⊢ HolomorphicAt I I (fun x => uncurry (lift' f ∞) (x, ∞)) x

case f0.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 : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
x x✝ : ℂ
⊢ HolomorphicAt I I (fun x => uncurry (lift' f ∞) (x, ↑x✝)) x
Theorem: RiemannSphere.holomorphicLift'
Proof state before:
case f0.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 : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
x : ℂ
⊢ HolomorphicAt I I (fun x => uncurry (lift' f ∞) (x, ∞)) x
Tactic:
simp only [uncurry, lift_inf']
Proof state after:
case f0.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 : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
x : ℂ
⊢ HolomorphicAt I I (fun x => ∞) x
Theorem: RiemannSphere.holomorphicLift'
Proof state before:
case f0.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 : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
x : ℂ
⊢ HolomorphicAt I I (fun x => ∞) x
Tactic:
exact holomorphicAt_const
Proof state after:
no goals
Theorem: RiemannSphere.holomorphicLift'
Proof state before:
case f0.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 : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
x x✝ : ℂ
⊢ HolomorphicAt I I (fun x => uncurry (lift' f ∞) (x, ↑x✝)) x
Tactic:
exact (holomorphic_coe _).comp ((fa _ (mem_univ ⟨_,_⟩)).along_fst.holomorphicAt _ _)
Proof state after:
no goals
Theorem: RiemannSphere.holomorphicLift'
Proof state before:
case f1
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 : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
⊢ ∀ (x : ℂ) (y : 𝕊), HolomorphicAt I I (fun y => uncurry (lift' f ∞) (x, y)) y
Tactic:
intro x z
Proof state after:
case f1
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 : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
x : ℂ
z : 𝕊
⊢ HolomorphicAt I I (fun y => uncurry (lift' f ∞) (x, y)) z
Theorem: RiemannSphere.holomorphicLift'
Proof state before:
case f1
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 : ℂ → ℂ → ℂ
fa : AnalyticOn ℂ (uncurry f) univ
fi : ∀ (x : ℂ), Tendsto (uncurry f) ((𝓝 x).prod atInf) atInf
x : ℂ
z : 𝕊
⊢ HolomorphicAt I I (fun y => uncurry (lift' f ∞) (x, y)) z
Tactic:
exact holomorphic_lift (fun _ _ ↦ (fa _ (mem_univ ⟨_,_⟩)).along_snd)
  ((fi x).comp (tendsto_const_nhds.prod_mk Filter.tendsto_id)) z
Proof state after:
no goals
Theorem: Interval.mem_approx_iter_sqrt
Proof state before:
a : ℝ
x : Interval
n : ℕ
ax : a ∈ approx x
⊢ a ^ 2 ^ (-↑n) ∈ approx (x.iter_sqrt n)
Tactic:
rw [iter_sqrt]
Proof state after:
a : ℝ
x : Interval
n : ℕ
ax : a ∈ approx x
⊢ a ^ 2 ^ (-↑n) ∈ approx (x.log.scaleB' (-Fixed.ofNat0 n)).exp
Theorem: Interval.mem_approx_iter_sqrt
Proof state before:
a : ℝ
x : Interval
n : ℕ
ax : a ∈ approx x
⊢ a ^ 2 ^ (-↑n) ∈ approx (x.log.scaleB' (-Fixed.ofNat0 n)).exp
Tactic:
by_cases a0 : a ≤ 0
Proof state after:
case pos
a : ℝ
x : Interval
n : ℕ
ax : a ∈ approx x
a0 : a ≤ 0
⊢ a ^ 2 ^ (-↑n) ∈ approx (x.log.scaleB' (-Fixed.ofNat0 n)).exp

case neg
a : ℝ
x : Interval
n : ℕ
ax : a ∈ approx x
a0 : ¬a ≤ 0
⊢ a ^ 2 ^ (-↑n) ∈ approx (x.log.scaleB' (-Fixed.ofNat0 n)).exp
Theorem: Interval.mem_approx_iter_sqrt
Proof state before:
case pos
a : ℝ
x : Interval
n : ℕ
ax : a ∈ approx x
a0 : a ≤ 0
⊢ a ^ 2 ^ (-↑n) ∈ approx (x.log.scaleB' (-Fixed.ofNat0 n)).exp
Tactic:
simp only [log_nonpos a0 ax, nan_scaleB', exp_nan, approx_nan, mem_univ]
Proof state after:
no goals
Theorem: Interval.mem_approx_iter_sqrt
Proof state before:
case neg
a : ℝ
x : Interval
n : ℕ
ax : a ∈ approx x
a0 : ¬a ≤ 0
⊢ a ^ 2 ^ (-↑n) ∈ approx (x.log.scaleB' (-Fixed.ofNat0 n)).exp
Tactic:
rw [Real.rpow_def_of_pos (not_le.mp a0)]
Proof state after:
case neg
a : ℝ
x : Interval
n : ℕ
ax : a ∈ approx x
a0 : ¬a ≤ 0
⊢ (a.log * 2 ^ (-↑n)).exp ∈ approx (x.log.scaleB' (-Fixed.ofNat0 n)).exp
Theorem: Interval.mem_approx_iter_sqrt
Proof state before:
case neg
a : ℝ
x : Interval
n : ℕ
ax : a ∈ approx x
a0 : ¬a ≤ 0
⊢ (a.log * 2 ^ (-↑n)).exp ∈ approx (x.log.scaleB' (-Fixed.ofNat0 n)).exp
Tactic:
mono
Proof state after:
no goals
Theorem: Interval.mem_approx_iter_sqrt'
Proof state before:
a : ℝ
x : Interval
n : ℕ
a0 : 0 ≤ a
ax : a ^ 2 ^ n ∈ approx x
⊢ a ∈ approx (x.iter_sqrt n)
Tactic:
generalize hb : a^(2^n) = b at ax
Proof state after:
a : ℝ
x : Interval
n : ℕ
a0 : 0 ≤ a
b : ℝ
hb : a ^ 2 ^ n = b
ax : b ∈ approx x
⊢ a ∈ approx (x.iter_sqrt n)
Theorem: Interval.mem_approx_iter_sqrt'
Proof state before:
a : ℝ
x : Interval
n : ℕ
a0 : 0 ≤ a
b : ℝ
hb : a ^ 2 ^ n = b
ax : b ∈ approx x
⊢ a ∈ approx (x.iter_sqrt n)
Tactic:
have ab : a = b ^ (2 ^ (-n : ℝ) : ℝ) := by
  have e : (2:ℝ)^n = (2^n : ℕ) := by norm_num
  rw [←hb, Real.rpow_neg (by norm_num), Real.rpow_natCast, e,
    Real.pow_rpow_inv_natCast a0 (pow_ne_zero _ (by norm_num))]
Proof state after:
a : ℝ
x : Interval
n : ℕ
a0 : 0 ≤ a
b : ℝ
hb : a ^ 2 ^ n = b
ax : b ∈ approx x
ab : a = b ^ 2 ^ (-↑n)
⊢ a ∈ approx (x.iter_sqrt n)
Theorem: Interval.mem_approx_iter_sqrt'
Proof state before:
a : ℝ
x : Interval
n : ℕ
a0 : 0 ≤ a
b : ℝ
hb : a ^ 2 ^ n = b
ax : b ∈ approx x
ab : a = b ^ 2 ^ (-↑n)
⊢ a ∈ approx (x.iter_sqrt n)
Tactic:
rw [ab]
Proof state after:
a : ℝ
x : Interval
n : ℕ
a0 : 0 ≤ a
b : ℝ
hb : a ^ 2 ^ n = b
ax : b ∈ approx x
ab : a = b ^ 2 ^ (-↑n)
⊢ b ^ 2 ^ (-↑n) ∈ approx (x.iter_sqrt n)
Theorem: Interval.mem_approx_iter_sqrt'
Proof state before:
a : ℝ
x : Interval
n : ℕ
a0 : 0 ≤ a
b : ℝ
hb : a ^ 2 ^ n = b
ax : b ∈ approx x
ab : a = b ^ 2 ^ (-↑n)
⊢ b ^ 2 ^ (-↑n) ∈ approx (x.iter_sqrt n)
Tactic:
exact mem_approx_iter_sqrt ax
Proof state after:
no goals
Theorem: Interval.mem_approx_iter_sqrt'
Proof state before:
a : ℝ
x : Interval
n : ℕ
a0 : 0 ≤ a
b : ℝ
hb : a ^ 2 ^ n = b
ax : b ∈ approx x
⊢ a = b ^ 2 ^ (-↑n)
Tactic:
have e : (2:ℝ)^n = (2^n : ℕ) := by norm_num
Proof state after:
a : ℝ
x : Interval
n : ℕ
a0 : 0 ≤ a
b : ℝ
hb : a ^ 2 ^ n = b
ax : b ∈ approx x
e : 2 ^ n = ↑(2 ^ n)
⊢ a = b ^ 2 ^ (-↑n)