internlm/Lean-Github huggingface dataset:
Theorem: Super.has_ray
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
e x : ℂ
et0 : e ∈ t0
et1 : e ∈ t1
xq : x ∈ ball 0 q
⊢ ray e x = r h e x
Tactic:
simp only [mem_ball, Complex.dist_eq, sub_zero] at xq
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
e x : ℂ
et0 : e ∈ t0
et1 : e ∈ t1
xq : Complex.abs x < q
⊢ ray e x = r h e x
Theorem: Super.has_ray
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
e x : ℂ
et0 : e ∈ t0
et1 : e ∈ t1
xq : Complex.abs x < q
⊢ ray e x = r h e x
Tactic:
have hx : 0 ≤ abs x ∧ abs x < s.p e := ⟨Complex.abs.nonneg _, _root_.trans xq (lo _ et1)⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
e x : ℂ
et0 : e ∈ t0
et1 : e ∈ t1
xq : Complex.abs x < q
hx : 0 ≤ Complex.abs x ∧ Complex.abs x < s.p e
⊢ ray e x = r h e x
Theorem: Super.has_ray
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
e x : ℂ
et0 : e ∈ t0
et1 : e ∈ t1
xq : Complex.abs x < q
hx : 0 ≤ Complex.abs x ∧ Complex.abs x < s.p e
⊢ ray e x = r h e x
Tactic:
simp only [← hray, dif_pos hx.2]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
e x : ℂ
et0 : e ∈ t0
et1 : e ∈ t1
xq : Complex.abs x < q
hx : 0 ≤ Complex.abs x ∧ Complex.abs x < s.p e
⊢ r ⋯ e x = r h e x
Theorem: Super.has_ray
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
e x : ℂ
et0 : e ∈ t0
et1 : e ∈ t1
xq : Complex.abs x < q
hx : 0 ≤ Complex.abs x ∧ Complex.abs x < s.p e
⊢ r ⋯ e x = r h e x
Tactic:
refine ((g hx).unique (gh _ et0) xq.le).self_of_nhdsSet (x := ⟨e, x⟩) ⟨rfl, ?_⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
e x : ℂ
et0 : e ∈ t0
et1 : e ∈ t1
xq : Complex.abs x < q
hx : 0 ≤ Complex.abs x ∧ Complex.abs x < s.p e
⊢ (e, x).2 ∈ closedBall 0 (Complex.abs x)
Theorem: Super.has_ray
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z : S
d n : ℕ
p✝ : ℝ
s✝ : Super f d a
r✝ : ℂ → ℂ → S
s : Super f d a
inst✝ : OnePreimage s
r : {c : ℂ} → {p : ℝ} → 0 ≤ p ∧ p < s.p c → ℂ → ℂ → S
g : ∀ {c : ℂ} {p : ℝ} (h : 0 ≤ p ∧ p < s.p c), Grow s c p (s.np c p) (r h)
ray : ℂ → ℂ → S
hray : (fun c x => if h : Complex.abs x < s.p c then r ⋯ c x else a) = ray
c : ℂ
p : ℝ
h : 0 ≤ p ∧ p < s.p c
q : ℝ
pq : p < q
qs : q < s.p c
q0 : 0 ≤ q
gh✝ : ∀ᶠ (x : ℂ) in 𝓝 c, Grow s x q (s.np c p) (r h)
t0 : Set ℂ
gh : ∀ x ∈ t0, Grow s x q (s.np c p) (r h)
ot0 : IsOpen t0
ct0 : c ∈ t0
t1 : Set ℂ
lo : ∀ x ∈ t1, q < s.p x
ot1 : IsOpen t1
ct1 : c ∈ t1
e x : ℂ
et0 : e ∈ t0
et1 : e ∈ t1
xq : Complex.abs x < q
hx : 0 ≤ Complex.abs x ∧ Complex.abs x < s.p e
⊢ (e, x).2 ∈ closedBall 0 (Complex.abs x)
Tactic:
simp only [mem_closedBall, Complex.dist_eq, sub_zero, le_refl]
Proof state after:
no goals
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
⊢ ⋯.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹
Tactic:
have c0 : 0 < abs c := lt_trans (by norm_num) c16
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
⊢ ⋯.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
⊢ ⋯.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹
Tactic:
have z0 : 0 < abs z := lt_of_lt_of_le c0 cz
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
⊢ ⋯.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
⊢ ⋯.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹
Tactic:
set s := superF d
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ s.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ s.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹
Tactic:
set t := closedBall (0 : ℂ) (abs c)⁻¹
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
⊢ s.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
⊢ s.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹
Tactic:
suffices e : EqOn (fun z : ℂ ↦ s.bottcher c (z : 𝕊)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t by
  have z0' : z ≠ 0 := Complex.abs.ne_zero_iff.mp z0.ne'
  convert @e z⁻¹ _; rw [inv_coe (inv_ne_zero z0'), inv_inv]
  simp only [mem_closedBall, Complex.dist_eq, sub_zero, map_inv₀, inv_le_inv z0 c0, cz, t]
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
⊢ EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
⊢ EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
Tactic:
have a0 : HolomorphicOn I I (fun z : ℂ ↦ s.bottcher c (z : 𝕊)⁻¹) t := by
  intro z m
  refine (s.bottcher_holomorphicOn _ ?_).along_snd.comp (holomorphic_inv.comp holomorphic_coe _)
  simp only [mem_closedBall, Complex.dist_eq, sub_zero, t] at m
  by_cases z0 : z = 0; simp only [z0, coe_zero, inv_zero']; exact s.post_a c
  rw [inv_coe z0]; refine postcritical_large (by linarith) ?_
  rwa [map_inv₀, le_inv c0]; exact Complex.abs.pos z0
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
⊢ EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
⊢ EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
Tactic:
have a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t := by
  intro z m; apply AnalyticAt.holomorphicAt
  apply bottcherNear_analytic_z (superNearF d c)
  simp only [mem_setOf, mem_closedBall, Complex.dist_eq, sub_zero, t] at m ⊢
  refine lt_of_le_of_lt m ?_
  refine inv_lt_inv_of_lt (lt_of_lt_of_le (by norm_num) (le_max_left _ _)) ?_
  exact max_lt c16 (half_lt_self (lt_trans (by norm_num) c16))
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
⊢ EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
⊢ EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
Tactic:
refine (a0.eq_of_locally_eq a1 (convex_closedBall _ _).isPreconnected ?_).self_of_nhdsSet
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
⊢ ∃ x ∈ t, (𝓝 x).EventuallyEq (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d)
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
⊢ ∃ x ∈ t, (𝓝 x).EventuallyEq (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d)
Tactic:
use 0, mem_closedBall_self (by bound)
Proof state after:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
⊢ (𝓝 0).EventuallyEq (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d)
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
⊢ (𝓝 0).EventuallyEq (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d)
Tactic:
have e : ∀ᶠ z in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (z : 𝕊)⁻¹ := by
  simp only [Super.bottcherNear, extChartAt_inf_apply, inv_inv, toComplex_coe,
    RiemannSphere.inv_inf, toComplex_zero, sub_zero, Super.fl, eq_self_iff_true,
    Filter.eventually_true]
Proof state after:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
e : ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
⊢ (𝓝 0).EventuallyEq (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d)
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
e : ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
⊢ (𝓝 0).EventuallyEq (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d)
Tactic:
refine Filter.EventuallyEq.trans ?_ (Filter.EventuallyEq.symm e)
Proof state after:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
e : ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
⊢ (𝓝 0).EventuallyEq (fun z => s.bottcher c (↑z)⁻¹) fun x => s.bottcherNear c (↑x)⁻¹
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
e : ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
⊢ (𝓝 0).EventuallyEq (fun z => s.bottcher c (↑z)⁻¹) fun x => s.bottcherNear c (↑x)⁻¹
Tactic:
have i : Tendsto (fun z : ℂ ↦ (z : 𝕊)⁻¹) (𝓝 0) (𝓝 ∞) := by
  have h : ContinuousAt (fun z : ℂ ↦ (z : 𝕊)⁻¹) 0 :=
    (RiemannSphere.continuous_inv.comp continuous_coe).continuousAt
  simp only [ContinuousAt, coe_zero, inv_zero'] at h; exact h
Proof state after:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
e : ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
i : Tendsto (fun z => (↑z)⁻¹) (𝓝 0) (𝓝 ∞)
⊢ (𝓝 0).EventuallyEq (fun z => s.bottcher c (↑z)⁻¹) fun x => s.bottcherNear c (↑x)⁻¹
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
e : ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
i : Tendsto (fun z => (↑z)⁻¹) (𝓝 0) (𝓝 ∞)
⊢ (𝓝 0).EventuallyEq (fun z => s.bottcher c (↑z)⁻¹) fun x => s.bottcherNear c (↑x)⁻¹
Tactic:
exact i.eventually (s.bottcher_eq_bottcherNear c)
Proof state after:
no goals
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
⊢ 0 < 16
Tactic:
norm_num
Proof state after:
no goals
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
e : EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
⊢ s.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹
Tactic:
have z0' : z ≠ 0 := Complex.abs.ne_zero_iff.mp z0.ne'
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
e : EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
z0' : z ≠ 0
⊢ s.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
e : EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
z0' : z ≠ 0
⊢ s.bottcher c ↑z = bottcherNear (fl (f d) ∞ c) d z⁻¹
Tactic:
convert @e z⁻¹ _
Proof state after:
case h.e'_2.h.e'_13
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
e : EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
z0' : z ≠ 0
⊢ ↑z = (↑z⁻¹)⁻¹

c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
e : EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
z0' : z ≠ 0
⊢ z⁻¹ ∈ t