internlm/Lean-Github huggingface dataset:
Theorem: HolomorphicAt.pow
Proof state before:
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : M → 𝕜
x : M
fa : HolomorphicAt I 𝓘(𝕜, 𝕜) f x
n : ℕ
e : (fun x => f x ^ n) = (fun z => z ^ n) ∘ f
⊢ HolomorphicAt I 𝓘(𝕜, 𝕜) ((fun z => z ^ n) ∘ f) x
Tactic:
exact (((analyticAt_id _ _).pow _).holomorphicAt _ _).comp fa
Proof state after:
no goals
Theorem: HolomorphicAt.cpow
Proof state before:
𝕜 : Type
inst✝³¹ : NontriviallyNormedField 𝕜
E✝ A✝ : Type
inst✝³⁰ : NormedAddCommGroup E✝
inst✝²⁹ : NormedSpace 𝕜 E✝
inst✝²⁸ : CompleteSpace E✝
inst✝²⁷ : TopologicalSpace A✝
F B : Type
inst✝²⁶ : NormedAddCommGroup F
inst✝²⁵ : NormedSpace 𝕜 F
inst✝²⁴ : CompleteSpace F
inst✝²³ : TopologicalSpace B
G C : Type
inst✝²² : NormedAddCommGroup G
inst✝²¹ : NormedSpace 𝕜 G
inst✝²⁰ : TopologicalSpace C
H D : Type
inst✝¹⁹ : NormedAddCommGroup H
inst✝¹⁸ : NormedSpace 𝕜 H
inst✝¹⁷ : TopologicalSpace D
M✝ : Type
I✝ : ModelWithCorners 𝕜 E✝ A✝
inst✝¹⁶ : TopologicalSpace M✝
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁵ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝¹⁴ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝¹³ : TopologicalSpace P
inst✝¹² : I✝.Boundaryless
inst✝¹¹ : ChartedSpace A✝ M✝
cm : AnalyticManifold I✝ M✝
inst✝¹⁰ : J.Boundaryless
inst✝⁹ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝⁸ : K.Boundaryless
inst✝⁷ : ChartedSpace C O
co : AnalyticManifold K O
inst✝⁶ : L.Boundaryless
inst✝⁵ : ChartedSpace D P
cp : AnalyticManifold L P
E A M : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
inst✝² : TopologicalSpace A
I : ModelWithCorners ℂ E A
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace A M
f g : M → ℂ
x : M
fa : HolomorphicAt I 𝓘(ℂ, ℂ) f x
ga : HolomorphicAt I 𝓘(ℂ, ℂ) g x
a : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HolomorphicAt I 𝓘(ℂ, ℂ) (fun x => f x ^ g x) x
Tactic:
have e : (fun x ↦ f x ^ g x) = (fun p : ℂ × ℂ ↦ p.1 ^ p.2) ∘ fun x ↦ (f x, g x) := rfl
Proof state after:
𝕜 : Type
inst✝³¹ : NontriviallyNormedField 𝕜
E✝ A✝ : Type
inst✝³⁰ : NormedAddCommGroup E✝
inst✝²⁹ : NormedSpace 𝕜 E✝
inst✝²⁸ : CompleteSpace E✝
inst✝²⁷ : TopologicalSpace A✝
F B : Type
inst✝²⁶ : NormedAddCommGroup F
inst✝²⁵ : NormedSpace 𝕜 F
inst✝²⁴ : CompleteSpace F
inst✝²³ : TopologicalSpace B
G C : Type
inst✝²² : NormedAddCommGroup G
inst✝²¹ : NormedSpace 𝕜 G
inst✝²⁰ : TopologicalSpace C
H D : Type
inst✝¹⁹ : NormedAddCommGroup H
inst✝¹⁸ : NormedSpace 𝕜 H
inst✝¹⁷ : TopologicalSpace D
M✝ : Type
I✝ : ModelWithCorners 𝕜 E✝ A✝
inst✝¹⁶ : TopologicalSpace M✝
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁵ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝¹⁴ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝¹³ : TopologicalSpace P
inst✝¹² : I✝.Boundaryless
inst✝¹¹ : ChartedSpace A✝ M✝
cm : AnalyticManifold I✝ M✝
inst✝¹⁰ : J.Boundaryless
inst✝⁹ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝⁸ : K.Boundaryless
inst✝⁷ : ChartedSpace C O
co : AnalyticManifold K O
inst✝⁶ : L.Boundaryless
inst✝⁵ : ChartedSpace D P
cp : AnalyticManifold L P
E A M : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
inst✝² : TopologicalSpace A
I : ModelWithCorners ℂ E A
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace A M
f g : M → ℂ
x : M
fa : HolomorphicAt I 𝓘(ℂ, ℂ) f x
ga : HolomorphicAt I 𝓘(ℂ, ℂ) g x
a : 0 < (f x).re ∨ (f x).im ≠ 0
e : (fun x => f x ^ g x) = (fun p => p.1 ^ p.2) ∘ fun x => (f x, g x)
⊢ HolomorphicAt I 𝓘(ℂ, ℂ) (fun x => f x ^ g x) x
Theorem: HolomorphicAt.cpow
Proof state before:
𝕜 : Type
inst✝³¹ : NontriviallyNormedField 𝕜
E✝ A✝ : Type
inst✝³⁰ : NormedAddCommGroup E✝
inst✝²⁹ : NormedSpace 𝕜 E✝
inst✝²⁸ : CompleteSpace E✝
inst✝²⁷ : TopologicalSpace A✝
F B : Type
inst✝²⁶ : NormedAddCommGroup F
inst✝²⁵ : NormedSpace 𝕜 F
inst✝²⁴ : CompleteSpace F
inst✝²³ : TopologicalSpace B
G C : Type
inst✝²² : NormedAddCommGroup G
inst✝²¹ : NormedSpace 𝕜 G
inst✝²⁰ : TopologicalSpace C
H D : Type
inst✝¹⁹ : NormedAddCommGroup H
inst✝¹⁸ : NormedSpace 𝕜 H
inst✝¹⁷ : TopologicalSpace D
M✝ : Type
I✝ : ModelWithCorners 𝕜 E✝ A✝
inst✝¹⁶ : TopologicalSpace M✝
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁵ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝¹⁴ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝¹³ : TopologicalSpace P
inst✝¹² : I✝.Boundaryless
inst✝¹¹ : ChartedSpace A✝ M✝
cm : AnalyticManifold I✝ M✝
inst✝¹⁰ : J.Boundaryless
inst✝⁹ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝⁸ : K.Boundaryless
inst✝⁷ : ChartedSpace C O
co : AnalyticManifold K O
inst✝⁶ : L.Boundaryless
inst✝⁵ : ChartedSpace D P
cp : AnalyticManifold L P
E A M : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
inst✝² : TopologicalSpace A
I : ModelWithCorners ℂ E A
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace A M
f g : M → ℂ
x : M
fa : HolomorphicAt I 𝓘(ℂ, ℂ) f x
ga : HolomorphicAt I 𝓘(ℂ, ℂ) g x
a : 0 < (f x).re ∨ (f x).im ≠ 0
e : (fun x => f x ^ g x) = (fun p => p.1 ^ p.2) ∘ fun x => (f x, g x)
⊢ HolomorphicAt I 𝓘(ℂ, ℂ) (fun x => f x ^ g x) x
Tactic:
rw [e]
Proof state after:
𝕜 : Type
inst✝³¹ : NontriviallyNormedField 𝕜
E✝ A✝ : Type
inst✝³⁰ : NormedAddCommGroup E✝
inst✝²⁹ : NormedSpace 𝕜 E✝
inst✝²⁸ : CompleteSpace E✝
inst✝²⁷ : TopologicalSpace A✝
F B : Type
inst✝²⁶ : NormedAddCommGroup F
inst✝²⁵ : NormedSpace 𝕜 F
inst✝²⁴ : CompleteSpace F
inst✝²³ : TopologicalSpace B
G C : Type
inst✝²² : NormedAddCommGroup G
inst✝²¹ : NormedSpace 𝕜 G
inst✝²⁰ : TopologicalSpace C
H D : Type
inst✝¹⁹ : NormedAddCommGroup H
inst✝¹⁸ : NormedSpace 𝕜 H
inst✝¹⁷ : TopologicalSpace D
M✝ : Type
I✝ : ModelWithCorners 𝕜 E✝ A✝
inst✝¹⁶ : TopologicalSpace M✝
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁵ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝¹⁴ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝¹³ : TopologicalSpace P
inst✝¹² : I✝.Boundaryless
inst✝¹¹ : ChartedSpace A✝ M✝
cm : AnalyticManifold I✝ M✝
inst✝¹⁰ : J.Boundaryless
inst✝⁹ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝⁸ : K.Boundaryless
inst✝⁷ : ChartedSpace C O
co : AnalyticManifold K O
inst✝⁶ : L.Boundaryless
inst✝⁵ : ChartedSpace D P
cp : AnalyticManifold L P
E A M : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
inst✝² : TopologicalSpace A
I : ModelWithCorners ℂ E A
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace A M
f g : M → ℂ
x : M
fa : HolomorphicAt I 𝓘(ℂ, ℂ) f x
ga : HolomorphicAt I 𝓘(ℂ, ℂ) g x
a : 0 < (f x).re ∨ (f x).im ≠ 0
e : (fun x => f x ^ g x) = (fun p => p.1 ^ p.2) ∘ fun x => (f x, g x)
⊢ HolomorphicAt I 𝓘(ℂ, ℂ) ((fun p => p.1 ^ p.2) ∘ fun x => (f x, g x)) x
Theorem: HolomorphicAt.cpow
Proof state before:
𝕜 : Type
inst✝³¹ : NontriviallyNormedField 𝕜
E✝ A✝ : Type
inst✝³⁰ : NormedAddCommGroup E✝
inst✝²⁹ : NormedSpace 𝕜 E✝
inst✝²⁸ : CompleteSpace E✝
inst✝²⁷ : TopologicalSpace A✝
F B : Type
inst✝²⁶ : NormedAddCommGroup F
inst✝²⁵ : NormedSpace 𝕜 F
inst✝²⁴ : CompleteSpace F
inst✝²³ : TopologicalSpace B
G C : Type
inst✝²² : NormedAddCommGroup G
inst✝²¹ : NormedSpace 𝕜 G
inst✝²⁰ : TopologicalSpace C
H D : Type
inst✝¹⁹ : NormedAddCommGroup H
inst✝¹⁸ : NormedSpace 𝕜 H
inst✝¹⁷ : TopologicalSpace D
M✝ : Type
I✝ : ModelWithCorners 𝕜 E✝ A✝
inst✝¹⁶ : TopologicalSpace M✝
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁵ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝¹⁴ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝¹³ : TopologicalSpace P
inst✝¹² : I✝.Boundaryless
inst✝¹¹ : ChartedSpace A✝ M✝
cm : AnalyticManifold I✝ M✝
inst✝¹⁰ : J.Boundaryless
inst✝⁹ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝⁸ : K.Boundaryless
inst✝⁷ : ChartedSpace C O
co : AnalyticManifold K O
inst✝⁶ : L.Boundaryless
inst✝⁵ : ChartedSpace D P
cp : AnalyticManifold L P
E A M : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
inst✝² : TopologicalSpace A
I : ModelWithCorners ℂ E A
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace A M
f g : M → ℂ
x : M
fa : HolomorphicAt I 𝓘(ℂ, ℂ) f x
ga : HolomorphicAt I 𝓘(ℂ, ℂ) g x
a : 0 < (f x).re ∨ (f x).im ≠ 0
e : (fun x => f x ^ g x) = (fun p => p.1 ^ p.2) ∘ fun x => (f x, g x)
⊢ HolomorphicAt I 𝓘(ℂ, ℂ) ((fun p => p.1 ^ p.2) ∘ fun x => (f x, g x)) x
Tactic:
refine (((analyticAt_fst _).cpow (analyticAt_snd _) ?_).holomorphicAt _ _).comp (fa.prod ga)
Proof state after:
𝕜 : Type
inst✝³¹ : NontriviallyNormedField 𝕜
E✝ A✝ : Type
inst✝³⁰ : NormedAddCommGroup E✝
inst✝²⁹ : NormedSpace 𝕜 E✝
inst✝²⁸ : CompleteSpace E✝
inst✝²⁷ : TopologicalSpace A✝
F B : Type
inst✝²⁶ : NormedAddCommGroup F
inst✝²⁵ : NormedSpace 𝕜 F
inst✝²⁴ : CompleteSpace F
inst✝²³ : TopologicalSpace B
G C : Type
inst✝²² : NormedAddCommGroup G
inst✝²¹ : NormedSpace 𝕜 G
inst✝²⁰ : TopologicalSpace C
H D : Type
inst✝¹⁹ : NormedAddCommGroup H
inst✝¹⁸ : NormedSpace 𝕜 H
inst✝¹⁷ : TopologicalSpace D
M✝ : Type
I✝ : ModelWithCorners 𝕜 E✝ A✝
inst✝¹⁶ : TopologicalSpace M✝
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁵ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝¹⁴ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝¹³ : TopologicalSpace P
inst✝¹² : I✝.Boundaryless
inst✝¹¹ : ChartedSpace A✝ M✝
cm : AnalyticManifold I✝ M✝
inst✝¹⁰ : J.Boundaryless
inst✝⁹ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝⁸ : K.Boundaryless
inst✝⁷ : ChartedSpace C O
co : AnalyticManifold K O
inst✝⁶ : L.Boundaryless
inst✝⁵ : ChartedSpace D P
cp : AnalyticManifold L P
E A M : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
inst✝² : TopologicalSpace A
I : ModelWithCorners ℂ E A
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace A M
f g : M → ℂ
x : M
fa : HolomorphicAt I 𝓘(ℂ, ℂ) f x
ga : HolomorphicAt I 𝓘(ℂ, ℂ) g x
a : 0 < (f x).re ∨ (f x).im ≠ 0
e : (fun x => f x ^ g x) = (fun p => p.1 ^ p.2) ∘ fun x => (f x, g x)
⊢ ((fun x => (f x, g x)) x).1 ∈ Complex.slitPlane
Theorem: HolomorphicAt.cpow
Proof state before:
𝕜 : Type
inst✝³¹ : NontriviallyNormedField 𝕜
E✝ A✝ : Type
inst✝³⁰ : NormedAddCommGroup E✝
inst✝²⁹ : NormedSpace 𝕜 E✝
inst✝²⁸ : CompleteSpace E✝
inst✝²⁷ : TopologicalSpace A✝
F B : Type
inst✝²⁶ : NormedAddCommGroup F
inst✝²⁵ : NormedSpace 𝕜 F
inst✝²⁴ : CompleteSpace F
inst✝²³ : TopologicalSpace B
G C : Type
inst✝²² : NormedAddCommGroup G
inst✝²¹ : NormedSpace 𝕜 G
inst✝²⁰ : TopologicalSpace C
H D : Type
inst✝¹⁹ : NormedAddCommGroup H
inst✝¹⁸ : NormedSpace 𝕜 H
inst✝¹⁷ : TopologicalSpace D
M✝ : Type
I✝ : ModelWithCorners 𝕜 E✝ A✝
inst✝¹⁶ : TopologicalSpace M✝
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁵ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝¹⁴ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝¹³ : TopologicalSpace P
inst✝¹² : I✝.Boundaryless
inst✝¹¹ : ChartedSpace A✝ M✝
cm : AnalyticManifold I✝ M✝
inst✝¹⁰ : J.Boundaryless
inst✝⁹ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝⁸ : K.Boundaryless
inst✝⁷ : ChartedSpace C O
co : AnalyticManifold K O
inst✝⁶ : L.Boundaryless
inst✝⁵ : ChartedSpace D P
cp : AnalyticManifold L P
E A M : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
inst✝² : TopologicalSpace A
I : ModelWithCorners ℂ E A
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace A M
f g : M → ℂ
x : M
fa : HolomorphicAt I 𝓘(ℂ, ℂ) f x
ga : HolomorphicAt I 𝓘(ℂ, ℂ) g x
a : 0 < (f x).re ∨ (f x).im ≠ 0
e : (fun x => f x ^ g x) = (fun p => p.1 ^ p.2) ∘ fun x => (f x, g x)
⊢ ((fun x => (f x, g x)) x).1 ∈ Complex.slitPlane
Tactic:
exact a
Proof state after:
no goals
Theorem: HolomorphicAt.smoothAt
Proof state before:
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : M → N
x : M
fa : HolomorphicAt I J f x
⊢ SmoothAt I J f x
Tactic:
rw [holomorphicAt_iff] at fa
Proof state after:
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : M → N
x : M
fa :
  ContinuousAt f x ∧
    AnalyticAt 𝕜 (↑(_root_.extChartAt J (f x)) ∘ f ∘ ↑(_root_.extChartAt I x).symm) (↑(_root_.extChartAt I x) x)
⊢ SmoothAt I J f x
Theorem: HolomorphicAt.smoothAt
Proof state before:
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : M → N
x : M
fa :
  ContinuousAt f x ∧
    AnalyticAt 𝕜 (↑(_root_.extChartAt J (f x)) ∘ f ∘ ↑(_root_.extChartAt I x).symm) (↑(_root_.extChartAt I x) x)
⊢ SmoothAt I J f x
Tactic:
simp only [SmoothAt, contMDiffAt_iff]
Proof state after:
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : M → N
x : M
fa :
  ContinuousAt f x ∧
    AnalyticAt 𝕜 (↑(_root_.extChartAt J (f x)) ∘ f ∘ ↑(_root_.extChartAt I x).symm) (↑(_root_.extChartAt I x) x)
⊢ ContinuousAt f x ∧
    ContDiffWithinAt 𝕜 ⊤ (↑(_root_.extChartAt J (f x)) ∘ f ∘ ↑(_root_.extChartAt I x).symm) (range ↑I)
      (↑(_root_.extChartAt I x) x)
Theorem: HolomorphicAt.smoothAt
Proof state before:
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : M → N
x : M
fa :
  ContinuousAt f x ∧
    AnalyticAt 𝕜 (↑(_root_.extChartAt J (f x)) ∘ f ∘ ↑(_root_.extChartAt I x).symm) (↑(_root_.extChartAt I x) x)
⊢ ContinuousAt f x ∧
    ContDiffWithinAt 𝕜 ⊤ (↑(_root_.extChartAt J (f x)) ∘ f ∘ ↑(_root_.extChartAt I x).symm) (range ↑I)
      (↑(_root_.extChartAt I x) x)
Tactic:
use fa.1
Proof state after:
case right
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : M → N
x : M
fa :
  ContinuousAt f x ∧
    AnalyticAt 𝕜 (↑(_root_.extChartAt J (f x)) ∘ f ∘ ↑(_root_.extChartAt I x).symm) (↑(_root_.extChartAt I x) x)
⊢ ContDiffWithinAt 𝕜 ⊤ (↑(_root_.extChartAt J (f x)) ∘ f ∘ ↑(_root_.extChartAt I x).symm) (range ↑I)
    (↑(_root_.extChartAt I x) x)
Theorem: HolomorphicAt.smoothAt
Proof state before:
case right
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : M → N
x : M
fa :
  ContinuousAt f x ∧
    AnalyticAt 𝕜 (↑(_root_.extChartAt J (f x)) ∘ f ∘ ↑(_root_.extChartAt I x).symm) (↑(_root_.extChartAt I x) x)
⊢ ContDiffWithinAt 𝕜 ⊤ (↑(_root_.extChartAt J (f x)) ∘ f ∘ ↑(_root_.extChartAt I x).symm) (range ↑I)
    (↑(_root_.extChartAt I x) x)
Tactic:
use fa.2.contDiffAt.contDiffWithinAt
Proof state after:
no goals
Theorem: Holomorphic.iter
Proof state before:
case succ
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : M → M
fa : Holomorphic I I f
n : ℕ
h : Holomorphic I I f^[n]
⊢ Holomorphic I I f^[n + 1]
Tactic:
simp only [Function.iterate_succ']
Proof state after:
case succ
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : M → M
fa : Holomorphic I I f
n : ℕ
h : Holomorphic I I f^[n]
⊢ Holomorphic I I (f ∘ f^[n])