internlm/Lean-Github huggingface dataset:
Theorem: Super.abs_bottcher
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Tactic:
by_cases m : (c, z) ∈ s.basin
Proof state after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
m : (c, z) ∈ s.basin
⊢ Complex.abs (s.bottcher c z) = s.potential c z

case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
m : (c, z) ∉ s.basin
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Theorem: Super.abs_bottcher
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
⊢ ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
Tactic:
intro c z m
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
m : (c, z) ∈ s.post
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Theorem: Super.abs_bottcher
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
m : (c, z) ∈ s.post
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Tactic:
rcases s.ray_surj m with ⟨x, m, e⟩
Proof state after:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
m✝ : (c, z) ∈ s.post
x : ℂ
m : (c, x) ∈ s.ext
e : s.ray c x = z
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Theorem: Super.abs_bottcher
Proof state before:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
m✝ : (c, z) ∈ s.post
x : ℂ
m : (c, x) ∈ s.ext
e : s.ray c x = z
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Tactic:
rw [← e, s.bottcher_ray m, s.ray_potential m]
Proof state after:
no goals
Theorem: Super.abs_bottcher
Proof state before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
m : (c, z) ∈ s.basin
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Tactic:
rcases s.basin_post m with ⟨n, p⟩
Proof state after:
case pos.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
m : (c, z) ∈ s.basin
n : ℕ
p : (c, (f c)^[n] z) ∈ s.post
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Theorem: Super.abs_bottcher
Proof state before:
case pos.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
m : (c, z) ∈ s.basin
n : ℕ
p : (c, (f c)^[n] z) ∈ s.post
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Tactic:
rw [← Real.pow_rpow_inv_natCast (Complex.abs.nonneg _) (pow_ne_zero n s.d0), ←
  Complex.abs.map_pow, ← s.bottcher_eqn_iter n, base p, s.potential_eqn_iter,
  Real.pow_rpow_inv_natCast s.potential_nonneg (pow_ne_zero n s.d0)]
Proof state after:
no goals
Theorem: Super.abs_bottcher
Proof state before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
m : (c, z) ∉ s.basin
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Tactic:
have m' := m
Proof state after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
m m' : (c, z) ∉ s.basin
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Theorem: Super.abs_bottcher
Proof state before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
m m' : (c, z) ∉ s.basin
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Tactic:
simp only [Super.basin, not_exists, mem_setOf] at m'
Proof state after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
m : (c, z) ∉ s.basin
m' : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Theorem: Super.abs_bottcher
Proof state before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
m : (c, z) ∉ s.basin
m' : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Tactic:
simp only [s.bottcher_not_basin m, Complex.abs.map_one, s.potential_eq_one m']
Proof state after:
no goals
Theorem: Super.bottcher_lt_one
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
m : (c, z) ∈ s.post
⊢ Complex.abs (s.bottcher c z) < 1
Tactic:
replace m := s.bottcher_ext m
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
m : (c, s.bottcher c z) ∈ s.ext
⊢ Complex.abs (s.bottcher c z) < 1
Theorem: Super.bottcher_lt_one
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
m : (c, s.bottcher c z) ∈ s.ext
⊢ Complex.abs (s.bottcher c z) < 1
Tactic:
simp only [Super.ext, mem_setOf] at m
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
m : Complex.abs (s.bottcher c z) < s.p c
⊢ Complex.abs (s.bottcher c z) < 1
Theorem: Super.bottcher_lt_one
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
m : Complex.abs (s.bottcher c z) < s.p c
⊢ Complex.abs (s.bottcher c z) < 1
Tactic:
exact lt_of_lt_of_le m s.p_le_one
Proof state after:
no goals
Theorem: HolomorphicAt.local_inj
Proof state before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
⊢ ∀ᶠ (p : S × S) in 𝓝 (z, z), f p.1 = f p.2 → p.1 = p.2
Tactic:
rcases complex_inverse_fun' fa nc with ⟨g, ga, gf, fg⟩
Proof state after:
case intro.intro.intro
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
⊢ ∀ᶠ (p : S × S) in 𝓝 (z, z), f p.1 = f p.2 → p.1 = p.2
Theorem: HolomorphicAt.local_inj
Proof state before:
case intro.intro.intro
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
⊢ ∀ᶠ (p : S × S) in 𝓝 (z, z), f p.1 = f p.2 → p.1 = p.2
Tactic:
have n : NontrivialHolomorphicAt g (f z) := by
  rw [← gf.self_of_nhds] at fa
  refine (NontrivialHolomorphicAt.anti ?_ fa ga).2
  exact (nontrivialHolomorphicAt_id _).congr (Filter.EventuallyEq.symm fg)
Proof state after:
case intro.intro.intro
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
⊢ ∀ᶠ (p : S × S) in 𝓝 (z, z), f p.1 = f p.2 → p.1 = p.2
Theorem: HolomorphicAt.local_inj
Proof state before:
case intro.intro.intro
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
⊢ ∀ᶠ (p : S × S) in 𝓝 (z, z), f p.1 = f p.2 → p.1 = p.2
Tactic:
have o := n.nhds_eq_map_nhds
Proof state after:
case intro.intro.intro
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 (g (f z)) = Filter.map g (𝓝 (f z))
⊢ ∀ᶠ (p : S × S) in 𝓝 (z, z), f p.1 = f p.2 → p.1 = p.2
Theorem: HolomorphicAt.local_inj
Proof state before:
case intro.intro.intro
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 (g (f z)) = Filter.map g (𝓝 (f z))
⊢ ∀ᶠ (p : S × S) in 𝓝 (z, z), f p.1 = f p.2 → p.1 = p.2
Tactic:
rw [gf.self_of_nhds] at o
Proof state after:
case intro.intro.intro
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
⊢ ∀ᶠ (p : S × S) in 𝓝 (z, z), f p.1 = f p.2 → p.1 = p.2
Theorem: HolomorphicAt.local_inj
Proof state before:
case intro.intro.intro
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
⊢ ∀ᶠ (p : S × S) in 𝓝 (z, z), f p.1 = f p.2 → p.1 = p.2
Tactic:
simp only [nhds_prod_eq, o, Filter.prod_map_map_eq, Filter.eventually_map]
Proof state after:
case intro.intro.intro
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
⊢ ∀ᶠ (a : T × T) in 𝓝 (f z) ×ˢ 𝓝 (f z), f (g a.1) = f (g a.2) → g a.1 = g a.2
Theorem: HolomorphicAt.local_inj
Proof state before:
case intro.intro.intro
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
⊢ ∀ᶠ (a : T × T) in 𝓝 (f z) ×ˢ 𝓝 (f z), f (g a.1) = f (g a.2) → g a.1 = g a.2
Tactic:
refine (fg.prod_mk fg).mp (eventually_of_forall ?_)
Proof state after:
case intro.intro.intro
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
⊢ ∀ (x : T × T), f (g x.1) = x.1 ∧ f (g x.2) = x.2 → f (g x.1) = f (g x.2) → g x.1 = g x.2
Theorem: HolomorphicAt.local_inj
Proof state before:
case intro.intro.intro
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
⊢ ∀ (x : T × T), f (g x.1) = x.1 ∧ f (g x.2) = x.2 → f (g x.1) = f (g x.2) → g x.1 = g x.2
Tactic:
intro ⟨x, y⟩ ⟨ex, ey⟩ h
Proof state after:
case intro.intro.intro
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
x y : T
ex : f (g (x, y).1) = (x, y).1
ey : f (g (x, y).2) = (x, y).2
h : f (g (x, y).1) = f (g (x, y).2)
⊢ g (x, y).1 = g (x, y).2
Theorem: HolomorphicAt.local_inj
Proof state before:
case intro.intro.intro
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
x y : T
ex : f (g (x, y).1) = (x, y).1
ey : f (g (x, y).2) = (x, y).2
h : f (g (x, y).1) = f (g (x, y).2)
⊢ g (x, y).1 = g (x, y).2
Tactic:
simp only at ex ey
Proof state after:
case intro.intro.intro
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
x y : T
ex : f (g x) = x
ey : f (g y) = y
h : f (g (x, y).1) = f (g (x, y).2)
⊢ g (x, y).1 = g (x, y).2
Theorem: HolomorphicAt.local_inj
Proof state before:
case intro.intro.intro
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
x y : T
ex : f (g x) = x
ey : f (g y) = y
h : f (g (x, y).1) = f (g (x, y).2)
⊢ g (x, y).1 = g (x, y).2
Tactic:
simp only [ex, ey] at h
Proof state after:
case intro.intro.intro
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
x y : T
ex : f (g x) = x
ey : f (g y) = y
h : x = y
⊢ g (x, y).1 = g (x, y).2
Theorem: HolomorphicAt.local_inj
Proof state before:
case intro.intro.intro
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
n : NontrivialHolomorphicAt g (f z)
o : 𝓝 z = Filter.map g (𝓝 (f z))
x y : T
ex : f (g x) = x
ey : f (g y) = y
h : x = y
⊢ g (x, y).1 = g (x, y).2
Tactic:
simp only [h]
Proof state after:
no goals
Theorem: HolomorphicAt.local_inj
Proof state before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
fa : HolomorphicAt I I f z
nc : mfderiv I I f z ≠ 0
g : T → S
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
⊢ NontrivialHolomorphicAt g (f z)
Tactic:
rw [← gf.self_of_nhds] at fa
Proof state after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
nc : mfderiv I I f z ≠ 0
g : T → S
fa : HolomorphicAt I I f (g (f z))
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
⊢ NontrivialHolomorphicAt g (f z)
Theorem: HolomorphicAt.local_inj
Proof state before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
nc : mfderiv I I f z ≠ 0
g : T → S
fa : HolomorphicAt I I f (g (f z))
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
⊢ NontrivialHolomorphicAt g (f z)
Tactic:
refine (NontrivialHolomorphicAt.anti ?_ fa ga).2
Proof state after:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
nc : mfderiv I I f z ≠ 0
g : T → S
fa : HolomorphicAt I I f (g (f z))
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
⊢ NontrivialHolomorphicAt (fun z => f (g z)) (f z)
Theorem: HolomorphicAt.local_inj
Proof state before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : S → T
z : S
nc : mfderiv I I f z ≠ 0
g : T → S
fa : HolomorphicAt I I f (g (f z))
ga : HolomorphicAt I I g (f z)
gf : ∀ᶠ (x : S) in 𝓝 z, g (f x) = x
fg : ∀ᶠ (x : T) in 𝓝 (f z), f (g x) = x
⊢ NontrivialHolomorphicAt (fun z => f (g z)) (f z)
Tactic:
exact (nontrivialHolomorphicAt_id _).congr (Filter.EventuallyEq.symm fg)
Proof state after:
no goals
Theorem: HolomorphicAt.local_inj''
Proof state before:
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
⊢ ∀ᶠ (p : (ℂ × S) × ℂ × S) in 𝓝 ((c, z), c, z), p.1.1 = p.2.1 → f p.1.1 p.1.2 = f p.2.1 p.2.2 → p.1 = p.2
Tactic:
rcases complex_inverse_fun fa nc with ⟨g, ga, gf, fg⟩
Proof state after:
case intro.intro.intro
S : Type
inst✝³ : TopologicalSpace S
inst✝² : ChartedSpace ℂ S
cms : AnalyticManifold I S
T : Type
inst✝¹ : TopologicalSpace T
inst✝ : ChartedSpace ℂ T
cmt : AnalyticManifold I T
f : ℂ → S → T
c : ℂ
z : S
fa : HolomorphicAt (I.prod I) I (uncurry f) (c, z)
nc : mfderiv I I (f c) z ≠ 0
g : ℂ → T → S
ga : HolomorphicAt (I.prod I) I (uncurry g) (c, f c z)
gf : ∀ᶠ (x : ℂ × S) in 𝓝 (c, z), g x.1 (f x.1 x.2) = x.2
fg : ∀ᶠ (x : ℂ × T) in 𝓝 (c, f c z), f x.1 (g x.1 x.2) = x.2
⊢ ∀ᶠ (p : (ℂ × S) × ℂ × S) in 𝓝 ((c, z), c, z), p.1.1 = p.2.1 → f p.1.1 p.1.2 = f p.2.1 p.2.2 → p.1 = p.2