internlm/Lean-Github huggingface dataset:
Theorem: log1p_small'
Proof state before:
case h₁
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ ContinuousAt (fun t => 1 + t) z

case h₂
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ 1 + z ∈ slitPlane
Tactic:
apply ContinuousAt.add
Proof state after:
case h₁.hf
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ ContinuousAt (fun x => 1) z

case h₁.hg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ ContinuousAt (fun x => x) z

case h₂
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ 1 + z ∈ slitPlane
Theorem: log1p_small'
Proof state before:
case h₁.hf
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ ContinuousAt (fun x => 1) z

case h₁.hg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ ContinuousAt (fun x => x) z

case h₂
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ 1 + z ∈ slitPlane
Tactic:
exact continuousAt_const
Proof state after:
case h₁.hg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ ContinuousAt (fun x => x) z

case h₂
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ 1 + z ∈ slitPlane
Theorem: log1p_small'
Proof state before:
case h₁.hg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ ContinuousAt (fun x => x) z

case h₂
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ 1 + z ∈ slitPlane
Tactic:
exact continuousAt_id
Proof state after:
case h₂
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ 1 + z ∈ slitPlane
Theorem: log1p_small'
Proof state before:
case h₂
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ 1 + z ∈ slitPlane
Tactic:
refine mem_slitPlane_of_near_one ?_
Proof state after:
case h₂
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ Complex.abs (1 + z - 1) < 1
Theorem: log1p_small'
Proof state before:
case h₂
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ Complex.abs (1 + z - 1) < 1
Tactic:
simp only [add_sub_cancel_left, lt_of_le_of_lt zr r1]
Proof state after:
no goals
Theorem: log1p_small'
Proof state before:
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
fc : ContinuousAt (fun z => (1 + z).log) z
⊢ 1 / (1 - r) > 0
Tactic:
bound
Proof state after:
no goals
Theorem: log1p_small'
Proof state before:
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
fc : ContinuousAt (fun z => (1 + z).log) z
w : ℂ
wr : Complex.abs w < r
⊢ r < 1
Tactic:
bound
Proof state after:
no goals
Theorem: log1p_small
Proof state before:
z : ℂ
zs : Complex.abs z ≤ 1 / 2
⊢ 1 / 2 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: log1p_small
Proof state before:
z : ℂ
zs : Complex.abs z ≤ 1 / 2
⊢ 1 / (1 - 1 / 2) * Complex.abs z = 2 * Complex.abs z
Tactic:
norm_num
Proof state after:
no goals
Theorem: Real.log1p_small'
Proof state before:
x r : ℝ
r1 : r < 1
xr : |x| ≤ r
⊢ |(1 + x).log| ≤ 1 / (1 - r) * |x|
Tactic:
set z := (x : ℂ)
Proof state after:
x r : ℝ
r1 : r < 1
xr : |x| ≤ r
z : ℂ := ↑x
⊢ |(1 + x).log| ≤ 1 / (1 - r) * |x|
Theorem: Real.log1p_small'
Proof state before:
x r : ℝ
r1 : r < 1
xr : |x| ≤ r
z : ℂ := ↑x
⊢ |(1 + x).log| ≤ 1 / (1 - r) * |x|
Tactic:
have zx : abs z = |x| := Complex.abs_ofReal _
Proof state after:
x r : ℝ
r1 : r < 1
xr : |x| ≤ r
z : ℂ := ↑x
zx : Complex.abs z = |x|
⊢ |(1 + x).log| ≤ 1 / (1 - r) * |x|
Theorem: Real.log1p_small'
Proof state before:
x r : ℝ
r1 : r < 1
xr : |x| ≤ r
z : ℂ := ↑x
zx : Complex.abs z = |x|
⊢ |(1 + x).log| ≤ 1 / (1 - r) * |x|
Tactic:
simp only [← Complex.log_ofReal_re, ← zx] at xr ⊢
Proof state after:
x r : ℝ
r1 : r < 1
z : ℂ := ↑x
zx : Complex.abs z = |x|
xr : Complex.abs z ≤ r
⊢ |(↑(1 + x)).log.re| ≤ 1 / (1 - r) * Complex.abs z
Theorem: Real.log1p_small'
Proof state before:
x r : ℝ
r1 : r < 1
z : ℂ := ↑x
zx : Complex.abs z = |x|
xr : Complex.abs z ≤ r
⊢ |(↑(1 + x)).log.re| ≤ 1 / (1 - r) * Complex.abs z
Tactic:
refine _root_.trans (_root_.trans (Complex.abs_re_le_abs _) ?_) (_root_.log1p_small' r1 xr)
Proof state after:
x r : ℝ
r1 : r < 1
z : ℂ := ↑x
zx : Complex.abs z = |x|
xr : Complex.abs z ≤ r
⊢ Complex.abs (↑(1 + x)).log ≤ Complex.abs (1 + z).log
Theorem: Real.log1p_small'
Proof state before:
x r : ℝ
r1 : r < 1
z : ℂ := ↑x
zx : Complex.abs z = |x|
xr : Complex.abs z ≤ r
⊢ Complex.abs (↑(1 + x)).log ≤ Complex.abs (1 + z).log
Tactic:
simp only [Complex.ofReal_add, Complex.ofReal_one, le_refl]
Proof state after:
no goals
Theorem: Real.log1p_small
Proof state before:
x : ℝ
xr : |x| ≤ 1 / 2
⊢ 1 / 2 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: Real.log1p_small
Proof state before:
x : ℝ
xr : |x| ≤ 1 / 2
⊢ 1 / (1 - 1 / 2) * |x| = 2 * |x|
Tactic:
norm_num
Proof state after:
no goals
Theorem: log_small
Proof state before:
z : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
⊢ Complex.abs z.log ≤ 2 * Complex.abs (z - 1)
Tactic:
generalize zw : z - 1 = z1
Proof state after:
z : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
z1 : ℂ
zw : z - 1 = z1
⊢ Complex.abs z.log ≤ 2 * Complex.abs z1
Theorem: log_small
Proof state before:
z : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
z1 : ℂ
zw : z - 1 = z1
⊢ Complex.abs z.log ≤ 2 * Complex.abs z1
Tactic:
have wz : z = 1 + z1 := by rw [← zw]; ring
Proof state after:
z : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs z.log ≤ 2 * Complex.abs z1
Theorem: log_small
Proof state before:
z : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs z.log ≤ 2 * Complex.abs z1
Tactic:
rw [wz]
Proof state after:
z : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs (1 + z1).log ≤ 2 * Complex.abs z1
Theorem: log_small
Proof state before:
z : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs (1 + z1).log ≤ 2 * Complex.abs z1
Tactic:
refine log1p_small ?_
Proof state after:
z : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs z1 ≤ 1 / 2
Theorem: log_small
Proof state before:
z : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs z1 ≤ 1 / 2
Tactic:
rw [← zw]
Proof state after:
z : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs (z - 1) ≤ 1 / 2
Theorem: log_small
Proof state before:
z : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs (z - 1) ≤ 1 / 2
Tactic:
assumption
Proof state after:
no goals
Theorem: log_small
Proof state before:
z : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
z1 : ℂ
zw : z - 1 = z1
⊢ z = 1 + z1
Tactic:
rw [← zw]
Proof state after:
z : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
z1 : ℂ
zw : z - 1 = z1
⊢ z = 1 + (z - 1)
Theorem: log_small
Proof state before:
z : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
z1 : ℂ
zw : z - 1 = z1
⊢ z = 1 + (z - 1)
Tactic:
ring
Proof state after:
no goals
Theorem: weak_exp_small
Proof state before:
z : ℂ
h : Complex.abs z < 1
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Tactic:
have hr : 0 ≤ (1 : ℝ) := by norm_num
Proof state after:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Theorem: weak_exp_small
Proof state before:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Tactic:
have L := Complex.locally_lipschitz_exp hr (by bound) 0 z
  (by simpa only [sub_zero, Complex.norm_eq_abs])
Proof state after:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
L : ‖z.exp - exp 0‖ ≤ (1 + 1) * ‖exp 0‖ * ‖z - 0‖
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Theorem: weak_exp_small
Proof state before:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
L : ‖z.exp - exp 0‖ ≤ (1 + 1) * ‖exp 0‖ * ‖z - 0‖
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Tactic:
simp only [Complex.exp_zero, Complex.norm_eq_abs, norm_one, mul_one, sub_zero] at L
Proof state after:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
L : Complex.abs (z.exp - 1) ≤ (1 + 1) * Complex.abs z
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Theorem: weak_exp_small
Proof state before:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
L : Complex.abs (z.exp - 1) ≤ (1 + 1) * Complex.abs z
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Tactic:
have t : 1 + 1 = (2 : ℝ) := by norm_num
Proof state after:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
L : Complex.abs (z.exp - 1) ≤ (1 + 1) * Complex.abs z
t : 1 + 1 = 2
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Theorem: weak_exp_small
Proof state before:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
L : Complex.abs (z.exp - 1) ≤ (1 + 1) * Complex.abs z
t : 1 + 1 = 2
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Tactic:
rw [t] at L
Proof state after:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
L : Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
t : 1 + 1 = 2
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Theorem: weak_exp_small
Proof state before:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
L : Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
t : 1 + 1 = 2
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Tactic:
assumption
Proof state after:
no goals
Theorem: weak_exp_small
Proof state before:
z : ℂ
h : Complex.abs z < 1
⊢ 0 ≤ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: weak_exp_small
Proof state before:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
⊢ 1 ≤ 1
Tactic:
bound
Proof state after:
no goals
Theorem: weak_exp_small
Proof state before:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
⊢ ‖z - 0‖ < 1
Tactic:
simpa only [sub_zero, Complex.norm_eq_abs]
Proof state after:
no goals
Theorem: weak_exp_small
Proof state before:
z : ℂ
h : Complex.abs z < 1
hr : 0 ≤ 1
L : Complex.abs (z.exp - 1) ≤ (1 + 1) * Complex.abs z
⊢ 1 + 1 = 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: exp_small
Proof state before:
z : ℂ
zs : Complex.abs z ≤ 1
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Tactic:
have rp : (1 : ℝ) > 0 := by norm_num
Proof state after:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Theorem: exp_small
Proof state before:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Tactic:
have cp : (2 : ℝ) > 0 := by norm_num
Proof state after:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Theorem: exp_small
Proof state before:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Tactic:
have fc : ContinuousAt (fun z ↦ exp z - 1) z := by
  apply ContinuousAt.sub; apply ContinuousAt.cexp
  exact continuousAt_id; exact continuousAt_const
Proof state after:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
fc : ContinuousAt (fun z => z.exp - 1) z
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Theorem: exp_small
Proof state before:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
fc : ContinuousAt (fun z => z.exp - 1) z
⊢ Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Tactic:
apply weak_to_strong_small rp cp zs fc
Proof state after:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
fc : ContinuousAt (fun z => z.exp - 1) z
⊢ ∀ (z : ℂ), Complex.abs z < 1 → Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Theorem: exp_small
Proof state before:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
fc : ContinuousAt (fun z => z.exp - 1) z
⊢ ∀ (z : ℂ), Complex.abs z < 1 → Complex.abs (z.exp - 1) ≤ 2 * Complex.abs z
Tactic:
intro w wr
Proof state after:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
fc : ContinuousAt (fun z => z.exp - 1) z
w : ℂ
wr : Complex.abs w < 1
⊢ Complex.abs (w.exp - 1) ≤ 2 * Complex.abs w
Theorem: exp_small
Proof state before:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
fc : ContinuousAt (fun z => z.exp - 1) z
w : ℂ
wr : Complex.abs w < 1
⊢ Complex.abs (w.exp - 1) ≤ 2 * Complex.abs w
Tactic:
exact weak_exp_small wr
Proof state after:
no goals
Theorem: exp_small
Proof state before:
z : ℂ
zs : Complex.abs z ≤ 1
⊢ 1 > 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: exp_small
Proof state before:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
⊢ 2 > 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: exp_small
Proof state before:
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ ContinuousAt (fun z => z.exp - 1) z
Tactic:
apply ContinuousAt.sub
Proof state after:
case hf
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ ContinuousAt (fun x => x.exp) z

case hg
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ ContinuousAt (fun x => 1) z
Theorem: exp_small
Proof state before:
case hf
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ ContinuousAt (fun x => x.exp) z

case hg
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ ContinuousAt (fun x => 1) z
Tactic:
apply ContinuousAt.cexp
Proof state after:
case hf.h
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ ContinuousAt (fun y => y) z

case hg
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ ContinuousAt (fun x => 1) z
Theorem: exp_small
Proof state before:
case hf.h
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ ContinuousAt (fun y => y) z

case hg
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ ContinuousAt (fun x => 1) z
Tactic:
exact continuousAt_id
Proof state after:
case hg
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ ContinuousAt (fun x => 1) z
Theorem: exp_small
Proof state before:
case hg
z : ℂ
zs : Complex.abs z ≤ 1
rp : 1 > 0
cp : 2 > 0
⊢ ContinuousAt (fun x => 1) z
Tactic:
exact continuousAt_const
Proof state after:
no goals
Theorem: pow1p_small
Proof state before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
⊢ Complex.abs ((1 + z) ^ w - 1) ≤ 4 * Complex.abs z * Complex.abs w
Tactic:
have z1 : 1 + z ≠ 0 := by
  rw [←Complex.abs.ne_zero_iff]; apply ne_of_gt
  calc abs (1 + z) ≥ abs (1 : ℂ) - abs z := by bound
    _ ≥ abs (1 : ℂ) - 1/2 := by bound
    _ > 0 := by norm_num
Proof state after:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
⊢ Complex.abs ((1 + z) ^ w - 1) ≤ 4 * Complex.abs z * Complex.abs w
Theorem: pow1p_small
Proof state before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
⊢ Complex.abs ((1 + z) ^ w - 1) ≤ 4 * Complex.abs z * Complex.abs w
Tactic:
rw [Complex.cpow_def_of_ne_zero z1]
Proof state after:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 4 * Complex.abs z * Complex.abs w
Theorem: pow1p_small
Proof state before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 4 * Complex.abs z * Complex.abs w
Tactic:
have ls := log1p_small zs
Proof state after:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 4 * Complex.abs z * Complex.abs w
Theorem: pow1p_small
Proof state before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 4 * Complex.abs z * Complex.abs w
Tactic:
have eas : abs (log (1 + z) * w) ≤ 1 := by
  rw [Complex.abs.map_mul]
  calc abs (log (1 + z)) * abs w ≤ 2 * abs z * abs w := by bound
    _ ≤ 2 * (1/2) * 1 := by bound
    _ = 1 := by norm_num
Proof state after:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 4 * Complex.abs z * Complex.abs w
Theorem: pow1p_small
Proof state before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 4 * Complex.abs z * Complex.abs w
Tactic:
have es := exp_small eas
Proof state after:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs ((1 + z).log * w)
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 4 * Complex.abs z * Complex.abs w
Theorem: pow1p_small
Proof state before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs ((1 + z).log * w)
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 4 * Complex.abs z * Complex.abs w
Tactic:
rw [Complex.abs.map_mul, ←mul_assoc] at es
Proof state after:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 4 * Complex.abs z * Complex.abs w
Theorem: pow1p_small
Proof state before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 4 * Complex.abs z * Complex.abs w
Tactic:
trans 2 * abs (log (1 + z)) * abs w
Proof state after:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w

z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w
⊢ 2 * Complex.abs (1 + z).log * Complex.abs w ≤ 4 * Complex.abs z * Complex.abs w
Theorem: pow1p_small
Proof state before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w
⊢ Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w

z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w
⊢ 2 * Complex.abs (1 + z).log * Complex.abs w ≤ 4 * Complex.abs z * Complex.abs w
Tactic:
exact es
Proof state after:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w
⊢ 2 * Complex.abs (1 + z).log * Complex.abs w ≤ 4 * Complex.abs z * Complex.abs w
Theorem: pow1p_small
Proof state before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w
⊢ 2 * Complex.abs (1 + z).log * Complex.abs w ≤ 4 * Complex.abs z * Complex.abs w
Tactic:
calc 2 * abs (log (1 + z)) * abs w ≤ 2 * (2 * abs z) * abs w := by bound
  _ = 4 * abs z * abs w := by ring
Proof state after:
no goals
Theorem: pow1p_small
Proof state before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
⊢ 1 + z ≠ 0
Tactic:
rw [←Complex.abs.ne_zero_iff]
Proof state after:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
⊢ Complex.abs (1 + z) ≠ 0
Theorem: pow1p_small
Proof state before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
⊢ Complex.abs (1 + z) ≠ 0
Tactic:
apply ne_of_gt
Proof state after:
case h
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
⊢ 0 < Complex.abs (1 + z)
Theorem: pow1p_small
Proof state before:
case h
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
⊢ 0 < Complex.abs (1 + z)
Tactic:
calc abs (1 + z) ≥ abs (1 : ℂ) - abs z := by bound
  _ ≥ abs (1 : ℂ) - 1/2 := by bound
  _ > 0 := by norm_num
Proof state after:
no goals
Theorem: pow1p_small
Proof state before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
⊢ Complex.abs (1 + z) ≥ Complex.abs 1 - Complex.abs z
Tactic:
bound
Proof state after:
no goals
Theorem: pow1p_small
Proof state before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
⊢ Complex.abs 1 - Complex.abs z ≥ Complex.abs 1 - 1 / 2
Tactic:
bound
Proof state after:
no goals
Theorem: pow1p_small
Proof state before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
⊢ Complex.abs 1 - 1 / 2 > 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: pow1p_small
Proof state before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
⊢ Complex.abs ((1 + z).log * w) ≤ 1
Tactic:
rw [Complex.abs.map_mul]
Proof state after:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
⊢ Complex.abs (1 + z).log * Complex.abs w ≤ 1
Theorem: pow1p_small
Proof state before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
⊢ Complex.abs (1 + z).log * Complex.abs w ≤ 1
Tactic:
calc abs (log (1 + z)) * abs w ≤ 2 * abs z * abs w := by bound
  _ ≤ 2 * (1/2) * 1 := by bound
  _ = 1 := by norm_num
Proof state after:
no goals
Theorem: pow1p_small
Proof state before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
⊢ Complex.abs (1 + z).log * Complex.abs w ≤ 2 * Complex.abs z * Complex.abs w
Tactic:
bound
Proof state after:
no goals
Theorem: pow1p_small
Proof state before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
⊢ 2 * Complex.abs z * Complex.abs w ≤ 2 * (1 / 2) * 1
Tactic:
bound
Proof state after:
no goals
Theorem: pow1p_small
Proof state before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
⊢ 2 * (1 / 2) * 1 = 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: pow1p_small
Proof state before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w
⊢ 2 * Complex.abs (1 + z).log * Complex.abs w ≤ 2 * (2 * Complex.abs z) * Complex.abs w
Tactic:
bound
Proof state after:
no goals
Theorem: pow1p_small
Proof state before:
z w : ℂ
zs : Complex.abs z ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : 1 + z ≠ 0
ls : Complex.abs (1 + z).log ≤ 2 * Complex.abs z
eas : Complex.abs ((1 + z).log * w) ≤ 1
es : Complex.abs (((1 + z).log * w).exp - 1) ≤ 2 * Complex.abs (1 + z).log * Complex.abs w
⊢ 2 * (2 * Complex.abs z) * Complex.abs w = 4 * Complex.abs z * Complex.abs w
Tactic:
ring
Proof state after:
no goals
Theorem: pow_small
Proof state before:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
⊢ Complex.abs (z ^ w - 1) ≤ 4 * Complex.abs (z - 1) * Complex.abs w
Tactic:
generalize zw : z - 1 = z1
Proof state after:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
⊢ Complex.abs (z ^ w - 1) ≤ 4 * Complex.abs z1 * Complex.abs w
Theorem: pow_small
Proof state before:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
⊢ Complex.abs (z ^ w - 1) ≤ 4 * Complex.abs z1 * Complex.abs w
Tactic:
have wz : z = 1 + z1 := by rw [← zw]; ring
Proof state after:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs (z ^ w - 1) ≤ 4 * Complex.abs z1 * Complex.abs w
Theorem: pow_small
Proof state before:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs (z ^ w - 1) ≤ 4 * Complex.abs z1 * Complex.abs w
Tactic:
rw [wz]
Proof state after:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs ((1 + z1) ^ w - 1) ≤ 4 * Complex.abs z1 * Complex.abs w