internlm/Lean-Github huggingface dataset:
Theorem: symmDiff_bound
Proof state before:
A B : Finset ℕ
f : ℕ → ℂ
⊢ dist ((A \ B).sum f + (A ∩ B).sum f) ((B \ A).sum f + (A ∩ B).sum f) ≤ (A ∆ B).sum fun n => Complex.abs (f n)
Tactic:
rw [dist_add_right ((A \ B).sum f) ((B \ A).sum f) ((A ∩ B).sum f)]
Proof state after:
A B : Finset ℕ
f : ℕ → ℂ
⊢ dist ((A \ B).sum f) ((B \ A).sum f) ≤ (A ∆ B).sum fun n => Complex.abs (f n)
Theorem: symmDiff_bound
Proof state before:
A B : Finset ℕ
f : ℕ → ℂ
⊢ dist ((A \ B).sum f) ((B \ A).sum f) ≤ (A ∆ B).sum fun n => Complex.abs (f n)
Tactic:
rw [Complex.dist_eq]
Proof state after:
A B : Finset ℕ
f : ℕ → ℂ
⊢ Complex.abs ((A \ B).sum f - (B \ A).sum f) ≤ (A ∆ B).sum fun n => Complex.abs (f n)
Theorem: symmDiff_bound
Proof state before:
A B : Finset ℕ
f : ℕ → ℂ
⊢ Complex.abs ((A \ B).sum f - (B \ A).sum f) ≤ (A ∆ B).sum fun n => Complex.abs (f n)
Tactic:
trans (A \ B).sum (fun n ↦ abs (f n)) + (B \ A).sum (fun n ↦ abs (f n))
Proof state after:
A B : Finset ℕ
f : ℕ → ℂ
⊢ Complex.abs ((A \ B).sum f - (B \ A).sum f) ≤
    ((A \ B).sum fun n => Complex.abs (f n)) + (B \ A).sum fun n => Complex.abs (f n)

A B : Finset ℕ
f : ℕ → ℂ
⊢ (((A \ B).sum fun n => Complex.abs (f n)) + (B \ A).sum fun n => Complex.abs (f n)) ≤
    (A ∆ B).sum fun n => Complex.abs (f n)
Theorem: symmDiff_bound
Proof state before:
A B : Finset ℕ
f : ℕ → ℂ
⊢ Complex.abs ((A \ B).sum f - (B \ A).sum f) ≤
    ((A \ B).sum fun n => Complex.abs (f n)) + (B \ A).sum fun n => Complex.abs (f n)
Tactic:
have ha := finset_complex_abs_sum_le (A \ B) f
Proof state after:
A B : Finset ℕ
f : ℕ → ℂ
ha : Complex.abs ((A \ B).sum fun n => f n) ≤ (A \ B).sum fun n => Complex.abs (f n)
⊢ Complex.abs ((A \ B).sum f - (B \ A).sum f) ≤
    ((A \ B).sum fun n => Complex.abs (f n)) + (B \ A).sum fun n => Complex.abs (f n)
Theorem: symmDiff_bound
Proof state before:
A B : Finset ℕ
f : ℕ → ℂ
ha : Complex.abs ((A \ B).sum fun n => f n) ≤ (A \ B).sum fun n => Complex.abs (f n)
⊢ Complex.abs ((A \ B).sum f - (B \ A).sum f) ≤
    ((A \ B).sum fun n => Complex.abs (f n)) + (B \ A).sum fun n => Complex.abs (f n)
Tactic:
have hb := finset_complex_abs_sum_le (B \ A) f
Proof state after:
A B : Finset ℕ
f : ℕ → ℂ
ha : Complex.abs ((A \ B).sum fun n => f n) ≤ (A \ B).sum fun n => Complex.abs (f n)
hb : Complex.abs ((B \ A).sum fun n => f n) ≤ (B \ A).sum fun n => Complex.abs (f n)
⊢ Complex.abs ((A \ B).sum f - (B \ A).sum f) ≤
    ((A \ B).sum fun n => Complex.abs (f n)) + (B \ A).sum fun n => Complex.abs (f n)
Theorem: symmDiff_bound
Proof state before:
A B : Finset ℕ
f : ℕ → ℂ
ha : Complex.abs ((A \ B).sum fun n => f n) ≤ (A \ B).sum fun n => Complex.abs (f n)
hb : Complex.abs ((B \ A).sum fun n => f n) ≤ (B \ A).sum fun n => Complex.abs (f n)
⊢ Complex.abs ((A \ B).sum f - (B \ A).sum f) ≤
    ((A \ B).sum fun n => Complex.abs (f n)) + (B \ A).sum fun n => Complex.abs (f n)
Tactic:
calc abs ((A \ B).sum f - (B \ A).sum f)
  _ ≤ abs ((A \ B).sum f) + abs ((B \ A).sum f) := by bound
  _ ≤ (A \ B).sum (fun n ↦ abs (f n)) + (B \ A).sum (fun n ↦ abs (f n)) := by bound
Proof state after:
no goals
Theorem: symmDiff_bound
Proof state before:
A B : Finset ℕ
f : ℕ → ℂ
ha : Complex.abs ((A \ B).sum fun n => f n) ≤ (A \ B).sum fun n => Complex.abs (f n)
hb : Complex.abs ((B \ A).sum fun n => f n) ≤ (B \ A).sum fun n => Complex.abs (f n)
⊢ Complex.abs ((A \ B).sum f - (B \ A).sum f) ≤ Complex.abs ((A \ B).sum f) + Complex.abs ((B \ A).sum f)
Tactic:
bound
Proof state after:
no goals
Theorem: symmDiff_bound
Proof state before:
A B : Finset ℕ
f : ℕ → ℂ
ha : Complex.abs ((A \ B).sum fun n => f n) ≤ (A \ B).sum fun n => Complex.abs (f n)
hb : Complex.abs ((B \ A).sum fun n => f n) ≤ (B \ A).sum fun n => Complex.abs (f n)
⊢ Complex.abs ((A \ B).sum f) + Complex.abs ((B \ A).sum f) ≤
    ((A \ B).sum fun n => Complex.abs (f n)) + (B \ A).sum fun n => Complex.abs (f n)
Tactic:
bound
Proof state after:
no goals
Theorem: symmDiff_bound
Proof state before:
A B : Finset ℕ
f : ℕ → ℂ
⊢ (((A \ B).sum fun n => Complex.abs (f n)) + (B \ A).sum fun n => Complex.abs (f n)) ≤
    (A ∆ B).sum fun n => Complex.abs (f n)
Tactic:
apply le_of_eq
Proof state after:
case a
A B : Finset ℕ
f : ℕ → ℂ
⊢ (((A \ B).sum fun n => Complex.abs (f n)) + (B \ A).sum fun n => Complex.abs (f n)) =
    (A ∆ B).sum fun n => Complex.abs (f n)
Theorem: symmDiff_bound
Proof state before:
case a
A B : Finset ℕ
f : ℕ → ℂ
⊢ (((A \ B).sum fun n => Complex.abs (f n)) + (B \ A).sum fun n => Complex.abs (f n)) =
    (A ∆ B).sum fun n => Complex.abs (f n)
Tactic:
rw [←Finset.sum_union (sdiff_sdiff_disjoint A B), symmDiff_union]
Proof state after:
no goals
Theorem: symmDiff_late
Proof state before:
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
⊢ Late (A ∆ B) m
Tactic:
intro n ab
Proof state after:
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
ab : n ∈ A ∆ B
⊢ n ≥ m
Theorem: symmDiff_late
Proof state before:
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
ab : n ∈ A ∆ B
⊢ n ≥ m
Tactic:
rw [symmDiff_def, Finset.sup_eq_union, Finset.mem_union] at ab
Proof state after:
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
ab : n ∈ A \ B ∨ n ∈ B \ A
⊢ n ≥ m
Theorem: symmDiff_late
Proof state before:
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
ab : n ∈ A \ B ∨ n ∈ B \ A
⊢ n ≥ m
Tactic:
by_contra h
Proof state after:
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
ab : n ∈ A \ B ∨ n ∈ B \ A
h : ¬n ≥ m
⊢ False
Theorem: symmDiff_late
Proof state before:
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
ab : n ∈ A \ B ∨ n ∈ B \ A
h : ¬n ≥ m
⊢ False
Tactic:
simp at h
Proof state after:
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
ab : n ∈ A \ B ∨ n ∈ B \ A
h : n < m
⊢ False
Theorem: symmDiff_late
Proof state before:
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
ab : n ∈ A \ B ∨ n ∈ B \ A
h : n < m
⊢ False
Tactic:
cases' ab with a b
Proof state after:
case inl
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h : n < m
a : n ∈ A \ B
⊢ False

case inr
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h : n < m
b : n ∈ B \ A
⊢ False
Theorem: symmDiff_late
Proof state before:
case inl
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h : n < m
a : n ∈ A \ B
⊢ False
Tactic:
rw [Finset.mem_sdiff] at a
Proof state after:
case inl
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h : n < m
a : n ∈ A ∧ n ∉ B
⊢ False
Theorem: symmDiff_late
Proof state before:
case inl
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h : n < m
a : n ∈ A ∧ n ∉ B
⊢ False
Tactic:
have h := Finset.mem_of_subset hb (Finset.mem_range.mpr h)
Proof state after:
case inl
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h✝ : n < m
a : n ∈ A ∧ n ∉ B
h : n ∈ B
⊢ False
Theorem: symmDiff_late
Proof state before:
case inl
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h✝ : n < m
a : n ∈ A ∧ n ∉ B
h : n ∈ B
⊢ False
Tactic:
exact a.2 h
Proof state after:
no goals
Theorem: symmDiff_late
Proof state before:
case inr
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h : n < m
b : n ∈ B \ A
⊢ False
Tactic:
rw [Finset.mem_sdiff] at b
Proof state after:
case inr
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h : n < m
b : n ∈ B ∧ n ∉ A
⊢ False
Theorem: symmDiff_late
Proof state before:
case inr
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h : n < m
b : n ∈ B ∧ n ∉ A
⊢ False
Tactic:
have h := Finset.mem_of_subset ha (Finset.mem_range.mpr h)
Proof state after:
case inr
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h✝ : n < m
b : n ∈ B ∧ n ∉ A
h : n ∈ A
⊢ False
Theorem: symmDiff_late
Proof state before:
case inr
A B : Finset ℕ
m : ℕ
ha : A ≥ Finset.range m
hb : B ≥ Finset.range m
n : ℕ
h✝ : n < m
b : n ∈ B ∧ n ∉ A
h : n ∈ A
⊢ False
Tactic:
exact b.2 h
Proof state after:
no goals
Theorem: sub_near
Proof state before:
a z : ℂ
⊢ |Complex.abs (a - z) - Complex.abs a| ≤ Complex.abs z
Tactic:
rw [abs_le]
Proof state after:
a z : ℂ
⊢ -Complex.abs z ≤ Complex.abs (a - z) - Complex.abs a ∧ Complex.abs (a - z) - Complex.abs a ≤ Complex.abs z
Theorem: sub_near
Proof state before:
a z : ℂ
⊢ -Complex.abs z ≤ Complex.abs (a - z) - Complex.abs a ∧ Complex.abs (a - z) - Complex.abs a ≤ Complex.abs z
Tactic:
constructor
Proof state after:
case left
a z : ℂ
⊢ -Complex.abs z ≤ Complex.abs (a - z) - Complex.abs a

case right
a z : ℂ
⊢ Complex.abs (a - z) - Complex.abs a ≤ Complex.abs z
Theorem: sub_near
Proof state before:
case left
a z : ℂ
⊢ -Complex.abs z ≤ Complex.abs (a - z) - Complex.abs a
Tactic:
simp only [neg_le_sub_iff_le_add]
Proof state after:
case left
a z : ℂ
⊢ Complex.abs a ≤ Complex.abs (a - z) + Complex.abs z
Theorem: sub_near
Proof state before:
case left
a z : ℂ
⊢ Complex.abs a ≤ Complex.abs (a - z) + Complex.abs z
Tactic:
calc abs (a - z) + abs z
  _ ≥ |abs a - abs z| + abs z := by bound
  _ ≥ abs a - abs z + abs z := by bound
  _ = abs a := by simp only [sub_add_cancel]
Proof state after:
no goals
Theorem: sub_near
Proof state before:
a z : ℂ
⊢ Complex.abs (a - z) + Complex.abs z ≥ |Complex.abs a - Complex.abs z| + Complex.abs z
Tactic:
bound
Proof state after:
no goals
Theorem: sub_near
Proof state before:
a z : ℂ
⊢ |Complex.abs a - Complex.abs z| + Complex.abs z ≥ Complex.abs a - Complex.abs z + Complex.abs z
Tactic:
bound
Proof state after:
no goals
Theorem: sub_near
Proof state before:
a z : ℂ
⊢ Complex.abs a - Complex.abs z + Complex.abs z = Complex.abs a
Tactic:
simp only [sub_add_cancel]
Proof state after:
no goals
Theorem: sub_near
Proof state before:
case right
a z : ℂ
⊢ Complex.abs (a - z) - Complex.abs a ≤ Complex.abs z
Tactic:
calc
  abs (a - z) - abs a ≤ abs a + abs z - abs a := by bound
  _ = abs z := by simp only [add_sub_cancel_left]
Proof state after:
no goals
Theorem: sub_near
Proof state before:
a z : ℂ
⊢ Complex.abs (a - z) - Complex.abs a ≤ Complex.abs a + Complex.abs z - Complex.abs a
Tactic:
bound
Proof state after:
no goals
Theorem: sub_near
Proof state before:
a z : ℂ
⊢ Complex.abs a + Complex.abs z - Complex.abs a = Complex.abs z
Tactic:
simp only [add_sub_cancel_left]
Proof state after:
no goals
Theorem: add_near
Proof state before:
a z : ℂ
⊢ |Complex.abs (a + z) - Complex.abs a| ≤ Complex.abs z
Tactic:
have h := sub_near a (-z)
Proof state after:
a z : ℂ
h : |Complex.abs (a - -z) - Complex.abs a| ≤ Complex.abs (-z)
⊢ |Complex.abs (a + z) - Complex.abs a| ≤ Complex.abs z
Theorem: add_near
Proof state before:
a z : ℂ
h : |Complex.abs (a - -z) - Complex.abs a| ≤ Complex.abs (-z)
⊢ |Complex.abs (a + z) - Complex.abs a| ≤ Complex.abs z
Tactic:
simp only [sub_neg_eq_add, map_neg_eq_map] at h
Proof state after:
a z : ℂ
h : |Complex.abs (a + z) - Complex.abs a| ≤ Complex.abs z
⊢ |Complex.abs (a + z) - Complex.abs a| ≤ Complex.abs z
Theorem: add_near
Proof state before:
a z : ℂ
h : |Complex.abs (a + z) - Complex.abs a| ≤ Complex.abs z
⊢ |Complex.abs (a + z) - Complex.abs a| ≤ Complex.abs z
Tactic:
assumption
Proof state after:
no goals
Theorem: mem_slitPlane_of_near_one
Proof state before:
z : ℂ
⊢ Complex.abs (z - 1) < 1 → z ∈ slitPlane
Tactic:
intro h
Proof state after:
z : ℂ
h : Complex.abs (z - 1) < 1
⊢ z ∈ slitPlane
Theorem: mem_slitPlane_of_near_one
Proof state before:
z : ℂ
h : Complex.abs (z - 1) < 1
⊢ z ∈ slitPlane
Tactic:
apply Or.inl
Proof state after:
case h
z : ℂ
h : Complex.abs (z - 1) < 1
⊢ 0 < z.re
Theorem: mem_slitPlane_of_near_one
Proof state before:
case h
z : ℂ
h : Complex.abs (z - 1) < 1
⊢ 0 < z.re
Tactic:
have hr : (1 - z).re < 1 := by
  calc
    (1 - z).re ≤ |(1 - z).re| := le_abs_self (1 - z).re
    _ ≤ abs (1 - z) := (Complex.abs_re_le_abs _)
    _ = abs (z - 1) := by rw [←Complex.abs.map_neg (1 - z)]; simp only [neg_sub]
    _ < 1 := h
Proof state after:
case h
z : ℂ
h : Complex.abs (z - 1) < 1
hr : (1 - z).re < 1
⊢ 0 < z.re
Theorem: mem_slitPlane_of_near_one
Proof state before:
case h
z : ℂ
h : Complex.abs (z - 1) < 1
hr : (1 - z).re < 1
⊢ 0 < z.re
Tactic:
simp only [Complex.sub_re, Complex.one_re, sub_lt_self_iff] at hr
Proof state after:
case h
z : ℂ
h : Complex.abs (z - 1) < 1
hr : 0 < z.re
⊢ 0 < z.re
Theorem: mem_slitPlane_of_near_one
Proof state before:
case h
z : ℂ
h : Complex.abs (z - 1) < 1
hr : 0 < z.re
⊢ 0 < z.re
Tactic:
assumption
Proof state after:
no goals
Theorem: mem_slitPlane_of_near_one
Proof state before:
z : ℂ
h : Complex.abs (z - 1) < 1
⊢ (1 - z).re < 1
Tactic:
calc
  (1 - z).re ≤ |(1 - z).re| := le_abs_self (1 - z).re
  _ ≤ abs (1 - z) := (Complex.abs_re_le_abs _)
  _ = abs (z - 1) := by rw [←Complex.abs.map_neg (1 - z)]; simp only [neg_sub]
  _ < 1 := h
Proof state after:
no goals
Theorem: mem_slitPlane_of_near_one
Proof state before:
z : ℂ
h : Complex.abs (z - 1) < 1
⊢ Complex.abs (1 - z) = Complex.abs (z - 1)
Tactic:
rw [←Complex.abs.map_neg (1 - z)]
Proof state after:
z : ℂ
h : Complex.abs (z - 1) < 1
⊢ Complex.abs (-(1 - z)) = Complex.abs (z - 1)
Theorem: mem_slitPlane_of_near_one
Proof state before:
z : ℂ
h : Complex.abs (z - 1) < 1
⊢ Complex.abs (-(1 - z)) = Complex.abs (z - 1)
Tactic:
simp only [neg_sub]
Proof state after:
no goals
Theorem: near_one_avoids_zero
Proof state before:
z : ℂ
⊢ Complex.abs (z - 1) < 1 → z ≠ 0
Tactic:
intro h
Proof state after:
z : ℂ
h : Complex.abs (z - 1) < 1
⊢ z ≠ 0
Theorem: near_one_avoids_zero
Proof state before:
z : ℂ
h : Complex.abs (z - 1) < 1
⊢ z ≠ 0
Tactic:
exact Complex.slitPlane_ne_zero (mem_slitPlane_of_near_one h)
Proof state after:
no goals
Theorem: derivWithin.clog
Proof state before:
f : ℂ → ℂ
z : ℂ
s : Set ℂ
o : IsOpen s
zs : z ∈ s
hf : DifferentiableWithinAt ℂ f s z
hx : (f z).re > 0 ∨ (f z).im ≠ 0
⊢ derivWithin (fun z => (f z).log) s z = derivWithin f s z / f z
Tactic:
have hz := DifferentiableWithinAt.hasDerivWithinAt hf
Proof state after:
f : ℂ → ℂ
z : ℂ
s : Set ℂ
o : IsOpen s
zs : z ∈ s
hf : DifferentiableWithinAt ℂ f s z
hx : (f z).re > 0 ∨ (f z).im ≠ 0
hz : HasDerivWithinAt f (derivWithin f s z) s z
⊢ derivWithin (fun z => (f z).log) s z = derivWithin f s z / f z
Theorem: derivWithin.clog
Proof state before:
f : ℂ → ℂ
z : ℂ
s : Set ℂ
o : IsOpen s
zs : z ∈ s
hf : DifferentiableWithinAt ℂ f s z
hx : (f z).re > 0 ∨ (f z).im ≠ 0
hz : HasDerivWithinAt f (derivWithin f s z) s z
⊢ derivWithin (fun z => (f z).log) s z = derivWithin f s z / f z
Tactic:
have h := HasDerivWithinAt.clog hz hx
Proof state after:
f : ℂ → ℂ
z : ℂ
s : Set ℂ
o : IsOpen s
zs : z ∈ s
hf : DifferentiableWithinAt ℂ f s z
hx : (f z).re > 0 ∨ (f z).im ≠ 0
hz : HasDerivWithinAt f (derivWithin f s z) s z
h : HasDerivWithinAt (fun t => (f t).log) (derivWithin f s z / f z) s z
⊢ derivWithin (fun z => (f z).log) s z = derivWithin f s z / f z
Theorem: derivWithin.clog
Proof state before:
f : ℂ → ℂ
z : ℂ
s : Set ℂ
o : IsOpen s
zs : z ∈ s
hf : DifferentiableWithinAt ℂ f s z
hx : (f z).re > 0 ∨ (f z).im ≠ 0
hz : HasDerivWithinAt f (derivWithin f s z) s z
h : HasDerivWithinAt (fun t => (f t).log) (derivWithin f s z / f z) s z
⊢ derivWithin (fun z => (f z).log) s z = derivWithin f s z / f z
Tactic:
have u := o.uniqueDiffWithinAt (𝕜 := ℂ) zs
Proof state after:
f : ℂ → ℂ
z : ℂ
s : Set ℂ
o : IsOpen s
zs : z ∈ s
hf : DifferentiableWithinAt ℂ f s z
hx : (f z).re > 0 ∨ (f z).im ≠ 0
hz : HasDerivWithinAt f (derivWithin f s z) s z
h : HasDerivWithinAt (fun t => (f t).log) (derivWithin f s z / f z) s z
u : UniqueDiffWithinAt ℂ s z
⊢ derivWithin (fun z => (f z).log) s z = derivWithin f s z / f z
Theorem: derivWithin.clog
Proof state before:
f : ℂ → ℂ
z : ℂ
s : Set ℂ
o : IsOpen s
zs : z ∈ s
hf : DifferentiableWithinAt ℂ f s z
hx : (f z).re > 0 ∨ (f z).im ≠ 0
hz : HasDerivWithinAt f (derivWithin f s z) s z
h : HasDerivWithinAt (fun t => (f t).log) (derivWithin f s z / f z) s z
u : UniqueDiffWithinAt ℂ s z
⊢ derivWithin (fun z => (f z).log) s z = derivWithin f s z / f z
Tactic:
rw [HasDerivWithinAt.derivWithin h u]
Proof state after:
no goals
Theorem: weak_log1p_small
Proof state before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
by_cases rp : r ≤ 0
Proof state after:
case pos
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : r ≤ 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z

case neg
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : ¬r ≤ 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Theorem: weak_log1p_small
Proof state before:
case pos
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : r ≤ 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
have a0 : abs z < 0 := lt_of_lt_of_le h rp
Proof state after:
case pos
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : r ≤ 0
a0 : Complex.abs z < 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Theorem: weak_log1p_small
Proof state before:
case pos
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : r ≤ 0
a0 : Complex.abs z < 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
have a0' : abs z ≥ 0 := by bound
Proof state after:
case pos
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : r ≤ 0
a0 : Complex.abs z < 0
a0' : Complex.abs z ≥ 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Theorem: weak_log1p_small
Proof state before:
case pos
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : r ≤ 0
a0 : Complex.abs z < 0
a0' : Complex.abs z ≥ 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
exfalso
Proof state after:
case pos
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : r ≤ 0
a0 : Complex.abs z < 0
a0' : Complex.abs z ≥ 0
⊢ False
Theorem: weak_log1p_small
Proof state before:
case pos
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : r ≤ 0
a0 : Complex.abs z < 0
a0' : Complex.abs z ≥ 0
⊢ False
Tactic:
linarith [a0, a0']
Proof state after:
no goals
Theorem: weak_log1p_small
Proof state before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : r ≤ 0
a0 : Complex.abs z < 0
⊢ Complex.abs z ≥ 0
Tactic:
bound
Proof state after:
no goals
Theorem: weak_log1p_small
Proof state before:
case neg
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : ¬r ≤ 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
simp only [not_le] at rp
Proof state after:
case neg
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Theorem: weak_log1p_small
Proof state before:
case neg
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
L : ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
simp only [Complex.log_one, sub_zero, Complex.norm_eq_abs, one_div, add_sub_cancel_left] at L
Proof state after:
case neg
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
L : Complex.abs (1 + z).log ≤ (1 - r)⁻¹ * Complex.abs z
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Theorem: weak_log1p_small
Proof state before:
case neg
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
L : Complex.abs (1 + z).log ≤ (1 - r)⁻¹ * Complex.abs z
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
simpa only [one_div, ge_iff_le]
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
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖
Tactic:
generalize hs : Metric.ball (1:ℂ) r = s
Proof state after:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖
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
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖
Tactic:
have o : IsOpen s := by rw [← hs]; exact Metric.isOpen_ball
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
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖
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).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖
Tactic:
have s1z : 1 + z ∈ s := by simp [← hs]; assumption
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
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖
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 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖
Tactic:
have s1 : (1:ℂ) ∈ s := by simp [← hs]; assumption
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
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖
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
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖
Tactic:
have sp : ∀ w : ℂ, w ∈ s → w.re > 0 ∨ w.im ≠ 0 := by
  intro w ws
  apply mem_slitPlane_of_near_one
  simp only [Metric.mem_ball, Complex.dist_eq, ← hs] at ws
  calc abs (w - 1) < r := by assumption
    _ < 1 := r1
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
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖
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
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖
Tactic:
have sa : ∀ w : ℂ, w ∈ s → abs w ≥ 1 - r := by
  intro w ws
  simp only [Metric.mem_ball, Complex.dist_eq, ← hs] at ws
  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:
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
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖
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
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖
Tactic:
refine Convex.norm_image_sub_le_of_norm_derivWithin_le ?_ ?_ ?_ s1 s1z
Proof state after:
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

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)

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
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
⊢ IsOpen s
Tactic:
rw [← 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
⊢ IsOpen (Metric.ball 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
⊢ IsOpen (Metric.ball 1 r)
Tactic:
exact Metric.isOpen_ball
Proof state after:
no goals