internlm/Lean-Github huggingface dataset:
Theorem: tendsto_f'_atInf
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
zz : Complex.abs z ≤ Complex.abs (z ^ d)
⊢ Complex.abs (z ^ d + (c + (e - c))) ≥ Complex.abs (z ^ d) - Complex.abs (c + (e - c))
Tactic:
bound
Proof state after:
no goals
Theorem: tendsto_f'_atInf
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
zz : Complex.abs z ≤ Complex.abs (z ^ d)
⊢ Complex.abs (z ^ d) - Complex.abs (c + (e - c)) ≥ Complex.abs (z ^ d) - (Complex.abs c + Complex.abs (e - c))
Tactic:
bound
Proof state after:
no goals
Theorem: tendsto_f'_atInf
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
zz : Complex.abs z ≤ Complex.abs (z ^ d)
⊢ Complex.abs (z ^ d) - (Complex.abs c + Complex.abs (e - c)) ≥ Complex.abs z - (Complex.abs c + 1)
Tactic:
bound
Proof state after:
no goals
Theorem: tendsto_f'_atInf
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
zz : Complex.abs z ≤ Complex.abs (z ^ d)
⊢ Complex.abs z - (Complex.abs c + 1) > max r 0 + Complex.abs c + 1 - (Complex.abs c + 1)
Tactic:
bound
Proof state after:
no goals
Theorem: tendsto_f'_atInf
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
r : ℝ
e : ℂ
ec : Complex.abs (e - c) < 1
z : ℂ
h : max r 0 + Complex.abs c + 1 < Complex.abs z
zz : Complex.abs z ≤ Complex.abs (z ^ d)
⊢ max r 0 + Complex.abs c + 1 - (Complex.abs c + 1) = max r 0
Tactic:
ring_nf
Proof state after:
no goals
Theorem: writtenInExtChartAt_coe_f
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ writtenInExtChartAt I I (↑z) (f d c) = f' d c
Tactic:
simp only [writtenInExtChartAt, f, Function.comp, lift_coe', RiemannSphere.extChartAt_coe,
  PartialEquiv.symm_symm, coePartialEquiv_apply, coePartialEquiv_symm_apply, toComplex_coe]
Proof state after:
no goals
Theorem: fl_f
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ fl (f d) ∞ = fun c z => z ^ d / (1 + c * z ^ d)
Tactic:
funext c z
Proof state after:
case h.h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
⊢ fl (f d) ∞ c z = z ^ d / (1 + c * z ^ d)
Theorem: fl_f
Proof state before:
case h.h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
⊢ fl (f d) ∞ c z = z ^ d / (1 + c * z ^ d)
Tactic:
simp only [fl, RiemannSphere.extChartAt_inf, Function.comp, invEquiv_apply,
  PartialEquiv.trans_apply, Equiv.toPartialEquiv_apply, PartialEquiv.coe_trans_symm,
  coePartialEquiv_symm_apply, PartialEquiv.symm_symm, coePartialEquiv_apply,
  Equiv.toPartialEquiv_symm_apply, invEquiv_symm, RiemannSphere.inv_inf, toComplex_zero,
  add_zero, sub_zero]
Proof state after:
case h.h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
⊢ (f d c (↑z)⁻¹)⁻¹.toComplex = z ^ d / (1 + c * z ^ d)
Theorem: fl_f
Proof state before:
case h.h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
⊢ (f d c (↑z)⁻¹)⁻¹.toComplex = z ^ d / (1 + c * z ^ d)
Tactic:
by_cases z0 : z = 0
Proof state after:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : z = 0
⊢ (f d c (↑z)⁻¹)⁻¹.toComplex = z ^ d / (1 + c * z ^ d)

case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
⊢ (f d c (↑z)⁻¹)⁻¹.toComplex = z ^ d / (1 + c * z ^ d)
Theorem: fl_f
Proof state before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
⊢ (f d c (↑z)⁻¹)⁻¹.toComplex = z ^ d / (1 + c * z ^ d)
Tactic:
simp only [f, f', inv_coe z0, lift_coe', inv_pow]
Proof state after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
⊢ (↑((z ^ d)⁻¹ + c))⁻¹.toComplex = z ^ d / (1 + c * z ^ d)
Theorem: fl_f
Proof state before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
⊢ (↑((z ^ d)⁻¹ + c))⁻¹.toComplex = z ^ d / (1 + c * z ^ d)
Tactic:
have zd := pow_ne_zero d z0
Proof state after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
⊢ (↑((z ^ d)⁻¹ + c))⁻¹.toComplex = z ^ d / (1 + c * z ^ d)
Theorem: fl_f
Proof state before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
⊢ (↑((z ^ d)⁻¹ + c))⁻¹.toComplex = z ^ d / (1 + c * z ^ d)
Tactic:
by_cases h : (z ^ d)⁻¹ + c = 0
Proof state after:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : (z ^ d)⁻¹ + c = 0
⊢ (↑((z ^ d)⁻¹ + c))⁻¹.toComplex = z ^ d / (1 + c * z ^ d)

case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : ¬(z ^ d)⁻¹ + c = 0
⊢ (↑((z ^ d)⁻¹ + c))⁻¹.toComplex = z ^ d / (1 + c * z ^ d)
Theorem: fl_f
Proof state before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : ¬(z ^ d)⁻¹ + c = 0
⊢ (↑((z ^ d)⁻¹ + c))⁻¹.toComplex = z ^ d / (1 + c * z ^ d)
Tactic:
rw [inv_coe h, toComplex_coe, eq_div_iff, inv_mul_eq_iff_eq_mul₀ h, right_distrib,
  inv_mul_cancel zd]
Proof state after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : ¬(z ^ d)⁻¹ + c = 0
⊢ 1 + c * z ^ d ≠ 0
Theorem: fl_f
Proof state before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : ¬(z ^ d)⁻¹ + c = 0
⊢ 1 + c * z ^ d ≠ 0
Tactic:
contrapose h
Proof state after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : ¬1 + c * z ^ d ≠ 0
⊢ ¬¬(z ^ d)⁻¹ + c = 0
Theorem: fl_f
Proof state before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : ¬1 + c * z ^ d ≠ 0
⊢ ¬¬(z ^ d)⁻¹ + c = 0
Tactic:
rw [not_not]
Proof state after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : ¬1 + c * z ^ d ≠ 0
⊢ (z ^ d)⁻¹ + c = 0
Theorem: fl_f
Proof state before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : ¬1 + c * z ^ d ≠ 0
⊢ (z ^ d)⁻¹ + c = 0
Tactic:
rw [not_not, add_comm, add_eq_zero_iff_eq_neg, ← eq_div_iff zd, neg_div, ←
  inv_eq_one_div, ← add_eq_zero_iff_eq_neg, add_comm] at h
Proof state after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : (z ^ d)⁻¹ + c = 0
⊢ (z ^ d)⁻¹ + c = 0
Theorem: fl_f
Proof state before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : (z ^ d)⁻¹ + c = 0
⊢ (z ^ d)⁻¹ + c = 0
Tactic:
exact h
Proof state after:
no goals
Theorem: fl_f
Proof state before:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : z = 0
⊢ (f d c (↑z)⁻¹)⁻¹.toComplex = z ^ d / (1 + c * z ^ d)
Tactic:
simp only [z0, coe_zero, inv_zero', f, lift_inf', RiemannSphere.inv_inf, toComplex_zero,
  zero_pow (d_ne_zero _), zero_div]
Proof state after:
no goals
Theorem: fl_f
Proof state before:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : (z ^ d)⁻¹ + c = 0
⊢ (↑((z ^ d)⁻¹ + c))⁻¹.toComplex = z ^ d / (1 + c * z ^ d)
Tactic:
simp only [h, coe_zero, inv_zero', toComplex_inf]
Proof state after:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : (z ^ d)⁻¹ + c = 0
⊢ 0 = z ^ d / (1 + c * z ^ d)
Theorem: fl_f
Proof state before:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z0 : ¬z = 0
zd : z ^ d ≠ 0
h : (z ^ d)⁻¹ + c = 0
⊢ 0 = z ^ d / (1 + c * z ^ d)
Tactic:
simp only [← add_eq_zero_iff_neg_eq.mp h, neg_mul, inv_mul_cancel zd, ← sub_eq_add_neg,
  sub_self, div_zero]
Proof state after:
no goals
Theorem: gl_f
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ g (fl (f d) ∞ c) d z = gl d c z
Tactic:
simp only [fl_f, gl, g]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ (if z = 0 then 1 else z ^ d / (1 + c * z ^ d) / z ^ d) = (1 + c * z ^ d)⁻¹
Theorem: gl_f
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ (if z = 0 then 1 else z ^ d / (1 + c * z ^ d) / z ^ d) = (1 + c * z ^ d)⁻¹
Tactic:
by_cases z0 : z = 0
Proof state after:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z0 : z = 0
⊢ (if z = 0 then 1 else z ^ d / (1 + c * z ^ d) / z ^ d) = (1 + c * z ^ d)⁻¹

case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z0 : ¬z = 0
⊢ (if z = 0 then 1 else z ^ d / (1 + c * z ^ d) / z ^ d) = (1 + c * z ^ d)⁻¹
Theorem: gl_f
Proof state before:
case pos
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z0 : z = 0
⊢ (if z = 0 then 1 else z ^ d / (1 + c * z ^ d) / z ^ d) = (1 + c * z ^ d)⁻¹

case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z0 : ¬z = 0
⊢ (if z = 0 then 1 else z ^ d / (1 + c * z ^ d) / z ^ d) = (1 + c * z ^ d)⁻¹
Tactic:
simp only [if_pos, z0, zero_pow (d_ne_zero _), MulZeroClass.mul_zero, add_zero, inv_one]
Proof state after:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z0 : ¬z = 0
⊢ (if z = 0 then 1 else z ^ d / (1 + c * z ^ d) / z ^ d) = (1 + c * z ^ d)⁻¹
Theorem: gl_f
Proof state before:
case neg
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z0 : ¬z = 0
⊢ (if z = 0 then 1 else z ^ d / (1 + c * z ^ d) / z ^ d) = (1 + c * z ^ d)⁻¹
Tactic:
rw [if_neg z0, div_eq_mul_inv _ (_ + _), mul_comm, mul_div_assoc, div_self (pow_ne_zero _ z0),
  mul_one]
Proof state after:
no goals
Theorem: analyticAt_gl
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ AnalyticAt ℂ (gl d c) 0
Tactic:
apply (analyticAt_const.add (analyticAt_const.mul ((analyticAt_id _ _).pow _))).inv
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ((fun x => 1) + fun x => c * id x ^ d) 0 ≠ 0
Theorem: analyticAt_gl
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ((fun x => 1) + fun x => c * id x ^ d) 0 ≠ 0
Tactic:
simp only [Pi.pow_apply, id_eq, Pi.add_apply, ne_eq, zero_pow (d_ne_zero _), mul_zero, add_zero,
  one_ne_zero, not_false_eq_true]
Proof state after:
no goals
Theorem: fl_f'
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ fl (f d) ∞ = fun c z => (z - 0) ^ d • gl d c z
Tactic:
funext c z
Proof state after:
case h.h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
⊢ fl (f d) ∞ c z = (z - 0) ^ d • gl d c z
Theorem: fl_f'
Proof state before:
case h.h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
⊢ fl (f d) ∞ c z = (z - 0) ^ d • gl d c z
Tactic:
simp only [fl_f, gl, sub_zero, Algebra.id.smul_eq_mul, div_eq_mul_inv]
Proof state after:
no goals
Theorem: gl_zero
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ gl d c 0 = 1
Tactic:
simp only [gl, zero_pow (d_ne_zero _), MulZeroClass.mul_zero]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ (1 + 0)⁻¹ = 1
Theorem: gl_zero
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ (1 + 0)⁻¹ = 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: gl_frequently_ne_zero
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∃ᶠ (z : ℂ) in 𝓝 0, gl d c z ≠ 0
Tactic:
refine (analyticAt_gl.continuousAt.eventually_ne ?_).frequently
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ gl d c 0 ≠ 0
Theorem: gl_frequently_ne_zero
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ gl d c 0 ≠ 0
Tactic:
simp only [gl_zero]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 1 ≠ 0
Theorem: gl_frequently_ne_zero
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 1 ≠ 0
Tactic:
exact one_ne_zero
Proof state after:
no goals
Theorem: fc_f
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ leadingCoeff (fl (f d) ∞ c) 0 = 1
Tactic:
rw [fl_f', analyticAt_gl.monomial_mul_leadingCoeff gl_frequently_ne_zero, leadingCoeff_of_ne_zero]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ gl d c 0 = 1

c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ gl d c 0 ≠ 0
Theorem: fc_f
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ gl d c 0 = 1

c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ gl d c 0 ≠ 0
Tactic:
exact gl_zero
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ gl d c 0 ≠ 0
Theorem: fc_f
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ gl d c 0 ≠ 0
Tactic:
rw [gl_zero]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 1 ≠ 0
Theorem: fc_f
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 1 ≠ 0
Tactic:
exact one_ne_zero
Proof state after:
no goals
Theorem: fd_f
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ orderAt (fl (f d) ∞ c) 0 = d
Tactic:
rw [fl_f', analyticAt_gl.monomial_mul_orderAt gl_frequently_ne_zero, orderAt_eq_zero, add_zero]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ gl d c 0 ≠ 0
Theorem: fd_f
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ gl d c 0 ≠ 0
Tactic:
rw [gl_zero]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 1 ≠ 0
Theorem: fd_f
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 1 ≠ 0
Tactic:
exact one_ne_zero
Proof state after:
no goals
Theorem: f_inf
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ f d c ∞ = ∞
Tactic:
simp only [f, f', lift_inf', eq_self_iff_true, imp_true_iff]
Proof state after:
no goals
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ SuperNear (fl (f d) ∞ c) d {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
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
⊢ SuperNear (fl (f d) ∞ c) d {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
⊢ SuperNear (fl (f d) ∞ c) d {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
Tactic:
generalize ht : {z : ℂ | abs z < (max 16 (abs c / 2))⁻¹} = t
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
⊢ SuperNear (fl (f d) ∞ c) d t
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
⊢ SuperNear (fl (f d) ∞ c) d t
Tactic:
have cz : ∀ {z}, z ∈ t → abs (c * z ^ d) ≤ 1 / 8 := by
  intro z m; simp only [← ht, mem_setOf] at m
  simp only [Complex.abs.map_mul, Complex.abs.map_pow]
  trans abs c * (max 16 (abs c / 2))⁻¹ ^ d; bound
  rw [inv_pow, mul_inv_le_iff]; swap; bound
  rw [mul_one_div]; rw [le_div_iff, mul_comm]; swap; norm_num
  refine le_trans ?_ (pow_le_pow_right (le_max_of_le_left (by norm_num)) (two_le_d d))
  by_cases cb : abs c / 2 ≤ 16
  rw [max_eq_left cb, pow_two]; linarith
  rw [max_eq_right (not_le.mp cb).le, pow_two]; nlinarith
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
⊢ SuperNear (fl (f d) ∞ c) d t
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
⊢ SuperNear (fl (f d) ∞ c) d t
Tactic:
have cz1 : ∀ {z}, z ∈ t → 7 / 8 ≤ abs (1 + c * z ^ d) := by
  intro z m
  calc abs (1 + c * z ^ d)
    _ ≥ Complex.abs 1 - abs (c * z ^ d) := by bound
    _ ≥ Complex.abs 1 - 1 / 8 := by linarith [cz m]
    _ = 7 / 8 := by norm_num
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
⊢ SuperNear (fl (f d) ∞ c) d t
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
⊢ SuperNear (fl (f d) ∞ c) d t
Tactic:
have zb : ∀ {z}, z ∈ t → abs z ≤ 1 / 8 := by
  intro z m; rw [← ht] at m; refine le_trans (le_of_lt m) ?_
  rw [one_div]; exact inv_le_inv_of_le (by norm_num) (le_trans (by norm_num) (le_max_left _ _))
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
⊢ SuperNear (fl (f d) ∞ c) d t
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
cz : ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
cz1 : ∀ {z : ℂ}, z ∈ t → 7 / 8 ≤ Complex.abs (1 + c * z ^ d)
zb : ∀ {z : ℂ}, z ∈ t → Complex.abs z ≤ 1 / 8
⊢ SuperNear (fl (f d) ∞ c) d t
Tactic:
exact
  { d2 := two_le_d d
    fa0 := (s.fla c).along_snd
    fd := fd_f
    fc := fc_f
    o := by rw [← ht]; exact isOpen_lt Complex.continuous_abs continuous_const
    t0 := by simp only [← ht, mem_setOf, Complex.abs.map_zero]; bound
    t2 := fun {z} m ↦ le_trans (zb m) (by norm_num)
    fa := by
      intro z m; rw [fl_f]
      refine ((analyticAt_id _ _).pow _).div (analyticAt_const.add
        (analyticAt_const.mul ((analyticAt_id _ _).pow _))) ?_
      rw [← Complex.abs.ne_zero_iff]; exact (lt_of_lt_of_le (by norm_num) (cz1 m)).ne'
    ft := by
      intro z m; specialize cz1 m; specialize zb m
      simp only [fl_f, mem_setOf, map_div₀, Complex.abs.map_pow, ← ht] at m ⊢
      refine lt_of_le_of_lt ?_ m; rw [div_le_iff (lt_of_lt_of_le (by norm_num) cz1)]
      refine le_trans (pow_le_pow_of_le_one (Complex.abs.nonneg _)
        (le_trans zb (by norm_num)) (two_le_d d)) ?_
      rw [pow_two]; refine mul_le_mul_of_nonneg_left ?_ (Complex.abs.nonneg _)
      exact le_trans zb (le_trans (by norm_num) cz1)
    gs' := by
      intro z z0 m; simp only [fl_f, div_div_cancel_left' (pow_ne_zero d z0)]
      specialize cz1 m
      have czp : 0 < abs (1 + c * z ^ d) := lt_of_lt_of_le (by norm_num) cz1
      refine le_of_mul_le_mul_right ?_ czp
      rw [← Complex.abs.map_mul, mul_sub_right_distrib, one_mul,
        inv_mul_cancel (Complex.abs.ne_zero_iff.mp czp.ne'), ← sub_sub, sub_self, zero_sub,
        Complex.abs.map_neg]
      exact le_trans (cz m) (le_trans (by norm_num)
        (mul_le_mul_of_nonneg_left cz1 (by norm_num))) }
Proof state after:
no goals
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
⊢ ∀ {z : ℂ}, z ∈ t → Complex.abs (c * z ^ d) ≤ 1 / 8
Tactic:
intro z m
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : z ∈ t
⊢ Complex.abs (c * z ^ d) ≤ 1 / 8
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : z ∈ t
⊢ Complex.abs (c * z ^ d) ≤ 1 / 8
Tactic:
simp only [← ht, mem_setOf] at m
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs (c * z ^ d) ≤ 1 / 8
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs (c * z ^ d) ≤ 1 / 8
Tactic:
simp only [Complex.abs.map_mul, Complex.abs.map_pow]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c * Complex.abs z ^ d ≤ 1 / 8
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c * Complex.abs z ^ d ≤ 1 / 8
Tactic:
trans abs c * (max 16 (abs c / 2))⁻¹ ^ d
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c * Complex.abs z ^ d ≤ Complex.abs c * (max 16 (Complex.abs c / 2))⁻¹ ^ d

c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c * (max 16 (Complex.abs c / 2))⁻¹ ^ d ≤ 1 / 8
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c * Complex.abs z ^ d ≤ Complex.abs c * (max 16 (Complex.abs c / 2))⁻¹ ^ d

c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c * (max 16 (Complex.abs c / 2))⁻¹ ^ d ≤ 1 / 8
Tactic:
bound
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c * (max 16 (Complex.abs c / 2))⁻¹ ^ d ≤ 1 / 8
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c * (max 16 (Complex.abs c / 2))⁻¹ ^ d ≤ 1 / 8
Tactic:
rw [inv_pow, mul_inv_le_iff]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d * (1 / 8)

c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 0 < max 16 (Complex.abs c / 2) ^ d
Theorem: superNearF
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d * (1 / 8)

c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 0 < max 16 (Complex.abs c / 2) ^ d
Tactic:
swap
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ 0 < max 16 (Complex.abs c / 2) ^ d

c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
s : Super (f d) d ∞ := superF d
t : Set ℂ
ht : {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹} = t
z : ℂ
m : Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
⊢ Complex.abs c ≤ max 16 (Complex.abs c / 2) ^ d * (1 / 8)