Theorem: bottcher_large_approx (Ray/Dynamics/Multibrot/Basic.lean)

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
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)

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
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)

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]
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)

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
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)

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))
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)

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
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)

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]
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) < ε

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
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

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⟩
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

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
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

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
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

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'
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

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
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

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
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

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
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

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
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

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]
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

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 (bottcherNear (s.fl c) d z⁻¹ * z - 1) < e
Tactic:
exact h
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ ∀ᶠ (z : ℂ) in atInf, s.bottcher c ↑z * z = s.bottcherNear c ↑z * z
Tactic:
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])
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ ∀ᶠ (z : ℂ) in atInf, s.bottcher c ↑z = s.bottcherNear c ↑z

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ ∀ᶠ (z : ℂ) in atInf, s.bottcher c ↑z = s.bottcherNear c ↑z
Tactic:
refine coe_tendsto_inf.eventually (p := fun z ↦ s.bottcher c z = s.bottcherNear c z) ?_
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ ∀ᶠ (y : 𝕊) in 𝓝 ∞, (fun z => s.bottcher c z = s.bottcherNear c z) y

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ ∀ᶠ (y : 𝕊) in 𝓝 ∞, (fun z => s.bottcher c z = s.bottcherNear c z) y
Tactic:
apply s.bottcher_eq_bottcherNear
State after:
no goals

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 = s.bottcherNear c ↑z
⊢ ∀ᶠ (z : ℂ) in atInf, s.bottcher c ↑z * z = s.bottcherNear c ↑z * z
Tactic:
exact e.mp (eventually_of_forall fun z e ↦ by rw [e])
State after:
no goals

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 = s.bottcherNear c ↑z
z : ℂ
e : s.bottcher c ↑z = s.bottcherNear c ↑z
⊢ s.bottcher c ↑z * z = s.bottcherNear c ↑z * z
Tactic:
rw [e]
State after:
no goals

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
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 z⁻¹ < r
Tactic:
simp only [one_div, map_inv₀] at zr ⊢
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
r : ℝ
rp : r > 0
h : ∀ {x : ℂ}, Complex.abs x < r → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < e
z : ℂ
az0 : Complex.abs z ≠ 0
z0 : z ≠ 0
zr : r⁻¹ < Complex.abs z
⊢ (Complex.abs z)⁻¹ < r

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
r : ℝ
rp : r > 0
h : ∀ {x : ℂ}, Complex.abs x < r → (Complex.abs x)⁻¹ * Complex.abs (bottcherNear (s.fl c) d x - x) < e
z : ℂ
az0 : Complex.abs z ≠ 0
z0 : z ≠ 0
zr : r⁻¹ < Complex.abs z
⊢ (Complex.abs z)⁻¹ < r
Tactic:
exact inv_lt_of_inv_lt rp zr
State after:
no goals