internlm/Lean-Github huggingface dataset:
Theorem: osgoodManifold
Proof state before:
case right.h
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    ContinuousAt (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) x ∧
      AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (z, x.2)) x.1 ∧
        AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (x.1, z)) x.2
Tactic:
apply ((isOpen_extChartAt_target II p).eventually_mem (mem_extChartAt_target II p)).mp
Proof state after:
case right.h
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
⊢ ∀ᶠ (x : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    x ∈ (extChartAt (I.prod I) p).target →
      ContinuousAt (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) x ∧
        AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (z, x.2)) x.1 ∧
          AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (x.1, z)) x.2
Theorem: osgoodManifold
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
⊢ ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
Tactic:
refine (fc.continuousAt.comp (continuousAt_extChartAt_symm II p)).eventually_mem
    ((isOpen_extChartAt_source I (f p)).mem_nhds ?_)
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
⊢ (f ∘ ↑(extChartAt (I.prod I) p).symm) (↑(extChartAt (I.prod I) p) p) ∈ (extChartAt I (f p)).source
Theorem: osgoodManifold
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
⊢ (f ∘ ↑(extChartAt (I.prod I) p).symm) (↑(extChartAt (I.prod I) p) p) ∈ (extChartAt I (f p)).source
Tactic:
simp only [Function.comp, (extChartAt II p).left_inv (mem_extChartAt_source _ _)]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
⊢ f p ∈ (extChartAt I (f p)).source
Theorem: osgoodManifold
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
⊢ f p ∈ (extChartAt I (f p)).source
Tactic:
apply mem_extChartAt_source
Proof state after:
no goals
Theorem: osgoodManifold
Proof state before:
case right.h.refine_1
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ ContinuousAt (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) q
Tactic:
exact (continuousAt_extChartAt' I fm).comp_of_eq
    (fc.continuousAt.comp (continuousAt_extChartAt_symm'' _ m)) rfl
Proof state after:
no goals
Theorem: osgoodManifold
Proof state before:
case right.h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (z, q.2)) q.1
Tactic:
apply HolomorphicAt.analyticAt I I
Proof state after:
case right.h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ HolomorphicAt I I (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (z, q.2)) q.1
Theorem: osgoodManifold
Proof state before:
case right.h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ HolomorphicAt I I (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (z, q.2)) q.1
Tactic:
refine (HolomorphicAt.extChartAt fm).comp_of_eq ?_ rfl
Proof state after:
case right.h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ HolomorphicAt I I (fun z => (f ∘ ↑(extChartAt (I.prod I) p).symm) (z, q.2)) q.1
Theorem: osgoodManifold
Proof state before:
case right.h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ HolomorphicAt I I (fun z => (f ∘ ↑(extChartAt (I.prod I) p).symm) (z, q.2)) q.1
Tactic:
rw [extChartAt_prod] at m
Proof state after:
case right.h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ ((extChartAt I p.1).prod (extChartAt I p.2)).target
⊢ HolomorphicAt I I (fun z => (f ∘ ↑(extChartAt (I.prod I) p).symm) (z, q.2)) q.1
Theorem: osgoodManifold
Proof state before:
case right.h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ ((extChartAt I p.1).prod (extChartAt I p.2)).target
⊢ HolomorphicAt I I (fun z => (f ∘ ↑(extChartAt (I.prod I) p).symm) (z, q.2)) q.1
Tactic:
simp only [Function.comp, extChartAt_prod, PartialEquiv.prod_symm, PartialEquiv.prod_coe,
  PartialEquiv.prod_target, mem_prod_eq] at m ⊢
Proof state after:
case right.h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q.1 ∈ (extChartAt I p.1).target ∧ q.2 ∈ (extChartAt I p.2).target
⊢ HolomorphicAt I I (fun z => f (↑(extChartAt I p.1).symm z, ↑(extChartAt I p.2).symm q.2)) q.1
Theorem: osgoodManifold
Proof state before:
case right.h.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q.1 ∈ (extChartAt I p.1).target ∧ q.2 ∈ (extChartAt I p.2).target
⊢ HolomorphicAt I I (fun z => f (↑(extChartAt I p.1).symm z, ↑(extChartAt I p.2).symm q.2)) q.1
Tactic:
exact (f0 _ _).comp (HolomorphicAt.extChartAt_symm m.1)
Proof state after:
no goals
Theorem: osgoodManifold
Proof state before:
case right.h.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ AnalyticAt ℂ (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (q.1, z)) q.2
Tactic:
apply HolomorphicAt.analyticAt I I
Proof state after:
case right.h.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ HolomorphicAt I I (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (q.1, z)) q.2
Theorem: osgoodManifold
Proof state before:
case right.h.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ HolomorphicAt I I (fun z => (↑(extChartAt I (f p)) ∘ f ∘ ↑(extChartAt (I.prod I) p).symm) (q.1, z)) q.2
Tactic:
refine (HolomorphicAt.extChartAt fm).comp_of_eq ?_ rfl
Proof state after:
case right.h.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ HolomorphicAt I I (fun z => (f ∘ ↑(extChartAt (I.prod I) p).symm) (q.1, z)) q.2
Theorem: osgoodManifold
Proof state before:
case right.h.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ (extChartAt (I.prod I) p).target
⊢ HolomorphicAt I I (fun z => (f ∘ ↑(extChartAt (I.prod I) p).symm) (q.1, z)) q.2
Tactic:
rw [extChartAt_prod] at m
Proof state after:
case right.h.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ ((extChartAt I p.1).prod (extChartAt I p.2)).target
⊢ HolomorphicAt I I (fun z => (f ∘ ↑(extChartAt (I.prod I) p).symm) (q.1, z)) q.2
Theorem: osgoodManifold
Proof state before:
case right.h.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q ∈ ((extChartAt I p.1).prod (extChartAt I p.2)).target
⊢ HolomorphicAt I I (fun z => (f ∘ ↑(extChartAt (I.prod I) p).symm) (q.1, z)) q.2
Tactic:
simp only [Function.comp, extChartAt_prod, PartialEquiv.prod_symm, PartialEquiv.prod_coe,
  PartialEquiv.prod_target, mem_prod_eq] at m ⊢
Proof state after:
case right.h.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q.1 ∈ (extChartAt I p.1).target ∧ q.2 ∈ (extChartAt I p.2).target
⊢ HolomorphicAt I I (fun z => f (↑(extChartAt I p.1).symm q.1, ↑(extChartAt I p.2).symm z)) q.2
Theorem: osgoodManifold
Proof state before:
case right.h.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : S × T → U
fc : Continuous f
f0 : ∀ (x : S) (y : T), HolomorphicAt I I (fun x => f (x, y)) x
f1 : ∀ (x : S) (y : T), HolomorphicAt I I (fun y => f (x, y)) y
p : S × T
fm✝ :
  ∀ᶠ (q : ℂ × ℂ) in 𝓝 (↑(extChartAt (I.prod I) p) p),
    f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
q : ℂ × ℂ
fm : f (↑(extChartAt (I.prod I) p).symm q) ∈ (extChartAt I (f p)).source
m : q.1 ∈ (extChartAt I p.1).target ∧ q.2 ∈ (extChartAt I p.2).target
⊢ HolomorphicAt I I (fun z => f (↑(extChartAt I p.1).symm q.1, ↑(extChartAt I p.2).symm z)) q.2
Tactic:
exact (f1 _ _).comp (HolomorphicAt.extChartAt_symm m.2)
Proof state after:
no goals
Theorem: exp_ofNat_lt
Proof state before:
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
h0 : autoParam (2.7182818286 ^ a < b) _auto✝
⊢ (↑a).exp < b
Tactic:
rw [←Real.exp_one_pow a]
Proof state after:
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
h0 : autoParam (2.7182818286 ^ a < b) _auto✝
⊢ exp 1 ^ a < b
Theorem: exp_ofNat_lt
Proof state before:
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
h0 : autoParam (2.7182818286 ^ a < b) _auto✝
⊢ exp 1 ^ a < b
Tactic:
exact _root_.trans (pow_lt_pow_left Real.exp_one_lt_d9 (Real.exp_nonneg _) a0) h0
Proof state after:
no goals
Theorem: exp_neg_ofNat_lt
Proof state before:
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (0 < b) _auto✝
h0 : autoParam (b⁻¹ < 2.7182818283 ^ a) _auto✝
⊢ (-↑a).exp < b
Tactic:
rw [Real.exp_neg, inv_lt, ←Real.exp_one_pow a]
Proof state after:
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (0 < b) _auto✝
h0 : autoParam (b⁻¹ < 2.7182818283 ^ a) _auto✝
⊢ b⁻¹ < exp 1 ^ a

case ha
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (0 < b) _auto✝
h0 : autoParam (b⁻¹ < 2.7182818283 ^ a) _auto✝
⊢ 0 < (↑a).exp

case hb
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (0 < b) _auto✝
h0 : autoParam (b⁻¹ < 2.7182818283 ^ a) _auto✝
⊢ 0 < b
Theorem: exp_neg_ofNat_lt
Proof state before:
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (0 < b) _auto✝
h0 : autoParam (b⁻¹ < 2.7182818283 ^ a) _auto✝
⊢ b⁻¹ < exp 1 ^ a
Tactic:
exact _root_.trans h0 (pow_lt_pow_left Real.exp_one_gt_d9 (by norm_num) a0)
Proof state after:
no goals
Theorem: exp_neg_ofNat_lt
Proof state before:
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (0 < b) _auto✝
h0 : autoParam (b⁻¹ < 2.7182818283 ^ a) _auto✝
⊢ 0 ≤ 2.7182818283
Tactic:
norm_num
Proof state after:
no goals
Theorem: exp_neg_ofNat_lt
Proof state before:
case ha
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (0 < b) _auto✝
h0 : autoParam (b⁻¹ < 2.7182818283 ^ a) _auto✝
⊢ 0 < (↑a).exp
Tactic:
exact Real.exp_pos _
Proof state after:
no goals
Theorem: exp_neg_ofNat_lt
Proof state before:
case hb
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
b0 : autoParam (0 < b) _auto✝
h0 : autoParam (b⁻¹ < 2.7182818283 ^ a) _auto✝
⊢ 0 < b
Tactic:
exact b0
Proof state after:
no goals