internlm/Lean-Github huggingface dataset:
Theorem: weak_log1p_small
Proof state before:
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.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
aw : Complex.abs w ≥ 1 - r
⊢ 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.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
aw : Complex.abs w ≥ 1 - r
⊢ 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:
linarith
Proof state after:
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.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:
norm_num
Proof state after:
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
⊢ r < 1

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.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
⊢ r < 1

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.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.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:
exact differentiableWithinAt_id
Proof state after:
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.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:
exact sp w ws
Proof state after:
no goals
Theorem: weak_log1p_small
Proof state before:
case refine_3
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
⊢ Convex ℝ s
Tactic:
rw [← hs]
Proof state after:
case refine_3
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
⊢ Convex ℝ (Metric.ball 1 r)
Theorem: weak_log1p_small
Proof state before:
case refine_3
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
⊢ Convex ℝ (Metric.ball 1 r)
Tactic:
exact convex_ball _ _
Proof state after:
no goals
Theorem: le_of_forall_small_le_add
Proof state before:
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
⊢ a ≤ b
Tactic:
apply le_of_forall_pos_lt_add
Proof state after:
case h
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
⊢ ∀ (ε : ℝ), 0 < ε → a < b + ε
Theorem: le_of_forall_small_le_add
Proof state before:
case h
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
⊢ ∀ (ε : ℝ), 0 < ε → a < b + ε
Tactic:
intro e ep
Proof state after:
case h
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
⊢ a < b + e
Theorem: le_of_forall_small_le_add
Proof state before:
case h
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
⊢ a < b + e
Tactic:
by_cases et : e ≥ t
Proof state after:
case pos
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
et : e ≥ t
⊢ a < b + e

case neg
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
et : ¬e ≥ t
⊢ a < b + e
Theorem: le_of_forall_small_le_add
Proof state before:
case pos
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
et : e ≥ t
⊢ a < b + e
Tactic:
specialize h (t/2) (by bound) (by bound)
Proof state after:
case pos
a b t : ℝ
tp : 0 < t
e : ℝ
ep : 0 < e
et : e ≥ t
h : a ≤ b + t / 2
⊢ a < b + e
Theorem: le_of_forall_small_le_add
Proof state before:
case pos
a b t : ℝ
tp : 0 < t
e : ℝ
ep : 0 < e
et : e ≥ t
h : a ≤ b + t / 2
⊢ a < b + e
Tactic:
calc a ≤ b + t/2 := h
  _ ≤ b + e/2 := by bound
  _ < b + e := by bound
Proof state after:
no goals
Theorem: le_of_forall_small_le_add
Proof state before:
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
et : e ≥ t
⊢ 0 < t / 2
Tactic:
bound
Proof state after:
no goals
Theorem: le_of_forall_small_le_add
Proof state before:
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
et : e ≥ t
⊢ t / 2 < t
Tactic:
bound
Proof state after:
no goals
Theorem: le_of_forall_small_le_add
Proof state before:
a b t : ℝ
tp : 0 < t
e : ℝ
ep : 0 < e
et : e ≥ t
h : a ≤ b + t / 2
⊢ b + t / 2 ≤ b + e / 2
Tactic:
bound
Proof state after:
no goals
Theorem: le_of_forall_small_le_add
Proof state before:
a b t : ℝ
tp : 0 < t
e : ℝ
ep : 0 < e
et : e ≥ t
h : a ≤ b + t / 2
⊢ b + e / 2 < b + e
Tactic:
bound
Proof state after:
no goals
Theorem: le_of_forall_small_le_add
Proof state before:
case neg
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
et : ¬e ≥ t
⊢ a < b + e
Tactic:
simp only [ge_iff_le, not_le] at et
Proof state after:
case neg
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
et : e < t
⊢ a < b + e
Theorem: le_of_forall_small_le_add
Proof state before:
case neg
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
et : e < t
⊢ a < b + e
Tactic:
calc a ≤ b + e/2 := h (e/2) (by bound) (by linarith)
  _ < b + e := by bound
Proof state after:
no goals
Theorem: le_of_forall_small_le_add
Proof state before:
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
et : e < t
⊢ 0 < e / 2
Tactic:
bound
Proof state after:
no goals
Theorem: le_of_forall_small_le_add
Proof state before:
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
et : e < t
⊢ e / 2 < t
Tactic:
linarith
Proof state after:
no goals
Theorem: le_of_forall_small_le_add
Proof state before:
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
et : e < t
⊢ b + e / 2 < b + e
Tactic:
bound
Proof state after:
no goals
Theorem: one_over_one_sub_le
Proof state before:
x : ℝ
⊢ 0 ≤ x → x ≤ 1 / 2 → 1 / (1 - x) ≤ 1 + 2 * x
Tactic:
intro xp xh
Proof state after:
x : ℝ
xp : 0 ≤ x
xh : x ≤ 1 / 2
⊢ 1 / (1 - x) ≤ 1 + 2 * x
Theorem: one_over_one_sub_le
Proof state before:
x : ℝ
xp : 0 ≤ x
xh : x ≤ 1 / 2
⊢ 1 / (1 - x) ≤ 1 + 2 * x
Tactic:
have x1 : 1 - x > 0 := by linarith
Proof state after:
x : ℝ
xp : 0 ≤ x
xh : x ≤ 1 / 2
x1 : 1 - x > 0
⊢ 1 / (1 - x) ≤ 1 + 2 * x
Theorem: one_over_one_sub_le
Proof state before:
x : ℝ
xp : 0 ≤ x
xh : x ≤ 1 / 2
x1 : 1 - x > 0
⊢ 1 / (1 - x) ≤ 1 + 2 * x
Tactic:
rw [div_le_iff x1]
Proof state after:
x : ℝ
xp : 0 ≤ x
xh : x ≤ 1 / 2
x1 : 1 - x > 0
⊢ 1 ≤ (1 + 2 * x) * (1 - x)
Theorem: one_over_one_sub_le
Proof state before:
x : ℝ
xp : 0 ≤ x
xh : x ≤ 1 / 2
x1 : 1 - x > 0
⊢ 1 ≤ (1 + 2 * x) * (1 - x)
Tactic:
calc (1 + 2*x) * (1 - x) = 1 + x * (1 - 2*x) := by ring
  _ ≥ 1 + x * (1 - 2 * (1/2)) := by bound
  _ = 1 := by ring
Proof state after:
no goals
Theorem: one_over_one_sub_le
Proof state before:
x : ℝ
xp : 0 ≤ x
xh : x ≤ 1 / 2
⊢ 1 - x > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: one_over_one_sub_le
Proof state before:
x : ℝ
xp : 0 ≤ x
xh : x ≤ 1 / 2
x1 : 1 - x > 0
⊢ (1 + 2 * x) * (1 - x) = 1 + x * (1 - 2 * x)
Tactic:
ring
Proof state after:
no goals
Theorem: one_over_one_sub_le
Proof state before:
x : ℝ
xp : 0 ≤ x
xh : x ≤ 1 / 2
x1 : 1 - x > 0
⊢ 1 + x * (1 - 2 * x) ≥ 1 + x * (1 - 2 * (1 / 2))
Tactic:
bound
Proof state after:
no goals
Theorem: one_over_one_sub_le
Proof state before:
x : ℝ
xp : 0 ≤ x
xh : x ≤ 1 / 2
x1 : 1 - x > 0
⊢ 1 + x * (1 - 2 * (1 / 2)) = 1
Tactic:
ring
Proof state after:
no goals
Theorem: Metric.continuous_near
Proof state before:
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
⊢ ∀ (e : ℝ), 0 < e → ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
Tactic:
intro e ep
Proof state after:
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
Theorem: Metric.continuous_near
Proof state before:
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
Tactic:
rcases Metric.continuousAt_iff.mp fc e ep with ⟨s,sp,sc⟩
Proof state after:
case intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, dist x z < s → dist (f x) (f z) < e
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
Theorem: Metric.continuous_near
Proof state before:
case intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, dist x z < s → dist (f x) (f z) < e
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
Tactic:
simp_rw [ Complex.dist_eq ] at sc
Proof state after:
case intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
Theorem: Metric.continuous_near
Proof state before:
case intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
Tactic:
by_cases sr : s ≤ r
Proof state after:
case pos
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : s ≤ r
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e

case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : ¬s ≤ r
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
Theorem: Metric.continuous_near
Proof state before:
case pos
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : s ≤ r
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e

case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : ¬s ≤ r
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
Tactic:
exists s
Proof state after:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : ¬s ≤ r
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
Theorem: Metric.continuous_near
Proof state before:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : ¬s ≤ r
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
Tactic:
simp only [not_le] at sr
Proof state after:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
Theorem: Metric.continuous_near
Proof state before:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
Tactic:
exists r
Proof state after:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
⊢ 0 < r ∧ r ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < r → Complex.abs (f w - f z) < e
Theorem: Metric.continuous_near
Proof state before:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
⊢ 0 < r ∧ r ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < r → Complex.abs (f w - f z) < e
Tactic:
refine ⟨rp, by bound, ?_⟩
Proof state after:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
⊢ ∀ {w : ℂ}, Complex.abs (w - z) < r → Complex.abs (f w - f z) < e
Theorem: Metric.continuous_near
Proof state before:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
⊢ ∀ {w : ℂ}, Complex.abs (w - z) < r → Complex.abs (f w - f z) < e
Tactic:
intro w wr
Proof state after:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
w : ℂ
wr : Complex.abs (w - z) < r
⊢ Complex.abs (f w - f z) < e
Theorem: Metric.continuous_near
Proof state before:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
w : ℂ
wr : Complex.abs (w - z) < r
⊢ Complex.abs (f w - f z) < e
Tactic:
refine @sc w ?_
Proof state after:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
w : ℂ
wr : Complex.abs (w - z) < r
⊢ Complex.abs (w - z) < s
Theorem: Metric.continuous_near
Proof state before:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
w : ℂ
wr : Complex.abs (w - z) < r
⊢ Complex.abs (w - z) < s
Tactic:
trans r
Proof state after:
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
w : ℂ
wr : Complex.abs (w - z) < r
⊢ Complex.abs (w - z) < r

f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
w : ℂ
wr : Complex.abs (w - z) < r
⊢ r < s
Theorem: Metric.continuous_near
Proof state before:
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
w : ℂ
wr : Complex.abs (w - z) < r
⊢ Complex.abs (w - z) < r

f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
w : ℂ
wr : Complex.abs (w - z) < r
⊢ r < s
Tactic:
assumption
Proof state after:
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
w : ℂ
wr : Complex.abs (w - z) < r
⊢ r < s
Theorem: Metric.continuous_near
Proof state before:
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
w : ℂ
wr : Complex.abs (w - z) < r
⊢ r < s
Tactic:
assumption
Proof state after:
no goals
Theorem: Metric.continuous_near
Proof state before:
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
⊢ r ≤ r
Tactic:
bound
Proof state after:
no goals
Theorem: slightly_smaller
Proof state before:
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Tactic:
by_cases rz : abs z < r
Proof state after:
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

case neg
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
Theorem: slightly_smaller
Proof state before:
case neg
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:
simp only [not_lt] at rz
Proof state after:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
⊢ ∃ 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
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Tactic:
have azp : 0 < abs z := Complex.abs.pos nz
Proof state after:
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