internlm/Lean-Github huggingface dataset:
Theorem: slightly_smaller
Proof state before:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Tactic:
generalize ha : 1 - r/2/abs z = a
Proof state after:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Theorem: slightly_smaller
Proof state before:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Tactic:
have a0 : 0 ≤ a := by rw [←ha, sub_nonneg, div_le_one azp]; exact _root_.trans (by bound) rz
Proof state after:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Theorem: slightly_smaller
Proof state before:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Tactic:
have a1 : a < 1 := by rw [←ha, sub_lt_self_iff]; positivity
Proof state after:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Theorem: slightly_smaller
Proof state before:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Tactic:
generalize hw : ↑a * z = w
Proof state after:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Theorem: slightly_smaller
Proof state before:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Tactic:
use w
Proof state after:
case h
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Theorem: slightly_smaller
Proof state before:
case h
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Tactic:
constructor
Proof state after:
case h.left
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs (w - z) < r

case h.right
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs w < Complex.abs z
Theorem: slightly_smaller
Proof state before:
case pos
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : Complex.abs z < r
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Tactic:
use 0
Proof state after:
case h
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : Complex.abs z < r
⊢ Complex.abs (0 - z) < r ∧ Complex.abs 0 < Complex.abs z
Theorem: slightly_smaller
Proof state before:
case h
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : Complex.abs z < r
⊢ Complex.abs (0 - z) < r ∧ Complex.abs 0 < Complex.abs z
Tactic:
simp only [zero_sub, map_neg_eq_map, rz, map_zero, AbsoluteValue.pos_iff, ne_eq, nz,
  not_false_eq_true, and_self]
Proof state after:
no goals
Theorem: slightly_smaller
Proof state before:
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
⊢ 0 ≤ a
Tactic:
rw [←ha, sub_nonneg, div_le_one azp]
Proof state after:
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
⊢ r / 2 ≤ Complex.abs z
Theorem: slightly_smaller
Proof state before:
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
⊢ r / 2 ≤ Complex.abs z
Tactic:
exact _root_.trans (by bound) rz
Proof state after:
no goals
Theorem: slightly_smaller
Proof state before:
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
⊢ r / 2 ≤ r
Tactic:
bound
Proof state after:
no goals
Theorem: slightly_smaller
Proof state before:
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
⊢ a < 1
Tactic:
rw [←ha, sub_lt_self_iff]
Proof state after:
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
⊢ 0 < r / 2 / Complex.abs z
Theorem: slightly_smaller
Proof state before:
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
⊢ 0 < r / 2 / Complex.abs z
Tactic:
positivity
Proof state after:
no goals
Theorem: slightly_smaller
Proof state before:
case h.left
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs (w - z) < r
Tactic:
rw [←hw,←ha]
Proof state after:
case h.left
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs (↑(1 - r / 2 / Complex.abs z) * z - z) < r
Theorem: slightly_smaller
Proof state before:
case h.left
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs (↑(1 - r / 2 / Complex.abs z) * z - z) < r
Tactic:
simp only [Complex.ofReal_sub, Complex.ofReal_one, Complex.ofReal_div]
Proof state after:
case h.left
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs ((1 - ↑r / ↑2 / ↑(Complex.abs z)) * z - z) < r
Theorem: slightly_smaller
Proof state before:
case h.left
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs ((1 - ↑r / ↑2 / ↑(Complex.abs z)) * z - z) < r
Tactic:
rw [mul_sub_right_distrib]
Proof state after:
case h.left
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs (1 * z - ↑r / ↑2 / ↑(Complex.abs z) * z - z) < r
Theorem: slightly_smaller
Proof state before:
case h.left
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs (1 * z - ↑r / ↑2 / ↑(Complex.abs z) * z - z) < r
Tactic:
simp only [one_mul, sub_sub_cancel_left, AbsoluteValue.map_neg, AbsoluteValue.map_mul, map_div₀,
  Complex.abs_ofReal, Complex.abs_two, Complex.abs_abs, abs_of_pos rp, div_mul (r/2),
  div_mul_cancel₀ _ azp.ne', div_one, abs_two, div_self azp.ne']
Proof state after:
case h.left
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ r / 2 < r
Theorem: slightly_smaller
Proof state before:
case h.left
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ r / 2 < r
Tactic:
bound
Proof state after:
no goals
Theorem: slightly_smaller
Proof state before:
case h.right
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs w < Complex.abs z
Tactic:
simp only [←hw, AbsoluteValue.map_mul, Complex.abs_ofReal, abs_of_nonneg a0]
Proof state after:
case h.right
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ a * Complex.abs z < Complex.abs z
Theorem: slightly_smaller
Proof state before:
case h.right
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ a * Complex.abs z < Complex.abs z
Tactic:
calc a * abs z < 1 * abs z := mul_lt_mul_of_pos_right a1 azp
  _ = abs z := by ring
Proof state after:
no goals
Theorem: slightly_smaller
Proof state before:
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ 1 * Complex.abs z = Complex.abs z
Tactic:
ring
Proof state after:
no goals
Theorem: frequently_smaller
Proof state before:
z : ℂ
z0 : z ≠ 0
⊢ ∃ᶠ (w : ℂ) in 𝓝 z, Complex.abs w < Complex.abs z
Tactic:
simp only [Filter.Frequently, Metric.eventually_nhds_iff, not_exists, not_forall, not_not,
  Complex.dist_eq, not_and]
Proof state after:
z : ℂ
z0 : z ≠ 0
⊢ ∀ x > 0, ∃ x_1, ∃ (_ : Complex.abs (x_1 - z) < x), Complex.abs x_1 < Complex.abs z
Theorem: frequently_smaller
Proof state before:
z : ℂ
z0 : z ≠ 0
⊢ ∀ x > 0, ∃ x_1, ∃ (_ : Complex.abs (x_1 - z) < x), Complex.abs x_1 < Complex.abs z
Tactic:
intro r rp
Proof state after:
z : ℂ
z0 : z ≠ 0
r : ℝ
rp : r > 0
⊢ ∃ x, ∃ (_ : Complex.abs (x - z) < r), Complex.abs x < Complex.abs z
Theorem: frequently_smaller
Proof state before:
z : ℂ
z0 : z ≠ 0
r : ℝ
rp : r > 0
⊢ ∃ x, ∃ (_ : Complex.abs (x - z) < r), Complex.abs x < Complex.abs z
Tactic:
rcases slightly_smaller z0 rp with ⟨w, b, lt⟩
Proof state after:
case intro.intro
z : ℂ
z0 : z ≠ 0
r : ℝ
rp : r > 0
w : ℂ
b : Complex.abs (w - z) < r
lt : Complex.abs w < Complex.abs z
⊢ ∃ x, ∃ (_ : Complex.abs (x - z) < r), Complex.abs x < Complex.abs z
Theorem: frequently_smaller
Proof state before:
case intro.intro
z : ℂ
z0 : z ≠ 0
r : ℝ
rp : r > 0
w : ℂ
b : Complex.abs (w - z) < r
lt : Complex.abs w < Complex.abs z
⊢ ∃ x, ∃ (_ : Complex.abs (x - z) < r), Complex.abs x < Complex.abs z
Tactic:
use w, b, lt
Proof state after:
no goals
Theorem: weak_to_strong_small
Proof state before:
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
⊢ Complex.abs (f z) ≤ c * Complex.abs z
Tactic:
by_cases nz : z = 0
Proof state after:
case pos
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : z = 0
⊢ Complex.abs (f z) ≤ c * Complex.abs z

case neg
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
⊢ Complex.abs (f z) ≤ c * Complex.abs z
Theorem: weak_to_strong_small
Proof state before:
case neg
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
⊢ Complex.abs (f z) ≤ c * Complex.abs z
Tactic:
apply le_of_forall_small_le_add zero_lt_one
Proof state after:
case neg
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
⊢ ∀ (e : ℝ), 0 < e → e < 1 → Complex.abs (f z) ≤ c * Complex.abs z + e
Theorem: weak_to_strong_small
Proof state before:
case neg
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
⊢ ∀ (e : ℝ), 0 < e → e < 1 → Complex.abs (f z) ≤ c * Complex.abs z + e
Tactic:
intro e ep _
Proof state after:
case neg
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
⊢ Complex.abs (f z) ≤ c * Complex.abs z + e
Theorem: weak_to_strong_small
Proof state before:
case neg
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
⊢ Complex.abs (f z) ≤ c * Complex.abs z + e
Tactic:
rcases Metric.continuous_near fc rp e ep with ⟨s,sp,_,sc⟩
Proof state after:
case neg.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
s : ℝ
sp : 0 < s
left✝ : s ≤ r
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
⊢ Complex.abs (f z) ≤ c * Complex.abs z + e
Theorem: weak_to_strong_small
Proof state before:
case neg.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
s : ℝ
sp : 0 < s
left✝ : s ≤ r
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
⊢ Complex.abs (f z) ≤ c * Complex.abs z + e
Tactic:
rcases slightly_smaller nz sp with ⟨w,wz,awz⟩
Proof state after:
case neg.intro.intro.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
s : ℝ
sp : 0 < s
left✝ : s ≤ r
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
w : ℂ
wz : Complex.abs (w - z) < s
awz : Complex.abs w < Complex.abs z
⊢ Complex.abs (f z) ≤ c * Complex.abs z + e
Theorem: weak_to_strong_small
Proof state before:
case neg.intro.intro.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
s : ℝ
sp : 0 < s
left✝ : s ≤ r
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
w : ℂ
wz : Complex.abs (w - z) < s
awz : Complex.abs w < Complex.abs z
⊢ Complex.abs (f z) ≤ c * Complex.abs z + e
Tactic:
have wr : abs w < r := lt_of_lt_of_le awz zr
Proof state after:
case neg.intro.intro.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
s : ℝ
sp : 0 < s
left✝ : s ≤ r
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
w : ℂ
wz : Complex.abs (w - z) < s
awz : Complex.abs w < Complex.abs z
wr : Complex.abs w < r
⊢ Complex.abs (f z) ≤ c * Complex.abs z + e
Theorem: weak_to_strong_small
Proof state before:
case neg.intro.intro.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
s : ℝ
sp : 0 < s
left✝ : s ≤ r
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
w : ℂ
wz : Complex.abs (w - z) < s
awz : Complex.abs w < Complex.abs z
wr : Complex.abs w < r
⊢ Complex.abs (f z) ≤ c * Complex.abs z + e
Tactic:
calc abs (f z) = abs (f w - (f w - f z)) := by ring_nf
  _ ≤ abs (f w) + abs (f w - f z) := by bound
  _ ≤ c * abs w + e := by bound [h w wr, sc wz]
  _ ≤ c * abs z + e := by bound
Proof state after:
no goals
Theorem: weak_to_strong_small
Proof state before:
case pos
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : z = 0
⊢ Complex.abs (f z) ≤ c * Complex.abs z
Tactic:
refine h z ?_
Proof state after:
case pos
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : z = 0
⊢ Complex.abs z < r
Theorem: weak_to_strong_small
Proof state before:
case pos
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : z = 0
⊢ Complex.abs z < r
Tactic:
rw [nz]
Proof state after:
case pos
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : z = 0
⊢ Complex.abs 0 < r
Theorem: weak_to_strong_small
Proof state before:
case pos
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : z = 0
⊢ Complex.abs 0 < r
Tactic:
simpa
Proof state after:
no goals
Theorem: weak_to_strong_small
Proof state before:
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
s : ℝ
sp : 0 < s
left✝ : s ≤ r
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
w : ℂ
wz : Complex.abs (w - z) < s
awz : Complex.abs w < Complex.abs z
wr : Complex.abs w < r
⊢ Complex.abs (f z) = Complex.abs (f w - (f w - f z))
Tactic:
ring_nf
Proof state after:
no goals
Theorem: weak_to_strong_small
Proof state before:
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
s : ℝ
sp : 0 < s
left✝ : s ≤ r
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
w : ℂ
wz : Complex.abs (w - z) < s
awz : Complex.abs w < Complex.abs z
wr : Complex.abs w < r
⊢ Complex.abs (f w - (f w - f z)) ≤ Complex.abs (f w) + Complex.abs (f w - f z)
Tactic:
bound
Proof state after:
no goals
Theorem: weak_to_strong_small
Proof state before:
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
s : ℝ
sp : 0 < s
left✝ : s ≤ r
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
w : ℂ
wz : Complex.abs (w - z) < s
awz : Complex.abs w < Complex.abs z
wr : Complex.abs w < r
⊢ Complex.abs (f w) + Complex.abs (f w - f z) ≤ c * Complex.abs w + e
Tactic:
bound [h w wr, sc wz]
Proof state after:
no goals
Theorem: weak_to_strong_small
Proof state before:
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
s : ℝ
sp : 0 < s
left✝ : s ≤ r
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
w : ℂ
wz : Complex.abs (w - z) < s
awz : Complex.abs w < Complex.abs z
wr : Complex.abs w < r
⊢ c * Complex.abs w + e ≤ c * Complex.abs z + e
Tactic:
bound
Proof state after:
no goals
Theorem: log1p_small'
Proof state before:
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
by_cases r0 : r ≤ 0
Proof state after:
case pos
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : r ≤ 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z

case neg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : ¬r ≤ 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Theorem: log1p_small'
Proof state before:
case neg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : ¬r ≤ 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
simp only [not_le] at r0
Proof state after:
case neg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Theorem: log1p_small'
Proof state before:
case neg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
have fc : ContinuousAt (fun z ↦ log (1 + z)) z := by
  apply ContinuousAt.clog; apply ContinuousAt.add; exact continuousAt_const; exact continuousAt_id
  refine mem_slitPlane_of_near_one ?_
  simp only [add_sub_cancel_left, lt_of_le_of_lt zr r1]
Proof state after:
case neg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
fc : ContinuousAt (fun z => (1 + z).log) z
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Theorem: log1p_small'
Proof state before:
case neg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
fc : ContinuousAt (fun z => (1 + z).log) z
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
apply weak_to_strong_small r0 (by bound) zr fc
Proof state after:
case neg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
fc : ContinuousAt (fun z => (1 + z).log) z
⊢ ∀ (z : ℂ), Complex.abs z < r → Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Theorem: log1p_small'
Proof state before:
case neg
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
fc : ContinuousAt (fun z => (1 + z).log) z
⊢ ∀ (z : ℂ), Complex.abs z < r → Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
intro w wr
Proof state after:
case neg
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
⊢ Complex.abs (1 + w).log ≤ 1 / (1 - r) * Complex.abs w
Theorem: log1p_small'
Proof state before:
case neg
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
⊢ Complex.abs (1 + w).log ≤ 1 / (1 - r) * Complex.abs w
Tactic:
exact @weak_log1p_small w r (by bound) wr
Proof state after:
no goals
Theorem: log1p_small'
Proof state before:
case pos
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : r ≤ 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
have z0 := le_antisymm (le_trans zr r0) (Complex.abs.nonneg _)
Proof state after:
case pos
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : r ≤ 0
z0 : Complex.abs z = 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Theorem: log1p_small'
Proof state before:
case pos
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : r ≤ 0
z0 : Complex.abs z = 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
simp only [map_eq_zero] at z0
Proof state after:
case pos
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : r ≤ 0
z0 : z = 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Theorem: log1p_small'
Proof state before:
case pos
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : r ≤ 0
z0 : z = 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
simp only [z0, add_zero, Complex.log_one, map_zero, r0, sub_zero, ne_eq, one_ne_zero,
  not_false_eq_true, div_self, mul_zero, le_refl]
Proof state after:
no goals
Theorem: log1p_small'
Proof state before:
z : ℂ
r : ℝ
r1 : r < 1
zr : Complex.abs z ≤ r
r0 : 0 < r
⊢ ContinuousAt (fun z => (1 + z).log) z
Tactic:
apply ContinuousAt.clog
Proof state after:
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