internlm/Lean-Github huggingface dataset:
Theorem: weak_log1p_small
Proof state before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
⊢ 1 + z ∈ s
Tactic:
simp [← hs]
Proof state after:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
⊢ Complex.abs z < r
Theorem: weak_log1p_small
Proof state before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
⊢ Complex.abs z < r
Tactic:
assumption
Proof state after:
no goals
Theorem: weak_log1p_small
Proof state before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
⊢ 1 ∈ s
Tactic:
simp [← hs]
Proof state after:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
⊢ 0 < r
Theorem: weak_log1p_small
Proof state before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
⊢ 0 < r
Tactic:
assumption
Proof state after:
no goals
Theorem: weak_log1p_small
Proof state before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
⊢ ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
Tactic:
intro w ws
Proof state after:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Theorem: weak_log1p_small
Proof state before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Tactic:
apply mem_slitPlane_of_near_one
Proof state after:
case a
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
w : ℂ
ws : w ∈ s
⊢ Complex.abs (w - 1) < 1
Theorem: weak_log1p_small
Proof state before:
case a
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
w : ℂ
ws : w ∈ s
⊢ Complex.abs (w - 1) < 1
Tactic:
simp only [Metric.mem_ball, Complex.dist_eq, ← hs] at ws
Proof state after:
case a
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
w : ℂ
ws : Complex.abs (w - 1) < r
⊢ Complex.abs (w - 1) < 1
Theorem: weak_log1p_small
Proof state before:
case a
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
w : ℂ
ws : Complex.abs (w - 1) < r
⊢ Complex.abs (w - 1) < 1
Tactic:
calc abs (w - 1) < r := by assumption
  _ < 1 := r1
Proof state after:
no goals
Theorem: weak_log1p_small
Proof state before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
w : ℂ
ws : Complex.abs (w - 1) < r
⊢ Complex.abs (w - 1) < r
Tactic:
assumption
Proof state after:
no goals
Theorem: weak_log1p_small
Proof state before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
⊢ ∀ w ∈ s, Complex.abs w ≥ 1 - r
Tactic:
intro w ws
Proof state after:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
w : ℂ
ws : w ∈ s
⊢ Complex.abs w ≥ 1 - r
Theorem: weak_log1p_small
Proof state before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
w : ℂ
ws : w ∈ s
⊢ Complex.abs w ≥ 1 - r
Tactic:
simp only [Metric.mem_ball, Complex.dist_eq, ← hs] at ws
Proof state after:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
w : ℂ
ws : Complex.abs (w - 1) < r
⊢ Complex.abs w ≥ 1 - r
Theorem: weak_log1p_small
Proof state before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
w : ℂ
ws : Complex.abs (w - 1) < r
⊢ Complex.abs w ≥ 1 - r
Tactic:
calc abs w = abs (1 + (w - 1)) := by ring_nf
  _ ≥ abs (1 : ℂ) - abs (w - 1) := by bound
  _ ≥ abs (1 : ℂ) - r := by bound
  _ = 1 - r := by rw [Complex.abs.map_one]
Proof state after:
no goals
Theorem: weak_log1p_small
Proof state before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
w : ℂ
ws : Complex.abs (w - 1) < r
⊢ Complex.abs w = Complex.abs (1 + (w - 1))
Tactic:
ring_nf
Proof state after:
no goals
Theorem: weak_log1p_small
Proof state before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
w : ℂ
ws : Complex.abs (w - 1) < r
⊢ Complex.abs (1 + (w - 1)) ≥ Complex.abs 1 - Complex.abs (w - 1)
Tactic:
bound
Proof state after:
no goals
Theorem: weak_log1p_small
Proof state before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
w : ℂ
ws : Complex.abs (w - 1) < r
⊢ Complex.abs 1 - Complex.abs (w - 1) ≥ Complex.abs 1 - r
Tactic:
bound
Proof state after:
no goals
Theorem: weak_log1p_small
Proof state before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
w : ℂ
ws : Complex.abs (w - 1) < r
⊢ Complex.abs 1 - r = 1 - r
Tactic:
rw [Complex.abs.map_one]
Proof state after:
no goals
Theorem: weak_log1p_small
Proof state before:
case refine_1
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
⊢ DifferentiableOn ℂ log s
Tactic:
exact DifferentiableOn.clog differentiableOn_id sp
Proof state after:
no goals
Theorem: weak_log1p_small
Proof state before:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
⊢ ∀ x ∈ s, ‖derivWithin log s x‖ ≤ 1 / (1 - r)
Tactic:
intro w ws
Proof state after:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ ‖derivWithin log s w‖ ≤ 1 / (1 - r)
Theorem: weak_log1p_small
Proof state before:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ ‖derivWithin log s w‖ ≤ 1 / (1 - r)
Tactic:
rw [derivWithin.clog o ws, derivWithin.cid o ws]
Proof state after:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ ‖1 / w‖ ≤ 1 / (1 - r)

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Theorem: weak_log1p_small
Proof state before:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ ‖1 / w‖ ≤ 1 / (1 - r)

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Tactic:
simp only [one_div, norm_inv, Complex.norm_eq_abs]
Proof state after:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ (Complex.abs w)⁻¹ ≤ (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Theorem: weak_log1p_small
Proof state before:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ (Complex.abs w)⁻¹ ≤ (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Tactic:
rw [inv_le]
Proof state after:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ (1 - r)⁻¹⁻¹ ≤ Complex.abs w

case refine_2.ha
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < Complex.abs w

case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Theorem: weak_log1p_small
Proof state before:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ (1 - r)⁻¹⁻¹ ≤ Complex.abs w

case refine_2.ha
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < Complex.abs w

case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Tactic:
have aw := sa w ws
Proof state after:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
aw : Complex.abs w ≥ 1 - r
⊢ (1 - r)⁻¹⁻¹ ≤ Complex.abs w

case refine_2.ha
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < Complex.abs w

case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Theorem: weak_log1p_small
Proof state before:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
aw : Complex.abs w ≥ 1 - r
⊢ (1 - r)⁻¹⁻¹ ≤ Complex.abs w

case refine_2.ha
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < Complex.abs w

case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Tactic:
simp at aw
Proof state after:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
aw : 1 ≤ Complex.abs w + r
⊢ (1 - r)⁻¹⁻¹ ≤ Complex.abs w

case refine_2.ha
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < Complex.abs w

case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Theorem: weak_log1p_small
Proof state before:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
aw : 1 ≤ Complex.abs w + r
⊢ (1 - r)⁻¹⁻¹ ≤ Complex.abs w

case refine_2.ha
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < Complex.abs w

case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Tactic:
field_simp
Proof state after:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
aw : 1 ≤ Complex.abs w + r
⊢ 1 ≤ Complex.abs w + r

case refine_2.ha
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < Complex.abs w

case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Theorem: weak_log1p_small
Proof state before:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
aw : 1 ≤ Complex.abs w + r
⊢ 1 ≤ Complex.abs w + r

case refine_2.ha
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < Complex.abs w

case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Tactic:
assumption
Proof state after:
case refine_2.ha
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < Complex.abs w

case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0