internlm/Lean-Github huggingface dataset:
Theorem: SuperAt.super_on_ball
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
z0 : z ≠ 0
zs : Complex.abs z < r
⊢ Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
Tactic:
specialize gs zs
Proof state after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
z : ℂ
z0 : z ≠ 0
zs : Complex.abs z < r
gs : Complex.abs (g f d z - 1) < 1 / 4
⊢ Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
Theorem: SuperAt.super_on_ball
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
z : ℂ
z0 : z ≠ 0
zs : Complex.abs z < r
gs : Complex.abs (g f d z - 1) < 1 / 4
⊢ Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
Tactic:
simp only [g, z0, if_false, eq_self_iff_true, if_true] at gs
Proof state after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
z : ℂ
z0 : z ≠ 0
zs : Complex.abs z < r
gs : Complex.abs (f z / z ^ d - 1) < 1 / 4
⊢ Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
Theorem: SuperAt.super_on_ball
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
z : ℂ
z0 : z ≠ 0
zs : Complex.abs z < r
gs : Complex.abs (f z / z ^ d - 1) < 1 / 4
⊢ Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
Tactic:
exact gs.le
Proof state after:
no goals
Theorem: SuperAt.super_on_ball
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
gs : ∀ {z : ℂ}, z ≠ 0 → z ∈ ball 0 r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
⊢ ∀ {z : ℂ}, z ∈ ball 0 r → Complex.abs z ≤ 1 / 2
Tactic:
intro z zs
Proof state after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
gs : ∀ {z : ℂ}, z ≠ 0 → z ∈ ball 0 r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z : ℂ
zs : z ∈ ball 0 r
⊢ Complex.abs z ≤ 1 / 2
Theorem: SuperAt.super_on_ball
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
gs : ∀ {z : ℂ}, z ≠ 0 → z ∈ ball 0 r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z : ℂ
zs : z ∈ ball 0 r
⊢ Complex.abs z ≤ 1 / 2
Tactic:
simp only [mem_ball_zero_iff, Complex.norm_eq_abs] at zs
Proof state after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
gs : ∀ {z : ℂ}, z ≠ 0 → z ∈ ball 0 r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z : ℂ
zs : Complex.abs z < r
⊢ Complex.abs z ≤ 1 / 2
Theorem: SuperAt.super_on_ball
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
gs : ∀ {z : ℂ}, z ≠ 0 → z ∈ ball 0 r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z : ℂ
zs : Complex.abs z < r
⊢ Complex.abs z ≤ 1 / 2
Tactic:
exact le_trans zs.le r2
Proof state after:
no goals
Theorem: SuperAt.super_on_ball
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
gs : ∀ {z : ℂ}, z ≠ 0 → z ∈ ball 0 r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
⊢ MapsTo f (ball 0 r) (ball 0 r)
Tactic:
intro z zs
Proof state after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
gs : ∀ {z : ℂ}, z ≠ 0 → z ∈ ball 0 r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z : ℂ
zs : z ∈ ball 0 r
⊢ f z ∈ ball 0 r
Theorem: SuperAt.super_on_ball
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
gs : ∀ {z : ℂ}, z ≠ 0 → z ∈ ball 0 r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z : ℂ
zs : z ∈ ball 0 r
⊢ f z ∈ ball 0 r
Tactic:
simp only [mem_ball_zero_iff, Complex.norm_eq_abs] at zs gs ⊢
Proof state after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
⊢ Complex.abs (f z) < r
Theorem: SuperAt.super_on_ball
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
⊢ Complex.abs (f z) < r
Tactic:
by_cases z0 : z = 0
Proof state after:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : z = 0
⊢ Complex.abs (f z) < r

case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ Complex.abs (f z) < r
Theorem: SuperAt.super_on_ball
Proof state before:
case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ Complex.abs (f z) < r
Tactic:
calc abs (f z)
  _ = abs (f z / z ^ d * z ^ d) := by rw [div_mul_cancel₀ _ (pow_ne_zero d z0)]
  _ = abs (f z / z ^ d - 1 + 1) * abs z ^ d := by
    simp only [AbsoluteValue.map_mul, Complex.abs_pow, sub_add_cancel]
  _ ≤ (abs (f z / z ^ d - 1) + abs (1 : ℂ)) * r ^ d := by bound
  _ ≤ (1 / 4 + abs (1 : ℂ)) * r ^ d := by bound [gs z0 zs]
  _ ≤ 5 / 4 * r ^ (d - 1) * r := by
    rw [mul_assoc, ← pow_succ, Nat.sub_add_cancel (le_trans one_le_two s.d2)]; norm_num
  _ ≤ 5 / 4 * (1 / 2 : ℝ) ^ (d - 1) * r := by bound
  _ ≤ 5 / 4 * (1 / 2 : ℝ) ^ (2 - 1) * r := by bound
  _ = 5 / 8 * r := by norm_num
  _ < r := by linarith
Proof state after:
no goals
Theorem: SuperAt.super_on_ball
Proof state before:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : z = 0
⊢ Complex.abs (f z) < r
Tactic:
simp only [z0, s.f0, rp, AbsoluteValue.map_zero]
Proof state after:
no goals
Theorem: SuperAt.super_on_ball
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ Complex.abs (f z) = Complex.abs (f z / z ^ d * z ^ d)
Tactic:
rw [div_mul_cancel₀ _ (pow_ne_zero d z0)]
Proof state after:
no goals
Theorem: SuperAt.super_on_ball
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ Complex.abs (f z / z ^ d * z ^ d) = Complex.abs (f z / z ^ d - 1 + 1) * Complex.abs z ^ d
Tactic:
simp only [AbsoluteValue.map_mul, Complex.abs_pow, sub_add_cancel]
Proof state after:
no goals
Theorem: SuperAt.super_on_ball
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ Complex.abs (f z / z ^ d - 1 + 1) * Complex.abs z ^ d ≤ (Complex.abs (f z / z ^ d - 1) + Complex.abs 1) * r ^ d
Tactic:
bound
Proof state after:
no goals
Theorem: SuperAt.super_on_ball
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ (Complex.abs (f z / z ^ d - 1) + Complex.abs 1) * r ^ d ≤ (1 / 4 + Complex.abs 1) * r ^ d
Tactic:
bound [gs z0 zs]
Proof state after:
no goals
Theorem: SuperAt.super_on_ball
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ (1 / 4 + Complex.abs 1) * r ^ d ≤ 5 / 4 * r ^ (d - 1) * r
Tactic:
rw [mul_assoc, ← pow_succ, Nat.sub_add_cancel (le_trans one_le_two s.d2)]
Proof state after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ (1 / 4 + Complex.abs 1) * r ^ d ≤ 5 / 4 * r ^ d
Theorem: SuperAt.super_on_ball
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ (1 / 4 + Complex.abs 1) * r ^ d ≤ 5 / 4 * r ^ d
Tactic:
norm_num
Proof state after:
no goals
Theorem: SuperAt.super_on_ball
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ 5 / 4 * r ^ (d - 1) * r ≤ 5 / 4 * (1 / 2) ^ (d - 1) * r
Tactic:
bound
Proof state after:
no goals
Theorem: SuperAt.super_on_ball
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ 5 / 4 * (1 / 2) ^ (d - 1) * r ≤ 5 / 4 * (1 / 2) ^ (2 - 1) * r
Tactic:
bound
Proof state after:
no goals
Theorem: SuperAt.super_on_ball
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ 5 / 4 * (1 / 2) ^ (2 - 1) * r = 5 / 8 * r
Tactic:
norm_num
Proof state after:
no goals
Theorem: SuperAt.super_on_ball
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperAt f d
r : ℝ
rp : 0 < r
r2 : r ≤ 1 / 2
fa : AnalyticOn ℂ f (ball 0 r)
gs✝ : ∀ {z : ℂ}, Complex.abs z < r → Complex.abs (g f d z - 1) < 1 / 4
z : ℂ
zs : Complex.abs z < r
gs : ∀ {z : ℂ}, z ≠ 0 → Complex.abs z < r → Complex.abs (f z / z ^ d - 1) ≤ 1 / 4
z0 : ¬z = 0
⊢ 5 / 8 * r < r
Tactic:
linarith
Proof state after:
no goals
Theorem: SuperAt.superNear
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
⊢ ∃ t, SuperNear f d t
Tactic:
rcases s.fa0.exists_ball_analyticOn with ⟨r0, r0p, fa⟩
Proof state after:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
⊢ ∃ t, SuperNear f d t
Theorem: SuperAt.superNear
Proof state before:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
⊢ ∃ t, SuperNear f d t
Tactic:
rcases Metric.continuousAt_iff.mp (s.ga_of_fa (fa 0 (mem_ball_self r0p))).continuousAt (1 / 4)
    (by norm_num) with
  ⟨r1, r1p, gs⟩
Proof state after:
case intro.intro.intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
⊢ ∃ t, SuperNear f d t
Theorem: SuperAt.superNear
Proof state before:
case intro.intro.intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
⊢ ∃ t, SuperNear f d t
Tactic:
set r := min r0 (min r1 (1 / 2))
Proof state after:
case intro.intro.intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
r : ℝ := min r0 (min r1 (1 / 2))
⊢ ∃ t, SuperNear f d t
Theorem: SuperAt.superNear
Proof state before:
case intro.intro.intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
r : ℝ := min r0 (min r1 (1 / 2))
⊢ ∃ t, SuperNear f d t
Tactic:
use ball 0 r
Proof state after:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
r : ℝ := min r0 (min r1 (1 / 2))
⊢ SuperNear f d (ball 0 r)
Theorem: SuperAt.superNear
Proof state before:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
r : ℝ := min r0 (min r1 (1 / 2))
⊢ SuperNear f d (ball 0 r)
Tactic:
have rp : 0 < r := by bound
Proof state after:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
r : ℝ := min r0 (min r1 (1 / 2))
rp : 0 < r
⊢ SuperNear f d (ball 0 r)
Theorem: SuperAt.superNear
Proof state before:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
r : ℝ := min r0 (min r1 (1 / 2))
rp : 0 < r
⊢ SuperNear f d (ball 0 r)
Tactic:
have r2 : r ≤ 1 / 2 := le_trans (min_le_right _ _) (min_le_right _ _)
Proof state after:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
r : ℝ := min r0 (min r1 (1 / 2))
rp : 0 < r
r2 : r ≤ 1 / 2
⊢ SuperNear f d (ball 0 r)
Theorem: SuperAt.superNear
Proof state before:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
r : ℝ := min r0 (min r1 (1 / 2))
rp : 0 < r
r2 : r ≤ 1 / 2
⊢ SuperNear f d (ball 0 r)
Tactic:
have rr1 : r ≤ r1 := le_trans (min_le_right r0 _) (min_le_left r1 _)
Proof state after:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
r : ℝ := min r0 (min r1 (1 / 2))
rp : 0 < r
r2 : r ≤ 1 / 2
rr1 : r ≤ r1
⊢ SuperNear f d (ball 0 r)
Theorem: SuperAt.superNear
Proof state before:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
r : ℝ := min r0 (min r1 (1 / 2))
rp : 0 < r
r2 : r ≤ 1 / 2
rr1 : r ≤ r1
⊢ SuperNear f d (ball 0 r)
Tactic:
simp only [g0, dist_zero_right, Complex.norm_eq_abs, Complex.dist_eq, sub_zero] at gs
Proof state after:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
r : ℝ := min r0 (min r1 (1 / 2))
rp : 0 < r
r2 : r ≤ 1 / 2
rr1 : r ≤ r1
gs : ∀ {x : ℂ}, Complex.abs x < r1 → Complex.abs (g f d x - 1) < 1 / 4
⊢ SuperNear f d (ball 0 r)
Theorem: SuperAt.superNear
Proof state before:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
r : ℝ := min r0 (min r1 (1 / 2))
rp : 0 < r
r2 : r ≤ 1 / 2
rr1 : r ≤ r1
gs : ∀ {x : ℂ}, Complex.abs x < r1 → Complex.abs (g f d x - 1) < 1 / 4
⊢ SuperNear f d (ball 0 r)
Tactic:
exact s.super_on_ball rp r2 (fa.mono (Metric.ball_subset_ball (min_le_left r0 _))) (fun {z} zr ↦
  gs (lt_of_lt_of_le zr rr1))
Proof state after:
no goals
Theorem: SuperAt.superNear
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
⊢ 1 / 4 > 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: SuperAt.superNear
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperAt f d
r0 : ℝ
r0p : 0 < r0
fa : AnalyticOn ℂ f (ball 0 r0)
r1 : ℝ
r1p : r1 > 0
gs : ∀ {x : ℂ}, dist x 0 < r1 → dist (g f d x) (g f d 0) < 1 / 4
r : ℝ := min r0 (min r1 (1 / 2))
⊢ 0 < r
Tactic:
bound
Proof state after:
no goals
Theorem: SuperNear.gs
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
⊢ Complex.abs (g f d z - 1) ≤ 1 / 4
Tactic:
by_cases z0 : z = 0
Proof state after:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
z0 : z = 0
⊢ Complex.abs (g f d z - 1) ≤ 1 / 4

case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
z0 : ¬z = 0
⊢ Complex.abs (g f d z - 1) ≤ 1 / 4
Theorem: SuperNear.gs
Proof state before:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
z0 : z = 0
⊢ Complex.abs (g f d z - 1) ≤ 1 / 4
Tactic:
simp only [z0, g0, sub_self, AbsoluteValue.map_zero, one_div, inv_nonneg, zero_le_bit0,
  zero_le_one]
Proof state after:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
z0 : z = 0
⊢ 0 ≤ 4
Theorem: SuperNear.gs
Proof state before:
case pos
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
z0 : z = 0
⊢ 0 ≤ 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: SuperNear.gs
Proof state before:
case neg
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
z0 : ¬z = 0
⊢ Complex.abs (g f d z - 1) ≤ 1 / 4
Tactic:
simp only [g, z0, if_false, s.gs' z0 zt]
Proof state after:
no goals
Theorem: SuperNear.g_ne_zero
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
⊢ g f d z ≠ 0
Tactic:
have h := s.gs zt
Proof state after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
h : Complex.abs (g f d z - 1) ≤ 1 / 4
⊢ g f d z ≠ 0
Theorem: SuperNear.g_ne_zero
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
h : Complex.abs (g f d z - 1) ≤ 1 / 4
⊢ g f d z ≠ 0
Tactic:
contrapose h
Proof state after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
h : ¬g f d z ≠ 0
⊢ ¬Complex.abs (g f d z - 1) ≤ 1 / 4
Theorem: SuperNear.g_ne_zero
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
h : ¬g f d z ≠ 0
⊢ ¬Complex.abs (g f d z - 1) ≤ 1 / 4
Tactic:
simp only [not_not] at h
Proof state after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
h : g f d z = 0
⊢ ¬Complex.abs (g f d z - 1) ≤ 1 / 4
Theorem: SuperNear.g_ne_zero
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
h : g f d z = 0
⊢ ¬Complex.abs (g f d z - 1) ≤ 1 / 4
Tactic:
simp only [h]
Proof state after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
h : g f d z = 0
⊢ ¬Complex.abs (0 - 1) ≤ 1 / 4
Theorem: SuperNear.g_ne_zero
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
h : g f d z = 0
⊢ ¬Complex.abs (0 - 1) ≤ 1 / 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: SuperNear.f_ne_zero
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
z : ℂ
zt : z ∈ t
z0 : z ≠ 0
⊢ f z ≠ 0
Tactic:
simp only [s.fg, mul_ne_zero (pow_ne_zero _ z0) (s.g_ne_zero zt), Ne, not_false_iff]
Proof state after:
no goals
Theorem: term_eqn
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ∀ (n : ℕ), term f d n (f z) = term f d (n + 1) z ^ d
Tactic:
intro n
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
⊢ term f d n (f z) = term f d (n + 1) z ^ d
Theorem: term_eqn
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
⊢ term f d n (f z) = term f d (n + 1) z ^ d
Tactic:
simp only [term, ← Function.iterate_succ_apply, pow_mul_nat, div_mul, pow_succ' _ (n + 1),
  mul_div_cancel_left₀ _ s.dz, Nat.succ_eq_add_one, Nat.cast_mul]
Proof state after:
no goals
Theorem: term_base
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ f z = (z * term f d 0 z) ^ d
Tactic:
rw [term]
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ f z = (z * g f d (f^[0] z) ^ (1 / ↑(d ^ (0 + 1)))) ^ d
Theorem: term_base
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ f z = (z * g f d (f^[0] z) ^ (1 / ↑(d ^ (0 + 1)))) ^ d
Tactic:
simp only [Function.iterate_zero, id, pow_one, one_div]
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ f z = (z * g f d z ^ (↑(d ^ (0 + 1)))⁻¹) ^ d
Theorem: term_base
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ f z = (z * g f d z ^ (↑(d ^ (0 + 1)))⁻¹) ^ d
Tactic:
rw [mul_pow, pow_mul_nat, zero_add, pow_one, inv_mul_cancel _]
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ f z = z ^ d * g f d z ^ 1

f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ↑d ≠ 0
Theorem: term_base
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ f z = z ^ d * g f d z ^ 1
Tactic:
rw [s.fg]
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ z ^ d * g f d z = z ^ d * g f d z ^ 1
Theorem: term_base
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ z ^ d * g f d z = z ^ d * g f d z ^ 1
Tactic:
simp only [Complex.cpow_one]
Proof state after:
no goals
Theorem: term_base
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ↑d ≠ 0
Tactic:
simp only [Ne, Nat.cast_eq_zero]
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ¬d = 0
Theorem: term_base
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ¬d = 0
Tactic:
exact (gt_of_ge_of_gt s.d2 (by norm_num)).ne'
Proof state after:
no goals
Theorem: term_base
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ 2 > 0
Tactic:
norm_num
Proof state after:
no goals