internlm/Lean-Github huggingface dataset:
Theorem: bottcher_surj
Proof state before:
case a.refine_3.intro.intro.a.hs
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
mt : x ∈ closure (bottcher d '' t)
⊢ ContinuousOn (bottcher d) (multibrotExt d)
Tactic:
exact (bottcherHolomorphic d).continuousOn
Proof state after:
no goals
Theorem: bottcher_surj
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
⊢ t ⊆ multibrotExt d
Tactic:
intro c m
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m✝ : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
c : 𝕊
m : c ∈ t
⊢ c ∈ multibrotExt d
Theorem: bottcher_surj
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m✝ : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
c : 𝕊
m : c ∈ t
⊢ c ∈ multibrotExt d
Tactic:
rw [← potential_lt_one]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m✝ : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
c : 𝕊
m : c ∈ t
⊢ potential d c < 1
Theorem: bottcher_surj
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m✝ : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
c : 𝕊
m : c ∈ t
⊢ potential d c < 1
Tactic:
exact lt_of_le_of_lt m b1
Proof state after:
no goals
Theorem: bottcher_surj
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : x ∈ closure (bottcher d '' multibrotExt d)
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
⊢ x ∈ closure (bottcher d '' t)
Tactic:
rw [mem_closure_iff_frequently] at m ⊢
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ bottcher d '' multibrotExt d
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
⊢ ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ bottcher d '' t
Theorem: bottcher_surj
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ bottcher d '' multibrotExt d
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
⊢ ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ bottcher d '' t
Tactic:
apply m.mp
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ bottcher d '' multibrotExt d
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
⊢ ∀ᶠ (x : ℂ) in 𝓝 x, x ∈ bottcher d '' multibrotExt d → x ∈ bottcher d '' t
Theorem: bottcher_surj
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ bottcher d '' multibrotExt d
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
⊢ ∀ᶠ (x : ℂ) in 𝓝 x, x ∈ bottcher d '' multibrotExt d → x ∈ bottcher d '' t
Tactic:
have lt : ∀ᶠ y : ℂ in 𝓝 x, abs y < b :=
  Complex.continuous_abs.continuousAt.eventually_lt continuousAt_const xb
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ bottcher d '' multibrotExt d
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
lt : ∀ᶠ (y : ℂ) in 𝓝 x, Complex.abs y < b
⊢ ∀ᶠ (x : ℂ) in 𝓝 x, x ∈ bottcher d '' multibrotExt d → x ∈ bottcher d '' t
Theorem: bottcher_surj
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ bottcher d '' multibrotExt d
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
lt : ∀ᶠ (y : ℂ) in 𝓝 x, Complex.abs y < b
⊢ ∀ᶠ (x : ℂ) in 𝓝 x, x ∈ bottcher d '' multibrotExt d → x ∈ bottcher d '' t
Tactic:
refine lt.mp (eventually_of_forall fun y lt m ↦ ?_)
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m✝ : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ bottcher d '' multibrotExt d
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
lt✝ : ∀ᶠ (y : ℂ) in 𝓝 x, Complex.abs y < b
y : ℂ
lt : Complex.abs y < b
m : y ∈ bottcher d '' multibrotExt d
⊢ y ∈ bottcher d '' t
Theorem: bottcher_surj
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m✝ : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ bottcher d '' multibrotExt d
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
lt✝ : ∀ᶠ (y : ℂ) in 𝓝 x, Complex.abs y < b
y : ℂ
lt : Complex.abs y < b
m : y ∈ bottcher d '' multibrotExt d
⊢ y ∈ bottcher d '' t
Tactic:
rcases m with ⟨c, _, cy⟩
Proof state after:
case intro.intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ bottcher d '' multibrotExt d
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
lt✝ : ∀ᶠ (y : ℂ) in 𝓝 x, Complex.abs y < b
y : ℂ
lt : Complex.abs y < b
c : 𝕊
left✝ : c ∈ multibrotExt d
cy : bottcher d c = y
⊢ y ∈ bottcher d '' t
Theorem: bottcher_surj
Proof state before:
case intro.intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ bottcher d '' multibrotExt d
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
lt✝ : ∀ᶠ (y : ℂ) in 𝓝 x, Complex.abs y < b
y : ℂ
lt : Complex.abs y < b
c : 𝕊
left✝ : c ∈ multibrotExt d
cy : bottcher d c = y
⊢ y ∈ bottcher d '' t
Tactic:
rw [← cy]
Proof state after:
case intro.intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ bottcher d '' multibrotExt d
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
lt✝ : ∀ᶠ (y : ℂ) in 𝓝 x, Complex.abs y < b
y : ℂ
lt : Complex.abs y < b
c : 𝕊
left✝ : c ∈ multibrotExt d
cy : bottcher d c = y
⊢ bottcher d c ∈ bottcher d '' t
Theorem: bottcher_surj
Proof state before:
case intro.intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ bottcher d '' multibrotExt d
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
lt✝ : ∀ᶠ (y : ℂ) in 𝓝 x, Complex.abs y < b
y : ℂ
lt : Complex.abs y < b
c : 𝕊
left✝ : c ∈ multibrotExt d
cy : bottcher d c = y
⊢ bottcher d c ∈ bottcher d '' t
Tactic:
rw [← cy, abs_bottcher] at lt
Proof state after:
case intro.intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ bottcher d '' multibrotExt d
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
lt✝ : ∀ᶠ (y : ℂ) in 𝓝 x, Complex.abs y < b
y : ℂ
c : 𝕊
lt : potential d c < b
left✝ : c ∈ multibrotExt d
cy : bottcher d c = y
⊢ bottcher d c ∈ bottcher d '' t
Theorem: bottcher_surj
Proof state before:
case intro.intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x : ℂ
m : ∃ᶠ (x : ℂ) in 𝓝 x, x ∈ bottcher d '' multibrotExt d
x1 : Complex.abs x < 1
b : ℝ
xb : Complex.abs x < b
b1 : b < 1
t : Set 𝕊 := {e | potential d e ≤ b}
ct : IsCompact t
ts : t ⊆ multibrotExt d
lt✝ : ∀ᶠ (y : ℂ) in 𝓝 x, Complex.abs y < b
y : ℂ
c : 𝕊
lt : potential d c < b
left✝ : c ∈ multibrotExt d
cy : bottcher d c = y
⊢ bottcher d c ∈ bottcher d '' t
Tactic:
exact ⟨c, lt.le, rfl⟩
Proof state after:
no goals
Theorem: bottcher_large_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ Tendsto (fun z => ⋯.bottcher c ↑z * z) atInf (𝓝 1)
Tactic:
set s := superF d
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ Tendsto (fun z => s.bottcher c ↑z * z) atInf (𝓝 1)
Theorem: bottcher_large_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ Tendsto (fun z => s.bottcher c ↑z * z) atInf (𝓝 1)
Tactic:
have e : ∀ᶠ z : ℂ in atInf, s.bottcher c z * z = s.bottcherNear c z * z := by
  suffices e : ∀ᶠ z : ℂ in atInf, s.bottcher c z = s.bottcherNear c z by
    exact e.mp (eventually_of_forall fun z e ↦ by rw [e])
  refine coe_tendsto_inf.eventually (p := fun z ↦ s.bottcher c z = s.bottcherNear c z) ?_
  apply s.bottcher_eq_bottcherNear
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
e : ∀ᶠ (z : ℂ) in atInf, s.bottcher c ↑z * z = s.bottcherNear c ↑z * z
⊢ Tendsto (fun z => s.bottcher c ↑z * z) atInf (𝓝 1)
Theorem: bottcher_large_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
e : ∀ᶠ (z : ℂ) in atInf, s.bottcher c ↑z * z = s.bottcherNear c ↑z * z
⊢ Tendsto (fun z => s.bottcher c ↑z * z) atInf (𝓝 1)
Tactic:
rw [Filter.tendsto_congr' e]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
e : ∀ᶠ (z : ℂ) in atInf, s.bottcher c ↑z * z = s.bottcherNear c ↑z * z
⊢ Tendsto (fun x => s.bottcherNear c ↑x * x) atInf (𝓝 1)
Theorem: bottcher_large_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
e : ∀ᶠ (z : ℂ) in atInf, s.bottcher c ↑z * z = s.bottcherNear c ↑z * z
⊢ Tendsto (fun x => s.bottcherNear c ↑x * x) atInf (𝓝 1)
Tactic:
clear e
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ Tendsto (fun x => s.bottcherNear c ↑x * x) atInf (𝓝 1)
Theorem: bottcher_large_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ Tendsto (fun x => s.bottcherNear c ↑x * x) atInf (𝓝 1)
Tactic:
have m := bottcherNear_monic (s.superNearC.s (mem_univ c))
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : HasDerivAt (bottcherNear (s.fl c) d) 1 0
⊢ Tendsto (fun x => s.bottcherNear c ↑x * x) atInf (𝓝 1)
Theorem: bottcher_large_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : HasDerivAt (bottcherNear (s.fl c) d) 1 0
⊢ Tendsto (fun x => s.bottcherNear c ↑x * x) atInf (𝓝 1)
Tactic:
simp only [hasDerivAt_iff_tendsto, sub_zero, bottcherNear_zero, smul_eq_mul, mul_one,
  Metric.tendsto_nhds_nhds, Real.dist_eq, Complex.norm_eq_abs, Complex.dist_eq, abs_mul,
  abs_of_nonneg (Complex.abs.nonneg _), abs_inv] at m
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
⊢ Tendsto (fun x => s.bottcherNear c ↑x * x) atInf (𝓝 1)
Theorem: bottcher_large_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
⊢ Tendsto (fun x => s.bottcherNear c ↑x * x) atInf (𝓝 1)
Tactic:
simp only [Metric.tendsto_nhds, atInf_basis.eventually_iff, true_and_iff, mem_setOf,
  Complex.dist_eq, Complex.norm_eq_abs]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
⊢ ∀ ε > 0, ∃ i, ∀ ⦃x : ℂ⦄, i < Complex.abs x → Complex.abs (s.bottcherNear c ↑x * x - 1) < ε
Theorem: bottcher_large_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
⊢ ∀ ε > 0, ∃ i, ∀ ⦃x : ℂ⦄, i < Complex.abs x → Complex.abs (s.bottcherNear c ↑x * x - 1) < ε
Tactic:
intro e ep
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
⊢ ∃ i, ∀ ⦃x : ℂ⦄, i < Complex.abs x → Complex.abs (s.bottcherNear c ↑x * x - 1) < e
Theorem: bottcher_large_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
⊢ ∃ i, ∀ ⦃x : ℂ⦄, i < Complex.abs x → Complex.abs (s.bottcherNear c ↑x * x - 1) < e
Tactic:
rcases m e ep with ⟨r, rp, h⟩
Proof state after:
case intro.intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
r : ℝ
rp : r > 0
h : ∀ {x : ℂ}, Complex.abs x < r → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < e
⊢ ∃ i, ∀ ⦃x : ℂ⦄, i < Complex.abs x → Complex.abs (s.bottcherNear c ↑x * x - 1) < e
Theorem: bottcher_large_approx
Proof state before:
case intro.intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
r : ℝ
rp : r > 0
h : ∀ {x : ℂ}, Complex.abs x < r → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < e
⊢ ∃ i, ∀ ⦃x : ℂ⦄, i < Complex.abs x → Complex.abs (s.bottcherNear c ↑x * x - 1) < e
Tactic:
use 1 / r
Proof state after:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
r : ℝ
rp : r > 0
h : ∀ {x : ℂ}, Complex.abs x < r → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < e
⊢ ∀ ⦃x : ℂ⦄, 1 / r < Complex.abs x → Complex.abs (s.bottcherNear c ↑x * x - 1) < e
Theorem: bottcher_large_approx
Proof state before:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
r : ℝ
rp : r > 0
h : ∀ {x : ℂ}, Complex.abs x < r → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < e
⊢ ∀ ⦃x : ℂ⦄, 1 / r < Complex.abs x → Complex.abs (s.bottcherNear c ↑x * x - 1) < e
Tactic:
intro z zr
Proof state after:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
r : ℝ
rp : r > 0
h : ∀ {x : ℂ}, Complex.abs x < r → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < e
z : ℂ
zr : 1 / r < Complex.abs z
⊢ Complex.abs (s.bottcherNear c ↑z * z - 1) < e
Theorem: bottcher_large_approx
Proof state before:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
r : ℝ
rp : r > 0
h : ∀ {x : ℂ}, Complex.abs x < r → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < e
z : ℂ
zr : 1 / r < Complex.abs z
⊢ Complex.abs (s.bottcherNear c ↑z * z - 1) < e
Tactic:
have az0 : abs z ≠ 0 := (lt_trans (one_div_pos.mpr rp) zr).ne'
Proof state after:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
r : ℝ
rp : r > 0
h : ∀ {x : ℂ}, Complex.abs x < r → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < e
z : ℂ
zr : 1 / r < Complex.abs z
az0 : Complex.abs z ≠ 0
⊢ Complex.abs (s.bottcherNear c ↑z * z - 1) < e
Theorem: bottcher_large_approx
Proof state before:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
r : ℝ
rp : r > 0
h : ∀ {x : ℂ}, Complex.abs x < r → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < e
z : ℂ
zr : 1 / r < Complex.abs z
az0 : Complex.abs z ≠ 0
⊢ Complex.abs (s.bottcherNear c ↑z * z - 1) < e
Tactic:
have z0 : z ≠ 0 := Complex.abs.ne_zero_iff.mp az0
Proof state after:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
r : ℝ
rp : r > 0
h : ∀ {x : ℂ}, Complex.abs x < r → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < e
z : ℂ
zr : 1 / r < Complex.abs z
az0 : Complex.abs z ≠ 0
z0 : z ≠ 0
⊢ Complex.abs (s.bottcherNear c ↑z * z - 1) < e
Theorem: bottcher_large_approx
Proof state before:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
r : ℝ
rp : r > 0
h : ∀ {x : ℂ}, Complex.abs x < r → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < e
z : ℂ
zr : 1 / r < Complex.abs z
az0 : Complex.abs z ≠ 0
z0 : z ≠ 0
⊢ Complex.abs (s.bottcherNear c ↑z * z - 1) < e
Tactic:
have zir : abs (z⁻¹) < r := by
  simp only [one_div, map_inv₀] at zr ⊢; exact inv_lt_of_inv_lt rp zr
Proof state after:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
r : ℝ
rp : r > 0
h : ∀ {x : ℂ}, Complex.abs x < r → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < e
z : ℂ
zr : 1 / r < Complex.abs z
az0 : Complex.abs z ≠ 0
z0 : z ≠ 0
zir : Complex.abs z⁻¹ < r
⊢ Complex.abs (s.bottcherNear c ↑z * z - 1) < e
Theorem: bottcher_large_approx
Proof state before:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
r : ℝ
rp : r > 0
h : ∀ {x : ℂ}, Complex.abs x < r → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < e
z : ℂ
zr : 1 / r < Complex.abs z
az0 : Complex.abs z ≠ 0
z0 : z ≠ 0
zir : Complex.abs z⁻¹ < r
⊢ Complex.abs (s.bottcherNear c ↑z * z - 1) < e
Tactic:
specialize @h z⁻¹ zir
Proof state after:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
r : ℝ
rp : r > 0
z : ℂ
zr : 1 / r < Complex.abs z
az0 : Complex.abs z ≠ 0
z0 : z ≠ 0
zir : Complex.abs z⁻¹ < r
h : (Complex.abs z⁻¹)⁻¹ * Complex.abs (bottcherNear (s.fl c) d z⁻¹ - z⁻¹) < e
⊢ Complex.abs (s.bottcherNear c ↑z * z - 1) < e
Theorem: bottcher_large_approx
Proof state before:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
r : ℝ
rp : r > 0
z : ℂ
zr : 1 / r < Complex.abs z
az0 : Complex.abs z ≠ 0
z0 : z ≠ 0
zir : Complex.abs z⁻¹ < r
h : (Complex.abs z⁻¹)⁻¹ * Complex.abs (bottcherNear (s.fl c) d z⁻¹ - z⁻¹) < e
⊢ Complex.abs (s.bottcherNear c ↑z * z - 1) < e
Tactic:
simp only [map_inv₀, inv_inv, ← Complex.abs.map_mul, sub_mul, inv_mul_cancel z0,
  mul_comm z _] at h
Proof state after:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
r : ℝ
rp : r > 0
z : ℂ
zr : 1 / r < Complex.abs z
az0 : Complex.abs z ≠ 0
z0 : z ≠ 0
zir : Complex.abs z⁻¹ < r
h : Complex.abs (bottcherNear (s.fl c) d z⁻¹ * z - 1) < e
⊢ Complex.abs (s.bottcherNear c ↑z * z - 1) < e
Theorem: bottcher_large_approx
Proof state before:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
r : ℝ
rp : r > 0
z : ℂ
zr : 1 / r < Complex.abs z
az0 : Complex.abs z ≠ 0
z0 : z ≠ 0
zir : Complex.abs z⁻¹ < r
h : Complex.abs (bottcherNear (s.fl c) d z⁻¹ * z - 1) < e
⊢ Complex.abs (s.bottcherNear c ↑z * z - 1) < e
Tactic:
simp only [Super.bottcherNear, extChartAt_inf, PartialEquiv.trans_apply,
  coePartialEquiv_symm_apply, Equiv.toPartialEquiv_apply, invEquiv_apply, RiemannSphere.inv_inf,
  toComplex_zero, sub_zero, inv_coe z0, toComplex_coe]
Proof state after:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
m : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℂ}, Complex.abs x < δ → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < ε
e : ℝ
ep : e > 0
r : ℝ
rp : r > 0
z : ℂ
zr : 1 / r < Complex.abs z
az0 : Complex.abs z ≠ 0
z0 : z ≠ 0
zir : Complex.abs z⁻¹ < r
h : Complex.abs (bottcherNear (s.fl c) d z⁻¹ * z - 1) < e
⊢ Complex.abs (bottcherNear (s.fl c) d z⁻¹ * z - 1) < e